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 . j > 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 . j > 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 . j > 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 . j) - (Mean f) by XREAL_1:14, A1;
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,(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