let x, y be set ; :: thesis: for f being Function st ( x in dom f implies ( y in dom f & f . x = f . y ) ) holds
f = f * ((id (dom f)) +* (x,y))
let f be Function; :: thesis: ( ( x in dom f implies ( y in dom f & f . x = f . y ) ) implies f = f * ((id (dom f)) +* (x,y)) )
assume A1: ( x in dom f implies ( y in dom f & f . x = f . y ) ) ; :: thesis: f = f * ((id (dom f)) +* (x,y))
set g1 = (id (dom f)) +* (x,y);
set g = f * ((id (dom f)) +* (x,y));
A2: dom (id (dom f)) = dom f ;

per cases ( not x in dom f or x in dom f ) ;

suppose not x in dom f ; :: thesis: f = f * ((id (dom f)) +* (x,y))

then id (dom f) = (id (dom f)) +* (x,y) by Def2;
hence f = f * ((id (dom f)) +* (x,y)) by RELAT_1:52; :: thesis: verum

end;

suppose A3: x in dom f ; :: thesis: f = f * ((id (dom f)) +* (x,y))

A4: dom ((id (dom f)) +* (x,y)) = dom f by A2, Th29;

now :: thesis: ( dom f = dom (f * ((id (dom f)) +* (x,y))) & ( for a being object st a in dom f holds
f . a = (f * ((id (dom f)) +* (x,y))) . a ) )

rng ((id (dom f)) +* (x,y)) c= dom f

proof

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in rng ((id (dom f)) +* (x,y)) or b in dom f )
assume b in rng ((id (dom f)) +* (x,y)) ; :: thesis: b in dom f
then consider a being object such that
A5: a in dom ((id (dom f)) +* (x,y)) and
A6: b = ((id (dom f)) +* (x,y)) . a by FUNCT_1:def 3;

per cases ( a = x or a <> x ) ;

suppose a = x ; :: thesis: b in dom f

hence b in dom f by A1, A2, A3, A6, Th30; :: thesis: verum

end;

suppose a <> x ; :: thesis: b in dom f

then (id (dom f)) . a = ((id (dom f)) +* (x,y)) . a by Th31;
hence b in dom f by A4, A5, A6, FUNCT_1:18; :: thesis: verum

end;

end;

end;

hence dom f = dom (f * ((id (dom f)) +* (x,y))) by A4, RELAT_1:27; :: thesis: for a being object st a in dom f holds
f . a = (f * ((id (dom f)) +* (x,y))) . a
let a be object ; :: thesis: ( a in dom f implies f . a = (f * ((id (dom f)) +* (x,y))) . a )
assume a in dom f ; :: thesis: f . a = (f * ((id (dom f)) +* (x,y))) . a
thus f . a = (f * ((id (dom f)) +* (x,y))) . a by A1, A3, Th106; :: thesis: verum

end;

hence f = f * ((id (dom f)) +* (x,y)) ; :: thesis: verum

end;

end;