let A be non empty set ; :: thesis: for y being set
for f being Function holds (f +* (A --> y)) .: A = {y}
let y be set ; :: thesis: for f being Function holds (f +* (A --> y)) .: A = {y}
let f be Function; :: thesis: (f +* (A --> y)) .: A = {y}
now :: thesis: for u being object holds
( ( u in (f +* (A --> y)) .: A implies u = y ) & ( u = y implies u in (f +* (A --> y)) .: A ) )
let u be object ; :: thesis: ( ( u in (f +* (A --> y)) .: A implies u = y ) & ( u = y implies u in (f +* (A --> y)) .: A ) )
thus ( u in (f +* (A --> y)) .: A implies u = y ) :: thesis: ( u = y implies u in (f +* (A --> y)) .: A )
proof
assume u in (f +* (A --> y)) .: A ; :: thesis: u = y
then consider z being object such that
z in dom (f +* (A --> y)) and
A1: z in A and
A2: u = (f +* (A --> y)) . z by FUNCT_1:def 6;
z in dom (A --> y) by A1, FUNCOP_1:13;
then u = (A --> y) . z by A2, FUNCT_4:13;
hence u = y by A1, FUNCOP_1:7; :: thesis: verum
end;
consider x being object such that
A3: x in A by XBOOLE_0:def 1;
A4: x in dom (A --> y) by A3, FUNCOP_1:13;
then A5: x in dom (f +* (A --> y)) by FUNCT_4:12;
(A --> y) . x = y by A3, FUNCOP_1:7;
then y = (f +* (A --> y)) . x by A4, FUNCT_4:13;
hence ( u = y implies u in (f +* (A --> y)) .: A ) by A3, A5, FUNCT_1:def 6; :: thesis: verum
end;
hence (f +* (A --> y)) .: A = {y} by TARSKI:def 1; :: thesis: verum