let V be Z_Module; :: thesis: VectQuot (V,(torsion_part V)) is torsion-free
set W = torsion_part V;
set ZQ = VectQuot (V,(torsion_part V));
for v being Vector of (VectQuot (V,(torsion_part V))) st v <> 0. (VectQuot (V,(torsion_part V))) holds
not v is torsion

proof

let v be Vector of (VectQuot (V,(torsion_part V))); :: thesis: ( v <> 0. (VectQuot (V,(torsion_part V))) implies not v is torsion )
assume AS: v <> 0. (VectQuot (V,(torsion_part V))) ; :: thesis: not v is torsion
assume v is torsion ; :: thesis: contradiction
then consider i being Element of INT.Ring such that
P1: ( i <> 0 & i * v = 0. (VectQuot (V,(torsion_part V))) ) ;
P3: v is Element of CosetSet (V,(torsion_part V)) by VECTSP10:def 6;
then v in CosetSet (V,(torsion_part V)) ;
then ex A being Coset of torsion_part V st v = A ;
then consider a being VECTOR of V such that
A3: v = a + (torsion_part V) by VECTSP_4:def 6;
A4: i * v = (lmultCoset (V,(torsion_part V))) . (i,v) by VECTSP10:def 6
.= (i * a) + (torsion_part V) by VECTSP10:def 5, A3, P3 ;
i * v = zeroCoset (V,(torsion_part V)) by P1, VECTSP10:def 6
.= the carrier of (torsion_part V) ;
then i * a in torsion_part V by ZMODUL01:63, A4;
then i * a in { v where v is VECTOR of V : v is torsion } by defTorsionPart;
then ex w being VECTOR of V st
( i * a = w & w is torsion ) ;
then consider j being Element of INT.Ring such that
A5: ( j <> 0 & j * (i * a) = 0. V ) ;
(j * i) * a = 0. V by A5, VECTSP_1:def 16;
then a is torsion by A5, P1;
then a in { v where v is VECTOR of V : v is torsion } ;
then a in torsion_part V by defTorsionPart;
then v = zeroCoset (V,(torsion_part V)) by A3, ZMODUL01:63;
hence contradiction by AS, VECTSP10:def 6; :: thesis: verum

end;

hence VectQuot (V,(torsion_part V)) is torsion-free ; :: thesis: verum