let r be Complex; :: thesis: Product <*r*> = r
reconsider r9 = r as Element of COMPLEX by XCMPLX_0:def 2;
reconsider F = <*r9*> as FinSequence of COMPLEX ;
multcomplex $$ F = r by FINSOP_1:11;
hence Product <*r*> = r by Def13; :: thesis: verum