theorem ReplaceGamma: :: RVSUM_3:28

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