theorem Th21: :: ZMODUL03:21

for p being prime Element of INT.Ring
for V being free Z_Module
for I being Basis of V
for u1, u2 being Vector of V st u1 <> u2 & u1 in I & u2 in I holds
ZMtoMQV (V,p,u1) <> ZMtoMQV (V,p,u2)