let f be Complex_Sequence; :: thesis: ( f is empty-yielding implies f is natural-valued )
assume f is empty-yielding ; :: thesis: f is natural-valued
then for x being object st x in dom f holds
f . x is natural ;
hence f is natural-valued by VALUED_0:def 12; :: thesis: verum