let y, x be set ; :: 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 A1: ( f . y = x & y in dom f ) ; :: thesis: {y} \/ ((f | ((dom f) \ {y})) " {x}) = f " {x}
set d = (dom f) \ {y};
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;

{y} c= f " {x}

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in {y} or z in f " {x} )
assume A4: z in {y} ; :: thesis: z in f " {x}
( z = y & f . y in {x} ) by A1, A4, TARSKI:def 1;
hence z in f " {x} by A1, FUNCT_1:def 13; :: thesis: verum

end;

then A5: {y} \/ ((f | ((dom f) \ {y})) " {x}) c= f " {x} by A2, XBOOLE_1:8;
f " {x} c= {y} \/ ((f | ((dom f) \ {y})) " {x})

proof

let x1 be set ; :: according to TARSKI:def 3 :: thesis: ( not x1 in f " {x} or x1 in {y} \/ ((f | ((dom f) \ {y})) " {x}) )
assume A6: 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 A6, FUNCT_1:def 13, 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:90, 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 A6, FUNCT_1:70, FUNCT_1:def 13, TARSKI:def 1;
then ( x1 in (f | ((dom f) \ {y})) " {x} or x1 in {y} ) by FUNCT_1:def 13;
hence x1 in {y} \/ ((f | ((dom f) \ {y})) " {x}) by XBOOLE_0:def 3; :: thesis: verum

end;

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