let V be Z_Module; :: thesis: 0. V is torsion
(1. INT.Ring) * (0. V) = 0. V by ZMODUL01:1;
hence 0. V is torsion ; :: thesis: verum