theorem Th63: :: MATRIXJ1:63
for K being Field
for A being Matrix of K
for p being FinSequence of K holds mlt (p,<*A*>) = <*((p /. 1) * A)*>