let i be Nat; :: thesis: for F being FinSequence of COMPLEX
for M being Matrix of COMPLEX st len F = width M holds
mlt F,((Line (M *' ),i) *' ) = (mlt (Line (M *' ),i),(F *' )) *'
let F be FinSequence of COMPLEX ; :: thesis: for M being Matrix of COMPLEX st len F = width M holds
mlt F,((Line (M *' ),i) *' ) = (mlt (Line (M *' ),i),(F *' )) *'
let M be Matrix of COMPLEX ; :: thesis: ( len F = width M implies mlt F,((Line (M *' ),i) *' ) = (mlt (Line (M *' ),i),(F *' )) *' )
assume A1: len F = width M ; :: thesis: mlt F,((Line (M *' ),i) *' ) = (mlt (Line (M *' ),i),(F *' )) *'
len (Line (M *' ),i) = width (M *' ) by MATRIX_1:def 8
.= width M by Def1 ;
hence mlt F,((Line (M *' ),i) *' ) = (mlt (Line (M *' ),i),(F *' )) *' by A1, Th25; :: thesis: verum