let D be non empty set ; :: thesis: 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)
let i, m9, n9 be Nat; :: thesis: 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)
let A9 be Matrix of n9,m9,D; :: thesis: 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)
let P, Q be finite without_zero Subset of NAT; :: thesis: 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)
let F, FQ be FinSequence of D; :: thesis: ( len F = width A9 & FQ = F * (Sgm Q) & [:P,Q:] c= Indices A9 implies RLine ((Segm (A9,P,Q)),i,FQ) = Segm ((RLine (A9,((Sgm P) . i),F)),P,Q) )
assume that
A1: len F = width A9 and
A2: FQ = F * (Sgm Q) and
A3: [:P,Q:] c= Indices A9 ; :: thesis: RLine ((Segm (A9,P,Q)),i,FQ) = Segm ((RLine (A9,((Sgm P) . i),F)),P,Q)
set SQ = Sgm Q;
set SP = Sgm P;
A4: card P = len (Segm (A9,P,Q)) by MATRIX_0:def 2;
A5: rng (Sgm Q) = Q by FINSEQ_1:def 14;
A7: rng (Sgm P) = P by FINSEQ_1:def 14;
A8: Sgm P is one-to-one by FINSEQ_3:92;
A9: dom (Sgm P) = Seg (card P) by FINSEQ_3:40;

per cases ( i in dom (Sgm P) or not i in dom (Sgm P) ) ;

suppose i in dom (Sgm P) ; :: thesis: RLine ((Segm (A9,P,Q)),i,FQ) = Segm ((RLine (A9,((Sgm P) . i),F)),P,Q)

then (Sgm P) " {((Sgm P) . i)} = {i} by A8, FINSEQ_5:4;
hence RLine ((Segm (A9,P,Q)),i,FQ) = Segm ((RLine (A9,((Sgm P) . i),F)),P,Q) by A1, A2, A3, A7, A5, Th37; :: thesis: verum

end;

suppose A10: not i in dom (Sgm P) ; :: thesis: RLine ((Segm (A9,P,Q)),i,FQ) = Segm ((RLine (A9,((Sgm P) . i),F)),P,Q)

A11: not 0 in Seg (len A9) ;
(Sgm P) . i = 0 by A10, FUNCT_1:def 2;
hence Segm ((RLine (A9,((Sgm P) . i),F)),P,Q) = Segm (A9,P,Q) by A11, Th40
.= RLine ((Segm (A9,P,Q)),i,FQ) by A9, A4, A10, Th40 ;
:: thesis: verum

end;

end;