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 by RELAT_1:71;

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 A2, Def3;
hence f = f * ((id (dom f)) +* x,y) by RELAT_1:78; :: 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, Th32;

now

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

proof

let b be set ; :: 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 set such that
A5: a in dom ((id (dom f)) +* x,y) and
A6: b = ((id (dom f)) +* x,y) . a by FUNCT_1:def 5;

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, Th33; :: thesis: verum

end;

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

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

end;

end;

end;

hence dom f = dom (f * ((id (dom f)) +* x,y)) by A4, RELAT_1:46; :: thesis: for a being set st a in dom f holds
f . a = (f * ((id (dom f)) +* x,y)) . a
let a be set ; :: 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, Th109; :: thesis: verum

end;

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

end;

end;