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