for V1 being free finite-rank Z_Module
for b1 being OrdBasis of V1
for v being Element of V1 holds v = Sum (lmlt ((v |-- b1),b1))