let f be heterogeneous non empty real-valued positive FinSequence; 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; verum