theorem Th28: :: MATRIX13:28

for D being non empty set
for 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 j in Seg m & rng nt c= Seg (len A) holds
Col ((Segm (A,nt,mt)),j) = (Col (A,(mt . j))) * nt