let K be Field; :: thesis: for A being Matrix of K
for p being FinSequence of K holds mlt p,<*A*> = <*((p /. 1) * A)*>
let A be Matrix of K; :: thesis: for p being FinSequence of K holds mlt p,<*A*> = <*((p /. 1) * A)*>
let p be FinSequence of K; :: thesis: mlt p,<*A*> = <*((p /. 1) * A)*>
A1: dom (mlt p,<*A*>) = dom <*A*> by Def9
.= Seg 1 by FINSEQ_1:55 ;
then 1 in dom (mlt p,<*A*>) ;
then A2: (mlt p,<*A*>) . 1 = (p /. 1) * (<*A*> . 1) by Def9
.= (p /. 1) * A by FINSEQ_1:57 ;
len (mlt p,<*A*>) = 1 by A1, FINSEQ_1:def 3;
hence mlt p,<*A*> = <*((p /. 1) * A)*> by A2, FINSEQ_1:57; :: thesis: verum