let f be FinSequence; :: thesis: ( f is empty-yielding implies f is NAT -valued )
assume f is empty-yielding ; :: thesis: f is NAT -valued
then ( ( 0 in NAT & rng f = {{}} ) or f = {} ) by PBOOLE:2;
then ( f is natural-valued or f is NAT -valued ) by ZFMISC_1:31, VALUED_0:def 6;
hence f is NAT -valued ; :: thesis: verum