let Y be RealNormSpace; for E being Point of Y
for q being FinSequence of REAL
for S being FinSequence of Y 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
let E be Point of Y; for q being FinSequence of REAL
for S being FinSequence of Y 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 being FinSequence of REAL
for S being FinSequence of Y 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 being FinSequence of REAL
for S being FinSequence of Y 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 be
FinSequence of
REAL ;
for S being FinSequence of Y 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 S be
FinSequence of
Y;
( 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)
by RLVECT_1:def 6;
A12:
(
i = len (S | i) &
i = len (q | i) )
by FINSEQ_1:59, A5, NAT_1:11;
reconsider v =
S . (i + 1) as
Point of
Y by A9;
S | i = S | (dom (S | i))
by FINSEQ_1:def 3, A12;
then
Sum S = (Sum (S | i)) + v
by A5, A12, RLVECT_1:38;
hence
Sum S = (Sum q) * E
by A9, A4, A6, A12, A11;
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 being FinSequence of REAL
for S being FinSequence of Y 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