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 Th13
.= |.p.| ^ <*|.x.|*> by Th10 ; :: thesis: |.(<*x*> ^ p).| = <*|.x.|*> ^ |.p.|
thus |.(<*x*> ^ p).| = |.<*x*>.| ^ |.p.| by Th13
.= <*|.x.|*> ^ |.p.| by Th10 ; :: thesis: verum