let f, g be Function; :: thesis: ( f c= g implies g +* f = g )
assume A1: f c= g ; :: thesis: g +* f = g
then f tolerates g by PARTFUN1:54;
hence g +* f = f \/ g by Th30
.= g by A1, XBOOLE_1:12 ;
:: thesis: verum