let V be Z_Module; :: thesis: (0). V is torsion
for x being Vector of ((0). V) holds x is torsion

proof

let x be Vector of ((0). V); :: thesis: x is torsion
x in (0). V ;
then x = 0. V by ZMODUL02:66
.= 0. ((0). V) by ZMODUL01:26 ;
hence x is torsion ; :: thesis: verum

end;

hence (0). V is torsion ; :: thesis: verum