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