let f, g, h be Function; :: thesis: ( f c= g & dom f misses dom h implies f c= g +* h )
assume f c= g ; :: thesis: ( not dom f misses dom h or f c= g +* h )
then A1: f +* h c= g +* h by Th123;
assume dom f misses dom h ; :: thesis: f c= g +* h
then f c= f +* h by Th32;
hence f c= g +* h by A1; :: thesis: verum