dom (NPower (n,0)) = Seg 0 by Def8
.= {} ;
hence Sum (NPower (n,0)) = 0 by RVSUM_1:72, RELAT_1:41; :: thesis: verum