theorem LMSUM1: :: ZMODLAT2:69

for K being Field
for n, i being Nat st i in Seg n holds
for s being FinSequence of (n -VectSp_over K) ex si being FinSequence of K st
( len si = len s & (Sum s) . i = Sum si & ( for k being Nat st k in dom si holds
si . k = (s /. k) . i ) )