theorem BlaBla2: :: RVSUM_3:39

for f being heterogeneous non empty real-valued positive FinSequence
for i, j being object st i in MeanLess f & j in MeanMore f holds
( i in dom f & j in dom f & i <> j & f . i < Mean f & f . j > Mean f )