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