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 that
A1: C c= A and
A2: not x in A ; :: thesis: ((id A) +* (B --> x)) " (C \/ {x}) = C \/ B
A3: C \ {x} = C

proof

thus C \ {x} c= C ; :: according to XBOOLE_0:def 10 :: thesis: C c= C \ {x}
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in C or y in C \ {x} )
assume A4: 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, A2, A4; :: thesis: verum

end;

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

end;

A5: ((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 object ; :: 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 object ; :: 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 A6: y in (C \ B) \/ B by XBOOLE_1:39;

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

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

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

proof

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

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: 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;

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: verum