let D be non empty set ; :: thesis: for n9, m9, m, n 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 n9, m9, m, n 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_1:27;

now

A5: dom nt = Seg n by FINSEQ_2:144;
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_1:26;
then k in Seg n by A6, ZFMISC_1:106;
then A7: i <> nt . k by A1, A5, FUNCT_1:def 5;
reconsider K = k, M = m as Element of NAT by ORDINAL1:def 13;
[(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_1:28; :: thesis: verum

end;

end;