theorem :: MATRLIN2:16

for i being Nat
for K being Field
for V1 being finite-dimensional VectSp of K
for R being FinSequence of V1 st i in dom R holds
Sum (lmlt ((Line ((1. (K,(len R))),i)),R)) = R /. i