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

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in (g +* (x .--> y)) .: (A \ {x}) or u in g .: (A \ {x}) )
A1: dom (x .--> y) = {x} ;
assume u in (g +* (x .--> y)) .: (A \ {x}) ; :: thesis: u in g .: (A \ {x})
then consider z being object such that
A2: z in dom (g +* (x .--> y)) and
A3: z in A \ {x} and
A4: u = (g +* (x .--> y)) . z by FUNCT_1:def 6;
A5: not z in {x} by A3, XBOOLE_0:def 5;
then A6: z in dom g by A2, A1, FUNCT_4:12;
u = g . z by A4, A5, A1, FUNCT_4:11;
hence u in g .: (A \ {x}) by A3, A6, FUNCT_1:def 6; :: thesis: verum

end;

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in g .: (A \ {x}) or u in (g +* (x .--> y)) .: (A \ {x}) )
assume u in g .: (A \ {x}) ; :: thesis: u in (g +* (x .--> y)) .: (A \ {x})
then consider z being object such that
A7: z in dom g and
A8: z in A \ {x} and
A9: u = g . z by FUNCT_1:def 6;
not z in {x} by A8, XBOOLE_0:def 5;
then not z in dom (x .--> y) ;
then A10: u = (g +* (x .--> y)) . z by A9, FUNCT_4:11;
z in dom (g +* (x .--> y)) by A7, FUNCT_4:12;
hence u in (g +* (x .--> y)) .: (A \ {x}) by A8, A10, FUNCT_1:def 6; :: thesis: verum