let D be non empty set ; :: thesis: for i, j, m, n, m9, n9 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 i, j, m, n, m9, n9 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 S1[ 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 S1[k,x]
proof
let k be Nat; :: thesis: ( k in Seg n implies ex x being Element of NAT st S1[k,x] )
assume k in Seg n ; :: thesis: ex x being Element of NAT st S1[k,x]
per cases ( nt . k = i or nt . k <> i ) ;
suppose A4: nt . k = i ; :: thesis: ex x being Element of NAT st S1[k,x]
reconsider J = j as Element of NAT by ORDINAL1:def 12;
take J ; :: thesis: S1[k,J]
thus S1[k,J] by A4; :: thesis: verum
end;
suppose A5: nt . k <> i ; :: thesis: ex x being Element of NAT st S1[k,x]
reconsider ntk = nt . k as Element of NAT by ORDINAL1:def 12;
take ntk ; :: thesis: S1[k,ntk]
thus S1[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
S1[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}
proof
let y be object ; :: 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:124;
assume y in rng p9 ; :: thesis: y in ((rng nt) \ {i}) \/ {j}
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: 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 object ; :: 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 object such that
A15: x in dom nt and
A16: nt . x = y by FUNCT_1:def 3;
A17: dom nt = Seg n by FINSEQ_2:124;
then consider k being 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 3; :: thesis: verum
end;
suppose y in {j} ; :: thesis: y in rng p9
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: 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_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;
now :: thesis: for k, l being Nat st [k,l] in Indices (Segm ((RLine (A9,i,(Line (A9,j)))),nt,mt)) holds
(Segm ((RLine (A9,i,(Line (A9,j)))),nt,mt)) * (k,l) = (Segm (A9,p9,mt)) * (k,l)
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 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: verum
end;
hence Segm ((RLine (A9,i,(Line (A9,j)))),nt,mt) = Segm (A9,p9,mt) by MATRIX_0:27; :: thesis: verum