set M = { F_{3}(w) where w is Element of F_{1}() : w in F_{2}() } ;

per cases
( F_{1}() is empty or not F_{1}() is empty )
;

end;

suppose A2:
F_{1}() is empty
; :: thesis: { F_{3}(w) where w is Element of F_{1}() : w in F_{2}() } is finite

{ F_{3}(w) where w is Element of F_{1}() : w in F_{2}() } c= {F_{3}({})}
_{3}(w) where w is Element of F_{1}() : w in F_{2}() } is finite
; :: thesis: verum

end;proof

hence
{ F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F_{3}(w) where w is Element of F_{1}() : w in F_{2}() } or x in {F_{3}({})} )

assume x in { F_{3}(w) where w is Element of F_{1}() : w in F_{2}() }
; :: thesis: x in {F_{3}({})}

then consider w being Element of F_{1}() such that

A3: ( x = F_{3}(w) & w in F_{2}() )
;

w = {} by A2, SUBSET_1:def 1;

hence x in {F_{3}({})}
by A3, TARSKI:def 1; :: thesis: verum

end;assume x in { F

then consider w being Element of F

A3: ( x = F

w = {} by A2, SUBSET_1:def 1;

hence x in {F

suppose A4:
not F_{1}() is empty
; :: thesis: { F_{3}(w) where w is Element of F_{1}() : w in F_{2}() } is finite

consider f being Function such that

A5: dom f = F_{2}() /\ F_{1}()
and

A6: for y being object st y in F_{2}() /\ F_{1}() holds

f . y = F_{3}(y)
from FUNCT_1:sch 3();

{ F_{3}(w) where w is Element of F_{1}() : w in F_{2}() } = f .: F_{2}()
_{3}(w) where w is Element of F_{1}() : w in F_{2}() } is finite
by A1; :: thesis: verum

end;A5: dom f = F

A6: for y being object st y in F

f . y = F

{ F

proof

hence
{ F
thus
{ F_{3}(w) where w is Element of F_{1}() : w in F_{2}() } c= f .: F_{2}()
:: according to XBOOLE_0:def 10 :: thesis: f .: F_{2}() c= { F_{3}(w) where w is Element of F_{1}() : w in F_{2}() } _{2}() or x in { F_{3}(w) where w is Element of F_{1}() : w in F_{2}() } )

assume x in f .: F_{2}()
; :: thesis: x in { F_{3}(w) where w is Element of F_{1}() : w in F_{2}() }

then consider y being object such that

A10: y in dom f and

A11: y in F_{2}()
and

A12: x = f . y by FUNCT_1:def 6;

reconsider y = y as Element of F_{1}() by A5, A10, XBOOLE_0:def 4;

x = F_{3}(y)
by A5, A6, A10, A12;

hence x in { F_{3}(w) where w is Element of F_{1}() : w in F_{2}() }
by A11; :: thesis: verum

end;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in f .: F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F_{3}(w) where w is Element of F_{1}() : w in F_{2}() } or x in f .: F_{2}() )

assume x in { F_{3}(w) where w is Element of F_{1}() : w in F_{2}() }
; :: thesis: x in f .: F_{2}()

then consider u being Element of F_{1}() such that

A7: x = F_{3}(u)
and

A8: u in F_{2}()
;

A9: u in dom f by A4, A5, A8, XBOOLE_0:def 4;

then f . u = F_{3}(u)
by A5, A6;

hence x in f .: F_{2}()
by A7, A8, A9, FUNCT_1:def 6; :: thesis: verum

end;assume x in { F

then consider u being Element of F

A7: x = F

A8: u in F

A9: u in dom f by A4, A5, A8, XBOOLE_0:def 4;

then f . u = F

hence x in f .: F

assume x in f .: F

then consider y being object such that

A10: y in dom f and

A11: y in F

A12: x = f . y by FUNCT_1:def 6;

reconsider y = y as Element of F

x = F

hence x in { F