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_0:def 7
.= width M by Def1 ;
hence mlt (F,((Line ((M *'),i)) *')) = (mlt ((Line ((M *'),i)),(F *'))) *' by A1, Th22; :: thesis: verum