theorem Th12: :: POLYNOM5:12

for p, q being FinSequence of the carrier of F_Complex holds |.(p ^ q).| = |.p.| ^ |.q.|