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