let S be RealNormSpace-Sequence; :: thesis: for T being RealNormSpace
for Z being Subset of (product S)
for f, g being PartFunc of (product S),T
for i being set st Z is open & i in dom S & f is_partial_differentiable_on Z,i & g is_partial_differentiable_on Z,i holds
( f - g is_partial_differentiable_on Z,i & (f - g) `partial| (Z,i) = (f `partial| (Z,i)) - (g `partial| (Z,i)) )
let T be RealNormSpace; :: thesis: for Z being Subset of (product S)
for f, g being PartFunc of (product S),T
for i being set st Z is open & i in dom S & f is_partial_differentiable_on Z,i & g is_partial_differentiable_on Z,i holds
( f - g is_partial_differentiable_on Z,i & (f - g) `partial| (Z,i) = (f `partial| (Z,i)) - (g `partial| (Z,i)) )
let Z be Subset of (product S); :: thesis: for f, g being PartFunc of (product S),T
for i being set st Z is open & i in dom S & f is_partial_differentiable_on Z,i & g is_partial_differentiable_on Z,i holds
( f - g is_partial_differentiable_on Z,i & (f - g) `partial| (Z,i) = (f `partial| (Z,i)) - (g `partial| (Z,i)) )
let f, g be PartFunc of (product S),T; :: thesis: for i being set st Z is open & i in dom S & f is_partial_differentiable_on Z,i & g is_partial_differentiable_on Z,i holds
( f - g is_partial_differentiable_on Z,i & (f - g) `partial| (Z,i) = (f `partial| (Z,i)) - (g `partial| (Z,i)) )
let i be set ; :: thesis: ( Z is open & i in dom S & f is_partial_differentiable_on Z,i & g is_partial_differentiable_on Z,i implies ( f - g is_partial_differentiable_on Z,i & (f - g) `partial| (Z,i) = (f `partial| (Z,i)) - (g `partial| (Z,i)) ) )
assume that
A1: ( Z is open & i in dom S ) and
A2: f is_partial_differentiable_on Z,i and
A3: g is_partial_differentiable_on Z,i ; :: thesis: ( f - g is_partial_differentiable_on Z,i & (f - g) `partial| (Z,i) = (f `partial| (Z,i)) - (g `partial| (Z,i)) )
A4: ( - g is_partial_differentiable_on Z,i & (- g) `partial| (Z,i) = - (g `partial| (Z,i)) ) by A1, A3, Th28;
A5: f - g = f + (- g) by VFUNCT_1:25;
hence f - g is_partial_differentiable_on Z,i by A1, A2, A4, Th21; :: thesis: (f - g) `partial| (Z,i) = (f `partial| (Z,i)) - (g `partial| (Z,i))
thus (f - g) `partial| (Z,i) = (f `partial| (Z,i)) + (- (g `partial| (Z,i))) by A1, A2, A4, A5, Th21
.= (f `partial| (Z,i)) - (g `partial| (Z,i)) by VFUNCT_1:25 ; :: thesis: verum