let V be Z_Module; :: thesis: 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]) )
let v be Element of ModuleStr(# (Class (EQRZM V)),(addCoset V),(zeroCoset V),(lmultCoset V) #); :: thesis: ( V is Mult-cancelable implies ex i being Element of INT.Ring ex z being Element of V st
( i <> 0. INT.Ring & v = Class ((EQRZM V),[z,i]) ) )
assume V is Mult-cancelable ; :: thesis: ex i being Element of INT.Ring ex z being Element of V st
( i <> 0. INT.Ring & v = Class ((EQRZM V),[z,i]) )
v in Class (EQRZM V) ;
then consider A1 being object such that
A1: ( A1 in [: the carrier of V,(INT \ {0}):] & v = Class ((EQRZM V),A1) ) by EQREL_1:def 3;
consider z, i being object such that
A2: ( z in the carrier of V & i in INT \ {0} & A1 = [z,i] ) by A1, ZFMISC_1:def 2;
reconsider z = z as Element of V by A2;
A31: ( i in INT & not i in {0} ) by XBOOLE_0:def 5, A2;
reconsider i = i as Integer by A2;
reconsider i = i as Element of INT.Ring by A2;
take i ; :: thesis: ex z being Element of V st
( i <> 0. INT.Ring & v = Class ((EQRZM V),[z,i]) )
take z ; :: thesis: ( i <> 0. INT.Ring & v = Class ((EQRZM V),[z,i]) )
thus ( i <> 0. INT.Ring & v = Class ((EQRZM V),[z,i]) ) by A1, A2, A31, TARSKI:def 1; :: thesis: verum