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 Def10;
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 Def10
.= A + (G . 1) by FINSEQ_1:40 ;
hence <*A*> (+) G = <*(A + (G . 1))*> by A1, FINSEQ_1:40; :: thesis: verum