theorem Th19: :: MATRIX13:19

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 [:(rng nt),(rng mt):] c= Indices A & ( m = 0 implies n = 0 ) holds
Segm (A,nt,mt) = (Segm ((A @),mt,nt)) @