let x, y be object ; :: thesis: for f being Function st f . y <> x holds
(f | ((dom f) \ {y})) " {x} = f " {x}
let f be Function; :: thesis: ( f . y <> x implies (f | ((dom f) \ {y})) " {x} = f " {x} )
set d = (dom f) \ {y};
assume A1: f . y <> x ; :: thesis: (f | ((dom f) \ {y})) " {x} = f " {x}
A2: f " {x} c= (f | ((dom f) \ {y})) " {x}
proof
A3: dom (f | ((dom f) \ {y})) = (dom f) /\ ((dom f) \ {y}) by RELAT_1:61;
let x1 be object ; :: according to TARSKI:def 3 :: thesis: ( not x1 in f " {x} or x1 in (f | ((dom f) \ {y})) " {x} )
assume A4: x1 in f " {x} ; :: thesis: x1 in (f | ((dom f) \ {y})) " {x}
A5: f . x1 in {x} by A4, FUNCT_1:def 7;
f . x1 in {x} by A4, FUNCT_1:def 7;
then f . x1 = x by TARSKI:def 1;
then A6: not x1 in {y} by A1, TARSKI:def 1;
x1 in dom f by A4, FUNCT_1:def 7;
then x1 in (dom f) \ {y} by A6, XBOOLE_0:def 5;
then A7: x1 in dom (f | ((dom f) \ {y})) by A3, XBOOLE_0:def 4;
then f . x1 = (f | ((dom f) \ {y})) . x1 by FUNCT_1:47;
hence x1 in (f | ((dom f) \ {y})) " {x} by A7, A5, FUNCT_1:def 7; :: thesis: verum
end;
(f | ((dom f) \ {y})) " {x} c= f " {x}
proof
let x1 be object ; :: according to TARSKI:def 3 :: thesis: ( not x1 in (f | ((dom f) \ {y})) " {x} or x1 in f " {x} )
assume A8: x1 in (f | ((dom f) \ {y})) " {x} ; :: thesis: x1 in f " {x}
A9: (f | ((dom f) \ {y})) . x1 in {x} by A8, FUNCT_1:def 7;
A10: x1 in dom (f | ((dom f) \ {y})) by A8, FUNCT_1:def 7;
then ( dom (f | ((dom f) \ {y})) = (dom f) /\ ((dom f) \ {y}) & f . x1 = (f | ((dom f) \ {y})) . x1 ) by FUNCT_1:47, RELAT_1:61;
hence x1 in f " {x} by A10, A9, FUNCT_1:def 7; :: thesis: verum
end;
hence (f | ((dom f) \ {y})) " {x} = f " {x} by A2; :: thesis: verum