theorem :: ZMODUL04:36

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