let f be real-valued FinSequence; :: thesis: ( Sum f <> 0 implies Sum (f (/) (Sum f)) = 1 )
Sum (f (/) (Sum f)) = (Sum f) / (Sum f) by RVSUM_1:87;
hence ( Sum f <> 0 implies Sum (f (/) (Sum f)) = 1 ) by XCMPLX_1:60; :: thesis: verum