let m be non zero Nat; :: thesis: for f being PartFunc of (REAL m),REAL
for x being Element of REAL m st f is_differentiable_in x holds
for s being FinSequence of REAL m
for t being FinSequence of REAL st dom s = dom t & ( for i being Nat st i in dom s holds
t . i = (diff (f,x)) . (s . i) ) holds
(diff (f,x)) . (Sum s) = Sum t
let f be PartFunc of (REAL m),REAL; :: thesis: for x being Element of REAL m st f is_differentiable_in x holds
for s being FinSequence of REAL m
for t being FinSequence of REAL st dom s = dom t & ( for i being Nat st i in dom s holds
t . i = (diff (f,x)) . (s . i) ) holds
(diff (f,x)) . (Sum s) = Sum t
let x be Element of REAL m; :: thesis: ( f is_differentiable_in x implies for s being FinSequence of REAL m
for t being FinSequence of REAL st dom s = dom t & ( for i being Nat st i in dom s holds
t . i = (diff (f,x)) . (s . i) ) holds
(diff (f,x)) . (Sum s) = Sum t )
assume A1: f is_differentiable_in x ; :: thesis: for s being FinSequence of REAL m
for t being FinSequence of REAL st dom s = dom t & ( for i being Nat st i in dom s holds
t . i = (diff (f,x)) . (s . i) ) holds
(diff (f,x)) . (Sum s) = Sum t
defpred S₁[ Nat] means for s being FinSequence of REAL m
for t being FinSequence of REAL st len s = $1 & dom s = dom t & ( for i being Nat st i in dom s holds
t . i = (diff (f,x)) . (s . i) ) holds
(diff (f,x)) . (Sum s) = Sum t;
A2: S₁[ 0 ]

proof

let s be FinSequence of REAL m; :: thesis: for t being FinSequence of REAL st len s = 0 & dom s = dom t & ( for i being Nat st i in dom s holds
t . i = (diff (f,x)) . (s . i) ) holds
(diff (f,x)) . (Sum s) = Sum t
let t be FinSequence of REAL ; :: thesis: ( len s = 0 & dom s = dom t & ( for i being Nat st i in dom s holds
t . i = (diff (f,x)) . (s . i) ) implies (diff (f,x)) . (Sum s) = Sum t )
assume A3: ( len s = 0 & dom s = dom t & ( for i being Nat st i in dom s holds
t . i = (diff (f,x)) . (s . i) ) ) ; :: thesis: (diff (f,x)) . (Sum s) = Sum t
then Sum s = 0* m by EUCLID_7:def 11;
then A4: (diff (f,x)) . (Sum s) = (diff (f,x)) . (0 * (Sum s)) by EUCLID_4:3
.= 0 * ((diff (f,x)) . (Sum s)) by A1, Th24
.= 0 ;
dom t = Seg (len s) by A3, FINSEQ_1:def 3;
then t = <*> REAL by A3;
hence (diff (f,x)) . (Sum s) = Sum t by A4, RVSUM_1:72; :: thesis: verum

end;

A5: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A6: S₁[n] ; :: thesis: S₁[n + 1]
let s be FinSequence of REAL m; :: thesis: for t being FinSequence of REAL st len s = n + 1 & dom s = dom t & ( for i being Nat st i in dom s holds
t . i = (diff (f,x)) . (s . i) ) holds
(diff (f,x)) . (Sum s) = Sum t
let t be FinSequence of REAL ; :: thesis: ( len s = n + 1 & dom s = dom t & ( for i being Nat st i in dom s holds
t . i = (diff (f,x)) . (s . i) ) implies (diff (f,x)) . (Sum s) = Sum t )
assume A7: ( len s = n + 1 & dom s = dom t & ( for i being Nat st i in dom s holds
t . i = (diff (f,x)) . (s . i) ) ) ; :: thesis: (diff (f,x)) . (Sum s) = Sum t
reconsider sn = s | n as FinSequence of REAL m ;
reconsider tn = t | n as FinSequence of REAL ;
A8: n <= n + 1 by NAT_1:11;
A9: len sn = n by A7, FINSEQ_1:59, NAT_1:11;
dom t = Seg (len s) by FINSEQ_1:def 3, A7;
then A10: len t = n + 1 by A7, FINSEQ_1:def 3;
then len tn = n by FINSEQ_1:59, NAT_1:11;
then A11: dom tn = Seg n by FINSEQ_1:def 3
.= dom sn by A9, FINSEQ_1:def 3 ;
A12: for i being Nat st i in dom sn holds
tn . i = (diff (f,x)) . (sn . i)

proof

let i be Nat; :: thesis: ( i in dom sn implies tn . i = (diff (f,x)) . (sn . i) )
assume i in dom sn ; :: thesis: tn . i = (diff (f,x)) . (sn . i)
then A13: i in Seg n by A9, FINSEQ_1:def 3;
then i in Seg (n + 1) by A8, FINSEQ_1:5, TARSKI:def 3;
then i in dom s by A7, FINSEQ_1:def 3;
then A14: t . i = (diff (f,x)) . (s . i) by A7;
t . i = tn . i by A13, FUNCT_1:49;
hence tn . i = (diff (f,x)) . (sn . i) by A13, A14, FUNCT_1:49; :: thesis: verum

end;

A15: s = sn ^ <*(s . (n + 1))*> by A7, FINSEQ_3:55;
A16: t = tn ^ <*(t . (n + 1))*> by A10, FINSEQ_3:55;
n + 1 in Seg (n + 1) by FINSEQ_1:4;
then A17: n + 1 in dom s by A7, FINSEQ_1:def 3;
then s . (n + 1) in rng s by FUNCT_1:3;
then reconsider sn1 = s . (n + 1) as Element of REAL m ;
t . (n + 1) in rng t by A7, A17, FUNCT_1:3;
then reconsider tn1 = t . (n + 1) as Element of REAL ;
thus (diff (f,x)) . (Sum s) = (diff (f,x)) . ((Sum sn) + sn1) by A15, Th3
.= ((diff (f,x)) . (Sum sn)) + ((diff (f,x)) . sn1) by A1, Th23
.= (Sum tn) + ((diff (f,x)) . sn1) by A6, A9, A11, A12
.= (Sum tn) + tn1 by A7, A17
.= Sum t by A16, RVSUM_1:74 ; :: thesis: verum

end;

A18: for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A5);
let s be FinSequence of REAL m; :: thesis: for t being FinSequence of REAL st dom s = dom t & ( for i being Nat st i in dom s holds
t . i = (diff (f,x)) . (s . i) ) holds
(diff (f,x)) . (Sum s) = Sum t
let t be FinSequence of REAL ; :: thesis: ( dom s = dom t & ( for i being Nat st i in dom s holds
t . i = (diff (f,x)) . (s . i) ) implies (diff (f,x)) . (Sum s) = Sum t )
assume A19: ( dom s = dom t & ( for i being Nat st i in dom s holds
t . i = (diff (f,x)) . (s . i) ) ) ; :: thesis: (diff (f,x)) . (Sum s) = Sum t
( len s is Nat & len s = len s ) ;
hence (diff (f,x)) . (Sum s) = Sum t by A18, A19; :: thesis: verum