let R be Ring; :: thesis: for V being RightMod of R
for a being Scalar of R
for F, G being FinSequence of V st len F = len G & ( for k being Nat
for v being Vector of V st k in dom F & v = G . k holds
F . k = v * a ) holds
Sum F = (Sum G) * a
let V be RightMod of R; :: thesis: for a being Scalar of R
for F, G being FinSequence of V st len F = len G & ( for k being Nat
for v being Vector of V st k in dom F & v = G . k holds
F . k = v * a ) holds
Sum F = (Sum G) * a
let a be Scalar of R; :: thesis: for F, G being FinSequence of V st len F = len G & ( for k being Nat
for v being Vector of V st k in dom F & v = G . k holds
F . k = v * a ) holds
Sum F = (Sum G) * a
let F, G be FinSequence of V; :: thesis: ( len F = len G & ( for k being Nat
for v being Vector of V st k in dom F & v = G . k holds
F . k = v * a ) implies Sum F = (Sum G) * a )
defpred S₁[ Nat] means for H, I being FinSequence of V st len H = len I & len H = $1 & ( for k being Nat
for v being Vector of V st k in dom H & v = I . k holds
H . k = v * a ) holds
Sum H = (Sum I) * a;

now :: thesis: for n being Nat st ( for H, I being FinSequence of V st len H = len I & len H = n & ( for k being Nat
for v being Vector of V st k in dom H & v = I . k holds
H . k = v * a ) holds
Sum H = (Sum I) * a ) holds
for H, I being FinSequence of V st len H = len I & len H = n + 1 & ( for k being Nat
for v being Vector of V st k in dom H & v = I . k holds
H . k = v * a ) holds
Sum H = (Sum I) * a

let n be Nat; :: thesis: ( ( for H, I being FinSequence of V st len H = len I & len H = n & ( for k being Nat
for v being Vector of V st k in dom H & v = I . k holds
H . k = v * a ) holds
Sum H = (Sum I) * a ) implies for H, I being FinSequence of V st len H = len I & len H = n + 1 & ( for k being Nat
for v being Vector of V st k in dom H & v = I . k holds
H . k = v * a ) holds
Sum H = (Sum I) * a )
assume A1: for H, I being FinSequence of V st len H = len I & len H = n & ( for k being Nat
for v being Vector of V st k in dom H & v = I . k holds
H . k = v * a ) holds
Sum H = (Sum I) * a ; :: thesis: for H, I being FinSequence of V st len H = len I & len H = n + 1 & ( for k being Nat
for v being Vector of V st k in dom H & v = I . k holds
H . k = v * a ) holds
Sum H = (Sum I) * a
let H, I be FinSequence of V; :: thesis: ( len H = len I & len H = n + 1 & ( for k being Nat
for v being Vector of V st k in dom H & v = I . k holds
H . k = v * a ) implies Sum H = (Sum I) * a )
assume that
A2: len H = len I and
A3: len H = n + 1 and
A4: for k being Nat
for v being Vector of V st k in dom H & v = I . k holds
H . k = v * a ; :: thesis: Sum H = (Sum I) * a
reconsider p = H | (Seg n), q = I | (Seg n) as FinSequence of V by FINSEQ_1:18;
A5: n <= n + 1 by NAT_1:12;
then A6: len p = n by A3, FINSEQ_1:17;
A7: len q = n by A2, A3, A5, FINSEQ_1:17;

A8: now :: thesis: for k being Nat
for v being Vector of V st k in dom p & v = q . k holds
p . k = v * a

len p <= len H by A3, A5, FINSEQ_1:17;
then A9: dom p c= dom H by FINSEQ_3:30;
let k be Nat; :: thesis: for v being Vector of V st k in dom p & v = q . k holds
p . k = v * a
let v be Vector of V; :: thesis: ( k in dom p & v = q . k implies p . k = v * a )
assume that
A10: k in dom p and
A11: v = q . k ; :: thesis: p . k = v * a
dom p = dom q by A6, A7, FINSEQ_3:29;
then I . k = q . k by A10, FUNCT_1:47;
then H . k = v * a by A4, A10, A11, A9;
hence p . k = v * a by A10, FUNCT_1:47; :: thesis: verum

end;

A12: n + 1 in Seg (n + 1) by FINSEQ_1:4;
then ( n + 1 in dom H & n + 1 in dom I ) by A2, A3, FINSEQ_1:def 3;
then reconsider v1 = H . (n + 1), v2 = I . (n + 1) as Vector of V by FINSEQ_2:11;
n + 1 in dom H by A3, A12, FINSEQ_1:def 3;
then A13: v1 = v2 * a by A4;
thus Sum H = (Sum p) + v1 by A3, A6, Lm1
.= ((Sum q) * a) + (v2 * a) by A1, A6, A7, A8, A13
.= ((Sum q) + v2) * a by VECTSP_2:def 9
.= (Sum I) * a by A2, A3, A7, Lm1 ; :: thesis: verum

end;

then A14: for i being Nat st S₁[i] holds
S₁[i + 1] ;

now :: thesis: for H, I being FinSequence of V st len H = len I & len H = 0 & ( for k being Nat
for v being Vector of V st k in dom H & v = I . k holds
H . k = v * a ) holds
Sum H = (Sum I) * a

let H, I be FinSequence of V; :: thesis: ( len H = len I & len H = 0 & ( for k being Nat
for v being Vector of V st k in dom H & v = I . k holds
H . k = v * a ) implies Sum H = (Sum I) * a )
assume that
A15: len H = len I and
A16: len H = 0 and
for k being Nat
for v being Vector of V st k in dom H & v = I . k holds
H . k = v * a ; :: thesis: Sum H = (Sum I) * a
H = <*> the carrier of V by A16;
then A17: Sum H = 0. V by RLVECT_1:43;
I = <*> the carrier of V by A15, A16;
then Sum I = 0. V by RLVECT_1:43;
hence Sum H = (Sum I) * a by A17, VECTSP_2:32; :: thesis: verum

end;

then A18: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A18, A14);
hence ( len F = len G & ( for k being Nat
for v being Vector of V st k in dom F & v = G . k holds
F . k = v * a ) implies Sum F = (Sum G) * a ) ; :: thesis: verum