let f be non empty real-valued positive FinSequence; :: thesis: GMean f <= Mean f

per cases ( Het f = 0 or Het f <> 0 ) ;

suppose Het f = 0 ; :: thesis: GMean f <= Mean f

then reconsider ff = f as homogeneous non empty real-valued positive FinSequence ;
GMean ff = Mean ff by HetBase;
hence GMean f <= Mean f ; :: thesis: verum

end;

suppose Het f <> 0 ; :: thesis: GMean f <= Mean f

then reconsider ff = f as heterogeneous non empty real-valued positive FinSequence by HetHetero;
ex g being homogeneous non empty real-valued positive FinSequence st
( GMean g > GMean ff & Mean g = Mean ff ) by WOWTheo;
hence GMean f <= Mean f by HetBase; :: thesis: verum

end;

end;