for L being Field
for m, n, k being Element of NAT st m > 0 & n > 0 holds
for M1 being Matrix of m,n,L
for M2 being Matrix of n,k,L holds ((emb (m,L)) * M1) * M2 = (emb (m,L)) * (M1 * M2)