( QC-WFF is Subset of ([:NAT,NAT:] *) & p in QC-WFF ) by Def9, Th21;
hence p is FinSequence of [:NAT,NAT:] by FINSEQ_1:def 11; :: thesis: verum