let A, B, C, x be set ; :: thesis: ( C c= A implies ((id A) +* (B --> x)) " (C \ {x}) = (C \ B) \ {x} )
assume A1: C c= A ; :: thesis: ((id A) +* (B --> x)) " (C \ {x}) = (C \ B) \ {x}
set f = (id A) +* (B --> x);
thus ((id A) +* (B --> x)) " (C \ {x}) c= (C \ B) \ {x} :: according to XBOOLE_0:def 10 :: thesis: (C \ B) \ {x} c= ((id A) +* (B --> x)) " (C \ {x})
proof
let x1 be object ; :: according to TARSKI:def 3 :: thesis: ( not x1 in ((id A) +* (B --> x)) " (C \ {x}) or x1 in (C \ B) \ {x} )
assume A2: x1 in ((id A) +* (B --> x)) " (C \ {x}) ; :: thesis: x1 in (C \ B) \ {x}
then A3: ((id A) +* (B --> x)) . x1 in C \ {x} by FUNCT_1:def 7;
A4: not x1 in B
proof
assume A5: x1 in B ; :: thesis: contradiction
then A6: x1 in dom (B --> x) by FUNCOP_1:13;
then x1 in (dom (id A)) \/ (dom (B --> x)) by XBOOLE_0:def 3;
then ((id A) +* (B --> x)) . x1 = (B --> x) . x1 by A6, FUNCT_4:def 1;
then A7: ((id A) +* (B --> x)) . x1 = x by A5, FUNCOP_1:7;
not ((id A) +* (B --> x)) . x1 in {x} by A3, XBOOLE_0:def 5;
hence contradiction by A7, TARSKI:def 1; :: thesis: verum
end;
then A8: not x1 in dom (B --> x) ;
x1 in dom ((id A) +* (B --> x)) by A2, FUNCT_1:def 7;
then x1 in A \/ B by Th14;
then A9: ( x1 in A or x1 in B ) by XBOOLE_0:def 3;
then x1 in dom (id A) by A4;
then x1 in (dom (id A)) \/ (dom (B --> x)) by XBOOLE_0:def 3;
then ((id A) +* (B --> x)) . x1 = (id A) . x1 by A8, FUNCT_4:def 1;
then A10: ((id A) +* (B --> x)) . x1 = x1 by A4, A9, FUNCT_1:17;
then A11: not x1 in {x} by A3, XBOOLE_0:def 5;
x1 in C \ B by A3, A4, A10, XBOOLE_0:def 5;
hence x1 in (C \ B) \ {x} by A11, XBOOLE_0:def 5; :: thesis: verum
end;
let x1 be object ; :: according to TARSKI:def 3 :: thesis: ( not x1 in (C \ B) \ {x} or x1 in ((id A) +* (B --> x)) " (C \ {x}) )
assume A12: x1 in (C \ B) \ {x} ; :: thesis: x1 in ((id A) +* (B --> x)) " (C \ {x})
then not x1 in {x} by XBOOLE_0:def 5;
then A13: x1 in C \ {x} by A12, XBOOLE_0:def 5;
A14: x1 in C by A12;
then x1 in A by A1;
then x1 in dom (id A) ;
then A15: x1 in (dom (id A)) \/ (dom (B --> x)) by XBOOLE_0:def 3;
x1 in C \ B by A12, XBOOLE_0:def 5;
then not x1 in dom (B --> x) by XBOOLE_0:def 5;
then ((id A) +* (B --> x)) . x1 = (id A) . x1 by A15, FUNCT_4:def 1;
then A16: ((id A) +* (B --> x)) . x1 = x1 by A1, A14, FUNCT_1:17;
x1 in dom ((id A) +* (B --> x)) by A15, FUNCT_4:def 1;
hence x1 in ((id A) +* (B --> x)) " (C \ {x}) by A13, A16, FUNCT_1:def 7; :: thesis: verum