theorem PROJ4: :: ZMATRLIN:57
for V being free Z_Module
for B being Basis of V
for u being Vector of V holds (Coordinate (u,B)) . (0. V) = 0