theorem :: ZMODUL02:67

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