let D be non empty set ; :: thesis: for n9, m9, i being Nat
for A9 being Matrix of n9,m9,D
for Q, P 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 n9, m9, i be Nat; :: thesis: for A9 being Matrix of n9,m9,D
for Q, P 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 Q, P 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 Q, P 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_1:def 3;
ex m being Nat st Q c= Seg m by Th43;
then A5: rng (Sgm Q) = Q by FINSEQ_1:def 13;
A6: ex n being Nat st P c= Seg n by Th43;
then A7: rng (Sgm P) = P by FINSEQ_1:def 13;
A8: Sgm P is without_repeated_line by A6, FINSEQ_3:99;
A9: dom (Sgm P) = Seg (card P) by A6, FINSEQ_3:45;

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 4;
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;