reconsider p1 = r1, p2 = r2 as Element of NAT by ORDINAL1:def 12;
<*p1,p2*> is FinSequence-like ;
hence <*r1,r2*> is natural-valued ; :: thesis: verum