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:38 ;
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:40 ;
len (mlt (p,<*A*>)) = 1 by A1, FINSEQ_1:def 3;
hence mlt (p,<*A*>) = <*((p /. 1) * A)*> by A2, FINSEQ_1:40; :: thesis: verum