let K be Field; for A1, A2, B1, B2 being Matrix of K holds <*A1,B1*> (+) <*A2,B2*> = <*(A1 + A2),(B1 + B2)*>
let A1, A2, B1, B2 be Matrix of K; <*A1,B1*> (+) <*A2,B2*> = <*(A1 + A2),(B1 + B2)*>
A1:
len <*A2*> = 1
by FINSEQ_1:39;
len <*A1*> = 1
by FINSEQ_1:39;
hence <*A1,B1*> (+) <*A2,B2*> =
(<*A1*> (+) <*A2*>) ^ (<*B1*> (+) <*B2*>)
by A1, Th67
.=
(<*A1*> (+) <*A2*>) ^ <*(B1 + B2)*>
by Th69
.=
<*(A1 + A2),(B1 + B2)*>
by Th69
;
verum