theorem Th60: :: MATRIX13:60

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