let D be non empty set ; :: thesis: for m, n, m9, n9 being Nat
for A9 being Matrix of n9,m9,D
for mt being Element of m -tuples_on NAT
for F being FinSequence of D
for i being Nat
for nt being Element of n -tuples_on NAT st not i in rng nt & [:(rng nt),(rng mt):] c= Indices A9 holds
Segm (A9,nt,mt) = Segm ((RLine (A9,i,F)),nt,mt)
let m, n, m9, n9 be Nat; :: thesis: for A9 being Matrix of n9,m9,D
for mt being Element of m -tuples_on NAT
for F being FinSequence of D
for i being Nat
for nt being Element of n -tuples_on NAT st not i in rng nt & [:(rng nt),(rng mt):] c= Indices A9 holds
Segm (A9,nt,mt) = Segm ((RLine (A9,i,F)),nt,mt)
let A9 be Matrix of n9,m9,D; :: thesis: for mt being Element of m -tuples_on NAT
for F being FinSequence of D
for i being Nat
for nt being Element of n -tuples_on NAT st not i in rng nt & [:(rng nt),(rng mt):] c= Indices A9 holds
Segm (A9,nt,mt) = Segm ((RLine (A9,i,F)),nt,mt)
let mt be Element of m -tuples_on NAT; :: thesis: for F being FinSequence of D
for i being Nat
for nt being Element of n -tuples_on NAT st not i in rng nt & [:(rng nt),(rng mt):] c= Indices A9 holds
Segm (A9,nt,mt) = Segm ((RLine (A9,i,F)),nt,mt)
let F be FinSequence of D; :: thesis: for i being Nat
for nt being Element of n -tuples_on NAT st not i in rng nt & [:(rng nt),(rng mt):] c= Indices A9 holds
Segm (A9,nt,mt) = Segm ((RLine (A9,i,F)),nt,mt)
let i be Nat; :: thesis: for nt being Element of n -tuples_on NAT st not i in rng nt & [:(rng nt),(rng mt):] c= Indices A9 holds
Segm (A9,nt,mt) = Segm ((RLine (A9,i,F)),nt,mt)
let nt be Element of n -tuples_on NAT; :: thesis: ( not i in rng nt & [:(rng nt),(rng mt):] c= Indices A9 implies Segm (A9,nt,mt) = Segm ((RLine (A9,i,F)),nt,mt) )
assume that
A1: not i in rng nt and
A2: [:(rng nt),(rng mt):] c= Indices A9 ; :: thesis: Segm (A9,nt,mt) = Segm ((RLine (A9,i,F)),nt,mt)
set S = Segm (A9,nt,mt);
set R = RLine (A9,i,F);
set SR = Segm ((RLine (A9,i,F)),nt,mt);

per cases ( len F <> width A9 or len F = width A9 ) ;

suppose len F <> width A9 ; :: thesis: Segm (A9,nt,mt) = Segm ((RLine (A9,i,F)),nt,mt)

hence Segm (A9,nt,mt) = Segm ((RLine (A9,i,F)),nt,mt) by MATRIX11:def 3; :: thesis: verum

end;

suppose A3: len F = width A9 ; :: thesis: Segm (A9,nt,mt) = Segm ((RLine (A9,i,F)),nt,mt)

A4: Indices (Segm ((RLine (A9,i,F)),nt,mt)) = Indices (Segm (A9,nt,mt)) by MATRIX_0:26;

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

A5: dom nt = Seg n by FINSEQ_2:124;
let k, m be Nat; :: thesis: ( [k,m] in Indices (Segm ((RLine (A9,i,F)),nt,mt)) implies (Segm ((RLine (A9,i,F)),nt,mt)) * (k,m) = (Segm (A9,nt,mt)) * (k,m) )
assume A6: [k,m] in Indices (Segm ((RLine (A9,i,F)),nt,mt)) ; :: thesis: (Segm ((RLine (A9,i,F)),nt,mt)) * (k,m) = (Segm (A9,nt,mt)) * (k,m)
Indices (Segm ((RLine (A9,i,F)),nt,mt)) = [:(Seg n),(Seg (width (Segm ((RLine (A9,i,F)),nt,mt)))):] by MATRIX_0:25;
then k in Seg n by A6, ZFMISC_1:87;
then A7: i <> nt . k by A1, A5, FUNCT_1:def 3;
reconsider K = k, M = m as Element of NAT by ORDINAL1:def 12;
[(nt . K),(mt . M)] in Indices A9 by A2, A4, A6, Th17;
then A8: A9 * ((nt . K),(mt . M)) = (RLine (A9,i,F)) * ((nt . K),(mt . M)) by A3, A7, MATRIX11:def 3;
(Segm (A9,nt,mt)) * (K,M) = A9 * ((nt . K),(mt . M)) by A4, A6, Def1;
hence (Segm ((RLine (A9,i,F)),nt,mt)) * (k,m) = (Segm (A9,nt,mt)) * (k,m) by A6, A8, Def1; :: thesis: verum

end;

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

end;

end;