:: deftheorem defines Mean RVSUM_3:def 2 :
for f being real-valued FinSequence holds Mean f = (Sum f) / (len f);