let K be Field; 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; for p being FinSequence of K holds mlt (p,<*A*>) = <*((p /. 1) * A)*>
let p be FinSequence of K; 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; verum