let V be Z_Module; :: thesis: for v being Element of ModuleStr(# (Class ()),(),(),() #) 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 ((),[z,i]) )

let v be Element of ModuleStr(# (Class ()),(),(),() #); :: 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 ((),[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 ((),[z,i]) )

v in Class () ;
then consider A1 being object such that
A1: ( A1 in [: the carrier of V,():] & v = Class ((),A1) ) by EQREL_1:def 3;
consider z, i being object such that
A2: ( z in the carrier of V & i in INT \ & A1 = [z,i] ) by ;
reconsider z = z as Element of V by A2;
A31: ( i in INT & not i in ) by ;
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 ((),[z,i]) )

take z ; :: thesis: ( i <> 0. INT.Ring & v = Class ((),[z,i]) )
thus ( i <> 0. INT.Ring & v = Class ((),[z,i]) ) by ; :: thesis: verum