theorem :: RMOD_4:8

for R being Ring
for V being RightMod of R
for v1, v2, v3 being Vector of V st v1 <> v2 & v2 <> v3 & v1 <> v3 holds
Sum {v1,v2,v3} = (v1 + v2) + v3