let x, y be object ; :: thesis: for f being Function st f . y = x & y in dom f holds
{y} \/ ((f | ((dom f) \ {y})) " {x}) = f " {x}
let f be Function; :: thesis: ( f . y = x & y in dom f implies {y} \/ ((f | ((dom f) \ {y})) " {x}) = f " {x} )
assume that
A1: f . y = x and
A2: y in dom f ; :: thesis: {y} \/ ((f | ((dom f) \ {y})) " {x}) = f " {x}
set d = (dom f) \ {y};
A3: (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 A4: x1 in (f | ((dom f) \ {y})) " {x} ; :: thesis: x1 in f " {x}
A5: (f | ((dom f) \ {y})) . x1 in {x} by A4, FUNCT_1:def 7;
A6: x1 in dom (f | ((dom f) \ {y})) by A4, 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 A6, A5, FUNCT_1:def 7; :: thesis: verum

end;

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

proof

let x1 be object ; :: according to TARSKI:def 3 :: thesis: ( not x1 in f " {x} or x1 in {y} \/ ((f | ((dom f) \ {y})) " {x}) )
assume A8: x1 in f " {x} ; :: thesis: x1 in {y} \/ ((f | ((dom f) \ {y})) " {x})
( ( x1 in dom f & not x1 in {y} ) or x1 = y ) by A8, FUNCT_1:def 7, TARSKI:def 1;
then ( ( x1 in dom f & x1 in (dom f) \ {y} & dom (f | ((dom f) \ {y})) = (dom f) /\ ((dom f) \ {y}) ) or x1 = y ) by RELAT_1:61, XBOOLE_0:def 5;
then ( x1 in dom (f | ((dom f) \ {y})) or x1 = 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} ) or x1 in {y} ) by A8, FUNCT_1:47, FUNCT_1:def 7, TARSKI:def 1;
then ( x1 in (f | ((dom f) \ {y})) " {x} or x1 in {y} ) by FUNCT_1:def 7;
hence x1 in {y} \/ ((f | ((dom f) \ {y})) " {x}) by XBOOLE_0:def 3; :: thesis: verum

end;

{y} c= f " {x}

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in {y} or z in f " {x} )
assume z in {y} ; :: thesis: z in f " {x}
then A9: z = y by TARSKI:def 1;
f . y in {x} by A1, TARSKI:def 1;
hence z in f " {x} by A2, A9, FUNCT_1:def 7; :: thesis: verum

end;

hence {y} \/ ((f | ((dom f) \ {y})) " {x}) = f " {x} by A7, A3, XBOOLE_1:8; :: thesis: verum