let A, B, x be set ; :: thesis: ( not x in A implies ((id A) +* (B --> x)) " {x} = B )
set f = (id A) +* (B --> x);
assume A1: not x in A ; :: thesis: ((id A) +* (B --> x)) " {x} = B
thus ((id A) +* (B --> x)) " {x} c= B :: according to XBOOLE_0:def 10 :: thesis: B c= ((id A) +* (B --> x)) " {x}
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in ((id A) +* (B --> x)) " {x} or y in B )
assume A2: y in ((id A) +* (B --> x)) " {x} ; :: thesis: y in B
then A3: y in dom ((id A) +* (B --> x)) by FUNCT_1:def 7;
A4: ((id A) +* (B --> x)) . y in {x} by A2, FUNCT_1:def 7;
per cases ( y in dom (B --> x) or not y in dom (B --> x) ) ;
suppose y in dom (B --> x) ; :: thesis: y in B
hence y in B ; :: thesis: verum
end;
suppose A5: not y in dom (B --> x) ; :: thesis: y in B
then A6: ((id A) +* (B --> x)) . y = (id A) . y by FUNCT_4:11;
A7: ( y in dom (B --> x) or y in dom (id A) ) by A3, FUNCT_4:12;
then (id A) . y = y by A5, FUNCT_1:18;
then y = x by A4, A6, TARSKI:def 1;
hence y in B by A1, A7; :: thesis: verum
end;
end;
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in B or y in ((id A) +* (B --> x)) " {x} )
assume A8: y in B ; :: thesis: y in ((id A) +* (B --> x)) " {x}
then A9: y in dom (B --> x) by FUNCOP_1:13;
then ((id A) +* (B --> x)) . y = (B --> x) . y by FUNCT_4:13;
then ((id A) +* (B --> x)) . y = x by A8, FUNCOP_1:7;
then A10: ((id A) +* (B --> x)) . y in {x} by TARSKI:def 1;
y in dom ((id A) +* (B --> x)) by A9, FUNCT_4:12;
hence y in ((id A) +* (B --> x)) " {x} by A10, FUNCT_1:def 7; :: thesis: verum