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 & j in MeanMore f & i in MeanLess f holds
ex g being non empty real-valued positive FinSequence st
( g = Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) & GMean f < GMean g )
let i, j be Nat; :: thesis: ( i in dom f & j in dom f & i <> j & j in MeanMore f & i in MeanLess f implies ex g being non empty real-valued positive FinSequence st
( g = Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) & GMean f < GMean g ) )
assume A1: ( i in dom f & j in dom f & i <> j & j in MeanMore f & i in MeanLess f ) ; :: thesis: ex g being non empty real-valued positive FinSequence st
( g = Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) & GMean f < GMean g )
reconsider a = Mean f as positive Real ;
b1: ( f . i > 0 & f . j > 0 ) by A1, PosDef;
h1: Mean f < f . j by A1, BlaBla2;
then h2: (Mean f) - (Mean f) < (f . j) - (Mean f) by XREAL_1:14;
f . i > 0 by A1, PosDef;
then ((f . j) - (Mean f)) + (f . i) > 0 by h2;
then reconsider b = ((f . i) + (f . j)) - (Mean f) as positive Real ;
set g = Replace (f,i,j,a,b);
jj: dom f = dom (Replace (f,i,j,a,b)) by DinoDom;
reconsider g = Replace (f,i,j,a,b) as non empty real-valued positive FinSequence by ReplacePositive2, A1, h1;
take g ; :: thesis: ( g = Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) & GMean f < GMean g )
( f . j > (Mean f) + 0 & Mean f > (f . i) + 0 ) by A1, BlaBla2;
then ( (f . j) - (Mean f) > 0 & (Mean f) - (f . i) > 0 ) by XREAL_1:20;
then ((f . j) - (Mean f)) * ((Mean f) - (f . i)) > 0 ;
then k2: ((a * b) - ((f . i) * (f . j))) + ((f . i) * (f . j)) > 0 + ((f . i) * (f . j)) by XREAL_1:8;
(a * b) / ((f . i) * (f . j)) > 1 by k2, XREAL_1:187, b1;
then (Product f) * ((a * b) / ((f . i) * (f . j))) > (Product f) * 1 by XREAL_1:68;
then ((Product f) * (a * b)) / ((f . i) * (f . j)) > Product f by XCMPLX_1:74;
then (((Product f) * a) * b) / ((f . i) * (f . j)) > Product f ;
then Product g > Product f by A1, ProdReplace;
hence ( g = Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) & GMean f < GMean g ) by ProdGMean, jj, FINSEQ_3:29; :: thesis: verum