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;