consider f being Function such that
A1: ( dom f = F₂() & ( for x being set st x in F₂() holds
f . x = F₃(x) ) ) from FUNCT_1:sch 3();
{ F₃(w) where w is Element of F₁() : w in F₂() } c= rng f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { F₃(w) where w is Element of F₁() : w in F₂() } or x in rng f )
assume x in { F₃(w) where w is Element of F₁() : w in F₂() } ; :: thesis: x in rng f
then consider w being Element of F₁() such that
A2: x = F₃(w) and
A3: w in F₂() ;
f . w = x by A1, A2, A3;
hence x in rng f by A1, A3, FUNCT_1:def 3; :: thesis: verum

end;

hence card { F₃(w) where w is Element of F₁() : w in F₂() } c= card F₂() by A1, CARD_1:12; :: thesis: verum