let y, x be set ; :: 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 | ((dom f) \ {y})) " {x} c= f " {x}

proof

let x1 be set ; :: according to TARSKI:def 3 :: thesis: ( not x1 in (f | ((dom f) \ {y})) " {x} or x1 in f " {x} )
assume A3: x1 in (f | ((dom f) \ {y})) " {x} ; :: thesis: x1 in f " {x}
( x1 in dom (f | ((dom f) \ {y})) & dom (f | ((dom f) \ {y})) = (dom f) /\ ((dom f) \ {y}) ) by A3, FUNCT_1:def 13, RELAT_1:90;
then ( x1 in dom f & f . x1 = (f | ((dom f) \ {y})) . x1 & (f | ((dom f) \ {y})) . x1 in {x} ) by A3, FUNCT_1:70, FUNCT_1:def 13;
hence x1 in f " {x} by FUNCT_1:def 13; :: thesis: verum

end;

f " {x} c= (f | ((dom f) \ {y})) " {x}

proof

let x1 be set ; :: 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}
( x1 in dom f & f . x1 in {x} ) by A4, FUNCT_1:def 13;
then ( x1 in dom f & f . x1 = x ) by TARSKI:def 1;
then ( x1 in dom f & not x1 in {y} ) by A1, TARSKI:def 1;
then ( x1 in dom f & x1 in (dom f) \ {y} & dom (f | ((dom f) \ {y})) = (dom f) /\ ((dom f) \ {y}) ) by RELAT_1:90, XBOOLE_0:def 5;
then x1 in dom (f | ((dom f) \ {y})) by XBOOLE_0:def 4;
then ( x1 in dom (f | ((dom f) \ {y})) & f . x1 = (f | ((dom f) \ {y})) . x1 & f . x1 in {x} ) by A4, FUNCT_1:70, FUNCT_1:def 13;
hence x1 in (f | ((dom f) \ {y})) " {x} by FUNCT_1:def 13; :: thesis: verum

end;

hence (f | ((dom f) \ {y})) " {x} = f " {x} by A2, XBOOLE_0:def 10; :: thesis: verum