for K being Ring
for V being LeftMod of K
for A, A1, A2 being Subset of V st A is base & A = A1 \/ A2 & A1 misses A2 holds
V is_the_direct_sum_of Lin A1, Lin A2