let K be Field; :: thesis: for A being Matrix of K
for G being FinSequence_of_Matrix of K holds <*A*> (#) G = <*(A * (G . 1))*>
let A be Matrix of K; :: thesis: for G being FinSequence_of_Matrix of K holds <*A*> (#) G = <*(A * (G . 1))*>
let G be FinSequence_of_Matrix of K; :: thesis: <*A*> (#) G = <*(A * (G . 1))*>
dom (<*A*> (#) G) = dom <*A*> by Def11;
then A1: len (<*A*> (#) G) = len <*A*> by FINSEQ_3:29
.= 1 by FINSEQ_1:39 ;
then dom (<*A*> (#) G) = {1} by FINSEQ_1:2, FINSEQ_1:def 3;
then 1 in dom (<*A*> (#) G) by TARSKI:def 1;
then (<*A*> (#) G) . 1 = (<*A*> . 1) * (G . 1) by Def11
.= A * (G . 1) ;
hence <*A*> (#) G = <*(A * (G . 1))*> by A1, FINSEQ_1:40; :: thesis: verum