let E be Real; for q, S being FinSequence of REAL st len S = len q & ( for i being Nat st i in dom S holds
ex r being Real st
( r = q . i & S . i = r * E ) ) holds
Sum S = (Sum q) * E
defpred S1[ Nat] means for q, S being FinSequence of REAL st $1 = len S & len S = len q & ( for i being Nat st i in dom S holds
ex r being Real st
( r = q . i & S . i = r * E ) ) holds
Sum S = (Sum q) * E;
A1:
S1[ 0 ]
A3:
now for i being Nat st S1[i] holds
S1[i + 1]let i be
Nat;
( S1[i] implies S1[i + 1] )assume A4:
S1[
i]
;
S1[i + 1]now for q, S being FinSequence of REAL st i + 1 = len S & len S = len q & ( for i being Nat st i in dom S holds
ex r being Real st
( r = q . i & S . i = r * E ) ) holds
Sum S = (Sum q) * Elet q,
S be
FinSequence of
REAL ;
( i + 1 = len S & len S = len q & ( for i being Nat st i in dom S holds
ex r being Real st
( r = q . i & S . i = r * E ) ) implies Sum S = (Sum q) * E )set S0 =
S | i;
set q0 =
q | i;
assume A5:
(
i + 1
= len S &
len S = len q & ( for
i being
Nat st
i in dom S holds
ex
r being
Real st
(
r = q . i &
S . i = r * E ) ) )
;
Sum S = (Sum q) * EA6:
for
k being
Nat st
k in dom (S | i) holds
ex
r being
Real st
(
r = (q | i) . k &
(S | i) . k = r * E )
dom S = Seg (i + 1)
by A5, FINSEQ_1:def 3;
then consider r being
Real such that A9:
(
r = q . (i + 1) &
S . (i + 1) = r * E )
by A5, FINSEQ_1:4;
A10:
( 1
<= i + 1 &
i + 1
<= len q )
by A5, NAT_1:11;
q = (q | i) ^ <*(q /. (i + 1))*>
by A5, FINSEQ_5:21;
then
q = (q | i) ^ <*(q . (i + 1))*>
by A10, FINSEQ_4:15;
then
(Sum q) * E = ((Sum (q | i)) + (q . (i + 1))) * E
by RVSUM_1:74;
then A11:
(Sum q) * E = ((Sum (q | i)) * E) + ((q . (i + 1)) * E)
;
A12:
(
i = len (S | i) &
i = len (q | i) )
by A5, FINSEQ_1:59, NAT_1:11;
reconsider v =
S . (i + 1) as
Real ;
S = (S | i) ^ <*(S /. (len S))*>
by A5, FINSEQ_5:21;
then
S = (S | i) ^ <*v*>
by A5, A10, FINSEQ_4:15;
then
Sum S = (Sum (S | i)) + v
by RVSUM_1:74;
hence
Sum S = (Sum q) * E
by A4, A6, A9, A11, A12;
verum end; hence
S1[
i + 1]
;
verum end;
for i being Nat holds S1[i]
from NAT_1:sch 2(A1, A3);
hence
for q, S being FinSequence of REAL st len S = len q & ( for i being Nat st i in dom S holds
ex r being Real st
( r = q . i & S . i = r * E ) ) holds
Sum S = (Sum q) * E
; verum