let f, g be Function; :: thesis: ( dom f misses dom g implies f tolerates g )
assume dom f misses dom g ; :: thesis: f tolerates g
then f \/ g is Function by GRFUNC_1:31;
hence f tolerates g by Th130; :: thesis: verum