let p be complex-valued FinSequence; :: thesis: for x being Complex holds
( |.(p ^ <*x*>).| = |.p.| ^ <*|.x.|*> & |.(<*x*> ^ p).| = <*|.x.|*> ^ |.p.| )
let x be Complex; :: thesis: ( |.(p ^ <*x*>).| = |.p.| ^ <*|.x.|*> & |.(<*x*> ^ p).| = <*|.x.|*> ^ |.p.| )
thus |.(p ^ <*x*>).| = |.p.| ^ |.<*x*>.| by Th12
.= |.p.| ^ <*|.x.|*> by Th9 ; :: thesis: |.(<*x*> ^ p).| = <*|.x.|*> ^ |.p.|
thus |.(<*x*> ^ p).| = |.<*x*>.| ^ |.p.| by Th12
.= <*|.x.|*> ^ |.p.| by Th9 ; :: thesis: verum