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
dom g c= dom f by A1, GRFUNC_1:8;
then A3: dom g c= dom (f +* x,y) by Th32;

now

let z be set ; :: 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:8
.= (f +* x,y) . z by A2, A4, Th34 ;
:: thesis: verum

end;

hence g c= f +* x,y by A3, GRFUNC_1:8; :: thesis: verum