theorem MeanSum: :: RVSUM_3:19

for f being real-valued FinSequence holds HetSet f = (MeanLess f) \/ (MeanMore f)