n in NAT by ORDINAL1:def 12;
hence seq_const n is NAT -valued ; :: thesis: verum