set f = the Enumeration of F;
deffunc H₃( Nat) -> Element of LTLB_WFF = ( the Enumeration of F /. F) ^ ;
consider g being FinSequence of LTLB_WFF such that
A1: ( len g = len the Enumeration of F & ( for j being Nat st j in dom g holds
g . j = H₃(j) ) ) from FINSEQ_2:sch 1();
F ^ c= rng g

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F ^ or x in rng g )
assume x in F ^ ; :: thesis: x in rng g
then consider P being PNPair such that
A2: P ^ = x and
A3: P in F ;
A4: P in rng the Enumeration of F by RLAFFIN3:def 1, A3;
then A5: P .. the Enumeration of F in dom the Enumeration of F by FINSEQ_4:20;
then A6: the Enumeration of F /. (P .. the Enumeration of F) = the Enumeration of F . (P .. the Enumeration of F) by PARTFUN1:def 6
.= P by FINSEQ_4:19, A4 ;
A7: P .. the Enumeration of F in dom g by A5, A1, FINSEQ_3:29;
then g . (P .. the Enumeration of F) in rng g by FUNCT_1:3;
hence x in rng g by A1, A7, A6, A2; :: thesis: verum

end;

hence F ^ is finite ; :: thesis: verum