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 MeanLess f by A1;
then consider ii being Nat such that
A2: ( ii = i & ii in dom f & f . ii < Mean f ) ;
j in MeanMore f by A1;
then consider jj being Nat such that
A3: ( jj = j & jj in dom f & f . jj > Mean f ) ;
thus Homogen f is positive by A1, ReplacePositive2, A2, A3; :: thesis: verum