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