let D be non empty set ; :: thesis:
let i, j, m, n, m9, n9 be Nat; :: thesis:
let A9 be Matrix of n9,m9,D; :: thesis:
let nt be Element of n -tuples_on NAT; :: thesis:
let mt be Element of m -tuples_on NAT; :: thesis:
assume that
A1: i in rng nt and
A2: [:(rng nt),(rng mt):] c= Indices A9 ; :: thesis:
defpred S₁[ set , set ] means for k being Nat st k = $1 holds
( ( nt . k = i implies $2 = j ) & ( nt . k <> i implies $2 = nt . k ) );
A3: for k being Nat st k in Seg n holds
ex x being Element of NAT st S₁[k,x]

let k be Nat; :: thesis:
assume k in Seg n ; :: thesis:

end;

end;

consider p being FinSequence of NAT such that
A6: dom p = Seg n and
A7: for k being Nat st k in Seg n holds
S₁[k,p . k] from FINSEQ_1:sch 5(A3);
n in NAT by ORDINAL1:def 12;
then len p = n by A6, FINSEQ_1:def 3;
then reconsider p9 = p as Element of n -tuples_on NAT by FINSEQ_2:92;
A8: rng p9 c= ((rng nt) \ {i}) \/ {j}

let y be object ; :: according to TARSKI:def 3 :: thesis:
A9: dom nt = Seg n by FINSEQ_2:124;
assume y in rng p9 ; :: thesis:
then consider x being object such that
A10: x in dom p and
A11: p . x = y by FUNCT_1:def 3;
consider k being Nat such that
A12: x = k and
1 <= k and
k <= n by A6, A10;
( ( p . k = j & nt . k = i ) or ( p . k = nt . k & nt . k <> i & nt . k in rng nt ) ) by A6, A7, A10, A12, A9, FUNCT_1:def 3;
then ( p . k in {j} or ( p . k in rng nt & not p . k in {i} ) ) by TARSKI:def 1;
then ( p . k in {j} or p . k in (rng nt) \ {i} ) by XBOOLE_0:def 5;
hence y in ((rng nt) \ {i}) \/ {j} by A11, A12, XBOOLE_0:def 3; :: thesis:

end;

take p9 ; :: thesis:
((rng nt) \ {i}) \/ {j} c= rng p9

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A13: y in ((rng nt) \ {i}) \/ {j} ; :: thesis:

end;

then A19: y = j by TARSKI:def 1;
consider x being object such that
A20: x in dom nt and
A21: nt . x = i by A1, FUNCT_1:def 3;
A22: dom nt = Seg n by FINSEQ_2:124;
then consider k being Nat such that
A23: x = k and
1 <= k and
k <= n by A20;
p . k = j by A7, A20, A21, A22, A23;
hence y in rng p9 by A6, A20, A22, A23, A19, FUNCT_1:def 3; :: thesis:

end;

hence rng p9 = ((rng nt) \ {i}) \/ {j} by A8, XBOOLE_0:def 10; :: thesis:
set S = Segm (A9,p9,mt);
set LA = Line (A9,j);
set R = RLine (A9,i,(Line (A9,j)));
set SR = Segm ((RLine (A9,i,(Line (A9,j)))),nt,mt);
A24: Indices A9 = Indices (RLine (A9,i,(Line (A9,j)))) by MATRIX_0:26;
A25: len (Line (A9,j)) = width A9 by MATRIX_0:def 7;
A26: Indices (Segm (A9,p9,mt)) = Indices (Segm ((RLine (A9,i,(Line (A9,j)))),nt,mt)) by MATRIX_0:26;

let k, l be Nat; :: thesis:
assume A27: [k,l] in Indices (Segm ((RLine (A9,i,(Line (A9,j)))),nt,mt)) ; :: thesis:
reconsider K = k, L = l as Element of NAT by ORDINAL1:def 12;
A28: (Segm ((RLine (A9,i,(Line (A9,j)))),nt,mt)) * (K,L) = (RLine (A9,i,(Line (A9,j)))) * ((nt . K),(mt . L)) by A27, Def1;
Indices (Segm ((RLine (A9,i,(Line (A9,j)))),nt,mt)) = [:(Seg n),(Seg (width (Segm ((RLine (A9,i,(Line (A9,j)))),nt,mt)))):] by MATRIX_0:25;
then A29: K in Seg n by A27, ZFMISC_1:87;
A30: ( nt . K = i or nt . K <> i ) ;
A31: [(nt . K),(mt . L)] in Indices A9 by A2, A24, A27, Th17;
then mt . L in Seg (width A9) by ZFMISC_1:87;
then ( ( (Segm ((RLine (A9,i,(Line (A9,j)))),nt,mt)) * (K,L) = (Line (A9,j)) . (mt . L) & p9 . K = j & (Line (A9,j)) . (mt . L) = A9 * (j,(mt . L)) ) or ( (Segm ((RLine (A9,i,(Line (A9,j)))),nt,mt)) * (K,L) = A9 * ((nt . K),(mt . L)) & p9 . K = nt . K ) ) by A7, A25, A31, A28, A30, A29, MATRIX11:def 3, MATRIX_0:def 7;
hence (Segm ((RLine (A9,i,(Line (A9,j)))),nt,mt)) * (k,l) = (Segm (A9,p9,mt)) * (k,l) by A26, A27, Def1; :: thesis:

end;

hence Segm ((RLine (A9,i,(Line (A9,j)))),nt,mt) = Segm (A9,p9,mt) by MATRIX_0:27; :: thesis: