let Y be RealNormSpace; :: thesis: 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; :: thesis: 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 S₁[ 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: S₁[ 0 ]

proof

let q be FinSequence of REAL ; :: thesis: for S being FinSequence of Y st 0 = 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
let S be FinSequence of Y; :: thesis: ( 0 = 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 )
assume ( 0 = 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 ) ) ) ; :: thesis: Sum S = (Sum q) * E
then A2: ( <*> the carrier of Y = S & <*> REAL = q ) ;
then (Sum q) * E = 0. Y by RLVECT_1:10, RVSUM_1:72;
hence Sum S = (Sum q) * E by A2, RLVECT_1:43; :: thesis: verum

end;

A3: now :: thesis: for i being Nat st S₁[i] holds
S₁[i + 1]

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A4: S₁[i] ; :: thesis: S₁[i + 1]

now :: thesis: 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) * E

let q be FinSequence of REAL ; :: thesis: 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) * E
let S be FinSequence of Y; :: thesis: ( 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 ) ) ) ; :: thesis: Sum S = (Sum q) * E
A6: 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 )

proof

let k be Nat; :: thesis: ( k in dom (S | i) implies ex r being Real st
( r = (q | i) . k & (S | i) . k = r * E ) )
assume k in dom (S | i) ; :: thesis: ex r being Real st
( r = (q | i) . k & (S | i) . k = r * E )
then A7: ( k in Seg i & k in dom S ) by RELAT_1:57;
then consider r being Real such that
A8: ( r = q . k & S . k = r * E ) by A5;
take r ; :: thesis: ( r = (q | i) . k & (S | i) . k = r * E )
thus ( r = (q | i) . k & (S | i) . k = r * E ) by A8, A7, FUNCT_1:49; :: thesis: verum

end;

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; :: thesis: verum

end;

hence S₁[i + 1] ; :: thesis: verum

end;

for i being Nat holds S₁[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 ; :: thesis: verum