let R be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ; :: thesis: for a being Element of R

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over R

for F, G being FinSequence of V st len F = len G & ( for k being Nat

for v being Element of V st k in dom F & v = G . k holds

F . k = a * v ) holds

Sum F = a * (Sum G)

let a be Element of R; :: thesis: for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over R

for F, G being FinSequence of V st len F = len G & ( for k being Nat

for v being Element of V st k in dom F & v = G . k holds

F . k = a * v ) holds

Sum F = a * (Sum G)

let V be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over R; :: thesis: for F, G being FinSequence of V st len F = len G & ( for k being Nat

for v being Element of V st k in dom F & v = G . k holds

F . k = a * v ) holds

Sum F = a * (Sum G)

let F, G be FinSequence of V; :: thesis: ( len F = len G & ( for k being Nat

for v being Element of V st k in dom F & v = G . k holds

F . k = a * v ) implies Sum F = a * (Sum G) )

defpred S_{1}[ Nat] means for H, I being FinSequence of V st len H = len I & len H = $1 & ( for k being Nat

for v being Element of V st k in dom H & v = I . k holds

H . k = a * v ) holds

Sum H = a * (Sum I);

A1: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[ 0 ]
_{1}[n]
from NAT_1:sch 2(A16, A1);

hence ( len F = len G & ( for k being Nat

for v being Element of V st k in dom F & v = G . k holds

F . k = a * v ) implies Sum F = a * (Sum G) ) ; :: thesis: verum

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over R

for F, G being FinSequence of V st len F = len G & ( for k being Nat

for v being Element of V st k in dom F & v = G . k holds

F . k = a * v ) holds

Sum F = a * (Sum G)

let a be Element of R; :: thesis: for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over R

for F, G being FinSequence of V st len F = len G & ( for k being Nat

for v being Element of V st k in dom F & v = G . k holds

F . k = a * v ) holds

Sum F = a * (Sum G)

let V be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over R; :: thesis: for F, G being FinSequence of V st len F = len G & ( for k being Nat

for v being Element of V st k in dom F & v = G . k holds

F . k = a * v ) holds

Sum F = a * (Sum G)

let F, G be FinSequence of V; :: thesis: ( len F = len G & ( for k being Nat

for v being Element of V st k in dom F & v = G . k holds

F . k = a * v ) implies Sum F = a * (Sum G) )

defpred S

for v being Element of V st k in dom H & v = I . k holds

H . k = a * v ) holds

Sum H = a * (Sum I);

A1: for n being Nat st S

S

proof

A16:
S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A2: for H, I being FinSequence of V st len H = len I & len H = n & ( for k being Nat

for v being Element of V st k in dom H & v = I . k holds

H . k = a * v ) holds

Sum H = a * (Sum I) ; :: thesis: S_{1}[n + 1]

let H, I be FinSequence of V; :: thesis: ( len H = len I & len H = n + 1 & ( for k being Nat

for v being Element of V st k in dom H & v = I . k holds

H . k = a * v ) implies Sum H = a * (Sum I) )

assume that

A3: len H = len I and

A4: len H = n + 1 and

A5: for k being Nat

for v being Element of V st k in dom H & v = I . k holds

H . k = a * v ; :: thesis: Sum H = a * (Sum I)

reconsider p = H | (Seg n), q = I | (Seg n) as FinSequence of V by FINSEQ_1:18;

A6: n <= n + 1 by NAT_1:12;

then A7: q = I | (dom q) by A3, A4, FINSEQ_1:17;

A8: len p = n by A4, A6, FINSEQ_1:17;

A9: len q = n by A3, A4, A6, FINSEQ_1:17;

then A14: n + 1 in dom H by A4, FINSEQ_1:def 3;

dom H = dom I by A3, FINSEQ_3:29;

then reconsider v1 = H . (n + 1), v2 = I . (n + 1) as Element of V by A14, FINSEQ_2:11;

A15: v1 = a * v2 by A5, A14;

p = H | (dom p) by A4, A6, FINSEQ_1:17;

hence Sum H = (Sum p) + v1 by A4, A8, RLVECT_1:38

.= (a * (Sum q)) + (a * v2) by A2, A8, A9, A10, A15

.= a * ((Sum q) + v2) by VECTSP_1:def 14

.= a * (Sum I) by A3, A4, A9, A7, RLVECT_1:38 ;

:: thesis: verum

end;assume A2: for H, I being FinSequence of V st len H = len I & len H = n & ( for k being Nat

for v being Element of V st k in dom H & v = I . k holds

H . k = a * v ) holds

Sum H = a * (Sum I) ; :: thesis: S

let H, I be FinSequence of V; :: thesis: ( len H = len I & len H = n + 1 & ( for k being Nat

for v being Element of V st k in dom H & v = I . k holds

H . k = a * v ) implies Sum H = a * (Sum I) )

assume that

A3: len H = len I and

A4: len H = n + 1 and

A5: for k being Nat

for v being Element of V st k in dom H & v = I . k holds

H . k = a * v ; :: thesis: Sum H = a * (Sum I)

reconsider p = H | (Seg n), q = I | (Seg n) as FinSequence of V by FINSEQ_1:18;

A6: n <= n + 1 by NAT_1:12;

then A7: q = I | (dom q) by A3, A4, FINSEQ_1:17;

A8: len p = n by A4, A6, FINSEQ_1:17;

A9: len q = n by A3, A4, A6, FINSEQ_1:17;

A10: now :: thesis: for k being Nat

for v being Element of V st k in dom p & v = q . k holds

p . k = a * v

n + 1 in Seg (n + 1)
by FINSEQ_1:4;for v being Element of V st k in dom p & v = q . k holds

p . k = a * v

A11:
dom p c= dom H
by A4, A6, A8, FINSEQ_3:30;

let k be Nat; :: thesis: for v being Element of V st k in dom p & v = q . k holds

p . k = a * v

let v be Element of V; :: thesis: ( k in dom p & v = q . k implies p . k = a * v )

assume that

A12: k in dom p and

A13: v = q . k ; :: thesis: p . k = a * v

dom q = dom p by A8, A9, FINSEQ_3:29;

then I . k = q . k by A12, FUNCT_1:47;

then H . k = a * v by A5, A12, A13, A11;

hence p . k = a * v by A12, FUNCT_1:47; :: thesis: verum

end;let k be Nat; :: thesis: for v being Element of V st k in dom p & v = q . k holds

p . k = a * v

let v be Element of V; :: thesis: ( k in dom p & v = q . k implies p . k = a * v )

assume that

A12: k in dom p and

A13: v = q . k ; :: thesis: p . k = a * v

dom q = dom p by A8, A9, FINSEQ_3:29;

then I . k = q . k by A12, FUNCT_1:47;

then H . k = a * v by A5, A12, A13, A11;

hence p . k = a * v by A12, FUNCT_1:47; :: thesis: verum

then A14: n + 1 in dom H by A4, FINSEQ_1:def 3;

dom H = dom I by A3, FINSEQ_3:29;

then reconsider v1 = H . (n + 1), v2 = I . (n + 1) as Element of V by A14, FINSEQ_2:11;

A15: v1 = a * v2 by A5, A14;

p = H | (dom p) by A4, A6, FINSEQ_1:17;

hence Sum H = (Sum p) + v1 by A4, A8, RLVECT_1:38

.= (a * (Sum q)) + (a * v2) by A2, A8, A9, A10, A15

.= a * ((Sum q) + v2) by VECTSP_1:def 14

.= a * (Sum I) by A3, A4, A9, A7, RLVECT_1:38 ;

:: thesis: verum

proof

for n being Nat holds S
let H, I be FinSequence of V; :: thesis: ( len H = len I & len H = 0 & ( for k being Nat

for v being Element of V st k in dom H & v = I . k holds

H . k = a * v ) implies Sum H = a * (Sum I) )

assume that

A17: len H = len I and

A18: len H = 0 and

for k being Nat

for v being Element of V st k in dom H & v = I . k holds

H . k = a * v ; :: thesis: Sum H = a * (Sum I)

H = <*> the carrier of V by A18;

then A19: Sum H = 0. V by RLVECT_1:43;

I = <*> the carrier of V by A17, A18;

then Sum I = 0. V by RLVECT_1:43;

hence Sum H = a * (Sum I) by A19, VECTSP_1:14; :: thesis: verum

end;for v being Element of V st k in dom H & v = I . k holds

H . k = a * v ) implies Sum H = a * (Sum I) )

assume that

A17: len H = len I and

A18: len H = 0 and

for k being Nat

for v being Element of V st k in dom H & v = I . k holds

H . k = a * v ; :: thesis: Sum H = a * (Sum I)

H = <*> the carrier of V by A18;

then A19: Sum H = 0. V by RLVECT_1:43;

I = <*> the carrier of V by A17, A18;

then Sum I = 0. V by RLVECT_1:43;

hence Sum H = a * (Sum I) by A19, VECTSP_1:14; :: thesis: verum

hence ( len F = len G & ( for k being Nat

for v being Element of V st k in dom F & v = G . k holds

F . k = a * v ) implies Sum F = a * (Sum G) ) ; :: thesis: verum