let D be non empty set ; :: thesis: for n9, m9, m, i, n, j being Nat
for A9 being Matrix of n9,m9,D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st i in rng nt & [:(rng nt),(rng mt):] c= Indices A9 holds
ex nt1 being Element of n -tuples_on NAT st
( rng nt1 = ((rng nt) \ {i}) \/ {j} & Segm (RLine A9,i,(Line A9,j)),nt,mt = Segm A9,nt1,mt )
let n9, m9, m, i, n, j be Nat; :: thesis: for A9 being Matrix of n9,m9,D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st i in rng nt & [:(rng nt),(rng mt):] c= Indices A9 holds
ex nt1 being Element of n -tuples_on NAT st
( rng nt1 = ((rng nt) \ {i}) \/ {j} & Segm (RLine A9,i,(Line A9,j)),nt,mt = Segm A9,nt1,mt )
let A9 be Matrix of n9,m9,D; :: thesis: for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st i in rng nt & [:(rng nt),(rng mt):] c= Indices A9 holds
ex nt1 being Element of n -tuples_on NAT st
( rng nt1 = ((rng nt) \ {i}) \/ {j} & Segm (RLine A9,i,(Line A9,j)),nt,mt = Segm A9,nt1,mt )
let nt be Element of n -tuples_on NAT ; :: thesis: for mt being Element of m -tuples_on NAT st i in rng nt & [:(rng nt),(rng mt):] c= Indices A9 holds
ex nt1 being Element of n -tuples_on NAT st
( rng nt1 = ((rng nt) \ {i}) \/ {j} & Segm (RLine A9,i,(Line A9,j)),nt,mt = Segm A9,nt1,mt )
let mt be Element of m -tuples_on NAT ; :: thesis: ( i in rng nt & [:(rng nt),(rng mt):] c= Indices A9 implies ex nt1 being Element of n -tuples_on NAT st
( rng nt1 = ((rng nt) \ {i}) \/ {j} & Segm (RLine A9,i,(Line A9,j)),nt,mt = Segm A9,nt1,mt ) )
assume that
A1: i in rng nt and
A2: [:(rng nt),(rng mt):] c= Indices A9 ; :: thesis: ex nt1 being Element of n -tuples_on NAT st
( rng nt1 = ((rng nt) \ {i}) \/ {j} & Segm (RLine A9,i,(Line A9,j)),nt,mt = Segm A9,nt1,mt )
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]

proof

let k be Nat; :: thesis: ( k in Seg n implies ex x being Element of NAT st S₁[k,x] )
assume k in Seg n ; :: thesis: ex x being Element of NAT st S₁[k,x]

per cases ( nt . k = i or nt . k <> i ) ;

suppose A4: nt . k = i ; :: thesis: ex x being Element of NAT st S₁[k,x]

reconsider J = j as Element of NAT by ORDINAL1:def 13;
take J ; :: thesis: S₁[k,J]
thus S₁[k,J] by A4; :: thesis: verum

end;

suppose A5: nt . k <> i ; :: thesis: ex x being Element of NAT st S₁[k,x]

reconsider ntk = nt . k as Element of NAT by ORDINAL1:def 13;
take ntk ; :: thesis: S₁[k,ntk]
thus S₁[k,ntk] by A5; :: thesis: verum

end;

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 13;
then len p = n by A6, FINSEQ_1:def 3;
then reconsider p9 = p as Element of n -tuples_on NAT by FINSEQ_2:110;
A8: rng p9 c= ((rng nt) \ {i}) \/ {j}

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng p9 or y in ((rng nt) \ {i}) \/ {j} )
A9: dom nt = Seg n by FINSEQ_2:144;
assume y in rng p9 ; :: thesis: y in ((rng nt) \ {i}) \/ {j}
then consider x being set such that
A10: x in dom p and
A11: p . x = y by FUNCT_1:def 5;
consider k being Element of NAT such that
A12: x = k and
1 <= k and
k <= n by A6, A10;
( nt . k = i or nt . k <> i ) ;
then ( ( 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 5;
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: verum

end;

take p9 ; :: thesis: ( rng p9 = ((rng nt) \ {i}) \/ {j} & Segm (RLine A9,i,(Line A9,j)),nt,mt = Segm A9,p9,mt )
((rng nt) \ {i}) \/ {j} c= rng p9

proof

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

per cases ( y in (rng nt) \ {i} or y in {j} ) by A13, XBOOLE_0:def 3;

suppose A14: y in (rng nt) \ {i} ; :: thesis: y in rng p9

then consider x being set such that
A15: x in dom nt and
A16: nt . x = y by FUNCT_1:def 5;
A17: dom nt = Seg n by FINSEQ_2:144;
then consider k being Element of NAT such that
A18: x = k and
1 <= k and
k <= n by A15;
not y in {i} by A14, XBOOLE_0:def 5;
then y <> i by TARSKI:def 1;
then p . k = y by A7, A15, A16, A17, A18;
hence y in rng p9 by A6, A15, A17, A18, FUNCT_1:def 5; :: thesis: verum

end;

suppose y in {j} ; :: thesis: y in rng p9

then A19: y = j by TARSKI:def 1;
consider x being set such that
A20: x in dom nt and
A21: nt . x = i by A1, FUNCT_1:def 5;
A22: dom nt = Seg n by FINSEQ_2:144;
then consider k being Element of 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 5; :: thesis: verum

end;

end;

end;

hence rng p9 = ((rng nt) \ {i}) \/ {j} by A8, XBOOLE_0:def 10; :: thesis: Segm (RLine A9,i,(Line A9,j)),nt,mt = Segm A9,p9,mt
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_1:27;
A25: len (Line A9,j) = width A9 by MATRIX_1:def 8;
A26: Indices (Segm A9,p9,mt) = Indices (Segm (RLine A9,i,(Line A9,j)),nt,mt) by MATRIX_1:27;

now

let k, l be Nat; :: thesis: ( [k,l] in Indices (Segm (RLine A9,i,(Line A9,j)),nt,mt) implies (Segm (RLine A9,i,(Line A9,j)),nt,mt) * k,l = (Segm A9,p9,mt) * k,l )
assume A27: [k,l] in Indices (Segm (RLine A9,i,(Line A9,j)),nt,mt) ; :: thesis: (Segm (RLine A9,i,(Line A9,j)),nt,mt) * k,l = (Segm A9,p9,mt) * k,l
reconsider K = k, L = l as Element of NAT by ORDINAL1:def 13;
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_1:26;
then A29: K in Seg n by A27, ZFMISC_1:106;
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:106;
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_1:def 8;
hence (Segm (RLine A9,i,(Line A9,j)),nt,mt) * k,l = (Segm A9,p9,mt) * k,l by A26, A27, Def1; :: thesis: verum

end;

hence Segm (RLine A9,i,(Line A9,j)),nt,mt = Segm A9,p9,mt by MATRIX_1:28; :: thesis: verum