theorem LMEQRZM1: :: ZMODUL04:5

for V being Z_Module
for v being Element of ModuleStr(# (Class (EQRZM V)),(addCoset V),(zeroCoset V),(lmultCoset V) #) st V is Mult-cancelable holds
ex i being Element of INT.Ring ex z being Element of V st
( i <> 0. INT.Ring & v = Class ((EQRZM V),[z,i]) )