theorem ReplacePositive2: :: RVSUM_3:36

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 & f . j > Mean f holds
Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) is positive