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 set ; :: 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, XBOOLE_1:1;
hence x in Funcs Z,Y by A2, FUNCT_2:def 2; :: thesis: verum