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

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