let f be heterogeneous non empty real-valued positive FinSequence; :: thesis: GMean (Homogen f) > GMean f
consider i, j being Nat such that
A1: ( i = the Element of MeanLess f & j = the Element of MeanMore f & Homogen f = Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) ) by HomDef;
( i in dom f & j in dom f & i <> j ) by A1, BlaBla2;
then consider g being non empty real-valued positive FinSequence such that
J1: ( g = Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) & GMean f < GMean g ) by A1, ReplaceGMean3;
thus GMean (Homogen f) > GMean f by J1, A1; :: thesis: verum