1 in dom p by FINSEQ_5:6;
hence ( p . 1 is finite & p . 1 is NAT -defined ) ; :: thesis: verum