theorem Th13: :: COMPLSP2:17

for x being FinSequence of COMPLEX
for a being Complex holds (a * x) *' = (a *') * (x *')