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

not x in C \ B by A1, A2;

then C \ B misses {x} by ZFMISC_1:50;

then (C \ B) \ {x} = C \ B by XBOOLE_1:83;

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

assume that

A1: C c= A and

A2: not x in A ; :: thesis: ((id A) +* (B --> x)) " (C \ {x}) = C \ B

not x in C \ B by A1, A2;

then C \ B misses {x} by ZFMISC_1:50;

then (C \ B) \ {x} = C \ B by XBOOLE_1:83;

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