theorem Th12: :: NORMSP_4:11
for X being RealLinearSpace
for A, B being finite Subset of X st A misses B holds
(RAT_Sums A) + (RAT_Sums B) = RAT_Sums (A \/ B)