A2: F₁() is finite ;
set Z = { F₃(w) where w is Element of F₁() : w in F₁() } ;
{ F₃(w) where w is Element of F₁() : w in F₁() } is finite from FRAENKEL:sch 21(A2);
then reconsider Z = { F₃(w) where w is Element of F₁() : w in F₁() } as finite set ;
A3: Z = { F₃(w) where w is Element of F₁() : w in F₁() } ;
A4: card Z <= card F₁() from TREES_2:sch 3(A3);
F₂() c= Z

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in F₂() or x in Z )
assume x in F₂() ; :: thesis: x in Z
then ex w being Element of F₁() st
( x = F₃(w) & P₁[w] ) by A1;
hence x in Z ; :: thesis: verum

end;

then card F₂() <= card Z by NAT_1:43;
hence card F₂() <= card F₁() by A4, XXREAL_0:2; :: thesis: verum