let D be non empty set ; :: thesis: for m, n, m9, n9 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 m, n, m9, n9 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 7;
then nt . i in rng nt by FUNCT_1:def 3;
then ( rng mt = {} or [:(rng nt),(rng mt):] <> {} ) ;
then A7: rng mt c= Seg (width A9) by A3, ZFMISC_1:114;
nt . i in {j} by A4, A5, FUNCT_1:def 7;
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:124;
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_0:26;
dom F = Seg (width A9) by A1, FINSEQ_1:def 3;
then A11: dom Fmt = dom mt by A2, A7, RELAT_1:27;
A12: width (Segm (A9,nt,mt)) in NAT by ORDINAL1:def 12;
A13: n <> 0 by A6;
then width (Segm (A9,nt,mt)) = m by MATRIX_0:23;
then A14: len Fmt = width (Segm (A9,nt,mt)) by A11, A9, FINSEQ_1:def 3, A12;
A15: Indices A9 = Indices (RLine (A9,j,F)) by MATRIX_0:26;

now :: thesis: for k, l being Nat st [k,l] in Indices (Segm ((RLine (A9,j,F)),nt,mt)) holds
(RLine ((Segm (A9,nt,mt)),i,Fmt)) * (k,l) = (Segm ((RLine (A9,j,F)),nt,mt)) * (k,l)

A16: dom nt = Seg n by FINSEQ_2:124;
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 A17: [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₂)
A18: Indices (Segm (A9,nt,mt)) = [:(Seg n),(Seg m):] by A13, MATRIX_0:23;
then A19: k in Seg n by A10, A17, ZFMISC_1:87;
reconsider k9 = k, l9 = l as Element of NAT by ORDINAL1:def 12;
A20: (Segm ((RLine (A9,j,F)),nt,mt)) * (k,l) = (RLine (A9,j,F)) * ((nt . k9),(mt . l9)) by A17, Def1;
A21: [(nt . k9),(mt . l9)] in Indices A9 by A3, A15, A17, Th17;
A22: l in dom mt by A9, A10, A17, A18, ZFMISC_1:87;

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

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

then A24: (RLine ((Segm (A9,nt,mt)),i,Fmt)) * (k,l) = Fmt . l by A14, A10, A17, MATRIX11:def 3;
(Segm ((RLine (A9,j,F)),nt,mt)) * (k,l) = F . (mt . l) by A1, A8, A20, A21, A23, MATRIX11:def 3;
hence (RLine ((Segm (A9,nt,mt)),i,Fmt)) * (k,l) = (Segm ((RLine (A9,j,F)),nt,mt)) * (k,l) by A2, A22, A24, FUNCT_1:13; :: 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 A19, A16, FUNCT_1:def 7;
then A25: nt . k <> j by TARSKI:def 1;
then A26: (Segm ((RLine (A9,j,F)),nt,mt)) * (k,l) = A9 * ((nt . k9),(mt . l9)) by A1, A20, A21, MATRIX11:def 3;
(RLine ((Segm (A9,nt,mt)),i,Fmt)) * (k,l) = (Segm (A9,nt,mt)) * (k,l) by A8, A14, A10, A17, A25, MATRIX11:def 3;
hence (RLine ((Segm (A9,nt,mt)),i,Fmt)) * (k,l) = (Segm ((RLine (A9,j,F)),nt,mt)) * (k,l) by A10, A17, A26, Def1; :: thesis: verum

end;

end;

end;

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