let f be real-valued FinSequence; :: thesis: 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
let i, j be Nat; :: thesis: ( i in dom f & j in dom f & i <> j implies f, Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) are_gamma-equivalent )
set a = Mean f;
set b = ((f . i) + (f . j)) - (Mean f);
assume A1: ( i in dom f & j in dom f & i <> j ) ; :: thesis: f, Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) are_gamma-equivalent
A2: dom f = dom (Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f)))) by DinoDom;
Sum (Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f)))) = ((((Sum f) - (f . i)) - (f . j)) + (Mean f)) + (((f . i) + (f . j)) - (Mean f)) by SumReplace, A1
.= Sum f ;
hence f, Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) are_gamma-equivalent by FINSEQ_3:29, A2; :: thesis: verum