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