let f be constant non empty real-valued FinSequence; :: thesis: Mean f = the_value_of f
reconsider v = the_value_of f as Real ;
Mean f = ((len f) * v) / (len f) by ConstantSum
.= v * ((len f) / (len f)) by XCMPLX_1:74
.= v * 1 by XCMPLX_1:60 ;
hence Mean f = the_value_of f ; :: thesis: verum