let m be non empty Element of NAT ; for X being Subset of (REAL m)
for I being non empty FinSequence of NAT
for f, g being PartFunc of (REAL m),REAL st X is open & rng I c= Seg m & f is_partial_differentiable_on X,I & g is_partial_differentiable_on X,I holds
for i being Element of NAT st i <= (len I) - 1 holds
( (PartDiffSeq ((f - g),X,I)) . i is_partial_differentiable_on X,I /. (i + 1) & (PartDiffSeq ((f - g),X,I)) . i = ((PartDiffSeq (f,X,I)) . i) - ((PartDiffSeq (g,X,I)) . i) )
let Z be Subset of (REAL m); for I being non empty FinSequence of NAT
for f, g being PartFunc of (REAL m),REAL st Z is open & rng I c= Seg m & f is_partial_differentiable_on Z,I & g is_partial_differentiable_on Z,I holds
for i being Element of NAT st i <= (len I) - 1 holds
( (PartDiffSeq ((f - g),Z,I)) . i is_partial_differentiable_on Z,I /. (i + 1) & (PartDiffSeq ((f - g),Z,I)) . i = ((PartDiffSeq (f,Z,I)) . i) - ((PartDiffSeq (g,Z,I)) . i) )
let I be non empty FinSequence of NAT ; for f, g being PartFunc of (REAL m),REAL st Z is open & rng I c= Seg m & f is_partial_differentiable_on Z,I & g is_partial_differentiable_on Z,I holds
for i being Element of NAT st i <= (len I) - 1 holds
( (PartDiffSeq ((f - g),Z,I)) . i is_partial_differentiable_on Z,I /. (i + 1) & (PartDiffSeq ((f - g),Z,I)) . i = ((PartDiffSeq (f,Z,I)) . i) - ((PartDiffSeq (g,Z,I)) . i) )
let f, g be PartFunc of (REAL m),REAL; ( Z is open & rng I c= Seg m & f is_partial_differentiable_on Z,I & g is_partial_differentiable_on Z,I implies for i being Element of NAT st i <= (len I) - 1 holds
( (PartDiffSeq ((f - g),Z,I)) . i is_partial_differentiable_on Z,I /. (i + 1) & (PartDiffSeq ((f - g),Z,I)) . i = ((PartDiffSeq (f,Z,I)) . i) - ((PartDiffSeq (g,Z,I)) . i) ) )
assume AS:
( Z is open & rng I c= Seg m & f is_partial_differentiable_on Z,I & g is_partial_differentiable_on Z,I )
; for i being Element of NAT st i <= (len I) - 1 holds
( (PartDiffSeq ((f - g),Z,I)) . i is_partial_differentiable_on Z,I /. (i + 1) & (PartDiffSeq ((f - g),Z,I)) . i = ((PartDiffSeq (f,Z,I)) . i) - ((PartDiffSeq (g,Z,I)) . i) )
defpred S1[ Element of NAT ] means ( $1 <= (len I) - 1 implies ( (PartDiffSeq ((f - g),Z,I)) . $1 is_partial_differentiable_on Z,I /. ($1 + 1) & (PartDiffSeq ((f - g),Z,I)) . $1 = ((PartDiffSeq (f,Z,I)) . $1) - ((PartDiffSeq (g,Z,I)) . $1) ) );
reconsider Z0 = 0 as Element of NAT ;
A9:
S1[ 0 ]
proof
assume
0 <= (len I) - 1
;
( (PartDiffSeq ((f - g),Z,I)) . 0 is_partial_differentiable_on Z,I /. (0 + 1) & (PartDiffSeq ((f - g),Z,I)) . 0 = ((PartDiffSeq (f,Z,I)) . 0) - ((PartDiffSeq (g,Z,I)) . 0) )
then Q2:
(
(PartDiffSeq (f,Z,I)) . Z0 is_partial_differentiable_on Z,
I /. (Z0 + 1) &
(PartDiffSeq (g,Z,I)) . Z0 is_partial_differentiable_on Z,
I /. (Z0 + 1) )
by AS, TDef6;
(
f = (PartDiffSeq (f,Z,I)) . Z0 &
f - g = (PartDiffSeq ((f - g),Z,I)) . Z0 )
by TDef5;
then Q5:
(PartDiffSeq ((f - g),Z,I)) . Z0 = ((PartDiffSeq (f,Z,I)) . Z0) - ((PartDiffSeq (g,Z,I)) . Z0)
by TDef5;
1
<= len I
by FINSEQ_1:20;
then
I /. 1
in Seg m
by AS, XCWLM1;
then
( 1
<= I /. 1 &
I /. 1
<= m )
by FINSEQ_1:1;
hence
(
(PartDiffSeq ((f - g),Z,I)) . 0 is_partial_differentiable_on Z,
I /. (0 + 1) &
(PartDiffSeq ((f - g),Z,I)) . 0 = ((PartDiffSeq (f,Z,I)) . 0) - ((PartDiffSeq (g,Z,I)) . 0) )
by Q5, AS, Q2, XXX2;
verum
end;
A7:
for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be
Element of
NAT ;
( S1[k] implies S1[k + 1] )
assume A8:
S1[
k]
;
S1[k + 1]
assume A81:
k + 1
<= (len I) - 1
;
( (PartDiffSeq ((f - g),Z,I)) . (k + 1) is_partial_differentiable_on Z,I /. ((k + 1) + 1) & (PartDiffSeq ((f - g),Z,I)) . (k + 1) = ((PartDiffSeq (f,Z,I)) . (k + 1)) - ((PartDiffSeq (g,Z,I)) . (k + 1)) )
B1:
k <= k + 1
by NAT_1:11;
then A82:
k <= (len I) - 1
by A81, XXREAL_0:2;
A84:
(
(PartDiffSeq (f,Z,I)) . (k + 1) is_partial_differentiable_on Z,
I /. ((k + 1) + 1) &
(PartDiffSeq (g,Z,I)) . (k + 1) is_partial_differentiable_on Z,
I /. ((k + 1) + 1) )
by A81, AS, TDef6;
k + 1
<= ((len I) - 1) + 1
by A82, XREAL_1:6;
then
I /. (k + 1) in Seg m
by AS, XCWLM1, NAT_1:11;
then Q4:
( 1
<= I /. (k + 1) &
I /. (k + 1) <= m )
by FINSEQ_1:1;
A85:
(
(PartDiffSeq (f,Z,I)) . k is_partial_differentiable_on Z,
I /. (k + 1) &
(PartDiffSeq (g,Z,I)) . k is_partial_differentiable_on Z,
I /. (k + 1) )
by A82, AS, TDef6;
R1:
(PartDiffSeq (f,Z,I)) . (k + 1) = ((PartDiffSeq (f,Z,I)) . k) `partial| (
Z,
(I /. (k + 1)))
by TDef5;
(k + 1) + 1
<= ((len I) - 1) + 1
by A81, XREAL_1:6;
then
I /. ((k + 1) + 1) in Seg m
by AS, XCWLM1, NAT_1:11;
then Q5:
( 1
<= I /. ((k + 1) + 1) &
I /. ((k + 1) + 1) <= m )
by FINSEQ_1:1;
A86:
(PartDiffSeq ((f - g),Z,I)) . (k + 1) =
((PartDiffSeq ((f - g),Z,I)) . k) `partial| (
Z,
(I /. (k + 1)))
by TDef5
.=
(((PartDiffSeq (f,Z,I)) . k) `partial| (Z,(I /. (k + 1)))) - (((PartDiffSeq (g,Z,I)) . k) `partial| (Z,(I /. (k + 1))))
by A85, AS, Q4, XXX2, B1, A8, A81, XXREAL_0:2
.=
((PartDiffSeq (f,Z,I)) . (k + 1)) - ((PartDiffSeq (g,Z,I)) . (k + 1))
by R1, TDef5
;
hence
(PartDiffSeq ((f - g),Z,I)) . (k + 1) is_partial_differentiable_on Z,
I /. ((k + 1) + 1)
by AS, A84, Q5, XXX2;
(PartDiffSeq ((f - g),Z,I)) . (k + 1) = ((PartDiffSeq (f,Z,I)) . (k + 1)) - ((PartDiffSeq (g,Z,I)) . (k + 1))
thus
(PartDiffSeq ((f - g),Z,I)) . (k + 1) = ((PartDiffSeq (f,Z,I)) . (k + 1)) - ((PartDiffSeq (g,Z,I)) . (k + 1))
by A86;
verum
end;
for n being Element of NAT holds S1[n]
from NAT_1:sch 1(A9, A7);
hence
for i being Element of NAT st i <= (len I) - 1 holds
( (PartDiffSeq ((f - g),Z,I)) . i is_partial_differentiable_on Z,I /. (i + 1) & (PartDiffSeq ((f - g),Z,I)) . i = ((PartDiffSeq (f,Z,I)) . i) - ((PartDiffSeq (g,Z,I)) . i) )
; verum