for F being FinSequence of COMPLEX holds Product F = multcomplex $$ F ;