set AG = INT.Ring ;
set G = ModuleStr(# the carrier of INT.Ring, the addF of INT.Ring, the ZeroF of INT.Ring,(Int-mult-left INT.Ring) #);
reconsider G = ModuleStr(# the carrier of INT.Ring, the addF of INT.Ring, the ZeroF of INT.Ring,(Int-mult-left INT.Ring) #) as Z_Module by ZMODUL01:164;
reconsider v = 1. INT.Ring as Vector of G ;
set One = 1. INT.Ring;
for i being Element of INT.Ring st i <> 0 holds
i * v <> 0. G
proof
assume ex i being Element of INT.Ring st
( i <> 0 & i * v = 0. G ) ; :: thesis: contradiction
then consider i being Element of INT.Ring such that
B1: ( i <> 0 & i * v = 0. G ) ;
i * v = the lmult of G . (i,v) by VECTSP_1:def 12
.= (Int-mult-left INT.Ring) . (i,v)
.= i * (1. INT.Ring) by LMINTRNG2
.= i ;
hence contradiction by B1; :: thesis: verum
end;
then not v is torsion ;
hence not for b1 being Z_Module holds b1 is torsion by defTorsionModule; :: thesis: verum