consider f being FinSequence of NAT ;
take f ; :: thesis: f is natural-valued
thus f is natural-valued ; :: thesis: verum