theorem :: POLYNOM5:13

for p being complex-valued FinSequence
for x being Complex holds
( |.(p ^ <*x*>).| = |.p.| ^ <*|.x.|*> & |.(<*x*> ^ p).| = <*|.x.|*> ^ |.p.| )