let V be free Z_Module; :: thesis: V is Mult-cancelable

set I = the Basis of V;

assume A1: not V is Mult-cancelable ; :: thesis: contradiction

consider a being Element of INT.Ring, v being Vector of V such that

A2: ( a * v = 0. V & a <> 0. INT.Ring & v <> 0. V ) by A1;

the Basis of V is base ;

then ( the Basis of V is linearly-independent & Lin the Basis of V = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) ) ;

then consider lv being Linear_Combination of the Basis of V such that

A3: v = Sum lv by STRUCT_0:def 5, ZMODUL02:64;

Carrier lv <> {} by A2, A3, ZMODUL02:23;

then A4: Carrier (a * lv) <> {} by A2, ZMODUL02:29;

A5: a * lv is Linear_Combination of the Basis of V by ZMODUL02:31;

Sum (a * lv) = 0. V by A2, A3, ZMODUL02:53;

hence contradiction by A4, A5, VECTSP_7:def 3, VECTSP_7:def 1; :: thesis: verum

set I = the Basis of V;

assume A1: not V is Mult-cancelable ; :: thesis: contradiction

consider a being Element of INT.Ring, v being Vector of V such that

A2: ( a * v = 0. V & a <> 0. INT.Ring & v <> 0. V ) by A1;

the Basis of V is base ;

then ( the Basis of V is linearly-independent & Lin the Basis of V = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) ) ;

then consider lv being Linear_Combination of the Basis of V such that

A3: v = Sum lv by STRUCT_0:def 5, ZMODUL02:64;

Carrier lv <> {} by A2, A3, ZMODUL02:23;

then A4: Carrier (a * lv) <> {} by A2, ZMODUL02:29;

A5: a * lv is Linear_Combination of the Basis of V by ZMODUL02:31;

Sum (a * lv) = 0. V by A2, A3, ZMODUL02:53;

hence contradiction by A4, A5, VECTSP_7:def 3, VECTSP_7:def 1; :: thesis: verum