theorem Th10: :: NORMSP_4:9

for X being RealLinearSpace
for A, B being Subset of X
for l1 being Linear_Combination of A
for l2 being Linear_Combination of B st rng l1 c= RAT & rng l2 c= RAT & A misses B holds
ex l being Linear_Combination of A \/ B st
( Carrier l = (Carrier l1) \/ (Carrier l2) & rng l c= RAT & Sum l = (Sum l1) + (Sum l2) )