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 st k in dom F holds

G . k = a * (F /. k) ) holds

Sum G = a * (Sum F)

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 st k in dom F holds

G . k = a * (F /. k) ) holds

Sum G = a * (Sum F)

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 st k in dom F holds

G . k = a * (F /. k) ) holds

Sum G = a * (Sum F)

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

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

assume that

A1: len F = len G and

A2: for k being Nat st k in dom F holds

G . k = a * (F /. k) ; :: thesis: Sum G = a * (Sum F)

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 st k in dom F holds

G . k = a * (F /. k) ) holds

Sum G = a * (Sum F)

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 st k in dom F holds

G . k = a * (F /. k) ) holds

Sum G = a * (Sum F)

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 st k in dom F holds

G . k = a * (F /. k) ) holds

Sum G = a * (Sum F)

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

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

assume that

A1: len F = len G and

A2: for k being Nat st k in dom F holds

G . k = a * (F /. k) ; :: thesis: Sum G = a * (Sum F)

now :: thesis: for k being Nat

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

G . k = a * v

hence
Sum G = a * (Sum F)
by A1, Th66; :: thesis: verumfor v being Element of V st k in dom G & v = F . k holds

G . k = a * v

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

G . k = a * v

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

assume that

A3: k in dom G and

A4: v = F . k ; :: thesis: G . k = a * v

A5: k in dom F by A1, A3, FINSEQ_3:29;

then v = F /. k by A4, PARTFUN1:def 6;

hence G . k = a * v by A2, A5; :: thesis: verum

end;G . k = a * v

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

assume that

A3: k in dom G and

A4: v = F . k ; :: thesis: G . k = a * v

A5: k in dom F by A1, A3, FINSEQ_3:29;

then v = F /. k by A4, PARTFUN1:def 6;

hence G . k = a * v by A2, A5; :: thesis: verum