theorem Th12: :: POLYNOM5:12

for p, q being complex-valued FinSequence holds |.(p ^ q).| = |.p.| ^ |.q.|