let x, y, a be object ; :: 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
set g1 = (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 . a = (f * ((id (dom f)) +* (x,y))) . a

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

end;

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

A4: dom ((id (dom f)) +* (x,y)) = dom f by A2, Th29;
A5: ((id (dom f)) +* (x,y)) . x = y by A2, A3, Th30;
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 :: thesis: ( a <> x implies f . a = (f * ((id (dom f)) +* (x,y))) . a )

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 Th31
.= a by A6, FUNCT_1:18 ;
hence f . a = (f * ((id (dom f)) +* (x,y))) . a by A4, A6, FUNCT_1:13; :: thesis: verum

end;

hence f . a = (f * ((id (dom f)) +* (x,y))) . a by A1, A3, A5, A4, FUNCT_1:13; :: 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:25;
then not a in dom (f * ((id (dom f)) +* (x,y))) by A4, A7;
then (f * ((id (dom f)) +* (x,y))) . a = {} by FUNCT_1:def 2;
hence f . a = (f * ((id (dom f)) +* (x,y))) . a by A7, FUNCT_1:def 2; :: thesis: verum

end;

end;

end;

end;

end;