let A, B, C, x be set ; ( C c= A implies ((id A) +* (B --> x)) " (C \ {x}) = (C \ B) \ {x} )
assume A1:
C c= A
; ((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}
XBOOLE_0:def 10 (C \ B) \ {x} c= ((id A) +* (B --> x)) " (C \ {x})
let x1 be object ; TARSKI:def 3 ( not x1 in (C \ B) \ {x} or x1 in ((id A) +* (B --> x)) " (C \ {x}) )
assume A12:
x1 in (C \ B) \ {x}
; x1 in ((id A) +* (B --> x)) " (C \ {x})
then
not x1 in {x}
by XBOOLE_0:def 5;
then A13:
x1 in C \ {x}
by A12, XBOOLE_0:def 5;
A14:
x1 in C
by A12;
then
x1 in A
by A1;
then
x1 in dom (id A)
;
then A15:
x1 in (dom (id A)) \/ (dom (B --> x))
by XBOOLE_0:def 3;
x1 in C \ B
by A12, XBOOLE_0:def 5;
then
not x1 in dom (B --> x)
by XBOOLE_0:def 5;
then
((id A) +* (B --> x)) . x1 = (id A) . x1
by A15, FUNCT_4:def 1;
then A16:
((id A) +* (B --> x)) . x1 = x1
by A1, A14, FUNCT_1:17;
x1 in dom ((id A) +* (B --> x))
by A15, FUNCT_4:def 1;
hence
x1 in ((id A) +* (B --> x)) " (C \ {x})
by A13, A16, FUNCT_1:def 7; verum