let p be Prime; :: thesis: for V being free Z_Module
for i being Integer
for v being Element of V holds ZMtoMQV (V,p,((i mod p) * v)) = ZMtoMQV (V,p,(i * v))
let V be free Z_Module; :: thesis: for i being Integer
for v being Element of V holds ZMtoMQV (V,p,((i mod p) * v)) = ZMtoMQV (V,p,(i * v))
let i be Integer; :: thesis: for v being Element of V holds ZMtoMQV (V,p,((i mod p) * v)) = ZMtoMQV (V,p,(i * v))
let v be Element of V; :: thesis: ZMtoMQV (V,p,((i mod p) * v)) = ZMtoMQV (V,p,(i * v))
i is Element of INT by INT_1:def 2;
then reconsider a = i mod p as Element of (GF p) by Lm3;
reconsider t1 = ZMtoMQV (V,p,v) as Element of (Z_ModuleQuot (V,(p (*) V))) ;
ZMtoMQV (V,p,v) = v + (p (*) V) ;
then A1: v + (p (*) V) is Element of CosetSet (V,(p (*) V)) by ZMODUL02:def 10;
thus ZMtoMQV (V,p,((i mod p) * v)) = a * (ZMtoMQV (V,p,v)) by Th30
.= (i mod p) * t1 by ZMODUL02:def 11
.= i * t1 by ZMODUL02:2
.= (lmultCoset (V,(p (*) V))) . (i,(v + (p (*) V))) by ZMODUL02:def 10
.= ZMtoMQV (V,p,(i * v)) by A1, ZMODUL02:def 9 ; :: thesis: verum