theorem Th77: :: MATRIXJ1:77
for K being Field
for A1, A2, B1, B2 being Matrix of K holds <*A1,B1*> (#) <*A2,B2*> = <*(A1 * A2),(B1 * B2)*>