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();
A2: { 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 A3: x in { F₃(w) where w is Element of F₁() : w in F₂() } ; :: thesis: x in rng f
consider w being Element of F₁() such that
A4: x = F₃(w) and
A5: w in F₂() by A3;
A6: f . w = x by A1, A4, A5;
thus x in rng f by A1, A5, A6, FUNCT_1:def 5; :: thesis: verum

end;

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