let f, g be Function; :: thesis: ( f c= g implies ( f +* g = g & g +* f = g ) )
assume A1: f c= g ; :: thesis: ( f +* g = g & g +* f = g )
then dom f c= dom g by GRFUNC_1:8;
hence A2: f +* g = g by Th20; :: thesis: g +* f = g
f tolerates g by A1, PARTFUN1:135;
hence g +* f = g by A2, Th35; :: thesis: verum