theorem :: RVSUM_3:37

for f being heterogeneous non empty real-valued positive FinSequence ex i, j being Nat st
( i in dom f & j in dom f & i <> j & 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 ) )