theorem Th17: :: MATRPROB:17

for D1, D2 being non empty set
for M1 being Matrix of D1
for M2 being Matrix of D2 st M1 = M2 holds
for j being Nat st j in Seg (width M1) holds
Col (M1,j) = Col (M2,j)