theorem Th26: :: MEASURE9:28

for p being FinSequence of ExtREAL st not -infty in rng p holds
SumAll <*p*> = SumAll (<*p*> @)