theorem HomogenHet: :: RVSUM_3:43

for f being heterogeneous non empty real-valued positive FinSequence holds Het (Homogen f) < Het f