theorem Th36: :: POLYNOM8:36

for L being Field
for m being Element of NAT st 0 < m holds
for u, v, u1 being Matrix of m,L st ( for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
(u * v) * (i,j) = (emb (m,L)) * (u1 * (i,j)) ) holds
u * v = (emb (m,L)) * u1