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

proof

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

end;

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