0 <= len f by NAT_1:2;
then 0 + 1 <= len f by A1, NAT_1:13;
then A4: len f in Seg (len f) by FINSEQ_1:3;
Seg (len f) = dom f by FINSEQ_1:def 3;
then A6: f . (len f) in rng f by A4, FUNCT_1:def 5;
rng f c= [:CQC-WFF ,Proof_Step_Kinds :] by FINSEQ_1:def 4;
hence (f . (len f)) `1 is Element of CQC-WFF by A6, MCART_1:10; :: thesis: verum