reconsider p1 = r1, p2 = r2, p3 = r3 as Element of COMPLEX by XCMPLX_0:def 2;
reconsider f = <*p1,p2,p3*> as FinSequence of COMPLEX ;
f is FinSequence-like ;
hence <*r1,r2,r3*> is complex-valued ; :: thesis: verum