let f, g, h be Function; :: thesis: ( dom f misses dom h & f c= g implies f c= g +* h )
assume that
A1: dom f misses dom h and
A2: f c= g ; :: thesis: f c= g +* h
A3: (g +* h) | (dom f) = (g | (dom f)) +* (h | (dom f)) by Th71
.= (g | (dom f)) +* {} by A1, RELAT_1:66
.= g | (dom f) ;
f | (dom f) = f ;
then f c= (g +* h) | (dom f) by A2, A3, RELAT_1:76;
hence f c= g +* h by RELAT_1:184; :: thesis: verum