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