let f be heterogeneous non empty real-valued positive FinSequence; :: thesis: for i, j being Nat st i in dom f & j in dom f & i <> j & f . i > Mean f holds
Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) is positive
let i, j be Nat; :: thesis: ( i in dom f & j in dom f & i <> j & f . i > Mean f implies Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) is positive )
assume A1: ( i in dom f & j in dom f & i <> j & f . i > Mean f ) ; :: thesis: Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) is positive
set a = Mean f;
set b = ((f . i) + (f . j)) - (Mean f);
h2: (Mean f) - (Mean f) < (f . i) - (Mean f) by A1, XREAL_1:14;
f . j > 0 by A1, PosDef;
then ((f . i) - (Mean f)) + (f . j) > 0 by h2;
then reconsider b = ((f . i) + (f . j)) - (Mean f) as positive Real ;
set g = Replace (f,i,j,(Mean f),b);
for n being Nat st n in dom (Replace (f,i,j,(Mean f),b)) holds
(Replace (f,i,j,(Mean f),b)) . n > 0

proof

let n be Nat; :: thesis: ( n in dom (Replace (f,i,j,(Mean f),b)) implies (Replace (f,i,j,(Mean f),b)) . n > 0 )
assume n in dom (Replace (f,i,j,(Mean f),b)) ; :: thesis: (Replace (f,i,j,(Mean f),b)) . n > 0
then A2: n in dom f by DinoDom;

per cases ( n = i or n = j or ( n <> i & n <> j ) ) ;

suppose n = i ; :: thesis: (Replace (f,i,j,(Mean f),b)) . n > 0

hence (Replace (f,i,j,(Mean f),b)) . n > 0 by ReplaceValue3, A1; :: thesis: verum

end;

suppose n = j ; :: thesis: (Replace (f,i,j,(Mean f),b)) . n > 0

hence (Replace (f,i,j,(Mean f),b)) . n > 0 by ReplaceValue2, A1; :: thesis: verum

end;

suppose ( n <> i & n <> j ) ; :: thesis: (Replace (f,i,j,(Mean f),b)) . n > 0

then (Replace (f,i,j,(Mean f),b)) . n = f . n by A2, ReplaceValue, A1;
hence (Replace (f,i,j,(Mean f),b)) . n > 0 by PosDef, A2; :: thesis: verum

end;

end;

end;

hence Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) is positive ; :: thesis: verum