let f be heterogeneous non empty real-valued positive FinSequence; :: thesis:
defpred S₁[ Nat] means ex g being non empty real-valued positive FinSequence st
( Het g = $1 & Mean f = Mean g & GMean g > GMean f & Het g < Het f );
B1: ex k being Nat st S₁[k]

reconsider g = Homogen f as non empty real-valued positive FinSequence ;
take k = Het g; :: thesis:
take g ; :: thesis:
g,f are_gamma-equivalent by HomEqui;
hence ( Het g = k & Mean f = Mean g & GMean g > GMean f & Het g < Het f ) by HomogenHet, HomGMean; :: thesis:

end;

B2: for k being Nat st k <> 0 & S₁[k] holds
ex n being Nat st
( n < k & S₁[n] )

let k be Nat; :: thesis:
assume Y1: ( k <> 0 & S₁[k] ) ; :: thesis:
then consider g being non empty real-valued positive FinSequence such that
Y2: ( Het g = k & Mean f = Mean g & GMean g > GMean f & Het g < Het f ) ;
reconsider g = g as heterogeneous non empty real-valued positive FinSequence by Y1, Y2, HetHetero;
reconsider h = Homogen g as non empty real-valued positive FinSequence ;
take n = Het h; :: thesis:
thus n < k by Y2, HomogenHet; :: thesis:
thus S₁[n] :: thesis:

ex g1 being non empty real-valued positive FinSequence st
( Het g1 = n & Mean f = Mean g1 & GMean g1 > GMean f & Het g1 < Het f )

take h ; :: thesis:
h,g are_gamma-equivalent by HomEqui;
hence ( Het h = n & Mean f = Mean h & GMean h > GMean f & Het h < Het f ) by Y2, HomogenHet, XXREAL_0:2, HomGMean; :: thesis:

end;

hence S₁[n] ; :: thesis:

end;

end;

S₁[ 0 ] from NAT_1:sch 7(B1, B2);
then consider g being non empty real-valued positive FinSequence such that
WW: ( Het g = 0 & Mean f = Mean g & GMean g > GMean f & Het g < Het f ) ;
g is homogeneous by WW;
hence ex g being homogeneous non empty real-valued positive FinSequence st
( GMean g > GMean f & Mean g = Mean f ) by WW; :: thesis: