let f be non empty real-valued FinSequence; :: thesis: ( Het f <> 0 implies f is heterogeneous )
assume A1: Het f <> 0 ; :: thesis: f is heterogeneous
assume A3: f is homogeneous ; :: thesis: contradiction
then the_value_of f = Mean f by ConstantMean;
then consider x being set such that
A2: ( x in dom f & Mean f = f . x ) by FUNCT_1:def 12, A3;
HetSet f <> {} by A1;
then consider y being object such that
A5: y in HetSet f by XBOOLE_0:def 1;
consider z being Nat such that
A6: ( z = y & z in dom f & f . z <> Mean f ) by A5;
thus contradiction by A3, A2, A6; :: thesis: verum