set W = a (*) V;
for x being Vector of (VectQuot (V,(a (*) V))) holds x is torsion

proof

let x be Vector of (VectQuot (V,(a (*) V))); :: thesis: x is torsion
a <> 0. INT.Ring ;
then a <> 0 ;
then a * x = (a mod a) * x by ZMODUL02:2
.= 0. (VectQuot (V,(a (*) V))) by INT_1:50, ZMODUL01:1 ;
hence x is torsion ; :: thesis: verum

end;

hence VectQuot (V,(a (*) V)) is torsion ; :: thesis: verum