theorem Th37: :: MATRIX13:37

for D being non empty set
for m, n, m9, n9 being Nat
for A9 being Matrix of n9,m9,D
for F, Fmt being FinSequence of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st len F = width A9 & Fmt = F * mt & [:(rng nt),(rng mt):] c= Indices A9 holds
for i, j being Nat st nt " {j} = {i} holds
RLine ((Segm (A9,nt,mt)),i,Fmt) = Segm ((RLine (A9,j,F)),nt,mt)