let f, g be Function; :: thesis: ( g c= f implies f +* g = f )
assume A1: g c= f ; :: thesis: f +* g = f
then dom g c= dom f by GRFUNC_1:2;
then A2: dom f = (dom f) \/ (dom g) by XBOOLE_1:12;
for x being object st x in dom f holds
( ( x in dom g implies f . x = g . x ) & ( not x in dom g implies f . x = f . x ) ) by A1, GRFUNC_1:2;
hence f +* g = f by A2, FUNCT_4:def 1; :: thesis: verum