let f, g be Function; :: thesis: ( dom f misses dom g implies f +* g = g +* f )
assume dom f misses dom g ; :: thesis: f +* g = g +* f
then f tolerates g by PARTFUN1:138;
hence f +* g = g +* f by Th35; :: thesis: verum