theorem Huk1: :: RVSUM_3:5

for f being real-valued FinSequence holds Sum f = (len f) * (Mean f)