theorem Th24: :: MATRIX13:24

for D being non empty set
for i, 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 n & rng mt c= Seg (width A) holds
Line ((Segm (A,nt,mt)),i) = (Line (A,(nt . i))) * mt