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 & f . i < Mean f & Mean f < f . j )
take i = the Element of MeanLess f; :: thesis: ex j being Nat st
( i in dom f & j in dom f & i <> j & f . i < Mean f & Mean f < f . j )
take j = the Element of MeanMore f; :: thesis: ( i in dom f & j in dom f & i <> j & f . i < Mean f & Mean f < f . j )
i in MeanLess f ;
then consider ii being Nat such that
A1: ( ii = i & ii in dom f & f . ii < Mean f ) ;
j in MeanMore f ;
then consider jj being Nat such that
A2: ( jj = j & jj in dom f & f . jj > Mean f ) ;
thus ( i in dom f & j in dom f & i <> j & f . i < Mean f & Mean f < f . j ) by A1, A2; :: thesis: verum