for V being free Z_Module
for X being Basis of V
for v being Vector of V st v in X & v <> 0. V holds
(Coordinate (v,X)) . v = 1