let D be non empty set ; :: thesis: for n', m', m, n being Nat
for A' being Matrix of n',m',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 A' holds
Segm A',nt,mt = Segm (RLine A',i,F),nt,mt
let n', m', m, n be Nat; :: thesis: for A' being Matrix of n',m',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 A' holds
Segm A',nt,mt = Segm (RLine A',i,F),nt,mt
let A' be Matrix of n',m',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 A' holds
Segm A',nt,mt = Segm (RLine A',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 A' holds
Segm A',nt,mt = Segm (RLine A',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 A' holds
Segm A',nt,mt = Segm (RLine A',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 A' holds
Segm A',nt,mt = Segm (RLine A',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 A' implies Segm A',nt,mt = Segm (RLine A',i,F),nt,mt )
assume that
A1: not i in rng nt and
A2: [:(rng nt),(rng mt):] c= Indices A' ; :: thesis: Segm A',nt,mt = Segm (RLine A',i,F),nt,mt
set R = RLine A',i,F;
set S = Segm A',nt,mt;
set SR = Segm (RLine A',i,F),nt,mt;

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

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

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

end;

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

A4: Indices (Segm (RLine A',i,F),nt,mt) = Indices (Segm A',nt,mt) by MATRIX_1:27;

now

let k, m be Nat; :: thesis: ( [k,m] in Indices (Segm (RLine A',i,F),nt,mt) implies (Segm (RLine A',i,F),nt,mt) * k,m = (Segm A',nt,mt) * k,m )
assume A5: [k,m] in Indices (Segm (RLine A',i,F),nt,mt) ; :: thesis: (Segm (RLine A',i,F),nt,mt) * k,m = (Segm A',nt,mt) * k,m
reconsider K = k, M = m as Element of NAT by ORDINAL1:def 13;
Indices (Segm (RLine A',i,F),nt,mt) = [:(Seg n),(Seg (width (Segm (RLine A',i,F),nt,mt))):] by MATRIX_1:26;
then ( k in Seg n & dom nt = Seg n ) by A5, FINSEQ_2:144, ZFMISC_1:106;
then ( i <> nt . k & [(nt . K),(mt . M)] in Indices A' ) by A1, A2, A4, A5, Th17, FUNCT_1:def 5;
then ( (Segm A',nt,mt) * K,M = A' * (nt . K),(mt . M) & A' * (nt . K),(mt . M) = (RLine A',i,F) * (nt . K),(mt . M) ) by A3, A4, A5, Def1, MATRIX11:def 3;
hence (Segm (RLine A',i,F),nt,mt) * k,m = (Segm A',nt,mt) * k,m by A5, Def1; :: thesis: verum

end;

hence Segm A',nt,mt = Segm (RLine A',i,F),nt,mt by MATRIX_1:28; :: thesis: verum

end;

end;