let f, g, h be real-valued Function; :: thesis: ( f c= g implies h - f c= h - g )
A1: dom (h - g) = (dom h) /\ (dom g) by VALUED_1:12;
A2: dom (h - f) = (dom h) /\ (dom f) by VALUED_1:12;
assume A3: f c= g ; :: thesis: h - f c= h - g
then dom f c= dom g by GRFUNC_1:2;
then A4: dom (h - f) c= dom (h - g) by A1, A2, XBOOLE_1:27;
now :: thesis: for x being object st x in dom (h - f) holds
(h - f) . x = (h - g) . x
let x be object ; :: thesis: ( x in dom (h - f) implies (h - f) . x = (h - g) . x )
assume A5: x in dom (h - f) ; :: thesis: (h - f) . x = (h - g) . x
then A6: x in dom f by A2, XBOOLE_0:def 4;
thus (h - f) . x = (h . x) - (f . x) by A5, VALUED_1:13
.= (h . x) - (g . x) by A3, A6, GRFUNC_1:2
.= (h - g) . x by A4, A5, VALUED_1:13 ; :: thesis: verum
end;
hence h - f c= h - g by A4, GRFUNC_1:2; :: thesis: verum