let f, g be Function; 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 ; ( 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
; g c= f +* (x,y)
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; verum