:: deftheorem defines = RMOD_4:def 8 :
for R being Ring
for V being RightMod of R
for L1, L2 being Linear_Combination of V holds
( L1 = L2 iff for v being Vector of V holds L1 . v = L2 . v );