let K be Field; :: thesis: for A1, A2 being Matrix of K holds <*A1*> (+) <*A2*> = <*(A1 + A2)*>
let A1, A2 be Matrix of K; :: thesis: <*A1*> (+) <*A2*> = <*(A1 + A2)*>
thus <*A1*> (+) <*A2*> = <*(A1 + (<*A2*> . 1))*> by Th68
.= <*(A1 + A2)*> by FINSEQ_1:40 ; :: thesis: verum