for F being FinSequence of COMPLEX st len (F *') >= 1 holds
addcomplex $$ (F *') = (addcomplex $$ F) *'