set M = { F₃(w) where w is Element of F₁() : w in F₂() } ;
consider f being Function such that
A2: dom f = F₂() /\ F₁() and
A3: for y being set st y in F₂() /\ F₁() holds
f . y = F₃(y) from FUNCT_1:sch 3();
{ F₃(w) where w is Element of F₁() : w in F₂() } = f .: F₂()

proof

thus { F₃(w) where w is Element of F₁() : w in F₂() } c= f .: F₂() :: according to XBOOLE_0:def 10 :: thesis: f .: F₂() c= { F₃(w) where w is Element of F₁() : w in 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 f .: F₂() )
assume x in { F₃(w) where w is Element of F₁() : w in F₂() } ; :: thesis: x in f .: F₂()
then consider u being Element of F₁() such that
A4: x = F₃(u) and
A5: u in F₂() ;
A6: u in dom f by A2, A5, XBOOLE_0:def 4;
then f . u = F₃(u) by A2, A3;
hence x in f .: F₂() by A4, A5, A6, FUNCT_1:def 12; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in f .: F₂() or x in { F₃(w) where w is Element of F₁() : w in F₂() } )
assume x in f .: F₂() ; :: thesis: x in { F₃(w) where w is Element of F₁() : w in F₂() }
then consider y being set such that
A7: y in dom f and
A8: y in F₂() and
A9: x = f . y by FUNCT_1:def 12;
reconsider y = y as Element of F₁() by A2, A7, XBOOLE_0:def 4;
x = F₃(y) by A2, A3, A7, A9;
hence x in { F₃(w) where w is Element of F₁() : w in F₂() } by A8; :: thesis: verum

end;

hence { F₃(w) where w is Element of F₁() : w in F₂() } is finite by A1; :: thesis: verum