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

A3: now :: thesis: for z being object st z in dom g holds
g . z = (f +* (x,y)) . z

let z be object ; :: thesis: ( z in dom g implies g . z = (f +* (x,y)) . z )
assume A4: z in dom g ; :: thesis: g . z = (f +* (x,y)) . z
hence g . z = f . z by A1, GRFUNC_1:2
.= (f +* (x,y)) . z by A2, A4, Th31 ;
:: thesis: verum

end;

dom g c= dom f by A1, GRFUNC_1:2;
then dom g c= dom (f +* (x,y)) by Th29;
hence g c= f +* (x,y) by A3, GRFUNC_1:2; :: thesis: verum