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