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;

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

hence
x in product (X --> Y)
by A1, CARD_3:def 5; :: thesis: verumg . 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;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