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 S = Segm A',nt,mt;
set R = RLine A',i,F;
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

A5: dom nt = Seg n by FINSEQ_2:144;
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 A6: [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
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 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 A' by A2, A4, A6, Th17;
then A8: A' * (nt . K),(mt . M) = (RLine A',i,F) * (nt . K),(mt . M) by A3, A7, MATRIX11:def 3;
(Segm A',nt,mt) * K,M = A' * (nt . K),(mt . M) by A4, A6, Def1;
hence (Segm (RLine A',i,F),nt,mt) * k,m = (Segm A',nt,mt) * k,m by A6, A8, Def1; :: thesis: verum

end;

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

end;

end;