set i = the Element of MeanLess f;
set j = the Element of MeanMore f;
reconsider i = the Element of MeanLess f, j = the Element of MeanMore f as Nat ;
Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) is real-valued FinSequence ;
hence ex b₁ being real-valued FinSequence ex i, j being Nat st
( i = the Element of MeanLess f & j = the Element of MeanMore f & b₁ = Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) ) ; :: thesis: verum