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} )
assume A2: u in (g +* (x .--> y)) .: (A \ {x}) ; :: thesis: u in ((g +* (x .--> y)) .: A) \ {y}
then consider z being set such that
A3: ( z in dom (g +* (x .--> y)) & z in A \ {x} & u = (g +* (x .--> y)) . z ) by FUNCT_1:def 12;
( not z in {x} & dom (x .--> y) = {x} ) by A3, FUNCOP_1:19, XBOOLE_0:def 5;
then ( u = g . z & z in dom g ) by A3, FUNCT_4:12, FUNCT_4:13;
then u <> y by A1, A3, FUNCT_1:def 12;
then A4: 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 A2, A4, 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 A5: u in ((g +* (x .--> y)) .: A) \ {y} ; :: thesis: u in (g +* (x .--> y)) .: (A \ {x})
then consider z being set such that
A6: ( z in dom (g +* (x .--> y)) & z in A & u = (g +* (x .--> y)) . z ) by FUNCT_1:def 12;

now

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

end;

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