let f be heterogeneous non empty real-valued positive FinSequence; :: thesis: for i, j being object st i in MeanLess f & j in MeanMore f holds
( i in dom f & j in dom f & i <> j & f . i < Mean f & f . j > Mean f )
let i, j be object ; :: thesis: ( i in MeanLess f & j in MeanMore f implies ( i in dom f & j in dom f & i <> j & f . i < Mean f & f . j > Mean f ) )
assume A1: ( i in MeanLess f & j in MeanMore f ) ; :: thesis: ( i in dom f & j in dom f & i <> j & f . i < Mean f & f . j > Mean f )
then consider ii being Nat such that
A2: ( ii = i & ii in dom f & f . ii < Mean f ) ;
consider jj being Nat such that
A3: ( jj = j & jj in dom f & f . jj > Mean f ) by A1;
thus ( i in dom f & j in dom f & i <> j & f . i < Mean f & f . j > Mean f ) by A2, A3; :: thesis: verum