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 set ; :: according to TARSKI:def 3 :: thesis: ( not x1 in ((id A) +* (B --> x)) " (C \ {x}) or x1 in (C \ B) \ {x} )
assume x1 in ((id A) +* (B --> x)) " (C \ {x}) ; :: thesis: x1 in (C \ B) \ {x}
then A2: ( x1 in dom ((id A) +* (B --> x)) & ((id A) +* (B --> x)) . x1 in C \ {x} ) by FUNCT_1:def 13;
A3: not x1 in B

proof

assume A4: x1 in B ; :: thesis: contradiction
A5: not ((id A) +* (B --> x)) . x1 in {x} by A2, XBOOLE_0:def 5;
A6: x1 in dom (B --> x) by A4, FUNCOP_1:19;
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 ((id A) +* (B --> x)) . x1 = x by A4, FUNCOP_1:13;
hence contradiction by A5, TARSKI:def 1; :: thesis: verum

end;

then A7: not x1 in dom (B --> x) ;
x1 in A \/ B by A2, Th15;
then A8: ( x1 in A or x1 in B ) by XBOOLE_0:def 3;
then x1 in dom (id A) by A3, FUNCT_1:34;
then x1 in (dom (id A)) \/ (dom (B --> x)) by XBOOLE_0:def 3;
then ((id A) +* (B --> x)) . x1 = (id A) . x1 by A7, FUNCT_4:def 1;
then A9: ((id A) +* (B --> x)) . x1 = x1 by A3, A8, FUNCT_1:34;
then A10: ( x1 in C & not x1 in {x} ) by A2, XBOOLE_0:def 5;
x1 in C \ B by A2, A3, A9, XBOOLE_0:def 5;
hence x1 in (C \ B) \ {x} by A10, XBOOLE_0:def 5; :: thesis: verum

end;

let x1 be set ; :: according to TARSKI:def 3 :: thesis: ( not x1 in (C \ B) \ {x} or x1 in ((id A) +* (B --> x)) " (C \ {x}) )
assume x1 in (C \ B) \ {x} ; :: thesis: x1 in ((id A) +* (B --> x)) " (C \ {x})
then A11: ( x1 in C \ B & not x1 in {x} ) by XBOOLE_0:def 5;
then A12: ( x1 in C & not x1 in B & not x1 in {x} ) by XBOOLE_0:def 5;
then A13: x1 in A by A1;
A14: not x1 in dom (B --> x) by A12;
A15: x1 in C \ {x} by A11, XBOOLE_0:def 5;
x1 in dom (id A) by A13, FUNCT_1:34;
then A16: x1 in (dom (id A)) \/ (dom (B --> x)) by XBOOLE_0:def 3;
then A17: x1 in dom ((id A) +* (B --> x)) by FUNCT_4:def 1;
((id A) +* (B --> x)) . x1 = (id A) . x1 by A14, A16, FUNCT_4:def 1;
then ((id A) +* (B --> x)) . x1 = x1 by A1, A12, FUNCT_1:34;
hence x1 in ((id A) +* (B --> x)) " (C \ {x}) by A15, A17, FUNCT_1:def 13; :: thesis: verum