theorem lemBase: :: VECTSP13:26

for R being non degenerated commutative Ring
for n being Nat
for l being Linear_Combination of Base (R,n)
for v being Tuple of n, the carrier of R
for i being Nat st v = Sum l & 1 <= i & i <= n holds
v . i = l . (i _th_unit_vector (n,R))