let f be heterogeneous non empty real-valued FinSequence; :: thesis: for i, j being Nat st i = the Element of MeanLess f & j = the Element of 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 Nat; :: thesis: ( i = the Element of MeanLess f & j = the Element of MeanMore f implies ( i in dom f & j in dom f & i <> j & f . i < Mean f & f . j > Mean f ) )
assume A1: ( i = the Element of MeanLess f & j = the Element of MeanMore f ) ; :: thesis: ( i in dom f & j in dom f & i <> j & f . i < Mean f & f . j > Mean f )
i in MeanLess f by A1;
then consider ii being Nat such that
A2: ( ii = i & ii in dom f & f . ii < Mean f ) ;
j in MeanMore f by A1;
then consider jj being Nat such that
A3: ( 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 & f . j > Mean f ) by A2, A3; :: thesis: verum