let g, f be Function; :: thesis: g c= f +* g
dom (f +* g) = (dom f) \/ (dom g) by Def1;
then A1: dom g c= dom (f +* g) by XBOOLE_1:7;
for x being set st x in dom g holds
(f +* g) . x = g . x by Th14;
hence g c= f +* g by A1, GRFUNC_1:2; :: thesis: verum