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) . b2 = (g +* h) . b2
let x be object ; :: thesis: ( x in dom (f +* h) implies (f +* h) . b1 = (g +* h) . b1 )
assume x in dom (f +* h) ; :: thesis: (f +* h) . b1 = (g +* h) . b1
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) . b1 = (g +* h) . b1
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) . b1 = (g +* h) . b1
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