theorem Th24: :: MATRLIN:24

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
width (M1 ^ M2) = width M1