let f, g, h be real-valued Function; :: thesis: ( f c= g implies f - h c= g - h )
A1: dom (f - h) = (dom f) /\ (dom h) by VALUED_1:12;
A2: dom (g - h) = (dom g) /\ (dom h) by VALUED_1:12;
assume A3: f c= g ; :: thesis: f - h c= g - h
then dom f c= dom g by GRFUNC_1:2;
then A4: dom (f - h) c= dom (g - h) by A1, A2, XBOOLE_1:27;

now :: thesis: for x being object st x in dom (f - h) holds
(f - h) . x = (g - h) . x

let x be object ; :: thesis: ( x in dom (f - h) implies (f - h) . x = (g - h) . x )
assume A5: x in dom (f - h) ; :: thesis: (f - h) . x = (g - h) . x
then A6: x in dom f by A1, XBOOLE_0:def 4;
thus (f - h) . x = (f . x) - (h . x) by A5, VALUED_1:13
.= (g . x) - (h . x) by A3, A6, GRFUNC_1:2
.= (g - h) . x by A4, A5, VALUED_1:13 ; :: thesis: verum

end;

hence f - h c= g - h by A4, GRFUNC_1:2; :: thesis: verum