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 Integer, v being VECTOR of V such that
A2: ( a * v = 0. V & a <> 0 & v <> 0. V ) by A1;
( the Basis of V is linearly-independent & Lin the Basis of V = Z_ModuleStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) ) by Def2;
then consider lv being Z_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 Z_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, Def2, ZMODUL02:def 36; :: thesis: verum