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

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

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