let f be heterogeneous non empty real-valued positive FinSequence; :: thesis: Homogen f,f are_gamma-equivalent
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, BlaBla;
hence Homogen f,f are_gamma-equivalent by A1, ReplaceGamma; :: thesis: verum