let p be FinSequence of the carrier of F_Complex; :: thesis: for x being Element of F_Complex holds
( |.(p ^ <*x*>).| = |.p.| ^ <*|.x.|*> & |.(<*x*> ^ p).| = <*|.x.|*> ^ |.p.| )
let x be Element of F_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