let f, g 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 object st x in dom g holds
(f +* g) . x = g . x by Th13;
hence g c= f +* g by A1, GRFUNC_1:2; :: thesis: verum