set V = Rat-Module ;
for v being VECTOR of Rat-Module st v <> 0. Rat-Module holds
not v is torsion

proof

let v be VECTOR of Rat-Module; :: thesis: ( v <> 0. Rat-Module implies not v is torsion )
assume AS: v <> 0. Rat-Module ; :: thesis: not v is torsion
assume v is torsion ; :: thesis: contradiction
then consider i being Element of INT.Ring such that
P1: ( i <> 0. INT.Ring & i * v = 0. Rat-Module ) ;
reconsider v1 = v as Rational ;
i * v1 = 0 by LMTFRat2, P1;
hence contradiction by AS, P1; :: thesis: verum

end;

hence Rat-Module is torsion-free ; :: thesis: verum