( 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 b₁ being Element of CQC-WFF Al st b₁ = f . 1 ) & ( not 1 <= len f implies ex b₁ being Element of CQC-WFF Al st b₁ = VERUM Al ) ) ; :: thesis: verum