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