let A, B, C, x be set ; :: thesis: ( C c= A implies ((id A) +* (B --> x)) " (C \ {x}) = (C \ B) \ {x} )

assume A1: C c= A ; :: thesis: ((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} :: according to XBOOLE_0:def 10 :: thesis: (C \ B) \ {x} c= ((id A) +* (B --> x)) " (C \ {x})

assume A12: x1 in (C \ B) \ {x} ; :: thesis: 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; :: thesis: verum

assume A1: C c= A ; :: thesis: ((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} :: according to XBOOLE_0:def 10 :: thesis: (C \ B) \ {x} c= ((id A) +* (B --> x)) " (C \ {x})

proof

let x1 be object ; :: according to TARSKI:def 3 :: thesis: ( not x1 in (C \ B) \ {x} or x1 in ((id A) +* (B --> x)) " (C \ {x}) )
let x1 be object ; :: according to TARSKI:def 3 :: thesis: ( not x1 in ((id A) +* (B --> x)) " (C \ {x}) or x1 in (C \ B) \ {x} )

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

then A3: ((id A) +* (B --> x)) . x1 in C \ {x} by FUNCT_1:def 7;

A4: not x1 in B

x1 in dom ((id A) +* (B --> x)) by A2, FUNCT_1:def 7;

then x1 in A \/ B by Th14;

then A9: ( x1 in A or x1 in B ) by XBOOLE_0:def 3;

then x1 in dom (id A) by A4;

then x1 in (dom (id A)) \/ (dom (B --> x)) by XBOOLE_0:def 3;

then ((id A) +* (B --> x)) . x1 = (id A) . x1 by A8, FUNCT_4:def 1;

then A10: ((id A) +* (B --> x)) . x1 = x1 by A4, A9, FUNCT_1:17;

then A11: not x1 in {x} by A3, XBOOLE_0:def 5;

x1 in C \ B by A3, A4, A10, XBOOLE_0:def 5;

hence x1 in (C \ B) \ {x} by A11, XBOOLE_0:def 5; :: thesis: verum

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

then A3: ((id A) +* (B --> x)) . x1 in C \ {x} by FUNCT_1:def 7;

A4: not x1 in B

proof

then A8:
not x1 in dom (B --> x)
;
assume A5:
x1 in B
; :: thesis: contradiction

then A6: x1 in dom (B --> x) by FUNCOP_1:13;

then x1 in (dom (id A)) \/ (dom (B --> x)) by XBOOLE_0:def 3;

then ((id A) +* (B --> x)) . x1 = (B --> x) . x1 by A6, FUNCT_4:def 1;

then A7: ((id A) +* (B --> x)) . x1 = x by A5, FUNCOP_1:7;

not ((id A) +* (B --> x)) . x1 in {x} by A3, XBOOLE_0:def 5;

hence contradiction by A7, TARSKI:def 1; :: thesis: verum

end;then A6: x1 in dom (B --> x) by FUNCOP_1:13;

then x1 in (dom (id A)) \/ (dom (B --> x)) by XBOOLE_0:def 3;

then ((id A) +* (B --> x)) . x1 = (B --> x) . x1 by A6, FUNCT_4:def 1;

then A7: ((id A) +* (B --> x)) . x1 = x by A5, FUNCOP_1:7;

not ((id A) +* (B --> x)) . x1 in {x} by A3, XBOOLE_0:def 5;

hence contradiction by A7, TARSKI:def 1; :: thesis: verum

x1 in dom ((id A) +* (B --> x)) by A2, FUNCT_1:def 7;

then x1 in A \/ B by Th14;

then A9: ( x1 in A or x1 in B ) by XBOOLE_0:def 3;

then x1 in dom (id A) by A4;

then x1 in (dom (id A)) \/ (dom (B --> x)) by XBOOLE_0:def 3;

then ((id A) +* (B --> x)) . x1 = (id A) . x1 by A8, FUNCT_4:def 1;

then A10: ((id A) +* (B --> x)) . x1 = x1 by A4, A9, FUNCT_1:17;

then A11: not x1 in {x} by A3, XBOOLE_0:def 5;

x1 in C \ B by A3, A4, A10, XBOOLE_0:def 5;

hence x1 in (C \ B) \ {x} by A11, XBOOLE_0:def 5; :: thesis: verum

assume A12: x1 in (C \ B) \ {x} ; :: thesis: 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; :: thesis: verum