let F be Sequence; :: thesis: ( F is natural-valued implies F is Ordinal-yielding )
assume F is natural-valued ; :: thesis: F is Ordinal-yielding
then rng F c= NAT by VALUED_0:def 6;
hence F is Ordinal-yielding by ORDINAL2:def 4; :: thesis: verum