let f be heterogeneous non empty real-valued positive FinSequence; :: thesis: ex g being homogeneous non empty real-valued positive FinSequence st
( GMean g > GMean f & Mean g = Mean f )
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]

proof

reconsider g = Homogen f as non empty real-valued positive FinSequence ;
take k = Het g; :: thesis: S₁[k]
take g ; :: thesis: ( Het g = k & Mean f = Mean g & GMean g > GMean f & Het g < Het f )
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: verum

end;

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

proof

let k be Nat; :: thesis: ( k <> 0 & S₁[k] implies ex n being Nat st
( n < k & S₁[n] ) )
assume Y1: ( k <> 0 & S₁[k] ) ; :: thesis: ex n being Nat st
( n < k & S₁[n] )
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: ( n < k & S₁[n] )
thus n < k by Y2, HomogenHet; :: thesis: S₁[n]
thus S₁[n] :: thesis: verum

proof

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 )

proof

take h ; :: thesis: ( Het h = n & Mean f = Mean h & GMean h > GMean f & Het h < Het f )
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: verum

end;

hence S₁[n] ; :: thesis: verum

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: verum