theorem Th28: :: MATRLIN:28

for k, m, n being Nat
for D being non empty set
for M1 being Matrix of n,k,D
for M2 being Matrix of m,k,D st width M1 = width M2 holds
(M1 ^ M2) @ = (M1 @) ^^ (M2 @)