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

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