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

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;

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;

end;