for K being Ring
for V being LeftMod of K
for A being Subset of V st K is trivial holds
( ( for l being Linear_Combination of A holds Carrier l = {} ) & Lin A is trivial )