for f being heterogeneous non empty real-valued positive FinSequence
for i, j being Nat st i in dom f & j in dom f & i <> j & i in MeanMore f & j in MeanLess f holds
ex g being non empty real-valued positive FinSequence st
( g = Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) & GMean f < GMean g )