let f, g, h be Function; :: thesis: ( dom f misses dom h & f c= g +* h implies f c= g )
assume that
A1: dom f misses dom h and
A2: f c= g +* h ; :: thesis: f c= g
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 | (dom f) by A2, A3, RELAT_1:76;
hence f c= g by RELAT_1:184; :: thesis: verum