h
.
i
in
rng
h
by
FUNCT_1:3
;
then
h
.
i
in
NAT
*
;
hence
h
.
i
is
FinSequence
of
NAT
by
FINSEQ_1:def 11
;
:: thesis:
verum