let X, W be set ; :: thesis: ( W is Tarski & ( ( X in W & W is epsilon-transitive ) or ( X in W & X c= W ) or ( card X in card W & X c= W ) ) implies Funcs (X,W) c= W )
assume A1: W is Tarski ; :: thesis: ( ( not ( X in W & W is epsilon-transitive ) & not ( X in W & X c= W ) & not ( card X in card W & X c= W ) ) or Funcs (X,W) c= W )
assume A2: ( ( X in W & W is epsilon-transitive ) or ( X in W & X c= W ) or ( card X in card W & X c= W ) ) ; :: thesis: Funcs (X,W) c= W
A3: card X in card W by A1, A2, Th1;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Funcs (X,W) or x in W )
assume A4: x in Funcs (X,W) ; :: thesis: x in W
then consider f being Function such that
A5: x = f and
A6: dom f = X and
A7: rng f c= W by FUNCT_2:def 2;
A8: X c= W by A2;
A9: f c= W

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f or y in W )
assume A10: y in f ; :: thesis: y in W
then consider y1, y2 being object such that
A11: [y1,y2] = y by RELAT_1:def 1;
A12: y1 in dom f by A10, A11, FUNCT_1:1;
y2 = f . y1 by A10, A11, FUNCT_1:1;
then y2 in rng f by A12, FUNCT_1:def 3;
hence y in W by A1, A8, A6, A7, A11, A12, Th3; :: thesis: verum

end;

card f = card X by A4, A5, CARD_2:3;
hence x in W by A1, A3, A5, A9, CLASSES1:1; :: thesis: verum