reconsider p1 = r1, p2 = r2 as Element of REAL by XREAL_0:def 1;
<*p1,p2*> is FinSequence-like ;
hence <*r1,r2*> is real-valued ; :: thesis: verum