theorem Th2: :: BHSP_6:2

for X being RealUnitarySpace st the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity holds

for Y1, Y2 being finite Subset of X st Y1 misses Y2 holds

for Z being finite Subset of X st Z = Y1 \/ Y2 holds

setsum Z = (setsum Y1) + (setsum Y2)

for Y1, Y2 being finite Subset of X st Y1 misses Y2 holds

for Z being finite Subset of X st Z = Y1 \/ Y2 holds

setsum Z = (setsum Y1) + (setsum Y2)