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

end;

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