theorem HetMono: :: RVSUM_3:32

for f being real-valued FinSequence
for i, j being Nat st i in dom f & j in dom f & i <> j & f . i <> Mean f & f . j <> Mean f holds
Het f > Het (Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))))