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

proof

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

end;

((rng nt) \ {i}) \/ {j} c= rng p'

proof

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

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

suppose A12: y in (rng nt) \ {i} ; :: thesis: y in rng p'

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

end;

suppose A16: y in {j} ; :: thesis: y in rng p'

consider x being set such that
A17: ( x in dom nt & nt . x = i ) by A1, FUNCT_1:def 5;
A18: dom nt = Seg n by FINSEQ_2:144;
then consider k being Element of NAT such that
A19: ( x = k & 1 <= k & k <= n ) by A17;
( p . k = j & y = j ) by A7, A16, A17, A18, A19, TARSKI:def 1;
hence y in rng p' by A6, A17, A18, A19, FUNCT_1:def 5; :: thesis: verum

end;

end;

end;

hence rng p' = ((rng nt) \ {i}) \/ {j} by A8, XBOOLE_0:def 10; :: thesis: Segm (RLine A',i,(Line A',j)),nt,mt = Segm A',p',mt
set LA = Line A',j;
set R = RLine A',i,(Line A',j);
set SR = Segm (RLine A',i,(Line A',j)),nt,mt;
set S = Segm A',p',mt;
A20: ( Indices A' = Indices (RLine A',i,(Line A',j)) & Indices (Segm A',p',mt) = Indices (Segm (RLine A',i,(Line A',j)),nt,mt) & len (Line A',j) = width A' ) by MATRIX_1:27, MATRIX_1:def 8;

now

let k, l be Nat; :: thesis: ( [k,l] in Indices (Segm (RLine A',i,(Line A',j)),nt,mt) implies (Segm (RLine A',i,(Line A',j)),nt,mt) * k,l = (Segm A',p',mt) * k,l )
assume A21: [k,l] in Indices (Segm (RLine A',i,(Line A',j)),nt,mt) ; :: thesis: (Segm (RLine A',i,(Line A',j)),nt,mt) * k,l = (Segm A',p',mt) * k,l
reconsider K = k, L = l as Element of NAT by ORDINAL1:def 13;
A22: ( [(nt . K),(mt . L)] in Indices A' & Indices A' = [:(dom A'),(Seg (width A')):] & (Segm (RLine A',i,(Line A',j)),nt,mt) * K,L = (RLine A',i,(Line A',j)) * (nt . K),(mt . L) & Indices (Segm (RLine A',i,(Line A',j)),nt,mt) = [:(Seg n),(Seg (width (Segm (RLine A',i,(Line A',j)),nt,mt))):] ) by A2, A20, A21, Def1, Th17, MATRIX_1:26;
then ( ( nt . K = i or nt . K <> i ) & K in Seg n & mt . L in Seg (width A') ) by A21, ZFMISC_1:106;
then ( ( (Segm (RLine A',i,(Line A',j)),nt,mt) * K,L = (Line A',j) . (mt . L) & p' . K = j & (Line A',j) . (mt . L) = A' * j,(mt . L) ) or ( (Segm (RLine A',i,(Line A',j)),nt,mt) * K,L = A' * (nt . K),(mt . L) & p' . K = nt . K ) ) by A7, A20, A22, MATRIX11:def 3, MATRIX_1:def 8;
hence (Segm (RLine A',i,(Line A',j)),nt,mt) * k,l = (Segm A',p',mt) * k,l by A20, A21, Def1; :: thesis: verum

end;

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