let f1, f2, g1, g2 be Function; :: thesis: ( f1 c= g1 & f2 c= g2 & dom f1 misses dom g2 implies f1 +* f2 c= g1 +* g2 )
assume that
Z1: f1 c= g1 and
Z2: f2 c= g2 and
Z3: dom f1 misses dom g2 ; :: thesis: f1 +* f2 c= g1 +* g2
A: f1 c= g1 +* g2 by Z1, Z3, Th125;
g2 c= g1 +* g2 by Th26;
then f2 c= g1 +* g2 by Z2, XBOOLE_1:1;
hence f1 +* f2 c= g1 +* g2 by A, Th92; :: thesis: verum