( 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