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

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

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

then id (dom f) = (id (dom f)) +* x,y by A2, Def3;
hence f . a = (f * ((id (dom f)) +* x,y)) . a by RELAT_1:78; :: thesis: verum

end;

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

then A4: ((id (dom f)) +* x,y) . x = y by A2, Th33;
A5: dom ((id (dom f)) +* x,y) = dom f by A2, Th32;
thus f . a = (f * ((id (dom f)) +* x,y)) . a :: thesis: verum

proof

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

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

now

assume a <> x ; :: thesis: f . a = (f * ((id (dom f)) +* x,y)) . a
then ((id (dom f)) +* x,y) . a = (id (dom f)) . a by Th34
.= a by A6, FUNCT_1:35 ;
hence f . a = (f * ((id (dom f)) +* x,y)) . a by A5, A6, FUNCT_1:23; :: thesis: verum

end;

hence f . a = (f * ((id (dom f)) +* x,y)) . a by A1, A3, A4, A5, FUNCT_1:23; :: thesis: verum

end;

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

dom (f * ((id (dom f)) +* x,y)) c= dom ((id (dom f)) +* x,y) by RELAT_1:44;
then not a in dom (f * ((id (dom f)) +* x,y)) by A5, A7;
then ( (f * ((id (dom f)) +* x,y)) . a = {} & f . a = {} ) by A7, FUNCT_1:def 4;
hence f . a = (f * ((id (dom f)) +* x,y)) . a ; :: thesis: verum

end;

end;

end;

end;

end;