let D be non empty set ; :: thesis: for n9, m9, n, m being Nat
for A9 being Matrix of n9,m9,D
for F, Fmt being FinSequence of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st len F = width A9 & Fmt = F * mt & [:(rng nt),(rng mt):] c= Indices A9 holds
for i, j being Nat st nt " {j} = {i} holds
RLine ((Segm (A9,nt,mt)),i,Fmt) = Segm ((RLine (A9,j,F)),nt,mt)
let n9, m9, n, m be Nat; :: thesis: for A9 being Matrix of n9,m9,D
for F, Fmt being FinSequence of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st len F = width A9 & Fmt = F * mt & [:(rng nt),(rng mt):] c= Indices A9 holds
for i, j being Nat st nt " {j} = {i} holds
RLine ((Segm (A9,nt,mt)),i,Fmt) = Segm ((RLine (A9,j,F)),nt,mt)
let A9 be Matrix of n9,m9,D; :: thesis: for F, Fmt being FinSequence of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st len F = width A9 & Fmt = F * mt & [:(rng nt),(rng mt):] c= Indices A9 holds
for i, j being Nat st nt " {j} = {i} holds
RLine ((Segm (A9,nt,mt)),i,Fmt) = Segm ((RLine (A9,j,F)),nt,mt)
let F, Fmt be FinSequence of D; :: thesis: for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st len F = width A9 & Fmt = F * mt & [:(rng nt),(rng mt):] c= Indices A9 holds
for i, j being Nat st nt " {j} = {i} holds
RLine ((Segm (A9,nt,mt)),i,Fmt) = Segm ((RLine (A9,j,F)),nt,mt)
let nt be Element of n -tuples_on NAT; :: thesis: for mt being Element of m -tuples_on NAT st len F = width A9 & Fmt = F * mt & [:(rng nt),(rng mt):] c= Indices A9 holds
for i, j being Nat st nt " {j} = {i} holds
RLine ((Segm (A9,nt,mt)),i,Fmt) = Segm ((RLine (A9,j,F)),nt,mt)
let mt be Element of m -tuples_on NAT; :: thesis: ( len F = width A9 & Fmt = F * mt & [:(rng nt),(rng mt):] c= Indices A9 implies for i, j being Nat st nt " {j} = {i} holds
RLine ((Segm (A9,nt,mt)),i,Fmt) = Segm ((RLine (A9,j,F)),nt,mt) )
assume that
A1: len F = width A9 and
A2: Fmt = F * mt and
A3: [:(rng nt),(rng mt):] c= Indices A9 ; :: thesis: for i, j being Nat st nt " {j} = {i} holds
RLine ((Segm (A9,nt,mt)),i,Fmt) = Segm ((RLine (A9,j,F)),nt,mt)
let i, j be Nat; :: thesis: ( nt " {j} = {i} implies RLine ((Segm (A9,nt,mt)),i,Fmt) = Segm ((RLine (A9,j,F)),nt,mt) )
assume A4: nt " {j} = {i} ; :: thesis: RLine ((Segm (A9,nt,mt)),i,Fmt) = Segm ((RLine (A9,j,F)),nt,mt)
A5: i in {i} by TARSKI:def 1;
then A6: i in dom nt by A4, FUNCT_1:def 13;
then nt . i in rng nt by FUNCT_1:def 5;
then ( rng mt = {} or [:(rng nt),(rng mt):] <> {} ) ;
then A7: rng mt c= Seg (width A9) by A3, XBOOLE_1:2, ZFMISC_1:138;
nt . i in {j} by A4, A5, FUNCT_1:def 13;
then A8: nt . i = j by TARSKI:def 1;
set R = RLine (A9,j,F);
set SR = Segm ((RLine (A9,j,F)),nt,mt);
set S = Segm (A9,nt,mt);
A9: dom mt = Seg m by FINSEQ_2:144;
set RS = RLine ((Segm (A9,nt,mt)),i,Fmt);
A10: Indices (Segm ((RLine (A9,j,F)),nt,mt)) = Indices (Segm (A9,nt,mt)) by MATRIX_1:27;
dom F = Seg (width A9) by A1, FINSEQ_1:def 3;
then A11: dom Fmt = dom mt by A2, A7, RELAT_1:46;
A12: n <> 0 by A6;
then width (Segm (A9,nt,mt)) = m by MATRIX_1:24;
then A13: len Fmt = width (Segm (A9,nt,mt)) by A11, A9, FINSEQ_1:def 3;
A14: Indices A9 = Indices (RLine (A9,j,F)) by MATRIX_1:27;

now

A15: dom nt = Seg n by FINSEQ_2:144;
let k, l be Nat; :: thesis: ( [k,l] in Indices (Segm ((RLine (A9,j,F)),nt,mt)) implies (RLine ((Segm (A9,nt,mt)),i,Fmt)) * (b₁,b₂) = (Segm ((RLine (A9,j,F)),nt,mt)) * (b₁,b₂) )
assume A16: [k,l] in Indices (Segm ((RLine (A9,j,F)),nt,mt)) ; :: thesis: (RLine ((Segm (A9,nt,mt)),i,Fmt)) * (b₁,b₂) = (Segm ((RLine (A9,j,F)),nt,mt)) * (b₁,b₂)
A17: Indices (Segm (A9,nt,mt)) = [:(Seg n),(Seg m):] by A12, MATRIX_1:24;
then A18: k in Seg n by A10, A16, ZFMISC_1:106;
reconsider k9 = k, l9 = l as Element of NAT by ORDINAL1:def 13;
A19: (Segm ((RLine (A9,j,F)),nt,mt)) * (k,l) = (RLine (A9,j,F)) * ((nt . k9),(mt . l9)) by A16, Def1;
A20: [(nt . k9),(mt . l9)] in Indices A9 by A3, A14, A16, Th17;
A21: l in dom mt by A9, A10, A16, A17, ZFMISC_1:106;

per cases ( k = i or k <> i ) ;

suppose A22: k = i ; :: thesis: (RLine ((Segm (A9,nt,mt)),i,Fmt)) * (b₁,b₂) = (Segm ((RLine (A9,j,F)),nt,mt)) * (b₁,b₂)

then A23: (RLine ((Segm (A9,nt,mt)),i,Fmt)) * (k,l) = Fmt . l by A13, A10, A16, MATRIX11:def 3;
(Segm ((RLine (A9,j,F)),nt,mt)) * (k,l) = F . (mt . l) by A1, A8, A19, A20, A22, MATRIX11:def 3;
hence (RLine ((Segm (A9,nt,mt)),i,Fmt)) * (k,l) = (Segm ((RLine (A9,j,F)),nt,mt)) * (k,l) by A2, A21, A23, FUNCT_1:23; :: thesis: verum

end;

suppose k <> i ; :: thesis: (RLine ((Segm (A9,nt,mt)),i,Fmt)) * (b₁,b₂) = (Segm ((RLine (A9,j,F)),nt,mt)) * (b₁,b₂)

then not k in nt " {j} by A4, TARSKI:def 1;
then not nt . k in {j} by A18, A15, FUNCT_1:def 13;
then A24: nt . k <> j by TARSKI:def 1;
then A25: (Segm ((RLine (A9,j,F)),nt,mt)) * (k,l) = A9 * ((nt . k9),(mt . l9)) by A1, A19, A20, MATRIX11:def 3;
(RLine ((Segm (A9,nt,mt)),i,Fmt)) * (k,l) = (Segm (A9,nt,mt)) * (k,l) by A8, A13, A10, A16, A24, MATRIX11:def 3;
hence (RLine ((Segm (A9,nt,mt)),i,Fmt)) * (k,l) = (Segm ((RLine (A9,j,F)),nt,mt)) * (k,l) by A10, A16, A25, Def1; :: thesis: verum

end;

end;

end;

hence RLine ((Segm (A9,nt,mt)),i,Fmt) = Segm ((RLine (A9,j,F)),nt,mt) by MATRIX_1:28; :: thesis: verum