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 Th75
.= <*(A1 * A2)*> ; :: thesis: verum