theorem :: POLYNOM5:13

for p being FinSequence of the carrier of F_Complex
for x being Element of F_Complex holds
( |.(p ^ <*x*>).| = |.p.| ^ <*|.x.|*> & |.(<*x*> ^ p).| = <*|.x.|*> ^ |.p.| )