let p be prime Element of INT.Ring; :: thesis: 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))

let V be Z_Module; :: thesis: 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))

let s be Element of V; :: thesis: 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))

let a be Element of INT.Ring; :: thesis: for b being Element of (GF p) st b = a mod p holds

b * (ZMtoMQV (V,p,s)) = ZMtoMQV (V,p,(a * s))

let b be Element of (GF p); :: thesis: ( b = a mod p implies b * (ZMtoMQV (V,p,s)) = ZMtoMQV (V,p,(a * s)) )

assume A1: b = a mod p ; :: thesis: b * (ZMtoMQV (V,p,s)) = ZMtoMQV (V,p,(a * s))

A2: ZMtoMQV (V,p,s) = s + (p (*) V) ;

set t = ZMtoMQV (V,p,s);

reconsider t1 = ZMtoMQV (V,p,s) as Element of (VectQuot (V,(p (*) V))) ;

A3: s + (p (*) V) is Element of CosetSet (V,(p (*) V)) by A2, VECTSP10:def 6;

reconsider i = b as Nat ;

thus b * (ZMtoMQV (V,p,s)) = (a mod p) * t1 by A1, ZMODUL02:def 11

.= a * t1 by ZMODUL02:2

.= (lmultCoset (V,(p (*) V))) . (a,(s + (p (*) V))) by VECTSP10:def 6

.= ZMtoMQV (V,p,(a * s)) by A3, VECTSP10:def 5 ; :: thesis: verum

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))

let V be Z_Module; :: thesis: 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))

let s be Element of V; :: thesis: 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))

let a be Element of INT.Ring; :: thesis: for b being Element of (GF p) st b = a mod p holds

b * (ZMtoMQV (V,p,s)) = ZMtoMQV (V,p,(a * s))

let b be Element of (GF p); :: thesis: ( b = a mod p implies b * (ZMtoMQV (V,p,s)) = ZMtoMQV (V,p,(a * s)) )

assume A1: b = a mod p ; :: thesis: b * (ZMtoMQV (V,p,s)) = ZMtoMQV (V,p,(a * s))

A2: ZMtoMQV (V,p,s) = s + (p (*) V) ;

set t = ZMtoMQV (V,p,s);

reconsider t1 = ZMtoMQV (V,p,s) as Element of (VectQuot (V,(p (*) V))) ;

A3: s + (p (*) V) is Element of CosetSet (V,(p (*) V)) by A2, VECTSP10:def 6;

reconsider i = b as Nat ;

thus b * (ZMtoMQV (V,p,s)) = (a mod p) * t1 by A1, ZMODUL02:def 11

.= a * t1 by ZMODUL02:2

.= (lmultCoset (V,(p (*) V))) . (a,(s + (p (*) V))) by VECTSP10:def 6

.= ZMtoMQV (V,p,(a * s)) by A3, VECTSP10:def 5 ; :: thesis: verum