let W, X 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 )
then A2: W is subset-closed ;
assume ( ( 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
then A3: ( X c= W & card X in card W ) by A2, Th1, ORDINAL1:def 2;
let x be set ; :: 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 & dom f = X & rng f c= W ) by FUNCT_2:def 2;
A6: f c= W

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in f or y in W )
assume A7: y in f ; :: thesis: y in W
then consider y1, y2 being set such that
A8: [y1,y2] = y by RELAT_1:def 1;
A9: ( y1 in dom f & y2 = f . y1 ) by A7, A8, FUNCT_1:8;
then y2 in rng f by FUNCT_1:def 5;
hence y in W by A1, A3, A5, A8, A9, Th4; :: thesis: verum

end;

card f = card X by A4, A5, CARD_2:7;
hence x in W by A1, A3, A5, A6, CLASSES1:2; :: thesis: verum