:: 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;