let a be FinSequence of REAL ; :: thesis: for s being XFinSequence of st len s > len a & s . 0 = 0 & ( for i being Nat st i < len a holds
s . (i + 1) = (s . i) + (a . (i + 1)) ) holds
Sum a = s . (len a)
let s be XFinSequence of ; :: thesis: ( len s > len a & s . 0 = 0 & ( for i being Nat st i < len a holds
s . (i + 1) = (s . i) + (a . (i + 1)) ) implies Sum a = s . (len a) )
assume A1:
( len s > len a & s . 0 = 0 & ( for i being Nat st i < len a holds
s . (i + 1) = (s . i) + (a . (i + 1)) ) )
; :: thesis: Sum a = s . (len a)
defpred S1[ Nat] means ( $1 <= len a implies Sum (a | $1) = s . $1 );
A2:
S1[ 0 ]
by A1, RVSUM_1:102;
A3:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
:: thesis: ( S1[k] implies S1[k + 1] )
assume A4:
S1[
k]
;
:: thesis: S1[k + 1]
reconsider k1 =
k as
Element of
NAT by ORDINAL1:def 13;
reconsider m =
k1 + 1 as
Nat ;
(
k + 1
<= len a implies
Sum (a | m) = s . (k + 1) )
proof
assume A5:
k + 1
<= len a
;
:: thesis: Sum (a | m) = s . (k + 1)
A6:
1
<= k + 1
by NAT_1:11;
A7:
k < len a
by A5, NAT_1:13;
A8:
a | m = (a | k) ^ <*(a /. m)*>
by A5, JORDAN8:2;
reconsider q0 =
a | k as
FinSequence of
REAL ;
reconsider rx =
a /. m as
Element of
REAL ;
reconsider x0 =
<*(a /. m)*> as
FinSequence of
REAL ;
m in Seg m
by A6, FINSEQ_1:3;
then
m in Seg (len (a | m))
by A5, FINSEQ_1:80;
then A9:
m in dom (a | m)
by FINSEQ_1:def 3;
A10:
len (a | m) =
(len q0) + (len <*rx*>)
by A8, FINSEQ_1:35
.=
(len q0) + 1
by FINSEQ_1:57
;
A11:
len (a | m) = m
by A5, FINSEQ_1:80;
m in Seg (len a)
by A5, A6, FINSEQ_1:3;
then A12:
m in dom a
by FINSEQ_1:def 3;
A13:
rx =
(a | m) . m
by A8, A10, A11, FINSEQ_1:59
.=
(a | m) /. m
by A9, PARTFUN1:def 8
.=
a /. m
by A9, FINSEQ_4:85
.=
a . m
by A12, PARTFUN1:def 8
;
Sum x0 = rx
by RVSUM_1:103;
then
Sum (a | m) = (s . k) + rx
by A4, A5, A8, NAT_1:13, RVSUM_1:105;
hence
Sum (a | m) = s . (k + 1)
by A1, A7, A13;
:: thesis: verum
end;
hence
S1[
k + 1]
;
:: thesis: verum
end;
for k being Nat holds S1[k]
from NAT_1:sch 2(A2, A3);
then
S1[ len a]
;
hence
Sum a = s . (len a)
by FINSEQ_1:79; :: thesis: verum