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