theorem Th30: :: ZMODUL03:30

for p being prime Element of INT.Ring
for V being free Z_Module
for s being Element of V
for a being Element of INT.Ring
for b being Element of (GF p) st a = b holds
b * (ZMtoMQV (V,p,s)) = ZMtoMQV (V,p,(a * s))