( 1 <= len f implies ex p being Element of CQC-WFF st p = f . 1 )

proof

assume 1 <= len f ; :: thesis: ex p being Element of CQC-WFF st p = f . 1
then 1 in dom f by FINSEQ_3:27;
then f . 1 in CQC-WFF by FINSEQ_2:13;
hence ex p being Element of CQC-WFF st p = f . 1 ; :: thesis: verum

end;

hence ( ( 1 <= len f implies ex b₁ being Element of CQC-WFF st b₁ = f . 1 ) & ( not 1 <= len f implies ex b₁ being Element of CQC-WFF st b₁ = VERUM ) ) ; :: thesis: verum