let f be heterogeneous non empty real-valued positive FinSequence; :: thesis: Het (Homogen f) < Het 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;
A2: ( i in dom f & j in dom f & i <> j ) by A1, BlaBla;
( f . i <> Mean f & f . j <> Mean f ) by A1, BlaBla;
hence Het (Homogen f) < Het f by HetMono, A1, A2; :: thesis: verum