theorem Th11: :: NORMSP_4:10

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