let m be non zero Element of NAT ; for X being Subset of (REAL m)
for f, g being PartFunc of (REAL m),REAL st X c= dom f & X c= dom g & f is_differentiable_on X & g is_differentiable_on X holds
( f - g is_differentiable_on X & ( for x being Element of REAL m st x in X holds
((f - g) `| X) /. x = ((f `| X) /. x) - ((g `| X) /. x) ) )
let X be Subset of (REAL m); for f, g being PartFunc of (REAL m),REAL st X c= dom f & X c= dom g & f is_differentiable_on X & g is_differentiable_on X holds
( f - g is_differentiable_on X & ( for x being Element of REAL m st x in X holds
((f - g) `| X) /. x = ((f `| X) /. x) - ((g `| X) /. x) ) )
let f, g be PartFunc of (REAL m),REAL; ( X c= dom f & X c= dom g & f is_differentiable_on X & g is_differentiable_on X implies ( f - g is_differentiable_on X & ( for x being Element of REAL m st x in X holds
((f - g) `| X) /. x = ((f `| X) /. x) - ((g `| X) /. x) ) ) )
assume A1:
( X c= dom f & X c= dom g )
; ( not f is_differentiable_on X or not g is_differentiable_on X or ( f - g is_differentiable_on X & ( for x being Element of REAL m st x in X holds
((f - g) `| X) /. x = ((f `| X) /. x) - ((g `| X) /. x) ) ) )
assume A2:
( f is_differentiable_on X & g is_differentiable_on X )
; ( f - g is_differentiable_on X & ( for x being Element of REAL m st x in X holds
((f - g) `| X) /. x = ((f `| X) /. x) - ((g `| X) /. x) ) )
then A3:
X is open
by A1, Th55;
dom (f - g) = (dom f) /\ (dom g)
by VALUED_1:12;
then A4:
X c= dom (f - g)
by A1, XBOOLE_1:19;
A5:
now for x being Element of REAL m st x in X holds
( f - g is_differentiable_in x & diff ((f - g),x) = (diff (f,x)) - (diff (g,x)) )let x be
Element of
REAL m;
( x in X implies ( f - g is_differentiable_in x & diff ((f - g),x) = (diff (f,x)) - (diff (g,x)) ) )assume
x in X
;
( f - g is_differentiable_in x & diff ((f - g),x) = (diff (f,x)) - (diff (g,x)) )then
(
f is_differentiable_in x &
g is_differentiable_in x )
by A1, A2, A3, Th54;
hence
(
f - g is_differentiable_in x &
diff (
(f - g),
x)
= (diff (f,x)) - (diff (g,x)) )
by Th51;
verum end;
then
for x being Element of REAL m st x in X holds
f - g is_differentiable_in x
;
hence
f - g is_differentiable_on X
by A4, A3, Th54; for x being Element of REAL m st x in X holds
((f - g) `| X) /. x = ((f `| X) /. x) - ((g `| X) /. x)
let x be Element of REAL m; ( x in X implies ((f - g) `| X) /. x = ((f `| X) /. x) - ((g `| X) /. x) )
assume A6:
x in X
; ((f - g) `| X) /. x = ((f `| X) /. x) - ((g `| X) /. x)
then
((f - g) `| X) /. x = diff ((f - g),x)
by A4, Def4;
then
((f - g) `| X) /. x = (diff (f,x)) - (diff (g,x))
by A6, A5;
then
((f - g) `| X) /. x = ((f `| X) /. x) - (diff (g,x))
by A1, A6, Def4;
hence
((f - g) `| X) /. x = ((f `| X) /. x) - ((g `| X) /. x)
by A1, A6, Def4; verum