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