( 1 <= len f implies ex p being Element of CQC-WFF Al st p = f . 1 )
proof
assume 1 <= len f ; :: thesis: ex p being Element of CQC-WFF Al st p = f . 1
then 1 in dom f by FINSEQ_3:25;
then f . 1 in CQC-WFF Al by FINSEQ_2:11;
hence ex p being Element of CQC-WFF Al st p = f . 1 ; :: thesis: verum
end;
hence ( ( 1 <= len f implies ex b1 being Element of CQC-WFF Al st b1 = f . 1 ) & ( not 1 <= len f implies ex b1 being Element of CQC-WFF Al st b1 = VERUM Al ) ) ; :: thesis: verum