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

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;

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