let R be Ring; :: thesis: for a being Element of R
for V being LeftMod 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 = a * (F /. k) ) holds
Sum G = a * (Sum F)
let a be Element of R; :: thesis: for V being LeftMod 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 = a * (F /. k) ) holds
Sum G = a * (Sum F)
let V be LeftMod 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 = 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)
A3: ( dom F = Seg (len F) & dom G = Seg (len G) ) by FINSEQ_1:def 3;
now :: thesis: for k being Nat
for v being Vector of V st k in dom G & v = F . k holds
G . k = a * v
let k be Nat; :: thesis: for v being Vector of V st k in dom G & v = F . k holds
G . k = a * v
let v be Vector of V; :: thesis: ( k in dom G & v = F . k implies G . k = a * v )
assume that
A4: k in dom G and
A5: v = F . k ; :: thesis: G . k = a * v
v = F /. k by A1, A3, A4, A5, PARTFUN1:def 6;
hence G . k = a * v by A1, A2, A3, A4; :: thesis: verum
end;
hence Sum G = a * (Sum F) by A1, Th12; :: thesis: verum