let X, Y, Z be set ; :: thesis: ( X c= Y implies Funcs (Z,X) c= Funcs (Z,Y) )
assume A1: X c= Y ; :: thesis: Funcs (Z,X) c= Funcs (Z,Y)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Funcs (Z,X) or x in Funcs (Z,Y) )
assume x in Funcs (Z,X) ; :: thesis: x in Funcs (Z,Y)
then consider f being Function such that
A2: ( x = f & dom f = Z ) and
A3: rng f c= X by FUNCT_2:def 2;
rng f c= Y by A1, A3;
hence x in Funcs (Z,Y) by A2, FUNCT_2:def 2; :: thesis: verum