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 st k in dom F holds
G . k = (F /. k) * a ) holds
Sum G = (Sum F) * 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 st k in dom F holds
G . k = (F /. k) * a ) holds
Sum G = (Sum F) * a
let a be Scalar of 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 = (F /. k) * a ) holds
Sum G = (Sum F) * a
let F, G be FinSequence of V; :: thesis: ( len F = len G & ( for k being Nat st k in dom F holds
G . k = (F /. k) * a ) implies Sum G = (Sum F) * a )
assume that
A1: len F = len G and
A2: for k being Nat st k in dom F holds
G . k = (F /. k) * a ; :: thesis: Sum G = (Sum F) * a

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

let k be Nat; :: thesis: for v being Vector of V st k in dom G & v = F . k holds
G . k = v * a
let v be Vector of V; :: thesis: ( k in dom G & v = F . k implies G . k = v * a )
assume that
A3: k in dom G and
A4: v = F . k ; :: thesis: G . k = v * a
A5: k in dom F by A1, A3, FINSEQ_3:29;
then v = F /. k by A4, PARTFUN1:def 6;
hence G . k = v * a by A2, A5; :: thesis: verum

end;

hence Sum G = (Sum F) * a by A1, Th1; :: thesis: verum