let f be heterogeneous real-valued FinSequence; :: thesis: MeanMore 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 MeanMore f or x in MeanLess f ) by XBOOLE_0:def 3;

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

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

end;

suppose x in MeanLess f ; :: thesis: MeanMore 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
G0: len R1 = len f by CARD_1:def 7;
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, g0, CARD_1:def 7;
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 A2, FINSEQ_2:57, CARD_1:def 7; :: thesis: verum

end;

then Sum R1 > Sum f by Th83, G1, G0;
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 MeanMore f by B1;
hence MeanMore f <> {} ; :: thesis: verum

end;

end;