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