let f be heterogeneous non empty real-valued positive FinSequence; :: thesis: ex i, j being Nat st
( i in dom f & j in dom f & i <> j & 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 ) )
consider j, i being Nat such that
A1: ( j in dom f & i in dom f & j <> i & f . j < Mean f & Mean f < f . i ) by ExDiff;
take i ; :: thesis: ex j being Nat st
( i in dom f & j in dom f & i <> j & 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 ) )
take j ; :: thesis: ( i in dom f & j in dom f & i <> j & 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 ) )
thus ( i in dom f & j in dom f & i <> j ) by A1; :: 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;
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,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 ReplacePositive, A1;
take g ; :: thesis: ( g = Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) & GMean f < GMean g )
( f . i > (Mean f) + 0 & Mean f > (f . j) + 0 ) by A1;
then ( (f . i) - (Mean f) > 0 & (Mean f) - (f . j) > 0 ) by XREAL_1:20;
then ((f . i) - (Mean f)) * ((Mean f) - (f . j)) > 0 ;
then ((a * b) - ((f . i) * (f . j))) + ((f . i) * (f . j)) > 0 + ((f . i) * (f . j)) by XREAL_1:8;
then (a * b) / ((f . i) * (f . j)) > 1 by 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