reconsider p = r as Element of COMPLEX by XCMPLX_0:def 2;
reconsider f = <*p*> as FinSequence of COMPLEX ;
f is FinSequence-like ;
hence <*r*> is complex-yielding ; :: thesis: verum