set M = { F₃(w) where w is Element of F₁() : w in F₂() } ;

per cases ( F₁() is empty or not F₁() is empty ) ;

suppose A2: F₁() is empty ; :: thesis: { F₃(w) where w is Element of F₁() : w in F₂() } is countable

{ F₃(w) where w is Element of F₁() : w in F₂() } c= {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₂() } or x in {F₃({})} )
assume x in { F₃(w) where w is Element of F₁() : w in F₂() } ; :: thesis: x in {F₃({})}
then consider w being Element of F₁() such that
A3: ( x = F₃(w) & w in F₂() ) ;
w = {} by A2, SUBSET_1:def 1;
hence x in {F₃({})} by A3, TARSKI:def 1; :: thesis: verum

end;

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

end;

suppose A4: not F₁() is empty ; :: thesis: { F₃(w) where w is Element of F₁() : w in F₂() } is countable

consider f being Function such that
A5: dom f = F₂() /\ F₁() and
A6: for y being object 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 object ; :: 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
A7: x = F₃(u) and
A8: u in F₂() ;
A9: u in dom f by A4, A5, A8, XBOOLE_0:def 4;
then f . u = F₃(u) by A5, A6;
hence x in f .: F₂() by A7, A8, A9, FUNCT_1:def 6; :: thesis: verum

end;

let x be object ; :: 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 object such that
A10: y in dom f and
A11: y in F₂() and
A12: x = f . y by FUNCT_1:def 6;
reconsider y = y as Element of F₁() by A5, A10, XBOOLE_0:def 4;
x = F₃(y) by A5, A6, A10, A12;
hence x in { F₃(w) where w is Element of F₁() : w in F₂() } by A11; :: thesis: verum

end;

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

end;

end;