theorem Th17: :: MATRIX15:17

for k, m, n being Nat
for D being non empty set
for A being Matrix of n,m,D
for B being Matrix of n,k,D
for i being Nat st i in Seg (width B) holds
Col ((A ^^ B),((width A) + i)) = Col (B,i)