let f be heterogeneous real-valued FinSequence; :: thesis: MeanLess f <> {}
Het f <> {} by HetHomo;
then HetSet f <> {} ;
then consider x being object such that
A1: x in HetSet f by XBOOLE_0:7;
x in (MeanLess f) \/ (MeanMore f) by A1, MeanSum;

per cases then ( x in MeanLess f or x in MeanMore f ) by XBOOLE_0:def 3;

suppose x in MeanLess f ; :: thesis: MeanLess f <> {}

hence MeanLess f <> {} ; :: thesis: verum

end;

suppose x in MeanMore f ; :: thesis: MeanLess f <> {}

then consider n being Nat such that
A2: ( x = n & n in dom f & f . n > Mean f ) ;
reconsider R1 = (len f) |-> (Mean f) as real-valued FinSequence ;
set ff = f;
reconsider w = len R1 as Nat ;
ex i being Nat st
( i in dom f & f . i < Mean f )

proof

assume TT: for i being Nat st i in dom f holds
f . i >= Mean f ; :: thesis: contradiction
G1: for j being Nat st j in Seg w holds
R1 . j <= f . j

proof

let j be Nat; :: thesis: ( j in Seg w implies R1 . j <= f . j )
assume g0: j in Seg w ; :: thesis: R1 . j <= f . j
then G2: j in Seg (len f) by CARD_1:def 7;
G3: j in dom f by FINSEQ_1:def 3, CARD_1:def 7, g0;
R1 . j = Mean f by G2, FINSEQ_2:57;
hence R1 . j <= f . j by TT, G3; :: thesis: verum

end;

ex j being Nat st
( j in Seg w & R1 . j < f . j )

proof

take n ; :: thesis: ( n in Seg w & R1 . n < f . n )
n in Seg (len f) by A2, FINSEQ_1:def 3;
hence ( n in Seg w & R1 . n < f . n ) by CARD_1:def 7, A2, FINSEQ_2:57; :: thesis: verum

end;

then Sum R1 < Sum f by Th83, G1, CARD_1:def 7;
then Sum f > (len f) * (Mean f) by RVSUM_1:80;
hence contradiction by Huk1; :: thesis: verum

end;

then consider m being Nat such that
B1: ( m in dom f & f . m < Mean f ) ;
m in MeanLess f by B1;
hence MeanLess f <> {} ; :: thesis: verum

end;

end;