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