let p be Element of MC-wff ; :: thesis: p is FinSequence-like
( MC-wff c= NAT * & p in MC-wff ) by Def7;
hence p is FinSequence-like by FINSEQ_1:def 11; :: thesis: verum