theorem Th29: :: MATRIX13:29

for D being non empty set
for i, j, m, n being Nat
for A being Matrix of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st i in Seg m & j in Seg m & mt . i = mt . j holds
Col ((Segm (A,nt,mt)),i) = Col ((Segm (A,nt,mt)),j)