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