for K being Field
for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for v being Element of V1 holds v = Sum (lmlt ((v |-- b1),b1))