Metamath Proof Explorer


Syntax definition cseq

Description: Extend class notation with recursive sequence builder.

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