( 1 <= len f implies ex p being Element of CQC-WFF Al st p = f . 1 )
_{1} being Element of CQC-WFF Al st b_{1} = f . 1 ) & ( not 1 <= len f implies ex b_{1} being Element of CQC-WFF Al st b_{1} = VERUM Al ) )
; :: thesis: verum

proof

hence
( ( 1 <= len f implies ex b
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;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