theorem Th6: :: MOD_3:6

for R being Ring
for V being LeftMod of R holds Lin ({} the carrier of V) = (0). V by VECTSP_7:9;