theorem ThCarrier1: :: ZMODUL04:25

for K being Ring
for V being VectSp of K
for A being Subset of V
for l1, l2 being Linear_Combination of A st (Carrier l1) /\ (Carrier l2) = {} holds
Carrier (l1 + l2) = (Carrier l1) \/ (Carrier l2)