theorem :: RVSUM_3:6

for f being real-valued FinSequence holds Mean (f ^ <*(Mean f)*>) = Mean f