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