let f be heterogeneous non empty real-valued FinSequence; :: thesis: MeanLess f misses MeanMore f
assume MeanLess f meets MeanMore f ; :: thesis: contradiction
then consider x being object such that
A1: ( x in MeanLess f & x in MeanMore f ) by XBOOLE_0:3;
consider i being Nat such that
A2: ( i = x & i in dom f & f . i < Mean f ) by A1;
consider j being Nat such that
A3: ( j = x & j in dom f & f . j > Mean f ) by A1;
thus contradiction by A2, A3; :: thesis: verum