:: deftheorem HomDef defines Homogen RVSUM_3:def 10 :
for f being heterogeneous non empty real-valued positive FinSequence
for b₂ being real-valued FinSequence holds
( b₂ = Homogen f iff ex i, j being Nat st
( i = the Element of MeanLess f & j = the Element of MeanMore f & b₂ = Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) ) );