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
A1: f1 c= g1 and
A2: f2 c= g2 and
A3: dom f1 misses dom g2 ; :: thesis: f1 +* f2 c= g1 +* g2
A4: f1 c= g1 +* g2 by A1, A3, Th117;
g2 c= g1 +* g2 by Th25;
then f2 c= g1 +* g2 by A2;
hence f1 +* f2 c= g1 +* g2 by A4, Th87; :: thesis: verum