:: deftheorem defDivisibleModule defines divisible ZMODUL08:def 2 :
for V being Z_Module holds
( V is divisible iff for v being Vector of V holds v is divisible );