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