let f, h, g be Function; :: thesis: ( dom f misses dom h & f c= g +* h implies f c= g )
assume that
Z1: dom f misses dom h and
Z2: f c= g +* h ; :: thesis: f c= g
A: (g +* h) | (dom f) = (g | (dom f)) +* (h | (dom f)) by Th75
.= (g | (dom f)) +* {} by Z1, RELAT_1:95
.= g | (dom f) by Th22 ;
f | (dom f) = f by RELAT_1:98;
then f c= g | (dom f) by Z2, A, RELAT_1:105;
hence f c= g by RELAT_1:219; :: thesis: verum