let p be prime Element of INT.Ring; :: thesis: 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))
let V be free Z_Module; :: thesis: for s, t being Element of V holds (ZMtoMQV (V,p,s)) + (ZMtoMQV (V,p,t)) = ZMtoMQV (V,p,(s + t))
let s, t be Element of V; :: thesis: (ZMtoMQV (V,p,s)) + (ZMtoMQV (V,p,t)) = ZMtoMQV (V,p,(s + t))
set s1 = ZMtoMQV (V,p,s);
set t1 = ZMtoMQV (V,p,t);
A1: ZMtoMQV (V,p,s) = s + (p (*) V) ;
A2: ZMtoMQV (V,p,t) = t + (p (*) V) ;
A3: s + (p (*) V) is Element of CosetSet (V,(p (*) V)) by A1, VECTSP10:def 6;
A4: t + (p (*) V) is Element of CosetSet (V,(p (*) V)) by A2, VECTSP10:def 6;
thus (ZMtoMQV (V,p,s)) + (ZMtoMQV (V,p,t)) = (addCoset (V,(p (*) V))) . ((s + (p (*) V)),(t + (p (*) V))) by VECTSP10:def 6
.= ZMtoMQV (V,p,(s + t)) by A3, A4, VECTSP10:def 3 ; :: thesis: verum