let K be Field; :: thesis: for A1, B1, A2, B2 being Matrix of K holds <*A1,B1*> (#) <*A2,B2*> = <*(A1 * A2),(B1 * B2)*>
let A1, B1, A2, B2 be Matrix of K; :: thesis: <*A1,B1*> (#) <*A2,B2*> = <*(A1 * A2),(B1 * B2)*>
( len <*A1*> = 1 & len <*A2*> = 1 ) by FINSEQ_1:56;
hence <*A1,B1*> (#) <*A2,B2*> = (<*A1*> (#) <*A2*>) ^ (<*B1*> (#) <*B2*>) by Th74
.= (<*A1*> (#) <*A2*>) ^ <*(B1 * B2)*> by Th76
.= <*(A1 * A2),(B1 * B2)*> by Th76 ;
:: thesis: verum