let A, B, C, x be set ; :: thesis:
assume that
A1: C c= A and
A2: not x in A ; :: thesis:
A3: C \ {x} = C

proof

thus C \ {x} c= C ; :: according to XBOOLE_0:def 10 :: thesis:
let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A4: y in C ; :: thesis:
not y in {x}

proof

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

end;

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

end;

A5: ((C \ B) \ {x}) \/ B = C \/ B

proof

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

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in ((C \ B) \ {x}) \/ B ; :: thesis:
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:

end;

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in C \/ B ; :: thesis:
then A6: y in (C \ B) \/ B by XBOOLE_1:39;

per cases by A6, XBOOLE_0:def 3;

suppose A7: y in C \ B ; :: thesis:

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

proof

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

end;

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

end;

suppose y in B ; :: thesis:

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

end;

end;

end;

set f = (id A) +* (B --> x);
((id A) +* (B --> x)) " {x} = B by A2, Th17;
then ((id A) +* (B --> x)) " (C \/ {x}) = (((id A) +* (B --> x)) " C) \/ B by RELAT_1:140;
hence ((id A) +* (B --> x)) " (C \/ {x}) = C \/ B by A1, A3, A5, Th16; :: thesis: