assume AS: Z_ModuleQuot (V,(torsion_part V)) is trivial ; :: thesis: contradiction
consider v being VECTOR of V such that
P1: not v is torsion by ZMODUL06:def 2;
v + (torsion_part V) is Coset of torsion_part V by VECTSP_4:def 6;
then v + (torsion_part V) in CosetSet (V,(torsion_part V)) ;
then reconsider B = v + (torsion_part V) as Element of CosetSet (V,(torsion_part V)) ;
reconsider u = B as VECTOR of (Z_ModuleQuot (V,(torsion_part V))) by ZMODUL02:def 10;
u = 0. (Z_ModuleQuot (V,(torsion_part V))) by AS
.= zeroCoset (V,(torsion_part V)) by ZMODUL02:def 10
.= the carrier of (torsion_part V) ;
then v in torsion_part V by ZMODUL01:63;
then v in { v where v is VECTOR of V : v is torsion } by defTorsionPart;
then ex u being VECTOR of V st
( v = u & u is torsion ) ;
hence contradiction by P1; :: thesis: verum