let A, B, C, x be set ; :: thesis: ( C c= A & not x in A implies ((id A) +* (B --> x)) " (C \/ {x}) = C \/ B )
assume A1: ( C c= A & not x in A ) ; :: thesis: ((id A) +* (B --> x)) " (C \/ {x}) = C \/ B
set f = (id A) +* (B --> x);
A2: C \ {x} = C

proof

thus C \ {x} c= C ; :: according to XBOOLE_0:def 10 :: thesis: C c= C \ {x}
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in C or y in C \ {x} )
assume A3: y in C ; :: thesis: y in C \ {x}
not y in {x}

proof

assume y in {x} ; :: thesis: contradiction
then y = x by TARSKI:def 1;
hence contradiction by A1, A3; :: thesis: verum

end;

hence y in C \ {x} by A3, XBOOLE_0:def 5; :: thesis: verum

end;

((id A) +* (B --> x)) " {x} = B by A1, Th18;
then A4: ((id A) +* (B --> x)) " (C \/ {x}) = (((id A) +* (B --> x)) " C) \/ B by RELAT_1:175;
((C \ B) \ {x}) \/ B = C \/ B

proof

thus ((C \ B) \ {x}) \/ B c= C \/ B :: according to XBOOLE_0:def 10 :: thesis: C \/ B c= ((C \ B) \ {x}) \/ B

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in ((C \ B) \ {x}) \/ B or y in C \/ B )
assume y in ((C \ B) \ {x}) \/ B ; :: thesis: y in C \/ B
then ( y in (C \ B) \ {x} or y in B ) by XBOOLE_0:def 3;
hence y in C \/ B by XBOOLE_0:def 3; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in C \/ B or y in ((C \ B) \ {x}) \/ B )
assume y in C \/ B ; :: thesis: y in ((C \ B) \ {x}) \/ B
then A5: y in (C \ B) \/ B by XBOOLE_1:39;

per cases ( y in C \ B or y in B ) by A5, XBOOLE_0:def 3;

suppose A6: y in C \ B ; :: thesis: y in ((C \ B) \ {x}) \/ B

then A7: y in C ;
not y in {x}

proof

assume y in {x} ; :: thesis: contradiction
then x in C by A7, TARSKI:def 1;
hence contradiction by A1; :: thesis: verum

end;

then y in (C \ B) \ {x} by A6, XBOOLE_0:def 5;
hence y in ((C \ B) \ {x}) \/ B by XBOOLE_0:def 3; :: thesis: verum

end;

suppose y in B ; :: thesis: y in ((C \ B) \ {x}) \/ B

hence y in ((C \ B) \ {x}) \/ B by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence ((id A) +* (B --> x)) " (C \/ {x}) = C \/ B by A1, A2, A4, Th17; :: thesis: verum