let s be positive Nat; :: thesis: Sum (s |-> (s ")) = 1
thus Sum (s |-> (s ")) = s * (s ") by RVSUM_1:80
.= 1 by XCMPLX_0:def 7 ; :: thesis: verum