let p be Prime; :: thesis: for V being free Z_Module
for s being Element of V
for a being Integer
for b being Element of (GF p) st a = b holds
b * (ZMtoMQV (V,p,s)) = ZMtoMQV (V,p,(a * s))
let V be free Z_Module; :: thesis: for s being Element of V
for a being Integer
for b being Element of (GF p) st a = b holds
b * (ZMtoMQV (V,p,s)) = ZMtoMQV (V,p,(a * s))
let s be Element of V; :: thesis: for a being Integer
for b being Element of (GF p) st a = b holds
b * (ZMtoMQV (V,p,s)) = ZMtoMQV (V,p,(a * s))
let a be Integer; :: thesis: for b being Element of (GF p) st a = b holds
b * (ZMtoMQV (V,p,s)) = ZMtoMQV (V,p,(a * s))
let b be Element of (GF p); :: thesis: ( a = b implies b * (ZMtoMQV (V,p,s)) = ZMtoMQV (V,p,(a * s)) )
set t = ZMtoMQV (V,p,s);
assume A1: a = b ; :: thesis: b * (ZMtoMQV (V,p,s)) = ZMtoMQV (V,p,(a * s))
A2: ZMtoMQV (V,p,s) = s + (p (*) V) ;
reconsider t1 = ZMtoMQV (V,p,s) as Element of (Z_ModuleQuot (V,(p (*) V))) ;
A3: s + (p (*) V) is Element of CosetSet (V,(p (*) V)) by A2, ZMODUL02:def 10;
reconsider i = b as Nat ;
A4: b = i mod p by NAT_1:44, NAT_D:24;
reconsider i = i as Integer ;
thus b * (ZMtoMQV (V,p,s)) = (i mod p) * t1 by A4, ZMODUL02:def 11
.= (lmultCoset (V,(p (*) V))) . ((i mod p),(s + (p (*) V))) by ZMODUL02:def 10
.= ZMtoMQV (V,p,(a * s)) by A1, A4, A3, ZMODUL02:def 9 ; :: thesis: verum