let x, y be set ; :: thesis: for g being Function
for A being set st not y in g .: (A \ {x}) holds
(g +* (x .--> y)) .: (A \ {x}) = ((g +* (x .--> y)) .: A) \ {y}
let g be Function; :: thesis: for A being set st not y in g .: (A \ {x}) holds
(g +* (x .--> y)) .: (A \ {x}) = ((g +* (x .--> y)) .: A) \ {y}
let A be set ; :: thesis: ( not y in g .: (A \ {x}) implies (g +* (x .--> y)) .: (A \ {x}) = ((g +* (x .--> y)) .: A) \ {y} )
assume A1: not y in g .: (A \ {x}) ; :: thesis: (g +* (x .--> y)) .: (A \ {x}) = ((g +* (x .--> y)) .: A) \ {y}
thus (g +* (x .--> y)) .: (A \ {x}) c= ((g +* (x .--> y)) .: A) \ {y} :: according to XBOOLE_0:def 10 :: thesis: ((g +* (x .--> y)) .: A) \ {y} c= (g +* (x .--> y)) .: (A \ {x})

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in (g +* (x .--> y)) .: (A \ {x}) or u in ((g +* (x .--> y)) .: A) \ {y} )
A2: dom (x .--> y) = {x} by FUNCOP_1:19;
assume A3: u in (g +* (x .--> y)) .: (A \ {x}) ; :: thesis: u in ((g +* (x .--> y)) .: A) \ {y}
then consider z being set such that
A4: z in dom (g +* (x .--> y)) and
A5: z in A \ {x} and
A6: u = (g +* (x .--> y)) . z by FUNCT_1:def 12;
A7: not z in {x} by A5, XBOOLE_0:def 5;
then A8: z in dom g by A4, A2, FUNCT_4:13;
u = g . z by A6, A7, A2, FUNCT_4:12;
then u <> y by A1, A5, A8, FUNCT_1:def 12;
then A9: not u in {y} by TARSKI:def 1;
(g +* (x .--> y)) .: (A \ {x}) c= (g +* (x .--> y)) .: A by RELAT_1:156;
hence u in ((g +* (x .--> y)) .: A) \ {y} by A3, A9, XBOOLE_0:def 5; :: thesis: verum

end;

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in ((g +* (x .--> y)) .: A) \ {y} or u in (g +* (x .--> y)) .: (A \ {x}) )
assume A10: u in ((g +* (x .--> y)) .: A) \ {y} ; :: thesis: u in (g +* (x .--> y)) .: (A \ {x})
then consider z being set such that
A11: z in dom (g +* (x .--> y)) and
A12: z in A and
A13: u = (g +* (x .--> y)) . z by FUNCT_1:def 12;

now

assume A14: z in {x} ; :: thesis: contradiction
then z in dom (x .--> y) by FUNCOP_1:19;
then u = (x .--> y) . z by A13, FUNCT_4:14;
then u = y by A14, FUNCOP_1:13;
then u in {y} by TARSKI:def 1;
hence contradiction by A10, XBOOLE_0:def 5; :: thesis: verum

end;

then z in A \ {x} by A12, XBOOLE_0:def 5;
hence u in (g +* (x .--> y)) .: (A \ {x}) by A11, A13, FUNCT_1:def 12; :: thesis: verum