per cases
( len f > 0 or not len f > 0 )
;

end;

suppose
len f > 0
; :: thesis: ( ( len f > 0 implies f . (len f) is Element of CQC-WFF Al ) & ( not len f > 0 implies VERUM Al is Element of CQC-WFF Al ) )

then
0 + 1 <= len f
by NAT_1:13;

then len f in dom f by FINSEQ_3:25;

then f . (len f) in rng f by FUNCT_1:3;

hence ( ( len f > 0 implies f . (len f) is Element of CQC-WFF Al ) & ( not len f > 0 implies VERUM Al is Element of CQC-WFF Al ) ) ; :: thesis: verum

end;then len f in dom f by FINSEQ_3:25;

then f . (len f) in rng f by FUNCT_1:3;

hence ( ( len f > 0 implies f . (len f) is Element of CQC-WFF Al ) & ( not len f > 0 implies VERUM Al is Element of CQC-WFF Al ) ) ; :: thesis: verum

suppose A1:
not len f > 0
; :: thesis: ( ( len f > 0 implies f . (len f) is Element of CQC-WFF Al ) & ( not len f > 0 implies VERUM Al is Element of CQC-WFF Al ) )

thus
( ( len f > 0 implies f . (len f) is Element of CQC-WFF Al ) & ( not len f > 0 implies VERUM Al is Element of CQC-WFF Al ) )
by A1; :: thesis: verum

end;