let f be real-valued FinSequence; :: thesis: Mean (f ^ <*(Mean f)*>) = Mean f
Mean (f ^ <*(Mean f)*>) = ((Sum f) + (Mean f)) / (len (f ^ <*(Mean f)*>)) by RVSUM_1:74
.= ((Sum f) + (Mean f)) / ((len f) + (len <*(Mean f)*>)) by FINSEQ_1:22
.= ((Sum f) + (Mean f)) / ((len f) + 1) by FINSEQ_1:39
.= (((len f) * (Mean f)) + (Mean f)) / ((len f) + 1) by Huk1
.= ((Mean f) * ((len f) + 1)) / ((len f) + 1)
.= Mean f by XCMPLX_1:89 ;
hence Mean (f ^ <*(Mean f)*>) = Mean f ; :: thesis: verum