let f be real-valued FinSequence; :: thesis: Sum f = (len f) * (Mean f)

per cases ( len f <> 0 or len f = 0 ) ;

suppose len f <> 0 ; :: thesis: Sum f = (len f) * (Mean f)

hence Sum f = (len f) * (Mean f) by XCMPLX_1:87; :: thesis: verum

end;

suppose len f = 0 ; :: thesis: Sum f = (len f) * (Mean f)

then f = <*> REAL ;
hence Sum f = (len f) * (Mean f) by RVSUM_1:72; :: thesis: verum

end;

end;