for GF being Ring
for V being LeftMod of GF holds Lin ({} the carrier of V) = (0). V