let f be heterogeneous non empty real-valued positive FinSequence; :: thesis: dom (Homogen f) = dom 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;
thus dom (Homogen f) = dom f by DinoDom, A1; :: thesis: verum