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