let X be non empty set ; :: thesis: for Y being set
for Z being Subset of Y holds product (X --> Z) c= product (X --> Y)
let Y be set ; :: thesis: for Z being Subset of Y holds product (X --> Z) c= product (X --> Y)
let Z be Subset of Y; :: thesis: product (X --> Z) c= product (X --> Y)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in product (X --> Z) or x in product (X --> Y) )
assume x in product (X --> Z) ; :: thesis: x in product (X --> Y)
then consider g being Function such that
A1: ( x = g & dom g = dom (X --> Z) ) and
A2: for y being object st y in dom (X --> Z) holds
g . y in (X --> Z) . y by CARD_3:def 5;

now :: thesis: for y being object st y in dom (X --> Y) holds
g . y in (X --> Y) . y

let y be object ; :: thesis: ( y in dom (X --> Y) implies g . y in (X --> Y) . y )
assume a4: y in dom (X --> Y) ; :: thesis: g . y in (X --> Y) . y
then A4: y in X ;
A5: ( (X --> Z) . y = Z & (X --> Y) . y = Y ) by a4, FUNCOP_1:7;
y in dom (X --> Z) by A4;
then g . y in (X --> Z) . y by A2;
hence g . y in (X --> Y) . y by A5; :: thesis: verum

end;

hence x in product (X --> Y) by A1, CARD_3:def 5; :: thesis: verum