let X, Y be non empty set ; :: thesis: for y being Element of Y holds X --> y in product (X --> Y)
let y be Element of Y; :: thesis: X --> y in product (X --> Y)
set f = X --> y;
A1: dom (X --> y) = X
.= dom (X --> Y) ;
for x being object st x in dom (X --> Y) holds
(X --> y) . x in (X --> Y) . x
proof
let x be object ; :: thesis: ( x in dom (X --> Y) implies (X --> y) . x in (X --> Y) . x )
assume A2: x in dom (X --> Y) ; :: thesis: (X --> y) . x in (X --> Y) . x
then A3: (X --> Y) . x = Y by FUNCOP_1:7;
(X --> y) . x = y by A2, FUNCOP_1:7;
hence (X --> y) . x in (X --> Y) . x by A3; :: thesis: verum
end;
hence X --> y in product (X --> Y) by A1, CARD_3:def 5; :: thesis: verum