set f = the FinSequence of NAT ;
take the FinSequence of NAT ; :: thesis: the FinSequence of NAT is natural-valued
thus the FinSequence of NAT is natural-valued ; :: thesis: verum