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

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in f or y in Tarski-Class W )
assume A9: y in f ; :: thesis: y in Tarski-Class W
then consider y1, y2 being set such that
A10: [y1,y2] = y by RELAT_1:def 1;
A11: y1 in dom f by A9, A10, FUNCT_1:8;
y2 = f . y1 by A9, A10, FUNCT_1:8;
then y2 in rng f by A11, FUNCT_1:def 5;
hence y in Tarski-Class W by A7, A5, A6, A10, A11, CLASSES1:31; :: thesis: verum

end;

card f = card X by A3, A4, CARD_2:7;
hence x in Tarski-Class W by A2, A4, A8, CLASSES1:9; :: thesis: verum