theorem Th59: :: MATRIX13:59

for D being non empty set
for i, m9, n9 being Nat
for A9 being Matrix of n9,m9,D
for P, Q being finite without_zero Subset of NAT
for F, FQ being FinSequence of D st len F = width A9 & FQ = F * (Sgm Q) & [:P,Q:] c= Indices A9 holds
RLine ((Segm (A9,P,Q)),i,FQ) = Segm ((RLine (A9,((Sgm P) . i),F)),P,Q)