theorem Th42: :: MATRIX13:42

for D being non empty set
for 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 nt = idseq (len A) & mt = idseq (width A) holds
Segm (A,nt,mt) = A