theorem Th20: :: MATRIXC1:22

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