let D be non empty set ; :: thesis: for n', m', i being Nat
for A' being Matrix of n',m',D
for Q, P being finite without_zero Subset of
for F, FQ being FinSequence of D st len F = width A' & FQ = F * (Sgm Q) & [:P,Q:] c= Indices A' holds
RLine (Segm A',P,Q),i,FQ = Segm (RLine A',((Sgm P) . i),F),P,Q
let n', m', i be Nat; :: thesis: for A' being Matrix of n',m',D
for Q, P being finite without_zero Subset of
for F, FQ being FinSequence of D st len F = width A' & FQ = F * (Sgm Q) & [:P,Q:] c= Indices A' holds
RLine (Segm A',P,Q),i,FQ = Segm (RLine A',((Sgm P) . i),F),P,Q
let A' be Matrix of n',m',D; :: thesis: for Q, P being finite without_zero Subset of
for F, FQ being FinSequence of D st len F = width A' & FQ = F * (Sgm Q) & [:P,Q:] c= Indices A' holds
RLine (Segm A',P,Q),i,FQ = Segm (RLine A',((Sgm P) . i),F),P,Q
let Q, P be finite without_zero Subset of ; :: thesis: for F, FQ being FinSequence of D st len F = width A' & FQ = F * (Sgm Q) & [:P,Q:] c= Indices A' holds
RLine (Segm A',P,Q),i,FQ = Segm (RLine A',((Sgm P) . i),F),P,Q
let F, FQ be FinSequence of D; :: thesis: ( len F = width A' & FQ = F * (Sgm Q) & [:P,Q:] c= Indices A' implies RLine (Segm A',P,Q),i,FQ = Segm (RLine A',((Sgm P) . i),F),P,Q )
assume that
A1: len F = width A' and
A2: FQ = F * (Sgm Q) and
A3: [:P,Q:] c= Indices A' ; :: thesis: RLine (Segm A',P,Q),i,FQ = Segm (RLine A',((Sgm P) . i),F),P,Q
set SQ = Sgm Q;
set SP = Sgm P;
A4: card P = len (Segm A',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 A',P,Q),i,FQ = Segm (RLine A',((Sgm P) . i),F),P,Q

then (Sgm P) " {((Sgm P) . i)} = {i} by A8, FINSEQ_5:4;
hence RLine (Segm A',P,Q),i,FQ = Segm (RLine A',((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 A',P,Q),i,FQ = Segm (RLine A',((Sgm P) . i),F),P,Q

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

end;

end;