assume AS: VectQuot (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 (VectQuot (V,(torsion_part V))) by VECTSP10:def 6;
u = 0. (VectQuot (V,(torsion_part V))) by AS
.= zeroCoset (V,(torsion_part V)) by VECTSP10:def 6
.= 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