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