theorem :: LMOD_7:7

for K being Ring
for V being LeftMod of K holds
( SubJoin V is commutative & SubJoin V is associative & SubJoin V is having_a_unity & (0). V = the_unity_wrt (SubJoin V) )