reconsider p = r as Element of NAT by ORDINAL1:def 12;
<*p*> is FinSequence-like ;
hence <*r*> is natural-valued ; :: thesis: verum