let F be XFinSequence of NAT ; :: thesis: F is natural-valued
rng F c= NAT by RELAT_1:def 19;
hence F is natural-valued by VALUED_0:def 6; :: thesis: verum