A1: for n being Nat st n in dom h holds
h . n >= 0 ;
Sum h is integer ;
then Sum h is Element of NAT by A1, RVSUM_1:84, INT_1:3;
hence Sum h is natural ; :: thesis: verum