:: GOBOARD2 semantic presentation begin theorem :: GOBOARD2:1 for f being FinSequence of (TOP-REAL 2) st ( for n, m being Element of NAT st m > n + 1 & n in dom f & n + 1 in dom f & m in dom f & m + 1 in dom f holds LSeg (f,n) misses LSeg (f,m) ) holds f is s.n.c. proof let f be FinSequence of (TOP-REAL 2); ::_thesis: ( ( for n, m being Element of NAT st m > n + 1 & n in dom f & n + 1 in dom f & m in dom f & m + 1 in dom f holds LSeg (f,n) misses LSeg (f,m) ) implies f is s.n.c. ) assume A1: for n, m being Element of NAT st m > n + 1 & n in dom f & n + 1 in dom f & m in dom f & m + 1 in dom f holds LSeg (f,n) misses LSeg (f,m) ; ::_thesis: f is s.n.c. let n, m be Nat; :: according to TOPREAL1:def_7 ::_thesis: ( m <= n + 1 or LSeg (f,n) misses LSeg (f,m) ) assume A2: m > n + 1 ; ::_thesis: LSeg (f,n) misses LSeg (f,m) A3: ( n <= n + 1 & m <= m + 1 ) by NAT_1:11; percases ( ( n in dom f & n + 1 in dom f & m in dom f & m + 1 in dom f ) or not n in dom f or not n + 1 in dom f or not m in dom f or not m + 1 in dom f ) ; suppose ( n in dom f & n + 1 in dom f & m in dom f & m + 1 in dom f ) ; ::_thesis: LSeg (f,n) misses LSeg (f,m) hence LSeg (f,n) misses LSeg (f,m) by A1, A2; ::_thesis: verum end; suppose ( not n in dom f or not n + 1 in dom f or not m in dom f or not m + 1 in dom f ) ; ::_thesis: LSeg (f,n) misses LSeg (f,m) then ( not 1 <= n or not n <= len f or not 1 <= n + 1 or not n + 1 <= len f or not 1 <= m or not m <= len f or not 1 <= m + 1 or not m + 1 <= len f ) by FINSEQ_3:25; then ( not 1 <= n or not n + 1 <= len f or not 1 <= m or not m + 1 <= len f ) by A3, XXREAL_0:2; then ( LSeg (f,m) = {} or LSeg (f,n) = {} ) by TOPREAL1:def_3; hence LSeg (f,n) misses LSeg (f,m) by XBOOLE_1:65; ::_thesis: verum end; end; end; theorem :: GOBOARD2:2 for f being FinSequence of (TOP-REAL 2) for i being Element of NAT st f is unfolded & f is s.n.c. & f is one-to-one & f /. (len f) in LSeg (f,i) & i in dom f & i + 1 in dom f holds i + 1 = len f proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for i being Element of NAT st f is unfolded & f is s.n.c. & f is one-to-one & f /. (len f) in LSeg (f,i) & i in dom f & i + 1 in dom f holds i + 1 = len f let i be Element of NAT ; ::_thesis: ( f is unfolded & f is s.n.c. & f is one-to-one & f /. (len f) in LSeg (f,i) & i in dom f & i + 1 in dom f implies i + 1 = len f ) assume that A1: f is unfolded and A2: f is s.n.c. and A3: f is one-to-one and A4: f /. (len f) in LSeg (f,i) and A5: i in dom f and A6: i + 1 in dom f and A7: i + 1 <> len f ; ::_thesis: contradiction A8: 1 <= i by A5, FINSEQ_3:25; A9: i <= len f by A5, FINSEQ_3:25; then reconsider l = (len f) - 1 as Element of NAT by A8, INT_1:5, XXREAL_0:2; 1 <= len f by A8, A9, XXREAL_0:2; then A10: l + 1 in dom f by FINSEQ_3:25; A11: i + 1 <= len f by A6, FINSEQ_3:25; then i + 1 < len f by A7, XXREAL_0:1; then A12: (i + 1) + 1 <= len f by NAT_1:13; then A13: i + 1 <= (len f) - 1 by XREAL_1:19; i <= l by A11, XREAL_1:19; then A14: 1 <= l by A8, XXREAL_0:2; then A15: f /. (l + 1) in LSeg (f,l) by TOPREAL1:21; 1 <= i + 1 by A6, FINSEQ_3:25; then A16: f /. (i + 2) in LSeg (f,(i + 1)) by A12, TOPREAL1:21; l <= len f by XREAL_1:43; then A17: l in dom f by A14, FINSEQ_3:25; l <> l + 1 ; then A18: f /. l <> f /. (l + 1) by A3, A17, A10, PARTFUN2:10; (i + 1) + 1 = i + (1 + 1) ; then A19: (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} by A1, A8, A12, TOPREAL1:def_6; now__::_thesis:_contradiction percases ( l = i + 1 or l <> i + 1 ) ; supposeA20: l = i + 1 ; ::_thesis: contradiction then f /. (len f) in (LSeg (f,i)) /\ (LSeg (f,(i + 1))) by A4, A16, XBOOLE_0:def_4; hence contradiction by A18, A19, A20, TARSKI:def_1; ::_thesis: verum end; suppose l <> i + 1 ; ::_thesis: contradiction then i + 1 < l by A13, XXREAL_0:1; then LSeg (f,i) misses LSeg (f,l) by A2, TOPREAL1:def_7; then (LSeg (f,i)) /\ (LSeg (f,l)) = {} by XBOOLE_0:def_7; hence contradiction by A4, A15, XBOOLE_0:def_4; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; theorem Th3: :: GOBOARD2:3 for f being FinSequence of (TOP-REAL 2) for k being Element of NAT st k <> 0 & len f = k + 1 holds L~ f = (L~ (f | k)) \/ (LSeg (f,k)) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for k being Element of NAT st k <> 0 & len f = k + 1 holds L~ f = (L~ (f | k)) \/ (LSeg (f,k)) let k be Element of NAT ; ::_thesis: ( k <> 0 & len f = k + 1 implies L~ f = (L~ (f | k)) \/ (LSeg (f,k)) ) assume that A1: k <> 0 and A2: len f = k + 1 ; ::_thesis: L~ f = (L~ (f | k)) \/ (LSeg (f,k)) A3: 0 + 1 <= k by A1, NAT_1:13; set f1 = f | k; set lf = { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ; set l1 = { (LSeg ((f | k),j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len (f | k) ) } ; k <= len f by A2, NAT_1:13; then A4: len (f | k) = k by FINSEQ_1:59; thus L~ f c= (L~ (f | k)) \/ (LSeg (f,k)) :: according to XBOOLE_0:def_10 ::_thesis: (L~ (f | k)) \/ (LSeg (f,k)) c= L~ f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in L~ f or x in (L~ (f | k)) \/ (LSeg (f,k)) ) assume x in L~ f ; ::_thesis: x in (L~ (f | k)) \/ (LSeg (f,k)) then consider X being set such that A5: x in X and A6: X in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } by TARSKI:def_4; consider n being Element of NAT such that A7: X = LSeg (f,n) and A8: 1 <= n and A9: n + 1 <= len f by A6; now__::_thesis:_x_in_(L~_(f_|_k))_\/_(LSeg_(f,k)) percases ( n + 1 = len f or n + 1 <> len f ) ; suppose n + 1 = len f ; ::_thesis: x in (L~ (f | k)) \/ (LSeg (f,k)) hence x in (L~ (f | k)) \/ (LSeg (f,k)) by A2, A5, A7, XBOOLE_0:def_3; ::_thesis: verum end; supposeA10: n + 1 <> len f ; ::_thesis: x in (L~ (f | k)) \/ (LSeg (f,k)) A11: 1 <= n + 1 by A8, NAT_1:13; n <= k by A2, A9, XREAL_1:6; then A12: n in dom (f | k) by A4, A8, FINSEQ_3:25; A13: n + 1 < len f by A9, A10, XXREAL_0:1; then n + 1 <= k by A2, NAT_1:13; then n + 1 in dom (f | k) by A4, A11, FINSEQ_3:25; then A14: X = LSeg ((f | k),n) by A7, A12, TOPREAL3:17; n + 1 <= k by A2, A13, NAT_1:13; then X in { (LSeg ((f | k),j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len (f | k) ) } by A4, A8, A14; then x in union { (LSeg ((f | k),j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len (f | k) ) } by A5, TARSKI:def_4; hence x in (L~ (f | k)) \/ (LSeg (f,k)) by XBOOLE_0:def_3; ::_thesis: verum end; end; end; hence x in (L~ (f | k)) \/ (LSeg (f,k)) ; ::_thesis: verum end; A15: k <= k + 1 by NAT_1:11; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (L~ (f | k)) \/ (LSeg (f,k)) or x in L~ f ) assume A16: x in (L~ (f | k)) \/ (LSeg (f,k)) ; ::_thesis: x in L~ f now__::_thesis:_x_in_L~_f percases ( x in L~ (f | k) or x in LSeg (f,k) ) by A16, XBOOLE_0:def_3; suppose x in L~ (f | k) ; ::_thesis: x in L~ f then consider X being set such that A17: x in X and A18: X in { (LSeg ((f | k),j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len (f | k) ) } by TARSKI:def_4; consider n being Element of NAT such that A19: X = LSeg ((f | k),n) and A20: 1 <= n and A21: n + 1 <= len (f | k) by A18; n <= n + 1 by NAT_1:11; then n <= len (f | k) by A21, XXREAL_0:2; then A22: n in dom (f | k) by A20, FINSEQ_3:25; 1 <= n + 1 by NAT_1:11; then n + 1 in dom (f | k) by A21, FINSEQ_3:25; then A23: X = LSeg (f,n) by A19, A22, TOPREAL3:17; n + 1 <= len f by A2, A15, A4, A21, XXREAL_0:2; then X in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } by A20, A23; hence x in L~ f by A17, TARSKI:def_4; ::_thesis: verum end; supposeA24: x in LSeg (f,k) ; ::_thesis: x in L~ f LSeg (f,k) in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } by A2, A3; hence x in L~ f by A24, TARSKI:def_4; ::_thesis: verum end; end; end; hence x in L~ f ; ::_thesis: verum end; theorem :: GOBOARD2:4 for f being FinSequence of (TOP-REAL 2) for k being Element of NAT st 1 < k & len f = k + 1 & f is unfolded & f is s.n.c. holds (L~ (f | k)) /\ (LSeg (f,k)) = {(f /. k)} proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for k being Element of NAT st 1 < k & len f = k + 1 & f is unfolded & f is s.n.c. holds (L~ (f | k)) /\ (LSeg (f,k)) = {(f /. k)} let k be Element of NAT ; ::_thesis: ( 1 < k & len f = k + 1 & f is unfolded & f is s.n.c. implies (L~ (f | k)) /\ (LSeg (f,k)) = {(f /. k)} ) assume that A1: 1 < k and A2: len f = k + 1 and A3: f is unfolded and A4: f is s.n.c. ; ::_thesis: (L~ (f | k)) /\ (LSeg (f,k)) = {(f /. k)} set f1 = f | k; A5: len (f | k) = k by A2, FINSEQ_1:59, NAT_1:11; reconsider k1 = k - 1 as Element of NAT by A1, INT_1:5; set f2 = (f | k) | k1; set l2 = { (LSeg (((f | k) | k1),m)) where m is Element of NAT : ( 1 <= m & m + 1 <= len ((f | k) | k1) ) } ; A6: dom (f | k) = Seg (len (f | k)) by FINSEQ_1:def_3; A7: k in Seg k by A1, FINSEQ_1:1; A8: dom ((f | k) | k1) = Seg (len ((f | k) | k1)) by FINSEQ_1:def_3; A9: k1 < k by XREAL_1:44; A10: k1 <= k by XREAL_1:44; then A11: len ((f | k) | k1) = k1 by A5, FINSEQ_1:59; A12: Seg k1 c= Seg k by A10, FINSEQ_1:5; L~ ((f | k) | k1) misses LSeg (f,k) proof assume not L~ ((f | k) | k1) misses LSeg (f,k) ; ::_thesis: contradiction then consider x being set such that A13: x in L~ ((f | k) | k1) and A14: x in LSeg (f,k) by XBOOLE_0:3; consider X being set such that A15: x in X and A16: X in { (LSeg (((f | k) | k1),m)) where m is Element of NAT : ( 1 <= m & m + 1 <= len ((f | k) | k1) ) } by A13, TARSKI:def_4; consider n being Element of NAT such that A17: X = LSeg (((f | k) | k1),n) and A18: 1 <= n and A19: n + 1 <= len ((f | k) | k1) by A16; A20: ( n in dom ((f | k) | k1) & n + 1 in dom ((f | k) | k1) ) by A18, A19, SEQ_4:134; then LSeg (((f | k) | k1),n) = LSeg ((f | k),n) by TOPREAL3:17; then LSeg (((f | k) | k1),n) = LSeg (f,n) by A6, A12, A8, A5, A11, A20, TOPREAL3:17; then A21: LSeg (f,n) meets LSeg (f,k) by A14, A15, A17, XBOOLE_0:3; n + 1 < k by A9, A11, A19, XXREAL_0:2; hence contradiction by A4, A21, TOPREAL1:def_7; ::_thesis: verum end; then A22: (L~ ((f | k) | k1)) /\ (LSeg (f,k)) = {} by XBOOLE_0:def_7; A23: k + 1 = k1 + (1 + 1) ; 1 + 1 <= k by A1, NAT_1:13; then A24: 1 <= k1 by XREAL_1:19; then A25: k1 in Seg k by A10, FINSEQ_1:1; k1 + 1 in Seg k by A1, FINSEQ_1:1; then L~ (f | k) = (L~ ((f | k) | k1)) \/ (LSeg ((f | k),k1)) by A24, A5, Th3; hence (L~ (f | k)) /\ (LSeg (f,k)) = {} \/ ((LSeg ((f | k),k1)) /\ (LSeg (f,k))) by A22, XBOOLE_1:23 .= (LSeg (f,k1)) /\ (LSeg (f,(k1 + 1))) by A6, A7, A25, A5, TOPREAL3:17 .= {(f /. k)} by A2, A3, A24, A23, TOPREAL1:def_6 ; ::_thesis: verum end; theorem :: GOBOARD2:5 for f1, f2 being FinSequence of (TOP-REAL 2) for n, m being Element of NAT st len f1 < n & n + 1 <= len (f1 ^ f2) & m + (len f1) = n holds LSeg ((f1 ^ f2),n) = LSeg (f2,m) proof let f1, f2 be FinSequence of (TOP-REAL 2); ::_thesis: for n, m being Element of NAT st len f1 < n & n + 1 <= len (f1 ^ f2) & m + (len f1) = n holds LSeg ((f1 ^ f2),n) = LSeg (f2,m) let n, m be Element of NAT ; ::_thesis: ( len f1 < n & n + 1 <= len (f1 ^ f2) & m + (len f1) = n implies LSeg ((f1 ^ f2),n) = LSeg (f2,m) ) set f = f1 ^ f2; assume that A1: len f1 < n and A2: n + 1 <= len (f1 ^ f2) and A3: m + (len f1) = n ; ::_thesis: LSeg ((f1 ^ f2),n) = LSeg (f2,m) A4: 1 <= m by A1, A3, NAT_1:19; reconsider p = (f1 ^ f2) /. n, q = (f1 ^ f2) /. (n + 1) as Point of (TOP-REAL 2) ; A5: n + 1 = (m + 1) + (len f1) by A3; len (f1 ^ f2) = (len f1) + (len f2) by FINSEQ_1:22; then A6: m + 1 <= len f2 by A2, A5, XREAL_1:6; then A7: (f1 ^ f2) /. (n + 1) = f2 /. (m + 1) by A5, NAT_1:11, SEQ_4:136; m <= m + 1 by NAT_1:11; then m <= len f2 by A6, XXREAL_0:2; then A8: (f1 ^ f2) /. n = f2 /. m by A3, A4, SEQ_4:136; 0 + 1 <= n by A1, NAT_1:13; hence LSeg ((f1 ^ f2),n) = LSeg (p,q) by A2, TOPREAL1:def_3 .= LSeg (f2,m) by A4, A6, A8, A7, TOPREAL1:def_3 ; ::_thesis: verum end; theorem Th6: :: GOBOARD2:6 for f, g being FinSequence of (TOP-REAL 2) holds L~ f c= L~ (f ^ g) proof let f, g be FinSequence of (TOP-REAL 2); ::_thesis: L~ f c= L~ (f ^ g) set f1 = f ^ g; set lf = { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ; set l1 = { (LSeg ((f ^ g),j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len (f ^ g) ) } ; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in L~ f or x in L~ (f ^ g) ) assume x in L~ f ; ::_thesis: x in L~ (f ^ g) then consider X being set such that A1: x in X and A2: X in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } by TARSKI:def_4; consider n being Element of NAT such that A3: X = LSeg (f,n) and A4: 1 <= n and A5: n + 1 <= len f by A2; n <= n + 1 by NAT_1:11; then n <= len f by A5, XXREAL_0:2; then A6: n in dom f by A4, FINSEQ_3:25; len (f ^ g) = (len f) + (len g) by FINSEQ_1:22; then len f <= len (f ^ g) by XREAL_1:31; then A7: n + 1 <= len (f ^ g) by A5, XXREAL_0:2; 1 <= n + 1 by XREAL_1:31; then n + 1 in dom f by A5, FINSEQ_3:25; then X = LSeg ((f ^ g),n) by A3, A6, TOPREAL3:18; then X in { (LSeg ((f ^ g),j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len (f ^ g) ) } by A4, A7; hence x in L~ (f ^ g) by A1, TARSKI:def_4; ::_thesis: verum end; theorem :: GOBOARD2:7 for f being FinSequence of (TOP-REAL 2) for i being Element of NAT st f is s.n.c. holds f | i is s.n.c. proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for i being Element of NAT st f is s.n.c. holds f | i is s.n.c. let i be Element of NAT ; ::_thesis: ( f is s.n.c. implies f | i is s.n.c. ) assume A1: f is s.n.c. ; ::_thesis: f | i is s.n.c. set f1 = f | i; let n, m be Nat; :: according to TOPREAL1:def_7 ::_thesis: ( m <= n + 1 or LSeg ((f | i),n) misses LSeg ((f | i),m) ) assume m > n + 1 ; ::_thesis: LSeg ((f | i),n) misses LSeg ((f | i),m) then LSeg (f,n) misses LSeg (f,m) by A1, TOPREAL1:def_7; then A2: (LSeg (f,n)) /\ (LSeg (f,m)) = {} by XBOOLE_0:def_7; now__::_thesis:_LSeg_((f_|_i),n)_misses_LSeg_((f_|_i),m) A3: m <= m + 1 by NAT_1:11; A4: n <= n + 1 by NAT_1:11; now__::_thesis:_LSeg_((f_|_i),n)_misses_LSeg_((f_|_i),m) percases ( n in dom (f | i) or not n in dom (f | i) ) ; supposeA5: n in dom (f | i) ; ::_thesis: LSeg ((f | i),n) misses LSeg ((f | i),m) now__::_thesis:_LSeg_((f_|_i),n)_misses_LSeg_((f_|_i),m) percases ( n + 1 in dom (f | i) or not n + 1 in dom (f | i) ) ; suppose n + 1 in dom (f | i) ; ::_thesis: LSeg ((f | i),n) misses LSeg ((f | i),m) then A6: LSeg (f,n) = LSeg ((f | i),n) by A5, TOPREAL3:17; now__::_thesis:_LSeg_((f_|_i),n)_misses_LSeg_((f_|_i),m) percases ( m in dom (f | i) or not m in dom (f | i) ) ; supposeA7: m in dom (f | i) ; ::_thesis: LSeg ((f | i),n) misses LSeg ((f | i),m) now__::_thesis:_(LSeg_((f_|_i),n))_/\_(LSeg_((f_|_i),m))_=_{} percases ( m + 1 in dom (f | i) or not m + 1 in dom (f | i) ) ; suppose m + 1 in dom (f | i) ; ::_thesis: (LSeg ((f | i),n)) /\ (LSeg ((f | i),m)) = {} hence (LSeg ((f | i),n)) /\ (LSeg ((f | i),m)) = {} by A2, A6, A7, TOPREAL3:17; ::_thesis: verum end; suppose not m + 1 in dom (f | i) ; ::_thesis: (LSeg ((f | i),n)) /\ (LSeg ((f | i),m)) = {} then ( not 1 <= m + 1 or not m + 1 <= len (f | i) ) by FINSEQ_3:25; then LSeg ((f | i),m) = {} by NAT_1:11, TOPREAL1:def_3; hence (LSeg ((f | i),n)) /\ (LSeg ((f | i),m)) = {} ; ::_thesis: verum end; end; end; hence LSeg ((f | i),n) misses LSeg ((f | i),m) by XBOOLE_0:def_7; ::_thesis: verum end; suppose not m in dom (f | i) ; ::_thesis: LSeg ((f | i),n) misses LSeg ((f | i),m) then ( not 1 <= m or not m <= len (f | i) ) by FINSEQ_3:25; then ( not 1 <= m or not m + 1 <= len (f | i) ) by A3, XXREAL_0:2; then LSeg ((f | i),m) = {} by TOPREAL1:def_3; hence LSeg ((f | i),n) misses LSeg ((f | i),m) by XBOOLE_1:65; ::_thesis: verum end; end; end; hence LSeg ((f | i),n) misses LSeg ((f | i),m) ; ::_thesis: verum end; suppose not n + 1 in dom (f | i) ; ::_thesis: LSeg ((f | i),n) misses LSeg ((f | i),m) then ( not 1 <= n + 1 or not n + 1 <= len (f | i) ) by FINSEQ_3:25; then LSeg ((f | i),n) = {} by NAT_1:11, TOPREAL1:def_3; hence LSeg ((f | i),n) misses LSeg ((f | i),m) by XBOOLE_1:65; ::_thesis: verum end; end; end; hence LSeg ((f | i),n) misses LSeg ((f | i),m) ; ::_thesis: verum end; suppose not n in dom (f | i) ; ::_thesis: LSeg ((f | i),n) misses LSeg ((f | i),m) then ( not 1 <= n or not n <= len (f | i) ) by FINSEQ_3:25; then ( not 1 <= n or not n + 1 <= len (f | i) ) by A4, XXREAL_0:2; then LSeg ((f | i),n) = {} by TOPREAL1:def_3; hence LSeg ((f | i),n) misses LSeg ((f | i),m) by XBOOLE_1:65; ::_thesis: verum end; end; end; hence LSeg ((f | i),n) misses LSeg ((f | i),m) ; ::_thesis: verum end; hence LSeg ((f | i),n) misses LSeg ((f | i),m) ; ::_thesis: verum end; theorem :: GOBOARD2:8 for f1, f2 being FinSequence of (TOP-REAL 2) st f1 is special & f2 is special & ( (f1 /. (len f1)) `1 = (f2 /. 1) `1 or (f1 /. (len f1)) `2 = (f2 /. 1) `2 ) holds f1 ^ f2 is special proof let f1, f2 be FinSequence of (TOP-REAL 2); ::_thesis: ( f1 is special & f2 is special & ( (f1 /. (len f1)) `1 = (f2 /. 1) `1 or (f1 /. (len f1)) `2 = (f2 /. 1) `2 ) implies f1 ^ f2 is special ) assume that A1: f1 is special and A2: f2 is special and A3: ( (f1 /. (len f1)) `1 = (f2 /. 1) `1 or (f1 /. (len f1)) `2 = (f2 /. 1) `2 ) ; ::_thesis: f1 ^ f2 is special let n be Nat; :: according to TOPREAL1:def_5 ::_thesis: ( not 1 <= n or not n + 1 <= len (f1 ^ f2) or ((f1 ^ f2) /. n) `1 = ((f1 ^ f2) /. (n + 1)) `1 or ((f1 ^ f2) /. n) `2 = ((f1 ^ f2) /. (n + 1)) `2 ) set f = f1 ^ f2; assume that A4: 1 <= n and A5: n + 1 <= len (f1 ^ f2) ; ::_thesis: ( ((f1 ^ f2) /. n) `1 = ((f1 ^ f2) /. (n + 1)) `1 or ((f1 ^ f2) /. n) `2 = ((f1 ^ f2) /. (n + 1)) `2 ) reconsider n = n as Element of NAT by ORDINAL1:def_12; set p = (f1 ^ f2) /. n; set q = (f1 ^ f2) /. (n + 1); A6: len (f1 ^ f2) = (len f1) + (len f2) by FINSEQ_1:22; percases ( n + 1 <= len f1 or len f1 < n + 1 ) ; supposeA7: n + 1 <= len f1 ; ::_thesis: ( ((f1 ^ f2) /. n) `1 = ((f1 ^ f2) /. (n + 1)) `1 or ((f1 ^ f2) /. n) `2 = ((f1 ^ f2) /. (n + 1)) `2 ) then n + 1 in dom f1 by A4, SEQ_4:134; then A8: f1 /. (n + 1) = (f1 ^ f2) /. (n + 1) by FINSEQ_4:68; n in dom f1 by A4, A7, SEQ_4:134; then f1 /. n = (f1 ^ f2) /. n by FINSEQ_4:68; hence ( ((f1 ^ f2) /. n) `1 = ((f1 ^ f2) /. (n + 1)) `1 or ((f1 ^ f2) /. n) `2 = ((f1 ^ f2) /. (n + 1)) `2 ) by A1, A4, A7, A8, TOPREAL1:def_5; ::_thesis: verum end; suppose len f1 < n + 1 ; ::_thesis: ( ((f1 ^ f2) /. n) `1 = ((f1 ^ f2) /. (n + 1)) `1 or ((f1 ^ f2) /. n) `2 = ((f1 ^ f2) /. (n + 1)) `2 ) then A9: len f1 <= n by NAT_1:13; then reconsider n1 = n - (len f1) as Element of NAT by INT_1:5; now__::_thesis:_(_((f1_^_f2)_/._n)_`1_=_((f1_^_f2)_/._(n_+_1))_`1_or_((f1_^_f2)_/._n)_`2_=_((f1_^_f2)_/._(n_+_1))_`2_) percases ( n = len f1 or n <> len f1 ) ; supposeA10: n = len f1 ; ::_thesis: ( ((f1 ^ f2) /. n) `1 = ((f1 ^ f2) /. (n + 1)) `1 or ((f1 ^ f2) /. n) `2 = ((f1 ^ f2) /. (n + 1)) `2 ) then n in dom f1 by A4, FINSEQ_3:25; then A11: (f1 ^ f2) /. n = f1 /. n by FINSEQ_4:68; len f2 >= 1 by A5, A6, A10, XREAL_1:6; hence ( ((f1 ^ f2) /. n) `1 = ((f1 ^ f2) /. (n + 1)) `1 or ((f1 ^ f2) /. n) `2 = ((f1 ^ f2) /. (n + 1)) `2 ) by A3, A10, A11, SEQ_4:136; ::_thesis: verum end; suppose n <> len f1 ; ::_thesis: ( ((f1 ^ f2) /. n) `1 = ((f1 ^ f2) /. (n + 1)) `1 or ((f1 ^ f2) /. n) `2 = ((f1 ^ f2) /. (n + 1)) `2 ) then len f1 < n by A9, XXREAL_0:1; then (len f1) + 1 <= n by NAT_1:13; then A12: 1 <= n1 by XREAL_1:19; A13: n + 1 = (n1 + 1) + (len f1) ; then A14: n1 + 1 <= len f2 by A5, A6, XREAL_1:6; then A15: f2 /. (n1 + 1) = (f1 ^ f2) /. (n + 1) by A13, NAT_1:11, SEQ_4:136; n1 + 1 >= n1 by NAT_1:11; then ( n = n1 + (len f1) & n1 <= len f2 ) by A14, XXREAL_0:2; then f2 /. n1 = (f1 ^ f2) /. n by A12, SEQ_4:136; hence ( ((f1 ^ f2) /. n) `1 = ((f1 ^ f2) /. (n + 1)) `1 or ((f1 ^ f2) /. n) `2 = ((f1 ^ f2) /. (n + 1)) `2 ) by A2, A12, A14, A15, TOPREAL1:def_5; ::_thesis: verum end; end; end; hence ( ((f1 ^ f2) /. n) `1 = ((f1 ^ f2) /. (n + 1)) `1 or ((f1 ^ f2) /. n) `2 = ((f1 ^ f2) /. (n + 1)) `2 ) ; ::_thesis: verum end; end; end; theorem Th9: :: GOBOARD2:9 for f being FinSequence of (TOP-REAL 2) st f <> {} holds X_axis f <> {} proof let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f <> {} implies X_axis f <> {} ) A1: len (X_axis f) = len f by GOBOARD1:def_1; assume ( f <> {} & X_axis f = {} ) ; ::_thesis: contradiction hence contradiction by A1; ::_thesis: verum end; theorem Th10: :: GOBOARD2:10 for f being FinSequence of (TOP-REAL 2) st f <> {} holds Y_axis f <> {} proof let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f <> {} implies Y_axis f <> {} ) A1: len (Y_axis f) = len f by GOBOARD1:def_2; assume ( f <> {} & Y_axis f = {} ) ; ::_thesis: contradiction hence contradiction by A1; ::_thesis: verum end; registration let f be non empty FinSequence of (TOP-REAL 2); cluster X_axis f -> non empty ; coherence not X_axis f is empty by Th9; cluster Y_axis f -> non empty ; coherence not Y_axis f is empty by Th10; end; theorem Th11: :: GOBOARD2:11 for f being FinSequence of (TOP-REAL 2) for G being Go-board st f is special holds for n being Element of NAT st n in dom f & n + 1 in dom f holds for i, j, m, k being Element of NAT st [i,j] in Indices G & [m,k] in Indices G & f /. n = G * (i,j) & f /. (n + 1) = G * (m,k) & not i = m holds k = j proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for G being Go-board st f is special holds for n being Element of NAT st n in dom f & n + 1 in dom f holds for i, j, m, k being Element of NAT st [i,j] in Indices G & [m,k] in Indices G & f /. n = G * (i,j) & f /. (n + 1) = G * (m,k) & not i = m holds k = j let G be Go-board; ::_thesis: ( f is special implies for n being Element of NAT st n in dom f & n + 1 in dom f holds for i, j, m, k being Element of NAT st [i,j] in Indices G & [m,k] in Indices G & f /. n = G * (i,j) & f /. (n + 1) = G * (m,k) & not i = m holds k = j ) assume A1: f is special ; ::_thesis: for n being Element of NAT st n in dom f & n + 1 in dom f holds for i, j, m, k being Element of NAT st [i,j] in Indices G & [m,k] in Indices G & f /. n = G * (i,j) & f /. (n + 1) = G * (m,k) & not i = m holds k = j let n be Element of NAT ; ::_thesis: ( n in dom f & n + 1 in dom f implies for i, j, m, k being Element of NAT st [i,j] in Indices G & [m,k] in Indices G & f /. n = G * (i,j) & f /. (n + 1) = G * (m,k) & not i = m holds k = j ) assume ( n in dom f & n + 1 in dom f ) ; ::_thesis: for i, j, m, k being Element of NAT st [i,j] in Indices G & [m,k] in Indices G & f /. n = G * (i,j) & f /. (n + 1) = G * (m,k) & not i = m holds k = j then A2: ( 1 <= n & n + 1 <= len f ) by FINSEQ_3:25; let i, j, m, k be Element of NAT ; ::_thesis: ( [i,j] in Indices G & [m,k] in Indices G & f /. n = G * (i,j) & f /. (n + 1) = G * (m,k) & not i = m implies k = j ) assume that A3: [i,j] in Indices G and A4: [m,k] in Indices G and A5: ( f /. n = G * (i,j) & f /. (n + 1) = G * (m,k) ) ; ::_thesis: ( i = m or k = j ) reconsider cj = Col (G,j), lm = Line (G,m) as FinSequence of (TOP-REAL 2) ; set xj = X_axis cj; set yj = Y_axis cj; set xm = X_axis lm; set ym = Y_axis lm; len cj = len G by MATRIX_1:def_8; then A6: dom cj = dom G by FINSEQ_3:29; assume that A7: i <> m and A8: k <> j ; ::_thesis: contradiction A9: ( len (X_axis lm) = len lm & dom (X_axis lm) = Seg (len (X_axis lm)) ) by FINSEQ_1:def_3, GOBOARD1:def_1; A10: len (X_axis cj) = len cj by GOBOARD1:def_1; then A11: dom (X_axis cj) = dom cj by FINSEQ_3:29; A12: Indices G = [:(dom G),(Seg (width G)):] by MATRIX_1:def_4; then A13: i in dom G by A3, ZFMISC_1:87; then cj /. i = cj . i by A6, PARTFUN1:def_6; then A14: G * (i,j) = cj /. i by A13, MATRIX_1:def_8; then A15: (X_axis cj) . i = (G * (i,j)) `1 by A13, A6, A11, GOBOARD1:def_1; A16: m in dom G by A4, A12, ZFMISC_1:87; then cj /. m = cj . m by A6, PARTFUN1:def_6; then A17: G * (m,j) = cj /. m by A16, MATRIX_1:def_8; then A18: (X_axis cj) . m = (G * (m,j)) `1 by A16, A6, A11, GOBOARD1:def_1; A19: Y_axis lm is increasing by A16, GOBOARD1:def_6; A20: X_axis lm is constant by A16, GOBOARD1:def_4; A21: dom (Y_axis cj) = Seg (len (Y_axis cj)) by FINSEQ_1:def_3; A22: ( dom (X_axis cj) = Seg (len (X_axis cj)) & len (Y_axis cj) = len cj ) by FINSEQ_1:def_3, GOBOARD1:def_2; then A23: (Y_axis cj) . m = (G * (m,j)) `2 by A16, A10, A21, A6, A11, A17, GOBOARD1:def_2; A24: j in Seg (width G) by A3, A12, ZFMISC_1:87; then A25: X_axis cj is increasing by GOBOARD1:def_7; A26: len lm = width G by MATRIX_1:def_7; then A27: dom lm = Seg (width G) by FINSEQ_1:def_3; then lm /. j = lm . j by A24, PARTFUN1:def_6; then A28: G * (m,j) = lm /. j by A24, MATRIX_1:def_7; then A29: (X_axis lm) . j = (G * (m,j)) `1 by A24, A26, A9, GOBOARD1:def_1; A30: k in Seg (width G) by A4, A12, ZFMISC_1:87; then lm /. k = lm . k by A27, PARTFUN1:def_6; then A31: G * (m,k) = lm /. k by A30, MATRIX_1:def_7; then A32: (X_axis lm) . k = (G * (m,k)) `1 by A30, A26, A9, GOBOARD1:def_1; A33: Y_axis cj is constant by A24, GOBOARD1:def_5; A34: ( len (Y_axis lm) = len lm & dom (Y_axis lm) = Seg (len (Y_axis lm)) ) by FINSEQ_1:def_3, GOBOARD1:def_2; then A35: (Y_axis lm) . j = (G * (m,j)) `2 by A24, A26, A28, GOBOARD1:def_2; A36: (Y_axis lm) . k = (G * (m,k)) `2 by A30, A26, A34, A31, GOBOARD1:def_2; A37: (Y_axis cj) . i = (G * (i,j)) `2 by A13, A10, A22, A21, A6, A11, A14, GOBOARD1:def_2; now__::_thesis:_contradiction percases ( (G * (i,j)) `1 = (G * (m,k)) `1 or (G * (i,j)) `2 = (G * (m,k)) `2 ) by A1, A5, A2, TOPREAL1:def_5; supposeA38: (G * (i,j)) `1 = (G * (m,k)) `1 ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( i > m or i < m ) by A7, XXREAL_0:1; suppose i > m ; ::_thesis: contradiction then (G * (m,j)) `1 < (G * (i,j)) `1 by A13, A16, A6, A11, A25, A15, A18, SEQM_3:def_1; hence contradiction by A24, A30, A26, A9, A20, A29, A32, A38, SEQM_3:def_10; ::_thesis: verum end; suppose i < m ; ::_thesis: contradiction then (G * (m,j)) `1 > (G * (i,j)) `1 by A13, A16, A6, A11, A25, A15, A18, SEQM_3:def_1; hence contradiction by A24, A30, A26, A9, A20, A29, A32, A38, SEQM_3:def_10; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; supposeA39: (G * (i,j)) `2 = (G * (m,k)) `2 ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( k > j or k < j ) by A8, XXREAL_0:1; suppose k > j ; ::_thesis: contradiction then (G * (m,j)) `2 < (G * (m,k)) `2 by A24, A30, A26, A34, A19, A35, A36, SEQM_3:def_1; hence contradiction by A13, A16, A10, A22, A21, A6, A11, A33, A37, A23, A39, SEQM_3:def_10; ::_thesis: verum end; suppose k < j ; ::_thesis: contradiction then (G * (m,j)) `2 > (G * (m,k)) `2 by A24, A30, A26, A34, A19, A35, A36, SEQM_3:def_1; hence contradiction by A13, A16, A10, A22, A21, A6, A11, A33, A37, A23, A39, SEQM_3:def_10; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; theorem :: GOBOARD2:12 for f being FinSequence of (TOP-REAL 2) for G being Go-board st ( for n being Element of NAT st n in dom f holds ex i, j being Element of NAT st ( [i,j] in Indices G & f /. n = G * (i,j) ) ) & f is special & ( for n being Element of NAT st n in dom f & n + 1 in dom f holds f /. n <> f /. (n + 1) ) holds ex g being FinSequence of (TOP-REAL 2) st ( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for G being Go-board st ( for n being Element of NAT st n in dom f holds ex i, j being Element of NAT st ( [i,j] in Indices G & f /. n = G * (i,j) ) ) & f is special & ( for n being Element of NAT st n in dom f & n + 1 in dom f holds f /. n <> f /. (n + 1) ) holds ex g being FinSequence of (TOP-REAL 2) st ( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) let G be Go-board; ::_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 G & f /. n = G * (i,j) ) ) & f is special & ( for n being Element of NAT st n in dom f & n + 1 in dom f holds f /. n <> f /. (n + 1) ) implies ex g being FinSequence of (TOP-REAL 2) st ( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) ) defpred S1[ Element of NAT ] means for f being FinSequence of (TOP-REAL 2) st len f = $1 & ( for n being Element of NAT st n in dom f holds ex i, j being Element of NAT st ( [i,j] in Indices G & f /. n = G * (i,j) ) ) & f is special & ( for n being Element of NAT st n in dom f & n + 1 in dom f holds f /. n <> f /. (n + 1) ) holds ex g being FinSequence of (TOP-REAL 2) st ( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ); 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 f be FinSequence of (TOP-REAL 2); ::_thesis: ( len f = k + 1 & ( for n being Element of NAT st n in dom f holds ex i, j being Element of NAT st ( [i,j] in Indices G & f /. n = G * (i,j) ) ) & f is special & ( for n being Element of NAT st n in dom f & n + 1 in dom f holds f /. n <> f /. (n + 1) ) implies ex g being FinSequence of (TOP-REAL 2) st ( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) ) assume that A3: len f = k + 1 and A4: for n being Element of NAT st n in dom f holds ex i, j being Element of NAT st ( [i,j] in Indices G & f /. n = G * (i,j) ) and A5: f is special and A6: for n being Element of NAT st n in dom f & n + 1 in dom f holds f /. n <> f /. (n + 1) ; ::_thesis: ex g being FinSequence of (TOP-REAL 2) st ( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) A7: dom f = Seg (len f) by FINSEQ_1:def_3; now__::_thesis:_ex_g_being_FinSequence_of_(TOP-REAL_2)_st_ (_g_is_sequence_on_G_&_L~_f_=_L~_g_&_g_/._1_=_f_/._1_&_g_/._(len_g)_=_f_/._(len_f)_&_len_f_<=_len_g_) percases ( k = 0 or k <> 0 ) ; supposeA8: k = 0 ; ::_thesis: ex g being FinSequence of (TOP-REAL 2) st ( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) take g = f; ::_thesis: ( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) A9: dom f = {1} by A3, A8, FINSEQ_1:2, FINSEQ_1:def_3; now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_g_&_n_+_1_in_dom_g_holds_ for_i1,_i2,_j1,_j2_being_Element_of_NAT_st_[i1,i2]_in_Indices_G_&_[j1,j2]_in_Indices_G_&_g_/._n_=_G_*_(i1,i2)_&_g_/._(n_+_1)_=_G_*_(j1,j2)_holds_ (abs_(i1_-_j1))_+_(abs_(i2_-_j2))_=_1 let n be Element of NAT ; ::_thesis: ( n in dom g & n + 1 in dom g implies for i1, i2, j1, j2 being Element of NAT st [i1,i2] in Indices G & [j1,j2] in Indices G & g /. n = G * (i1,i2) & g /. (n + 1) = G * (j1,j2) holds (abs (i1 - j1)) + (abs (i2 - j2)) = 1 ) assume that A10: n in dom g and A11: n + 1 in dom g ; ::_thesis: for i1, i2, j1, j2 being Element of NAT st [i1,i2] in Indices G & [j1,j2] in Indices G & g /. n = G * (i1,i2) & g /. (n + 1) = G * (j1,j2) holds (abs (i1 - j1)) + (abs (i2 - j2)) = 1 n = 1 by A9, A10, TARSKI:def_1; hence for i1, i2, j1, j2 being Element of NAT st [i1,i2] in Indices G & [j1,j2] in Indices G & g /. n = G * (i1,i2) & g /. (n + 1) = G * (j1,j2) holds (abs (i1 - j1)) + (abs (i2 - j2)) = 1 by A9, A11, TARSKI:def_1; ::_thesis: verum end; hence ( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) by A4, GOBOARD1:def_9; ::_thesis: verum end; supposeA12: k <> 0 ; ::_thesis: ex g being FinSequence of (TOP-REAL 2) st ( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) then A13: 0 + 1 <= k by NAT_1:13; then A14: k in Seg k by FINSEQ_1:1; A15: 1 in Seg k by A13, FINSEQ_1:1; A16: k <= k + 1 by NAT_1:11; then A17: k in dom f by A3, A7, A13, FINSEQ_1:1; then consider i1, i2 being Element of NAT such that A18: [i1,i2] in Indices G and A19: f /. k = G * (i1,i2) by A4; reconsider l1 = Line (G,i1), c1 = Col (G,i2) as FinSequence of (TOP-REAL 2) ; set x1 = X_axis l1; set y1 = Y_axis l1; set x2 = X_axis c1; set y2 = Y_axis c1; A20: ( dom (Y_axis l1) = Seg (len (Y_axis l1)) & len (Y_axis l1) = len l1 ) by FINSEQ_1:def_3, GOBOARD1:def_2; len (Y_axis c1) = len c1 by GOBOARD1:def_2; then A21: dom (Y_axis c1) = dom c1 by FINSEQ_3:29; len (X_axis c1) = len c1 by GOBOARD1:def_1; then A22: dom (X_axis c1) = dom c1 by FINSEQ_3:29; set f1 = f | k; A23: len (f | k) = k by A3, FINSEQ_1:59, NAT_1:11; A24: dom (f | k) = Seg (len (f | k)) by FINSEQ_1:def_3; A25: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_(f_|_k)_holds_ ex_i,_j_being_Element_of_NAT_st_ (_[i,j]_in_Indices_G_&_(f_|_k)_/._n_=_G_*_(i,j)_) let n be Element of NAT ; ::_thesis: ( n in dom (f | k) implies ex i, j being Element of NAT st ( [i,j] in Indices G & (f | k) /. n = G * (i,j) ) ) assume A26: n in dom (f | k) ; ::_thesis: ex i, j being Element of NAT st ( [i,j] in Indices G & (f | k) /. n = G * (i,j) ) then n in dom f by A17, A23, A24, FINSEQ_4:71; then consider i, j being Element of NAT such that A27: ( [i,j] in Indices G & f /. n = G * (i,j) ) by A4; take i = i; ::_thesis: ex j being Element of NAT st ( [i,j] in Indices G & (f | k) /. n = G * (i,j) ) take j = j; ::_thesis: ( [i,j] in Indices G & (f | k) /. n = G * (i,j) ) thus ( [i,j] in Indices G & (f | k) /. n = G * (i,j) ) by A17, A23, A24, A26, A27, FINSEQ_4:71; ::_thesis: verum end; A28: f | k is special proof let n be Nat; :: according to TOPREAL1:def_5 ::_thesis: ( not 1 <= n or not n + 1 <= len (f | k) or ((f | k) /. n) `1 = ((f | k) /. (n + 1)) `1 or ((f | k) /. n) `2 = ((f | k) /. (n + 1)) `2 ) assume that A29: 1 <= n and A30: n + 1 <= len (f | k) ; ::_thesis: ( ((f | k) /. n) `1 = ((f | k) /. (n + 1)) `1 or ((f | k) /. n) `2 = ((f | k) /. (n + 1)) `2 ) n <= n + 1 by NAT_1:11; then n <= len (f | k) by A30, XXREAL_0:2; then n in dom (f | k) by A29, FINSEQ_3:25; then A31: (f | k) /. n = f /. n by A17, A23, A24, FINSEQ_4:71; 1 <= n + 1 by NAT_1:11; then n + 1 in dom (f | k) by A30, FINSEQ_3:25; then A32: (f | k) /. (n + 1) = f /. (n + 1) by A17, A23, A24, FINSEQ_4:71; n + 1 <= len f by A3, A16, A23, A30, XXREAL_0:2; hence ( ((f | k) /. n) `1 = ((f | k) /. (n + 1)) `1 or ((f | k) /. n) `2 = ((f | k) /. (n + 1)) `2 ) by A5, A29, A31, A32, TOPREAL1:def_5; ::_thesis: verum end; now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_(f_|_k)_&_n_+_1_in_dom_(f_|_k)_holds_ (f_|_k)_/._n_<>_(f_|_k)_/._(n_+_1) let n be Element of NAT ; ::_thesis: ( n in dom (f | k) & n + 1 in dom (f | k) implies (f | k) /. n <> (f | k) /. (n + 1) ) assume A33: ( n in dom (f | k) & n + 1 in dom (f | k) ) ; ::_thesis: (f | k) /. n <> (f | k) /. (n + 1) then A34: ( (f | k) /. n = f /. n & (f | k) /. (n + 1) = f /. (n + 1) ) by A17, A23, A24, FINSEQ_4:71; ( n in dom f & n + 1 in dom f ) by A17, A23, A24, A33, FINSEQ_4:71; hence (f | k) /. n <> (f | k) /. (n + 1) by A6, A34; ::_thesis: verum end; then consider g1 being FinSequence of (TOP-REAL 2) such that A35: g1 is_sequence_on G and A36: L~ g1 = L~ (f | k) and A37: g1 /. 1 = (f | k) /. 1 and A38: g1 /. (len g1) = (f | k) /. (len (f | k)) and A39: len (f | k) <= len g1 by A2, A23, A25, A28; A40: for n being Element of NAT st n in dom g1 holds ex m, k being Element of NAT st ( [m,k] in Indices G & g1 /. n = G * (m,k) ) by A35, GOBOARD1:def_9; A41: for n being Element of NAT st n in dom g1 & n + 1 in dom g1 holds for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & g1 /. n = G * (m,k) & g1 /. (n + 1) = G * (i,j) holds (abs (m - i)) + (abs (k - j)) = 1 by A35, GOBOARD1:def_9; A42: ( dom (X_axis l1) = Seg (len (X_axis l1)) & len (X_axis l1) = len l1 ) by FINSEQ_1:def_3, GOBOARD1:def_1; len c1 = len G by MATRIX_1:def_8; then A43: dom c1 = dom G by FINSEQ_3:29; 1 <= len f by A3, NAT_1:11; then A44: k + 1 in dom f by A3, FINSEQ_3:25; then consider j1, j2 being Element of NAT such that A45: [j1,j2] in Indices G and A46: f /. (k + 1) = G * (j1,j2) by A4; A47: Indices G = [:(dom G),(Seg (width G)):] by MATRIX_1:def_4; then A48: j1 in dom G by A45, ZFMISC_1:87; A49: i1 in dom G by A18, A47, ZFMISC_1:87; then A50: X_axis l1 is constant by GOBOARD1:def_4; A51: i2 in Seg (width G) by A18, A47, ZFMISC_1:87; then A52: X_axis c1 is increasing by GOBOARD1:def_7; A53: Y_axis c1 is constant by A51, GOBOARD1:def_5; A54: Y_axis l1 is increasing by A49, GOBOARD1:def_6; A55: len l1 = width G by MATRIX_1:def_7; A56: j2 in Seg (width G) by A45, A47, ZFMISC_1:87; A57: dom g1 = Seg (len g1) by FINSEQ_1:def_3; now__::_thesis:_ex_g_being_FinSequence_of_(TOP-REAL_2)_st_ (_g_is_sequence_on_G_&_L~_f_=_L~_g_&_g_/._1_=_f_/._1_&_g_/._(len_g)_=_f_/._(len_f)_&_len_f_<=_len_g_) percases ( i1 = j1 or i2 = j2 ) by A5, A17, A18, A19, A44, A45, A46, Th11; supposeA58: i1 = j1 ; ::_thesis: ex g being FinSequence of (TOP-REAL 2) st ( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) set ppi = G * (i1,i2); set pj = G * (i1,j2); now__::_thesis:_(_(_i2_>_j2_&_ex_g_being_FinSequence_of_the_carrier_of_(TOP-REAL_2)_st_ (_g_is_sequence_on_G_&_L~_g_=_L~_f_&_g_/._1_=_f_/._1_&_g_/._(len_g)_=_f_/._(len_f)_&_len_f_<=_len_g_)_)_or_(_i2_=_j2_&_contradiction_)_or_(_i2_<_j2_&_ex_g_being_FinSequence_of_the_carrier_of_(TOP-REAL_2)_st_ (_g_is_sequence_on_G_&_L~_g_=_L~_f_&_g_/._1_=_f_/._1_&_g_/._(len_g)_=_f_/._(len_f)_&_len_f_<=_len_g_)_)_) percases ( i2 > j2 or i2 = j2 or i2 < j2 ) by XXREAL_0:1; caseA59: i2 > j2 ; ::_thesis: ex g being FinSequence of the carrier of (TOP-REAL 2) st ( g is_sequence_on G & L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) j2 in dom l1 by A56, A55, FINSEQ_1:def_3; then l1 /. j2 = l1 . j2 by PARTFUN1:def_6; then A60: l1 /. j2 = G * (i1,j2) by A56, MATRIX_1:def_7; then A61: (Y_axis l1) . j2 = (G * (i1,j2)) `2 by A56, A20, A55, GOBOARD1:def_2; i2 in dom l1 by A51, A55, FINSEQ_1:def_3; then l1 /. i2 = l1 . i2 by PARTFUN1:def_6; then A62: l1 /. i2 = G * (i1,i2) by A51, MATRIX_1:def_7; then A63: (Y_axis l1) . i2 = (G * (i1,i2)) `2 by A51, A20, A55, GOBOARD1:def_2; then A64: (G * (i1,j2)) `2 < (G * (i1,i2)) `2 by A51, A56, A54, A20, A55, A59, A61, SEQM_3:def_1; A65: (X_axis l1) . j2 = (G * (i1,j2)) `1 by A56, A42, A55, A60, GOBOARD1:def_1; (X_axis l1) . i2 = (G * (i1,i2)) `1 by A51, A42, A55, A62, GOBOARD1:def_1; then A66: (G * (i1,i2)) `1 = (G * (i1,j2)) `1 by A51, A56, A50, A42, A55, A65, SEQM_3:def_10; reconsider l = i2 - j2 as Element of NAT by A59, INT_1:5; defpred S2[ Nat, set ] means for m being Element of NAT st m = i2 - $1 holds $2 = G * (i1,m); set lk = { w where w is Point of (TOP-REAL 2) : ( w `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= w `2 & w `2 <= (G * (i1,i2)) `2 ) } ; A67: G * (i1,i2) = |[((G * (i1,i2)) `1),((G * (i1,i2)) `2)]| by EUCLID:53; A68: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_Seg_l_holds_ (_i2_-_n_is_Element_of_NAT_&_[i1,(i2_-_n)]_in_Indices_G_&_i2_-_n_in_Seg_(width_G)_) let n be Element of NAT ; ::_thesis: ( n in Seg l implies ( i2 - n is Element of NAT & [i1,(i2 - n)] in Indices G & i2 - n in Seg (width G) ) ) assume n in Seg l ; ::_thesis: ( i2 - n is Element of NAT & [i1,(i2 - n)] in Indices G & i2 - n in Seg (width G) ) then A69: n <= l by FINSEQ_1:1; l <= i2 by XREAL_1:43; then reconsider w = i2 - n as Element of NAT by A69, INT_1:5, XXREAL_0:2; ( i2 - n <= i2 & i2 <= width G ) by A51, FINSEQ_1:1, XREAL_1:43; then A70: w <= width G by XXREAL_0:2; A71: 1 <= j2 by A56, FINSEQ_1:1; i2 - l <= i2 - n by A69, XREAL_1:13; then 1 <= w by A71, XXREAL_0:2; then w in Seg (width G) by A70, FINSEQ_1:1; hence ( i2 - n is Element of NAT & [i1,(i2 - n)] in Indices G & i2 - n in Seg (width G) ) by A47, A49, ZFMISC_1:87; ::_thesis: verum end; A72: now__::_thesis:_for_n_being_Nat_st_n_in_Seg_l_holds_ ex_p_being_Element_of_the_carrier_of_(TOP-REAL_2)_st_S2[n,p] let n be Nat; ::_thesis: ( n in Seg l implies ex p being Element of the carrier of (TOP-REAL 2) st S2[n,p] ) assume n in Seg l ; ::_thesis: ex p being Element of the carrier of (TOP-REAL 2) st S2[n,p] then reconsider m = i2 - n as Element of NAT by A68; take p = G * (i1,m); ::_thesis: S2[n,p] thus S2[n,p] ; ::_thesis: verum end; consider g2 being FinSequence of (TOP-REAL 2) such that A73: ( len g2 = l & ( for n being Nat st n in Seg l holds S2[n,g2 /. n] ) ) from FINSEQ_4:sch_1(A72); take g = g1 ^ g2; ::_thesis: ( g is_sequence_on G & L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) A74: dom g2 = Seg l by A73, FINSEQ_1:def_3; A75: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_g2_&_n_+_1_in_dom_g2_holds_ for_l1,_l2,_l3,_l4_being_Element_of_NAT_st_[l1,l2]_in_Indices_G_&_[l3,l4]_in_Indices_G_&_g2_/._n_=_G_*_(l1,l2)_&_g2_/._(n_+_1)_=_G_*_(l3,l4)_holds_ (abs_(l1_-_l3))_+_(abs_(l2_-_l4))_=_1 let n be Element of NAT ; ::_thesis: ( n in dom g2 & n + 1 in dom g2 implies for l1, l2, l3, l4 being Element of NAT st [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) holds (abs (l1 - l3)) + (abs (l2 - l4)) = 1 ) assume that A76: n in dom g2 and A77: n + 1 in dom g2 ; ::_thesis: for l1, l2, l3, l4 being Element of NAT st [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) holds (abs (l1 - l3)) + (abs (l2 - l4)) = 1 reconsider m1 = i2 - n, m2 = i2 - (n + 1) as Element of NAT by A68, A74, A76, A77; let l1, l2, l3, l4 be Element of NAT ; ::_thesis: ( [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) implies (abs (l1 - l3)) + (abs (l2 - l4)) = 1 ) assume that A78: [l1,l2] in Indices G and A79: [l3,l4] in Indices G and A80: g2 /. n = G * (l1,l2) and A81: g2 /. (n + 1) = G * (l3,l4) ; ::_thesis: (abs (l1 - l3)) + (abs (l2 - l4)) = 1 ( [i1,(i2 - (n + 1))] in Indices G & g2 /. (n + 1) = G * (i1,m2) ) by A68, A73, A74, A77; then A82: ( l3 = i1 & l4 = m2 ) by A79, A81, GOBOARD1:5; ( [i1,(i2 - n)] in Indices G & g2 /. n = G * (i1,m1) ) by A68, A73, A74, A76; then ( l1 = i1 & l2 = m1 ) by A78, A80, GOBOARD1:5; hence (abs (l1 - l3)) + (abs (l2 - l4)) = 0 + (abs ((i2 - n) - (i2 - (n + 1)))) by A82, ABSVALUE:2 .= 1 by ABSVALUE:def_1 ; ::_thesis: verum end; now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_g2_holds_ ex_k,_m_being_Element_of_NAT_st_ (_[k,m]_in_Indices_G_&_g2_/._n_=_G_*_(k,m)_) let n be Element of NAT ; ::_thesis: ( n in dom g2 implies ex k, m being Element of NAT st ( [k,m] in Indices G & g2 /. n = G * (k,m) ) ) assume A83: n in dom g2 ; ::_thesis: ex k, m being Element of NAT st ( [k,m] in Indices G & g2 /. n = G * (k,m) ) then reconsider m = i2 - n as Element of NAT by A68, A74; take k = i1; ::_thesis: ex m being Element of NAT st ( [k,m] in Indices G & g2 /. n = G * (k,m) ) take m = m; ::_thesis: ( [k,m] in Indices G & g2 /. n = G * (k,m) ) thus ( [k,m] in Indices G & g2 /. n = G * (k,m) ) by A68, A73, A74, A83; ::_thesis: verum end; then A84: for n being Element of NAT st n in dom g holds ex i, j being Element of NAT st ( [i,j] in Indices G & g /. n = G * (i,j) ) by A40, GOBOARD1:23; now__::_thesis:_for_l1,_l2,_l3,_l4_being_Element_of_NAT_st_[l1,l2]_in_Indices_G_&_[l3,l4]_in_Indices_G_&_g1_/._(len_g1)_=_G_*_(l1,l2)_&_g2_/._1_=_G_*_(l3,l4)_&_len_g1_in_dom_g1_&_1_in_dom_g2_holds_ (abs_(l1_-_l3))_+_(abs_(l2_-_l4))_=_1 let l1, l2, l3, l4 be Element of NAT ; ::_thesis: ( [l1,l2] in Indices G & [l3,l4] in Indices G & g1 /. (len g1) = G * (l1,l2) & g2 /. 1 = G * (l3,l4) & len g1 in dom g1 & 1 in dom g2 implies (abs (l1 - l3)) + (abs (l2 - l4)) = 1 ) assume that A85: [l1,l2] in Indices G and A86: [l3,l4] in Indices G and A87: g1 /. (len g1) = G * (l1,l2) and A88: g2 /. 1 = G * (l3,l4) and len g1 in dom g1 and A89: 1 in dom g2 ; ::_thesis: (abs (l1 - l3)) + (abs (l2 - l4)) = 1 reconsider m1 = i2 - 1 as Element of NAT by A68, A74, A89; ( [i1,(i2 - 1)] in Indices G & g2 /. 1 = G * (i1,m1) ) by A68, A73, A74, A89; then A90: ( l3 = i1 & l4 = m1 ) by A86, A88, GOBOARD1:5; (f | k) /. (len (f | k)) = f /. k by A17, A23, A14, FINSEQ_4:71; then ( l1 = i1 & l2 = i2 ) by A38, A18, A19, A85, A87, GOBOARD1:5; hence (abs (l1 - l3)) + (abs (l2 - l4)) = 0 + (abs (i2 - (i2 - 1))) by A90, ABSVALUE:2 .= 1 by ABSVALUE:def_1 ; ::_thesis: verum end; then for n being Element of NAT st n in dom g & n + 1 in dom g holds for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & g /. n = G * (m,k) & g /. (n + 1) = G * (i,j) holds (abs (m - i)) + (abs (k - j)) = 1 by A41, A75, GOBOARD1:24; hence g is_sequence_on G by A84, GOBOARD1:def_9; ::_thesis: ( L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) reconsider m1 = i2 - l as Element of NAT ; A91: G * (i1,j2) = |[((G * (i1,j2)) `1),((G * (i1,j2)) `2)]| by EUCLID:53; A92: LSeg (f,k) = LSeg ((G * (i1,j2)),(G * (i1,i2))) by A3, A13, A19, A46, A58, TOPREAL1:def_3 .= { w where w is Point of (TOP-REAL 2) : ( w `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= w `2 & w `2 <= (G * (i1,i2)) `2 ) } by A64, A66, A67, A91, TOPREAL3:9 ; thus L~ g = L~ f ::_thesis: ( g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) proof set lg = { (LSeg (g,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } ; set lf = { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } ; A93: len g = (len g1) + (len g2) by FINSEQ_1:22; A94: now__::_thesis:_for_j_being_Element_of_NAT_st_len_g1_<=_j_&_j_<=_len_g_holds_ for_p_being_Point_of_(TOP-REAL_2)_st_p_=_g_/._j_holds_ (_p_`1_=_(G_*_(i1,i2))_`1_&_(G_*_(i1,j2))_`2_<=_p_`2_&_p_`2_<=_(G_*_(i1,i2))_`2_&_p_in_rng_l1_) let j be Element of NAT ; ::_thesis: ( len g1 <= j & j <= len g implies for p being Point of (TOP-REAL 2) st p = g /. j holds ( p `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 & p in rng l1 ) ) assume that A95: len g1 <= j and A96: j <= len g ; ::_thesis: for p being Point of (TOP-REAL 2) st p = g /. j holds ( p `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 & p in rng l1 ) reconsider w = j - (len g1) as Element of NAT by A95, INT_1:5; let p be Point of (TOP-REAL 2); ::_thesis: ( p = g /. j implies ( p `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 & p in rng l1 ) ) assume A97: p = g /. j ; ::_thesis: ( p `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 & p in rng l1 ) A98: dom l1 = Seg (len l1) by FINSEQ_1:def_3; now__::_thesis:_(_p_`1_=_(G_*_(i1,i2))_`1_&_(G_*_(i1,j2))_`2_<=_p_`2_&_p_`2_<=_(G_*_(i1,i2))_`2_&_p_in_rng_l1_) percases ( j = len g1 or j <> len g1 ) ; supposeA99: j = len g1 ; ::_thesis: ( p `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 & p in rng l1 ) 1 <= len g1 by A13, A23, A39, XXREAL_0:2; then len g1 in dom g1 by FINSEQ_3:25; then A100: g /. (len g1) = (f | k) /. (len (f | k)) by A38, FINSEQ_4:68 .= G * (i1,i2) by A17, A23, A14, A19, FINSEQ_4:71 ; hence p `1 = (G * (i1,i2)) `1 by A97, A99; ::_thesis: ( (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 & p in rng l1 ) thus ( (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 ) by A51, A56, A54, A20, A55, A59, A63, A61, A97, A99, A100, SEQM_3:def_1; ::_thesis: p in rng l1 thus p in rng l1 by A51, A55, A62, A97, A98, A99, A100, PARTFUN2:2; ::_thesis: verum end; supposeA101: j <> len g1 ; ::_thesis: ( p `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 & p in rng l1 ) A102: w + (len g1) = j ; then A103: w <= len g2 by A93, A96, XREAL_1:6; A104: j - (len g1) <> 0 by A101; then A105: w >= 1 by NAT_1:14; then A106: w in dom g2 by A103, FINSEQ_3:25; then reconsider u = i2 - w as Element of NAT by A68, A74; A107: g /. j = g2 /. w by A105, A102, A103, SEQ_4:136; A108: (X_axis l1) . i2 = (G * (i1,i2)) `1 by A51, A42, A55, A62, GOBOARD1:def_1; A109: u < i2 by A104, XREAL_1:44; A110: g2 /. w = G * (i1,u) by A73, A74, A106; A111: i2 - w in Seg (width G) by A68, A74, A106; then u in dom l1 by A55, FINSEQ_1:def_3; then l1 /. u = l1 . u by PARTFUN1:def_6; then A112: l1 /. u = G * (i1,u) by A111, MATRIX_1:def_7; then A113: (Y_axis l1) . u = (G * (i1,u)) `2 by A20, A55, A111, GOBOARD1:def_2; (X_axis l1) . u = (G * (i1,u)) `1 by A42, A55, A111, A112, GOBOARD1:def_1; hence p `1 = (G * (i1,i2)) `1 by A51, A50, A42, A55, A97, A107, A111, A110, A108, SEQM_3:def_10; ::_thesis: ( (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 & p in rng l1 ) A114: (Y_axis l1) . j2 = (G * (i1,j2)) `2 by A56, A20, A55, A60, GOBOARD1:def_2; now__::_thesis:_(G_*_(i1,j2))_`2_<=_p_`2 percases ( u = j2 or u <> j2 ) ; suppose u = j2 ; ::_thesis: (G * (i1,j2)) `2 <= p `2 hence (G * (i1,j2)) `2 <= p `2 by A97, A105, A102, A103, A110, SEQ_4:136; ::_thesis: verum end; supposeA115: u <> j2 ; ::_thesis: (G * (i1,j2)) `2 <= p `2 i2 - (len g2) <= u by A103, XREAL_1:13; then j2 < u by A73, A115, XXREAL_0:1; hence (G * (i1,j2)) `2 <= p `2 by A56, A54, A20, A55, A97, A107, A111, A110, A113, A114, SEQM_3:def_1; ::_thesis: verum end; end; end; hence (G * (i1,j2)) `2 <= p `2 ; ::_thesis: ( p `2 <= (G * (i1,i2)) `2 & p in rng l1 ) (Y_axis l1) . i2 = (G * (i1,i2)) `2 by A51, A20, A55, A62, GOBOARD1:def_2; hence p `2 <= (G * (i1,i2)) `2 by A51, A54, A20, A55, A97, A107, A111, A110, A113, A109, SEQM_3:def_1; ::_thesis: p in rng l1 thus p in rng l1 by A55, A97, A98, A107, A111, A110, A112, PARTFUN2:2; ::_thesis: verum end; end; end; hence ( p `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 & p in rng l1 ) ; ::_thesis: verum end; thus L~ g c= L~ f :: according to XBOOLE_0:def_10 ::_thesis: L~ f c= L~ g proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in L~ g or x in L~ f ) assume x in L~ g ; ::_thesis: x in L~ f then consider X being set such that A116: x in X and A117: X in { (LSeg (g,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } by TARSKI:def_4; consider i being Element of NAT such that A118: X = LSeg (g,i) and A119: 1 <= i and A120: i + 1 <= len g by A117; now__::_thesis:_x_in_L~_f percases ( i + 1 <= len g1 or i + 1 > len g1 ) ; supposeA121: i + 1 <= len g1 ; ::_thesis: x in L~ f i <= i + 1 by NAT_1:11; then i <= len g1 by A121, XXREAL_0:2; then A122: i in dom g1 by A119, FINSEQ_3:25; 1 <= i + 1 by NAT_1:11; then i + 1 in dom g1 by A121, FINSEQ_3:25; then X = LSeg (g1,i) by A118, A122, TOPREAL3:18; then X in { (LSeg (g1,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g1 ) } by A119, A121; then A123: x in L~ (f | k) by A36, A116, TARSKI:def_4; L~ (f | k) c= L~ f by TOPREAL3:20; hence x in L~ f by A123; ::_thesis: verum end; supposeA124: i + 1 > len g1 ; ::_thesis: x in L~ f reconsider q1 = g /. i, q2 = g /. (i + 1) as Point of (TOP-REAL 2) ; A125: i <= len g by A120, NAT_1:13; A126: len g1 <= i by A124, NAT_1:13; then A127: q1 `1 = (G * (i1,i2)) `1 by A94, A125; A128: q1 `2 <= (G * (i1,i2)) `2 by A94, A126, A125; A129: (G * (i1,j2)) `2 <= q1 `2 by A94, A126, A125; q2 `1 = (G * (i1,i2)) `1 by A94, A120, A124; then A130: q2 = |[(q1 `1),(q2 `2)]| by A127, EUCLID:53; A131: q2 `2 <= (G * (i1,i2)) `2 by A94, A120, A124; A132: ( q1 = |[(q1 `1),(q1 `2)]| & LSeg (g,i) = LSeg (q2,q1) ) by A119, A120, EUCLID:53, TOPREAL1:def_3; A133: (G * (i1,j2)) `2 <= q2 `2 by A94, A120, A124; now__::_thesis:_x_in_L~_f percases ( q1 `2 > q2 `2 or q1 `2 = q2 `2 or q1 `2 < q2 `2 ) by XXREAL_0:1; suppose q1 `2 > q2 `2 ; ::_thesis: x in L~ f then LSeg (g,i) = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = q1 `1 & q2 `2 <= p2 `2 & p2 `2 <= q1 `2 ) } by A130, A132, TOPREAL3:9; then consider p2 being Point of (TOP-REAL 2) such that A134: ( p2 = x & p2 `1 = q1 `1 ) and A135: ( q2 `2 <= p2 `2 & p2 `2 <= q1 `2 ) by A116, A118; ( (G * (i1,j2)) `2 <= p2 `2 & p2 `2 <= (G * (i1,i2)) `2 ) by A128, A133, A135, XXREAL_0:2; then A136: x in LSeg (f,k) by A92, A127, A134; LSeg (f,k) in { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } by A3, A13; hence x in L~ f by A136, TARSKI:def_4; ::_thesis: verum end; suppose q1 `2 = q2 `2 ; ::_thesis: x in L~ f then LSeg (g,i) = {q1} by A130, A132, RLTOPSP1:70; then x = q1 by A116, A118, TARSKI:def_1; then A137: x in LSeg (f,k) by A92, A127, A129, A128; LSeg (f,k) in { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } by A3, A13; hence x in L~ f by A137, TARSKI:def_4; ::_thesis: verum end; suppose q1 `2 < q2 `2 ; ::_thesis: x in L~ f then LSeg (g,i) = { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `1 = q1 `1 & q1 `2 <= p1 `2 & p1 `2 <= q2 `2 ) } by A130, A132, TOPREAL3:9; then consider p2 being Point of (TOP-REAL 2) such that A138: ( p2 = x & p2 `1 = q1 `1 ) and A139: ( q1 `2 <= p2 `2 & p2 `2 <= q2 `2 ) by A116, A118; ( (G * (i1,j2)) `2 <= p2 `2 & p2 `2 <= (G * (i1,i2)) `2 ) by A129, A131, A139, XXREAL_0:2; then A140: x in LSeg (f,k) by A92, A127, A138; LSeg (f,k) in { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } by A3, A13; hence x in L~ f by A140, TARSKI:def_4; ::_thesis: verum end; end; end; hence x in L~ f ; ::_thesis: verum end; end; end; hence x in L~ f ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in L~ f or x in L~ g ) assume x in L~ f ; ::_thesis: x in L~ g then A141: x in (L~ (f | k)) \/ (LSeg (f,k)) by A3, A12, Th3; now__::_thesis:_x_in_L~_g percases ( x in L~ (f | k) or x in LSeg (f,k) ) by A141, XBOOLE_0:def_3; supposeA142: x in L~ (f | k) ; ::_thesis: x in L~ g L~ g1 c= L~ g by Th6; hence x in L~ g by A36, A142; ::_thesis: verum end; suppose x in LSeg (f,k) ; ::_thesis: x in L~ g then consider p1 being Point of (TOP-REAL 2) such that A143: p1 = x and A144: p1 `1 = (G * (i1,i2)) `1 and A145: (G * (i1,j2)) `2 <= p1 `2 and A146: p1 `2 <= (G * (i1,i2)) `2 by A92; defpred S3[ Nat] means ( len g1 <= $1 & $1 <= len g & ( for q being Point of (TOP-REAL 2) st q = g /. $1 holds q `2 >= p1 `2 ) ); A147: now__::_thesis:_ex_n_being_Nat_st_S3[n] reconsider n = len g1 as Nat ; take n = n; ::_thesis: S3[n] thus S3[n] ::_thesis: verum proof thus ( len g1 <= n & n <= len g ) by A93, XREAL_1:31; ::_thesis: for q being Point of (TOP-REAL 2) st q = g /. n holds q `2 >= p1 `2 1 <= len g1 by A13, A23, A39, XXREAL_0:2; then A148: len g1 in dom g1 by FINSEQ_3:25; let q be Point of (TOP-REAL 2); ::_thesis: ( q = g /. n implies q `2 >= p1 `2 ) assume q = g /. n ; ::_thesis: q `2 >= p1 `2 then q = (f | k) /. (len (f | k)) by A38, A148, FINSEQ_4:68 .= G * (i1,i2) by A17, A23, A14, A19, FINSEQ_4:71 ; hence q `2 >= p1 `2 by A146; ::_thesis: verum end; end; A149: for n being Nat st S3[n] holds n <= len g ; consider ma being Nat such that A150: ( S3[ma] & ( for n being Nat st S3[n] holds n <= ma ) ) from NAT_1:sch_6(A149, A147); reconsider ma = ma as Element of NAT by ORDINAL1:def_12; now__::_thesis:_x_in_L~_g percases ( ma = len g or ma <> len g ) ; supposeA151: ma = len g ; ::_thesis: x in L~ g j2 + 1 <= i2 by A59, NAT_1:13; then A152: 1 <= l by XREAL_1:19; then 0 + 1 <= ma by A73, A93, A151, XREAL_1:7; then reconsider m1 = ma - 1 as Element of NAT by INT_1:5; A153: m1 + 1 = ma ; (len g1) + 1 <= ma by A73, A93, A151, A152, XREAL_1:7; then A154: m1 >= len g1 by A153, XREAL_1:6; reconsider q = g /. m1 as Point of (TOP-REAL 2) ; set lq = { e where e is Point of (TOP-REAL 2) : ( e `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= e `2 & e `2 <= q `2 ) } ; A155: i2 - l = j2 ; A156: l in dom g2 by A74, A152, FINSEQ_1:1; then A157: g /. ma = g2 /. l by A73, A93, A151, FINSEQ_4:69 .= G * (i1,j2) by A73, A74, A156, A155 ; then p1 `2 <= (G * (i1,j2)) `2 by A150; then A158: p1 `2 = (G * (i1,j2)) `2 by A145, XXREAL_0:1; A159: m1 <= len g by A151, A153, NAT_1:11; then A160: q `1 = (G * (i1,i2)) `1 by A94, A154; A161: (G * (i1,j2)) `2 <= q `2 by A94, A154, A159; 1 <= len g1 by A13, A23, A39, XXREAL_0:2; then A162: 1 <= m1 by A154, XXREAL_0:2; then ( q = |[(q `1),(q `2)]| & LSeg (g,m1) = LSeg ((G * (i1,j2)),q) ) by A151, A157, A153, EUCLID:53, TOPREAL1:def_3; then LSeg (g,m1) = { e where e is Point of (TOP-REAL 2) : ( e `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= e `2 & e `2 <= q `2 ) } by A66, A91, A160, A161, TOPREAL3:9; then A163: p1 in LSeg (g,m1) by A144, A158, A161; LSeg (g,m1) in { (LSeg (g,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } by A151, A153, A162; hence x in L~ g by A143, A163, TARSKI:def_4; ::_thesis: verum end; suppose ma <> len g ; ::_thesis: x in L~ g then ma < len g by A150, XXREAL_0:1; then A164: ma + 1 <= len g by NAT_1:13; reconsider qa = g /. ma, qa1 = g /. (ma + 1) as Point of (TOP-REAL 2) ; set lma = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = (G * (i1,i2)) `1 & qa1 `2 <= p2 `2 & p2 `2 <= qa `2 ) } ; A165: qa1 = |[(qa1 `1),(qa1 `2)]| by EUCLID:53; A166: p1 `2 <= qa `2 by A150; A167: len g1 <= ma + 1 by A150, NAT_1:13; then A168: qa1 `1 = (G * (i1,i2)) `1 by A94, A164; A169: now__::_thesis:_not_p1_`2_<=_qa1_`2 assume p1 `2 <= qa1 `2 ; ::_thesis: contradiction then for q being Point of (TOP-REAL 2) st q = g /. (ma + 1) holds p1 `2 <= q `2 ; then ma + 1 <= ma by A150, A164, A167; hence contradiction by XREAL_1:29; ::_thesis: verum end; A170: ( qa `1 = (G * (i1,i2)) `1 & qa = |[(qa `1),(qa `2)]| ) by A94, A150, EUCLID:53; A171: 1 <= ma by A13, A23, A39, A150, NAT_1:13; then LSeg (g,ma) = LSeg (qa1,qa) by A164, TOPREAL1:def_3 .= { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = (G * (i1,i2)) `1 & qa1 `2 <= p2 `2 & p2 `2 <= qa `2 ) } by A166, A169, A168, A170, A165, TOPREAL3:9, XXREAL_0:2 ; then A172: x in LSeg (g,ma) by A143, A144, A166, A169; LSeg (g,ma) in { (LSeg (g,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } by A171, A164; hence x in L~ g by A172, TARSKI:def_4; ::_thesis: verum end; end; end; hence x in L~ g ; ::_thesis: verum end; end; end; hence x in L~ g ; ::_thesis: verum end; 1 <= len g1 by A13, A23, A39, XXREAL_0:2; then 1 in dom g1 by FINSEQ_3:25; hence g /. 1 = (f | k) /. 1 by A37, FINSEQ_4:68 .= f /. 1 by A17, A15, FINSEQ_4:71 ; ::_thesis: ( g /. (len g) = f /. (len f) & len f <= len g ) A173: len g = (len g1) + (len g2) by FINSEQ_1:22; j2 + 1 <= i2 by A59, NAT_1:13; then A174: 1 <= l by XREAL_1:19; then A175: l in dom g2 by A74, FINSEQ_1:1; hence g /. (len g) = g2 /. l by A73, A173, FINSEQ_4:69 .= G * (i1,m1) by A73, A74, A175 .= f /. (len f) by A3, A46, A58 ; ::_thesis: len f <= len g thus len f <= len g by A3, A23, A39, A73, A174, A173, XREAL_1:7; ::_thesis: verum end; case i2 = j2 ; ::_thesis: contradiction hence contradiction by A6, A17, A19, A44, A46, A58; ::_thesis: verum end; caseA176: i2 < j2 ; ::_thesis: ex g being FinSequence of the carrier of (TOP-REAL 2) st ( g is_sequence_on G & L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) set lk = { w where w is Point of (TOP-REAL 2) : ( w `1 = (G * (i1,i2)) `1 & (G * (i1,i2)) `2 <= w `2 & w `2 <= (G * (i1,j2)) `2 ) } ; A177: G * (i1,i2) = |[((G * (i1,i2)) `1),((G * (i1,i2)) `2)]| by EUCLID:53; reconsider l = j2 - i2 as Element of NAT by A176, INT_1:5; deffunc H1( Nat) -> Element of the carrier of (TOP-REAL 2) = G * (i1,(i2 + $1)); consider g2 being FinSequence of (TOP-REAL 2) such that A178: ( len g2 = l & ( for n being Nat st n in dom g2 holds g2 /. n = H1(n) ) ) from FINSEQ_4:sch_2(); take g = g1 ^ g2; ::_thesis: ( g is_sequence_on G & L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) A179: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_Seg_l_holds_ (_i2_+_n_in_Seg_(width_G)_&_[i1,(i2_+_n)]_in_Indices_G_) let n be Element of NAT ; ::_thesis: ( n in Seg l implies ( i2 + n in Seg (width G) & [i1,(i2 + n)] in Indices G ) ) A180: n <= i2 + n by NAT_1:11; assume A181: n in Seg l ; ::_thesis: ( i2 + n in Seg (width G) & [i1,(i2 + n)] in Indices G ) then n <= l by FINSEQ_1:1; then A182: i2 + n <= l + i2 by XREAL_1:7; j2 <= width G by A56, FINSEQ_1:1; then A183: i2 + n <= width G by A182, XXREAL_0:2; 1 <= n by A181, FINSEQ_1:1; then 1 <= i2 + n by A180, XXREAL_0:2; hence i2 + n in Seg (width G) by A183, FINSEQ_1:1; ::_thesis: [i1,(i2 + n)] in Indices G hence [i1,(i2 + n)] in Indices G by A47, A49, ZFMISC_1:87; ::_thesis: verum end; A184: dom g2 = Seg (len g2) by FINSEQ_1:def_3; now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_g2_holds_ ex_m_being_Element_of_NAT_ex_k_being_Element_of_NAT_st_ (_[m,k]_in_Indices_G_&_g2_/._n_=_G_*_(m,k)_) let n be Element of NAT ; ::_thesis: ( n in dom g2 implies ex m being Element of NAT ex k being Element of NAT st ( [m,k] in Indices G & g2 /. n = G * (m,k) ) ) assume A185: n in dom g2 ; ::_thesis: ex m being Element of NAT ex k being Element of NAT st ( [m,k] in Indices G & g2 /. n = G * (m,k) ) take m = i1; ::_thesis: ex k being Element of NAT st ( [m,k] in Indices G & g2 /. n = G * (m,k) ) take k = i2 + n; ::_thesis: ( [m,k] in Indices G & g2 /. n = G * (m,k) ) thus ( [m,k] in Indices G & g2 /. n = G * (m,k) ) by A178, A179, A184, A185; ::_thesis: verum end; then A186: for n being Element of NAT st n in dom g holds ex i, j being Element of NAT st ( [i,j] in Indices G & g /. n = G * (i,j) ) by A40, GOBOARD1:23; A187: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_g2_&_n_+_1_in_dom_g2_holds_ for_l1,_l2,_l3,_l4_being_Element_of_NAT_st_[l1,l2]_in_Indices_G_&_[l3,l4]_in_Indices_G_&_g2_/._n_=_G_*_(l1,l2)_&_g2_/._(n_+_1)_=_G_*_(l3,l4)_holds_ (abs_(l1_-_l3))_+_(abs_(l2_-_l4))_=_1 let n be Element of NAT ; ::_thesis: ( n in dom g2 & n + 1 in dom g2 implies for l1, l2, l3, l4 being Element of NAT st [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) holds (abs (l1 - l3)) + (abs (l2 - l4)) = 1 ) assume that A188: n in dom g2 and A189: n + 1 in dom g2 ; ::_thesis: for l1, l2, l3, l4 being Element of NAT st [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) holds (abs (l1 - l3)) + (abs (l2 - l4)) = 1 let l1, l2, l3, l4 be Element of NAT ; ::_thesis: ( [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) implies (abs (l1 - l3)) + (abs (l2 - l4)) = 1 ) assume that A190: [l1,l2] in Indices G and A191: [l3,l4] in Indices G and A192: g2 /. n = G * (l1,l2) and A193: g2 /. (n + 1) = G * (l3,l4) ; ::_thesis: (abs (l1 - l3)) + (abs (l2 - l4)) = 1 ( g2 /. (n + 1) = G * (i1,(i2 + (n + 1))) & [i1,(i2 + (n + 1))] in Indices G ) by A178, A179, A184, A189; then A194: ( l3 = i1 & l4 = i2 + (n + 1) ) by A191, A193, GOBOARD1:5; ( g2 /. n = G * (i1,(i2 + n)) & [i1,(i2 + n)] in Indices G ) by A178, A179, A184, A188; then ( l1 = i1 & l2 = i2 + n ) by A190, A192, GOBOARD1:5; hence (abs (l1 - l3)) + (abs (l2 - l4)) = 0 + (abs ((i2 + n) - (i2 + (n + 1)))) by A194, ABSVALUE:2 .= abs (- 1) .= abs 1 by COMPLEX1:52 .= 1 by ABSVALUE:def_1 ; ::_thesis: verum end; now__::_thesis:_for_l1,_l2,_l3,_l4_being_Element_of_NAT_st_[l1,l2]_in_Indices_G_&_[l3,l4]_in_Indices_G_&_g1_/._(len_g1)_=_G_*_(l1,l2)_&_g2_/._1_=_G_*_(l3,l4)_&_len_g1_in_dom_g1_&_1_in_dom_g2_holds_ (abs_(l1_-_l3))_+_(abs_(l2_-_l4))_=_1 let l1, l2, l3, l4 be Element of NAT ; ::_thesis: ( [l1,l2] in Indices G & [l3,l4] in Indices G & g1 /. (len g1) = G * (l1,l2) & g2 /. 1 = G * (l3,l4) & len g1 in dom g1 & 1 in dom g2 implies (abs (l1 - l3)) + (abs (l2 - l4)) = 1 ) assume that A195: [l1,l2] in Indices G and A196: [l3,l4] in Indices G and A197: g1 /. (len g1) = G * (l1,l2) and A198: g2 /. 1 = G * (l3,l4) and len g1 in dom g1 and A199: 1 in dom g2 ; ::_thesis: (abs (l1 - l3)) + (abs (l2 - l4)) = 1 ( g2 /. 1 = G * (i1,(i2 + 1)) & [i1,(i2 + 1)] in Indices G ) by A178, A179, A184, A199; then A200: ( l3 = i1 & l4 = i2 + 1 ) by A196, A198, GOBOARD1:5; (f | k) /. (len (f | k)) = f /. k by A17, A23, A14, FINSEQ_4:71; then ( l1 = i1 & l2 = i2 ) by A38, A18, A19, A195, A197, GOBOARD1:5; hence (abs (l1 - l3)) + (abs (l2 - l4)) = 0 + (abs (i2 - (i2 + 1))) by A200, ABSVALUE:2 .= abs ((i2 - i2) + (- 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 g & n + 1 in dom g holds for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & g /. n = G * (m,k) & g /. (n + 1) = G * (i,j) holds (abs (m - i)) + (abs (k - j)) = 1 by A41, A187, GOBOARD1:24; hence g is_sequence_on G by A186, GOBOARD1:def_9; ::_thesis: ( L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) A201: G * (i1,j2) = |[((G * (i1,j2)) `1),((G * (i1,j2)) `2)]| by EUCLID:53; j2 in dom l1 by A56, A55, FINSEQ_1:def_3; then l1 /. j2 = l1 . j2 by PARTFUN1:def_6; then A202: l1 /. j2 = G * (i1,j2) by A56, MATRIX_1:def_7; then A203: (Y_axis l1) . j2 = (G * (i1,j2)) `2 by A56, A20, A55, GOBOARD1:def_2; i2 in dom l1 by A51, A55, FINSEQ_1:def_3; then l1 /. i2 = l1 . i2 by PARTFUN1:def_6; then A204: l1 /. i2 = G * (i1,i2) by A51, MATRIX_1:def_7; then A205: (Y_axis l1) . i2 = (G * (i1,i2)) `2 by A51, A20, A55, GOBOARD1:def_2; then A206: (G * (i1,i2)) `2 < (G * (i1,j2)) `2 by A51, A56, A54, A20, A55, A176, A203, SEQM_3:def_1; A207: (X_axis l1) . j2 = (G * (i1,j2)) `1 by A56, A42, A55, A202, GOBOARD1:def_1; (X_axis l1) . i2 = (G * (i1,i2)) `1 by A51, A42, A55, A204, GOBOARD1:def_1; then A208: (G * (i1,i2)) `1 = (G * (i1,j2)) `1 by A51, A56, A50, A42, A55, A207, SEQM_3:def_10; A209: LSeg (f,k) = LSeg ((G * (i1,i2)),(G * (i1,j2))) by A3, A13, A19, A46, A58, TOPREAL1:def_3 .= { w where w is Point of (TOP-REAL 2) : ( w `1 = (G * (i1,i2)) `1 & (G * (i1,i2)) `2 <= w `2 & w `2 <= (G * (i1,j2)) `2 ) } by A206, A208, A177, A201, TOPREAL3:9 ; A210: dom g2 = Seg l by A178, FINSEQ_1:def_3; thus L~ g = L~ f ::_thesis: ( g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) proof set lg = { (LSeg (g,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } ; set lf = { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } ; A211: len g = (len g1) + (len g2) by FINSEQ_1:22; A212: now__::_thesis:_for_j_being_Element_of_NAT_st_len_g1_<=_j_&_j_<=_len_g_holds_ for_p_being_Point_of_(TOP-REAL_2)_st_p_=_g_/._j_holds_ (_p_`1_=_(G_*_(i1,i2))_`1_&_(G_*_(i1,i2))_`2_<=_p_`2_&_p_`2_<=_(G_*_(i1,j2))_`2_&_p_in_rng_l1_) let j be Element of NAT ; ::_thesis: ( len g1 <= j & j <= len g implies for p being Point of (TOP-REAL 2) st p = g /. j holds ( p `1 = (G * (i1,i2)) `1 & (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 & p in rng l1 ) ) assume that A213: len g1 <= j and A214: j <= len g ; ::_thesis: for p being Point of (TOP-REAL 2) st p = g /. j holds ( p `1 = (G * (i1,i2)) `1 & (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 & p in rng l1 ) reconsider w = j - (len g1) as Element of NAT by A213, INT_1:5; let p be Point of (TOP-REAL 2); ::_thesis: ( p = g /. j implies ( p `1 = (G * (i1,i2)) `1 & (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 & p in rng l1 ) ) assume A215: p = g /. j ; ::_thesis: ( p `1 = (G * (i1,i2)) `1 & (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 & p in rng l1 ) set u = i2 + w; A216: dom l1 = Seg (len l1) by FINSEQ_1:def_3; now__::_thesis:_(_p_`1_=_(G_*_(i1,i2))_`1_&_(G_*_(i1,i2))_`2_<=_p_`2_&_p_`2_<=_(G_*_(i1,j2))_`2_&_p_in_rng_l1_) percases ( j = len g1 or j <> len g1 ) ; supposeA217: j = len g1 ; ::_thesis: ( p `1 = (G * (i1,i2)) `1 & (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 & p in rng l1 ) 1 <= len g1 by A13, A23, A39, XXREAL_0:2; then len g1 in dom g1 by FINSEQ_3:25; then A218: g /. (len g1) = (f | k) /. (len (f | k)) by A38, FINSEQ_4:68 .= G * (i1,i2) by A17, A23, A14, A19, FINSEQ_4:71 ; hence p `1 = (G * (i1,i2)) `1 by A215, A217; ::_thesis: ( (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 & p in rng l1 ) thus ( (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 ) by A51, A56, A54, A20, A55, A176, A205, A203, A215, A217, A218, SEQM_3:def_1; ::_thesis: p in rng l1 thus p in rng l1 by A51, A55, A204, A215, A216, A217, A218, PARTFUN2:2; ::_thesis: verum end; supposeA219: j <> len g1 ; ::_thesis: ( p `1 = (G * (i1,i2)) `1 & (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 & p in rng l1 ) A220: w + (len g1) = j ; then A221: w <= len g2 by A211, A214, XREAL_1:6; A222: (X_axis l1) . i2 = (G * (i1,i2)) `1 by A51, A42, A55, A204, GOBOARD1:def_1; A223: j - (len g1) <> 0 by A219; then A224: w >= 1 by NAT_1:14; then A225: g /. j = g2 /. w by A220, A221, SEQ_4:136; A226: i2 < i2 + w by A223, XREAL_1:29; A227: w in dom g2 by A224, A221, FINSEQ_3:25; then A228: i2 + w in Seg (width G) by A210, A179; i2 + w in Seg (width G) by A210, A179, A227; then i2 + w in dom l1 by A55, FINSEQ_1:def_3; then l1 /. (i2 + w) = l1 . (i2 + w) by PARTFUN1:def_6; then A229: l1 /. (i2 + w) = G * (i1,(i2 + w)) by A228, MATRIX_1:def_7; then A230: (Y_axis l1) . (i2 + w) = (G * (i1,(i2 + w))) `2 by A20, A55, A228, GOBOARD1:def_2; A231: g2 /. w = G * (i1,(i2 + w)) by A178, A227; (X_axis l1) . (i2 + w) = (G * (i1,(i2 + w))) `1 by A42, A55, A228, A229, GOBOARD1:def_1; hence p `1 = (G * (i1,i2)) `1 by A51, A50, A42, A55, A215, A225, A231, A228, A222, SEQM_3:def_10; ::_thesis: ( (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 & p in rng l1 ) (Y_axis l1) . i2 = (G * (i1,i2)) `2 by A51, A20, A55, A204, GOBOARD1:def_2; hence (G * (i1,i2)) `2 <= p `2 by A51, A54, A20, A55, A215, A225, A231, A228, A230, A226, SEQM_3:def_1; ::_thesis: ( p `2 <= (G * (i1,j2)) `2 & p in rng l1 ) A232: (Y_axis l1) . j2 = (G * (i1,j2)) `2 by A56, A20, A55, A202, GOBOARD1:def_2; now__::_thesis:_p_`2_<=_(G_*_(i1,j2))_`2 percases ( i2 + w = j2 or i2 + w <> j2 ) ; suppose i2 + w = j2 ; ::_thesis: p `2 <= (G * (i1,j2)) `2 hence p `2 <= (G * (i1,j2)) `2 by A215, A224, A220, A221, A231, SEQ_4:136; ::_thesis: verum end; supposeA233: i2 + w <> j2 ; ::_thesis: p `2 <= (G * (i1,j2)) `2 i2 + w <= i2 + l by A178, A221, XREAL_1:7; then i2 + w < j2 by A233, XXREAL_0:1; hence p `2 <= (G * (i1,j2)) `2 by A56, A54, A20, A55, A215, A225, A231, A228, A230, A232, SEQM_3:def_1; ::_thesis: verum end; end; end; hence p `2 <= (G * (i1,j2)) `2 ; ::_thesis: p in rng l1 thus p in rng l1 by A55, A215, A216, A225, A231, A228, A229, PARTFUN2:2; ::_thesis: verum end; end; end; hence ( p `1 = (G * (i1,i2)) `1 & (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 & p in rng l1 ) ; ::_thesis: verum end; thus L~ g c= L~ f :: according to XBOOLE_0:def_10 ::_thesis: L~ f c= L~ g proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in L~ g or x in L~ f ) assume x in L~ g ; ::_thesis: x in L~ f then consider X being set such that A234: x in X and A235: X in { (LSeg (g,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } by TARSKI:def_4; consider i being Element of NAT such that A236: X = LSeg (g,i) and A237: 1 <= i and A238: i + 1 <= len g by A235; now__::_thesis:_x_in_L~_f percases ( i + 1 <= len g1 or i + 1 > len g1 ) ; supposeA239: i + 1 <= len g1 ; ::_thesis: x in L~ f i <= i + 1 by NAT_1:11; then i <= len g1 by A239, XXREAL_0:2; then A240: i in dom g1 by A237, FINSEQ_3:25; 1 <= i + 1 by NAT_1:11; then i + 1 in dom g1 by A239, FINSEQ_3:25; then X = LSeg (g1,i) by A236, A240, TOPREAL3:18; then X in { (LSeg (g1,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g1 ) } by A237, A239; then A241: x in L~ (f | k) by A36, A234, TARSKI:def_4; L~ (f | k) c= L~ f by TOPREAL3:20; hence x in L~ f by A241; ::_thesis: verum end; supposeA242: i + 1 > len g1 ; ::_thesis: x in L~ f reconsider q1 = g /. i, q2 = g /. (i + 1) as Point of (TOP-REAL 2) ; A243: i <= len g by A238, NAT_1:13; A244: len g1 <= i by A242, NAT_1:13; then A245: q1 `1 = (G * (i1,i2)) `1 by A212, A243; A246: q1 `2 <= (G * (i1,j2)) `2 by A212, A244, A243; A247: (G * (i1,i2)) `2 <= q1 `2 by A212, A244, A243; q2 `1 = (G * (i1,i2)) `1 by A212, A238, A242; then A248: q2 = |[(q1 `1),(q2 `2)]| by A245, EUCLID:53; A249: q2 `2 <= (G * (i1,j2)) `2 by A212, A238, A242; A250: ( q1 = |[(q1 `1),(q1 `2)]| & LSeg (g,i) = LSeg (q2,q1) ) by A237, A238, EUCLID:53, TOPREAL1:def_3; A251: (G * (i1,i2)) `2 <= q2 `2 by A212, A238, A242; now__::_thesis:_x_in_L~_f percases ( q1 `2 > q2 `2 or q1 `2 = q2 `2 or q1 `2 < q2 `2 ) by XXREAL_0:1; suppose q1 `2 > q2 `2 ; ::_thesis: x in L~ f then LSeg (g,i) = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = q1 `1 & q2 `2 <= p2 `2 & p2 `2 <= q1 `2 ) } by A248, A250, TOPREAL3:9; then consider p2 being Point of (TOP-REAL 2) such that A252: ( p2 = x & p2 `1 = q1 `1 ) and A253: ( q2 `2 <= p2 `2 & p2 `2 <= q1 `2 ) by A234, A236; ( (G * (i1,i2)) `2 <= p2 `2 & p2 `2 <= (G * (i1,j2)) `2 ) by A246, A251, A253, XXREAL_0:2; then A254: x in LSeg (f,k) by A209, A245, A252; LSeg (f,k) in { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } by A3, A13; hence x in L~ f by A254, TARSKI:def_4; ::_thesis: verum end; suppose q1 `2 = q2 `2 ; ::_thesis: x in L~ f then LSeg (g,i) = {q1} by A248, A250, RLTOPSP1:70; then x = q1 by A234, A236, TARSKI:def_1; then A255: x in LSeg (f,k) by A209, A245, A247, A246; LSeg (f,k) in { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } by A3, A13; hence x in L~ f by A255, TARSKI:def_4; ::_thesis: verum end; suppose q1 `2 < q2 `2 ; ::_thesis: x in L~ f then LSeg (g,i) = { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `1 = q1 `1 & q1 `2 <= p1 `2 & p1 `2 <= q2 `2 ) } by A248, A250, TOPREAL3:9; then consider p2 being Point of (TOP-REAL 2) such that A256: ( p2 = x & p2 `1 = q1 `1 ) and A257: ( q1 `2 <= p2 `2 & p2 `2 <= q2 `2 ) by A234, A236; ( (G * (i1,i2)) `2 <= p2 `2 & p2 `2 <= (G * (i1,j2)) `2 ) by A247, A249, A257, XXREAL_0:2; then A258: x in LSeg (f,k) by A209, A245, A256; LSeg (f,k) in { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } by A3, A13; hence x in L~ f by A258, TARSKI:def_4; ::_thesis: verum end; end; end; hence x in L~ f ; ::_thesis: verum end; end; end; hence x in L~ f ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in L~ f or x in L~ g ) assume x in L~ f ; ::_thesis: x in L~ g then A259: x in (L~ (f | k)) \/ (LSeg (f,k)) by A3, A12, Th3; now__::_thesis:_x_in_L~_g percases ( x in L~ (f | k) or x in LSeg (f,k) ) by A259, XBOOLE_0:def_3; supposeA260: x in L~ (f | k) ; ::_thesis: x in L~ g L~ g1 c= L~ g by Th6; hence x in L~ g by A36, A260; ::_thesis: verum end; suppose x in LSeg (f,k) ; ::_thesis: x in L~ g then consider p1 being Point of (TOP-REAL 2) such that A261: p1 = x and A262: p1 `1 = (G * (i1,i2)) `1 and A263: (G * (i1,i2)) `2 <= p1 `2 and A264: p1 `2 <= (G * (i1,j2)) `2 by A209; defpred S2[ Nat] means ( len g1 <= $1 & $1 <= len g & ( for q being Point of (TOP-REAL 2) st q = g /. $1 holds q `2 <= p1 `2 ) ); A265: now__::_thesis:_ex_n_being_Nat_st_S2[n] reconsider n = len g1 as Nat ; take n = n; ::_thesis: S2[n] thus S2[n] ::_thesis: verum proof thus ( len g1 <= n & n <= len g ) by A211, XREAL_1:31; ::_thesis: for q being Point of (TOP-REAL 2) st q = g /. n holds q `2 <= p1 `2 1 <= len g1 by A13, A23, A39, XXREAL_0:2; then A266: len g1 in dom g1 by FINSEQ_3:25; let q be Point of (TOP-REAL 2); ::_thesis: ( q = g /. n implies q `2 <= p1 `2 ) assume q = g /. n ; ::_thesis: q `2 <= p1 `2 then q = (f | k) /. (len (f | k)) by A38, A266, FINSEQ_4:68 .= G * (i1,i2) by A17, A23, A14, A19, FINSEQ_4:71 ; hence q `2 <= p1 `2 by A263; ::_thesis: verum end; end; A267: for n being Nat st S2[n] holds n <= len g ; consider ma being Nat such that A268: ( S2[ma] & ( for n being Nat st S2[n] holds n <= ma ) ) from NAT_1:sch_6(A267, A265); reconsider ma = ma as Element of NAT by ORDINAL1:def_12; now__::_thesis:_x_in_L~_g percases ( ma = len g or ma <> len g ) ; supposeA269: ma = len g ; ::_thesis: x in L~ g i2 + 1 <= j2 by A176, NAT_1:13; then A270: 1 <= l by XREAL_1:19; then 0 + 1 <= ma by A178, A211, A269, XREAL_1:7; then reconsider m1 = ma - 1 as Element of NAT by INT_1:5; A271: m1 + 1 = ma ; (len g1) + 1 <= ma by A178, A211, A269, A270, XREAL_1:7; then A272: m1 >= len g1 by A271, XREAL_1:6; reconsider q = g /. m1 as Point of (TOP-REAL 2) ; set lq = { e where e is Point of (TOP-REAL 2) : ( e `1 = (G * (i1,i2)) `1 & q `2 <= e `2 & e `2 <= (G * (i1,j2)) `2 ) } ; A273: i2 + l = j2 ; A274: l in dom g2 by A178, A270, FINSEQ_3:25; then A275: g /. ma = g2 /. l by A178, A211, A269, FINSEQ_4:69 .= G * (i1,j2) by A178, A274, A273 ; then (G * (i1,j2)) `2 <= p1 `2 by A268; then A276: p1 `2 = (G * (i1,j2)) `2 by A264, XXREAL_0:1; A277: m1 <= len g by A269, A271, NAT_1:11; then A278: q `1 = (G * (i1,i2)) `1 by A212, A272; A279: q `2 <= (G * (i1,j2)) `2 by A212, A272, A277; 1 <= len g1 by A13, A23, A39, XXREAL_0:2; then A280: 1 <= m1 by A272, XXREAL_0:2; then ( q = |[(q `1),(q `2)]| & LSeg (g,m1) = LSeg ((G * (i1,j2)),q) ) by A269, A275, A271, EUCLID:53, TOPREAL1:def_3; then LSeg (g,m1) = { e where e is Point of (TOP-REAL 2) : ( e `1 = (G * (i1,i2)) `1 & q `2 <= e `2 & e `2 <= (G * (i1,j2)) `2 ) } by A208, A201, A278, A279, TOPREAL3:9; then A281: p1 in LSeg (g,m1) by A262, A276, A279; LSeg (g,m1) in { (LSeg (g,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } by A269, A271, A280; hence x in L~ g by A261, A281, TARSKI:def_4; ::_thesis: verum end; suppose ma <> len g ; ::_thesis: x in L~ g then ma < len g by A268, XXREAL_0:1; then A282: ma + 1 <= len g by NAT_1:13; reconsider qa = g /. ma, qa1 = g /. (ma + 1) as Point of (TOP-REAL 2) ; set lma = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = (G * (i1,i2)) `1 & qa `2 <= p2 `2 & p2 `2 <= qa1 `2 ) } ; A283: qa1 = |[(qa1 `1),(qa1 `2)]| by EUCLID:53; A284: qa `2 <= p1 `2 by A268; A285: len g1 <= ma + 1 by A268, NAT_1:13; then A286: qa1 `1 = (G * (i1,i2)) `1 by A212, A282; A287: now__::_thesis:_not_qa1_`2_<=_p1_`2 assume qa1 `2 <= p1 `2 ; ::_thesis: contradiction then for q being Point of (TOP-REAL 2) st q = g /. (ma + 1) holds q `2 <= p1 `2 ; then ma + 1 <= ma by A268, A282, A285; hence contradiction by XREAL_1:29; ::_thesis: verum end; A288: ( qa `1 = (G * (i1,i2)) `1 & qa = |[(qa `1),(qa `2)]| ) by A212, A268, EUCLID:53; A289: 1 <= ma by A13, A23, A39, A268, NAT_1:13; then LSeg (g,ma) = LSeg (qa,qa1) by A282, TOPREAL1:def_3 .= { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = (G * (i1,i2)) `1 & qa `2 <= p2 `2 & p2 `2 <= qa1 `2 ) } by A284, A287, A286, A288, A283, TOPREAL3:9, XXREAL_0:2 ; then A290: x in LSeg (g,ma) by A261, A262, A284, A287; LSeg (g,ma) in { (LSeg (g,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } by A289, A282; hence x in L~ g by A290, TARSKI:def_4; ::_thesis: verum end; end; end; hence x in L~ g ; ::_thesis: verum end; end; end; hence x in L~ g ; ::_thesis: verum end; 1 <= len g1 by A13, A23, A39, XXREAL_0:2; then 1 in dom g1 by FINSEQ_3:25; hence g /. 1 = (f | k) /. 1 by A37, FINSEQ_4:68 .= f /. 1 by A17, A15, FINSEQ_4:71 ; ::_thesis: ( g /. (len g) = f /. (len f) & len f <= len g ) A291: len g = (len g1) + l by A178, FINSEQ_1:22; i2 + 1 <= j2 by A176, NAT_1:13; then A292: 1 <= l by XREAL_1:19; then A293: l in dom g2 by A178, A184, FINSEQ_1:1; hence g /. (len g) = g2 /. l by A291, FINSEQ_4:69 .= G * (i1,(i2 + l)) by A178, A293 .= f /. (len f) by A3, A46, A58 ; ::_thesis: len f <= len g thus len f <= len g by A3, A23, A39, A292, A291, XREAL_1:7; ::_thesis: verum end; end; end; hence ex g being FinSequence of (TOP-REAL 2) st ( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) ; ::_thesis: verum end; supposeA294: i2 = j2 ; ::_thesis: ex g being FinSequence of (TOP-REAL 2) st ( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) set ppi = G * (i1,i2); set pj = G * (j1,i2); now__::_thesis:_(_(_i1_>_j1_&_ex_g_being_FinSequence_of_the_carrier_of_(TOP-REAL_2)_st_ (_g_is_sequence_on_G_&_L~_g_=_L~_f_&_g_/._1_=_f_/._1_&_g_/._(len_g)_=_f_/._(len_f)_&_len_f_<=_len_g_)_)_or_(_i1_=_j1_&_contradiction_)_or_(_i1_<_j1_&_ex_g_being_FinSequence_of_the_carrier_of_(TOP-REAL_2)_st_ (_g_is_sequence_on_G_&_L~_g_=_L~_f_&_g_/._1_=_f_/._1_&_g_/._(len_g)_=_f_/._(len_f)_&_len_f_<=_len_g_)_)_) percases ( i1 > j1 or i1 = j1 or i1 < j1 ) by XXREAL_0:1; caseA295: i1 > j1 ; ::_thesis: ex g being FinSequence of the carrier of (TOP-REAL 2) st ( g is_sequence_on G & L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) c1 /. j1 = c1 . j1 by A48, A43, PARTFUN1:def_6; then A296: c1 /. j1 = G * (j1,i2) by A48, MATRIX_1:def_8; then A297: (X_axis c1) . j1 = (G * (j1,i2)) `1 by A48, A43, A22, GOBOARD1:def_1; c1 /. i1 = c1 . i1 by A49, A43, PARTFUN1:def_6; then A298: c1 /. i1 = G * (i1,i2) by A49, MATRIX_1:def_8; then A299: (X_axis c1) . i1 = (G * (i1,i2)) `1 by A49, A43, A22, GOBOARD1:def_1; then A300: (G * (j1,i2)) `1 < (G * (i1,i2)) `1 by A49, A48, A52, A43, A22, A295, A297, SEQM_3:def_1; A301: (Y_axis c1) . j1 = (G * (j1,i2)) `2 by A48, A43, A21, A296, GOBOARD1:def_2; (Y_axis c1) . i1 = (G * (i1,i2)) `2 by A49, A43, A21, A298, GOBOARD1:def_2; then A302: (G * (i1,i2)) `2 = (G * (j1,i2)) `2 by A49, A48, A53, A43, A21, A301, SEQM_3:def_10; reconsider l = i1 - j1 as Element of NAT by A295, INT_1:5; defpred S2[ Nat, set ] means for m being Element of NAT st m = i1 - $1 holds $2 = G * (m,i2); set lk = { w where w is Point of (TOP-REAL 2) : ( w `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= w `1 & w `1 <= (G * (i1,i2)) `1 ) } ; A303: G * (i1,i2) = |[((G * (i1,i2)) `1),((G * (i1,i2)) `2)]| by EUCLID:53; A304: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_Seg_l_holds_ (_i1_-_n_is_Element_of_NAT_&_[(i1_-_n),i2]_in_Indices_G_&_i1_-_n_in_dom_G_) let n be Element of NAT ; ::_thesis: ( n in Seg l implies ( i1 - n is Element of NAT & [(i1 - n),i2] in Indices G & i1 - n in dom G ) ) assume n in Seg l ; ::_thesis: ( i1 - n is Element of NAT & [(i1 - n),i2] in Indices G & i1 - n in dom G ) then A305: n <= l by FINSEQ_1:1; l <= i1 by XREAL_1:43; then reconsider w = i1 - n as Element of NAT by A305, INT_1:5, XXREAL_0:2; ( i1 - n <= i1 & i1 <= len G ) by A49, FINSEQ_3:25, XREAL_1:43; then A306: w <= len G by XXREAL_0:2; A307: 1 <= j1 by A48, FINSEQ_3:25; i1 - l <= i1 - n by A305, XREAL_1:13; then 1 <= w by A307, XXREAL_0:2; then w in dom G by A306, FINSEQ_3:25; hence ( i1 - n is Element of NAT & [(i1 - n),i2] in Indices G & i1 - n in dom G ) by A47, A51, ZFMISC_1:87; ::_thesis: verum end; A308: now__::_thesis:_for_n_being_Nat_st_n_in_Seg_l_holds_ ex_p_being_Element_of_the_carrier_of_(TOP-REAL_2)_st_S2[n,p] let n be Nat; ::_thesis: ( n in Seg l implies ex p being Element of the carrier of (TOP-REAL 2) st S2[n,p] ) assume n in Seg l ; ::_thesis: ex p being Element of the carrier of (TOP-REAL 2) st S2[n,p] then reconsider m = i1 - n as Element of NAT by A304; take p = G * (m,i2); ::_thesis: S2[n,p] thus S2[n,p] ; ::_thesis: verum end; consider g2 being FinSequence of (TOP-REAL 2) such that A309: ( len g2 = l & ( for n being Nat st n in Seg l holds S2[n,g2 /. n] ) ) from FINSEQ_4:sch_1(A308); take g = g1 ^ g2; ::_thesis: ( g is_sequence_on G & L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) A310: dom g2 = Seg l by A309, FINSEQ_1:def_3; A311: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_g2_&_n_+_1_in_dom_g2_holds_ for_l1,_l2,_l3,_l4_being_Element_of_NAT_st_[l1,l2]_in_Indices_G_&_[l3,l4]_in_Indices_G_&_g2_/._n_=_G_*_(l1,l2)_&_g2_/._(n_+_1)_=_G_*_(l3,l4)_holds_ (abs_(l1_-_l3))_+_(abs_(l2_-_l4))_=_1 let n be Element of NAT ; ::_thesis: ( n in dom g2 & n + 1 in dom g2 implies for l1, l2, l3, l4 being Element of NAT st [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) holds (abs (l1 - l3)) + (abs (l2 - l4)) = 1 ) assume that A312: n in dom g2 and A313: n + 1 in dom g2 ; ::_thesis: for l1, l2, l3, l4 being Element of NAT st [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) holds (abs (l1 - l3)) + (abs (l2 - l4)) = 1 reconsider m1 = i1 - n, m2 = i1 - (n + 1) as Element of NAT by A304, A310, A312, A313; let l1, l2, l3, l4 be Element of NAT ; ::_thesis: ( [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) implies (abs (l1 - l3)) + (abs (l2 - l4)) = 1 ) assume that A314: [l1,l2] in Indices G and A315: [l3,l4] in Indices G and A316: g2 /. n = G * (l1,l2) and A317: g2 /. (n + 1) = G * (l3,l4) ; ::_thesis: (abs (l1 - l3)) + (abs (l2 - l4)) = 1 ( [(i1 - (n + 1)),i2] in Indices G & g2 /. (n + 1) = G * (m2,i2) ) by A304, A309, A310, A313; then A318: ( l3 = m2 & l4 = i2 ) by A315, A317, GOBOARD1:5; ( [(i1 - n),i2] in Indices G & g2 /. n = G * (m1,i2) ) by A304, A309, A310, A312; then ( l1 = m1 & l2 = i2 ) by A314, A316, GOBOARD1:5; hence (abs (l1 - l3)) + (abs (l2 - l4)) = (abs ((i1 - n) - (i1 - (n + 1)))) + 0 by A318, ABSVALUE:2 .= 1 by ABSVALUE:def_1 ; ::_thesis: verum end; now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_g2_holds_ ex_m,_k_being_Element_of_NAT_st_ (_[m,k]_in_Indices_G_&_g2_/._n_=_G_*_(m,k)_) let n be Element of NAT ; ::_thesis: ( n in dom g2 implies ex m, k being Element of NAT st ( [m,k] in Indices G & g2 /. n = G * (m,k) ) ) assume A319: n in dom g2 ; ::_thesis: ex m, k being Element of NAT st ( [m,k] in Indices G & g2 /. n = G * (m,k) ) then reconsider m = i1 - n as Element of NAT by A304, A310; take m = m; ::_thesis: ex k being Element of NAT st ( [m,k] in Indices G & g2 /. n = G * (m,k) ) take k = i2; ::_thesis: ( [m,k] in Indices G & g2 /. n = G * (m,k) ) thus ( [m,k] in Indices G & g2 /. n = G * (m,k) ) by A304, A309, A310, A319; ::_thesis: verum end; then A320: for n being Element of NAT st n in dom g holds ex i, j being Element of NAT st ( [i,j] in Indices G & g /. n = G * (i,j) ) by A40, GOBOARD1:23; now__::_thesis:_for_l1,_l2,_l3,_l4_being_Element_of_NAT_st_[l1,l2]_in_Indices_G_&_[l3,l4]_in_Indices_G_&_g1_/._(len_g1)_=_G_*_(l1,l2)_&_g2_/._1_=_G_*_(l3,l4)_&_len_g1_in_dom_g1_&_1_in_dom_g2_holds_ (abs_(l1_-_l3))_+_(abs_(l2_-_l4))_=_1 let l1, l2, l3, l4 be Element of NAT ; ::_thesis: ( [l1,l2] in Indices G & [l3,l4] in Indices G & g1 /. (len g1) = G * (l1,l2) & g2 /. 1 = G * (l3,l4) & len g1 in dom g1 & 1 in dom g2 implies (abs (l1 - l3)) + (abs (l2 - l4)) = 1 ) assume that A321: [l1,l2] in Indices G and A322: [l3,l4] in Indices G and A323: g1 /. (len g1) = G * (l1,l2) and A324: g2 /. 1 = G * (l3,l4) and len g1 in dom g1 and A325: 1 in dom g2 ; ::_thesis: (abs (l1 - l3)) + (abs (l2 - l4)) = 1 reconsider m1 = i1 - 1 as Element of NAT by A304, A310, A325; ( [(i1 - 1),i2] in Indices G & g2 /. 1 = G * (m1,i2) ) by A304, A309, A310, A325; then A326: ( l3 = m1 & l4 = i2 ) by A322, A324, GOBOARD1:5; (f | k) /. (len (f | k)) = f /. k by A17, A23, A14, FINSEQ_4:71; then ( l1 = i1 & l2 = i2 ) by A38, A18, A19, A321, A323, GOBOARD1:5; hence (abs (l1 - l3)) + (abs (l2 - l4)) = (abs (i1 - (i1 - 1))) + 0 by A326, ABSVALUE:2 .= 1 by ABSVALUE:def_1 ; ::_thesis: verum end; then for n being Element of NAT st n in dom g & n + 1 in dom g holds for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & g /. n = G * (m,k) & g /. (n + 1) = G * (i,j) holds (abs (m - i)) + (abs (k - j)) = 1 by A41, A311, GOBOARD1:24; hence g is_sequence_on G by A320, GOBOARD1:def_9; ::_thesis: ( L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) reconsider m1 = i1 - l as Element of NAT ; A327: G * (j1,i2) = |[((G * (j1,i2)) `1),((G * (j1,i2)) `2)]| by EUCLID:53; A328: LSeg (f,k) = LSeg ((G * (j1,i2)),(G * (i1,i2))) by A3, A13, A19, A46, A294, TOPREAL1:def_3 .= { w where w is Point of (TOP-REAL 2) : ( w `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= w `1 & w `1 <= (G * (i1,i2)) `1 ) } by A300, A302, A303, A327, TOPREAL3:10 ; thus L~ g = L~ f ::_thesis: ( g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) proof set lg = { (LSeg (g,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } ; set lf = { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } ; A329: len g = (len g1) + (len g2) by FINSEQ_1:22; A330: now__::_thesis:_for_j_being_Element_of_NAT_st_len_g1_<=_j_&_j_<=_len_g_holds_ for_p_being_Point_of_(TOP-REAL_2)_st_p_=_g_/._j_holds_ (_p_`2_=_(G_*_(i1,i2))_`2_&_(G_*_(j1,i2))_`1_<=_p_`1_&_p_`1_<=_(G_*_(i1,i2))_`1_&_p_in_rng_c1_) let j be Element of NAT ; ::_thesis: ( len g1 <= j & j <= len g implies for p being Point of (TOP-REAL 2) st p = g /. j holds ( p `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 & p in rng c1 ) ) assume that A331: len g1 <= j and A332: j <= len g ; ::_thesis: for p being Point of (TOP-REAL 2) st p = g /. j holds ( p `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 & p in rng c1 ) reconsider w = j - (len g1) as Element of NAT by A331, INT_1:5; let p be Point of (TOP-REAL 2); ::_thesis: ( p = g /. j implies ( p `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 & p in rng c1 ) ) assume A333: p = g /. j ; ::_thesis: ( p `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 & p in rng c1 ) now__::_thesis:_(_p_`2_=_(G_*_(i1,i2))_`2_&_(G_*_(j1,i2))_`1_<=_p_`1_&_p_`1_<=_(G_*_(i1,i2))_`1_&_p_in_rng_c1_) percases ( j = len g1 or j <> len g1 ) ; supposeA334: j = len g1 ; ::_thesis: ( p `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 & p in rng c1 ) 1 <= len g1 by A13, A23, A39, XXREAL_0:2; then len g1 in dom g1 by FINSEQ_3:25; then A335: g /. (len g1) = (f | k) /. (len (f | k)) by A38, FINSEQ_4:68 .= G * (i1,i2) by A17, A23, A14, A19, FINSEQ_4:71 ; hence p `2 = (G * (i1,i2)) `2 by A333, A334; ::_thesis: ( (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 & p in rng c1 ) thus ( (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 ) by A49, A48, A52, A43, A22, A295, A299, A297, A333, A334, A335, SEQM_3:def_1; ::_thesis: p in rng c1 thus p in rng c1 by A49, A43, A298, A333, A334, A335, PARTFUN2:2; ::_thesis: verum end; supposeA336: j <> len g1 ; ::_thesis: ( p `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 & p in rng c1 ) A337: w + (len g1) = j ; then A338: w <= len g2 by A329, A332, XREAL_1:6; A339: j - (len g1) <> 0 by A336; then A340: w >= 1 by NAT_1:14; then A341: w in dom g2 by A338, FINSEQ_3:25; then reconsider u = i1 - w as Element of NAT by A304, A310; A342: g /. j = g2 /. w by A340, A337, A338, SEQ_4:136; A343: u < i1 by A339, XREAL_1:44; A344: g2 /. w = G * (u,i2) by A309, A310, A341; A345: (Y_axis c1) . i1 = (G * (i1,i2)) `2 by A49, A43, A21, A298, GOBOARD1:def_2; A346: i1 - w in dom G by A304, A310, A341; c1 /. u = c1 . u by A43, A304, A310, A341, PARTFUN1:def_6; then A347: c1 /. u = G * (u,i2) by A346, MATRIX_1:def_8; then A348: (X_axis c1) . u = (G * (u,i2)) `1 by A43, A22, A346, GOBOARD1:def_1; (Y_axis c1) . u = (G * (u,i2)) `2 by A43, A21, A346, A347, GOBOARD1:def_2; hence p `2 = (G * (i1,i2)) `2 by A49, A53, A43, A21, A333, A342, A346, A344, A345, SEQM_3:def_10; ::_thesis: ( (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 & p in rng c1 ) A349: (X_axis c1) . j1 = (G * (j1,i2)) `1 by A48, A43, A22, A296, GOBOARD1:def_1; now__::_thesis:_(G_*_(j1,i2))_`1_<=_p_`1 percases ( u = j1 or u <> j1 ) ; suppose u = j1 ; ::_thesis: (G * (j1,i2)) `1 <= p `1 hence (G * (j1,i2)) `1 <= p `1 by A333, A340, A337, A338, A344, SEQ_4:136; ::_thesis: verum end; supposeA350: u <> j1 ; ::_thesis: (G * (j1,i2)) `1 <= p `1 i1 - (len g2) <= u by A338, XREAL_1:13; then j1 < u by A309, A350, XXREAL_0:1; hence (G * (j1,i2)) `1 <= p `1 by A48, A52, A43, A22, A333, A342, A346, A344, A348, A349, SEQM_3:def_1; ::_thesis: verum end; end; end; hence (G * (j1,i2)) `1 <= p `1 ; ::_thesis: ( p `1 <= (G * (i1,i2)) `1 & p in rng c1 ) (X_axis c1) . i1 = (G * (i1,i2)) `1 by A49, A43, A22, A298, GOBOARD1:def_1; hence p `1 <= (G * (i1,i2)) `1 by A49, A52, A43, A22, A333, A342, A346, A344, A348, A343, SEQM_3:def_1; ::_thesis: p in rng c1 thus p in rng c1 by A43, A333, A342, A346, A344, A347, PARTFUN2:2; ::_thesis: verum end; end; end; hence ( p `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 & p in rng c1 ) ; ::_thesis: verum end; thus L~ g c= L~ f :: according to XBOOLE_0:def_10 ::_thesis: L~ f c= L~ g proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in L~ g or x in L~ f ) assume x in L~ g ; ::_thesis: x in L~ f then consider X being set such that A351: x in X and A352: X in { (LSeg (g,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } by TARSKI:def_4; consider i being Element of NAT such that A353: X = LSeg (g,i) and A354: 1 <= i and A355: i + 1 <= len g by A352; now__::_thesis:_x_in_L~_f percases ( i + 1 <= len g1 or i + 1 > len g1 ) ; supposeA356: i + 1 <= len g1 ; ::_thesis: x in L~ f i <= i + 1 by NAT_1:11; then i <= len g1 by A356, XXREAL_0:2; then A357: i in dom g1 by A354, FINSEQ_3:25; 1 <= i + 1 by NAT_1:11; then i + 1 in dom g1 by A356, FINSEQ_3:25; then X = LSeg (g1,i) by A353, A357, TOPREAL3:18; then X in { (LSeg (g1,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g1 ) } by A354, A356; then A358: x in L~ (f | k) by A36, A351, TARSKI:def_4; L~ (f | k) c= L~ f by TOPREAL3:20; hence x in L~ f by A358; ::_thesis: verum end; supposeA359: i + 1 > len g1 ; ::_thesis: x in L~ f reconsider q1 = g /. i, q2 = g /. (i + 1) as Point of (TOP-REAL 2) ; A360: i <= len g by A355, NAT_1:13; A361: len g1 <= i by A359, NAT_1:13; then A362: q1 `2 = (G * (i1,i2)) `2 by A330, A360; A363: q1 `1 <= (G * (i1,i2)) `1 by A330, A361, A360; A364: (G * (j1,i2)) `1 <= q1 `1 by A330, A361, A360; q2 `2 = (G * (i1,i2)) `2 by A330, A355, A359; then A365: q2 = |[(q2 `1),(q1 `2)]| by A362, EUCLID:53; A366: q2 `1 <= (G * (i1,i2)) `1 by A330, A355, A359; A367: ( q1 = |[(q1 `1),(q1 `2)]| & LSeg (g,i) = LSeg (q2,q1) ) by A354, A355, EUCLID:53, TOPREAL1:def_3; A368: (G * (j1,i2)) `1 <= q2 `1 by A330, A355, A359; now__::_thesis:_x_in_L~_f percases ( q1 `1 > q2 `1 or q1 `1 = q2 `1 or q1 `1 < q2 `1 ) by XXREAL_0:1; suppose q1 `1 > q2 `1 ; ::_thesis: x in L~ f then LSeg (g,i) = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `2 = q1 `2 & q2 `1 <= p2 `1 & p2 `1 <= q1 `1 ) } by A365, A367, TOPREAL3:10; then consider p2 being Point of (TOP-REAL 2) such that A369: ( p2 = x & p2 `2 = q1 `2 ) and A370: ( q2 `1 <= p2 `1 & p2 `1 <= q1 `1 ) by A351, A353; ( (G * (j1,i2)) `1 <= p2 `1 & p2 `1 <= (G * (i1,i2)) `1 ) by A363, A368, A370, XXREAL_0:2; then A371: x in LSeg (f,k) by A328, A362, A369; LSeg (f,k) in { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } by A3, A13; hence x in L~ f by A371, TARSKI:def_4; ::_thesis: verum end; suppose q1 `1 = q2 `1 ; ::_thesis: x in L~ f then LSeg (g,i) = {q1} by A365, A367, RLTOPSP1:70; then x = q1 by A351, A353, TARSKI:def_1; then A372: x in LSeg (f,k) by A328, A362, A364, A363; LSeg (f,k) in { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } by A3, A13; hence x in L~ f by A372, TARSKI:def_4; ::_thesis: verum end; suppose q1 `1 < q2 `1 ; ::_thesis: x in L~ f then LSeg (g,i) = { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `2 = q1 `2 & q1 `1 <= p1 `1 & p1 `1 <= q2 `1 ) } by A365, A367, TOPREAL3:10; then consider p2 being Point of (TOP-REAL 2) such that A373: ( p2 = x & p2 `2 = q1 `2 ) and A374: ( q1 `1 <= p2 `1 & p2 `1 <= q2 `1 ) by A351, A353; ( (G * (j1,i2)) `1 <= p2 `1 & p2 `1 <= (G * (i1,i2)) `1 ) by A364, A366, A374, XXREAL_0:2; then A375: x in LSeg (f,k) by A328, A362, A373; LSeg (f,k) in { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } by A3, A13; hence x in L~ f by A375, TARSKI:def_4; ::_thesis: verum end; end; end; hence x in L~ f ; ::_thesis: verum end; end; end; hence x in L~ f ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in L~ f or x in L~ g ) assume x in L~ f ; ::_thesis: x in L~ g then A376: x in (L~ (f | k)) \/ (LSeg (f,k)) by A3, A12, Th3; now__::_thesis:_x_in_L~_g percases ( x in L~ (f | k) or x in LSeg (f,k) ) by A376, XBOOLE_0:def_3; supposeA377: x in L~ (f | k) ; ::_thesis: x in L~ g L~ g1 c= L~ g by Th6; hence x in L~ g by A36, A377; ::_thesis: verum end; suppose x in LSeg (f,k) ; ::_thesis: x in L~ g then consider p1 being Point of (TOP-REAL 2) such that A378: p1 = x and A379: p1 `2 = (G * (i1,i2)) `2 and A380: (G * (j1,i2)) `1 <= p1 `1 and A381: p1 `1 <= (G * (i1,i2)) `1 by A328; defpred S3[ Nat] means ( len g1 <= $1 & $1 <= len g & ( for q being Point of (TOP-REAL 2) st q = g /. $1 holds q `1 >= p1 `1 ) ); A382: now__::_thesis:_ex_n_being_Nat_st_S3[n] reconsider n = len g1 as Nat ; take n = n; ::_thesis: S3[n] thus S3[n] ::_thesis: verum proof thus ( len g1 <= n & n <= len g ) by A329, XREAL_1:31; ::_thesis: for q being Point of (TOP-REAL 2) st q = g /. n holds q `1 >= p1 `1 1 <= len g1 by A13, A23, A39, XXREAL_0:2; then A383: len g1 in dom g1 by FINSEQ_3:25; let q be Point of (TOP-REAL 2); ::_thesis: ( q = g /. n implies q `1 >= p1 `1 ) assume q = g /. n ; ::_thesis: q `1 >= p1 `1 then q = (f | k) /. (len (f | k)) by A38, A383, FINSEQ_4:68 .= G * (i1,i2) by A17, A23, A14, A19, FINSEQ_4:71 ; hence q `1 >= p1 `1 by A381; ::_thesis: verum end; end; A384: for n being Nat st S3[n] holds n <= len g ; consider ma being Nat such that A385: ( S3[ma] & ( for n being Nat st S3[n] holds n <= ma ) ) from NAT_1:sch_6(A384, A382); reconsider ma = ma as Element of NAT by ORDINAL1:def_12; now__::_thesis:_x_in_L~_g percases ( ma = len g or ma <> len g ) ; supposeA386: ma = len g ; ::_thesis: x in L~ g j1 + 1 <= i1 by A295, NAT_1:13; then A387: 1 <= l by XREAL_1:19; then 0 + 1 <= ma by A309, A329, A386, XREAL_1:7; then reconsider m1 = ma - 1 as Element of NAT by INT_1:5; A388: m1 + 1 = ma ; (len g1) + 1 <= ma by A309, A329, A386, A387, XREAL_1:7; then A389: m1 >= len g1 by A388, XREAL_1:6; reconsider q = g /. m1 as Point of (TOP-REAL 2) ; set lq = { e where e is Point of (TOP-REAL 2) : ( e `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= e `1 & e `1 <= q `1 ) } ; A390: i1 - l = j1 ; A391: l in dom g2 by A310, A387, FINSEQ_1:1; then A392: g /. ma = g2 /. l by A309, A329, A386, FINSEQ_4:69 .= G * (j1,i2) by A309, A310, A391, A390 ; then p1 `1 <= (G * (j1,i2)) `1 by A385; then A393: p1 `1 = (G * (j1,i2)) `1 by A380, XXREAL_0:1; A394: m1 <= len g by A386, A388, NAT_1:11; then A395: q `2 = (G * (i1,i2)) `2 by A330, A389; A396: (G * (j1,i2)) `1 <= q `1 by A330, A389, A394; 1 <= len g1 by A13, A23, A39, XXREAL_0:2; then A397: 1 <= m1 by A389, XXREAL_0:2; then ( q = |[(q `1),(q `2)]| & LSeg (g,m1) = LSeg ((G * (j1,i2)),q) ) by A386, A392, A388, EUCLID:53, TOPREAL1:def_3; then LSeg (g,m1) = { e where e is Point of (TOP-REAL 2) : ( e `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= e `1 & e `1 <= q `1 ) } by A302, A327, A395, A396, TOPREAL3:10; then A398: p1 in LSeg (g,m1) by A379, A393, A396; LSeg (g,m1) in { (LSeg (g,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } by A386, A388, A397; hence x in L~ g by A378, A398, TARSKI:def_4; ::_thesis: verum end; suppose ma <> len g ; ::_thesis: x in L~ g then ma < len g by A385, XXREAL_0:1; then A399: ma + 1 <= len g by NAT_1:13; reconsider qa = g /. ma, qa1 = g /. (ma + 1) as Point of (TOP-REAL 2) ; set lma = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `2 = (G * (i1,i2)) `2 & qa1 `1 <= p2 `1 & p2 `1 <= qa `1 ) } ; A400: qa1 = |[(qa1 `1),(qa1 `2)]| by EUCLID:53; A401: p1 `1 <= qa `1 by A385; A402: len g1 <= ma + 1 by A385, NAT_1:13; then A403: qa1 `2 = (G * (i1,i2)) `2 by A330, A399; A404: now__::_thesis:_not_p1_`1_<=_qa1_`1 assume p1 `1 <= qa1 `1 ; ::_thesis: contradiction then for q being Point of (TOP-REAL 2) st q = g /. (ma + 1) holds p1 `1 <= q `1 ; then ma + 1 <= ma by A385, A399, A402; hence contradiction by XREAL_1:29; ::_thesis: verum end; A405: ( qa `2 = (G * (i1,i2)) `2 & qa = |[(qa `1),(qa `2)]| ) by A330, A385, EUCLID:53; A406: 1 <= ma by A13, A23, A39, A385, NAT_1:13; then LSeg (g,ma) = LSeg (qa1,qa) by A399, TOPREAL1:def_3 .= { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `2 = (G * (i1,i2)) `2 & qa1 `1 <= p2 `1 & p2 `1 <= qa `1 ) } by A401, A404, A403, A405, A400, TOPREAL3:10, XXREAL_0:2 ; then A407: x in LSeg (g,ma) by A378, A379, A401, A404; LSeg (g,ma) in { (LSeg (g,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } by A406, A399; hence x in L~ g by A407, TARSKI:def_4; ::_thesis: verum end; end; end; hence x in L~ g ; ::_thesis: verum end; end; end; hence x in L~ g ; ::_thesis: verum end; 1 <= len g1 by A13, A23, A39, XXREAL_0:2; then 1 in dom g1 by A57, FINSEQ_1:1; hence g /. 1 = (f | k) /. 1 by A37, FINSEQ_4:68 .= f /. 1 by A17, A15, FINSEQ_4:71 ; ::_thesis: ( g /. (len g) = f /. (len f) & len f <= len g ) A408: len g = (len g1) + (len g2) by FINSEQ_1:22; j1 + 1 <= i1 by A295, NAT_1:13; then A409: 1 <= l by XREAL_1:19; then A410: l in dom g2 by A310, FINSEQ_1:1; hence g /. (len g) = g2 /. l by A309, A408, FINSEQ_4:69 .= G * (m1,i2) by A309, A310, A410 .= f /. (len f) by A3, A46, A294 ; ::_thesis: len f <= len g thus len f <= len g by A3, A23, A39, A309, A409, A408, XREAL_1:7; ::_thesis: verum end; case i1 = j1 ; ::_thesis: contradiction hence contradiction by A6, A17, A19, A44, A46, A294; ::_thesis: verum end; caseA411: i1 < j1 ; ::_thesis: ex g being FinSequence of the carrier of (TOP-REAL 2) st ( g is_sequence_on G & L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) set lk = { w where w is Point of (TOP-REAL 2) : ( w `2 = (G * (i1,i2)) `2 & (G * (i1,i2)) `1 <= w `1 & w `1 <= (G * (j1,i2)) `1 ) } ; A412: G * (i1,i2) = |[((G * (i1,i2)) `1),((G * (i1,i2)) `2)]| by EUCLID:53; reconsider l = j1 - i1 as Element of NAT by A411, INT_1:5; deffunc H1( Nat) -> Element of the carrier of (TOP-REAL 2) = G * ((i1 + $1),i2); consider g2 being FinSequence of (TOP-REAL 2) such that A413: ( len g2 = l & ( for n being Nat st n in dom g2 holds g2 /. n = H1(n) ) ) from FINSEQ_4:sch_2(); take g = g1 ^ g2; ::_thesis: ( g is_sequence_on G & L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) A414: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_Seg_l_holds_ (_i1_+_n_in_dom_G_&_[(i1_+_n),i2]_in_Indices_G_) let n be Element of NAT ; ::_thesis: ( n in Seg l implies ( i1 + n in dom G & [(i1 + n),i2] in Indices G ) ) A415: n <= i1 + n by NAT_1:11; assume A416: n in Seg l ; ::_thesis: ( i1 + n in dom G & [(i1 + n),i2] in Indices G ) then n <= l by FINSEQ_1:1; then A417: i1 + n <= l + i1 by XREAL_1:7; j1 <= len G by A48, FINSEQ_3:25; then A418: i1 + n <= len G by A417, XXREAL_0:2; 1 <= n by A416, FINSEQ_1:1; then 1 <= i1 + n by A415, XXREAL_0:2; hence i1 + n in dom G by A418, FINSEQ_3:25; ::_thesis: [(i1 + n),i2] in Indices G hence [(i1 + n),i2] in Indices G by A47, A51, ZFMISC_1:87; ::_thesis: verum end; A419: dom g2 = Seg (len g2) by FINSEQ_1:def_3; now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_g2_holds_ ex_m_being_Element_of_NAT_ex_k_being_Element_of_NAT_st_ (_[m,k]_in_Indices_G_&_g2_/._n_=_G_*_(m,k)_) let n be Element of NAT ; ::_thesis: ( n in dom g2 implies ex m being Element of NAT ex k being Element of NAT st ( [m,k] in Indices G & g2 /. n = G * (m,k) ) ) assume A420: n in dom g2 ; ::_thesis: ex m being Element of NAT ex k being Element of NAT st ( [m,k] in Indices G & g2 /. n = G * (m,k) ) take m = i1 + n; ::_thesis: ex k being Element of NAT st ( [m,k] in Indices G & g2 /. n = G * (m,k) ) take k = i2; ::_thesis: ( [m,k] in Indices G & g2 /. n = G * (m,k) ) thus ( [m,k] in Indices G & g2 /. n = G * (m,k) ) by A413, A414, A419, A420; ::_thesis: verum end; then A421: for n being Element of NAT st n in dom g holds ex i, j being Element of NAT st ( [i,j] in Indices G & g /. n = G * (i,j) ) by A40, GOBOARD1:23; A422: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_g2_&_n_+_1_in_dom_g2_holds_ for_l1,_l2,_l3,_l4_being_Element_of_NAT_st_[l1,l2]_in_Indices_G_&_[l3,l4]_in_Indices_G_&_g2_/._n_=_G_*_(l1,l2)_&_g2_/._(n_+_1)_=_G_*_(l3,l4)_holds_ (abs_(l1_-_l3))_+_(abs_(l2_-_l4))_=_1 let n be Element of NAT ; ::_thesis: ( n in dom g2 & n + 1 in dom g2 implies for l1, l2, l3, l4 being Element of NAT st [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) holds (abs (l1 - l3)) + (abs (l2 - l4)) = 1 ) assume that A423: n in dom g2 and A424: n + 1 in dom g2 ; ::_thesis: for l1, l2, l3, l4 being Element of NAT st [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) holds (abs (l1 - l3)) + (abs (l2 - l4)) = 1 let l1, l2, l3, l4 be Element of NAT ; ::_thesis: ( [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) implies (abs (l1 - l3)) + (abs (l2 - l4)) = 1 ) assume that A425: [l1,l2] in Indices G and A426: [l3,l4] in Indices G and A427: g2 /. n = G * (l1,l2) and A428: g2 /. (n + 1) = G * (l3,l4) ; ::_thesis: (abs (l1 - l3)) + (abs (l2 - l4)) = 1 ( g2 /. (n + 1) = G * ((i1 + (n + 1)),i2) & [(i1 + (n + 1)),i2] in Indices G ) by A413, A414, A419, A424; then A429: ( l3 = i1 + (n + 1) & l4 = i2 ) by A426, A428, GOBOARD1:5; ( g2 /. n = G * ((i1 + n),i2) & [(i1 + n),i2] in Indices G ) by A413, A414, A419, A423; then ( l1 = i1 + n & l2 = i2 ) by A425, A427, GOBOARD1:5; hence (abs (l1 - l3)) + (abs (l2 - l4)) = (abs ((i1 + n) - (i1 + (n + 1)))) + 0 by A429, ABSVALUE:2 .= abs (- 1) .= abs 1 by COMPLEX1:52 .= 1 by ABSVALUE:def_1 ; ::_thesis: verum end; now__::_thesis:_for_l1,_l2,_l3,_l4_being_Element_of_NAT_st_[l1,l2]_in_Indices_G_&_[l3,l4]_in_Indices_G_&_g1_/._(len_g1)_=_G_*_(l1,l2)_&_g2_/._1_=_G_*_(l3,l4)_&_len_g1_in_dom_g1_&_1_in_dom_g2_holds_ (abs_(l1_-_l3))_+_(abs_(l2_-_l4))_=_1 let l1, l2, l3, l4 be Element of NAT ; ::_thesis: ( [l1,l2] in Indices G & [l3,l4] in Indices G & g1 /. (len g1) = G * (l1,l2) & g2 /. 1 = G * (l3,l4) & len g1 in dom g1 & 1 in dom g2 implies (abs (l1 - l3)) + (abs (l2 - l4)) = 1 ) assume that A430: [l1,l2] in Indices G and A431: [l3,l4] in Indices G and A432: g1 /. (len g1) = G * (l1,l2) and A433: g2 /. 1 = G * (l3,l4) and len g1 in dom g1 and A434: 1 in dom g2 ; ::_thesis: (abs (l1 - l3)) + (abs (l2 - l4)) = 1 ( g2 /. 1 = G * ((i1 + 1),i2) & [(i1 + 1),i2] in Indices G ) by A413, A414, A419, A434; then A435: ( l3 = i1 + 1 & l4 = i2 ) by A431, A433, GOBOARD1:5; (f | k) /. (len (f | k)) = f /. k by A17, A23, A14, FINSEQ_4:71; then ( l1 = i1 & l2 = i2 ) by A38, A18, A19, A430, A432, GOBOARD1:5; hence (abs (l1 - l3)) + (abs (l2 - l4)) = (abs (i1 - (i1 + 1))) + 0 by A435, ABSVALUE:2 .= abs ((i1 - i1) + (- 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 g & n + 1 in dom g holds for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & g /. n = G * (m,k) & g /. (n + 1) = G * (i,j) holds (abs (m - i)) + (abs (k - j)) = 1 by A41, A422, GOBOARD1:24; hence g is_sequence_on G by A421, GOBOARD1:def_9; ::_thesis: ( L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) A436: G * (j1,i2) = |[((G * (j1,i2)) `1),((G * (j1,i2)) `2)]| by EUCLID:53; c1 /. j1 = c1 . j1 by A48, A43, PARTFUN1:def_6; then A437: c1 /. j1 = G * (j1,i2) by A48, MATRIX_1:def_8; then A438: (X_axis c1) . j1 = (G * (j1,i2)) `1 by A48, A43, A22, GOBOARD1:def_1; c1 /. i1 = c1 . i1 by A49, A43, PARTFUN1:def_6; then A439: c1 /. i1 = G * (i1,i2) by A49, MATRIX_1:def_8; then A440: (X_axis c1) . i1 = (G * (i1,i2)) `1 by A49, A43, A22, GOBOARD1:def_1; then A441: (G * (i1,i2)) `1 < (G * (j1,i2)) `1 by A49, A48, A52, A43, A22, A411, A438, SEQM_3:def_1; A442: (Y_axis c1) . j1 = (G * (j1,i2)) `2 by A48, A43, A21, A437, GOBOARD1:def_2; (Y_axis c1) . i1 = (G * (i1,i2)) `2 by A49, A43, A21, A439, GOBOARD1:def_2; then A443: (G * (i1,i2)) `2 = (G * (j1,i2)) `2 by A49, A48, A53, A43, A21, A442, SEQM_3:def_10; A444: LSeg (f,k) = LSeg ((G * (i1,i2)),(G * (j1,i2))) by A3, A13, A19, A46, A294, TOPREAL1:def_3 .= { w where w is Point of (TOP-REAL 2) : ( w `2 = (G * (i1,i2)) `2 & (G * (i1,i2)) `1 <= w `1 & w `1 <= (G * (j1,i2)) `1 ) } by A441, A443, A412, A436, TOPREAL3:10 ; A445: dom g2 = Seg l by A413, FINSEQ_1:def_3; thus L~ g = L~ f ::_thesis: ( g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) proof set lg = { (LSeg (g,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } ; set lf = { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } ; A446: len g = (len g1) + (len g2) by FINSEQ_1:22; A447: now__::_thesis:_for_j_being_Element_of_NAT_st_len_g1_<=_j_&_j_<=_len_g_holds_ for_p_being_Point_of_(TOP-REAL_2)_st_p_=_g_/._j_holds_ (_p_`2_=_(G_*_(i1,i2))_`2_&_(G_*_(i1,i2))_`1_<=_p_`1_&_p_`1_<=_(G_*_(j1,i2))_`1_&_p_in_rng_c1_) let j be Element of NAT ; ::_thesis: ( len g1 <= j & j <= len g implies for p being Point of (TOP-REAL 2) st p = g /. j holds ( p `2 = (G * (i1,i2)) `2 & (G * (i1,i2)) `1 <= p `1 & p `1 <= (G * (j1,i2)) `1 & p in rng c1 ) ) assume that A448: len g1 <= j and A449: j <= len g ; ::_thesis: for p being Point of (TOP-REAL 2) st p = g /. j holds ( p `2 = (G * (i1,i2)) `2 & (G * (i1,i2)) `1 <= p `1 & p `1 <= (G * (j1,i2)) `1 & p in rng c1 ) reconsider w = j - (len g1) as Element of NAT by A448, INT_1:5; set u = i1 + w; let p be Point of (TOP-REAL 2); ::_thesis: ( p = g /. j implies ( p `2 = (G * (i1,i2)) `2 & (G * (i1,i2)) `1 <= p `1 & p `1 <= (G * (j1,i2)) `1 & p in rng c1 ) ) assume A450: p = g /. j ; ::_thesis: ( p `2 = (G * (i1,i2)) `2 & (G * (i1,i2)) `1 <= p `1 & p `1 <= (G * (j1,i2)) `1 & p in rng c1 ) now__::_thesis:_(_p_`2_=_(G_*_(i1,i2))_`2_&_(G_*_(i1,i2))_`1_<=_p_`1_&_p_`1_<=_(G_*_(j1,i2))_`1_&_p_in_rng_c1_) percases ( j = len g1 or j <> len g1 ) ; supposeA451: j = len g1 ; ::_thesis: ( p `2 = (G * (i1,i2)) `2 & (G * (i1,i2)) `1 <= p `1 & p `1 <= (G * (j1,i2)) `1 & p in rng c1 ) 1 <= len g1 by A13, A23, A39, XXREAL_0:2; then len g1 in dom g1 by FINSEQ_3:25; then A452: g /. (len g1) = (f | k) /. (len (f | k)) by A38, FINSEQ_4:68 .= G * (i1,i2) by A17, A23, A14, A19, FINSEQ_4:71 ; hence p `2 = (G * (i1,i2)) `2 by A450, A451; ::_thesis: ( (G * (i1,i2)) `1 <= p `1 & p `1 <= (G * (j1,i2)) `1 & p in rng c1 ) thus ( (G * (i1,i2)) `1 <= p `1 & p `1 <= (G * (j1,i2)) `1 ) by A49, A48, A52, A43, A22, A411, A440, A438, A450, A451, A452, SEQM_3:def_1; ::_thesis: p in rng c1 thus p in rng c1 by A49, A43, A439, A450, A451, A452, PARTFUN2:2; ::_thesis: verum end; supposeA453: j <> len g1 ; ::_thesis: ( p `2 = (G * (i1,i2)) `2 & (G * (i1,i2)) `1 <= p `1 & p `1 <= (G * (j1,i2)) `1 & p in rng c1 ) A454: w + (len g1) = j ; then A455: w <= len g2 by A446, A449, XREAL_1:6; A456: (Y_axis c1) . i1 = (G * (i1,i2)) `2 by A49, A43, A21, A439, GOBOARD1:def_2; A457: j - (len g1) <> 0 by A453; then A458: w >= 1 by NAT_1:14; then A459: g /. j = g2 /. w by A454, A455, SEQ_4:136; A460: i1 < i1 + w by A457, XREAL_1:29; A461: w in dom g2 by A458, A455, FINSEQ_3:25; then A462: i1 + w in dom G by A445, A414; c1 /. (i1 + w) = c1 . (i1 + w) by A43, A445, A414, A461, PARTFUN1:def_6; then A463: c1 /. (i1 + w) = G * ((i1 + w),i2) by A462, MATRIX_1:def_8; then A464: (X_axis c1) . (i1 + w) = (G * ((i1 + w),i2)) `1 by A43, A22, A462, GOBOARD1:def_1; A465: g2 /. w = G * ((i1 + w),i2) by A413, A461; (Y_axis c1) . (i1 + w) = (G * ((i1 + w),i2)) `2 by A43, A21, A462, A463, GOBOARD1:def_2; hence p `2 = (G * (i1,i2)) `2 by A49, A53, A43, A21, A450, A459, A465, A462, A456, SEQM_3:def_10; ::_thesis: ( (G * (i1,i2)) `1 <= p `1 & p `1 <= (G * (j1,i2)) `1 & p in rng c1 ) (X_axis c1) . i1 = (G * (i1,i2)) `1 by A49, A43, A22, A439, GOBOARD1:def_1; hence (G * (i1,i2)) `1 <= p `1 by A49, A52, A43, A22, A450, A459, A465, A462, A464, A460, SEQM_3:def_1; ::_thesis: ( p `1 <= (G * (j1,i2)) `1 & p in rng c1 ) A466: (X_axis c1) . j1 = (G * (j1,i2)) `1 by A48, A43, A22, A437, GOBOARD1:def_1; now__::_thesis:_p_`1_<=_(G_*_(j1,i2))_`1 percases ( i1 + w = j1 or i1 + w <> j1 ) ; suppose i1 + w = j1 ; ::_thesis: p `1 <= (G * (j1,i2)) `1 hence p `1 <= (G * (j1,i2)) `1 by A450, A458, A454, A455, A465, SEQ_4:136; ::_thesis: verum end; supposeA467: i1 + w <> j1 ; ::_thesis: p `1 <= (G * (j1,i2)) `1 i1 + w <= i1 + l by A413, A455, XREAL_1:7; then i1 + w < j1 by A467, XXREAL_0:1; hence p `1 <= (G * (j1,i2)) `1 by A48, A52, A43, A22, A450, A459, A465, A462, A464, A466, SEQM_3:def_1; ::_thesis: verum end; end; end; hence p `1 <= (G * (j1,i2)) `1 ; ::_thesis: p in rng c1 thus p in rng c1 by A43, A450, A459, A465, A462, A463, PARTFUN2:2; ::_thesis: verum end; end; end; hence ( p `2 = (G * (i1,i2)) `2 & (G * (i1,i2)) `1 <= p `1 & p `1 <= (G * (j1,i2)) `1 & p in rng c1 ) ; ::_thesis: verum end; thus L~ g c= L~ f :: according to XBOOLE_0:def_10 ::_thesis: L~ f c= L~ g proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in L~ g or x in L~ f ) assume x in L~ g ; ::_thesis: x in L~ f then consider X being set such that A468: x in X and A469: X in { (LSeg (g,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } by TARSKI:def_4; consider i being Element of NAT such that A470: X = LSeg (g,i) and A471: 1 <= i and A472: i + 1 <= len g by A469; now__::_thesis:_x_in_L~_f percases ( i + 1 <= len g1 or i + 1 > len g1 ) ; supposeA473: i + 1 <= len g1 ; ::_thesis: x in L~ f i <= i + 1 by NAT_1:11; then i <= len g1 by A473, XXREAL_0:2; then A474: i in dom g1 by A471, FINSEQ_3:25; 1 <= i + 1 by NAT_1:11; then i + 1 in dom g1 by A473, FINSEQ_3:25; then X = LSeg (g1,i) by A470, A474, TOPREAL3:18; then X in { (LSeg (g1,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g1 ) } by A471, A473; then A475: x in L~ (f | k) by A36, A468, TARSKI:def_4; L~ (f | k) c= L~ f by TOPREAL3:20; hence x in L~ f by A475; ::_thesis: verum end; supposeA476: i + 1 > len g1 ; ::_thesis: x in L~ f reconsider q1 = g /. i, q2 = g /. (i + 1) as Point of (TOP-REAL 2) ; A477: i <= len g by A472, NAT_1:13; A478: len g1 <= i by A476, NAT_1:13; then A479: q1 `2 = (G * (i1,i2)) `2 by A447, A477; A480: q1 `1 <= (G * (j1,i2)) `1 by A447, A478, A477; A481: (G * (i1,i2)) `1 <= q1 `1 by A447, A478, A477; q2 `2 = (G * (i1,i2)) `2 by A447, A472, A476; then A482: q2 = |[(q2 `1),(q1 `2)]| by A479, EUCLID:53; A483: q2 `1 <= (G * (j1,i2)) `1 by A447, A472, A476; A484: ( q1 = |[(q1 `1),(q1 `2)]| & LSeg (g,i) = LSeg (q2,q1) ) by A471, A472, EUCLID:53, TOPREAL1:def_3; A485: (G * (i1,i2)) `1 <= q2 `1 by A447, A472, A476; now__::_thesis:_x_in_L~_f percases ( q1 `1 > q2 `1 or q1 `1 = q2 `1 or q1 `1 < q2 `1 ) by XXREAL_0:1; suppose q1 `1 > q2 `1 ; ::_thesis: x in L~ f then LSeg (g,i) = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `2 = q1 `2 & q2 `1 <= p2 `1 & p2 `1 <= q1 `1 ) } by A482, A484, TOPREAL3:10; then consider p2 being Point of (TOP-REAL 2) such that A486: ( p2 = x & p2 `2 = q1 `2 ) and A487: ( q2 `1 <= p2 `1 & p2 `1 <= q1 `1 ) by A468, A470; ( (G * (i1,i2)) `1 <= p2 `1 & p2 `1 <= (G * (j1,i2)) `1 ) by A480, A485, A487, XXREAL_0:2; then A488: x in LSeg (f,k) by A444, A479, A486; LSeg (f,k) in { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } by A3, A13; hence x in L~ f by A488, TARSKI:def_4; ::_thesis: verum end; suppose q1 `1 = q2 `1 ; ::_thesis: x in L~ f then LSeg (g,i) = {q1} by A482, A484, RLTOPSP1:70; then x = q1 by A468, A470, TARSKI:def_1; then A489: x in LSeg (f,k) by A444, A479, A481, A480; LSeg (f,k) in { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } by A3, A13; hence x in L~ f by A489, TARSKI:def_4; ::_thesis: verum end; suppose q1 `1 < q2 `1 ; ::_thesis: x in L~ f then LSeg (g,i) = { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `2 = q1 `2 & q1 `1 <= p1 `1 & p1 `1 <= q2 `1 ) } by A482, A484, TOPREAL3:10; then consider p2 being Point of (TOP-REAL 2) such that A490: ( p2 = x & p2 `2 = q1 `2 ) and A491: ( q1 `1 <= p2 `1 & p2 `1 <= q2 `1 ) by A468, A470; ( (G * (i1,i2)) `1 <= p2 `1 & p2 `1 <= (G * (j1,i2)) `1 ) by A481, A483, A491, XXREAL_0:2; then A492: x in LSeg (f,k) by A444, A479, A490; LSeg (f,k) in { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } by A3, A13; hence x in L~ f by A492, TARSKI:def_4; ::_thesis: verum end; end; end; hence x in L~ f ; ::_thesis: verum end; end; end; hence x in L~ f ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in L~ f or x in L~ g ) assume x in L~ f ; ::_thesis: x in L~ g then A493: x in (L~ (f | k)) \/ (LSeg (f,k)) by A3, A12, Th3; now__::_thesis:_x_in_L~_g percases ( x in L~ (f | k) or x in LSeg (f,k) ) by A493, XBOOLE_0:def_3; supposeA494: x in L~ (f | k) ; ::_thesis: x in L~ g L~ g1 c= L~ g by Th6; hence x in L~ g by A36, A494; ::_thesis: verum end; suppose x in LSeg (f,k) ; ::_thesis: x in L~ g then consider p1 being Point of (TOP-REAL 2) such that A495: p1 = x and A496: p1 `2 = (G * (i1,i2)) `2 and A497: (G * (i1,i2)) `1 <= p1 `1 and A498: p1 `1 <= (G * (j1,i2)) `1 by A444; defpred S2[ Nat] means ( len g1 <= $1 & $1 <= len g & ( for q being Point of (TOP-REAL 2) st q = g /. $1 holds q `1 <= p1 `1 ) ); A499: now__::_thesis:_ex_n_being_Nat_st_S2[n] reconsider n = len g1 as Nat ; take n = n; ::_thesis: S2[n] thus S2[n] ::_thesis: verum proof thus ( len g1 <= n & n <= len g ) by A446, XREAL_1:31; ::_thesis: for q being Point of (TOP-REAL 2) st q = g /. n holds q `1 <= p1 `1 1 <= len g1 by A13, A23, A39, XXREAL_0:2; then A500: len g1 in dom g1 by FINSEQ_3:25; let q be Point of (TOP-REAL 2); ::_thesis: ( q = g /. n implies q `1 <= p1 `1 ) assume q = g /. n ; ::_thesis: q `1 <= p1 `1 then q = (f | k) /. (len (f | k)) by A38, A500, FINSEQ_4:68 .= G * (i1,i2) by A17, A23, A14, A19, FINSEQ_4:71 ; hence q `1 <= p1 `1 by A497; ::_thesis: verum end; end; A501: for n being Nat st S2[n] holds n <= len g ; consider ma being Nat such that A502: ( S2[ma] & ( for n being Nat st S2[n] holds n <= ma ) ) from NAT_1:sch_6(A501, A499); reconsider ma = ma as Element of NAT by ORDINAL1:def_12; now__::_thesis:_x_in_L~_g percases ( ma = len g or ma <> len g ) ; supposeA503: ma = len g ; ::_thesis: x in L~ g i1 + 1 <= j1 by A411, NAT_1:13; then A504: 1 <= l by XREAL_1:19; then 0 + 1 <= ma by A413, A446, A503, XREAL_1:7; then reconsider m1 = ma - 1 as Element of NAT by INT_1:5; A505: m1 + 1 = ma ; (len g1) + 1 <= ma by A413, A446, A503, A504, XREAL_1:7; then A506: m1 >= len g1 by A505, XREAL_1:6; reconsider q = g /. m1 as Point of (TOP-REAL 2) ; set lq = { e where e is Point of (TOP-REAL 2) : ( e `2 = (G * (i1,i2)) `2 & q `1 <= e `1 & e `1 <= (G * (j1,i2)) `1 ) } ; A507: i1 + l = j1 ; A508: l in dom g2 by A413, A504, FINSEQ_3:25; then A509: g /. ma = g2 /. l by A413, A446, A503, FINSEQ_4:69 .= G * (j1,i2) by A413, A508, A507 ; then (G * (j1,i2)) `1 <= p1 `1 by A502; then A510: p1 `1 = (G * (j1,i2)) `1 by A498, XXREAL_0:1; A511: m1 <= len g by A503, A505, NAT_1:11; then A512: q `2 = (G * (i1,i2)) `2 by A447, A506; A513: q `1 <= (G * (j1,i2)) `1 by A447, A506, A511; 1 <= len g1 by A13, A23, A39, XXREAL_0:2; then A514: 1 <= m1 by A506, XXREAL_0:2; then ( q = |[(q `1),(q `2)]| & LSeg (g,m1) = LSeg ((G * (j1,i2)),q) ) by A503, A509, A505, EUCLID:53, TOPREAL1:def_3; then LSeg (g,m1) = { e where e is Point of (TOP-REAL 2) : ( e `2 = (G * (i1,i2)) `2 & q `1 <= e `1 & e `1 <= (G * (j1,i2)) `1 ) } by A443, A436, A512, A513, TOPREAL3:10; then A515: p1 in LSeg (g,m1) by A496, A510, A513; LSeg (g,m1) in { (LSeg (g,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } by A503, A505, A514; hence x in L~ g by A495, A515, TARSKI:def_4; ::_thesis: verum end; suppose ma <> len g ; ::_thesis: x in L~ g then ma < len g by A502, XXREAL_0:1; then A516: ma + 1 <= len g by NAT_1:13; reconsider qa = g /. ma, qa1 = g /. (ma + 1) as Point of (TOP-REAL 2) ; set lma = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `2 = (G * (i1,i2)) `2 & qa `1 <= p2 `1 & p2 `1 <= qa1 `1 ) } ; A517: qa1 = |[(qa1 `1),(qa1 `2)]| by EUCLID:53; A518: qa `1 <= p1 `1 by A502; A519: len g1 <= ma + 1 by A502, NAT_1:13; then A520: qa1 `2 = (G * (i1,i2)) `2 by A447, A516; A521: now__::_thesis:_not_qa1_`1_<=_p1_`1 assume qa1 `1 <= p1 `1 ; ::_thesis: contradiction then for q being Point of (TOP-REAL 2) st q = g /. (ma + 1) holds q `1 <= p1 `1 ; then ma + 1 <= ma by A502, A516, A519; hence contradiction by XREAL_1:29; ::_thesis: verum end; A522: ( qa `2 = (G * (i1,i2)) `2 & qa = |[(qa `1),(qa `2)]| ) by A447, A502, EUCLID:53; A523: 1 <= ma by A13, A23, A39, A502, NAT_1:13; then LSeg (g,ma) = LSeg (qa,qa1) by A516, TOPREAL1:def_3 .= { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `2 = (G * (i1,i2)) `2 & qa `1 <= p2 `1 & p2 `1 <= qa1 `1 ) } by A518, A521, A520, A522, A517, TOPREAL3:10, XXREAL_0:2 ; then A524: x in LSeg (g,ma) by A495, A496, A518, A521; LSeg (g,ma) in { (LSeg (g,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } by A523, A516; hence x in L~ g by A524, TARSKI:def_4; ::_thesis: verum end; end; end; hence x in L~ g ; ::_thesis: verum end; end; end; hence x in L~ g ; ::_thesis: verum end; 1 <= len g1 by A13, A23, A39, XXREAL_0:2; then 1 in dom g1 by FINSEQ_3:25; hence g /. 1 = (f | k) /. 1 by A37, FINSEQ_4:68 .= f /. 1 by A17, A15, FINSEQ_4:71 ; ::_thesis: ( g /. (len g) = f /. (len f) & len f <= len g ) A525: len g = (len g1) + l by A413, FINSEQ_1:22; i1 + 1 <= j1 by A411, NAT_1:13; then A526: 1 <= l by XREAL_1:19; then A527: l in dom g2 by A413, A419, FINSEQ_1:1; hence g /. (len g) = g2 /. l by A525, FINSEQ_4:69 .= G * ((i1 + l),i2) by A413, A527 .= f /. (len f) by A3, A46, A294 ; ::_thesis: len f <= len g thus len f <= len g by A3, A23, A39, A526, A525, XREAL_1:7; ::_thesis: verum end; end; end; hence ex g being FinSequence of (TOP-REAL 2) st ( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) ; ::_thesis: verum end; end; end; hence ex g being FinSequence of (TOP-REAL 2) st ( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) ; ::_thesis: verum end; end; end; hence ex g being FinSequence of (TOP-REAL 2) st ( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) ; ::_thesis: verum end; A528: S1[ 0 ] proof let f be FinSequence of (TOP-REAL 2); ::_thesis: ( len f = 0 & ( for n being Element of NAT st n in dom f holds ex i, j being Element of NAT st ( [i,j] in Indices G & f /. n = G * (i,j) ) ) & f is special & ( for n being Element of NAT st n in dom f & n + 1 in dom f holds f /. n <> f /. (n + 1) ) implies ex g being FinSequence of (TOP-REAL 2) st ( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) ) assume that A529: len f = 0 and A530: for n being Element of NAT st n in dom f holds ex i, j being Element of NAT st ( [i,j] in Indices G & f /. n = G * (i,j) ) and f is special and for n being Element of NAT st n in dom f & n + 1 in dom f holds f /. n <> f /. (n + 1) ; ::_thesis: ex g being FinSequence of (TOP-REAL 2) st ( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) take g = f; ::_thesis: ( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) f = {} by A529; then for n being Element of NAT st n in dom g & n + 1 in dom g holds for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & g /. n = G * (m,k) & g /. (n + 1) = G * (i,j) holds (abs (m - i)) + (abs (k - j)) = 1 ; hence ( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) by A530, GOBOARD1:def_9; ::_thesis: verum end; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A528, A1); hence ( ( for n being Element of NAT st n in dom f holds ex i, j being Element of NAT st ( [i,j] in Indices G & f /. n = G * (i,j) ) ) & f is special & ( for n being Element of NAT st n in dom f & n + 1 in dom f holds f /. n <> f /. (n + 1) ) implies ex g being FinSequence of (TOP-REAL 2) st ( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) ) ; ::_thesis: verum end; definition let v1, v2 be FinSequence of REAL ; assume A1: v1 <> {} ; func GoB (v1,v2) -> Matrix of (TOP-REAL 2) means :Def1: :: GOBOARD2:def 1 ( len it = len v1 & width it = len v2 & ( for n, m being Element of NAT st [n,m] in Indices it holds it * (n,m) = |[(v1 . n),(v2 . m)]| ) ); existence ex b1 being Matrix of (TOP-REAL 2) st ( len b1 = len v1 & width b1 = len v2 & ( for n, m being Element of NAT st [n,m] in Indices b1 holds b1 * (n,m) = |[(v1 . n),(v2 . m)]| ) ) proof defpred S1[ Nat, Nat, Point of (TOP-REAL 2)] means ( [$1,$2] in [:(dom v1),(dom v2):] & ( for r, s being Real st v1 . $1 = r & v2 . $2 = s holds $3 = |[r,s]| ) ); A2: dom v1 = Seg (len v1) by FINSEQ_1:def_3; A3: for i, j being Nat st [i,j] in [:(Seg (len v1)),(Seg (len v2)):] holds ex p being Point of (TOP-REAL 2) st S1[i,j,p] proof let i, j be Nat; ::_thesis: ( [i,j] in [:(Seg (len v1)),(Seg (len v2)):] implies ex p being Point of (TOP-REAL 2) st S1[i,j,p] ) assume A4: [i,j] in [:(Seg (len v1)),(Seg (len v2)):] ; ::_thesis: ex p being Point of (TOP-REAL 2) st S1[i,j,p] reconsider i9 = i, j9 = j as Element of NAT by ORDINAL1:def_12; reconsider s1 = v1 . i9, s2 = v2 . j9 as Real ; take |[s1,s2]| ; ::_thesis: S1[i,j,|[s1,s2]|] thus [i,j] in [:(dom v1),(dom v2):] by A2, A4, FINSEQ_1:def_3; ::_thesis: for r, s being Real st v1 . i = r & v2 . j = s holds |[s1,s2]| = |[r,s]| let r, s be Real; ::_thesis: ( v1 . i = r & v2 . j = s implies |[s1,s2]| = |[r,s]| ) assume ( r = v1 . i & s = v2 . j ) ; ::_thesis: |[s1,s2]| = |[r,s]| hence |[s1,s2]| = |[r,s]| ; ::_thesis: verum end; consider M being Matrix of len v1, len v2, the carrier of (TOP-REAL 2) such that A5: for i, j being Nat st [i,j] in Indices M holds S1[i,j,M * (i,j)] from MATRIX_1:sch_2(A3); reconsider M = M as Matrix of the carrier of (TOP-REAL 2) ; take M ; ::_thesis: ( len M = len v1 & width M = len v2 & ( for n, m being Element of NAT st [n,m] in Indices M holds M * (n,m) = |[(v1 . n),(v2 . m)]| ) ) thus ( len M = len v1 & width M = len v2 ) by A1, MATRIX_1:23; ::_thesis: for n, m being Element of NAT st [n,m] in Indices M holds M * (n,m) = |[(v1 . n),(v2 . m)]| let n, m be Element of NAT ; ::_thesis: ( [n,m] in Indices M implies M * (n,m) = |[(v1 . n),(v2 . m)]| ) assume [n,m] in Indices M ; ::_thesis: M * (n,m) = |[(v1 . n),(v2 . m)]| hence M * (n,m) = |[(v1 . n),(v2 . m)]| by A5; ::_thesis: verum end; uniqueness for b1, b2 being Matrix of (TOP-REAL 2) st len b1 = len v1 & width b1 = len v2 & ( for n, m being Element of NAT st [n,m] in Indices b1 holds b1 * (n,m) = |[(v1 . n),(v2 . m)]| ) & len b2 = len v1 & width b2 = len v2 & ( for n, m being Element of NAT st [n,m] in Indices b2 holds b2 * (n,m) = |[(v1 . n),(v2 . m)]| ) holds b1 = b2 proof let G1, G2 be Matrix of (TOP-REAL 2); ::_thesis: ( len G1 = len v1 & width G1 = len v2 & ( for n, m being Element of NAT st [n,m] in Indices G1 holds G1 * (n,m) = |[(v1 . n),(v2 . m)]| ) & len G2 = len v1 & width G2 = len v2 & ( for n, m being Element of NAT st [n,m] in Indices G2 holds G2 * (n,m) = |[(v1 . n),(v2 . m)]| ) implies G1 = G2 ) assume that A6: ( len G1 = len v1 & width G1 = len v2 ) and A7: for n, m being Element of NAT st [n,m] in Indices G1 holds G1 * (n,m) = |[(v1 . n),(v2 . m)]| and A8: ( len G2 = len v1 & width G2 = len v2 ) and A9: for n, m being Element of NAT st [n,m] in Indices G2 holds G2 * (n,m) = |[(v1 . n),(v2 . m)]| ; ::_thesis: G1 = G2 A10: ( Indices G1 = [:(dom G1),(Seg (width G1)):] & Indices G2 = [:(dom G2),(Seg (width G2)):] ) by MATRIX_1:def_4; now__::_thesis:_for_n,_m_being_Nat_st_[n,m]_in_Indices_G1_holds_ G1_*_(n,m)_=_G2_*_(n,m) let n, m be Nat; ::_thesis: ( [n,m] in Indices G1 implies G1 * (n,m) = G2 * (n,m) ) reconsider m9 = m, n9 = n as Element of NAT by ORDINAL1:def_12; A11: ( dom G1 = Seg (len G1) & dom G2 = Seg (len G2) ) by FINSEQ_1:def_3; reconsider r = v1 . n9, s = v2 . m9 as Real ; assume A12: [n,m] in Indices G1 ; ::_thesis: G1 * (n,m) = G2 * (n,m) then G1 * (n,m) = |[r,s]| by A7; hence G1 * (n,m) = G2 * (n,m) by A6, A8, A9, A10, A12, A11; ::_thesis: verum end; hence G1 = G2 by A6, A8, MATRIX_1:21; ::_thesis: verum end; end; :: deftheorem Def1 defines GoB GOBOARD2:def_1_:_ for v1, v2 being FinSequence of REAL st v1 <> {} holds for b3 being Matrix of (TOP-REAL 2) holds ( b3 = GoB (v1,v2) iff ( len b3 = len v1 & width b3 = len v2 & ( for n, m being Element of NAT st [n,m] in Indices b3 holds b3 * (n,m) = |[(v1 . n),(v2 . m)]| ) ) ); registration let v1, v2 be non empty FinSequence of REAL ; cluster GoB (v1,v2) -> V3() X_equal-in-line Y_equal-in-column ; coherence ( not GoB (v1,v2) is empty-yielding & GoB (v1,v2) is X_equal-in-line & GoB (v1,v2) is Y_equal-in-column ) proof set M = GoB (v1,v2); A1: len (GoB (v1,v2)) = len v1 by Def1; then A2: dom (GoB (v1,v2)) = dom v1 by FINSEQ_3:29; A3: width (GoB (v1,v2)) = len v2 by Def1; hence GoB (v1,v2) is V3() by A1, GOBOARD1:def_3; ::_thesis: ( GoB (v1,v2) is X_equal-in-line & GoB (v1,v2) is Y_equal-in-column ) A4: Indices (GoB (v1,v2)) = [:(dom v1),(Seg (len v2)):] by A3, A2, MATRIX_1:def_4; thus GoB (v1,v2) is X_equal-in-line ::_thesis: GoB (v1,v2) is Y_equal-in-column proof let n be Element of NAT ; :: according to GOBOARD1:def_4 ::_thesis: ( not n in dom (GoB (v1,v2)) or X_axis (Line ((GoB (v1,v2)),n)) is constant ) reconsider l = Line ((GoB (v1,v2)),n) as FinSequence of (TOP-REAL 2) ; set x = X_axis l; assume A5: n in dom (GoB (v1,v2)) ; ::_thesis: X_axis (Line ((GoB (v1,v2)),n)) is constant A6: ( len l = width (GoB (v1,v2)) & dom (X_axis l) = Seg (len (X_axis l)) ) by FINSEQ_1:def_3, MATRIX_1:def_7; A7: len (X_axis l) = len l by GOBOARD1:def_1; then A8: dom (X_axis l) = dom l by FINSEQ_3:29; now__::_thesis:_for_i,_j_being_Element_of_NAT_st_i_in_dom_(X_axis_l)_&_j_in_dom_(X_axis_l)_holds_ (X_axis_l)_._i_=_(X_axis_l)_._j let i, j be Element of NAT ; ::_thesis: ( i in dom (X_axis l) & j in dom (X_axis l) implies (X_axis l) . i = (X_axis l) . j ) assume that A9: i in dom (X_axis l) and A10: j in dom (X_axis l) ; ::_thesis: (X_axis l) . i = (X_axis l) . j reconsider r = v1 . n, s1 = v2 . i, s2 = v2 . j as Real ; [n,i] in Indices (GoB (v1,v2)) by A3, A2, A4, A5, A7, A6, A9, ZFMISC_1:87; then (GoB (v1,v2)) * (n,i) = |[r,s1]| by Def1; then A11: ((GoB (v1,v2)) * (n,i)) `1 = r by EUCLID:52; l /. i = l . i by A8, A9, PARTFUN1:def_6; then l /. i = (GoB (v1,v2)) * (n,i) by A7, A6, A9, MATRIX_1:def_7; then A12: (X_axis l) . i = r by A9, A11, GOBOARD1:def_1; [n,j] in Indices (GoB (v1,v2)) by A3, A2, A4, A5, A7, A6, A10, ZFMISC_1:87; then (GoB (v1,v2)) * (n,j) = |[r,s2]| by Def1; then A13: ((GoB (v1,v2)) * (n,j)) `1 = r by EUCLID:52; l /. j = l . j by A8, A10, PARTFUN1:def_6; then l /. j = (GoB (v1,v2)) * (n,j) by A7, A6, A10, MATRIX_1:def_7; hence (X_axis l) . i = (X_axis l) . j by A10, A13, A12, GOBOARD1:def_1; ::_thesis: verum end; hence X_axis (Line ((GoB (v1,v2)),n)) is constant by SEQM_3:def_10; ::_thesis: verum end; thus GoB (v1,v2) is Y_equal-in-column ::_thesis: verum proof let n be Element of NAT ; :: according to GOBOARD1:def_5 ::_thesis: ( not n in Seg (width (GoB (v1,v2))) or Y_axis (Col ((GoB (v1,v2)),n)) is constant ) reconsider c = Col ((GoB (v1,v2)),n) as FinSequence of (TOP-REAL 2) ; set y = Y_axis c; len (Y_axis c) = len c by GOBOARD1:def_2; then A14: dom (Y_axis c) = dom c by FINSEQ_3:29; len c = len (GoB (v1,v2)) by MATRIX_1:def_8; then A15: dom c = dom (GoB (v1,v2)) by FINSEQ_3:29; assume A16: n in Seg (width (GoB (v1,v2))) ; ::_thesis: Y_axis (Col ((GoB (v1,v2)),n)) is constant now__::_thesis:_for_i,_j_being_Element_of_NAT_st_i_in_dom_(Y_axis_c)_&_j_in_dom_(Y_axis_c)_holds_ (Y_axis_c)_._i_=_(Y_axis_c)_._j let i, j be Element of NAT ; ::_thesis: ( i in dom (Y_axis c) & j in dom (Y_axis c) implies (Y_axis c) . i = (Y_axis c) . j ) assume that A17: i in dom (Y_axis c) and A18: j in dom (Y_axis c) ; ::_thesis: (Y_axis c) . i = (Y_axis c) . j reconsider r = v2 . n, s1 = v1 . i, s2 = v1 . j as Real ; [i,n] in Indices (GoB (v1,v2)) by A3, A2, A4, A16, A14, A15, A17, ZFMISC_1:87; then (GoB (v1,v2)) * (i,n) = |[s1,r]| by Def1; then A19: ((GoB (v1,v2)) * (i,n)) `2 = r by EUCLID:52; c /. i = c . i by A14, A17, PARTFUN1:def_6; then c /. i = (GoB (v1,v2)) * (i,n) by A14, A15, A17, MATRIX_1:def_8; then A20: (Y_axis c) . i = r by A17, A19, GOBOARD1:def_2; [j,n] in Indices (GoB (v1,v2)) by A3, A2, A4, A16, A14, A15, A18, ZFMISC_1:87; then (GoB (v1,v2)) * (j,n) = |[s2,r]| by Def1; then A21: ((GoB (v1,v2)) * (j,n)) `2 = r by EUCLID:52; c /. j = c . j by A14, A18, PARTFUN1:def_6; then c /. j = (GoB (v1,v2)) * (j,n) by A14, A15, A18, MATRIX_1:def_8; hence (Y_axis c) . i = (Y_axis c) . j by A18, A21, A20, GOBOARD1:def_2; ::_thesis: verum end; hence Y_axis (Col ((GoB (v1,v2)),n)) is constant by SEQM_3:def_10; ::_thesis: verum end; end; end; registration let v1, v2 be non empty increasing FinSequence of REAL ; cluster GoB (v1,v2) -> Y_increasing-in-line X_increasing-in-column ; coherence ( GoB (v1,v2) is Y_increasing-in-line & GoB (v1,v2) is X_increasing-in-column ) proof set M = GoB (v1,v2); A1: width (GoB (v1,v2)) = len v2 by Def1; A2: len (GoB (v1,v2)) = len v1 by Def1; then A3: dom (GoB (v1,v2)) = dom v1 by FINSEQ_3:29; then A4: Indices (GoB (v1,v2)) = [:(dom v1),(Seg (len v2)):] by A1, MATRIX_1:def_4; A5: dom v2 = Seg (len v2) by FINSEQ_1:def_3; thus GoB (v1,v2) is Y_increasing-in-line ::_thesis: GoB (v1,v2) is X_increasing-in-column proof let n be Element of NAT ; :: according to GOBOARD1:def_6 ::_thesis: ( not n in dom (GoB (v1,v2)) or Y_axis (Line ((GoB (v1,v2)),n)) is increasing ) reconsider l = Line ((GoB (v1,v2)),n) as FinSequence of (TOP-REAL 2) ; set y = Y_axis l; assume A6: n in dom (GoB (v1,v2)) ; ::_thesis: Y_axis (Line ((GoB (v1,v2)),n)) is increasing A7: ( len l = width (GoB (v1,v2)) & dom (Y_axis l) = Seg (len (Y_axis l)) ) by FINSEQ_1:def_3, MATRIX_1:def_7; A8: len (Y_axis l) = len l by GOBOARD1:def_2; then A9: dom (Y_axis l) = dom l by FINSEQ_3:29; now__::_thesis:_for_i,_j_being_Element_of_NAT_st_i_in_dom_(Y_axis_l)_&_j_in_dom_(Y_axis_l)_&_i_<_j_holds_ (Y_axis_l)_._i_<_(Y_axis_l)_._j let i, j be Element of NAT ; ::_thesis: ( i in dom (Y_axis l) & j in dom (Y_axis l) & i < j implies (Y_axis l) . i < (Y_axis l) . j ) assume that A10: i in dom (Y_axis l) and A11: j in dom (Y_axis l) and A12: i < j ; ::_thesis: (Y_axis l) . i < (Y_axis l) . j reconsider r = v1 . n, s1 = v2 . i, s2 = v2 . j as Real ; [n,j] in Indices (GoB (v1,v2)) by A1, A3, A4, A6, A8, A7, A11, ZFMISC_1:87; then (GoB (v1,v2)) * (n,j) = |[r,s2]| by Def1; then A13: ((GoB (v1,v2)) * (n,j)) `2 = s2 by EUCLID:52; l /. j = l . j by A9, A11, PARTFUN1:def_6; then l /. j = (GoB (v1,v2)) * (n,j) by A8, A7, A11, MATRIX_1:def_7; then A14: (Y_axis l) . j = s2 by A11, A13, GOBOARD1:def_2; [n,i] in Indices (GoB (v1,v2)) by A1, A3, A4, A6, A8, A7, A10, ZFMISC_1:87; then (GoB (v1,v2)) * (n,i) = |[r,s1]| by Def1; then A15: ((GoB (v1,v2)) * (n,i)) `2 = s1 by EUCLID:52; l /. i = l . i by A9, A10, PARTFUN1:def_6; then l /. i = (GoB (v1,v2)) * (n,i) by A8, A7, A10, MATRIX_1:def_7; then (Y_axis l) . i = s1 by A10, A15, GOBOARD1:def_2; hence (Y_axis l) . i < (Y_axis l) . j by A5, A1, A8, A7, A10, A11, A12, A14, SEQM_3:def_1; ::_thesis: verum end; hence Y_axis (Line ((GoB (v1,v2)),n)) is increasing by SEQM_3:def_1; ::_thesis: verum end; A16: dom v1 = Seg (len v1) by FINSEQ_1:def_3; thus GoB (v1,v2) is X_increasing-in-column ::_thesis: verum proof let n be Element of NAT ; :: according to GOBOARD1:def_7 ::_thesis: ( not n in Seg (width (GoB (v1,v2))) or X_axis (Col ((GoB (v1,v2)),n)) is increasing ) reconsider c = Col ((GoB (v1,v2)),n) as FinSequence of (TOP-REAL 2) ; set x = X_axis c; assume A17: n in Seg (width (GoB (v1,v2))) ; ::_thesis: X_axis (Col ((GoB (v1,v2)),n)) is increasing A18: len (X_axis c) = len c by GOBOARD1:def_1; then A19: dom (X_axis c) = dom c by FINSEQ_3:29; A20: len c = len (GoB (v1,v2)) by MATRIX_1:def_8; then A21: dom c = dom (GoB (v1,v2)) by FINSEQ_3:29; A22: dom (X_axis c) = Seg (len (X_axis c)) by FINSEQ_1:def_3; now__::_thesis:_for_i,_j_being_Element_of_NAT_st_i_in_dom_(X_axis_c)_&_j_in_dom_(X_axis_c)_&_i_<_j_holds_ (X_axis_c)_._i_<_(X_axis_c)_._j let i, j be Element of NAT ; ::_thesis: ( i in dom (X_axis c) & j in dom (X_axis c) & i < j implies (X_axis c) . i < (X_axis c) . j ) assume that A23: i in dom (X_axis c) and A24: j in dom (X_axis c) and A25: i < j ; ::_thesis: (X_axis c) . i < (X_axis c) . j reconsider r = v2 . n, s1 = v1 . i, s2 = v1 . j as Real ; [j,n] in Indices (GoB (v1,v2)) by A1, A3, A4, A17, A19, A21, A24, ZFMISC_1:87; then (GoB (v1,v2)) * (j,n) = |[s2,r]| by Def1; then A26: ((GoB (v1,v2)) * (j,n)) `1 = s2 by EUCLID:52; c /. j = c . j by A19, A24, PARTFUN1:def_6; then c /. j = (GoB (v1,v2)) * (j,n) by A19, A21, A24, MATRIX_1:def_8; then A27: (X_axis c) . j = s2 by A24, A26, GOBOARD1:def_1; [i,n] in Indices (GoB (v1,v2)) by A1, A3, A4, A17, A19, A21, A23, ZFMISC_1:87; then (GoB (v1,v2)) * (i,n) = |[s1,r]| by Def1; then A28: ((GoB (v1,v2)) * (i,n)) `1 = s1 by EUCLID:52; c /. i = c . i by A19, A23, PARTFUN1:def_6; then c /. i = (GoB (v1,v2)) * (i,n) by A19, A21, A23, MATRIX_1:def_8; then (X_axis c) . i = s1 by A23, A28, GOBOARD1:def_1; hence (X_axis c) . i < (X_axis c) . j by A16, A2, A18, A20, A22, A23, A24, A25, A27, SEQM_3:def_1; ::_thesis: verum end; hence X_axis (Col ((GoB (v1,v2)),n)) is increasing by SEQM_3:def_1; ::_thesis: verum end; end; end; definition let f be non empty FinSequence of (TOP-REAL 2); func GoB f -> Matrix of (TOP-REAL 2) equals :: GOBOARD2:def 2 GoB ((Incr (X_axis f)),(Incr (Y_axis f))); correctness coherence GoB ((Incr (X_axis f)),(Incr (Y_axis f))) is Matrix of (TOP-REAL 2); ; end; :: deftheorem defines GoB GOBOARD2:def_2_:_ for f being non empty FinSequence of (TOP-REAL 2) holds GoB f = GoB ((Incr (X_axis f)),(Incr (Y_axis f))); registration let f be non empty FinSequence of (TOP-REAL 2); cluster GoB f -> V3() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ; coherence ( not GoB f is empty-yielding & GoB f is X_equal-in-line & GoB f is Y_equal-in-column & GoB f is Y_increasing-in-line & GoB f is X_increasing-in-column ) ; end; theorem Th13: :: GOBOARD2:13 for f being non empty FinSequence of (TOP-REAL 2) holds ( len (GoB f) = card (rng (X_axis f)) & width (GoB f) = card (rng (Y_axis f)) ) proof let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: ( len (GoB f) = card (rng (X_axis f)) & width (GoB f) = card (rng (Y_axis f)) ) set x = X_axis f; set y = Y_axis f; ( len (Incr (X_axis f)) = card (rng (X_axis f)) & len (Incr (Y_axis f)) = card (rng (Y_axis f)) ) by SEQ_4:def_21; hence ( len (GoB f) = card (rng (X_axis f)) & width (GoB f) = card (rng (Y_axis f)) ) by Def1; ::_thesis: verum end; theorem :: GOBOARD2:14 for f being non empty FinSequence of (TOP-REAL 2) for n being Element of NAT st n in dom f holds ex i, j being Element of NAT st ( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) ) proof let f be non empty FinSequence of (TOP-REAL 2); ::_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 (GoB f) & f /. n = (GoB f) * (i,j) ) set x = X_axis f; set y = Y_axis f; let n be Element of NAT ; ::_thesis: ( n in dom f implies ex i, j being Element of NAT st ( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) ) ) assume A1: n in dom f ; ::_thesis: ex i, j being Element of NAT st ( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) ) A2: rng (Incr (Y_axis f)) = rng (Y_axis f) by SEQ_4:def_21; reconsider p = f /. n as Point of (TOP-REAL 2) ; A3: dom f = Seg (len f) by FINSEQ_1:def_3; ( dom (Y_axis f) = Seg (len (Y_axis f)) & len (Y_axis f) = len f ) by FINSEQ_1:def_3, GOBOARD1:def_2; then ( (Y_axis f) . n = p `2 & (Y_axis f) . n in rng (Y_axis f) ) by A1, A3, FUNCT_1:def_3, GOBOARD1:def_2; then consider j being Nat such that A4: j in dom (Incr (Y_axis f)) and A5: (Incr (Y_axis f)) . j = p `2 by A2, FINSEQ_2:10; A6: rng (Incr (X_axis f)) = rng (X_axis f) by SEQ_4:def_21; ( dom (X_axis f) = Seg (len (X_axis f)) & len (X_axis f) = len f ) by FINSEQ_1:def_3, GOBOARD1:def_1; then ( (X_axis f) . n = p `1 & (X_axis f) . n in rng (X_axis f) ) by A1, A3, FUNCT_1:def_3, GOBOARD1:def_1; then consider i being Nat such that A7: i in dom (Incr (X_axis f)) and A8: (Incr (X_axis f)) . i = p `1 by A6, FINSEQ_2:10; ( width (GoB f) = card (rng (Y_axis f)) & len (Incr (Y_axis f)) = card (rng (Y_axis f)) ) by Th13, SEQ_4:def_21; then A9: Seg (width (GoB f)) = dom (Incr (Y_axis f)) by FINSEQ_1:def_3; reconsider i = i, j = j as Element of NAT by ORDINAL1:def_12; take i ; ::_thesis: ex j being Element of NAT st ( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) ) take j ; ::_thesis: ( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) ) ( len (GoB f) = card (rng (X_axis f)) & len (Incr (X_axis f)) = card (rng (X_axis f)) ) by Th13, SEQ_4:def_21; then ( Indices (GoB f) = [:(dom (GoB f)),(Seg (width (GoB f))):] & dom (GoB f) = dom (Incr (X_axis f)) ) by FINSEQ_3:29, MATRIX_1:def_4; hence [i,j] in Indices (GoB f) by A7, A4, A9, ZFMISC_1:87; ::_thesis: f /. n = (GoB f) * (i,j) then (GoB f) * (i,j) = |[(p `1),(p `2)]| by A8, A5, Def1; hence f /. n = (GoB f) * (i,j) by EUCLID:53; ::_thesis: verum end; theorem :: GOBOARD2:15 for n being Element of NAT for f being non empty FinSequence of (TOP-REAL 2) st n in dom f & ( for m being Element of NAT st m in dom f holds (X_axis f) . n <= (X_axis f) . m ) holds f /. n in rng (Line ((GoB f),1)) proof let n be Element of NAT ; ::_thesis: for f being non empty FinSequence of (TOP-REAL 2) st n in dom f & ( for m being Element of NAT st m in dom f holds (X_axis f) . n <= (X_axis f) . m ) holds f /. n in rng (Line ((GoB f),1)) let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: ( n in dom f & ( for m being Element of NAT st m in dom f holds (X_axis f) . n <= (X_axis f) . m ) implies f /. n in rng (Line ((GoB f),1)) ) set x = X_axis f; set y = Y_axis f; set r = (X_axis f) . n; assume that A1: n in dom f and A2: for m being Element of NAT st m in dom f holds (X_axis f) . n <= (X_axis f) . m ; ::_thesis: f /. n in rng (Line ((GoB f),1)) reconsider p = f /. n as Point of (TOP-REAL 2) ; A3: dom f = Seg (len f) by FINSEQ_1:def_3; A4: ( dom (X_axis f) = Seg (len (X_axis f)) & len (X_axis f) = len f ) by FINSEQ_1:def_3, GOBOARD1:def_1; then A5: (X_axis f) . n = p `1 by A1, A3, GOBOARD1:def_1; A6: rng (Incr (X_axis f)) = rng (X_axis f) by SEQ_4:def_21; (X_axis f) . n in rng (X_axis f) by A1, A3, A4, FUNCT_1:def_3; then consider i being Nat such that A7: i in dom (Incr (X_axis f)) and A8: (Incr (X_axis f)) . i = p `1 by A5, A6, FINSEQ_2:10; reconsider i = i as Element of NAT by ORDINAL1:def_12; A9: 1 <= i by A7, FINSEQ_3:25; then reconsider i1 = i - 1 as Element of NAT by INT_1:5; A10: i <= len (Incr (X_axis f)) by A7, FINSEQ_3:25; A11: now__::_thesis:_not_i_<>_1 reconsider s = (Incr (X_axis f)) . i1 as Real ; assume i <> 1 ; ::_thesis: contradiction then 1 < i by A9, XXREAL_0:1; then 1 + 1 <= i by NAT_1:13; then A12: 1 <= i1 by XREAL_1:19; i1 <= i by XREAL_1:44; then i1 <= len (Incr (X_axis f)) by A10, XXREAL_0:2; then A13: i1 in dom (Incr (X_axis f)) by A12, FINSEQ_3:25; then (Incr (X_axis f)) . i1 in rng (Incr (X_axis f)) by FUNCT_1:def_3; then A14: ex m being Nat st ( m in dom (X_axis f) & (X_axis f) . m = s ) by A6, FINSEQ_2:10; i1 < i by XREAL_1:44; then s < (X_axis f) . n by A5, A7, A8, A13, SEQM_3:def_1; hence contradiction by A2, A3, A4, A14; ::_thesis: verum end; A15: rng (Incr (Y_axis f)) = rng (Y_axis f) by SEQ_4:def_21; ( dom (Y_axis f) = Seg (len (Y_axis f)) & len (Y_axis f) = len f ) by FINSEQ_1:def_3, GOBOARD1:def_2; then ( (Y_axis f) . n = p `2 & (Y_axis f) . n in rng (Y_axis f) ) by A1, A3, FUNCT_1:def_3, GOBOARD1:def_2; then consider j being Nat such that A16: j in dom (Incr (Y_axis f)) and A17: (Incr (Y_axis f)) . j = p `2 by A15, FINSEQ_2:10; A18: p = |[(p `1),(p `2)]| by EUCLID:53; len (Line ((GoB f),1)) = width (GoB f) by MATRIX_1:def_7; then A19: dom (Line ((GoB f),1)) = Seg (width (GoB f)) by FINSEQ_1:def_3; ( width (GoB f) = card (rng (Y_axis f)) & len (Incr (Y_axis f)) = card (rng (Y_axis f)) ) by Th13, SEQ_4:def_21; then A20: dom (Incr (Y_axis f)) = Seg (width (GoB f)) by FINSEQ_1:def_3; ( len (GoB f) = card (rng (X_axis f)) & len (Incr (X_axis f)) = card (rng (X_axis f)) ) by Th13, SEQ_4:def_21; then ( Indices (GoB f) = [:(dom (GoB f)),(Seg (width (GoB f))):] & dom (Incr (X_axis f)) = dom (GoB f) ) by FINSEQ_3:29, MATRIX_1:def_4; then [1,j] in Indices (GoB f) by A7, A16, A20, A11, ZFMISC_1:87; then (GoB f) * (1,j) = |[(p `1),(p `2)]| by A8, A16, A17, A11, Def1; then (Line ((GoB f),1)) . j = f /. n by A16, A20, A18, MATRIX_1:def_7; hence f /. n in rng (Line ((GoB f),1)) by A16, A20, A19, FUNCT_1:def_3; ::_thesis: verum end; theorem :: GOBOARD2:16 for n being Element of NAT for f being non empty FinSequence of (TOP-REAL 2) st n in dom f & ( for m being Element of NAT st m in dom f holds (X_axis f) . m <= (X_axis f) . n ) holds f /. n in rng (Line ((GoB f),(len (GoB f)))) proof let n be Element of NAT ; ::_thesis: for f being non empty FinSequence of (TOP-REAL 2) st n in dom f & ( for m being Element of NAT st m in dom f holds (X_axis f) . m <= (X_axis f) . n ) holds f /. n in rng (Line ((GoB f),(len (GoB f)))) let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: ( n in dom f & ( for m being Element of NAT st m in dom f holds (X_axis f) . m <= (X_axis f) . n ) implies f /. n in rng (Line ((GoB f),(len (GoB f)))) ) set x = X_axis f; set y = Y_axis f; set r = (X_axis f) . n; assume that A1: n in dom f and A2: for m being Element of NAT st m in dom f holds (X_axis f) . m <= (X_axis f) . n ; ::_thesis: f /. n in rng (Line ((GoB f),(len (GoB f)))) reconsider p = f /. n as Point of (TOP-REAL 2) ; A3: dom f = Seg (len f) by FINSEQ_1:def_3; A4: ( dom (X_axis f) = Seg (len (X_axis f)) & len (X_axis f) = len f ) by FINSEQ_1:def_3, GOBOARD1:def_1; then A5: (X_axis f) . n = p `1 by A1, A3, GOBOARD1:def_1; A6: rng (Incr (X_axis f)) = rng (X_axis f) by SEQ_4:def_21; (X_axis f) . n in rng (X_axis f) by A1, A3, A4, FUNCT_1:def_3; then consider i being Nat such that A7: i in dom (Incr (X_axis f)) and A8: (Incr (X_axis f)) . i = p `1 by A5, A6, FINSEQ_2:10; reconsider i = i as Element of NAT by ORDINAL1:def_12; A9: i <= len (Incr (X_axis f)) by A7, FINSEQ_3:25; A10: 1 <= i by A7, FINSEQ_3:25; A11: now__::_thesis:_not_i_<>_len_(Incr_(X_axis_f)) reconsider s = (Incr (X_axis f)) . (i + 1) as Real ; assume i <> len (Incr (X_axis f)) ; ::_thesis: contradiction then i < len (Incr (X_axis f)) by A9, XXREAL_0:1; then A12: i + 1 <= len (Incr (X_axis f)) by NAT_1:13; 1 <= i + 1 by A10, NAT_1:13; then A13: i + 1 in dom (Incr (X_axis f)) by A12, FINSEQ_3:25; then (Incr (X_axis f)) . (i + 1) in rng (Incr (X_axis f)) by FUNCT_1:def_3; then A14: ex m being Nat st ( m in dom (X_axis f) & (X_axis f) . m = s ) by A6, FINSEQ_2:10; i < i + 1 by NAT_1:13; then (X_axis f) . n < s by A5, A7, A8, A13, SEQM_3:def_1; hence contradiction by A2, A3, A4, A14; ::_thesis: verum end; A15: rng (Incr (Y_axis f)) = rng (Y_axis f) by SEQ_4:def_21; ( dom (Y_axis f) = Seg (len (Y_axis f)) & len (Y_axis f) = len f ) by FINSEQ_1:def_3, GOBOARD1:def_2; then ( (Y_axis f) . n = p `2 & (Y_axis f) . n in rng (Y_axis f) ) by A1, A3, FUNCT_1:def_3, GOBOARD1:def_2; then consider j being Nat such that A16: j in dom (Incr (Y_axis f)) and A17: (Incr (Y_axis f)) . j = p `2 by A15, FINSEQ_2:10; A18: p = |[(p `1),(p `2)]| by EUCLID:53; len (Line ((GoB f),(len (GoB f)))) = width (GoB f) by MATRIX_1:def_7; then A19: dom (Line ((GoB f),(len (GoB f)))) = Seg (width (GoB f)) by FINSEQ_1:def_3; ( width (GoB f) = card (rng (Y_axis f)) & len (Incr (Y_axis f)) = card (rng (Y_axis f)) ) by Th13, SEQ_4:def_21; then A20: dom (Incr (Y_axis f)) = Seg (width (GoB f)) by FINSEQ_1:def_3; A21: ( len (GoB f) = card (rng (X_axis f)) & len (Incr (X_axis f)) = card (rng (X_axis f)) ) by Th13, SEQ_4:def_21; then ( Indices (GoB f) = [:(dom (GoB f)),(Seg (width (GoB f))):] & dom (Incr (X_axis f)) = dom (GoB f) ) by FINSEQ_3:29, MATRIX_1:def_4; then [(len (GoB f)),j] in Indices (GoB f) by A21, A7, A16, A20, A11, ZFMISC_1:87; then (GoB f) * ((len (GoB f)),j) = |[(p `1),(p `2)]| by A21, A8, A16, A17, A11, Def1; then (Line ((GoB f),(len (GoB f)))) . j = f /. n by A16, A20, A18, MATRIX_1:def_7; hence f /. n in rng (Line ((GoB f),(len (GoB f)))) by A16, A20, A19, FUNCT_1:def_3; ::_thesis: verum end; theorem :: GOBOARD2:17 for n being Element of NAT for f being non empty FinSequence of (TOP-REAL 2) st n in dom f & ( for m being Element of NAT st m in dom f holds (Y_axis f) . n <= (Y_axis f) . m ) holds f /. n in rng (Col ((GoB f),1)) proof let n be Element of NAT ; ::_thesis: for f being non empty FinSequence of (TOP-REAL 2) st n in dom f & ( for m being Element of NAT st m in dom f holds (Y_axis f) . n <= (Y_axis f) . m ) holds f /. n in rng (Col ((GoB f),1)) let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: ( n in dom f & ( for m being Element of NAT st m in dom f holds (Y_axis f) . n <= (Y_axis f) . m ) implies f /. n in rng (Col ((GoB f),1)) ) set x = X_axis f; set y = Y_axis f; set r = (Y_axis f) . n; assume that A1: n in dom f and A2: for m being Element of NAT st m in dom f holds (Y_axis f) . n <= (Y_axis f) . m ; ::_thesis: f /. n in rng (Col ((GoB f),1)) reconsider p = f /. n as Point of (TOP-REAL 2) ; A3: dom f = Seg (len f) by FINSEQ_1:def_3; A4: ( dom (Y_axis f) = Seg (len (Y_axis f)) & len (Y_axis f) = len f ) by FINSEQ_1:def_3, GOBOARD1:def_2; then A5: (Y_axis f) . n = p `2 by A1, A3, GOBOARD1:def_2; A6: rng (Incr (Y_axis f)) = rng (Y_axis f) by SEQ_4:def_21; (Y_axis f) . n in rng (Y_axis f) by A1, A3, A4, FUNCT_1:def_3; then consider j being Nat such that A7: j in dom (Incr (Y_axis f)) and A8: (Incr (Y_axis f)) . j = p `2 by A5, A6, FINSEQ_2:10; reconsider j = j as Element of NAT by ORDINAL1:def_12; A9: 1 <= j by A7, FINSEQ_3:25; then reconsider j1 = j - 1 as Element of NAT by INT_1:5; A10: j <= len (Incr (Y_axis f)) by A7, FINSEQ_3:25; A11: now__::_thesis:_not_j_<>_1 reconsider s = (Incr (Y_axis f)) . j1 as Real ; assume j <> 1 ; ::_thesis: contradiction then 1 < j by A9, XXREAL_0:1; then 1 + 1 <= j by NAT_1:13; then A12: 1 <= j1 by XREAL_1:19; j1 <= j by XREAL_1:44; then j1 <= len (Incr (Y_axis f)) by A10, XXREAL_0:2; then A13: j1 in dom (Incr (Y_axis f)) by A12, FINSEQ_3:25; then (Incr (Y_axis f)) . j1 in rng (Incr (Y_axis f)) by FUNCT_1:def_3; then A14: ex m being Nat st ( m in dom (Y_axis f) & (Y_axis f) . m = s ) by A6, FINSEQ_2:10; j1 < j by XREAL_1:44; then s < (Y_axis f) . n by A5, A7, A8, A13, SEQM_3:def_1; hence contradiction by A2, A3, A4, A14; ::_thesis: verum end; A15: rng (Incr (X_axis f)) = rng (X_axis f) by SEQ_4:def_21; ( dom (X_axis f) = Seg (len (X_axis f)) & len (X_axis f) = len f ) by FINSEQ_1:def_3, GOBOARD1:def_1; then ( (X_axis f) . n = p `1 & (X_axis f) . n in rng (X_axis f) ) by A1, A3, FUNCT_1:def_3, GOBOARD1:def_1; then consider i being Nat such that A16: i in dom (Incr (X_axis f)) and A17: (Incr (X_axis f)) . i = p `1 by A15, FINSEQ_2:10; A18: p = |[(p `1),(p `2)]| by EUCLID:53; len (Col ((GoB f),1)) = len (GoB f) by MATRIX_1:def_8; then A19: dom (Col ((GoB f),1)) = dom (GoB f) by FINSEQ_3:29; ( len (GoB f) = card (rng (X_axis f)) & len (Incr (X_axis f)) = card (rng (X_axis f)) ) by Th13, SEQ_4:def_21; then A20: dom (Incr (X_axis f)) = dom (GoB f) by FINSEQ_3:29; ( width (GoB f) = card (rng (Y_axis f)) & len (Incr (Y_axis f)) = card (rng (Y_axis f)) ) by Th13, SEQ_4:def_21; then ( Indices (GoB f) = [:(dom (GoB f)),(Seg (width (GoB f))):] & dom (Incr (Y_axis f)) = Seg (width (GoB f)) ) by FINSEQ_1:def_3, MATRIX_1:def_4; then [i,1] in Indices (GoB f) by A16, A7, A20, A11, ZFMISC_1:87; then (GoB f) * (i,1) = |[(p `1),(p `2)]| by A16, A17, A8, A11, Def1; then (Col ((GoB f),1)) . i = f /. n by A16, A20, A18, MATRIX_1:def_8; hence f /. n in rng (Col ((GoB f),1)) by A16, A20, A19, FUNCT_1:def_3; ::_thesis: verum end; theorem :: GOBOARD2:18 for n being Element of NAT for f being non empty FinSequence of (TOP-REAL 2) st n in dom f & ( for m being Element of NAT st m in dom f holds (Y_axis f) . m <= (Y_axis f) . n ) holds f /. n in rng (Col ((GoB f),(width (GoB f)))) proof let n be Element of NAT ; ::_thesis: for f being non empty FinSequence of (TOP-REAL 2) st n in dom f & ( for m being Element of NAT st m in dom f holds (Y_axis f) . m <= (Y_axis f) . n ) holds f /. n in rng (Col ((GoB f),(width (GoB f)))) let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: ( n in dom f & ( for m being Element of NAT st m in dom f holds (Y_axis f) . m <= (Y_axis f) . n ) implies f /. n in rng (Col ((GoB f),(width (GoB f)))) ) set x = X_axis f; set y = Y_axis f; set r = (Y_axis f) . n; assume that A1: n in dom f and A2: for m being Element of NAT st m in dom f holds (Y_axis f) . m <= (Y_axis f) . n ; ::_thesis: f /. n in rng (Col ((GoB f),(width (GoB f)))) reconsider p = f /. n as Point of (TOP-REAL 2) ; A3: dom f = Seg (len f) by FINSEQ_1:def_3; A4: ( dom (Y_axis f) = Seg (len (Y_axis f)) & len (Y_axis f) = len f ) by FINSEQ_1:def_3, GOBOARD1:def_2; then A5: (Y_axis f) . n = p `2 by A1, A3, GOBOARD1:def_2; A6: rng (Incr (Y_axis f)) = rng (Y_axis f) by SEQ_4:def_21; (Y_axis f) . n in rng (Y_axis f) by A1, A3, A4, FUNCT_1:def_3; then consider j being Nat such that A7: j in dom (Incr (Y_axis f)) and A8: (Incr (Y_axis f)) . j = p `2 by A5, A6, FINSEQ_2:10; reconsider j = j as Element of NAT by ORDINAL1:def_12; A9: j <= len (Incr (Y_axis f)) by A7, FINSEQ_3:25; A10: 1 <= j by A7, FINSEQ_3:25; A11: now__::_thesis:_not_j_<>_len_(Incr_(Y_axis_f)) reconsider s = (Incr (Y_axis f)) . (j + 1) as Real ; assume j <> len (Incr (Y_axis f)) ; ::_thesis: contradiction then j < len (Incr (Y_axis f)) by A9, XXREAL_0:1; then A12: j + 1 <= len (Incr (Y_axis f)) by NAT_1:13; 1 <= j + 1 by A10, NAT_1:13; then A13: j + 1 in dom (Incr (Y_axis f)) by A12, FINSEQ_3:25; then (Incr (Y_axis f)) . (j + 1) in rng (Incr (Y_axis f)) by FUNCT_1:def_3; then A14: ex m being Nat st ( m in dom (Y_axis f) & (Y_axis f) . m = s ) by A6, FINSEQ_2:10; j < j + 1 by NAT_1:13; then (Y_axis f) . n < s by A5, A7, A8, A13, SEQM_3:def_1; hence contradiction by A2, A3, A4, A14; ::_thesis: verum end; A15: rng (Incr (X_axis f)) = rng (X_axis f) by SEQ_4:def_21; ( dom (X_axis f) = Seg (len (X_axis f)) & len (X_axis f) = len f ) by FINSEQ_1:def_3, GOBOARD1:def_1; then ( (X_axis f) . n = p `1 & (X_axis f) . n in rng (X_axis f) ) by A1, A3, FUNCT_1:def_3, GOBOARD1:def_1; then consider i being Nat such that A16: i in dom (Incr (X_axis f)) and A17: (Incr (X_axis f)) . i = p `1 by A15, FINSEQ_2:10; A18: p = |[(p `1),(p `2)]| by EUCLID:53; len (Col ((GoB f),(width (GoB f)))) = len (GoB f) by MATRIX_1:def_8; then A19: dom (Col ((GoB f),(width (GoB f)))) = dom (GoB f) by FINSEQ_3:29; ( len (GoB f) = card (rng (X_axis f)) & len (Incr (X_axis f)) = card (rng (X_axis f)) ) by Th13, SEQ_4:def_21; then A20: dom (Incr (X_axis f)) = dom (GoB f) by FINSEQ_3:29; A21: ( width (GoB f) = card (rng (Y_axis f)) & len (Incr (Y_axis f)) = card (rng (Y_axis f)) ) by Th13, SEQ_4:def_21; then ( Indices (GoB f) = [:(dom (GoB f)),(Seg (width (GoB f))):] & dom (Incr (Y_axis f)) = Seg (width (GoB f)) ) by FINSEQ_1:def_3, MATRIX_1:def_4; then [i,(width (GoB f))] in Indices (GoB f) by A21, A16, A7, A20, A11, ZFMISC_1:87; then (GoB f) * (i,(width (GoB f))) = |[(p `1),(p `2)]| by A21, A16, A17, A8, A11, Def1; then (Col ((GoB f),(width (GoB f)))) . i = f /. n by A16, A20, A18, MATRIX_1:def_8; hence f /. n in rng (Col ((GoB f),(width (GoB f)))) by A16, A20, A19, FUNCT_1:def_3; ::_thesis: verum end;