let X, Y, Z be set ; ( X c= Y implies Funcs (Z,X) c= Funcs (Z,Y) )
assume A1:
X c= Y
; Funcs (Z,X) c= Funcs (Z,Y)
let x be object ; TARSKI:def 3 ( not x in Funcs (Z,X) or x in Funcs (Z,Y) )
assume
x in Funcs (Z,X)
; 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; verum