consider f being Function such that
A1: ( dom f = F₂() & ( for x being object 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₂() & P₁[w] ) } c= rng f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F₃(w) where w is Element of F₁() : ( w in F₂() & P₁[w] ) } or x in rng f )
assume x in { F₃(w) where w is Element of F₁() : ( w in F₂() & P₁[w] ) } ; :: thesis: x in rng f
then consider w being Element of F₁() such that
A2: x = F₃(w) and
A3: w in F₂() and
P₁[w] ;
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₂() & P₁[w] ) } c= card F₂() by A1, CARD_1:12; :: thesis: verum