theorem Th5: :: LMOD_6:5

for K being Ring
for V being LeftMod of K st K is trivial holds
( ( for r being Scalar of K holds r = 0. K ) & ( for a being Vector of V holds a = 0. V ) )