for p being prime Element of INT.Ring
for V being free Z_Module
for s, t being Element of V holds (ZMtoMQV (V,p,s)) + (ZMtoMQV (V,p,t)) = ZMtoMQV (V,p,(s + t))