let f, g, h be Function; :: thesis: ( f c= g implies f +* h c= g +* h )
assume A1: f c= g ; :: thesis: f +* h c= g +* h

now :: thesis: ( dom (f +* h) c= dom (g +* h) & ( for x being object st x in dom (f +* h) holds
(f +* h) . x = (g +* h) . x ) )

( dom (f +* h) = (dom f) \/ (dom h) & dom (g +* h) = (dom g) \/ (dom h) ) by Def1;
hence dom (f +* h) c= dom (g +* h) by A1, RELAT_1:11, XBOOLE_1:9; :: thesis: for x being object st x in dom (f +* h) holds
(f +* h) . b₂ = (g +* h) . b₂
let x be object ; :: thesis: ( x in dom (f +* h) implies (f +* h) . b₁ = (g +* h) . b₁ )
assume x in dom (f +* h) ; :: thesis: (f +* h) . b₁ = (g +* h) . b₁
then A2: ( x in dom f or x in dom h ) by Th12;

per cases ( x in dom h or not x in dom h ) ;

suppose A3: x in dom h ; :: thesis: (f +* h) . b₁ = (g +* h) . b₁

hence (f +* h) . x = h . x by Th13
.= (g +* h) . x by A3, Th13 ;
:: thesis: verum

end;

suppose A4: not x in dom h ; :: thesis: (f +* h) . b₁ = (g +* h) . b₁

then ( (f +* h) . x = f . x & (g +* h) . x = g . x ) by Th11;
hence (f +* h) . x = (g +* h) . x by A1, A2, A4, GRFUNC_1:2; :: thesis: verum

end;

end;

end;

hence f +* h c= g +* h by GRFUNC_1:2; :: thesis: verum