theorem Th26: :: ZMODUL03:26

for p being prime Element of INT.Ring
for V being free Z_Module
for I being Basis of V holds card { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } = card I