Syntax Definition cseq 9211

Description: Extend class notation with recursive sequence builder.

Hypotheses

Ref	Expression
c.pl	class .+
cS	class S
cF	class F
cM	class M

Assertion

Ref	Expression
cseq	class seq M ( .+ , F , S )

See definition df-iseq 9212 for more information.