:: GOBOARD4 semantic presentation
begin
theorem Th1: :: GOBOARD4:1
for G being Go-board
for f1, f2 being FinSequence of (TOP-REAL 2) st 1 <= len f1 & 1 <= len f2 & f1 is_sequence_on G & f2 is_sequence_on G & f1 /. 1 in rng (Line (G,1)) & f1 /. (len f1) in rng (Line (G,(len G))) & f2 /. 1 in rng (Col (G,1)) & f2 /. (len f2) in rng (Col (G,(width G))) holds
rng f1 meets rng f2
proof
defpred S1[ Element of NAT ] means for G1 being Go-board
for g1, g2 being FinSequence of (TOP-REAL 2) st $1 = width G1 & $1 > 0 & 1 <= len g1 & 1 <= len g2 & g1 is_sequence_on G1 & g2 is_sequence_on G1 & g1 /. 1 in rng (Line (G1,1)) & g1 /. (len g1) in rng (Line (G1,(len G1))) & g2 /. 1 in rng (Col (G1,1)) & g2 /. (len g2) in rng (Col (G1,(width G1))) holds
(rng g1) /\ (rng g2) <> {} ;
let G be Go-board; ::_thesis: for f1, f2 being FinSequence of (TOP-REAL 2) st 1 <= len f1 & 1 <= len f2 & f1 is_sequence_on G & f2 is_sequence_on G & f1 /. 1 in rng (Line (G,1)) & f1 /. (len f1) in rng (Line (G,(len G))) & f2 /. 1 in rng (Col (G,1)) & f2 /. (len f2) in rng (Col (G,(width G))) holds
rng f1 meets rng f2
let f1, f2 be FinSequence of (TOP-REAL 2); ::_thesis: ( 1 <= len f1 & 1 <= len f2 & f1 is_sequence_on G & f2 is_sequence_on G & f1 /. 1 in rng (Line (G,1)) & f1 /. (len f1) in rng (Line (G,(len G))) & f2 /. 1 in rng (Col (G,1)) & f2 /. (len f2) in rng (Col (G,(width G))) implies rng f1 meets rng f2 )
A1: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; ::_thesis: S1[k + 1]
let G1 be Go-board; ::_thesis: for g1, g2 being FinSequence of (TOP-REAL 2) st k + 1 = width G1 & k + 1 > 0 & 1 <= len g1 & 1 <= len g2 & g1 is_sequence_on G1 & g2 is_sequence_on G1 & g1 /. 1 in rng (Line (G1,1)) & g1 /. (len g1) in rng (Line (G1,(len G1))) & g2 /. 1 in rng (Col (G1,1)) & g2 /. (len g2) in rng (Col (G1,(width G1))) holds
(rng g1) /\ (rng g2) <> {}
let g1, g2 be FinSequence of (TOP-REAL 2); ::_thesis: ( k + 1 = width G1 & k + 1 > 0 & 1 <= len g1 & 1 <= len g2 & g1 is_sequence_on G1 & g2 is_sequence_on G1 & g1 /. 1 in rng (Line (G1,1)) & g1 /. (len g1) in rng (Line (G1,(len G1))) & g2 /. 1 in rng (Col (G1,1)) & g2 /. (len g2) in rng (Col (G1,(width G1))) implies (rng g1) /\ (rng g2) <> {} )
assume that
A3: k + 1 = width G1 and
k + 1 > 0 and
A4: 1 <= len g1 and
A5: 1 <= len g2 and
A6: g1 is_sequence_on G1 and
A7: g2 is_sequence_on G1 and
A8: g1 /. 1 in rng (Line (G1,1)) and
A9: g1 /. (len g1) in rng (Line (G1,(len G1))) and
A10: g2 /. 1 in rng (Col (G1,1)) and
A11: g2 /. (len g2) in rng (Col (G1,(width G1))) ; ::_thesis: (rng g1) /\ (rng g2) <> {}
defpred S2[ Nat] means ( $1 in dom g2 & g2 /. $1 in rng (Col (G1,(width G1))) );
A12: ex m being Nat st S2[m]
proof
take n = len g2; ::_thesis: S2[n]
thus n in dom g2 by A5, FINSEQ_3:25; ::_thesis: g2 /. n in rng (Col (G1,(width G1)))
thus g2 /. n in rng (Col (G1,(width G1))) by A11; ::_thesis: verum
end;
consider m being Nat such that
A13: ( S2[m] & ( for i being Nat st S2[i] holds
m <= i ) ) from NAT_1:sch_5(A12);
reconsider m = m as Element of NAT by ORDINAL1:def_12;
set g = g2 | m;
A14: (g2 | m) /. 1 in rng (Col (G1,1)) by A10, A13, GOBOARD1:6;
A15: g2 | m is_sequence_on G1 by A7, GOBOARD1:22;
A16: m <= len g2 by A13, FINSEQ_3:25;
then A17: len (g2 | m) = m by FINSEQ_1:59;
A18: rng (g2 | m) c= rng g2
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (g2 | m) or x in rng g2 )
assume x in rng (g2 | m) ; ::_thesis: x in rng g2
then consider n being Element of NAT such that
A19: n in dom (g2 | m) and
A20: x = (g2 | m) /. n by PARTFUN2:2;
A21: n in Seg m by A17, A19, FINSEQ_1:def_3;
then A22: n in dom g2 by A13, FINSEQ_4:71;
x = g2 /. n by A13, A20, A21, FINSEQ_4:71;
hence x in rng g2 by A22, PARTFUN2:2; ::_thesis: verum
end;
reconsider L1 = Line (G1,1), Ll = Line (G1,(len G1)) as FinSequence of (TOP-REAL 2) ;
A23: dom g2 = Seg (len g2) by FINSEQ_1:def_3;
A24: dom (g2 | m) = Seg (len (g2 | m)) by FINSEQ_1:def_3;
0 <> len G1 by GOBOARD1:def_3;
then A25: 0 + 1 <= len G1 by NAT_1:14;
then A26: 1 in dom G1 by FINSEQ_3:25;
A27: len G1 in dom G1 by A25, FINSEQ_3:25;
A28: (g2 | m) /. (len (g2 | m)) in rng (Col (G1,(width G1))) by A13, GOBOARD1:7;
defpred S3[ Nat] means ( $1 in dom G1 & (rng (g2 | m)) /\ (rng (Line (G1,$1))) <> {} );
A29: for n being Nat st S3[n] holds
n <= len G1 by FINSEQ_3:25;
0 <> width G1 by GOBOARD1:def_3;
then A30: 0 + 1 <= width G1 by NAT_1:14;
then A31: 1 in Seg (width G1) by FINSEQ_1:1;
A32: 1 <= len (g2 | m) by A13, GOBOARD1:22;
then A33: 1 in dom (g2 | m) by FINSEQ_3:25;
A34: ex n being Nat st S3[n]
proof
consider i being Nat such that
A35: i in dom (Col (G1,1)) and
A36: (g2 | m) /. 1 = (Col (G1,1)) . i by A10, A13, FINSEQ_2:10, GOBOARD1:6;
reconsider i = i as Element of NAT by ORDINAL1:def_12;
take i ; ::_thesis: S3[i]
i in Seg (len (Col (G1,1))) by A35, FINSEQ_1:def_3;
then i in Seg (len G1) by MATRIX_1:def_8;
hence i in dom G1 by FINSEQ_1:def_3; ::_thesis: (rng (g2 | m)) /\ (rng (Line (G1,i))) <> {}
then A37: (g2 | m) /. 1 = (Line (G1,i)) . 1 by A31, A36, GOBOARD1:2;
A38: (g2 | m) /. 1 in rng (g2 | m) by A33, PARTFUN2:2;
len (Line (G1,i)) = width G1 by MATRIX_1:def_7;
then dom (Line (G1,i)) = Seg (width G1) by FINSEQ_1:def_3;
then (g2 | m) /. 1 in rng (Line (G1,i)) by A31, A37, FUNCT_1:def_3;
hence (rng (g2 | m)) /\ (rng (Line (G1,i))) <> {} by A38, XBOOLE_0:def_4; ::_thesis: verum
end;
consider mi being Nat such that
A39: ( S3[mi] & ( for n being Nat st S3[n] holds
mi <= n ) ) from NAT_1:sch_5(A34);
A40: ex n being Nat st S3[n] by A34;
consider ma being Nat such that
A41: ( S3[ma] & ( for n being Nat st S3[n] holds
n <= ma ) ) from NAT_1:sch_6(A29, A40);
reconsider mi = mi, ma = ma as Element of NAT by ORDINAL1:def_12;
A42: 1 <= mi by A39, FINSEQ_3:25;
reconsider Lmi = Line (G1,mi) as FinSequence of (TOP-REAL 2) ;
defpred S4[ Nat] means ( $1 in dom g1 & g1 /. $1 in rng (Line (G1,mi)) );
A43: for n being Nat st S4[n] holds
n <= len g1 by FINSEQ_3:25;
A44: mi <= len G1 by A39, FINSEQ_3:25;
then ex n being Element of NAT st S4[n] by A4, A6, A8, A9, A42, GOBOARD1:29;
then A45: ex n being Nat st S4[n] ;
consider ma1 being Nat such that
A46: ( S4[ma1] & ( for n being Nat st S4[n] holds
n <= ma1 ) ) from NAT_1:sch_6(A43, A45);
A47: ma <= len G1 by A41, FINSEQ_3:25;
1 <= mi by A39, FINSEQ_3:25;
then reconsider l1 = mi - 1, l2 = (len G1) - ma as Element of NAT by A47, INT_1:5;
A48: ma <= len G1 by A41, FINSEQ_3:25;
A49: for n being Element of NAT st S4[n] holds
n <= ma1 by A46;
reconsider ma1 = ma1 as Element of NAT by ORDINAL1:def_12;
consider k1 being Element of NAT such that
A50: k1 in dom Lmi and
A51: g1 /. ma1 = Lmi /. k1 by A46, PARTFUN2:2;
Seg (len Lmi) = dom Lmi by FINSEQ_1:def_3;
then A52: k1 in Seg (width G1) by A50, MATRIX_1:def_7;
A53: dom G1 = Seg (len G1) by FINSEQ_1:def_3;
A54: ( mi = ma implies (rng g1) /\ (rng g2) <> {} )
proof
consider n being Element of NAT such that
A55: n in dom g1 and
A56: g1 /. n in rng (Line (G1,mi)) by A4, A6, A8, A9, A42, A44, GOBOARD1:29;
consider i being Element of NAT such that
A57: i in dom (Line (G1,mi)) and
A58: g1 /. n = Lmi /. i by A56, PARTFUN2:2;
A59: 1 <= i by A57, FINSEQ_3:25;
A60: len (Line (G1,mi)) = width G1 by MATRIX_1:def_7;
then i <= width G1 by A57, FINSEQ_3:25;
then consider m being Element of NAT such that
A61: m in dom (g2 | m) and
A62: (g2 | m) /. m in rng (Col (G1,i)) by A32, A15, A14, A28, A59, GOBOARD1:33;
A63: (g2 | m) /. m in rng (g2 | m) by A61, PARTFUN2:2;
reconsider Ci = Col (G1,i) as FinSequence of (TOP-REAL 2) ;
A64: len (Col (G1,i)) = len G1 by MATRIX_1:def_8;
then A65: dom (Col (G1,i)) = Seg (len G1) by FINSEQ_1:def_3
.= dom G1 by FINSEQ_1:def_3 ;
assume A66: mi = ma ; ::_thesis: (rng g1) /\ (rng g2) <> {}
A67: dom (Line (G1,mi)) = Seg (len (Line (G1,mi))) by FINSEQ_1:def_3;
consider j being Element of NAT such that
A68: j in dom Ci and
A69: (g2 | m) /. m = Ci /. j by A62, PARTFUN2:2;
reconsider Lj = Line (G1,j) as FinSequence of (TOP-REAL 2) ;
len (Line (G1,mi)) = width G1 by MATRIX_1:def_7
.= len Lj by MATRIX_1:def_7 ;
then A70: dom (Line (G1,mi)) = dom Lj by A67, FINSEQ_1:def_3;
A71: (g2 | m) /. m = Ci . j by A68, A69, PARTFUN1:def_6
.= Lj . i by A57, A67, A60, A65, A68, GOBOARD1:2
.= Lj /. i by A57, A70, PARTFUN1:def_6 ;
len Lj = width G1 by MATRIX_1:def_7;
then i in dom Lj by A57, A67, A60, FINSEQ_1:def_3;
then (g2 | m) /. m in rng Lj by A71, PARTFUN2:2;
then A72: ( dom Ci = Seg (len Ci) & (rng (g2 | m)) /\ (rng (Line (G1,j))) <> {} ) by A63, FINSEQ_1:def_3, XBOOLE_0:def_4;
A73: now__::_thesis:_not_j_<>_mi
assume j <> mi ; ::_thesis: contradiction
then ( j < mi or j > mi ) by XXREAL_0:1;
hence contradiction by A39, A53, A41, A66, A64, A68, A72; ::_thesis: verum
end;
g1 /. n in rng g1 by A55, PARTFUN2:2;
hence (rng g1) /\ (rng g2) <> {} by A18, A58, A63, A71, A73, XBOOLE_0:def_4; ::_thesis: verum
end;
A74: width G1 in Seg (width G1) by A30, FINSEQ_1:1;
deffunc H1( Nat) -> Element of the U1 of (TOP-REAL 2) = G1 * ($1,k1);
reconsider Ck1 = Col (G1,k1) as FinSequence of (TOP-REAL 2) ;
consider h1 being FinSequence of (TOP-REAL 2) such that
A75: ( len h1 = l1 & ( for n being Nat st n in dom h1 holds
h1 /. n = H1(n) ) ) from FINSEQ_4:sch_2();
A76: dom g1 = Seg (len g1) by FINSEQ_1:def_3;
now__::_thesis:_(rng_g1)_/\_(rng_g2)_<>_{}
percases ( k = 0 or k <> 0 ) ;
supposeA77: k = 0 ; ::_thesis: (rng g1) /\ (rng g2) <> {}
reconsider c1 = Col (G1,1) as FinSequence of (TOP-REAL 2) ;
consider x being Element of NAT such that
A78: x in dom c1 and
A79: g2 /. 1 = c1 /. x by A10, PARTFUN2:2;
reconsider lx = Line (G1,x) as FinSequence of (TOP-REAL 2) ;
A80: 1 <= x by A78, FINSEQ_3:25;
A81: len c1 = len G1 by MATRIX_1:def_8;
then x <= len G1 by A78, FINSEQ_3:25;
then consider m being Element of NAT such that
A82: m in dom g1 and
A83: g1 /. m in rng lx by A4, A6, A8, A9, A80, GOBOARD1:29;
A84: g1 /. m in rng g1 by A82, PARTFUN2:2;
Seg (len c1) = dom c1 by FINSEQ_1:def_3;
then A85: x in dom G1 by A78, A81, FINSEQ_1:def_3;
A86: c1 /. x = c1 . x by A78, PARTFUN1:def_6;
consider y being Element of NAT such that
A87: y in dom lx and
A88: lx /. y = g1 /. m by A83, PARTFUN2:2;
( Seg (len lx) = dom lx & len lx = width G1 ) by FINSEQ_1:def_3, MATRIX_1:def_7;
then A89: y = 1 by A3, A77, A87, FINSEQ_1:2, TARSKI:def_1;
0 <> width G1 by GOBOARD1:def_3;
then 0 + 1 <= width G1 by NAT_1:14;
then A90: 1 in Seg (width G1) by FINSEQ_1:1;
1 in dom g2 by A5, FINSEQ_3:25;
then A91: g2 /. 1 in rng g2 by PARTFUN2:2;
lx /. y = lx . y by A87, PARTFUN1:def_6;
then g1 /. m = g2 /. 1 by A79, A90, A85, A88, A86, A89, GOBOARD1:2;
hence (rng g1) /\ (rng g2) <> {} by A84, A91, XBOOLE_0:def_4; ::_thesis: verum
end;
supposeA92: k <> 0 ; ::_thesis: (rng g1) /\ (rng g2) <> {}
then A93: 0 < k by NAT_1:3;
now__::_thesis:_(rng_g1)_/\_(rng_g2)_<>_{}
percases ( mi = ma or mi <> ma ) ;
suppose mi = ma ; ::_thesis: (rng g1) /\ (rng g2) <> {}
hence (rng g1) /\ (rng g2) <> {} by A54; ::_thesis: verum
end;
supposeA94: mi <> ma ; ::_thesis: (rng g1) /\ (rng g2) <> {}
1 <= ma1 by A46, FINSEQ_3:25;
then reconsider w = ma1 - 1 as Element of NAT by INT_1:5;
reconsider Lma = Line (G1,ma) as FinSequence of (TOP-REAL 2) ;
A95: Indices G1 = [:(dom G1),(Seg (width G1)):] by MATRIX_1:def_4;
A96: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_h1_holds_
n_in_dom_G1
let n be Element of NAT ; ::_thesis: ( n in dom h1 implies n in dom G1 )
A97: l1 <= mi by XREAL_1:43;
assume A98: n in dom h1 ; ::_thesis: n in dom G1
then A99: 1 <= n by FINSEQ_3:25;
n <= l1 by A75, A98, FINSEQ_3:25;
then A100: n <= mi by A97, XXREAL_0:2;
mi <= len G1 by A39, FINSEQ_3:25;
then n <= len G1 by A100, XXREAL_0:2;
hence n in dom G1 by A99, FINSEQ_3:25; ::_thesis: verum
end;
A101: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_h1_&_n_+_1_in_dom_h1_holds_
for_i1,_i2,_j1,_j2_being_Element_of_NAT_st_[i1,i2]_in_Indices_G1_&_[j1,j2]_in_Indices_G1_&_h1_/._n_=_G1_*_(i1,i2)_&_h1_/._(n_+_1)_=_G1_*_(j1,j2)_holds_
(abs_(i1_-_j1))_+_(abs_(i2_-_j2))_=_1
let n be Element of NAT ; ::_thesis: ( n in dom h1 & n + 1 in dom h1 implies for i1, i2, j1, j2 being Element of NAT st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & h1 /. n = G1 * (i1,i2) & h1 /. (n + 1) = G1 * (j1,j2) holds
(abs (i1 - j1)) + (abs (i2 - j2)) = 1 )
assume that
A102: n in dom h1 and
A103: n + 1 in dom h1 ; ::_thesis: for i1, i2, j1, j2 being Element of NAT st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & h1 /. n = G1 * (i1,i2) & h1 /. (n + 1) = G1 * (j1,j2) holds
(abs (i1 - j1)) + (abs (i2 - j2)) = 1
n + 1 in dom G1 by A96, A103;
then A104: [(n + 1),k1] in Indices G1 by A52, A95, ZFMISC_1:87;
let i1, i2, j1, j2 be Element of NAT ; ::_thesis: ( [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & h1 /. n = G1 * (i1,i2) & h1 /. (n + 1) = G1 * (j1,j2) implies (abs (i1 - j1)) + (abs (i2 - j2)) = 1 )
assume that
A105: [i1,i2] in Indices G1 and
A106: [j1,j2] in Indices G1 and
A107: h1 /. n = G1 * (i1,i2) and
A108: h1 /. (n + 1) = G1 * (j1,j2) ; ::_thesis: (abs (i1 - j1)) + (abs (i2 - j2)) = 1
h1 /. (n + 1) = G1 * ((n + 1),k1) by A75, A103;
then A109: ( j1 = n + 1 & j2 = k1 ) by A104, A106, A108, GOBOARD1:5;
n in dom G1 by A96, A102;
then A110: [n,k1] in Indices G1 by A52, A95, ZFMISC_1:87;
h1 /. n = G1 * (n,k1) by A75, A102;
then ( i1 = n & i2 = k1 ) by A110, A105, A107, GOBOARD1:5;
hence (abs (i1 - j1)) + (abs (i2 - j2)) = (abs ((n - n) + (- 1))) + 0 by A109, ABSVALUE:2
.= abs 1 by COMPLEX1:52
.= 1 by ABSVALUE:def_1 ;
::_thesis: verum
end;
A111: (rng h1) /\ (rng (g2 | m)) = {}
proof
set x = the Element of (rng h1) /\ (rng (g2 | m));
assume A112: not (rng h1) /\ (rng (g2 | m)) = {} ; ::_thesis: contradiction
then the Element of (rng h1) /\ (rng (g2 | m)) in rng h1 by XBOOLE_0:def_4;
then consider n1 being Element of NAT such that
A113: n1 in dom h1 and
A114: the Element of (rng h1) /\ (rng (g2 | m)) = h1 /. n1 by PARTFUN2:2;
A115: n1 <= l1 by A75, A113, FINSEQ_3:25;
n1 in dom G1 by A96, A113;
then A116: [n1,k1] in Indices G1 by A52, A95, ZFMISC_1:87;
the Element of (rng h1) /\ (rng (g2 | m)) in rng (g2 | m) by A112, XBOOLE_0:def_4;
then consider n2 being Element of NAT such that
A117: n2 in dom (g2 | m) and
A118: the Element of (rng h1) /\ (rng (g2 | m)) = (g2 | m) /. n2 by PARTFUN2:2;
A119: (g2 | m) /. n2 in rng (g2 | m) by A117, PARTFUN2:2;
consider i1, i2 being Element of NAT such that
A120: [i1,i2] in Indices G1 and
A121: (g2 | m) /. n2 = G1 * (i1,i2) by A15, A117, GOBOARD1:def_9;
reconsider L = Line (G1,i1) as FinSequence of (TOP-REAL 2) ;
A122: i2 in Seg (width G1) by A95, A120, ZFMISC_1:87;
A123: ( Seg (len L) = dom L & len L = width G1 ) by FINSEQ_1:def_3, MATRIX_1:def_7;
then L /. i2 = L . i2 by A122, PARTFUN1:def_6;
then (g2 | m) /. n2 = L /. i2 by A121, A122, MATRIX_1:def_7;
then (g2 | m) /. n2 in rng L by A122, A123, PARTFUN2:2;
then A124: (rng (g2 | m)) /\ (rng L) <> {} by A119, XBOOLE_0:def_4;
i1 in dom G1 by A95, A120, ZFMISC_1:87;
then A125: mi <= i1 by A39, A124;
the Element of (rng h1) /\ (rng (g2 | m)) = G1 * (n1,k1) by A75, A113, A114;
then i1 = n1 by A118, A120, A121, A116, GOBOARD1:5;
then mi <= mi - 1 by A115, A125, XXREAL_0:2;
hence contradiction by XREAL_1:44; ::_thesis: verum
end;
defpred S5[ Nat] means ( $1 in dom g1 & ma1 < $1 & g1 /. $1 in rng (Line (G1,ma)) );
A126: mi <= ma by A39, A41;
then A127: mi < ma by A94, XXREAL_0:1;
then ex n being Element of NAT st S5[n] by A6, A9, A39, A48, A46, GOBOARD1:37;
then A128: ex n being Nat st S5[n] ;
consider mi1 being Nat such that
A129: ( S5[mi1] & ( for n being Nat st S5[n] holds
mi1 <= n ) ) from NAT_1:sch_5(A128);
consider k2 being Element of NAT such that
A130: k2 in dom Lma and
A131: g1 /. mi1 = Lma /. k2 by A129, PARTFUN2:2;
deffunc H2( Nat) -> Element of the U1 of (TOP-REAL 2) = G1 * ((ma + $1),k2);
consider h2 being FinSequence of (TOP-REAL 2) such that
A132: ( len h2 = l2 & ( for n being Nat st n in dom h2 holds
h2 /. n = H2(n) ) ) from FINSEQ_4:sch_2();
reconsider Ck2 = Col (G1,k2) as FinSequence of (TOP-REAL 2) ;
dom Lma = Seg (len Lma) by FINSEQ_1:def_3;
then A133: k2 in Seg (width G1) by A130, MATRIX_1:def_7;
A134: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_h2_holds_
ma_+_n_in_dom_G1
let n be Element of NAT ; ::_thesis: ( n in dom h2 implies ma + n in dom G1 )
A135: n <= n + ma by NAT_1:11;
assume A136: n in dom h2 ; ::_thesis: ma + n in dom G1
then n <= l2 by A132, FINSEQ_3:25;
then A137: ma + n <= ma + l2 by XREAL_1:7;
1 <= n by A136, FINSEQ_3:25;
then 1 <= n + ma by A135, XXREAL_0:2;
hence ma + n in dom G1 by A137, FINSEQ_3:25; ::_thesis: verum
end;
A138: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_h2_holds_
ex_m_being_Element_of_NAT_ex_k2_being_Element_of_NAT_st_
(_[m,k2]_in_Indices_G1_&_h2_/._n_=_G1_*_(m,k2)_)
let n be Element of NAT ; ::_thesis: ( n in dom h2 implies ex m being Element of NAT ex k2 being Element of NAT st
( [m,k2] in Indices G1 & h2 /. n = G1 * (m,k2) ) )
assume A139: n in dom h2 ; ::_thesis: ex m being Element of NAT ex k2 being Element of NAT st
( [m,k2] in Indices G1 & h2 /. n = G1 * (m,k2) )
take m = ma + n; ::_thesis: ex k2 being Element of NAT st
( [m,k2] in Indices G1 & h2 /. n = G1 * (m,k2) )
take k2 = k2; ::_thesis: ( [m,k2] in Indices G1 & h2 /. n = G1 * (m,k2) )
ma + n in dom G1 by A134, A139;
hence ( [m,k2] in Indices G1 & h2 /. n = G1 * (m,k2) ) by A133, A132, A95, A139, ZFMISC_1:87; ::_thesis: verum
end;
A140: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_h2_&_n_+_1_in_dom_h2_holds_
for_i1,_i2,_j1,_j2_being_Element_of_NAT_st_[i1,i2]_in_Indices_G1_&_[j1,j2]_in_Indices_G1_&_h2_/._n_=_G1_*_(i1,i2)_&_h2_/._(n_+_1)_=_G1_*_(j1,j2)_holds_
(abs_(i1_-_j1))_+_(abs_(i2_-_j2))_=_1
let n be Element of NAT ; ::_thesis: ( n in dom h2 & n + 1 in dom h2 implies for i1, i2, j1, j2 being Element of NAT st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & h2 /. n = G1 * (i1,i2) & h2 /. (n + 1) = G1 * (j1,j2) holds
(abs (i1 - j1)) + (abs (i2 - j2)) = 1 )
assume that
A141: n in dom h2 and
A142: n + 1 in dom h2 ; ::_thesis: for i1, i2, j1, j2 being Element of NAT st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & h2 /. n = G1 * (i1,i2) & h2 /. (n + 1) = G1 * (j1,j2) holds
(abs (i1 - j1)) + (abs (i2 - j2)) = 1
ma + (n + 1) in dom G1 by A134, A142;
then A143: [((ma + n) + 1),k2] in Indices G1 by A133, A95, ZFMISC_1:87;
let i1, i2, j1, j2 be Element of NAT ; ::_thesis: ( [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & h2 /. n = G1 * (i1,i2) & h2 /. (n + 1) = G1 * (j1,j2) implies (abs (i1 - j1)) + (abs (i2 - j2)) = 1 )
assume that
A144: [i1,i2] in Indices G1 and
A145: [j1,j2] in Indices G1 and
A146: h2 /. n = G1 * (i1,i2) and
A147: h2 /. (n + 1) = G1 * (j1,j2) ; ::_thesis: (abs (i1 - j1)) + (abs (i2 - j2)) = 1
h2 /. (n + 1) = G1 * ((ma + (n + 1)),k2) by A132, A142;
then A148: ( j1 = (ma + n) + 1 & j2 = k2 ) by A143, A145, A147, GOBOARD1:5;
ma + n in dom G1 by A134, A141;
then A149: [(ma + n),k2] in Indices G1 by A133, A95, ZFMISC_1:87;
h2 /. n = G1 * ((ma + n),k2) by A132, A141;
then ( i1 = ma + n & i2 = k2 ) by A149, A144, A146, GOBOARD1:5;
hence (abs (i1 - j1)) + (abs (i2 - j2)) = (abs (((ma + n) - (ma + n)) + (- 1))) + 0 by A148, ABSVALUE:2
.= abs 1 by COMPLEX1:52
.= 1 by ABSVALUE:def_1 ;
::_thesis: verum
end;
A150: mi1 <= mi1 + 1 by NAT_1:11;
A151: 0 + 1 < width G1 by A3, A93, XREAL_1:6;
then A152: len (DelCol (G1,(width G1))) = len G1 by A74, GOBOARD1:def_8;
ma1 <= mi1 by A129;
then reconsider l = (mi1 + 1) - ma1 as Element of NAT by A150, INT_1:5, XXREAL_0:2;
set f1 = g1 | mi1;
defpred S6[ Nat, Element of (TOP-REAL 2)] means $2 = (g1 | mi1) /. (w + $1);
A153: for n being Nat st n in Seg l holds
ex p being Point of (TOP-REAL 2) st S6[n,p] ;
consider f being FinSequence of (TOP-REAL 2) such that
A154: ( len f = l & ( for n being Nat st n in Seg l holds
S6[n,f /. n] ) ) from FINSEQ_4:sch_1(A153);
A155: w + l = mi1 ;
A156: dom f = Seg l by A154, FINSEQ_1:def_3;
set ff = (h1 ^ f) ^ h2;
ma1 + 1 <= mi1 by A129, NAT_1:13;
then ma1 + 1 <= mi1 + 1 by NAT_1:13;
then A157: 1 <= l by XREAL_1:19;
A158: now__::_thesis:_((h1_^_f)_^_h2)_/._1_in_rng_(Line_(G1,1))
percases ( mi = 1 or mi <> 1 ) ;
supposeA159: mi = 1 ; ::_thesis: ((h1 ^ f) ^ h2) /. 1 in rng (Line (G1,1))
1 <= ma1 by A76, A46, FINSEQ_1:1;
then A160: ma1 in Seg mi1 by A129, FINSEQ_1:1;
A161: w + 1 = ma1 ;
A162: 1 in Seg l by A157, FINSEQ_1:1;
h1 = {} by A75, A159;
then (h1 ^ f) ^ h2 = f ^ h2 by FINSEQ_1:34;
then ((h1 ^ f) ^ h2) /. 1 = f /. 1 by A156, A162, FINSEQ_4:68
.= (g1 | mi1) /. ma1 by A154, A162, A161
.= g1 /. ma1 by A129, A160, FINSEQ_4:71 ;
hence ((h1 ^ f) ^ h2) /. 1 in rng (Line (G1,1)) by A46, A159; ::_thesis: verum
end;
supposeA163: mi <> 1 ; ::_thesis: ((h1 ^ f) ^ h2) /. 1 in rng (Line (G1,1))
1 <= mi by A39, FINSEQ_3:25;
then 1 < mi by A163, XXREAL_0:1;
then 1 + 1 <= mi by NAT_1:13;
then A164: 1 <= l1 by XREAL_1:19;
then A165: 1 in dom h1 by A75, FINSEQ_3:25;
A166: len (Line (G1,1)) = width G1 by MATRIX_1:def_7;
then A167: k1 in dom L1 by A52, FINSEQ_1:def_3;
dom (Line (G1,1)) = Seg (width G1) by A166, FINSEQ_1:def_3;
then A168: L1 /. k1 = L1 . k1 by A52, PARTFUN1:def_6;
( len (h1 ^ f) = (len h1) + (len f) & 0 <= len f ) by FINSEQ_1:22, NAT_1:2;
then 0 + 1 <= len (h1 ^ f) by A75, A164, XREAL_1:7;
then 1 in dom (h1 ^ f) by FINSEQ_3:25;
then ((h1 ^ f) ^ h2) /. 1 = (h1 ^ f) /. 1 by FINSEQ_4:68
.= h1 /. 1 by A165, FINSEQ_4:68
.= G1 * (1,k1) by A75, A165
.= L1 /. k1 by A52, A168, MATRIX_1:def_7 ;
hence ((h1 ^ f) ^ h2) /. 1 in rng (Line (G1,1)) by A167, PARTFUN2:2; ::_thesis: verum
end;
end;
end;
A169: for n being Element of NAT st n in Seg l holds
( (g1 | mi1) /. (w + n) = g1 /. (w + n) & w + n in dom g1 )
proof
0 + 1 <= ma1 by A46, FINSEQ_3:25;
then A170: 0 <= ma1 - 1 by XREAL_1:19;
let n be Element of NAT ; ::_thesis: ( n in Seg l implies ( (g1 | mi1) /. (w + n) = g1 /. (w + n) & w + n in dom g1 ) )
assume A171: n in Seg l ; ::_thesis: ( (g1 | mi1) /. (w + n) = g1 /. (w + n) & w + n in dom g1 )
n <= l by A171, FINSEQ_1:1;
then n + ma1 <= l + ma1 by XREAL_1:7;
then A172: (n + ma1) - 1 <= mi1 by XREAL_1:20;
1 <= n by A171, FINSEQ_1:1;
then 0 + 1 <= (ma1 - 1) + n by A170, XREAL_1:7;
then w + n in Seg mi1 by A172, FINSEQ_1:1;
hence ( (g1 | mi1) /. (w + n) = g1 /. (w + n) & w + n in dom g1 ) by A129, FINSEQ_4:71; ::_thesis: verum
end;
A173: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_f_holds_
ex_i,_j_being_Element_of_NAT_st_
(_[i,j]_in_Indices_G1_&_f_/._n_=_G1_*_(i,j)_)
let n be Element of NAT ; ::_thesis: ( n in dom f implies ex i, j being Element of NAT st
( [i,j] in Indices G1 & f /. n = G1 * (i,j) ) )
assume A174: n in dom f ; ::_thesis: ex i, j being Element of NAT st
( [i,j] in Indices G1 & f /. n = G1 * (i,j) )
then w + n in dom g1 by A169, A156;
then consider i, j being Element of NAT such that
A175: ( [i,j] in Indices G1 & g1 /. (w + n) = G1 * (i,j) ) by A6, GOBOARD1:def_9;
take i = i; ::_thesis: ex j being Element of NAT st
( [i,j] in Indices G1 & f /. n = G1 * (i,j) )
take j = j; ::_thesis: ( [i,j] in Indices G1 & f /. n = G1 * (i,j) )
f /. n = (g1 | mi1) /. (w + n) by A154, A156, A174;
hence ( [i,j] in Indices G1 & f /. n = G1 * (i,j) ) by A169, A156, A174, A175; ::_thesis: verum
end;
A176: Seg (len f) = dom f by FINSEQ_1:def_3;
A177: rng f c= rng g1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in rng g1 )
assume x in rng f ; ::_thesis: x in rng g1
then consider n being Element of NAT such that
A178: n in dom f and
A179: x = f /. n by PARTFUN2:2;
f /. n = (g1 | mi1) /. (w + n) by A154, A176, A178;
then A180: f /. n = g1 /. (w + n) by A169, A154, A176, A178;
w + n in dom g1 by A169, A154, A176, A178;
hence x in rng g1 by A179, A180, PARTFUN2:2; ::_thesis: verum
end;
A181: dom h2 = Seg (len h2) by FINSEQ_1:def_3;
A182: now__::_thesis:_((h1_^_f)_^_h2)_/._(len_((h1_^_f)_^_h2))_in_rng_(Line_(G1,(len_G1)))
percases ( ma = len G1 or ma <> len G1 ) ;
supposeA183: ma = len G1 ; ::_thesis: ((h1 ^ f) ^ h2) /. (len ((h1 ^ f) ^ h2)) in rng (Line (G1,(len G1)))
1 <= mi1 by A129, FINSEQ_3:25;
then A184: mi1 in Seg mi1 by FINSEQ_1:1;
A185: len f in dom f by A154, A176, A157, FINSEQ_1:1;
h2 = {} by A132, A183;
then A186: (h1 ^ f) ^ h2 = h1 ^ f by FINSEQ_1:34;
then ((h1 ^ f) ^ h2) /. (len ((h1 ^ f) ^ h2)) = ((h1 ^ f) ^ h2) /. ((len h1) + (len f)) by FINSEQ_1:22
.= f /. l by A154, A186, A185, FINSEQ_4:69
.= (g1 | mi1) /. mi1 by A154, A156, A155, A185
.= g1 /. mi1 by A129, A184, FINSEQ_4:71 ;
hence ((h1 ^ f) ^ h2) /. (len ((h1 ^ f) ^ h2)) in rng (Line (G1,(len G1))) by A129, A183; ::_thesis: verum
end;
supposeA187: ma <> len G1 ; ::_thesis: ((h1 ^ f) ^ h2) /. (len ((h1 ^ f) ^ h2)) in rng (Line (G1,(len G1)))
ma <= len G1 by A41, FINSEQ_3:25;
then ma < len G1 by A187, XXREAL_0:1;
then ma + 1 <= len G1 by NAT_1:13;
then A188: 1 <= l2 by XREAL_1:19;
then A189: l2 in Seg l2 by FINSEQ_1:1;
A190: len h2 in dom h2 by A132, A188, FINSEQ_3:25;
A191: len (Line (G1,(len G1))) = width G1 by MATRIX_1:def_7;
then A192: k2 in dom Ll by A133, FINSEQ_1:def_3;
k2 in dom Ll by A133, A191, FINSEQ_1:def_3;
then A193: Ll /. k2 = Ll . k2 by PARTFUN1:def_6;
((h1 ^ f) ^ h2) /. (len ((h1 ^ f) ^ h2)) = ((h1 ^ f) ^ h2) /. ((len (h1 ^ f)) + (len h2)) by FINSEQ_1:22
.= h2 /. l2 by A132, A190, FINSEQ_4:69
.= G1 * ((ma + l2),k2) by A132, A181, A189
.= Ll /. k2 by A133, A193, MATRIX_1:def_7 ;
hence ((h1 ^ f) ^ h2) /. (len ((h1 ^ f) ^ h2)) in rng (Line (G1,(len G1))) by A192, PARTFUN2:2; ::_thesis: verum
end;
end;
end;
0 + 0 <= (len h1) + (len h2) by NAT_1:2;
then A194: 0 + 1 <= (len f) + ((len h1) + (len h2)) by A154, A157, XREAL_1:7;
A195: rng ((h1 ^ f) ^ h2) = (rng (h1 ^ f)) \/ (rng h2) by FINSEQ_1:31
.= ((rng h1) \/ (rng f)) \/ (rng h2) by FINSEQ_1:31 ;
A196: for k being Element of NAT st k in Seg (width G1) & (rng f) /\ (rng (Col (G1,k))) = {} holds
(rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) = {}
proof
A197: len (Col (G1,k2)) = len G1 by MATRIX_1:def_8;
A198: len (Col (G1,k1)) = len G1 by MATRIX_1:def_8;
A199: w + 1 = ma1 ;
let k be Element of NAT ; ::_thesis: ( k in Seg (width G1) & (rng f) /\ (rng (Col (G1,k))) = {} implies (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) = {} )
assume that
A200: k in Seg (width G1) and
A201: (rng f) /\ (rng (Col (G1,k))) = {} ; ::_thesis: (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) = {}
set gg = Col (G1,k);
assume A202: (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) <> {} ; ::_thesis: contradiction
set x = the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k)));
rng ((h1 ^ f) ^ h2) = (rng f) \/ ((rng h1) \/ (rng h2)) by A195, XBOOLE_1:4;
then A203: (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) = {} \/ (((rng h1) \/ (rng h2)) /\ (rng (Col (G1,k)))) by A201, XBOOLE_1:23
.= ((rng h1) /\ (rng (Col (G1,k)))) \/ ((rng h2) /\ (rng (Col (G1,k)))) by XBOOLE_1:23 ;
now__::_thesis:_contradiction
percases ( the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) in (rng h1) /\ (rng (Col (G1,k))) or the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) in (rng h2) /\ (rng (Col (G1,k))) ) by A202, A203, XBOOLE_0:def_3;
supposeA204: the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) in (rng h1) /\ (rng (Col (G1,k))) ; ::_thesis: contradiction
then the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) in rng h1 by XBOOLE_0:def_4;
then consider i being Element of NAT such that
A205: i in dom h1 and
A206: the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) = h1 /. i by PARTFUN2:2;
A207: the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) = G1 * (i,k1) by A75, A205, A206;
reconsider y = the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) as Point of (TOP-REAL 2) by A206;
A208: Lmi /. k1 = Lmi . k1 by A50, PARTFUN1:def_6;
A209: the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) in rng (Col (G1,k)) by A204, XBOOLE_0:def_4;
A210: dom (Col (G1,k1)) = Seg (len G1) by A198, FINSEQ_1:def_3
.= dom G1 by FINSEQ_1:def_3 ;
then A211: Ck1 /. mi = Ck1 . mi by A39, PARTFUN1:def_6;
A212: i in dom Ck1 by A96, A205, A210;
Ck1 /. i = Ck1 . i by A96, A205, A210, PARTFUN1:def_6;
then y = Ck1 /. i by A207, A210, A212, MATRIX_1:def_8;
then y in rng Ck1 by A212, PARTFUN2:2;
then A213: k1 = k by A52, A200, A209, GOBOARD1:4;
A214: 1 in Seg l by A157, FINSEQ_1:1;
then ( f /. 1 = (g1 | mi1) /. ma1 & (g1 | mi1) /. ma1 = g1 /. (w + 1) ) by A169, A154, A199;
then f /. 1 = Ck1 /. mi by A39, A51, A52, A208, A211, GOBOARD1:2;
then A215: f /. 1 in rng (Col (G1,k)) by A39, A210, A213, PARTFUN2:2;
f /. 1 in rng f by A156, A214, PARTFUN2:2;
hence contradiction by A201, A215, XBOOLE_0:def_4; ::_thesis: verum
end;
supposeA216: the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) in (rng h2) /\ (rng (Col (G1,k))) ; ::_thesis: contradiction
then the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) in rng h2 by XBOOLE_0:def_4;
then consider i being Element of NAT such that
A217: i in dom h2 and
A218: the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) = h2 /. i by PARTFUN2:2;
A219: the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) = G1 * ((ma + i),k2) by A132, A217, A218;
reconsider y = the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) as Point of (TOP-REAL 2) by A218;
A220: Lma /. k2 = Lma . k2 by A130, PARTFUN1:def_6;
A221: the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) in rng (Col (G1,k)) by A216, XBOOLE_0:def_4;
A222: dom (Col (G1,k2)) = Seg (len G1) by A197, FINSEQ_1:def_3
.= dom G1 by FINSEQ_1:def_3 ;
then A223: Ck2 /. ma = Ck2 . ma by A41, PARTFUN1:def_6;
A224: ma + i in dom Ck2 by A134, A217, A222;
Ck2 /. (ma + i) = Ck2 . (ma + i) by A134, A217, A222, PARTFUN1:def_6;
then y = Ck2 /. (ma + i) by A219, A222, A224, MATRIX_1:def_8;
then y in rng Ck2 by A224, PARTFUN2:2;
then A225: k2 = k by A133, A200, A221, GOBOARD1:4;
A226: l in Seg l by A157, FINSEQ_1:1;
then ( f /. l = (g1 | mi1) /. (w + l) & (g1 | mi1) /. (w + l) = g1 /. (w + l) ) by A169, A154;
then f /. l = Ck2 /. ma by A41, A131, A133, A220, A223, GOBOARD1:2;
then A227: f /. l in rng (Col (G1,k)) by A41, A222, A225, PARTFUN2:2;
f /. l in rng f by A156, A226, PARTFUN2:2;
hence contradiction by A201, A227, XBOOLE_0:def_4; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
(rng h2) /\ (rng (g2 | m)) = {}
proof
set x = the Element of (rng h2) /\ (rng (g2 | m));
assume A228: not (rng h2) /\ (rng (g2 | m)) = {} ; ::_thesis: contradiction
then the Element of (rng h2) /\ (rng (g2 | m)) in rng h2 by XBOOLE_0:def_4;
then consider n1 being Element of NAT such that
A229: n1 in dom h2 and
A230: the Element of (rng h2) /\ (rng (g2 | m)) = h2 /. n1 by PARTFUN2:2;
A231: 1 <= n1 by A229, FINSEQ_3:25;
ma + n1 in dom G1 by A134, A229;
then A232: [(ma + n1),k2] in Indices G1 by A133, A95, ZFMISC_1:87;
the Element of (rng h2) /\ (rng (g2 | m)) in rng (g2 | m) by A228, XBOOLE_0:def_4;
then consider n2 being Element of NAT such that
A233: n2 in dom (g2 | m) and
A234: the Element of (rng h2) /\ (rng (g2 | m)) = (g2 | m) /. n2 by PARTFUN2:2;
consider i1, i2 being Element of NAT such that
A235: [i1,i2] in Indices G1 and
A236: (g2 | m) /. n2 = G1 * (i1,i2) by A15, A233, GOBOARD1:def_9;
reconsider L = Line (G1,i1) as FinSequence of (TOP-REAL 2) ;
A237: i2 in Seg (width G1) by A95, A235, ZFMISC_1:87;
A238: ( Seg (len L) = dom L & len L = width G1 ) by FINSEQ_1:def_3, MATRIX_1:def_7;
then L /. i2 = L . i2 by A237, PARTFUN1:def_6;
then (g2 | m) /. n2 = L /. i2 by A236, A237, MATRIX_1:def_7;
then A239: (g2 | m) /. n2 in rng L by A237, A238, PARTFUN2:2;
(g2 | m) /. n2 in rng (g2 | m) by A233, PARTFUN2:2;
then A240: (rng (g2 | m)) /\ (rng L) <> {} by A239, XBOOLE_0:def_4;
A241: i1 in dom G1 by A95, A235, ZFMISC_1:87;
the Element of (rng h2) /\ (rng (g2 | m)) = G1 * ((ma + n1),k2) by A132, A229, A230;
then i1 = ma + n1 by A234, A235, A236, A232, GOBOARD1:5;
then n1 <= 0 by A41, A241, A240, XREAL_1:29;
hence contradiction by A231, XXREAL_0:2; ::_thesis: verum
end;
then (rng ((h1 ^ f) ^ h2)) /\ (rng (g2 | m)) = (((rng h1) \/ (rng f)) /\ (rng (g2 | m))) \/ {} by A195, XBOOLE_1:23
.= {} \/ ((rng f) /\ (rng (g2 | m))) by A111, XBOOLE_1:23
.= (rng f) /\ (rng (g2 | m)) ;
then A242: (rng ((h1 ^ f) ^ h2)) /\ (rng (g2 | m)) c= (rng g1) /\ (rng g2) by A18, A177, XBOOLE_1:27;
A243: len (DelCol (G1,1)) = len G1 by A31, A151, GOBOARD1:def_8;
then A244: dom (DelCol (G1,1)) = Seg (len G1) by FINSEQ_1:def_3
.= dom G1 by FINSEQ_1:def_3 ;
A245: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_f_&_n_+_1_in_dom_f_holds_
for_i1,_i2,_j1,_j2_being_Element_of_NAT_st_[i1,i2]_in_Indices_G1_&_[j1,j2]_in_Indices_G1_&_f_/._n_=_G1_*_(i1,i2)_&_f_/._(n_+_1)_=_G1_*_(j1,j2)_holds_
(abs_(i1_-_j1))_+_(abs_(i2_-_j2))_=_1
let n be Element of NAT ; ::_thesis: ( n in dom f & n + 1 in dom f implies for i1, i2, j1, j2 being Element of NAT st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & f /. n = G1 * (i1,i2) & f /. (n + 1) = G1 * (j1,j2) holds
(abs (i1 - j1)) + (abs (i2 - j2)) = 1 )
assume that
A246: n in dom f and
A247: n + 1 in dom f ; ::_thesis: for i1, i2, j1, j2 being Element of NAT st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & f /. n = G1 * (i1,i2) & f /. (n + 1) = G1 * (j1,j2) holds
(abs (i1 - j1)) + (abs (i2 - j2)) = 1
f /. n = (g1 | mi1) /. (w + n) by A154, A156, A246;
then A248: f /. n = g1 /. (w + n) by A169, A156, A246;
f /. (n + 1) = (g1 | mi1) /. (w + (n + 1)) by A154, A156, A247;
then A249: ( (w + n) + 1 in dom g1 & f /. (n + 1) = g1 /. ((w + n) + 1) ) by A169, A156, A247;
let i1, i2, j1, j2 be Element of NAT ; ::_thesis: ( [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & f /. n = G1 * (i1,i2) & f /. (n + 1) = G1 * (j1,j2) implies (abs (i1 - j1)) + (abs (i2 - j2)) = 1 )
assume A250: ( [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & f /. n = G1 * (i1,i2) & f /. (n + 1) = G1 * (j1,j2) ) ; ::_thesis: (abs (i1 - j1)) + (abs (i2 - j2)) = 1
w + n in dom g1 by A169, A156, A246;
hence (abs (i1 - j1)) + (abs (i2 - j2)) = 1 by A6, A248, A249, A250, GOBOARD1:def_9; ::_thesis: verum
end;
set hf = h1 ^ f;
A251: len ((h1 ^ f) ^ h2) = (len (h1 ^ f)) + (len h2) by FINSEQ_1:22
.= ((len h1) + (len f)) + (len h2) by FINSEQ_1:22 ;
A252: now__::_thesis:_for_i1,_i2,_j1,_j2_being_Element_of_NAT_st_[i1,i2]_in_Indices_G1_&_[j1,j2]_in_Indices_G1_&_(h1_^_f)_/._(len_(h1_^_f))_=_G1_*_(i1,i2)_&_h2_/._1_=_G1_*_(j1,j2)_&_len_(h1_^_f)_in_dom_(h1_^_f)_&_1_in_dom_h2_holds_
(abs_(i1_-_j1))_+_(abs_(i2_-_j2))_=_1
let i1, i2, j1, j2 be Element of NAT ; ::_thesis: ( [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & (h1 ^ f) /. (len (h1 ^ f)) = G1 * (i1,i2) & h2 /. 1 = G1 * (j1,j2) & len (h1 ^ f) in dom (h1 ^ f) & 1 in dom h2 implies (abs (i1 - j1)) + (abs (i2 - j2)) = 1 )
assume that
A253: [i1,i2] in Indices G1 and
A254: [j1,j2] in Indices G1 and
A255: (h1 ^ f) /. (len (h1 ^ f)) = G1 * (i1,i2) and
A256: h2 /. 1 = G1 * (j1,j2) and
len (h1 ^ f) in dom (h1 ^ f) and
A257: 1 in dom h2 ; ::_thesis: (abs (i1 - j1)) + (abs (i2 - j2)) = 1
ma + 1 in dom G1 by A134, A257;
then A258: [(ma + 1),k2] in Indices G1 by A133, A95, ZFMISC_1:87;
A259: [ma,k2] in Indices G1 by A41, A133, A95, ZFMISC_1:87;
A260: Lma /. k2 = Lma . k2 by A130, PARTFUN1:def_6;
A261: len f in dom f by A154, A156, A157, FINSEQ_1:1;
(h1 ^ f) /. (len (h1 ^ f)) = (h1 ^ f) /. ((len h1) + (len f)) by FINSEQ_1:22
.= f /. (len f) by A261, FINSEQ_4:69
.= (g1 | mi1) /. (w + l) by A154, A156, A261
.= g1 /. mi1 by A169, A154, A156, A261
.= G1 * (ma,k2) by A131, A133, A260, MATRIX_1:def_7 ;
then A262: ( i1 = ma & i2 = k2 ) by A253, A255, A259, GOBOARD1:5;
h2 /. 1 = G1 * ((ma + 1),k2) by A132, A257;
then ( j1 = ma + 1 & j2 = k2 ) by A254, A256, A258, GOBOARD1:5;
hence (abs (i1 - j1)) + (abs (i2 - j2)) = (abs (ma - (ma + 1))) + 0 by A262, ABSVALUE:2
.= abs (- ((ma + 1) - ma))
.= abs 1 by COMPLEX1:52
.= 1 by ABSVALUE:def_1 ;
::_thesis: verum
end;
now__::_thesis:_for_i1,_i2,_j1,_j2_being_Element_of_NAT_st_[i1,i2]_in_Indices_G1_&_[j1,j2]_in_Indices_G1_&_h1_/._(len_h1)_=_G1_*_(i1,i2)_&_f_/._1_=_G1_*_(j1,j2)_&_len_h1_in_dom_h1_&_1_in_dom_f_holds_
(abs_(i1_-_j1))_+_(abs_(i2_-_j2))_=_1
A263: [mi,k1] in Indices G1 by A39, A52, A95, ZFMISC_1:87;
A264: Lmi /. k1 = Lmi . k1 by A50, PARTFUN1:def_6;
let i1, i2, j1, j2 be Element of NAT ; ::_thesis: ( [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & h1 /. (len h1) = G1 * (i1,i2) & f /. 1 = G1 * (j1,j2) & len h1 in dom h1 & 1 in dom f implies (abs (i1 - j1)) + (abs (i2 - j2)) = 1 )
assume that
A265: [i1,i2] in Indices G1 and
A266: [j1,j2] in Indices G1 and
A267: h1 /. (len h1) = G1 * (i1,i2) and
A268: f /. 1 = G1 * (j1,j2) and
A269: len h1 in dom h1 and
A270: 1 in dom f ; ::_thesis: (abs (i1 - j1)) + (abs (i2 - j2)) = 1
l1 in dom G1 by A75, A96, A269;
then A271: [l1,k1] in Indices G1 by A52, A95, ZFMISC_1:87;
A272: w + 1 = ma1 ;
then f /. 1 = (g1 | mi1) /. ma1 by A154, A156, A270;
then f /. 1 = g1 /. ma1 by A169, A156, A270, A272
.= G1 * (mi,k1) by A51, A52, A264, MATRIX_1:def_7 ;
then A273: ( j1 = mi & j2 = k1 ) by A266, A268, A263, GOBOARD1:5;
h1 /. (len h1) = G1 * (l1,k1) by A75, A269;
then ( i1 = l1 & i2 = k1 ) by A265, A267, A271, GOBOARD1:5;
hence (abs (i1 - j1)) + (abs (i2 - j2)) = (abs ((mi - 1) - mi)) + 0 by A273, ABSVALUE:2
.= abs (- 1)
.= abs 1 by COMPLEX1:52
.= 1 by ABSVALUE:def_1 ;
::_thesis: verum
end;
then for n being Element of NAT st n in dom (h1 ^ f) & n + 1 in dom (h1 ^ f) holds
for i1, i2, j1, j2 being Element of NAT st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & (h1 ^ f) /. n = G1 * (i1,i2) & (h1 ^ f) /. (n + 1) = G1 * (j1,j2) holds
(abs (i1 - j1)) + (abs (i2 - j2)) = 1 by A101, A245, GOBOARD1:24;
then A274: for n being Element of NAT st n in dom ((h1 ^ f) ^ h2) & n + 1 in dom ((h1 ^ f) ^ h2) holds
for m, k, i, j being Element of NAT st [m,k] in Indices G1 & [i,j] in Indices G1 & ((h1 ^ f) ^ h2) /. n = G1 * (m,k) & ((h1 ^ f) ^ h2) /. (n + 1) = G1 * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1 by A140, A252, GOBOARD1:24;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_h1_holds_
ex_i,_k1_being_Element_of_NAT_st_
(_[i,k1]_in_Indices_G1_&_h1_/._n_=_G1_*_(i,k1)_)
let n be Element of NAT ; ::_thesis: ( n in dom h1 implies ex i, k1 being Element of NAT st
( [i,k1] in Indices G1 & h1 /. n = G1 * (i,k1) ) )
assume A275: n in dom h1 ; ::_thesis: ex i, k1 being Element of NAT st
( [i,k1] in Indices G1 & h1 /. n = G1 * (i,k1) )
take i = n; ::_thesis: ex k1 being Element of NAT st
( [i,k1] in Indices G1 & h1 /. n = G1 * (i,k1) )
take k1 = k1; ::_thesis: ( [i,k1] in Indices G1 & h1 /. n = G1 * (i,k1) )
n in dom G1 by A96, A275;
hence ( [i,k1] in Indices G1 & h1 /. n = G1 * (i,k1) ) by A75, A52, A95, A275, ZFMISC_1:87; ::_thesis: verum
end;
then for n being Element of NAT st n in dom (h1 ^ f) holds
ex i, j being Element of NAT st
( [i,j] in Indices G1 & (h1 ^ f) /. n = G1 * (i,j) ) by A173, GOBOARD1:23;
then for n being Element of NAT st n in dom ((h1 ^ f) ^ h2) holds
ex i, j being Element of NAT st
( [i,j] in Indices G1 & ((h1 ^ f) ^ h2) /. n = G1 * (i,j) ) by A138, GOBOARD1:23;
then A276: (h1 ^ f) ^ h2 is_sequence_on G1 by A274, GOBOARD1:def_9;
A277: Seg (len ((h1 ^ f) ^ h2)) = dom ((h1 ^ f) ^ h2) by FINSEQ_1:def_3;
then A278: len ((h1 ^ f) ^ h2) in dom ((h1 ^ f) ^ h2) by A251, A194, FINSEQ_1:1;
A279: 1 in dom ((h1 ^ f) ^ h2) by A251, A194, A277, FINSEQ_1:1;
thus (rng g1) /\ (rng g2) <> {} ::_thesis: verum
proof
percases ( (rng f) /\ (rng (Col (G1,1))) = {} or (rng f) /\ (rng (Col (G1,1))) <> {} ) ;
supposeA280: (rng f) /\ (rng (Col (G1,1))) = {} ; ::_thesis: (rng g1) /\ (rng g2) <> {}
set D = DelCol (G1,1);
(rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,1))) = {} by A31, A196, A280;
then A281: rng ((h1 ^ f) ^ h2) misses rng (Col (G1,1)) by XBOOLE_0:def_7;
then A282: ( (h1 ^ f) ^ h2 is_sequence_on DelCol (G1,1) & ((h1 ^ f) ^ h2) /. 1 in rng (Line ((DelCol (G1,1)),1)) ) by A31, A26, A276, A158, A151, A279, GOBOARD1:21, GOBOARD1:25;
A283: ((h1 ^ f) ^ h2) /. (len ((h1 ^ f) ^ h2)) in rng (Line ((DelCol (G1,1)),(len (DelCol (G1,1))))) by A31, A27, A182, A151, A243, A278, A281, GOBOARD1:21;
defpred S7[ Nat] means ( $1 in dom (g2 | m) & (g2 | m) /. $1 in rng (Col (G1,1)) );
A284: ex m being Nat st S7[m]
proof
take 1 ; ::_thesis: S7[1]
thus S7[1] by A10, A13, A32, FINSEQ_3:25, GOBOARD1:6; ::_thesis: verum
end;
A285: for m being Nat st S7[m] holds
m <= len (g2 | m) by FINSEQ_3:25;
consider m being Nat such that
A286: ( S7[m] & ( for k being Nat st S7[k] holds
k <= m ) ) from NAT_1:sch_6(A285, A284);
A287: for k being Element of NAT st S7[k] holds
k <= m by A286;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
reconsider p = (g2 | m) /. m as Point of (TOP-REAL 2) ;
A288: now__::_thesis:_not_m_>=_len_(g2_|_m)
assume A289: m >= len (g2 | m) ; ::_thesis: contradiction
m <= len (g2 | m) by A286, FINSEQ_3:25;
then p in rng (Col (G1,(width G1))) by A28, A289, XXREAL_0:1;
then 1 = k + 1 by A3, A31, A74, A286, GOBOARD1:4;
hence contradiction by A92; ::_thesis: verum
end;
then reconsider ll = (len (g2 | m)) - m as Element of NAT by INT_1:5;
deffunc H3( Nat) -> Element of the U1 of (TOP-REAL 2) = (g2 | m) /. (m + $1);
consider t being FinSequence of (TOP-REAL 2) such that
A290: ( len t = ll & ( for n being Nat st n in dom t holds
t /. n = H3(n) ) ) from FINSEQ_4:sch_2();
A291: dom t = Seg ll by A290, FINSEQ_1:def_3;
A292: rng t c= rng (g2 | m)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng t or y in rng (g2 | m) )
assume y in rng t ; ::_thesis: y in rng (g2 | m)
then consider x being Element of NAT such that
A293: x in dom t and
A294: t /. x = y by PARTFUN2:2;
x <= ll by A291, A293, FINSEQ_1:1;
then A295: m + x <= m + ll by XREAL_1:7;
A296: x <= x + m by NAT_1:11;
1 <= x by A291, A293, FINSEQ_1:1;
then 1 <= x + m by A296, XXREAL_0:2;
then m + x in dom (g2 | m) by A295, FINSEQ_3:25;
then (g2 | m) /. (m + x) in rng (g2 | m) by PARTFUN2:2;
hence y in rng (g2 | m) by A290, A293, A294; ::_thesis: verum
end;
A297: for n being Element of NAT st n in dom t holds
m + n in dom (g2 | m)
proof
let n be Element of NAT ; ::_thesis: ( n in dom t implies m + n in dom (g2 | m) )
A298: n <= n + m by NAT_1:11;
assume A299: n in dom t ; ::_thesis: m + n in dom (g2 | m)
then n <= ll by A291, FINSEQ_1:1;
then A300: m + n <= m + ll by XREAL_1:7;
1 <= n by A291, A299, FINSEQ_1:1;
then 1 <= n + m by A298, XXREAL_0:2;
hence m + n in dom (g2 | m) by A300, FINSEQ_3:25; ::_thesis: verum
end;
A301: Seg (len t) = dom t by FINSEQ_1:def_3;
reconsider t = t as FinSequence of (TOP-REAL 2) ;
A302: width (DelCol (G1,1)) = k by A3, A31, A92, GOBOARD1:10, NAT_1:3;
A303: Indices (DelCol (G1,1)) = [:(dom (DelCol (G1,1))),(Seg (width (DelCol (G1,1)))):] by MATRIX_1:def_4;
A304: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_t_holds_
ex_i1,_l_being_Element_of_NAT_st_
(_[i1,l]_in_Indices_(DelCol_(G1,1))_&_t_/._n_=_(DelCol_(G1,1))_*_(i1,l)_)
let n be Element of NAT ; ::_thesis: ( n in dom t implies ex i1, l being Element of NAT st
( [i1,l] in Indices (DelCol (G1,1)) & t /. n = (DelCol (G1,1)) * (i1,l) ) )
assume A305: n in dom t ; ::_thesis: ex i1, l being Element of NAT st
( [i1,l] in Indices (DelCol (G1,1)) & t /. n = (DelCol (G1,1)) * (i1,l) )
then m + n in dom (g2 | m) by A297;
then consider i1, i2 being Element of NAT such that
A306: [i1,i2] in Indices G1 and
A307: (g2 | m) /. (m + n) = G1 * (i1,i2) by A15, GOBOARD1:def_9;
A308: i2 in Seg (width G1) by A95, A306, ZFMISC_1:87;
then A309: 1 <= i2 by FINSEQ_1:1;
then reconsider l = i2 - 1 as Element of NAT by INT_1:5;
reconsider Ci2 = Col (G1,i2) as FinSequence of (TOP-REAL 2) ;
A310: i1 in dom G1 by A95, A306, ZFMISC_1:87;
len Ci2 = len G1 by MATRIX_1:def_8;
then A311: dom Ci2 = Seg (len G1) by FINSEQ_1:def_3
.= dom G1 by FINSEQ_1:def_3 ;
then Ci2 /. i1 = Ci2 . i1 by A310, PARTFUN1:def_6;
then Ci2 /. i1 = G1 * (i1,i2) by A310, MATRIX_1:def_8;
then A312: (g2 | m) /. (m + n) in rng (Col (G1,i2)) by A307, A310, A311, PARTFUN2:2;
now__::_thesis:_not_i2_=_1
1 <= n by A291, A305, FINSEQ_1:1;
then A313: m + 1 <= m + n by XREAL_1:7;
assume i2 = 1 ; ::_thesis: contradiction
then m + n <= m by A286, A297, A305, A312;
then m + 1 <= m by A313, XXREAL_0:2;
then 1 <= m - m by XREAL_1:19;
then 1 <= 0 ;
hence contradiction ; ::_thesis: verum
end;
then 1 < i2 by A309, XXREAL_0:1;
then 1 + 1 <= i2 by NAT_1:13;
then A314: 1 <= l by XREAL_1:19;
take i1 = i1; ::_thesis: ex l being Element of NAT st
( [i1,l] in Indices (DelCol (G1,1)) & t /. n = (DelCol (G1,1)) * (i1,l) )
take l = l; ::_thesis: ( [i1,l] in Indices (DelCol (G1,1)) & t /. n = (DelCol (G1,1)) * (i1,l) )
A315: t /. n = (g2 | m) /. (m + n) by A290, A305;
i2 <= width G1 by A308, FINSEQ_1:1;
then A316: l <= width (DelCol (G1,1)) by A3, A302, XREAL_1:20;
then l in Seg (width (DelCol (G1,1))) by A314, FINSEQ_1:1;
hence [i1,l] in Indices (DelCol (G1,1)) by A244, A303, A310, ZFMISC_1:87; ::_thesis: t /. n = (DelCol (G1,1)) * (i1,l)
l + 1 = i2 ;
hence t /. n = (DelCol (G1,1)) * (i1,l) by A3, A31, A93, A302, A307, A310, A315, A314, A316, GOBOARD1:16; ::_thesis: verum
end;
0 <> width (DelCol (G1,1)) by GOBOARD1:def_3;
then 0 < width (DelCol (G1,1)) by NAT_1:3;
then A317: 0 + 1 <= width (DelCol (G1,1)) by NAT_1:13;
then A318: ( Col ((DelCol (G1,1)),1) = Col (G1,(1 + 1)) & 1 + 1 in Seg (width G1) ) by A3, A31, A93, A302, GOBOARD1:14;
m + 1 <= len (g2 | m) by A288, NAT_1:13;
then A319: 1 <= len t by A290, XREAL_1:19;
then 1 in Seg ll by A290, FINSEQ_1:1;
then t /. 1 = (g2 | m) /. (m + 1) by A290, A301;
then A320: t /. 1 in rng (Col ((DelCol (G1,1)),1)) by A32, A15, A28, A31, A286, A287, A318, GOBOARD1:32;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_t_&_n_+_1_in_dom_t_holds_
for_i1,_i2,_j1,_j2_being_Element_of_NAT_st_[i1,i2]_in_Indices_(DelCol_(G1,1))_&_[j1,j2]_in_Indices_(DelCol_(G1,1))_&_t_/._n_=_(DelCol_(G1,1))_*_(i1,i2)_&_t_/._(n_+_1)_=_(DelCol_(G1,1))_*_(j1,j2)_holds_
1_=_(abs_(i1_-_j1))_+_(abs_(i2_-_j2))
let n be Element of NAT ; ::_thesis: ( n in dom t & n + 1 in dom t implies for i1, i2, j1, j2 being Element of NAT st [i1,i2] in Indices (DelCol (G1,1)) & [j1,j2] in Indices (DelCol (G1,1)) & t /. n = (DelCol (G1,1)) * (i1,i2) & t /. (n + 1) = (DelCol (G1,1)) * (j1,j2) holds
1 = (abs (i1 - j1)) + (abs (i2 - j2)) )
assume that
A321: n in dom t and
A322: n + 1 in dom t ; ::_thesis: for i1, i2, j1, j2 being Element of NAT st [i1,i2] in Indices (DelCol (G1,1)) & [j1,j2] in Indices (DelCol (G1,1)) & t /. n = (DelCol (G1,1)) * (i1,i2) & t /. (n + 1) = (DelCol (G1,1)) * (j1,j2) holds
1 = (abs (i1 - j1)) + (abs (i2 - j2))
let i1, i2, j1, j2 be Element of NAT ; ::_thesis: ( [i1,i2] in Indices (DelCol (G1,1)) & [j1,j2] in Indices (DelCol (G1,1)) & t /. n = (DelCol (G1,1)) * (i1,i2) & t /. (n + 1) = (DelCol (G1,1)) * (j1,j2) implies 1 = (abs (i1 - j1)) + (abs (i2 - j2)) )
assume that
A323: [i1,i2] in Indices (DelCol (G1,1)) and
A324: [j1,j2] in Indices (DelCol (G1,1)) and
A325: t /. n = (DelCol (G1,1)) * (i1,i2) and
A326: t /. (n + 1) = (DelCol (G1,1)) * (j1,j2) ; ::_thesis: 1 = (abs (i1 - j1)) + (abs (i2 - j2))
A327: i1 in dom (DelCol (G1,1)) by A303, A323, ZFMISC_1:87;
i2 in Seg k by A302, A303, A323, ZFMISC_1:87;
then A328: ( 1 <= i2 & i2 <= k ) by FINSEQ_1:1;
then i2 + 1 in Seg (width G1) by A3, A31, A93, A244, A327, GOBOARD1:16;
then A329: [i1,(i2 + 1)] in Indices G1 by A95, A244, A327, ZFMISC_1:87;
t /. n = (g2 | m) /. (m + n) by A290, A321;
then A330: (g2 | m) /. (m + n) = G1 * (i1,(i2 + 1)) by A3, A31, A93, A244, A325, A327, A328, GOBOARD1:16;
m + (n + 1) = (m + n) + 1 ;
then A331: (m + n) + 1 in dom (g2 | m) by A297, A322;
A332: j1 in dom (DelCol (G1,1)) by A303, A324, ZFMISC_1:87;
j2 in Seg k by A302, A303, A324, ZFMISC_1:87;
then A333: ( 1 <= j2 & j2 <= k ) by FINSEQ_1:1;
then j2 + 1 in Seg (width G1) by A3, A31, A93, A244, A327, GOBOARD1:16;
then A334: [j1,(j2 + 1)] in Indices G1 by A95, A244, A332, ZFMISC_1:87;
t /. (n + 1) = (g2 | m) /. (m + (n + 1)) by A290, A322;
then A335: (g2 | m) /. ((m + n) + 1) = G1 * (j1,(j2 + 1)) by A3, A31, A93, A244, A326, A332, A333, GOBOARD1:16;
m + n in dom (g2 | m) by A297, A321;
hence 1 = (abs (i1 - j1)) + (abs ((i2 + 1) - (j2 + 1))) by A15, A330, A335, A329, A334, A331, GOBOARD1:def_9
.= (abs (i1 - j1)) + (abs (i2 - j2)) ;
::_thesis: verum
end;
then A336: t is_sequence_on DelCol (G1,1) by A304, GOBOARD1:def_9;
set x = the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng t);
A337: (rng ((h1 ^ f) ^ h2)) /\ (rng t) c= (rng ((h1 ^ f) ^ h2)) /\ (rng (g2 | m)) by A292, XBOOLE_1:26;
len t in Seg ll by A290, A319, FINSEQ_1:1;
then t /. (len t) = (g2 | m) /. (m + ll) by A290, A301
.= (g2 | m) /. (len (g2 | m)) ;
then t /. (len t) in rng (Col ((DelCol (G1,1)),(width (DelCol (G1,1))))) by A3, A28, A31, A93, A302, A317, GOBOARD1:14;
then (rng ((h1 ^ f) ^ h2)) /\ (rng t) <> {} by A2, A93, A251, A194, A302, A319, A320, A336, A282, A283;
then the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng t) in (rng ((h1 ^ f) ^ h2)) /\ (rng (g2 | m)) by A337, TARSKI:def_3;
hence (rng g1) /\ (rng g2) <> {} by A242; ::_thesis: verum
end;
supposeA338: (rng f) /\ (rng (Col (G1,1))) <> {} ; ::_thesis: (rng g1) /\ (rng g2) <> {}
set D = DelCol (G1,(width G1));
A339: 0 + 1 < k + 1 by A93, XREAL_1:6;
now__::_thesis:_(rng_g1)_/\_(rng_g2)_<>_{}
percases ( (rng f) /\ (rng (Col (G1,(width G1)))) = {} or (rng f) /\ (rng (Col (G1,(width G1)))) <> {} ) ;
suppose (rng f) /\ (rng (Col (G1,(width G1)))) = {} ; ::_thesis: (rng g1) /\ (rng g2) <> {}
then (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,(width G1)))) = {} by A74, A196;
then A340: rng ((h1 ^ f) ^ h2) misses rng (Col (G1,(width G1))) by XBOOLE_0:def_7;
then A341: (h1 ^ f) ^ h2 is_sequence_on DelCol (G1,(width G1)) by A74, A276, A151, GOBOARD1:25;
consider t being FinSequence of (TOP-REAL 2) such that
A342: ( t /. 1 in rng (Col ((DelCol (G1,(width G1))),1)) & t /. (len t) in rng (Col ((DelCol (G1,(width G1))),(width (DelCol (G1,(width G1)))))) & 1 <= len t & t is_sequence_on DelCol (G1,(width G1)) ) and
A343: rng t c= rng (g2 | m) by A3, A32, A15, A14, A28, A339, GOBOARD1:35;
set x = the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng t);
A344: (rng ((h1 ^ f) ^ h2)) /\ (rng t) c= (rng ((h1 ^ f) ^ h2)) /\ (rng (g2 | m)) by A343, XBOOLE_1:26;
A345: width (DelCol (G1,(width G1))) = k by A3, A74, A92, GOBOARD1:10, NAT_1:3;
( ((h1 ^ f) ^ h2) /. 1 in rng (Line ((DelCol (G1,(width G1))),1)) & ((h1 ^ f) ^ h2) /. (len ((h1 ^ f) ^ h2)) in rng (Line ((DelCol (G1,(width G1))),(len (DelCol (G1,(width G1)))))) ) by A74, A26, A27, A158, A182, A151, A152, A279, A278, A340, GOBOARD1:21;
then (rng ((h1 ^ f) ^ h2)) /\ (rng t) <> {} by A2, A93, A251, A194, A342, A345, A341;
then the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng t) in (rng ((h1 ^ f) ^ h2)) /\ (rng (g2 | m)) by A344, TARSKI:def_3;
hence (rng g1) /\ (rng g2) <> {} by A242; ::_thesis: verum
end;
supposeA346: (rng f) /\ (rng (Col (G1,(width G1)))) <> {} ; ::_thesis: (rng g1) /\ (rng g2) <> {}
A347: f is_sequence_on G1 by A173, A245, GOBOARD1:def_9;
then consider t being FinSequence of (TOP-REAL 2) such that
A348: rng t c= rng f and
A349: ( t /. 1 in rng (Col (G1,1)) & t /. (len t) in rng (Col (G1,(width G1))) & 1 <= len t & t is_sequence_on G1 ) by A338, A346, GOBOARD1:36;
consider tt being FinSequence of (TOP-REAL 2) such that
A350: ( tt /. 1 in rng (Col ((DelCol (G1,(width G1))),1)) & tt /. (len tt) in rng (Col ((DelCol (G1,(width G1))),(width (DelCol (G1,(width G1)))))) & 1 <= len tt & tt is_sequence_on DelCol (G1,(width G1)) ) and
A351: rng tt c= rng t by A3, A339, A349, GOBOARD1:35;
A352: ( Seg (len Lma) = dom Lma & len Lma = width G1 ) by FINSEQ_1:def_3, MATRIX_1:def_7;
reconsider lg = (len (g2 | m)) - 1 as Element of NAT by A32, INT_1:5;
defpred S7[ Nat] means ( $1 in dom (g2 | m) & (g2 | m) /. $1 in rng (Line (G1,mi)) );
defpred S8[ Nat] means ( $1 in dom (g2 | m) & (g2 | m) /. $1 in rng (Line (G1,ma)) );
A353: lg <= len (g2 | m) by XREAL_1:43;
A354: now__::_thesis:_ex_n_being_Nat_st_S7[n]
set x = the Element of (rng (g2 | m)) /\ (rng (Line (G1,mi)));
the Element of (rng (g2 | m)) /\ (rng (Line (G1,mi))) in rng (g2 | m) by A39, XBOOLE_0:def_4;
then consider n being Element of NAT such that
A355: ( n in dom (g2 | m) & the Element of (rng (g2 | m)) /\ (rng (Line (G1,mi))) = (g2 | m) /. n ) by PARTFUN2:2;
reconsider n = n as Nat ;
take n = n; ::_thesis: S7[n]
thus S7[n] by A39, A355, XBOOLE_0:def_4; ::_thesis: verum
end;
consider pf being Nat such that
A356: ( S7[pf] & ( for n being Nat st S7[n] holds
pf <= n ) ) from NAT_1:sch_5(A354);
defpred S9[ Element of NAT ] means ( $1 in dom f implies for m being Element of NAT st m in dom G1 & f /. $1 in rng (Line (G1,m)) holds
mi <= m );
reconsider C = Col (G1,(width G1)), Li = Line (G1,mi), La = Line (G1,ma) as FinSequence of (TOP-REAL 2) ;
A357: lg + 1 = len (g2 | m) ;
A358: now__::_thesis:_ex_n_being_Nat_st_S8[n]
set x = the Element of (rng (g2 | m)) /\ (rng (Line (G1,ma)));
the Element of (rng (g2 | m)) /\ (rng (Line (G1,ma))) in rng (g2 | m) by A41, XBOOLE_0:def_4;
then consider n being Element of NAT such that
A359: ( n in dom (g2 | m) & the Element of (rng (g2 | m)) /\ (rng (Line (G1,ma))) = (g2 | m) /. n ) by PARTFUN2:2;
reconsider n = n as Nat ;
take n = n; ::_thesis: S8[n]
thus S8[n] by A41, A359, XBOOLE_0:def_4; ::_thesis: verum
end;
consider pl being Nat such that
A360: ( S8[pl] & ( for n being Nat st S8[n] holds
pl <= n ) ) from NAT_1:sch_5(A358);
reconsider pf = pf, pl = pl as Element of NAT by ORDINAL1:def_12;
A361: 1 <= pf by A356, FINSEQ_3:25;
consider K2 being Element of NAT such that
A362: K2 in dom Lma and
A363: (g2 | m) /. pl = Lma /. K2 by A360, PARTFUN2:2;
reconsider CK2 = Col (G1,K2) as FinSequence of (TOP-REAL 2) ;
consider K1 being Element of NAT such that
A364: K1 in dom Li and
A365: (g2 | m) /. pf = Li /. K1 by A356, PARTFUN2:2;
reconsider CK1 = Col (G1,K1) as FinSequence of (TOP-REAL 2) ;
deffunc H3( Nat) -> Element of the U1 of (TOP-REAL 2) = G1 * ($1,K1);
consider h1 being FinSequence of (TOP-REAL 2) such that
A366: ( len h1 = l1 & ( for n being Nat st n in dom h1 holds
h1 /. n = H3(n) ) ) from FINSEQ_4:sch_2();
A367: for k being Element of NAT st S9[k] holds
S9[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S9[k] implies S9[k + 1] )
assume A368: S9[k] ; ::_thesis: S9[k + 1]
assume A369: k + 1 in dom f ; ::_thesis: for m being Element of NAT st m in dom G1 & f /. (k + 1) in rng (Line (G1,m)) holds
mi <= m
let m be Element of NAT ; ::_thesis: ( m in dom G1 & f /. (k + 1) in rng (Line (G1,m)) implies mi <= m )
assume A370: ( m in dom G1 & f /. (k + 1) in rng (Line (G1,m)) ) ; ::_thesis: mi <= m
now__::_thesis:_mi_<=_m
percases ( k = 0 or k <> 0 ) ;
supposeA371: k = 0 ; ::_thesis: mi <= m
( w + 1 = ma1 & 1 in Seg l ) by A157, FINSEQ_1:1;
then ( f /. 1 = (g1 | mi1) /. ma1 & (g1 | mi1) /. ma1 = g1 /. ma1 ) by A169, A154;
then f /. (k + 1) in rng Li by A50, A51, A371, PARTFUN2:2;
hence mi <= m by A39, A370, GOBOARD1:3; ::_thesis: verum
end;
suppose k <> 0 ; ::_thesis: mi <= m
then 0 < k by NAT_1:3;
then A372: 0 + 1 <= k by NAT_1:13;
k + 1 <= len f by A369, FINSEQ_3:25;
then A373: k <= len f by NAT_1:13;
then A374: k in dom f by A372, FINSEQ_3:25;
then consider i1, i2 being Element of NAT such that
A375: [i1,i2] in Indices G1 and
A376: f /. k = G1 * (i1,i2) by A173;
A377: i2 in Seg (width G1) by A95, A375, ZFMISC_1:87;
consider j1, j2 being Element of NAT such that
A378: [j1,j2] in Indices G1 and
A379: f /. (k + 1) = G1 * (j1,j2) by A173, A369;
reconsider Lj1 = Line (G1,j1) as FinSequence of (TOP-REAL 2) ;
A380: j2 in Seg (width G1) by A95, A378, ZFMISC_1:87;
A381: ( Seg (len Lj1) = dom Lj1 & len Lj1 = width G1 ) by FINSEQ_1:def_3, MATRIX_1:def_7;
then Lj1 /. j2 = Lj1 . j2 by A380, PARTFUN1:def_6;
then f /. (k + 1) = Lj1 /. j2 by A379, A380, MATRIX_1:def_7;
then A382: f /. (k + 1) in rng Lj1 by A380, A381, PARTFUN2:2;
A383: j1 in dom G1 by A95, A378, ZFMISC_1:87;
reconsider Li1 = Line (G1,i1) as FinSequence of (TOP-REAL 2) ;
A384: i1 in dom G1 by A95, A375, ZFMISC_1:87;
A385: ( Seg (len Li1) = dom Li1 & len Li1 = width G1 ) by FINSEQ_1:def_3, MATRIX_1:def_7;
then A386: Li1 /. i2 = Li1 . i2 by A377, PARTFUN1:def_6;
then f /. k = Li1 /. i2 by A376, A377, MATRIX_1:def_7;
then A387: f /. k in rng Li1 by A377, A385, PARTFUN2:2;
then A388: mi <= i1 by A368, A372, A373, A384, FINSEQ_3:25;
now__::_thesis:_mi_<=_m
percases ( mi = i1 or mi < i1 ) by A388, XXREAL_0:1;
supposeA389: mi = i1 ; ::_thesis: mi <= m
g1 /. (w + k) = (g1 | mi1) /. (w + k) by A169, A156, A374
.= f /. k by A154, A156, A374
.= Li1 /. i2 by A376, A377, A386, MATRIX_1:def_7 ;
then g1 /. (w + k) in rng (Line (G1,mi)) by A377, A385, A389, PARTFUN2:2;
then A390: w + k <= ma1 by A46, A169, A156, A374;
w + 1 <= w + k by A372, XREAL_1:7;
then w + k = ma1 by A390, XXREAL_0:1;
then A391: ma1 + 1 = w + (k + 1) ;
mi + 1 <= ma by A127, NAT_1:13;
then A392: mi + 1 <= len G1 by A48, XXREAL_0:2;
1 <= mi + 1 by A42, NAT_1:13;
then A393: mi + 1 in dom G1 by A392, FINSEQ_3:25;
( f /. (k + 1) = (g1 | mi1) /. (w + (k + 1)) & (g1 | mi1) /. (w + (k + 1)) = g1 /. (w + (k + 1)) ) by A169, A154, A156, A369;
then f /. (k + 1) in rng (Line (G1,(mi + 1))) by A4, A6, A9, A39, A46, A49, A391, A393, GOBOARD1:28;
then m = mi + 1 by A370, A393, GOBOARD1:3;
hence mi <= m by NAT_1:11; ::_thesis: verum
end;
supposeA394: mi < i1 ; ::_thesis: mi <= m
now__::_thesis:_mi_<=_m
percases ( f /. (k + 1) in rng (Line (G1,i1)) or for l being Element of NAT st f /. (k + 1) in rng (Line (G1,l)) & l in dom G1 holds
abs (i1 - l) = 1 ) by A347, A369, A374, A384, A387, GOBOARD1:27;
suppose f /. (k + 1) in rng (Line (G1,i1)) ; ::_thesis: mi <= m
hence mi <= m by A370, A384, A394, GOBOARD1:3; ::_thesis: verum
end;
suppose for l being Element of NAT st f /. (k + 1) in rng (Line (G1,l)) & l in dom G1 holds
abs (i1 - l) = 1 ; ::_thesis: mi <= m
then A395: abs (i1 - j1) = 1 by A383, A382;
now__::_thesis:_mi_<=_m
percases ( ( j1 < i1 & i1 = j1 + 1 ) or ( i1 < j1 & j1 = i1 + 1 ) ) by A395, SEQM_3:41;
supposeA396: ( j1 < i1 & i1 = j1 + 1 ) ; ::_thesis: mi <= m
then mi <= i1 - 1 by A394, NAT_1:13;
hence mi <= m by A370, A383, A382, A396, GOBOARD1:3; ::_thesis: verum
end;
suppose ( i1 < j1 & j1 = i1 + 1 ) ; ::_thesis: mi <= m
then mi < j1 by A394, XXREAL_0:2;
hence mi <= m by A370, A383, A382, GOBOARD1:3; ::_thesis: verum
end;
end;
end;
hence mi <= m ; ::_thesis: verum
end;
end;
end;
hence mi <= m ; ::_thesis: verum
end;
end;
end;
hence mi <= m ; ::_thesis: verum
end;
end;
end;
hence mi <= m ; ::_thesis: verum
end;
A397: ( Seg (len Li) = dom Li & len Li = width G1 ) by FINSEQ_1:def_3, MATRIX_1:def_7;
A398: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_h1_holds_
n_in_dom_G1
let n be Element of NAT ; ::_thesis: ( n in dom h1 implies n in dom G1 )
A399: l1 <= mi by XREAL_1:43;
assume A400: n in dom h1 ; ::_thesis: n in dom G1
then A401: 1 <= n by FINSEQ_3:25;
n <= l1 by A366, A400, FINSEQ_3:25;
then A402: n <= mi by A399, XXREAL_0:2;
mi <= len G1 by A39, FINSEQ_3:25;
then n <= len G1 by A402, XXREAL_0:2;
hence n in dom G1 by A401, FINSEQ_3:25; ::_thesis: verum
end;
A403: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_h1_holds_
ex_i,_K1_being_Element_of_NAT_st_
(_[i,K1]_in_Indices_G1_&_h1_/._n_=_G1_*_(i,K1)_)
let n be Element of NAT ; ::_thesis: ( n in dom h1 implies ex i, K1 being Element of NAT st
( [i,K1] in Indices G1 & h1 /. n = G1 * (i,K1) ) )
assume A404: n in dom h1 ; ::_thesis: ex i, K1 being Element of NAT st
( [i,K1] in Indices G1 & h1 /. n = G1 * (i,K1) )
take i = n; ::_thesis: ex K1 being Element of NAT st
( [i,K1] in Indices G1 & h1 /. n = G1 * (i,K1) )
take K1 = K1; ::_thesis: ( [i,K1] in Indices G1 & h1 /. n = G1 * (i,K1) )
n in dom G1 by A398, A404;
hence ( [i,K1] in Indices G1 & h1 /. n = G1 * (i,K1) ) by A95, A364, A397, A366, A404, ZFMISC_1:87; ::_thesis: verum
end;
A405: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_h1_&_n_+_1_in_dom_h1_holds_
for_i1,_i2,_j1,_j2_being_Element_of_NAT_st_[i1,i2]_in_Indices_G1_&_[j1,j2]_in_Indices_G1_&_h1_/._n_=_G1_*_(i1,i2)_&_h1_/._(n_+_1)_=_G1_*_(j1,j2)_holds_
(abs_(i1_-_j1))_+_(abs_(i2_-_j2))_=_1
let n be Element of NAT ; ::_thesis: ( n in dom h1 & n + 1 in dom h1 implies for i1, i2, j1, j2 being Element of NAT st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & h1 /. n = G1 * (i1,i2) & h1 /. (n + 1) = G1 * (j1,j2) holds
(abs (i1 - j1)) + (abs (i2 - j2)) = 1 )
assume that
A406: n in dom h1 and
A407: n + 1 in dom h1 ; ::_thesis: for i1, i2, j1, j2 being Element of NAT st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & h1 /. n = G1 * (i1,i2) & h1 /. (n + 1) = G1 * (j1,j2) holds
(abs (i1 - j1)) + (abs (i2 - j2)) = 1
n + 1 in dom G1 by A398, A407;
then A408: [(n + 1),K1] in Indices G1 by A95, A364, A397, ZFMISC_1:87;
let i1, i2, j1, j2 be Element of NAT ; ::_thesis: ( [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & h1 /. n = G1 * (i1,i2) & h1 /. (n + 1) = G1 * (j1,j2) implies (abs (i1 - j1)) + (abs (i2 - j2)) = 1 )
assume that
A409: [i1,i2] in Indices G1 and
A410: [j1,j2] in Indices G1 and
A411: h1 /. n = G1 * (i1,i2) and
A412: h1 /. (n + 1) = G1 * (j1,j2) ; ::_thesis: (abs (i1 - j1)) + (abs (i2 - j2)) = 1
h1 /. (n + 1) = G1 * ((n + 1),K1) by A366, A407;
then A413: ( j1 = n + 1 & j2 = K1 ) by A408, A410, A412, GOBOARD1:5;
n in dom G1 by A398, A406;
then A414: [n,K1] in Indices G1 by A95, A364, A397, ZFMISC_1:87;
h1 /. n = G1 * (n,K1) by A366, A406;
then ( i1 = n & i2 = K1 ) by A414, A409, A411, GOBOARD1:5;
hence (abs (i1 - j1)) + (abs (i2 - j2)) = (abs ((n - n) + (- 1))) + 0 by A413, ABSVALUE:2
.= abs 1 by COMPLEX1:52
.= 1 by ABSVALUE:def_1 ;
::_thesis: verum
end;
A415: pf <= len (g2 | m) by A356, FINSEQ_3:25;
A416: Lma /. K2 = Lma . K2 by A362, PARTFUN1:def_6;
then A417: (g2 | m) /. pl = G1 * (ma,K2) by A362, A363, A352, MATRIX_1:def_7;
deffunc H4( Nat) -> Element of the U1 of (TOP-REAL 2) = G1 * ((ma + $1),K2);
consider h2 being FinSequence of (TOP-REAL 2) such that
A418: ( len h2 = l2 & ( for n being Nat st n in dom h2 holds
h2 /. n = H4(n) ) ) from FINSEQ_4:sch_2();
A419: S9[ 0 ] by FINSEQ_3:25;
A420: for n being Element of NAT holds S9[n] from NAT_1:sch_1(A419, A367);
A421: (rng h1) /\ (rng tt) = {}
proof
set x = the Element of (rng h1) /\ (rng tt);
assume A422: not (rng h1) /\ (rng tt) = {} ; ::_thesis: contradiction
then the Element of (rng h1) /\ (rng tt) in rng h1 by XBOOLE_0:def_4;
then consider i2 being Element of NAT such that
A423: i2 in dom h1 and
A424: h1 /. i2 = the Element of (rng h1) /\ (rng tt) by PARTFUN2:2;
Seg (len h1) = dom h1 by FINSEQ_1:def_3;
then A425: ( l1 < mi & i2 <= l1 ) by A366, A423, FINSEQ_1:1, XREAL_1:44;
i2 in dom G1 by A398, A423;
then A426: [i2,K1] in Indices G1 by A95, A364, A397, ZFMISC_1:87;
the Element of (rng h1) /\ (rng tt) in rng tt by A422, XBOOLE_0:def_4;
then the Element of (rng h1) /\ (rng tt) in rng t by A351;
then consider i1 being Element of NAT such that
A427: i1 in dom f and
A428: f /. i1 = the Element of (rng h1) /\ (rng tt) by A348, PARTFUN2:2;
consider n1, n2 being Element of NAT such that
A429: [n1,n2] in Indices G1 and
A430: f /. i1 = G1 * (n1,n2) by A173, A427;
reconsider Ln1 = Line (G1,n1) as FinSequence of (TOP-REAL 2) ;
A431: n2 in Seg (width G1) by A95, A429, ZFMISC_1:87;
A432: ( Seg (len Ln1) = dom Ln1 & len Ln1 = width G1 ) by FINSEQ_1:def_3, MATRIX_1:def_7;
then Ln1 /. n2 = Ln1 . n2 by A431, PARTFUN1:def_6;
then f /. i1 = Ln1 /. n2 by A430, A431, MATRIX_1:def_7;
then A433: f /. i1 in rng Ln1 by A431, A432, PARTFUN2:2;
n1 in dom G1 by A95, A429, ZFMISC_1:87;
then A434: mi <= n1 by A420, A427, A433;
the Element of (rng h1) /\ (rng tt) = G1 * (i2,K1) by A366, A423, A424;
then i2 = n1 by A428, A429, A430, A426, GOBOARD1:5;
hence contradiction by A434, A425, XXREAL_0:2; ::_thesis: verum
end;
defpred S10[ Element of NAT ] means ( $1 in dom f implies for m being Element of NAT st m in dom G1 & f /. $1 in rng (Line (G1,m)) holds
m <= ma );
A435: for k being Element of NAT st S10[k] holds
S10[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S10[k] implies S10[k + 1] )
assume A436: S10[k] ; ::_thesis: S10[k + 1]
assume A437: k + 1 in dom f ; ::_thesis: for m being Element of NAT st m in dom G1 & f /. (k + 1) in rng (Line (G1,m)) holds
m <= ma
let m be Element of NAT ; ::_thesis: ( m in dom G1 & f /. (k + 1) in rng (Line (G1,m)) implies m <= ma )
assume A438: ( m in dom G1 & f /. (k + 1) in rng (Line (G1,m)) ) ; ::_thesis: m <= ma
now__::_thesis:_m_<=_ma
percases ( k = 0 or k <> 0 ) ;
supposeA439: k = 0 ; ::_thesis: m <= ma
1 in Seg l by A157, FINSEQ_1:1;
then ( f /. 1 = (g1 | mi1) /. (w + 1) & (g1 | mi1) /. (w + 1) = g1 /. (w + 1) ) by A169, A154;
then f /. (k + 1) in rng Li by A50, A51, A439, PARTFUN2:2;
hence m <= ma by A39, A126, A438, GOBOARD1:3; ::_thesis: verum
end;
supposeA440: k <> 0 ; ::_thesis: m <= ma
A441: k + 1 <= len f by A176, A437, FINSEQ_1:1;
then A442: k <= len f by NAT_1:13;
consider j1, j2 being Element of NAT such that
A443: [j1,j2] in Indices G1 and
A444: f /. (k + 1) = G1 * (j1,j2) by A173, A437;
reconsider Lj1 = Line (G1,j1) as FinSequence of (TOP-REAL 2) ;
A445: j2 in Seg (width G1) by A95, A443, ZFMISC_1:87;
A446: ( Seg (len Lj1) = dom Lj1 & len Lj1 = width G1 ) by FINSEQ_1:def_3, MATRIX_1:def_7;
then Lj1 /. j2 = Lj1 . j2 by A445, PARTFUN1:def_6;
then f /. (k + 1) = Lj1 /. j2 by A444, A445, MATRIX_1:def_7;
then A447: f /. (k + 1) in rng Lj1 by A445, A446, PARTFUN2:2;
A448: j1 in dom G1 by A95, A443, ZFMISC_1:87;
then A449: j1 = m by A438, A447, GOBOARD1:3;
0 < k by A440, NAT_1:3;
then A450: 0 + 1 <= k by NAT_1:13;
then A451: k in dom f by A442, FINSEQ_3:25;
then consider i1, i2 being Element of NAT such that
A452: [i1,i2] in Indices G1 and
A453: f /. k = G1 * (i1,i2) by A173;
reconsider Li1 = Line (G1,i1) as FinSequence of (TOP-REAL 2) ;
A454: i2 in Seg (width G1) by A95, A452, ZFMISC_1:87;
A455: ( Seg (len Li1) = dom Li1 & len Li1 = width G1 ) by FINSEQ_1:def_3, MATRIX_1:def_7;
then Li1 /. i2 = Li1 . i2 by A454, PARTFUN1:def_6;
then f /. k = Li1 /. i2 by A453, A454, MATRIX_1:def_7;
then A456: f /. k in rng Li1 by A454, A455, PARTFUN2:2;
A457: i1 in dom G1 by A95, A452, ZFMISC_1:87;
then A458: i1 <= ma by A436, A450, A442, A456, FINSEQ_3:25;
now__::_thesis:_(_(_ma_=_i1_&_contradiction_)_or_(_i1_<_ma_&_m_<=_ma_)_)
percases ( ma = i1 or i1 < ma ) by A458, XXREAL_0:1;
caseA459: ma = i1 ; ::_thesis: contradiction
A460: w + 1 <= w + k by A450, XREAL_1:7;
A461: ( f /. k = (g1 | mi1) /. (w + k) & (g1 | mi1) /. (w + k) = g1 /. (w + k) ) by A169, A154, A156, A451;
then ma1 <> w + k by A39, A41, A46, A94, A456, A459, GOBOARD1:3;
then ma1 < w + k by A460, XXREAL_0:1;
then A462: mi1 <= w + k by A129, A169, A156, A451, A456, A459, A461;
w + k <= mi1 by A154, A155, A442, XREAL_1:7;
then w + k = mi1 by A462, XXREAL_0:1;
hence contradiction by A154, A441, NAT_1:13; ::_thesis: verum
end;
caseA463: i1 < ma ; ::_thesis: m <= ma
now__::_thesis:_m_<=_ma
percases ( f /. (k + 1) in rng (Line (G1,i1)) or for l being Element of NAT st f /. (k + 1) in rng (Line (G1,l)) & l in dom G1 holds
abs (i1 - l) = 1 ) by A347, A437, A451, A457, A456, GOBOARD1:27;
suppose f /. (k + 1) in rng (Line (G1,i1)) ; ::_thesis: m <= ma
hence m <= ma by A438, A457, A463, GOBOARD1:3; ::_thesis: verum
end;
suppose for l being Element of NAT st f /. (k + 1) in rng (Line (G1,l)) & l in dom G1 holds
abs (i1 - l) = 1 ; ::_thesis: m <= ma
then A464: abs (i1 - j1) = 1 by A448, A447;
now__::_thesis:_m_<=_ma
percases ( ( j1 < i1 & i1 = j1 + 1 ) or ( i1 < j1 & j1 = i1 + 1 ) ) by A464, SEQM_3:41;
suppose ( j1 < i1 & i1 = j1 + 1 ) ; ::_thesis: m <= ma
hence m <= ma by A449, A463, XXREAL_0:2; ::_thesis: verum
end;
suppose ( i1 < j1 & j1 = i1 + 1 ) ; ::_thesis: m <= ma
hence m <= ma by A449, A463, NAT_1:13; ::_thesis: verum
end;
end;
end;
hence m <= ma ; ::_thesis: verum
end;
end;
end;
hence m <= ma ; ::_thesis: verum
end;
end;
end;
hence m <= ma ; ::_thesis: verum
end;
end;
end;
hence m <= ma ; ::_thesis: verum
end;
A465: Seg (len h1) = dom h1 by FINSEQ_1:def_3;
A466: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_h2_holds_
ma_+_n_in_dom_G1
let n be Element of NAT ; ::_thesis: ( n in dom h2 implies ma + n in dom G1 )
A467: n <= n + ma by NAT_1:11;
assume A468: n in dom h2 ; ::_thesis: ma + n in dom G1
then n <= l2 by A418, FINSEQ_3:25;
then A469: ma + n <= ma + l2 by XREAL_1:7;
1 <= n by A468, FINSEQ_3:25;
then 1 <= n + ma by A467, XXREAL_0:2;
hence ma + n in dom G1 by A469, FINSEQ_3:25; ::_thesis: verum
end;
A470: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_h2_holds_
ex_m_being_Element_of_NAT_ex_K2_being_Element_of_NAT_st_
(_[m,K2]_in_Indices_G1_&_h2_/._n_=_G1_*_(m,K2)_)
let n be Element of NAT ; ::_thesis: ( n in dom h2 implies ex m being Element of NAT ex K2 being Element of NAT st
( [m,K2] in Indices G1 & h2 /. n = G1 * (m,K2) ) )
assume A471: n in dom h2 ; ::_thesis: ex m being Element of NAT ex K2 being Element of NAT st
( [m,K2] in Indices G1 & h2 /. n = G1 * (m,K2) )
take m = ma + n; ::_thesis: ex K2 being Element of NAT st
( [m,K2] in Indices G1 & h2 /. n = G1 * (m,K2) )
take K2 = K2; ::_thesis: ( [m,K2] in Indices G1 & h2 /. n = G1 * (m,K2) )
ma + n in dom G1 by A466, A471;
hence ( [m,K2] in Indices G1 & h2 /. n = G1 * (m,K2) ) by A95, A362, A352, A418, A471, ZFMISC_1:87; ::_thesis: verum
end;
A472: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_h2_&_n_+_1_in_dom_h2_holds_
for_i1,_i2,_j1,_j2_being_Element_of_NAT_st_[i1,i2]_in_Indices_G1_&_[j1,j2]_in_Indices_G1_&_h2_/._n_=_G1_*_(i1,i2)_&_h2_/._(n_+_1)_=_G1_*_(j1,j2)_holds_
(abs_(i1_-_j1))_+_(abs_(i2_-_j2))_=_1
let n be Element of NAT ; ::_thesis: ( n in dom h2 & n + 1 in dom h2 implies for i1, i2, j1, j2 being Element of NAT st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & h2 /. n = G1 * (i1,i2) & h2 /. (n + 1) = G1 * (j1,j2) holds
(abs (i1 - j1)) + (abs (i2 - j2)) = 1 )
assume that
A473: n in dom h2 and
A474: n + 1 in dom h2 ; ::_thesis: for i1, i2, j1, j2 being Element of NAT st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & h2 /. n = G1 * (i1,i2) & h2 /. (n + 1) = G1 * (j1,j2) holds
(abs (i1 - j1)) + (abs (i2 - j2)) = 1
ma + (n + 1) in dom G1 by A466, A474;
then A475: [((ma + n) + 1),K2] in Indices G1 by A95, A362, A352, ZFMISC_1:87;
let i1, i2, j1, j2 be Element of NAT ; ::_thesis: ( [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & h2 /. n = G1 * (i1,i2) & h2 /. (n + 1) = G1 * (j1,j2) implies (abs (i1 - j1)) + (abs (i2 - j2)) = 1 )
assume that
A476: [i1,i2] in Indices G1 and
A477: [j1,j2] in Indices G1 and
A478: h2 /. n = G1 * (i1,i2) and
A479: h2 /. (n + 1) = G1 * (j1,j2) ; ::_thesis: (abs (i1 - j1)) + (abs (i2 - j2)) = 1
h2 /. (n + 1) = G1 * ((ma + (n + 1)),K2) by A418, A474;
then A480: ( j1 = (ma + n) + 1 & j2 = K2 ) by A475, A477, A479, GOBOARD1:5;
ma + n in dom G1 by A466, A473;
then A481: [(ma + n),K2] in Indices G1 by A95, A362, A352, ZFMISC_1:87;
h2 /. n = G1 * ((ma + n),K2) by A418, A473;
then ( i1 = ma + n & i2 = K2 ) by A481, A476, A478, GOBOARD1:5;
hence (abs (i1 - j1)) + (abs (i2 - j2)) = (abs (((ma + n) - (ma + n)) + (- 1))) + 0 by A480, ABSVALUE:2
.= abs 1 by COMPLEX1:52
.= 1 by ABSVALUE:def_1 ;
::_thesis: verum
end;
A482: Seg (len h2) = dom h2 by FINSEQ_1:def_3;
A483: pl <= len (g2 | m) by A360, FINSEQ_3:25;
A484: 1 <= pl by A360, FINSEQ_3:25;
A485: pl <> pf by A39, A41, A94, A356, A360, GOBOARD1:3;
now__::_thesis:_1_+_1_<=_len_(g2_|_m)
percases ( pf < pl or pf > pl ) by A485, XXREAL_0:1;
suppose pf < pl ; ::_thesis: 1 + 1 <= len (g2 | m)
then pf < len (g2 | m) by A483, XXREAL_0:2;
then 1 < len (g2 | m) by A361, XXREAL_0:2;
hence 1 + 1 <= len (g2 | m) by NAT_1:13; ::_thesis: verum
end;
suppose pf > pl ; ::_thesis: 1 + 1 <= len (g2 | m)
then pl < len (g2 | m) by A415, XXREAL_0:2;
then 1 < len (g2 | m) by A484, XXREAL_0:2;
hence 1 + 1 <= len (g2 | m) by NAT_1:13; ::_thesis: verum
end;
end;
end;
then 1 <= (len (g2 | m)) - 1 by XREAL_1:19;
then A486: lg in dom (g2 | m) by A353, FINSEQ_3:25;
A487: S10[ 0 ] by FINSEQ_3:25;
A488: for n being Element of NAT holds S10[n] from NAT_1:sch_1(A487, A435);
A489: (rng h2) /\ (rng tt) = {}
proof
set x = the Element of (rng h2) /\ (rng tt);
assume A490: not (rng h2) /\ (rng tt) = {} ; ::_thesis: contradiction
then the Element of (rng h2) /\ (rng tt) in rng h2 by XBOOLE_0:def_4;
then consider i2 being Element of NAT such that
A491: i2 in dom h2 and
A492: h2 /. i2 = the Element of (rng h2) /\ (rng tt) by PARTFUN2:2;
0 + 1 <= i2 by A491, FINSEQ_3:25;
then A493: 0 < i2 by NAT_1:13;
ma + i2 in dom G1 by A466, A491;
then A494: [(ma + i2),K2] in Indices G1 by A95, A362, A352, ZFMISC_1:87;
the Element of (rng h2) /\ (rng tt) in rng tt by A490, XBOOLE_0:def_4;
then the Element of (rng h2) /\ (rng tt) in rng t by A351;
then consider i1 being Element of NAT such that
A495: i1 in dom f and
A496: f /. i1 = the Element of (rng h2) /\ (rng tt) by A348, PARTFUN2:2;
consider n1, n2 being Element of NAT such that
A497: [n1,n2] in Indices G1 and
A498: f /. i1 = G1 * (n1,n2) by A173, A495;
reconsider Ln1 = Line (G1,n1) as FinSequence of (TOP-REAL 2) ;
A499: n2 in Seg (width G1) by A95, A497, ZFMISC_1:87;
A500: ( Seg (len Ln1) = dom Ln1 & len Ln1 = width G1 ) by FINSEQ_1:def_3, MATRIX_1:def_7;
then Ln1 /. n2 = Ln1 . n2 by A499, PARTFUN1:def_6;
then f /. i1 = Ln1 /. n2 by A498, A499, MATRIX_1:def_7;
then A501: f /. i1 in rng Ln1 by A499, A500, PARTFUN2:2;
A502: n1 in dom G1 by A95, A497, ZFMISC_1:87;
the Element of (rng h2) /\ (rng tt) = G1 * ((ma + i2),K2) by A418, A491, A492;
then ma + i2 = n1 by A496, A497, A498, A494, GOBOARD1:5;
hence contradiction by A488, A495, A502, A501, A493, XREAL_1:29; ::_thesis: verum
end;
1 <= len (g2 | m) by A13, GOBOARD1:22;
then A503: len (g2 | m) in dom (g2 | m) by FINSEQ_3:25;
A504: dom (g2 | m) c= dom g2 by A23, A24, A16, A17, FINSEQ_1:5;
now__::_thesis:_not_pl_=_len_(g2_|_m)
consider i2 being Element of NAT such that
A505: i2 in dom C and
A506: C /. i2 = (g2 | m) /. (len (g2 | m)) by A28, PARTFUN2:2;
A507: dom C = Seg (len C) by FINSEQ_1:def_3
.= Seg (len G1) by MATRIX_1:def_8
.= dom G1 by FINSEQ_1:def_3 ;
then A508: [i2,(width G1)] in Indices G1 by A74, A95, A505, ZFMISC_1:87;
C /. i2 = C . i2 by A505, PARTFUN1:def_6;
then A509: (g2 | m) /. (len (g2 | m)) = G1 * (i2,(width G1)) by A505, A506, A507, MATRIX_1:def_8;
assume A510: pl = len (g2 | m) ; ::_thesis: contradiction
consider n1, n2 being Element of NAT such that
A511: [n1,n2] in Indices G1 and
A512: (g2 | m) /. lg = G1 * (n1,n2) by A15, A486, GOBOARD1:def_9;
A513: n1 in dom G1 by A95, A511, ZFMISC_1:87;
A514: n2 in Seg (width G1) by A95, A511, ZFMISC_1:87;
[ma,K2] in Indices G1 by A41, A95, A362, A352, ZFMISC_1:87;
then i2 = ma by A417, A510, A509, A508, GOBOARD1:5;
then A515: (abs (n1 - ma)) + (abs (n2 - (width G1))) = 1 by A15, A486, A503, A357, A509, A508, A511, A512, GOBOARD1:def_9;
now__::_thesis:_contradiction
percases ( ( abs (n1 - ma) = 1 & n2 = width G1 ) or ( abs (n2 - (width G1)) = 1 & n1 = ma ) ) by A515, SEQM_3:42;
supposeA516: ( abs (n1 - ma) = 1 & n2 = width G1 ) ; ::_thesis: contradiction
A517: dom C = Seg (len C) by FINSEQ_1:def_3
.= Seg (len G1) by MATRIX_1:def_8
.= dom G1 by FINSEQ_1:def_3 ;
then C /. n1 = C . n1 by A513, PARTFUN1:def_6;
then (g2 | m) /. lg = C /. n1 by A512, A513, A516, MATRIX_1:def_8;
then A518: (g2 | m) /. lg in rng C by A513, A517, PARTFUN2:2;
(g2 | m) /. lg = g2 /. lg by A13, A24, A17, A486, FINSEQ_4:71;
hence contradiction by A13, A17, A486, A504, A518, XREAL_1:44; ::_thesis: verum
end;
supposeA519: ( abs (n2 - (width G1)) = 1 & n1 = ma ) ; ::_thesis: contradiction
len Lma = width G1 by MATRIX_1:def_7;
then A520: n2 in dom Lma by A514, FINSEQ_1:def_3;
then La /. n2 = Lma . n2 by PARTFUN1:def_6;
then (g2 | m) /. lg = Lma /. n2 by A512, A514, A519, MATRIX_1:def_7;
then (g2 | m) /. lg in rng Lma by A520, PARTFUN2:2;
hence contradiction by A360, A486, A510, XREAL_1:44; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
then A521: pl < len (g2 | m) by A483, XXREAL_0:1;
len C = len G1 by MATRIX_1:def_8;
then A522: dom C = Seg (len G1) by FINSEQ_1:def_3
.= dom G1 by FINSEQ_1:def_3 ;
A523: Li /. K1 = Li . K1 by A364, PARTFUN1:def_6;
then A524: (g2 | m) /. pf = G1 * (mi,K1) by A364, A365, A397, MATRIX_1:def_7;
now__::_thesis:_not_pf_=_len_(g2_|_m)
consider i2 being Element of NAT such that
A525: i2 in dom C and
A526: C /. i2 = (g2 | m) /. (len (g2 | m)) by A28, PARTFUN2:2;
C /. i2 = C . i2 by A525, PARTFUN1:def_6;
then A527: (g2 | m) /. (len (g2 | m)) = G1 * (i2,(width G1)) by A522, A525, A526, MATRIX_1:def_8;
A528: [i2,(width G1)] in Indices G1 by A74, A95, A522, A525, ZFMISC_1:87;
assume A529: pf = len (g2 | m) ; ::_thesis: contradiction
consider n1, n2 being Element of NAT such that
A530: [n1,n2] in Indices G1 and
A531: (g2 | m) /. lg = G1 * (n1,n2) by A15, A486, GOBOARD1:def_9;
A532: n1 in dom G1 by A95, A530, ZFMISC_1:87;
A533: n2 in Seg (width G1) by A95, A530, ZFMISC_1:87;
[mi,K1] in Indices G1 by A39, A95, A364, A397, ZFMISC_1:87;
then i2 = mi by A524, A529, A527, A528, GOBOARD1:5;
then A534: (abs (n1 - mi)) + (abs (n2 - (width G1))) = 1 by A15, A486, A503, A357, A527, A528, A530, A531, GOBOARD1:def_9;
now__::_thesis:_contradiction
percases ( ( abs (n1 - mi) = 1 & n2 = width G1 ) or ( abs (n2 - (width G1)) = 1 & n1 = mi ) ) by A534, SEQM_3:42;
supposeA535: ( abs (n1 - mi) = 1 & n2 = width G1 ) ; ::_thesis: contradiction
A536: dom C = Seg (len C) by FINSEQ_1:def_3
.= Seg (len G1) by MATRIX_1:def_8
.= dom G1 by FINSEQ_1:def_3 ;
then C /. n1 = C . n1 by A532, PARTFUN1:def_6;
then (g2 | m) /. lg = C /. n1 by A531, A532, A535, MATRIX_1:def_8;
then A537: (g2 | m) /. lg in rng C by A532, A536, PARTFUN2:2;
(g2 | m) /. lg = g2 /. lg by A13, A24, A17, A486, FINSEQ_4:71;
hence contradiction by A13, A17, A486, A504, A537, XREAL_1:44; ::_thesis: verum
end;
supposeA538: ( abs (n2 - (width G1)) = 1 & n1 = mi ) ; ::_thesis: contradiction
len Li = width G1 by MATRIX_1:def_7;
then A539: n2 in dom Li by A533, FINSEQ_1:def_3;
then Li /. n2 = Li . n2 by PARTFUN1:def_6;
then (g2 | m) /. lg = Li /. n2 by A531, A533, A538, MATRIX_1:def_7;
then (g2 | m) /. lg in rng Li by A539, PARTFUN2:2;
hence contradiction by A356, A486, A529, XREAL_1:44; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
then A540: pf < len (g2 | m) by A415, XXREAL_0:1;
now__::_thesis:_(rng_g1)_/\_(rng_g2)_<>_{}
percases ( pf < pl or pl < pf ) by A485, XXREAL_0:1;
supposeA541: pf < pl ; ::_thesis: (rng g1) /\ (rng g2) <> {}
pl <= pl + 1 by NAT_1:11;
then reconsider LL = (pl + 1) - pf as Element of NAT by A541, INT_1:5, XXREAL_0:2;
reconsider w1 = pf - 1 as Element of NAT by A361, INT_1:5;
set F1 = (g2 | m) | pl;
defpred S11[ Nat, Element of (TOP-REAL 2)] means $2 = ((g2 | m) | pl) /. (w1 + $1);
A542: for n being Nat st n in Seg LL holds
ex p being Point of (TOP-REAL 2) st S11[n,p] ;
consider F being FinSequence of (TOP-REAL 2) such that
A543: ( len F = LL & ( for n being Nat st n in Seg LL holds
S11[n,F /. n] ) ) from FINSEQ_4:sch_1(A542);
set hf = h1 ^ F;
set FF = (h1 ^ F) ^ h2;
A544: Seg (len F) = dom F by FINSEQ_1:def_3;
A545: for n being Element of NAT st n in Seg LL holds
( ((g2 | m) | pl) /. (w1 + n) = (g2 | m) /. (w1 + n) & w1 + n in dom (g2 | m) )
proof
0 + 1 <= pf by A24, A356, FINSEQ_1:1;
then A546: 0 <= w1 by XREAL_1:19;
let n be Element of NAT ; ::_thesis: ( n in Seg LL implies ( ((g2 | m) | pl) /. (w1 + n) = (g2 | m) /. (w1 + n) & w1 + n in dom (g2 | m) ) )
assume A547: n in Seg LL ; ::_thesis: ( ((g2 | m) | pl) /. (w1 + n) = (g2 | m) /. (w1 + n) & w1 + n in dom (g2 | m) )
n <= LL by A547, FINSEQ_1:1;
then n + pf <= LL + pf by XREAL_1:7;
then A548: (n + pf) - 1 <= pl by XREAL_1:20;
1 <= n by A547, FINSEQ_1:1;
then 0 + 1 <= w1 + n by A546, XREAL_1:7;
then w1 + n in Seg pl by A548, FINSEQ_1:1;
hence ( ((g2 | m) | pl) /. (w1 + n) = (g2 | m) /. (w1 + n) & w1 + n in dom (g2 | m) ) by A360, FINSEQ_4:71; ::_thesis: verum
end;
A549: rng F c= rng g2
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng F or x in rng g2 )
assume x in rng F ; ::_thesis: x in rng g2
then consider n being Element of NAT such that
A550: n in dom F and
A551: x = F /. n by PARTFUN2:2;
F /. n = ((g2 | m) | pl) /. (w1 + n) by A543, A544, A550;
then A552: F /. n = (g2 | m) /. (w1 + n) by A545, A543, A544, A550;
w1 + n in dom (g2 | m) by A545, A543, A544, A550;
then x in rng (g2 | m) by A551, A552, PARTFUN2:2;
hence x in rng g2 by A18; ::_thesis: verum
end;
pf + 1 <= pl by A541, NAT_1:13;
then pf + 1 <= pl + 1 by NAT_1:13;
then A553: 1 <= LL by XREAL_1:19;
A554: now__::_thesis:_for_i1,_i2,_j1,_j2_being_Element_of_NAT_st_[i1,i2]_in_Indices_G1_&_[j1,j2]_in_Indices_G1_&_(h1_^_F)_/._(len_(h1_^_F))_=_G1_*_(i1,i2)_&_h2_/._1_=_G1_*_(j1,j2)_&_len_(h1_^_F)_in_dom_(h1_^_F)_&_1_in_dom_h2_holds_
(abs_(i1_-_j1))_+_(abs_(i2_-_j2))_=_1
let i1, i2, j1, j2 be Element of NAT ; ::_thesis: ( [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & (h1 ^ F) /. (len (h1 ^ F)) = G1 * (i1,i2) & h2 /. 1 = G1 * (j1,j2) & len (h1 ^ F) in dom (h1 ^ F) & 1 in dom h2 implies (abs (i1 - j1)) + (abs (i2 - j2)) = 1 )
assume that
A555: [i1,i2] in Indices G1 and
A556: [j1,j2] in Indices G1 and
A557: (h1 ^ F) /. (len (h1 ^ F)) = G1 * (i1,i2) and
A558: h2 /. 1 = G1 * (j1,j2) and
len (h1 ^ F) in dom (h1 ^ F) and
A559: 1 in dom h2 ; ::_thesis: (abs (i1 - j1)) + (abs (i2 - j2)) = 1
ma + 1 in dom G1 by A466, A559;
then A560: [(ma + 1),K2] in Indices G1 by A95, A362, A352, ZFMISC_1:87;
A561: [ma,K2] in Indices G1 by A41, A95, A362, A352, ZFMISC_1:87;
A562: len F in dom F by A543, A544, A553, FINSEQ_1:1;
(h1 ^ F) /. (len (h1 ^ F)) = (h1 ^ F) /. ((len h1) + (len F)) by FINSEQ_1:22
.= F /. (len F) by A562, FINSEQ_4:69
.= ((g2 | m) | pl) /. (w1 + LL) by A543, A544, A562
.= G1 * (ma,K2) by A417, A545, A543, A544, A562 ;
then A563: ( i1 = ma & i2 = K2 ) by A555, A557, A561, GOBOARD1:5;
h2 /. 1 = G1 * ((ma + 1),K2) by A418, A559;
then ( j1 = ma + 1 & j2 = K2 ) by A556, A558, A560, GOBOARD1:5;
hence (abs (i1 - j1)) + (abs (i2 - j2)) = (abs (ma - (ma + 1))) + 0 by A563, ABSVALUE:2
.= abs (- ((ma + 1) - ma))
.= abs 1 by COMPLEX1:52
.= 1 by ABSVALUE:def_1 ;
::_thesis: verum
end;
A564: rng ((h1 ^ F) ^ h2) = (rng (h1 ^ F)) \/ (rng h2) by FINSEQ_1:31
.= ((rng h1) \/ (rng F)) \/ (rng h2) by FINSEQ_1:31 ;
A565: for k being Element of NAT st k in Seg (width G1) & (rng F) /\ (rng (Col (G1,k))) = {} holds
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = {}
proof
A566: len (Col (G1,K2)) = len G1 by MATRIX_1:def_8;
A567: len (Col (G1,K1)) = len G1 by MATRIX_1:def_8;
let k be Element of NAT ; ::_thesis: ( k in Seg (width G1) & (rng F) /\ (rng (Col (G1,k))) = {} implies (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = {} )
assume that
A568: k in Seg (width G1) and
A569: (rng F) /\ (rng (Col (G1,k))) = {} ; ::_thesis: (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = {}
set gg = Col (G1,k);
assume A570: (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) <> {} ; ::_thesis: contradiction
set x = the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k)));
rng ((h1 ^ F) ^ h2) = (rng F) \/ ((rng h1) \/ (rng h2)) by A564, XBOOLE_1:4;
then A571: (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = {} \/ (((rng h1) \/ (rng h2)) /\ (rng (Col (G1,k)))) by A569, XBOOLE_1:23
.= ((rng h1) /\ (rng (Col (G1,k)))) \/ ((rng h2) /\ (rng (Col (G1,k)))) by XBOOLE_1:23 ;
now__::_thesis:_contradiction
percases ( the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in (rng h1) /\ (rng (Col (G1,k))) or the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in (rng h2) /\ (rng (Col (G1,k))) ) by A570, A571, XBOOLE_0:def_3;
supposeA572: the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in (rng h1) /\ (rng (Col (G1,k))) ; ::_thesis: contradiction
then the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in rng h1 by XBOOLE_0:def_4;
then consider i being Element of NAT such that
A573: i in dom h1 and
A574: the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = h1 /. i by PARTFUN2:2;
A575: the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = G1 * (i,K1) by A366, A573, A574;
reconsider y = the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) as Point of (TOP-REAL 2) by A574;
A576: Lmi /. K1 = Lmi . K1 by A364, PARTFUN1:def_6;
A577: the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in rng (Col (G1,k)) by A572, XBOOLE_0:def_4;
A578: dom CK1 = Seg (len G1) by A567, FINSEQ_1:def_3
.= dom G1 by FINSEQ_1:def_3 ;
then A579: CK1 /. mi = CK1 . mi by A39, PARTFUN1:def_6;
A580: i in dom CK1 by A398, A573, A578;
CK1 /. i = CK1 . i by A398, A573, A578, PARTFUN1:def_6;
then y = CK1 /. i by A575, A578, A580, MATRIX_1:def_8;
then y in rng CK1 by A580, PARTFUN2:2;
then A581: K1 = k by A364, A397, A568, A577, GOBOARD1:4;
A582: 1 in Seg LL by A553, FINSEQ_1:1;
then ( F /. 1 = ((g2 | m) | pl) /. (w1 + 1) & ((g2 | m) | pl) /. (w1 + 1) = (g2 | m) /. (w1 + 1) ) by A545, A543;
then F /. 1 = CK1 /. mi by A39, A364, A365, A397, A576, A579, GOBOARD1:2;
then A583: F /. 1 in rng (Col (G1,k)) by A39, A578, A581, PARTFUN2:2;
F /. 1 in rng F by A543, A544, A582, PARTFUN2:2;
hence contradiction by A569, A583, XBOOLE_0:def_4; ::_thesis: verum
end;
supposeA584: the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in (rng h2) /\ (rng (Col (G1,k))) ; ::_thesis: contradiction
then the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in rng h2 by XBOOLE_0:def_4;
then consider i being Element of NAT such that
A585: i in dom h2 and
A586: the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = h2 /. i by PARTFUN2:2;
A587: the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = G1 * ((ma + i),K2) by A418, A585, A586;
reconsider y = the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) as Point of (TOP-REAL 2) by A586;
A588: Lma /. K2 = Lma . K2 by A362, PARTFUN1:def_6;
A589: the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in rng (Col (G1,k)) by A584, XBOOLE_0:def_4;
A590: dom CK2 = Seg (len G1) by A566, FINSEQ_1:def_3
.= dom G1 by FINSEQ_1:def_3 ;
then A591: CK2 /. ma = CK2 . ma by A41, PARTFUN1:def_6;
A592: ma + i in dom CK2 by A466, A585, A590;
CK2 /. (ma + i) = CK2 . (ma + i) by A466, A585, A590, PARTFUN1:def_6;
then y = CK2 /. (ma + i) by A587, A590, A592, MATRIX_1:def_8;
then y in rng CK2 by A592, PARTFUN2:2;
then A593: K2 = k by A362, A352, A568, A589, GOBOARD1:4;
A594: LL in Seg LL by A553, FINSEQ_1:1;
then ( F /. LL = ((g2 | m) | pl) /. (w1 + LL) & ((g2 | m) | pl) /. (w1 + LL) = (g2 | m) /. (w1 + LL) ) by A545, A543;
then F /. LL = CK2 /. ma by A41, A362, A363, A352, A588, A591, GOBOARD1:2;
then A595: F /. LL in rng (Col (G1,k)) by A41, A590, A593, PARTFUN2:2;
F /. LL in rng F by A543, A544, A594, PARTFUN2:2;
hence contradiction by A569, A595, XBOOLE_0:def_4; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
(rng F) /\ (rng C) = {}
proof
reconsider w = w1 as Element of NAT ;
set x = the Element of (rng F) /\ (rng C);
assume A596: not (rng F) /\ (rng C) = {} ; ::_thesis: contradiction
then A597: the Element of (rng F) /\ (rng C) in rng C by XBOOLE_0:def_4;
the Element of (rng F) /\ (rng C) in rng F by A596, XBOOLE_0:def_4;
then consider i1 being Element of NAT such that
A598: i1 in dom F and
A599: F /. i1 = the Element of (rng F) /\ (rng C) by PARTFUN2:2;
A600: Seg (len F) = dom F by FINSEQ_1:def_3;
then i1 <= LL by A543, A598, FINSEQ_1:1;
then A601: w + i1 <= w + LL by XREAL_1:7;
A602: w1 + i1 in dom (g2 | m) by A545, A543, A598, A600;
then A603: w + i1 in dom g2 by A13, A24, A17, FINSEQ_4:71;
( F /. i1 = ((g2 | m) | pl) /. (w1 + i1) & ((g2 | m) | pl) /. (w1 + i1) = (g2 | m) /. (w1 + i1) ) by A545, A543, A598, A600;
then g2 /. (w + i1) in rng C by A13, A24, A17, A597, A599, A602, FINSEQ_4:71;
then m <= w + i1 by A13, A603;
hence contradiction by A17, A521, A601, XXREAL_0:2; ::_thesis: verum
end;
then (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,(width G1)))) = {} by A74, A565;
then A604: rng ((h1 ^ F) ^ h2) misses rng (Col (G1,(width G1))) by XBOOLE_0:def_7;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_F_holds_
ex_i,_j_being_Element_of_NAT_st_
(_[i,j]_in_Indices_G1_&_F_/._n_=_G1_*_(i,j)_)
reconsider w = w1 as Element of NAT ;
let n be Element of NAT ; ::_thesis: ( n in dom F implies ex i, j being Element of NAT st
( [i,j] in Indices G1 & F /. n = G1 * (i,j) ) )
assume A605: n in dom F ; ::_thesis: ex i, j being Element of NAT st
( [i,j] in Indices G1 & F /. n = G1 * (i,j) )
then w1 + n in dom (g2 | m) by A545, A543, A544;
then consider i, j being Element of NAT such that
A606: ( [i,j] in Indices G1 & (g2 | m) /. (w + n) = G1 * (i,j) ) by A15, GOBOARD1:def_9;
take i = i; ::_thesis: ex j being Element of NAT st
( [i,j] in Indices G1 & F /. n = G1 * (i,j) )
take j = j; ::_thesis: ( [i,j] in Indices G1 & F /. n = G1 * (i,j) )
F /. n = ((g2 | m) | pl) /. (w1 + n) by A543, A544, A605;
hence ( [i,j] in Indices G1 & F /. n = G1 * (i,j) ) by A545, A543, A544, A605, A606; ::_thesis: verum
end;
then for n being Element of NAT st n in dom (h1 ^ F) holds
ex i, j being Element of NAT st
( [i,j] in Indices G1 & (h1 ^ F) /. n = G1 * (i,j) ) by A403, GOBOARD1:23;
then A607: for n being Element of NAT st n in dom ((h1 ^ F) ^ h2) holds
ex i, j being Element of NAT st
( [i,j] in Indices G1 & ((h1 ^ F) ^ h2) /. n = G1 * (i,j) ) by A470, GOBOARD1:23;
A608: now__::_thesis:_for_i1,_i2,_j1,_j2_being_Element_of_NAT_st_[i1,i2]_in_Indices_G1_&_[j1,j2]_in_Indices_G1_&_h1_/._(len_h1)_=_G1_*_(i1,i2)_&_F_/._1_=_G1_*_(j1,j2)_&_len_h1_in_dom_h1_&_1_in_dom_F_holds_
(abs_(i1_-_j1))_+_(abs_(i2_-_j2))_=_1
A609: [mi,K1] in Indices G1 by A39, A95, A364, A397, ZFMISC_1:87;
let i1, i2, j1, j2 be Element of NAT ; ::_thesis: ( [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & h1 /. (len h1) = G1 * (i1,i2) & F /. 1 = G1 * (j1,j2) & len h1 in dom h1 & 1 in dom F implies (abs (i1 - j1)) + (abs (i2 - j2)) = 1 )
assume that
A610: [i1,i2] in Indices G1 and
A611: [j1,j2] in Indices G1 and
A612: h1 /. (len h1) = G1 * (i1,i2) and
A613: F /. 1 = G1 * (j1,j2) and
A614: len h1 in dom h1 and
A615: 1 in dom F ; ::_thesis: (abs (i1 - j1)) + (abs (i2 - j2)) = 1
F /. 1 = ((g2 | m) | pl) /. (w1 + 1) by A543, A544, A615;
then F /. 1 = (g2 | m) /. (w1 + 1) by A545, A543, A544, A615
.= G1 * (mi,K1) by A364, A365, A397, A523, MATRIX_1:def_7 ;
then A616: ( j1 = mi & j2 = K1 ) by A611, A613, A609, GOBOARD1:5;
l1 in dom G1 by A366, A398, A614;
then A617: [l1,K1] in Indices G1 by A95, A364, A397, ZFMISC_1:87;
h1 /. (len h1) = G1 * (l1,K1) by A366, A614;
then ( i1 = l1 & i2 = K1 ) by A610, A612, A617, GOBOARD1:5;
hence (abs (i1 - j1)) + (abs (i2 - j2)) = (abs ((mi - 1) - mi)) + 0 by A616, ABSVALUE:2
.= abs (- 1)
.= abs 1 by COMPLEX1:52
.= 1 by ABSVALUE:def_1 ;
::_thesis: verum
end;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_F_&_n_+_1_in_dom_F_holds_
for_i1,_i2,_j1,_j2_being_Element_of_NAT_st_[i1,i2]_in_Indices_G1_&_[j1,j2]_in_Indices_G1_&_F_/._n_=_G1_*_(i1,i2)_&_F_/._(n_+_1)_=_G1_*_(j1,j2)_holds_
(abs_(i1_-_j1))_+_(abs_(i2_-_j2))_=_1
let n be Element of NAT ; ::_thesis: ( n in dom F & n + 1 in dom F implies for i1, i2, j1, j2 being Element of NAT st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & F /. n = G1 * (i1,i2) & F /. (n + 1) = G1 * (j1,j2) holds
(abs (i1 - j1)) + (abs (i2 - j2)) = 1 )
assume that
A618: n in dom F and
A619: n + 1 in dom F ; ::_thesis: for i1, i2, j1, j2 being Element of NAT st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & F /. n = G1 * (i1,i2) & F /. (n + 1) = G1 * (j1,j2) holds
(abs (i1 - j1)) + (abs (i2 - j2)) = 1
F /. n = ((g2 | m) | pl) /. (w1 + n) by A543, A544, A618;
then A620: F /. n = (g2 | m) /. (w1 + n) by A545, A543, A544, A618;
F /. (n + 1) = ((g2 | m) | pl) /. (w1 + (n + 1)) by A543, A544, A619;
then A621: ( (w1 + n) + 1 in dom (g2 | m) & F /. (n + 1) = (g2 | m) /. ((w1 + n) + 1) ) by A545, A543, A544, A619;
let i1, i2, j1, j2 be Element of NAT ; ::_thesis: ( [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & F /. n = G1 * (i1,i2) & F /. (n + 1) = G1 * (j1,j2) implies (abs (i1 - j1)) + (abs (i2 - j2)) = 1 )
assume A622: ( [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & F /. n = G1 * (i1,i2) & F /. (n + 1) = G1 * (j1,j2) ) ; ::_thesis: (abs (i1 - j1)) + (abs (i2 - j2)) = 1
w1 + n in dom (g2 | m) by A545, A543, A544, A618;
hence (abs (i1 - j1)) + (abs (i2 - j2)) = 1 by A15, A620, A621, A622, GOBOARD1:def_9; ::_thesis: verum
end;
then for n being Element of NAT st n in dom (h1 ^ F) & n + 1 in dom (h1 ^ F) holds
for i1, i2, j1, j2 being Element of NAT st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & (h1 ^ F) /. n = G1 * (i1,i2) & (h1 ^ F) /. (n + 1) = G1 * (j1,j2) holds
(abs (i1 - j1)) + (abs (i2 - j2)) = 1 by A405, A608, GOBOARD1:24;
then for n being Element of NAT st n in dom ((h1 ^ F) ^ h2) & n + 1 in dom ((h1 ^ F) ^ h2) holds
for i1, i2, j1, j2 being Element of NAT st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & ((h1 ^ F) ^ h2) /. n = G1 * (i1,i2) & ((h1 ^ F) ^ h2) /. (n + 1) = G1 * (j1,j2) holds
(abs (i1 - j1)) + (abs (i2 - j2)) = 1 by A472, A554, GOBOARD1:24;
then (h1 ^ F) ^ h2 is_sequence_on G1 by A607, GOBOARD1:def_9;
then A623: (h1 ^ F) ^ h2 is_sequence_on DelCol (G1,(width G1)) by A74, A151, A604, GOBOARD1:25;
set x = the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng tt);
0 + 0 <= (len h1) + (len h2) by NAT_1:2;
then A624: 0 + 1 <= (len F) + ((len h1) + (len h2)) by A543, A553, XREAL_1:7;
A625: now__::_thesis:_((h1_^_F)_^_h2)_/._1_in_rng_(Line_(G1,1))
percases ( mi = 1 or mi <> 1 ) ;
supposeA626: mi = 1 ; ::_thesis: ((h1 ^ F) ^ h2) /. 1 in rng (Line (G1,1))
A627: pf in Seg pl by A361, A541, FINSEQ_1:1;
A628: 1 in Seg LL by A553, FINSEQ_1:1;
h1 = {} by A366, A626;
then (h1 ^ F) ^ h2 = F ^ h2 by FINSEQ_1:34;
then ((h1 ^ F) ^ h2) /. 1 = F /. 1 by A543, A544, A628, FINSEQ_4:68
.= ((g2 | m) | pl) /. (w1 + 1) by A543, A628
.= (g2 | m) /. pf by A360, A627, FINSEQ_4:71 ;
hence ((h1 ^ F) ^ h2) /. 1 in rng (Line (G1,1)) by A356, A626; ::_thesis: verum
end;
supposeA629: mi <> 1 ; ::_thesis: ((h1 ^ F) ^ h2) /. 1 in rng (Line (G1,1))
1 <= mi by A39, FINSEQ_3:25;
then 1 < mi by A629, XXREAL_0:1;
then 1 + 1 <= mi by NAT_1:13;
then A630: 1 <= l1 by XREAL_1:19;
then A631: 1 in Seg l1 by FINSEQ_1:1;
len (Line (G1,1)) = width G1 by MATRIX_1:def_7;
then A632: K1 in dom L1 by A364, A397, FINSEQ_1:def_3;
then A633: L1 /. K1 = L1 . K1 by PARTFUN1:def_6;
( len (h1 ^ F) = (len h1) + (len F) & 0 <= len F ) by FINSEQ_1:22, NAT_1:2;
then 0 + 1 <= len (h1 ^ F) by A366, A630, XREAL_1:7;
then 1 in dom (h1 ^ F) by FINSEQ_3:25;
then ((h1 ^ F) ^ h2) /. 1 = (h1 ^ F) /. 1 by FINSEQ_4:68
.= h1 /. 1 by A366, A465, A631, FINSEQ_4:68
.= G1 * (1,K1) by A366, A465, A631
.= L1 /. K1 by A364, A397, A633, MATRIX_1:def_7 ;
hence ((h1 ^ F) ^ h2) /. 1 in rng (Line (G1,1)) by A632, PARTFUN2:2; ::_thesis: verum
end;
end;
end;
A634: w1 + LL = pl ;
A635: now__::_thesis:_((h1_^_F)_^_h2)_/._(len_((h1_^_F)_^_h2))_in_rng_(Line_(G1,(len_G1)))
percases ( ma = len G1 or ma <> len G1 ) ;
supposeA636: ma = len G1 ; ::_thesis: ((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) in rng (Line (G1,(len G1)))
1 <= pl by A24, A360, FINSEQ_1:1;
then A637: pl in Seg pl by FINSEQ_1:1;
A638: len F in dom F by A543, A553, FINSEQ_3:25;
h2 = {} by A418, A636;
then A639: (h1 ^ F) ^ h2 = h1 ^ F by FINSEQ_1:34;
then ((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) = ((h1 ^ F) ^ h2) /. ((len h1) + (len F)) by FINSEQ_1:22
.= F /. LL by A543, A639, A638, FINSEQ_4:69
.= ((g2 | m) | pl) /. pl by A543, A544, A634, A638
.= (g2 | m) /. pl by A360, A637, FINSEQ_4:71 ;
hence ((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) in rng (Line (G1,(len G1))) by A360, A636; ::_thesis: verum
end;
supposeA640: ma <> len G1 ; ::_thesis: ((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) in rng (Line (G1,(len G1)))
ma <= len G1 by A41, FINSEQ_3:25;
then ma < len G1 by A640, XXREAL_0:1;
then ma + 1 <= len G1 by NAT_1:13;
then A641: 1 <= l2 by XREAL_1:19;
then A642: l2 in Seg l2 by FINSEQ_1:1;
len (Line (G1,(len G1))) = width G1 by MATRIX_1:def_7;
then A643: K2 in dom Ll by A362, A352, FINSEQ_1:def_3;
then A644: Ll /. K2 = Ll . K2 by PARTFUN1:def_6;
A645: len h2 in dom h2 by A418, A641, FINSEQ_3:25;
((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) = ((h1 ^ F) ^ h2) /. ((len (h1 ^ F)) + (len h2)) by FINSEQ_1:22
.= h2 /. l2 by A418, A645, FINSEQ_4:69
.= G1 * ((ma + l2),K2) by A418, A482, A642
.= Ll /. K2 by A362, A352, A644, MATRIX_1:def_7 ;
hence ((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) in rng (Line (G1,(len G1))) by A643, PARTFUN2:2; ::_thesis: verum
end;
end;
end;
rng tt c= rng f by A348, A351, XBOOLE_1:1;
then A646: rng tt c= rng g1 by A177, XBOOLE_1:1;
A647: len ((h1 ^ F) ^ h2) = (len (h1 ^ F)) + (len h2) by FINSEQ_1:22
.= ((len h1) + (len F)) + (len h2) by FINSEQ_1:22 ;
then 1 in dom ((h1 ^ F) ^ h2) by A624, FINSEQ_3:25;
then A648: ((h1 ^ F) ^ h2) /. 1 in rng (Line ((DelCol (G1,(width G1))),1)) by A74, A26, A151, A625, A604, GOBOARD1:21;
len ((h1 ^ F) ^ h2) in dom ((h1 ^ F) ^ h2) by A647, A624, FINSEQ_3:25;
then A649: ((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) in rng (Line ((DelCol (G1,(width G1))),(len (DelCol (G1,(width G1)))))) by A74, A27, A151, A152, A635, A604, GOBOARD1:21;
width (DelCol (G1,(width G1))) = k by A3, A74, A92, GOBOARD1:10, NAT_1:3;
then (rng ((h1 ^ F) ^ h2)) /\ (rng tt) <> {} by A2, A93, A350, A647, A624, A623, A648, A649;
then A650: the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng tt) in (rng ((h1 ^ F) ^ h2)) /\ (rng tt) ;
(rng tt) /\ (rng ((h1 ^ F) ^ h2)) = (((rng h1) \/ (rng F)) /\ (rng tt)) \/ {} by A489, A564, XBOOLE_1:23
.= {} \/ ((rng F) /\ (rng tt)) by A421, XBOOLE_1:23
.= (rng tt) /\ (rng F) ;
then (rng ((h1 ^ F) ^ h2)) /\ (rng tt) c= (rng g1) /\ (rng g2) by A646, A549, XBOOLE_1:27;
hence (rng g1) /\ (rng g2) <> {} by A650; ::_thesis: verum
end;
supposeA651: pl < pf ; ::_thesis: (rng g1) /\ (rng g2) <> {}
pf <= pf + 1 by NAT_1:11;
then reconsider LL = (pf + 1) - pl as Element of NAT by A651, INT_1:5, XXREAL_0:2;
set F1 = (g2 | m) | pf;
defpred S11[ Nat, Element of (TOP-REAL 2)] means for k being Element of NAT st k = (pf + 1) - $1 holds
$2 = ((g2 | m) | pf) /. k;
A652: for n, k being Element of NAT st n in Seg LL & k = (pf + 1) - n holds
( ((g2 | m) | pf) /. k = (g2 | m) /. k & k in dom (g2 | m) )
proof
let n, k be Element of NAT ; ::_thesis: ( n in Seg LL & k = (pf + 1) - n implies ( ((g2 | m) | pf) /. k = (g2 | m) /. k & k in dom (g2 | m) ) )
assume that
A653: n in Seg LL and
A654: k = (pf + 1) - n ; ::_thesis: ( ((g2 | m) | pf) /. k = (g2 | m) /. k & k in dom (g2 | m) )
A655: n <= LL by A653, FINSEQ_1:1;
1 <= n by A653, FINSEQ_1:1;
then A656: (pf + 1) - n <= (pf + 1) - 1 by XREAL_1:13;
0 <= pl by NAT_1:2;
then LL <= (pf + 1) - 0 by XREAL_1:13;
then reconsider w = (pf + 1) - n as Element of NAT by A655, INT_1:5, XXREAL_0:2;
(pf + 1) - LL <= (pf + 1) - n by A655, XREAL_1:13;
then 1 <= (pf + 1) - n by A484, XXREAL_0:2;
then w in Seg pf by A656, FINSEQ_1:1;
hence ( ((g2 | m) | pf) /. k = (g2 | m) /. k & k in dom (g2 | m) ) by A356, A654, FINSEQ_4:71; ::_thesis: verum
end;
A657: for n being Element of NAT st n in Seg LL holds
(pf + 1) - n is Element of NAT
proof
let n be Element of NAT ; ::_thesis: ( n in Seg LL implies (pf + 1) - n is Element of NAT )
0 <= pl by NAT_1:2;
then A658: LL <= (pf + 1) - 0 by XREAL_1:13;
assume n in Seg LL ; ::_thesis: (pf + 1) - n is Element of NAT
then n <= LL by FINSEQ_1:1;
hence (pf + 1) - n is Element of NAT by A658, INT_1:5, XXREAL_0:2; ::_thesis: verum
end;
A659: for n being Nat st n in Seg LL holds
ex p being Point of (TOP-REAL 2) st S11[n,p]
proof
let n be Nat; ::_thesis: ( n in Seg LL implies ex p being Point of (TOP-REAL 2) st S11[n,p] )
assume A660: n in Seg LL ; ::_thesis: ex p being Point of (TOP-REAL 2) st S11[n,p]
then reconsider k = (pf + 1) - n as Element of NAT by A657;
take (g2 | m) /. k ; ::_thesis: S11[n,(g2 | m) /. k]
thus S11[n,(g2 | m) /. k] by A652, A660; ::_thesis: verum
end;
consider F being FinSequence of (TOP-REAL 2) such that
A661: ( len F = LL & ( for n being Nat st n in Seg LL holds
S11[n,F /. n] ) ) from FINSEQ_4:sch_1(A659);
set hf = h1 ^ F;
set FF = (h1 ^ F) ^ h2;
A662: Seg (len F) = dom F by FINSEQ_1:def_3;
A663: rng F c= rng g2
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng F or x in rng g2 )
assume x in rng F ; ::_thesis: x in rng g2
then consider n being Element of NAT such that
A664: n in dom F and
A665: x = F /. n by PARTFUN2:2;
reconsider u = (pf + 1) - n as Element of NAT by A657, A661, A662, A664;
F /. n = ((g2 | m) | pf) /. u by A661, A662, A664;
then ( (pf + 1) - n in dom (g2 | m) & F /. n = (g2 | m) /. u ) by A652, A661, A662, A664;
then x in rng (g2 | m) by A665, PARTFUN2:2;
hence x in rng g2 by A18; ::_thesis: verum
end;
pl + 1 <= pf by A651, NAT_1:13;
then pl + 1 <= pf + 1 by NAT_1:13;
then A666: 1 <= LL by XREAL_1:19;
A667: now__::_thesis:_for_i1,_i2,_j1,_j2_being_Element_of_NAT_st_[i1,i2]_in_Indices_G1_&_[j1,j2]_in_Indices_G1_&_(h1_^_F)_/._(len_(h1_^_F))_=_G1_*_(i1,i2)_&_h2_/._1_=_G1_*_(j1,j2)_&_len_(h1_^_F)_in_dom_(h1_^_F)_&_1_in_dom_h2_holds_
(abs_(i1_-_j1))_+_(abs_(i2_-_j2))_=_1
reconsider u = (pf + 1) - LL as Element of NAT ;
let i1, i2, j1, j2 be Element of NAT ; ::_thesis: ( [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & (h1 ^ F) /. (len (h1 ^ F)) = G1 * (i1,i2) & h2 /. 1 = G1 * (j1,j2) & len (h1 ^ F) in dom (h1 ^ F) & 1 in dom h2 implies (abs (i1 - j1)) + (abs (i2 - j2)) = 1 )
assume that
A668: [i1,i2] in Indices G1 and
A669: [j1,j2] in Indices G1 and
A670: (h1 ^ F) /. (len (h1 ^ F)) = G1 * (i1,i2) and
A671: h2 /. 1 = G1 * (j1,j2) and
len (h1 ^ F) in dom (h1 ^ F) and
A672: 1 in dom h2 ; ::_thesis: (abs (i1 - j1)) + (abs (i2 - j2)) = 1
ma + 1 in dom G1 by A466, A672;
then A673: [(ma + 1),K2] in Indices G1 by A95, A362, A352, ZFMISC_1:87;
A674: [ma,K2] in Indices G1 by A41, A95, A362, A352, ZFMISC_1:87;
A675: len F in dom F by A661, A666, FINSEQ_3:25;
(h1 ^ F) /. (len (h1 ^ F)) = (h1 ^ F) /. ((len h1) + (len F)) by FINSEQ_1:22
.= F /. (len F) by A675, FINSEQ_4:69
.= ((g2 | m) | pf) /. u by A661, A662, A675
.= (g2 | m) /. u by A652, A661, A662, A675
.= G1 * (ma,K2) by A362, A363, A352, A416, MATRIX_1:def_7 ;
then A676: ( i1 = ma & i2 = K2 ) by A668, A670, A674, GOBOARD1:5;
h2 /. 1 = G1 * ((ma + 1),K2) by A418, A672;
then ( j1 = ma + 1 & j2 = K2 ) by A669, A671, A673, GOBOARD1:5;
hence (abs (i1 - j1)) + (abs (i2 - j2)) = (abs (ma - (ma + 1))) + 0 by A676, ABSVALUE:2
.= abs (- ((ma + 1) - ma))
.= abs 1 by COMPLEX1:52
.= 1 by ABSVALUE:def_1 ;
::_thesis: verum
end;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_F_holds_
ex_i,_j_being_Element_of_NAT_st_
(_[i,j]_in_Indices_G1_&_F_/._n_=_G1_*_(i,j)_)
let n be Element of NAT ; ::_thesis: ( n in dom F implies ex i, j being Element of NAT st
( [i,j] in Indices G1 & F /. n = G1 * (i,j) ) )
assume A677: n in dom F ; ::_thesis: ex i, j being Element of NAT st
( [i,j] in Indices G1 & F /. n = G1 * (i,j) )
then reconsider w = (pf + 1) - n as Element of NAT by A657, A661, A662;
A678: F /. n = ((g2 | m) | pf) /. w by A661, A662, A677;
then (pf + 1) - n in dom (g2 | m) by A652, A661, A662, A677;
then consider i, j being Element of NAT such that
A679: ( [i,j] in Indices G1 & (g2 | m) /. w = G1 * (i,j) ) by A15, GOBOARD1:def_9;
take i = i; ::_thesis: ex j being Element of NAT st
( [i,j] in Indices G1 & F /. n = G1 * (i,j) )
take j = j; ::_thesis: ( [i,j] in Indices G1 & F /. n = G1 * (i,j) )
thus ( [i,j] in Indices G1 & F /. n = G1 * (i,j) ) by A652, A661, A662, A677, A678, A679; ::_thesis: verum
end;
then for n being Element of NAT st n in dom (h1 ^ F) holds
ex i, j being Element of NAT st
( [i,j] in Indices G1 & (h1 ^ F) /. n = G1 * (i,j) ) by A403, GOBOARD1:23;
then A680: for n being Element of NAT st n in dom ((h1 ^ F) ^ h2) holds
ex i, j being Element of NAT st
( [i,j] in Indices G1 & ((h1 ^ F) ^ h2) /. n = G1 * (i,j) ) by A470, GOBOARD1:23;
set x = the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng tt);
0 + 0 <= (len h1) + (len h2) by NAT_1:2;
then A681: 0 + 1 <= (len F) + ((len h1) + (len h2)) by A661, A666, XREAL_1:7;
A682: rng ((h1 ^ F) ^ h2) = (rng (h1 ^ F)) \/ (rng h2) by FINSEQ_1:31
.= ((rng h1) \/ (rng F)) \/ (rng h2) by FINSEQ_1:31 ;
A683: for k being Element of NAT st k in Seg (width G1) & (rng F) /\ (rng (Col (G1,k))) = {} holds
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = {}
proof
A684: len (Col (G1,K2)) = len G1 by MATRIX_1:def_8;
A685: len (Col (G1,K1)) = len G1 by MATRIX_1:def_8;
let k be Element of NAT ; ::_thesis: ( k in Seg (width G1) & (rng F) /\ (rng (Col (G1,k))) = {} implies (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = {} )
assume that
A686: k in Seg (width G1) and
A687: (rng F) /\ (rng (Col (G1,k))) = {} ; ::_thesis: (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = {}
set gg = Col (G1,k);
assume A688: (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) <> {} ; ::_thesis: contradiction
set x = the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k)));
rng ((h1 ^ F) ^ h2) = (rng F) \/ ((rng h1) \/ (rng h2)) by A682, XBOOLE_1:4;
then A689: (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = {} \/ (((rng h1) \/ (rng h2)) /\ (rng (Col (G1,k)))) by A687, XBOOLE_1:23
.= ((rng h1) /\ (rng (Col (G1,k)))) \/ ((rng h2) /\ (rng (Col (G1,k)))) by XBOOLE_1:23 ;
now__::_thesis:_contradiction
percases ( the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in (rng h1) /\ (rng (Col (G1,k))) or the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in (rng h2) /\ (rng (Col (G1,k))) ) by A688, A689, XBOOLE_0:def_3;
supposeA690: the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in (rng h1) /\ (rng (Col (G1,k))) ; ::_thesis: contradiction
then A691: the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in rng (Col (G1,k)) by XBOOLE_0:def_4;
A692: 1 in Seg LL by A666, FINSEQ_1:1;
(pf + 1) - 1 = pf ;
then A693: ( F /. 1 = ((g2 | m) | pf) /. pf & ((g2 | m) | pf) /. pf = (g2 | m) /. pf ) by A652, A661, A692;
the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in rng h1 by A690, XBOOLE_0:def_4;
then consider i being Element of NAT such that
A694: i in dom h1 and
A695: the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = h1 /. i by PARTFUN2:2;
A696: the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = G1 * (i,K1) by A366, A694, A695;
reconsider y = the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) as Point of (TOP-REAL 2) by A695;
A697: Lmi /. K1 = Lmi . K1 by A364, PARTFUN1:def_6;
A698: dom CK1 = Seg (len G1) by A685, FINSEQ_1:def_3
.= dom G1 by FINSEQ_1:def_3 ;
then A699: i in dom CK1 by A398, A694;
CK1 /. i = CK1 . i by A398, A694, A698, PARTFUN1:def_6;
then y = CK1 /. i by A696, A698, A699, MATRIX_1:def_8;
then y in rng CK1 by A699, PARTFUN2:2;
then A700: K1 = k by A364, A397, A686, A691, GOBOARD1:4;
CK1 /. mi = CK1 . mi by A39, A698, PARTFUN1:def_6;
then F /. 1 = CK1 /. mi by A39, A364, A365, A397, A697, A693, GOBOARD1:2;
then A701: F /. 1 in rng (Col (G1,k)) by A39, A698, A700, PARTFUN2:2;
F /. 1 in rng F by A661, A662, A692, PARTFUN2:2;
hence contradiction by A687, A701, XBOOLE_0:def_4; ::_thesis: verum
end;
supposeA702: the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in (rng h2) /\ (rng (Col (G1,k))) ; ::_thesis: contradiction
then the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in rng h2 by XBOOLE_0:def_4;
then consider i being Element of NAT such that
A703: i in dom h2 and
A704: the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = h2 /. i by PARTFUN2:2;
A705: the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = G1 * ((ma + i),K2) by A418, A703, A704;
reconsider y = the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) as Point of (TOP-REAL 2) by A704;
A706: the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in rng (Col (G1,k)) by A702, XBOOLE_0:def_4;
reconsider u = (pf + 1) - LL as Element of NAT ;
A707: Lma /. K2 = Lma . K2 by A362, PARTFUN1:def_6;
A708: dom CK2 = Seg (len G1) by A684, FINSEQ_1:def_3
.= dom G1 by FINSEQ_1:def_3 ;
then A709: CK2 /. ma = CK2 . ma by A41, PARTFUN1:def_6;
A710: ma + i in dom CK2 by A466, A703, A708;
CK2 /. (ma + i) = CK2 . (ma + i) by A466, A703, A708, PARTFUN1:def_6;
then y = CK2 /. (ma + i) by A705, A708, A710, MATRIX_1:def_8;
then y in rng CK2 by A710, PARTFUN2:2;
then A711: K2 = k by A362, A352, A686, A706, GOBOARD1:4;
A712: LL in Seg LL by A666, FINSEQ_1:1;
then ( F /. LL = ((g2 | m) | pf) /. u & ((g2 | m) | pf) /. u = (g2 | m) /. u ) by A652, A661;
then F /. LL = CK2 /. ma by A41, A362, A363, A352, A707, A709, GOBOARD1:2;
then A713: F /. LL in rng (Col (G1,k)) by A41, A708, A711, PARTFUN2:2;
F /. LL in rng F by A661, A662, A712, PARTFUN2:2;
hence contradiction by A687, A713, XBOOLE_0:def_4; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
(rng F) /\ (rng C) = {}
proof
set x = the Element of (rng F) /\ (rng C);
assume A714: not (rng F) /\ (rng C) = {} ; ::_thesis: contradiction
then A715: the Element of (rng F) /\ (rng C) in rng C by XBOOLE_0:def_4;
the Element of (rng F) /\ (rng C) in rng F by A714, XBOOLE_0:def_4;
then consider i1 being Element of NAT such that
A716: i1 in dom F and
A717: F /. i1 = the Element of (rng F) /\ (rng C) by PARTFUN2:2;
reconsider w = (pf + 1) - i1 as Element of NAT by A657, A661, A662, A716;
1 <= i1 by A716, FINSEQ_3:25;
then A718: w <= (pf + 1) - 1 by XREAL_1:13;
A719: w in dom (g2 | m) by A652, A661, A662, A716;
then A720: w in dom g2 by A13, A24, A17, FINSEQ_4:71;
( F /. i1 = ((g2 | m) | pf) /. w & ((g2 | m) | pf) /. w = (g2 | m) /. w ) by A652, A661, A662, A716;
then g2 /. w in rng C by A13, A24, A17, A715, A717, A719, FINSEQ_4:71;
then m <= w by A13, A720;
hence contradiction by A17, A540, A718, XXREAL_0:2; ::_thesis: verum
end;
then (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,(width G1)))) = {} by A74, A683;
then A721: rng ((h1 ^ F) ^ h2) misses rng (Col (G1,(width G1))) by XBOOLE_0:def_7;
A722: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_F_&_n_+_1_in_dom_F_holds_
for_i1,_i2,_j1,_j2_being_Element_of_NAT_st_[i1,i2]_in_Indices_G1_&_[j1,j2]_in_Indices_G1_&_F_/._n_=_G1_*_(i1,i2)_&_F_/._(n_+_1)_=_G1_*_(j1,j2)_holds_
1_=_(abs_(i1_-_j1))_+_(abs_(i2_-_j2))
let n be Element of NAT ; ::_thesis: ( n in dom F & n + 1 in dom F implies for i1, i2, j1, j2 being Element of NAT st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & F /. n = G1 * (i1,i2) & F /. (n + 1) = G1 * (j1,j2) holds
1 = (abs (i1 - j1)) + (abs (i2 - j2)) )
assume that
A723: n in dom F and
A724: n + 1 in dom F ; ::_thesis: for i1, i2, j1, j2 being Element of NAT st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & F /. n = G1 * (i1,i2) & F /. (n + 1) = G1 * (j1,j2) holds
1 = (abs (i1 - j1)) + (abs (i2 - j2))
reconsider w3 = (pf + 1) - n, w2 = (pf + 1) - (n + 1) as Element of NAT by A657, A661, A662, A723, A724;
F /. n = ((g2 | m) | pf) /. w3 by A661, A662, A723;
then A725: ( (pf + 1) - n in dom (g2 | m) & F /. n = (g2 | m) /. w3 ) by A652, A661, A662, A723;
F /. (n + 1) = ((g2 | m) | pf) /. w2 by A661, A662, A724;
then A726: ( (pf + 1) - (n + 1) in dom (g2 | m) & F /. (n + 1) = (g2 | m) /. w2 ) by A652, A661, A662, A724;
let i1, i2, j1, j2 be Element of NAT ; ::_thesis: ( [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & F /. n = G1 * (i1,i2) & F /. (n + 1) = G1 * (j1,j2) implies 1 = (abs (i1 - j1)) + (abs (i2 - j2)) )
assume A727: ( [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & F /. n = G1 * (i1,i2) & F /. (n + 1) = G1 * (j1,j2) ) ; ::_thesis: 1 = (abs (i1 - j1)) + (abs (i2 - j2))
w2 + 1 = (pf + 1) - n ;
hence 1 = (abs (j1 - i1)) + (abs (j2 - i2)) by A15, A725, A726, A727, GOBOARD1:def_9
.= (abs (- (i1 - j1))) + (abs (- (i2 - j2)))
.= (abs (i1 - j1)) + (abs (- (i2 - j2))) by COMPLEX1:52
.= (abs (i1 - j1)) + (abs (i2 - j2)) by COMPLEX1:52 ;
::_thesis: verum
end;
A728: (pf + 1) - 1 = pf ;
A729: now__::_thesis:_((h1_^_F)_^_h2)_/._1_in_rng_(Line_(G1,1))
percases ( mi = 1 or mi <> 1 ) ;
supposeA730: mi = 1 ; ::_thesis: ((h1 ^ F) ^ h2) /. 1 in rng (Line (G1,1))
A731: pf in Seg pf by A361, FINSEQ_1:1;
A732: 1 in Seg LL by A666, FINSEQ_1:1;
h1 = {} by A366, A730;
then (h1 ^ F) ^ h2 = F ^ h2 by FINSEQ_1:34;
then ((h1 ^ F) ^ h2) /. 1 = F /. 1 by A661, A662, A732, FINSEQ_4:68
.= ((g2 | m) | pf) /. pf by A661, A728, A732
.= (g2 | m) /. pf by A356, A731, FINSEQ_4:71 ;
hence ((h1 ^ F) ^ h2) /. 1 in rng (Line (G1,1)) by A356, A730; ::_thesis: verum
end;
supposeA733: mi <> 1 ; ::_thesis: ((h1 ^ F) ^ h2) /. 1 in rng (Line (G1,1))
1 <= mi by A39, FINSEQ_3:25;
then 1 < mi by A733, XXREAL_0:1;
then 1 + 1 <= mi by NAT_1:13;
then A734: 1 <= l1 by XREAL_1:19;
then A735: 1 in Seg l1 by FINSEQ_1:1;
len (Line (G1,1)) = width G1 by MATRIX_1:def_7;
then A736: K1 in dom L1 by A364, A397, FINSEQ_1:def_3;
then A737: L1 /. K1 = L1 . K1 by PARTFUN1:def_6;
( len (h1 ^ F) = (len h1) + (len F) & 0 <= len F ) by FINSEQ_1:22, NAT_1:2;
then 0 + 1 <= len (h1 ^ F) by A366, A734, XREAL_1:7;
then 1 in dom (h1 ^ F) by FINSEQ_3:25;
then ((h1 ^ F) ^ h2) /. 1 = (h1 ^ F) /. 1 by FINSEQ_4:68
.= h1 /. 1 by A366, A465, A735, FINSEQ_4:68
.= G1 * (1,K1) by A366, A465, A735
.= L1 /. K1 by A364, A397, A737, MATRIX_1:def_7 ;
hence ((h1 ^ F) ^ h2) /. 1 in rng (Line (G1,1)) by A736, PARTFUN2:2; ::_thesis: verum
end;
end;
end;
rng tt c= rng f by A348, A351, XBOOLE_1:1;
then A738: rng tt c= rng g1 by A177, XBOOLE_1:1;
now__::_thesis:_for_i1,_i2,_j1,_j2_being_Element_of_NAT_st_[i1,i2]_in_Indices_G1_&_[j1,j2]_in_Indices_G1_&_h1_/._(len_h1)_=_G1_*_(i1,i2)_&_F_/._1_=_G1_*_(j1,j2)_&_len_h1_in_dom_h1_&_1_in_dom_F_holds_
(abs_(i1_-_j1))_+_(abs_(i2_-_j2))_=_1
A739: [mi,K1] in Indices G1 by A39, A95, A364, A397, ZFMISC_1:87;
reconsider w4 = (pf + 1) - 1 as Element of NAT ;
let i1, i2, j1, j2 be Element of NAT ; ::_thesis: ( [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & h1 /. (len h1) = G1 * (i1,i2) & F /. 1 = G1 * (j1,j2) & len h1 in dom h1 & 1 in dom F implies (abs (i1 - j1)) + (abs (i2 - j2)) = 1 )
assume that
A740: [i1,i2] in Indices G1 and
A741: [j1,j2] in Indices G1 and
A742: h1 /. (len h1) = G1 * (i1,i2) and
A743: F /. 1 = G1 * (j1,j2) and
A744: len h1 in dom h1 and
A745: 1 in dom F ; ::_thesis: (abs (i1 - j1)) + (abs (i2 - j2)) = 1
F /. 1 = ((g2 | m) | pf) /. w4 by A661, A662, A745
.= (g2 | m) /. w4 by A652, A661, A662, A745
.= G1 * (mi,K1) by A364, A365, A397, A523, MATRIX_1:def_7 ;
then A746: ( j1 = mi & j2 = K1 ) by A741, A743, A739, GOBOARD1:5;
l1 in dom G1 by A366, A398, A744;
then A747: [l1,K1] in Indices G1 by A95, A364, A397, ZFMISC_1:87;
h1 /. (len h1) = G1 * (l1,K1) by A366, A744;
then ( i1 = l1 & i2 = K1 ) by A740, A742, A747, GOBOARD1:5;
hence (abs (i1 - j1)) + (abs (i2 - j2)) = (abs ((mi - 1) - mi)) + 0 by A746, ABSVALUE:2
.= abs (- 1)
.= abs 1 by COMPLEX1:52
.= 1 by ABSVALUE:def_1 ;
::_thesis: verum
end;
then for n being Element of NAT st n in dom (h1 ^ F) & n + 1 in dom (h1 ^ F) holds
for i1, i2, j1, j2 being Element of NAT st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & (h1 ^ F) /. n = G1 * (i1,i2) & (h1 ^ F) /. (n + 1) = G1 * (j1,j2) holds
(abs (i1 - j1)) + (abs (i2 - j2)) = 1 by A405, A722, GOBOARD1:24;
then for n being Element of NAT st n in dom ((h1 ^ F) ^ h2) & n + 1 in dom ((h1 ^ F) ^ h2) holds
for m, k, i, j being Element of NAT st [m,k] in Indices G1 & [i,j] in Indices G1 & ((h1 ^ F) ^ h2) /. n = G1 * (m,k) & ((h1 ^ F) ^ h2) /. (n + 1) = G1 * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1 by A472, A667, GOBOARD1:24;
then (h1 ^ F) ^ h2 is_sequence_on G1 by A680, GOBOARD1:def_9;
then A748: (h1 ^ F) ^ h2 is_sequence_on DelCol (G1,(width G1)) by A74, A151, A721, GOBOARD1:25;
A749: len ((h1 ^ F) ^ h2) = (len (h1 ^ F)) + (len h2) by FINSEQ_1:22
.= ((len h1) + (len F)) + (len h2) by FINSEQ_1:22 ;
then 1 in dom ((h1 ^ F) ^ h2) by A681, FINSEQ_3:25;
then A750: ((h1 ^ F) ^ h2) /. 1 in rng (Line ((DelCol (G1,(width G1))),1)) by A74, A26, A151, A729, A721, GOBOARD1:21;
A751: now__::_thesis:_((h1_^_F)_^_h2)_/._(len_((h1_^_F)_^_h2))_in_rng_(Line_(G1,(len_G1)))
percases ( ma = len G1 or ma <> len G1 ) ;
supposeA752: ma = len G1 ; ::_thesis: ((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) in rng (Line (G1,(len G1)))
A753: pl in Seg pf by A484, A651, FINSEQ_1:1;
A754: (pf + 1) - ((pf + 1) - pl) = pl ;
A755: len F in dom F by A661, A666, FINSEQ_3:25;
h2 = {} by A418, A752;
then A756: (h1 ^ F) ^ h2 = h1 ^ F by FINSEQ_1:34;
then ((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) = ((h1 ^ F) ^ h2) /. ((len h1) + (len F)) by FINSEQ_1:22
.= F /. LL by A661, A756, A755, FINSEQ_4:69
.= ((g2 | m) | pf) /. pl by A661, A662, A754, A755
.= (g2 | m) /. pl by A356, A753, FINSEQ_4:71 ;
hence ((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) in rng (Line (G1,(len G1))) by A360, A752; ::_thesis: verum
end;
supposeA757: ma <> len G1 ; ::_thesis: ((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) in rng (Line (G1,(len G1)))
ma <= len G1 by A41, FINSEQ_3:25;
then ma < len G1 by A757, XXREAL_0:1;
then ma + 1 <= len G1 by NAT_1:13;
then A758: 1 <= l2 by XREAL_1:19;
then A759: l2 in Seg l2 by FINSEQ_1:1;
len (Line (G1,(len G1))) = width G1 by MATRIX_1:def_7;
then A760: K2 in dom Ll by A362, A352, FINSEQ_1:def_3;
then A761: Ll /. K2 = Ll . K2 by PARTFUN1:def_6;
A762: len h2 in dom h2 by A418, A758, FINSEQ_3:25;
((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) = ((h1 ^ F) ^ h2) /. ((len (h1 ^ F)) + (len h2)) by FINSEQ_1:22
.= h2 /. l2 by A418, A762, FINSEQ_4:69
.= G1 * ((ma + l2),K2) by A418, A482, A759
.= Ll /. K2 by A362, A352, A761, MATRIX_1:def_7 ;
hence ((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) in rng (Line (G1,(len G1))) by A760, PARTFUN2:2; ::_thesis: verum
end;
end;
end;
len ((h1 ^ F) ^ h2) in dom ((h1 ^ F) ^ h2) by A749, A681, FINSEQ_3:25;
then A763: ((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) in rng (Line ((DelCol (G1,(width G1))),(len (DelCol (G1,(width G1)))))) by A74, A27, A151, A152, A751, A721, GOBOARD1:21;
width (DelCol (G1,(width G1))) = k by A3, A74, A92, GOBOARD1:10, NAT_1:3;
then (rng ((h1 ^ F) ^ h2)) /\ (rng tt) <> {} by A2, A93, A350, A749, A681, A748, A750, A763;
then A764: the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng tt) in (rng ((h1 ^ F) ^ h2)) /\ (rng tt) ;
(rng tt) /\ (rng ((h1 ^ F) ^ h2)) = (((rng h1) \/ (rng F)) /\ (rng tt)) \/ {} by A489, A682, XBOOLE_1:23
.= {} \/ ((rng F) /\ (rng tt)) by A421, XBOOLE_1:23
.= (rng tt) /\ (rng F) ;
then (rng ((h1 ^ F) ^ h2)) /\ (rng tt) c= (rng g1) /\ (rng g2) by A738, A663, XBOOLE_1:27;
hence (rng g1) /\ (rng g2) <> {} by A764; ::_thesis: verum
end;
end;
end;
hence (rng g1) /\ (rng g2) <> {} ; ::_thesis: verum
end;
end;
end;
hence (rng g1) /\ (rng g2) <> {} ; ::_thesis: verum
end;
end;
end;
end;
end;
end;
hence (rng g1) /\ (rng g2) <> {} ; ::_thesis: verum
end;
end;
end;
hence (rng g1) /\ (rng g2) <> {} ; ::_thesis: verum
end;
A765: S1[ 0 ] ;
A766: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A765, A1);
A767: now__::_thesis:_for_k_being_Element_of_NAT_
for_G1_being_Go-board
for_g1,_g2_being_FinSequence_of_(TOP-REAL_2)_st_k_=_width_G1_&_k_>_0_&_1_<=_len_g1_&_1_<=_len_g2_&_g1_is_sequence_on_G1_&_g2_is_sequence_on_G1_&_g1_/._1_in_rng_(Line_(G1,1))_&_g1_/._(len_g1)_in_rng_(Line_(G1,(len_G1)))_&_g2_/._1_in_rng_(Col_(G1,1))_&_g2_/._(len_g2)_in_rng_(Col_(G1,(width_G1)))_holds_
rng_g1_meets_rng_g2
let k be Element of NAT ; ::_thesis: for G1 being Go-board
for g1, g2 being FinSequence of (TOP-REAL 2) st k = width G1 & k > 0 & 1 <= len g1 & 1 <= len g2 & g1 is_sequence_on G1 & g2 is_sequence_on G1 & g1 /. 1 in rng (Line (G1,1)) & g1 /. (len g1) in rng (Line (G1,(len G1))) & g2 /. 1 in rng (Col (G1,1)) & g2 /. (len g2) in rng (Col (G1,(width G1))) holds
rng g1 meets rng g2
let G1 be Go-board; ::_thesis: for g1, g2 being FinSequence of (TOP-REAL 2) st k = width G1 & k > 0 & 1 <= len g1 & 1 <= len g2 & g1 is_sequence_on G1 & g2 is_sequence_on G1 & g1 /. 1 in rng (Line (G1,1)) & g1 /. (len g1) in rng (Line (G1,(len G1))) & g2 /. 1 in rng (Col (G1,1)) & g2 /. (len g2) in rng (Col (G1,(width G1))) holds
rng g1 meets rng g2
let g1, g2 be FinSequence of (TOP-REAL 2); ::_thesis: ( k = width G1 & k > 0 & 1 <= len g1 & 1 <= len g2 & g1 is_sequence_on G1 & g2 is_sequence_on G1 & g1 /. 1 in rng (Line (G1,1)) & g1 /. (len g1) in rng (Line (G1,(len G1))) & g2 /. 1 in rng (Col (G1,1)) & g2 /. (len g2) in rng (Col (G1,(width G1))) implies rng g1 meets rng g2 )
assume ( k = width G1 & k > 0 & 1 <= len g1 & 1 <= len g2 & g1 is_sequence_on G1 & g2 is_sequence_on G1 & g1 /. 1 in rng (Line (G1,1)) & g1 /. (len g1) in rng (Line (G1,(len G1))) & g2 /. 1 in rng (Col (G1,1)) & g2 /. (len g2) in rng (Col (G1,(width G1))) ) ; ::_thesis: rng g1 meets rng g2
then (rng g1) /\ (rng g2) <> {} by A766;
hence rng g1 meets rng g2 by XBOOLE_0:def_7; ::_thesis: verum
end;
width G <> 0 by GOBOARD1:def_3;
then A768: width G > 0 by NAT_1:3;
assume ( 1 <= len f1 & 1 <= len f2 & f1 is_sequence_on G & f2 is_sequence_on G & f1 /. 1 in rng (Line (G,1)) & f1 /. (len f1) in rng (Line (G,(len G))) & f2 /. 1 in rng (Col (G,1)) & f2 /. (len f2) in rng (Col (G,(width G))) ) ; ::_thesis: rng f1 meets rng f2
hence rng f1 meets rng f2 by A767, A768; ::_thesis: verum
end;
theorem Th2: :: GOBOARD4:2
for G being Go-board
for f1, f2 being FinSequence of (TOP-REAL 2) st 2 <= len f1 & 2 <= len f2 & f1 is_sequence_on G & f2 is_sequence_on G & f1 /. 1 in rng (Line (G,1)) & f1 /. (len f1) in rng (Line (G,(len G))) & f2 /. 1 in rng (Col (G,1)) & f2 /. (len f2) in rng (Col (G,(width G))) holds
L~ f1 meets L~ f2
proof
let G be Go-board; ::_thesis: for f1, f2 being FinSequence of (TOP-REAL 2) st 2 <= len f1 & 2 <= len f2 & f1 is_sequence_on G & f2 is_sequence_on G & f1 /. 1 in rng (Line (G,1)) & f1 /. (len f1) in rng (Line (G,(len G))) & f2 /. 1 in rng (Col (G,1)) & f2 /. (len f2) in rng (Col (G,(width G))) holds
L~ f1 meets L~ f2
let f1, f2 be FinSequence of (TOP-REAL 2); ::_thesis: ( 2 <= len f1 & 2 <= len f2 & f1 is_sequence_on G & f2 is_sequence_on G & f1 /. 1 in rng (Line (G,1)) & f1 /. (len f1) in rng (Line (G,(len G))) & f2 /. 1 in rng (Col (G,1)) & f2 /. (len f2) in rng (Col (G,(width G))) implies L~ f1 meets L~ f2 )
assume that
A1: 2 <= len f1 and
A2: 2 <= len f2 and
A3: ( f1 is_sequence_on G & f2 is_sequence_on G & f1 /. 1 in rng (Line (G,1)) & f1 /. (len f1) in rng (Line (G,(len G))) & f2 /. 1 in rng (Col (G,1)) & f2 /. (len f2) in rng (Col (G,(width G))) ) ; ::_thesis: L~ f1 meets L~ f2
( 1 <= len f1 & 1 <= len f2 ) by A1, A2, XXREAL_0:2;
then rng f1 meets rng f2 by A3, Th1;
then consider x being set such that
A4: x in rng f1 and
A5: x in rng f2 by XBOOLE_0:3;
ex m being Element of NAT st
( m in dom f2 & f2 /. m = x ) by A5, PARTFUN2:2;
then A6: x in L~ f2 by A2, GOBOARD1:1;
ex n being Element of NAT st
( n in dom f1 & f1 /. n = x ) by A4, PARTFUN2:2;
then x in L~ f1 by A1, GOBOARD1:1;
hence L~ f1 meets L~ f2 by A6, XBOOLE_0:3; ::_thesis: verum
end;
theorem :: GOBOARD4:3
for G being Go-board
for f1, f2 being FinSequence of (TOP-REAL 2) st 2 <= len f1 & 2 <= len f2 & f1 is_sequence_on G & f2 is_sequence_on G & f1 /. 1 in rng (Line (G,1)) & f1 /. (len f1) in rng (Line (G,(len G))) & f2 /. 1 in rng (Col (G,1)) & f2 /. (len f2) in rng (Col (G,(width G))) holds
L~ f1 meets L~ f2 by Th2;
definition
let f be Relation;
let r, s be Real;
predf lies_between r,s means :Def1: :: GOBOARD4:def 1
rng f c= [.r,s.];
end;
:: deftheorem Def1 defines lies_between GOBOARD4:def_1_:_
for f being Relation
for r, s being Real holds
( f lies_between r,s iff rng f c= [.r,s.] );
definition
let f be FinSequence of REAL ;
let r, s be Real;
redefine pred f lies_between r,s means :Def2: :: GOBOARD4:def 2
for n being Element of NAT st n in dom f holds
( r <= f . n & f . n <= s );
compatibility
( f lies_between r,s iff for n being Element of NAT st n in dom f holds
( r <= f . n & f . n <= s ) )
proof
hereby ::_thesis: ( ( for n being Element of NAT st n in dom f holds
( r <= f . n & f . n <= s ) ) implies f lies_between r,s )
assume f lies_between r,s ; ::_thesis: for n being Element of NAT st n in dom f holds
( r <= f . n & f . n <= s )
then A1: rng f c= [.r,s.] by Def1;
let n be Element of NAT ; ::_thesis: ( n in dom f implies ( r <= f . n & f . n <= s ) )
assume n in dom f ; ::_thesis: ( r <= f . n & f . n <= s )
then f . n in rng f by FUNCT_1:3;
hence ( r <= f . n & f . n <= s ) by A1, XXREAL_1:1; ::_thesis: verum
end;
assume A2: for n being Element of NAT st n in dom f holds
( r <= f . n & f . n <= s ) ; ::_thesis: f lies_between r,s
let y be set ; :: according to TARSKI:def_3,GOBOARD4:def_1 ::_thesis: ( not y in rng f or y in [.r,s.] )
assume y in rng f ; ::_thesis: y in [.r,s.]
then consider x being set such that
A3: x in dom f and
A4: y = f . x by FUNCT_1:def_3;
reconsider n = x as Element of NAT by A3;
( r <= f . n & f . n <= s ) by A2, A3;
hence y in [.r,s.] by A4, XXREAL_1:1; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines lies_between GOBOARD4:def_2_:_
for f being FinSequence of REAL
for r, s being Real holds
( f lies_between r,s iff for n being Element of NAT st n in dom f holds
( r <= f . n & f . n <= s ) );
theorem Th4: :: GOBOARD4:4
for f1, f2 being FinSequence of (TOP-REAL 2) st 2 <= len f1 & 2 <= len f2 & f1 is special & f2 is special & ( for n being Element of NAT st n in dom f1 & n + 1 in dom f1 holds
f1 /. n <> f1 /. (n + 1) ) & ( for n being Element of NAT st n in dom f2 & n + 1 in dom f2 holds
f2 /. n <> f2 /. (n + 1) ) & X_axis f1 lies_between (X_axis f1) . 1,(X_axis f1) . (len f1) & X_axis f2 lies_between (X_axis f1) . 1,(X_axis f1) . (len f1) & Y_axis f1 lies_between (Y_axis f2) . 1,(Y_axis f2) . (len f2) & Y_axis f2 lies_between (Y_axis f2) . 1,(Y_axis f2) . (len f2) holds
L~ f1 meets L~ f2
proof
let f1, f2 be FinSequence of (TOP-REAL 2); ::_thesis: ( 2 <= len f1 & 2 <= len f2 & f1 is special & f2 is special & ( for n being Element of NAT st n in dom f1 & n + 1 in dom f1 holds
f1 /. n <> f1 /. (n + 1) ) & ( for n being Element of NAT st n in dom f2 & n + 1 in dom f2 holds
f2 /. n <> f2 /. (n + 1) ) & X_axis f1 lies_between (X_axis f1) . 1,(X_axis f1) . (len f1) & X_axis f2 lies_between (X_axis f1) . 1,(X_axis f1) . (len f1) & Y_axis f1 lies_between (Y_axis f2) . 1,(Y_axis f2) . (len f2) & Y_axis f2 lies_between (Y_axis f2) . 1,(Y_axis f2) . (len f2) implies L~ f1 meets L~ f2 )
assume that
A1: 2 <= len f1 and
A2: 2 <= len f2 and
A3: f1 is special and
A4: f2 is special and
A5: for n being Element of NAT st n in dom f1 & n + 1 in dom f1 holds
f1 /. n <> f1 /. (n + 1) and
A6: for n being Element of NAT st n in dom f2 & n + 1 in dom f2 holds
f2 /. n <> f2 /. (n + 1) and
A7: X_axis f1 lies_between (X_axis f1) . 1,(X_axis f1) . (len f1) and
A8: X_axis f2 lies_between (X_axis f1) . 1,(X_axis f1) . (len f1) and
A9: Y_axis f1 lies_between (Y_axis f2) . 1,(Y_axis f2) . (len f2) and
A10: Y_axis f2 lies_between (Y_axis f2) . 1,(Y_axis f2) . (len f2) ; ::_thesis: L~ f1 meets L~ f2
( len f1 <> 0 & len f2 <> 0 ) by A1, A2;
then reconsider f1 = f1, f2 = f2 as non empty FinSequence of (TOP-REAL 2) ;
reconsider f = f1 ^ f2 as non empty FinSequence of (TOP-REAL 2) ;
A11: Seg (len f2) = dom f2 by FINSEQ_1:def_3;
reconsider p1 = f1 /. 1, p2 = f1 /. (len f1), q1 = f2 /. 1, q2 = f2 /. (len f2) as Point of (TOP-REAL 2) ;
set x = X_axis f;
set y = Y_axis f;
set x1 = X_axis f1;
set y1 = Y_axis f1;
set x2 = X_axis f2;
set y2 = Y_axis f2;
A12: Seg (len f1) = dom f1 by FINSEQ_1:def_3;
A13: 1 <= len f1 by A1, XXREAL_0:2;
then A14: 1 in dom f1 by FINSEQ_3:25;
then A15: f /. 1 = f1 /. 1 by FINSEQ_4:68;
A16: Seg (len f) = dom f by FINSEQ_1:def_3;
set G = GoB f;
A17: ( dom (X_axis f) = Seg (len (X_axis f)) & len (X_axis f) = len f ) by FINSEQ_1:def_3, GOBOARD1:def_1;
A18: ( Seg (len (X_axis f2)) = dom (X_axis f2) & len (X_axis f2) = len f2 ) by FINSEQ_1:def_3, GOBOARD1:def_1;
A19: len f = (len f1) + (len f2) by FINSEQ_1:22;
A20: ( Seg (len (X_axis f1)) = dom (X_axis f1) & len (X_axis f1) = len f1 ) by FINSEQ_1:def_3, GOBOARD1:def_1;
then A21: (X_axis f1) . 1 = p1 `1 by A12, A14, GOBOARD1:def_1;
A22: now__::_thesis:_for_m_being_Element_of_NAT_st_m_in_dom_f_holds_
p1_`1_<=_(X_axis_f)_._m
let m be Element of NAT ; ::_thesis: ( m in dom f implies p1 `1 <= (X_axis f) . m )
set s = (X_axis f) . m;
assume A23: m in dom f ; ::_thesis: p1 `1 <= (X_axis f) . m
then A24: m <= len f by FINSEQ_3:25;
A25: 1 <= m by A23, FINSEQ_3:25;
now__::_thesis:_p1_`1_<=_(X_axis_f)_._m
percases ( m <= len f1 or len f1 < m ) ;
supposeA26: m <= len f1 ; ::_thesis: p1 `1 <= (X_axis f) . m
reconsider u = f1 /. m as Point of (TOP-REAL 2) ;
A27: m in dom f1 by A25, A26, FINSEQ_3:25;
then f /. m = u by FINSEQ_4:68;
then A28: (X_axis f) . m = u `1 by A16, A17, A23, GOBOARD1:def_1;
(X_axis f1) . m = u `1 by A12, A20, A27, GOBOARD1:def_1;
hence p1 `1 <= (X_axis f) . m by A7, A12, A20, A21, A27, A28, Def2; ::_thesis: verum
end;
supposeA29: len f1 < m ; ::_thesis: p1 `1 <= (X_axis f) . m
then reconsider w5 = m - (len f1) as Element of NAT by INT_1:5;
w5 > 0 by A29, XREAL_1:50;
then A30: 1 <= w5 by NAT_1:14;
A31: m = w5 + (len f1) ;
then reconsider m1 = m - (len f1) as Element of NAT ;
reconsider u = f2 /. m1 as Point of (TOP-REAL 2) ;
A32: w5 <= len f2 by A19, A24, A31, XREAL_1:6;
then f /. m = f2 /. w5 by A31, A30, SEQ_4:136;
then A33: (X_axis f) . m = u `1 by A16, A17, A23, GOBOARD1:def_1;
A34: m1 in dom f2 by A30, A32, FINSEQ_3:25;
then (X_axis f2) . m1 = u `1 by A11, A18, GOBOARD1:def_1;
hence p1 `1 <= (X_axis f) . m by A8, A11, A18, A21, A34, A33, Def2; ::_thesis: verum
end;
end;
end;
hence p1 `1 <= (X_axis f) . m ; ::_thesis: verum
end;
len f = (len f1) + (len f2) by FINSEQ_1:22;
then 2 + 2 <= len f by A1, A2, XREAL_1:7;
then 1 <= len f by XXREAL_0:2;
then A35: 1 in dom f by FINSEQ_3:25;
then (X_axis f) . 1 = p1 `1 by A16, A17, A15, GOBOARD1:def_1;
then A36: f /. 1 in rng (Line ((GoB f),1)) by A35, A22, GOBOARD2:15;
A37: len f1 in dom f1 by A13, FINSEQ_3:25;
then A38: f /. (len f1) = f1 /. (len f1) by FINSEQ_4:68;
A39: (X_axis f1) . (len f1) = p2 `1 by A12, A20, A37, GOBOARD1:def_1;
A40: now__::_thesis:_for_m_being_Element_of_NAT_st_m_in_dom_f_holds_
(X_axis_f)_._m_<=_p2_`1
let m be Element of NAT ; ::_thesis: ( m in dom f implies (X_axis f) . m <= p2 `1 )
set s = (X_axis f) . m;
assume A41: m in dom f ; ::_thesis: (X_axis f) . m <= p2 `1
then A42: m <= len f by FINSEQ_3:25;
A43: 1 <= m by A41, FINSEQ_3:25;
now__::_thesis:_(X_axis_f)_._m_<=_p2_`1
percases ( m <= len f1 or len f1 < m ) ;
supposeA44: m <= len f1 ; ::_thesis: (X_axis f) . m <= p2 `1
reconsider u = f1 /. m as Point of (TOP-REAL 2) ;
A45: m in dom f1 by A43, A44, FINSEQ_3:25;
then f /. m = u by FINSEQ_4:68;
then A46: (X_axis f) . m = u `1 by A16, A17, A41, GOBOARD1:def_1;
(X_axis f1) . m = u `1 by A12, A20, A45, GOBOARD1:def_1;
hence (X_axis f) . m <= p2 `1 by A7, A12, A20, A39, A45, A46, Def2; ::_thesis: verum
end;
supposeA47: len f1 < m ; ::_thesis: (X_axis f) . m <= p2 `1
then reconsider w5 = m - (len f1) as Element of NAT by INT_1:5;
w5 > 0 by A47, XREAL_1:50;
then A48: 1 <= w5 by NAT_1:14;
A49: m = w5 + (len f1) ;
then reconsider m1 = m - (len f1) as Element of NAT ;
reconsider u = f2 /. m1 as Point of (TOP-REAL 2) ;
A50: w5 <= len f2 by A19, A42, A49, XREAL_1:6;
then f /. m = f2 /. w5 by A49, A48, SEQ_4:136;
then A51: (X_axis f) . m = u `1 by A16, A17, A41, GOBOARD1:def_1;
A52: m1 in dom f2 by A48, A50, FINSEQ_3:25;
then (X_axis f2) . m1 = u `1 by A11, A18, GOBOARD1:def_1;
hence (X_axis f) . m <= p2 `1 by A8, A11, A18, A39, A52, A51, Def2; ::_thesis: verum
end;
end;
end;
hence (X_axis f) . m <= p2 `1 ; ::_thesis: verum
end;
A53: dom f1 c= dom f by FINSEQ_1:26;
then (X_axis f) . (len f1) = p2 `1 by A16, A17, A37, A38, GOBOARD1:def_1;
then A54: f /. (len f1) in rng (Line ((GoB f),(len (GoB f)))) by A53, A37, A40, GOBOARD2:16;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_f1_holds_
ex_i,_j_being_Element_of_NAT_st_
(_[i,j]_in_Indices_(GoB_f)_&_f1_/._n_=_(GoB_f)_*_(i,j)_)
let n be Element of NAT ; ::_thesis: ( n in dom f1 implies ex i, j being Element of NAT st
( [i,j] in Indices (GoB f) & f1 /. n = (GoB f) * (i,j) ) )
assume A55: n in dom f1 ; ::_thesis: ex i, j being Element of NAT st
( [i,j] in Indices (GoB f) & f1 /. n = (GoB f) * (i,j) )
dom f1 c= dom f by FINSEQ_1:26;
then consider i, j being Element of NAT such that
A56: ( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) ) by A55, GOBOARD2:14;
take i = i; ::_thesis: ex j being Element of NAT st
( [i,j] in Indices (GoB f) & f1 /. n = (GoB f) * (i,j) )
take j = j; ::_thesis: ( [i,j] in Indices (GoB f) & f1 /. n = (GoB f) * (i,j) )
thus ( [i,j] in Indices (GoB f) & f1 /. n = (GoB f) * (i,j) ) by A55, A56, FINSEQ_4:68; ::_thesis: verum
end;
then consider g1 being FinSequence of (TOP-REAL 2) such that
A57: ( g1 is_sequence_on GoB f & L~ g1 = L~ f1 & g1 /. 1 = f1 /. 1 & g1 /. (len g1) = f1 /. (len f1) ) and
A58: len f1 <= len g1 by A3, A5, GOBOARD2:12;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_f2_holds_
ex_i,_j_being_Element_of_NAT_st_
(_[i,j]_in_Indices_(GoB_f)_&_f2_/._n_=_(GoB_f)_*_(i,j)_)
let n be Element of NAT ; ::_thesis: ( n in dom f2 implies ex i, j being Element of NAT st
( [i,j] in Indices (GoB f) & f2 /. n = (GoB f) * (i,j) ) )
assume A59: n in dom f2 ; ::_thesis: ex i, j being Element of NAT st
( [i,j] in Indices (GoB f) & f2 /. n = (GoB f) * (i,j) )
then (len f1) + n in dom f by FINSEQ_1:28;
then consider i, j being Element of NAT such that
A60: ( [i,j] in Indices (GoB f) & f /. ((len f1) + n) = (GoB f) * (i,j) ) by GOBOARD2:14;
take i = i; ::_thesis: ex j being Element of NAT st
( [i,j] in Indices (GoB f) & f2 /. n = (GoB f) * (i,j) )
take j = j; ::_thesis: ( [i,j] in Indices (GoB f) & f2 /. n = (GoB f) * (i,j) )
thus ( [i,j] in Indices (GoB f) & f2 /. n = (GoB f) * (i,j) ) by A59, A60, FINSEQ_4:69; ::_thesis: verum
end;
then consider g2 being FinSequence of (TOP-REAL 2) such that
A61: ( g2 is_sequence_on GoB f & L~ g2 = L~ f2 & g2 /. 1 = f2 /. 1 & g2 /. (len g2) = f2 /. (len f2) ) and
A62: len f2 <= len g2 by A4, A6, GOBOARD2:12;
A63: 2 <= len g2 by A2, A62, XXREAL_0:2;
A64: 1 <= len f2 by A2, XXREAL_0:2;
then A65: 1 in dom f2 by FINSEQ_3:25;
then A66: f /. ((len f1) + 1) = f2 /. 1 by FINSEQ_4:69;
A67: ( Seg (len (Y_axis f)) = dom (Y_axis f) & len (Y_axis f) = len f ) by FINSEQ_1:def_3, GOBOARD1:def_2;
A68: ( Seg (len (Y_axis f1)) = dom (Y_axis f1) & len (Y_axis f1) = len f1 ) by FINSEQ_1:def_3, GOBOARD1:def_2;
A69: ( Seg (len (Y_axis f2)) = dom (Y_axis f2) & len (Y_axis f2) = len f2 ) by FINSEQ_1:def_3, GOBOARD1:def_2;
then A70: (Y_axis f2) . 1 = q1 `2 by A11, A65, GOBOARD1:def_2;
A71: now__::_thesis:_for_m_being_Element_of_NAT_st_m_in_dom_f_holds_
q1_`2_<=_(Y_axis_f)_._m
let m be Element of NAT ; ::_thesis: ( m in dom f implies q1 `2 <= (Y_axis f) . m )
set s = (Y_axis f) . m;
assume A72: m in dom f ; ::_thesis: q1 `2 <= (Y_axis f) . m
then A73: m <= len f by FINSEQ_3:25;
A74: 1 <= m by A72, FINSEQ_3:25;
now__::_thesis:_q1_`2_<=_(Y_axis_f)_._m
percases ( m <= len f1 or len f1 < m ) ;
supposeA75: m <= len f1 ; ::_thesis: q1 `2 <= (Y_axis f) . m
reconsider u = f1 /. m as Point of (TOP-REAL 2) ;
A76: m in dom f1 by A74, A75, FINSEQ_3:25;
then f /. m = u by FINSEQ_4:68;
then A77: (Y_axis f) . m = u `2 by A16, A67, A72, GOBOARD1:def_2;
(Y_axis f1) . m = u `2 by A12, A68, A76, GOBOARD1:def_2;
hence q1 `2 <= (Y_axis f) . m by A9, A12, A68, A70, A76, A77, Def2; ::_thesis: verum
end;
supposeA78: len f1 < m ; ::_thesis: q1 `2 <= (Y_axis f) . m
then reconsider w5 = m - (len f1) as Element of NAT by INT_1:5;
w5 > 0 by A78, XREAL_1:50;
then A79: 1 <= w5 by NAT_1:14;
A80: m = w5 + (len f1) ;
then reconsider m1 = m - (len f1) as Element of NAT ;
reconsider u = f2 /. m1 as Point of (TOP-REAL 2) ;
A81: w5 <= len f2 by A19, A73, A80, XREAL_1:6;
then f /. m = f2 /. w5 by A80, A79, SEQ_4:136;
then A82: (Y_axis f) . m = u `2 by A16, A67, A72, GOBOARD1:def_2;
A83: m1 in dom f2 by A79, A81, FINSEQ_3:25;
then (Y_axis f2) . m1 = u `2 by A11, A69, GOBOARD1:def_2;
hence q1 `2 <= (Y_axis f) . m by A10, A11, A69, A70, A83, A82, Def2; ::_thesis: verum
end;
end;
end;
hence q1 `2 <= (Y_axis f) . m ; ::_thesis: verum
end;
A84: (len f1) + 1 in dom f by A65, FINSEQ_1:28;
then (Y_axis f) . ((len f1) + 1) = q1 `2 by A16, A67, A66, GOBOARD1:def_2;
then A85: f /. ((len f1) + 1) in rng (Col ((GoB f),1)) by A84, A71, GOBOARD2:17;
A86: len f2 in dom f2 by A64, FINSEQ_3:25;
then A87: f /. ((len f1) + (len f2)) = f2 /. (len f2) by FINSEQ_4:69;
A88: (Y_axis f2) . (len f2) = q2 `2 by A11, A69, A86, GOBOARD1:def_2;
A89: now__::_thesis:_for_m_being_Element_of_NAT_st_m_in_dom_f_holds_
(Y_axis_f)_._m_<=_q2_`2
let m be Element of NAT ; ::_thesis: ( m in dom f implies (Y_axis f) . m <= q2 `2 )
set s = (Y_axis f) . m;
assume A90: m in dom f ; ::_thesis: (Y_axis f) . m <= q2 `2
then A91: m <= len f by FINSEQ_3:25;
A92: 1 <= m by A90, FINSEQ_3:25;
now__::_thesis:_(Y_axis_f)_._m_<=_q2_`2
percases ( m <= len f1 or len f1 < m ) ;
supposeA93: m <= len f1 ; ::_thesis: (Y_axis f) . m <= q2 `2
reconsider u = f1 /. m as Point of (TOP-REAL 2) ;
A94: m in dom f1 by A92, A93, FINSEQ_3:25;
then f /. m = u by FINSEQ_4:68;
then A95: (Y_axis f) . m = u `2 by A16, A67, A90, GOBOARD1:def_2;
(Y_axis f1) . m = u `2 by A12, A68, A94, GOBOARD1:def_2;
hence (Y_axis f) . m <= q2 `2 by A9, A12, A68, A88, A94, A95, Def2; ::_thesis: verum
end;
supposeA96: len f1 < m ; ::_thesis: (Y_axis f) . m <= q2 `2
then reconsider w5 = m - (len f1) as Element of NAT by INT_1:5;
w5 > 0 by A96, XREAL_1:50;
then A97: 1 <= w5 by NAT_1:14;
A98: m = w5 + (len f1) ;
then reconsider m1 = m - (len f1) as Element of NAT ;
reconsider u = f2 /. m1 as Point of (TOP-REAL 2) ;
A99: w5 <= len f2 by A19, A91, A98, XREAL_1:6;
then f /. m = f2 /. w5 by A98, A97, SEQ_4:136;
then A100: (Y_axis f) . m = u `2 by A16, A67, A90, GOBOARD1:def_2;
A101: m1 in dom f2 by A97, A99, FINSEQ_3:25;
then (Y_axis f2) . m1 = u `2 by A11, A69, GOBOARD1:def_2;
hence (Y_axis f) . m <= q2 `2 by A10, A11, A69, A88, A101, A100, Def2; ::_thesis: verum
end;
end;
end;
hence (Y_axis f) . m <= q2 `2 ; ::_thesis: verum
end;
A102: (len f1) + (len f2) in dom f by A86, FINSEQ_1:28;
then (Y_axis f) . ((len f1) + (len f2)) = q2 `2 by A16, A67, A87, GOBOARD1:def_2;
then A103: f /. ((len f1) + (len f2)) in rng (Col ((GoB f),(width (GoB f)))) by A102, A89, GOBOARD2:18;
2 <= len g1 by A1, A58, XXREAL_0:2;
hence L~ f1 meets L~ f2 by A57, A61, A15, A38, A66, A87, A36, A54, A85, A103, A63, Th2; ::_thesis: verum
end;
theorem Th5: :: GOBOARD4:5
for f1, f2 being FinSequence of (TOP-REAL 2) st f1 is one-to-one & f1 is special & 2 <= len f1 & f2 is one-to-one & f2 is special & 2 <= len f2 & X_axis f1 lies_between (X_axis f1) . 1,(X_axis f1) . (len f1) & X_axis f2 lies_between (X_axis f1) . 1,(X_axis f1) . (len f1) & Y_axis f1 lies_between (Y_axis f2) . 1,(Y_axis f2) . (len f2) & Y_axis f2 lies_between (Y_axis f2) . 1,(Y_axis f2) . (len f2) holds
L~ f1 meets L~ f2
proof
let f1, f2 be FinSequence of (TOP-REAL 2); ::_thesis: ( f1 is one-to-one & f1 is special & 2 <= len f1 & f2 is one-to-one & f2 is special & 2 <= len f2 & X_axis f1 lies_between (X_axis f1) . 1,(X_axis f1) . (len f1) & X_axis f2 lies_between (X_axis f1) . 1,(X_axis f1) . (len f1) & Y_axis f1 lies_between (Y_axis f2) . 1,(Y_axis f2) . (len f2) & Y_axis f2 lies_between (Y_axis f2) . 1,(Y_axis f2) . (len f2) implies L~ f1 meets L~ f2 )
assume that
A1: ( f1 is one-to-one & f1 is special ) and
A2: 2 <= len f1 and
A3: ( f2 is one-to-one & f2 is special ) and
A4: ( 2 <= len f2 & X_axis f1 lies_between (X_axis f1) . 1,(X_axis f1) . (len f1) & X_axis f2 lies_between (X_axis f1) . 1,(X_axis f1) . (len f1) & Y_axis f1 lies_between (Y_axis f2) . 1,(Y_axis f2) . (len f2) & Y_axis f2 lies_between (Y_axis f2) . 1,(Y_axis f2) . (len f2) ) ; ::_thesis: L~ f1 meets L~ f2
A5: for n being Element of NAT st n in dom f2 & n + 1 in dom f2 holds
f2 /. n <> f2 /. (n + 1)
proof
let n be Element of NAT ; ::_thesis: ( n in dom f2 & n + 1 in dom f2 implies f2 /. n <> f2 /. (n + 1) )
assume ( n in dom f2 & n + 1 in dom f2 & f2 /. n = f2 /. (n + 1) ) ; ::_thesis: contradiction
then n = n + 1 by A3, PARTFUN2:10;
hence contradiction ; ::_thesis: verum
end;
for n being Element of NAT st n in dom f1 & n + 1 in dom f1 holds
f1 /. n <> f1 /. (n + 1)
proof
let n be Element of NAT ; ::_thesis: ( n in dom f1 & n + 1 in dom f1 implies f1 /. n <> f1 /. (n + 1) )
assume ( n in dom f1 & n + 1 in dom f1 & f1 /. n = f1 /. (n + 1) ) ; ::_thesis: contradiction
then n = n + 1 by A1, PARTFUN2:10;
hence contradiction ; ::_thesis: verum
end;
hence L~ f1 meets L~ f2 by A1, A2, A3, A4, A5, Th4; ::_thesis: verum
end;
theorem :: GOBOARD4:6
for P1, P2 being Subset of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P1 is_S-P_arc_joining p1,q1 & P2 is_S-P_arc_joining p2,q2 & ( for p being Point of (TOP-REAL 2) st p in P1 \/ P2 holds
( p1 `1 <= p `1 & p `1 <= q1 `1 ) ) & ( for p being Point of (TOP-REAL 2) st p in P1 \/ P2 holds
( p2 `2 <= p `2 & p `2 <= q2 `2 ) ) holds
P1 meets P2
proof
let P1, P2 be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P1 is_S-P_arc_joining p1,q1 & P2 is_S-P_arc_joining p2,q2 & ( for p being Point of (TOP-REAL 2) st p in P1 \/ P2 holds
( p1 `1 <= p `1 & p `1 <= q1 `1 ) ) & ( for p being Point of (TOP-REAL 2) st p in P1 \/ P2 holds
( p2 `2 <= p `2 & p `2 <= q2 `2 ) ) holds
P1 meets P2
let p1, p2, q1, q2 be Point of (TOP-REAL 2); ::_thesis: ( P1 is_S-P_arc_joining p1,q1 & P2 is_S-P_arc_joining p2,q2 & ( for p being Point of (TOP-REAL 2) st p in P1 \/ P2 holds
( p1 `1 <= p `1 & p `1 <= q1 `1 ) ) & ( for p being Point of (TOP-REAL 2) st p in P1 \/ P2 holds
( p2 `2 <= p `2 & p `2 <= q2 `2 ) ) implies P1 meets P2 )
assume that
A1: P1 is_S-P_arc_joining p1,q1 and
A2: P2 is_S-P_arc_joining p2,q2 and
A3: for p being Point of (TOP-REAL 2) st p in P1 \/ P2 holds
( p1 `1 <= p `1 & p `1 <= q1 `1 ) and
A4: for p being Point of (TOP-REAL 2) st p in P1 \/ P2 holds
( p2 `2 <= p `2 & p `2 <= q2 `2 ) ; ::_thesis: P1 meets P2
consider f1 being FinSequence of (TOP-REAL 2) such that
A5: f1 is being_S-Seq and
A6: P1 = L~ f1 and
A7: p1 = f1 /. 1 and
A8: q1 = f1 /. (len f1) by A1, TOPREAL4:def_1;
len f1 <> 0 by A5, TOPREAL1:def_8;
then reconsider f1 = f1 as non empty FinSequence of (TOP-REAL 2) ;
A9: Seg (len f1) = dom f1 by FINSEQ_1:def_3;
consider f2 being FinSequence of (TOP-REAL 2) such that
A10: f2 is being_S-Seq and
A11: P2 = L~ f2 and
A12: p2 = f2 /. 1 and
A13: q2 = f2 /. (len f2) by A2, TOPREAL4:def_1;
len f2 <> 0 by A10, TOPREAL1:def_8;
then reconsider f2 = f2 as non empty FinSequence of (TOP-REAL 2) ;
A14: Seg (len f2) = dom f2 by FINSEQ_1:def_3;
set x1 = X_axis f1;
set y1 = Y_axis f1;
set x2 = X_axis f2;
set y2 = Y_axis f2;
A15: ( Seg (len (X_axis f1)) = dom (X_axis f1) & len (X_axis f1) = len f1 ) by FINSEQ_1:def_3, GOBOARD1:def_1;
A16: ( dom (Y_axis f2) = Seg (len (Y_axis f2)) & len (Y_axis f2) = len f2 ) by FINSEQ_1:def_3, GOBOARD1:def_2;
A17: 2 <= len f2 by A10, TOPREAL1:def_8;
then A18: 1 <= len f2 by XXREAL_0:2;
then 1 in dom f2 by FINSEQ_3:25;
then A19: (Y_axis f2) . 1 = p2 `2 by A12, A14, A16, GOBOARD1:def_2;
len f2 in dom f2 by A18, FINSEQ_3:25;
then A20: (Y_axis f2) . (len f2) = q2 `2 by A13, A14, A16, GOBOARD1:def_2;
A21: Y_axis f2 lies_between (Y_axis f2) . 1,(Y_axis f2) . (len f2)
proof
let n be Element of NAT ; :: according to GOBOARD4:def_2 ::_thesis: ( n in dom (Y_axis f2) implies ( (Y_axis f2) . 1 <= (Y_axis f2) . n & (Y_axis f2) . n <= (Y_axis f2) . (len f2) ) )
set q = f2 /. n;
assume A22: n in dom (Y_axis f2) ; ::_thesis: ( (Y_axis f2) . 1 <= (Y_axis f2) . n & (Y_axis f2) . n <= (Y_axis f2) . (len f2) )
then f2 /. n in L~ f2 by A17, A14, A16, GOBOARD1:1;
then A23: f2 /. n in P1 \/ P2 by A11, XBOOLE_0:def_3;
(Y_axis f2) . n = (f2 /. n) `2 by A22, GOBOARD1:def_2;
hence ( (Y_axis f2) . 1 <= (Y_axis f2) . n & (Y_axis f2) . n <= (Y_axis f2) . (len f2) ) by A4, A19, A20, A23; ::_thesis: verum
end;
A24: 2 <= len f1 by A5, TOPREAL1:def_8;
then A25: 1 <= len f1 by XXREAL_0:2;
then 1 in dom f1 by FINSEQ_3:25;
then A26: (X_axis f1) . 1 = p1 `1 by A7, A9, A15, GOBOARD1:def_1;
len f1 in dom f1 by A25, FINSEQ_3:25;
then A27: (X_axis f1) . (len f1) = q1 `1 by A8, A9, A15, GOBOARD1:def_1;
A28: X_axis f1 lies_between (X_axis f1) . 1,(X_axis f1) . (len f1)
proof
let n be Element of NAT ; :: according to GOBOARD4:def_2 ::_thesis: ( n in dom (X_axis f1) implies ( (X_axis f1) . 1 <= (X_axis f1) . n & (X_axis f1) . n <= (X_axis f1) . (len f1) ) )
set q = f1 /. n;
assume A29: n in dom (X_axis f1) ; ::_thesis: ( (X_axis f1) . 1 <= (X_axis f1) . n & (X_axis f1) . n <= (X_axis f1) . (len f1) )
then f1 /. n in L~ f1 by A24, A9, A15, GOBOARD1:1;
then A30: f1 /. n in P1 \/ P2 by A6, XBOOLE_0:def_3;
(X_axis f1) . n = (f1 /. n) `1 by A29, GOBOARD1:def_1;
hence ( (X_axis f1) . 1 <= (X_axis f1) . n & (X_axis f1) . n <= (X_axis f1) . (len f1) ) by A3, A26, A27, A30; ::_thesis: verum
end;
A31: ( dom (X_axis f2) = Seg (len (X_axis f2)) & len (X_axis f2) = len f2 ) by FINSEQ_1:def_3, GOBOARD1:def_1;
A32: X_axis f2 lies_between (X_axis f1) . 1,(X_axis f1) . (len f1)
proof
let n be Element of NAT ; :: according to GOBOARD4:def_2 ::_thesis: ( n in dom (X_axis f2) implies ( (X_axis f1) . 1 <= (X_axis f2) . n & (X_axis f2) . n <= (X_axis f1) . (len f1) ) )
set q = f2 /. n;
assume A33: n in dom (X_axis f2) ; ::_thesis: ( (X_axis f1) . 1 <= (X_axis f2) . n & (X_axis f2) . n <= (X_axis f1) . (len f1) )
then f2 /. n in L~ f2 by A17, A14, A31, GOBOARD1:1;
then A34: f2 /. n in P1 \/ P2 by A11, XBOOLE_0:def_3;
(X_axis f2) . n = (f2 /. n) `1 by A33, GOBOARD1:def_1;
hence ( (X_axis f1) . 1 <= (X_axis f2) . n & (X_axis f2) . n <= (X_axis f1) . (len f1) ) by A3, A26, A27, A34; ::_thesis: verum
end;
A35: ( dom (Y_axis f1) = Seg (len (Y_axis f1)) & len (Y_axis f1) = len f1 ) by FINSEQ_1:def_3, GOBOARD1:def_2;
A36: Y_axis f1 lies_between (Y_axis f2) . 1,(Y_axis f2) . (len f2)
proof
let n be Element of NAT ; :: according to GOBOARD4:def_2 ::_thesis: ( n in dom (Y_axis f1) implies ( (Y_axis f2) . 1 <= (Y_axis f1) . n & (Y_axis f1) . n <= (Y_axis f2) . (len f2) ) )
set q = f1 /. n;
assume A37: n in dom (Y_axis f1) ; ::_thesis: ( (Y_axis f2) . 1 <= (Y_axis f1) . n & (Y_axis f1) . n <= (Y_axis f2) . (len f2) )
then f1 /. n in L~ f1 by A24, A9, A35, GOBOARD1:1;
then A38: f1 /. n in P1 \/ P2 by A6, XBOOLE_0:def_3;
(Y_axis f1) . n = (f1 /. n) `2 by A37, GOBOARD1:def_2;
hence ( (Y_axis f2) . 1 <= (Y_axis f1) . n & (Y_axis f1) . n <= (Y_axis f2) . (len f2) ) by A4, A19, A20, A38; ::_thesis: verum
end;
A39: ( f2 is one-to-one & f2 is special ) by A10, TOPREAL1:def_8;
( f1 is one-to-one & f1 is special ) by A5, TOPREAL1:def_8;
hence P1 meets P2 by A6, A11, A39, A24, A17, A28, A32, A36, A21, Th5; ::_thesis: verum
end;