:: TOPREAL8 semantic presentation begin theorem Th1: :: TOPREAL8:1 for A, x, y being set st A c= {x,y} & x in A & not y in A holds A = {x} proof let A, x, y be set ; ::_thesis: ( A c= {x,y} & x in A & not y in A implies A = {x} ) assume that A1: A c= {x,y} and A2: x in A and A3: not y in A ; ::_thesis: A = {x} percases ( A = {} or A = {x} or A = {y} or A = {x,y} ) by A1, ZFMISC_1:36; suppose A = {} ; ::_thesis: A = {x} hence A = {x} by A2; ::_thesis: verum end; suppose A = {x} ; ::_thesis: A = {x} hence A = {x} ; ::_thesis: verum end; suppose A = {y} ; ::_thesis: A = {x} hence A = {x} by A3, TARSKI:def_1; ::_thesis: verum end; suppose A = {x,y} ; ::_thesis: A = {x} hence A = {x} by A3, TARSKI:def_2; ::_thesis: verum end; end; end; registration cluster trivial V16() Function-like for set ; existence ex b1 being Function st b1 is trivial proof take {} ; ::_thesis: {} is trivial thus {} is trivial ; ::_thesis: verum end; end; begin registration clusterV16() V19( NAT ) Function-like non constant V29() FinSequence-like FinSubsequence-like for set ; existence not for b1 being FinSequence holds b1 is constant proof set f = the non constant FinSequence; take the non constant FinSequence ; ::_thesis: not the non constant FinSequence is constant thus not the non constant FinSequence is constant ; ::_thesis: verum end; end; theorem Th2: :: TOPREAL8:2 for f being non trivial FinSequence holds 1 < len f proof let f be non trivial FinSequence; ::_thesis: 1 < len f 1 + 1 <= len f by NAT_D:60; hence 1 < len f by NAT_1:13; ::_thesis: verum end; theorem Th3: :: TOPREAL8:3 for D being non trivial set for f being non constant circular FinSequence of D holds len f > 2 proof let D be non trivial set ; ::_thesis: for f being non constant circular FinSequence of D holds len f > 2 let f be non constant circular FinSequence of D; ::_thesis: len f > 2 assume A1: len f <= 2 ; ::_thesis: contradiction percases ( len f < 1 + 1 or len f = 2 ) by A1, XXREAL_0:1; suppose len f < 1 + 1 ; ::_thesis: contradiction then len f <= 1 by NAT_1:13; then reconsider f = f as trivial Function by Th2; f is constant ; hence contradiction ; ::_thesis: verum end; supposeA2: len f = 2 ; ::_thesis: contradiction then A3: dom f = {1,2} by FINSEQ_1:2, FINSEQ_1:def_3; for n, m being Element of NAT st n in dom f & m in dom f holds f . n = f . m proof let n, m be Element of NAT ; ::_thesis: ( n in dom f & m in dom f implies f . n = f . m ) assume that A4: n in dom f and A5: m in dom f ; ::_thesis: f . n = f . m percases ( ( n = 1 & m = 1 ) or ( n = 2 & m = 2 ) or ( n = 1 & m = 2 ) or ( n = 2 & m = 1 ) ) by A3, A4, A5, TARSKI:def_2; suppose ( ( n = 1 & m = 1 ) or ( n = 2 & m = 2 ) ) ; ::_thesis: f . n = f . m hence f . n = f . m ; ::_thesis: verum end; supposethat A6: n = 1 and A7: m = 2 ; ::_thesis: f . n = f . m A8: m in dom f by A3, A7, TARSKI:def_2; n in dom f by A3, A6, TARSKI:def_2; hence f . n = f /. 1 by A6, PARTFUN1:def_6 .= f /. (len f) by FINSEQ_6:def_1 .= f . m by A2, A7, A8, PARTFUN1:def_6 ; ::_thesis: verum end; supposethat A9: n = 2 and A10: m = 1 ; ::_thesis: f . n = f . m A11: n in dom f by A3, A9, TARSKI:def_2; m in dom f by A3, A10, TARSKI:def_2; hence f . m = f /. 1 by A10, PARTFUN1:def_6 .= f /. (len f) by FINSEQ_6:def_1 .= f . n by A2, A9, A11, PARTFUN1:def_6 ; ::_thesis: verum end; end; end; hence contradiction by SEQM_3:def_10; ::_thesis: verum end; end; end; theorem Th4: :: TOPREAL8:4 for f being FinSequence for x being set holds ( x in rng f or x .. f = 0 ) proof let f be FinSequence; ::_thesis: for x being set holds ( x in rng f or x .. f = 0 ) let x be set ; ::_thesis: ( x in rng f or x .. f = 0 ) assume A1: not x in rng f ; ::_thesis: x .. f = 0 A2: now__::_thesis:_not_f_"_{x}_<>_{} assume f " {x} <> {} ; ::_thesis: contradiction then consider y being set such that A3: y in f " {x} by XBOOLE_0:def_1; f . y in {x} by A3, FUNCT_1:def_7; then A4: f . y = x by TARSKI:def_1; y in dom f by A3, FUNCT_1:def_7; hence contradiction by A1, A4, FUNCT_1:3; ::_thesis: verum end; thus x .. f = (Sgm (f " {x})) . 1 by FINSEQ_4:def_4 .= 0 by A2, FINSEQ_3:43 ; ::_thesis: verum end; theorem Th5: :: TOPREAL8:5 for p being set for D being non empty set for f being non empty FinSequence of D for g being FinSequence of D st p .. f = len f holds (f ^ g) |-- p = g proof let p be set ; ::_thesis: for D being non empty set for f being non empty FinSequence of D for g being FinSequence of D st p .. f = len f holds (f ^ g) |-- p = g let D be non empty set ; ::_thesis: for f being non empty FinSequence of D for g being FinSequence of D st p .. f = len f holds (f ^ g) |-- p = g let f be non empty FinSequence of D; ::_thesis: for g being FinSequence of D st p .. f = len f holds (f ^ g) |-- p = g let g be FinSequence of D; ::_thesis: ( p .. f = len f implies (f ^ g) |-- p = g ) assume A1: p .. f = len f ; ::_thesis: (f ^ g) |-- p = g A2: p in rng f by A1, Th4; then A3: p .. (f ^ g) = len f by A1, FINSEQ_6:6; rng f c= rng (f ^ g) by FINSEQ_1:29; hence (f ^ g) |-- p = (f ^ g) /^ (p .. (f ^ g)) by A2, FINSEQ_5:35 .= g by A3, FINSEQ_5:37 ; ::_thesis: verum end; theorem Th6: :: TOPREAL8:6 for D being non empty set for f being non empty one-to-one FinSequence of D holds (f /. (len f)) .. f = len f proof let D be non empty set ; ::_thesis: for f being non empty one-to-one FinSequence of D holds (f /. (len f)) .. f = len f let f be non empty one-to-one FinSequence of D; ::_thesis: (f /. (len f)) .. f = len f A1: len f in dom f by FINSEQ_5:6; A2: for i being Nat st 1 <= i & i < len f holds f . i <> f . (len f) proof let i be Nat; ::_thesis: ( 1 <= i & i < len f implies f . i <> f . (len f) ) assume that A3: 1 <= i and A4: i < len f ; ::_thesis: f . i <> f . (len f) i in dom f by A3, A4, FINSEQ_3:25; hence f . i <> f . (len f) by A1, A4, FUNCT_1:def_4; ::_thesis: verum end; f /. (len f) = f . (len f) by A1, PARTFUN1:def_6; hence (f /. (len f)) .. f = len f by A1, A2, FINSEQ_6:2; ::_thesis: verum end; theorem Th7: :: TOPREAL8:7 for f, g being FinSequence holds len f <= len (f ^' g) proof let f, g be FinSequence; ::_thesis: len f <= len (f ^' g) f ^' g = f ^ ((2,(len g)) -cut g) by GRAPH_2:def_2; then len (f ^' g) = (len f) + (len ((2,(len g)) -cut g)) by FINSEQ_1:22; hence len f <= len (f ^' g) by NAT_1:11; ::_thesis: verum end; theorem Th8: :: TOPREAL8:8 for f, g being FinSequence for x being set st x in rng f holds x .. f = x .. (f ^' g) proof let f, g be FinSequence; ::_thesis: for x being set st x in rng f holds x .. f = x .. (f ^' g) let x be set ; ::_thesis: ( x in rng f implies x .. f = x .. (f ^' g) ) assume A1: x in rng f ; ::_thesis: x .. f = x .. (f ^' g) then A2: f . (x .. f) = x by FINSEQ_4:19; A3: x .. f in dom f by A1, FINSEQ_4:20; then A4: x .. f <= len f by FINSEQ_3:25; A5: for i being Nat st 1 <= i & i < x .. f holds (f ^' g) . i <> x proof let i be Nat; ::_thesis: ( 1 <= i & i < x .. f implies (f ^' g) . i <> x ) assume that A6: 1 <= i and A7: i < x .. f ; ::_thesis: (f ^' g) . i <> x A8: i < len f by A4, A7, XXREAL_0:2; then A9: i in dom f by A6, FINSEQ_3:25; i in NAT by ORDINAL1:def_12; then (f ^' g) . i = f . i by A6, A8, GRAPH_2:14; hence (f ^' g) . i <> x by A7, A9, FINSEQ_4:24; ::_thesis: verum end; len f <= len (f ^' g) by Th7; then A10: dom f c= dom (f ^' g) by FINSEQ_3:30; 1 <= x .. f by A3, FINSEQ_3:25; then (f ^' g) . (x .. f) = x by A2, A4, GRAPH_2:14; hence x .. f = x .. (f ^' g) by A3, A10, A5, FINSEQ_6:2; ::_thesis: verum end; theorem :: TOPREAL8:9 for f being non empty FinSequence for g being FinSequence holds len g <= len (f ^' g) proof let f be non empty FinSequence; ::_thesis: for g being FinSequence holds len g <= len (f ^' g) let g be FinSequence; ::_thesis: len g <= len (f ^' g) percases ( g = {} or g <> {} ) ; suppose g = {} ; ::_thesis: len g <= len (f ^' g) hence len g <= len (f ^' g) ; ::_thesis: verum end; supposeA1: g <> {} ; ::_thesis: len g <= len (f ^' g) A2: len f >= 1 by NAT_1:14; (len (f ^' g)) + 1 = (len f) + (len g) by A1, GRAPH_2:13; then (len (f ^' g)) + 1 >= 1 + (len g) by A2, XREAL_1:6; hence len g <= len (f ^' g) by XREAL_1:6; ::_thesis: verum end; end; end; theorem Th10: :: TOPREAL8:10 for f, g being FinSequence holds rng f c= rng (f ^' g) proof let f, g be FinSequence; ::_thesis: rng f c= rng (f ^' g) f ^' g = f ^ ((2,(len g)) -cut g) by GRAPH_2:def_2; hence rng f c= rng (f ^' g) by FINSEQ_1:29; ::_thesis: verum end; theorem Th11: :: TOPREAL8:11 for D being non empty set for f being non empty FinSequence of D for g being non trivial FinSequence of D st g /. (len g) = f /. 1 holds f ^' g is circular proof let D be non empty set ; ::_thesis: for f being non empty FinSequence of D for g being non trivial FinSequence of D st g /. (len g) = f /. 1 holds f ^' g is circular let f be non empty FinSequence of D; ::_thesis: for g being non trivial FinSequence of D st g /. (len g) = f /. 1 holds f ^' g is circular let g be non trivial FinSequence of D; ::_thesis: ( g /. (len g) = f /. 1 implies f ^' g is circular ) assume g /. (len g) = f /. 1 ; ::_thesis: f ^' g is circular hence (f ^' g) /. 1 = g /. (len g) by GRAPH_2:53 .= (f ^' g) /. (len (f ^' g)) by GRAPH_2:54 ; :: according to FINSEQ_6:def_1 ::_thesis: verum end; theorem Th12: :: TOPREAL8:12 for D being non empty set for M being Matrix of D for f being FinSequence of D for g being non empty FinSequence of D st f /. (len f) = g /. 1 & f is_sequence_on M & g is_sequence_on M holds f ^' g is_sequence_on M proof let D be non empty set ; ::_thesis: for M being Matrix of D for f being FinSequence of D for g being non empty FinSequence of D st f /. (len f) = g /. 1 & f is_sequence_on M & g is_sequence_on M holds f ^' g is_sequence_on M let M be Matrix of D; ::_thesis: for f being FinSequence of D for g being non empty FinSequence of D st f /. (len f) = g /. 1 & f is_sequence_on M & g is_sequence_on M holds f ^' g is_sequence_on M let f be FinSequence of D; ::_thesis: for g being non empty FinSequence of D st f /. (len f) = g /. 1 & f is_sequence_on M & g is_sequence_on M holds f ^' g is_sequence_on M let g be non empty FinSequence of D; ::_thesis: ( f /. (len f) = g /. 1 & f is_sequence_on M & g is_sequence_on M implies f ^' g is_sequence_on M ) assume that A1: f /. (len f) = g /. 1 and A2: f is_sequence_on M and A3: g is_sequence_on M ; ::_thesis: f ^' g is_sequence_on M A4: (len (f ^' g)) + 1 = (len f) + (len g) by GRAPH_2:13; thus for n being Element of NAT st n in dom (f ^' g) holds ex i, j being Element of NAT st ( [i,j] in Indices M & (f ^' g) /. n = M * (i,j) ) :: according to GOBOARD1:def_9 ::_thesis: for b1 being Element of NAT holds ( not b1 in dom (f ^' g) or not b1 + 1 in dom (f ^' g) or for b2, b3, b4, b5 being Element of NAT holds ( not [b2,b3] in Indices M or not [b4,b5] in Indices M or not (f ^' g) /. b1 = M * (b2,b3) or not (f ^' g) /. (b1 + 1) = M * (b4,b5) or K144((b2 - b4)) + K144((b3 - b5)) = 1 ) ) proof let n be Element of NAT ; ::_thesis: ( n in dom (f ^' g) implies ex i, j being Element of NAT st ( [i,j] in Indices M & (f ^' g) /. n = M * (i,j) ) ) assume A5: n in dom (f ^' g) ; ::_thesis: ex i, j being Element of NAT st ( [i,j] in Indices M & (f ^' g) /. n = M * (i,j) ) percases ( n <= len f or n > len f ) ; supposeA6: n <= len f ; ::_thesis: ex i, j being Element of NAT st ( [i,j] in Indices M & (f ^' g) /. n = M * (i,j) ) A7: 1 <= n by A5, FINSEQ_3:25; then n in dom f by A6, FINSEQ_3:25; then consider i, j being Element of NAT such that A8: [i,j] in Indices M and A9: f /. n = M * (i,j) by A2, GOBOARD1:def_9; take i ; ::_thesis: ex j being Element of NAT st ( [i,j] in Indices M & (f ^' g) /. n = M * (i,j) ) take j ; ::_thesis: ( [i,j] in Indices M & (f ^' g) /. n = M * (i,j) ) thus [i,j] in Indices M by A8; ::_thesis: (f ^' g) /. n = M * (i,j) thus (f ^' g) /. n = M * (i,j) by A6, A7, A9, GRAPH_2:57; ::_thesis: verum end; supposeA10: n > len f ; ::_thesis: ex i, j being Element of NAT st ( [i,j] in Indices M & (f ^' g) /. n = M * (i,j) ) then consider k being Nat such that A11: n = (len f) + k by NAT_1:10; reconsider k = k as Element of NAT by ORDINAL1:def_12; A12: 1 <= k + 1 by NAT_1:11; n <= len (f ^' g) by A5, FINSEQ_3:25; then n < (len f) + (len g) by A4, NAT_1:13; then A13: k < len g by A11, XREAL_1:6; then k + 1 <= len g by NAT_1:13; then k + 1 in dom g by A12, FINSEQ_3:25; then consider i, j being Element of NAT such that A14: [i,j] in Indices M and A15: g /. (k + 1) = M * (i,j) by A3, GOBOARD1:def_9; take i ; ::_thesis: ex j being Element of NAT st ( [i,j] in Indices M & (f ^' g) /. n = M * (i,j) ) take j ; ::_thesis: ( [i,j] in Indices M & (f ^' g) /. n = M * (i,j) ) thus [i,j] in Indices M by A14; ::_thesis: (f ^' g) /. n = M * (i,j) (len f) + 1 <= n by A10, NAT_1:13; then 1 <= k by A11, XREAL_1:6; hence (f ^' g) /. n = M * (i,j) by A11, A13, A15, GRAPH_2:58; ::_thesis: verum end; end; end; let n be Element of NAT ; ::_thesis: ( not n in dom (f ^' g) or not n + 1 in dom (f ^' g) or for b1, b2, b3, b4 being Element of NAT holds ( not [b1,b2] in Indices M or not [b3,b4] in Indices M or not (f ^' g) /. n = M * (b1,b2) or not (f ^' g) /. (n + 1) = M * (b3,b4) or K144((b1 - b3)) + K144((b2 - b4)) = 1 ) ) assume that A16: n in dom (f ^' g) and A17: n + 1 in dom (f ^' g) ; ::_thesis: for b1, b2, b3, b4 being Element of NAT holds ( not [b1,b2] in Indices M or not [b3,b4] in Indices M or not (f ^' g) /. n = M * (b1,b2) or not (f ^' g) /. (n + 1) = M * (b3,b4) or K144((b1 - b3)) + K144((b2 - b4)) = 1 ) let m, k, i, j be Element of NAT ; ::_thesis: ( not [m,k] in Indices M or not [i,j] in Indices M or not (f ^' g) /. n = M * (m,k) or not (f ^' g) /. (n + 1) = M * (i,j) or K144((m - i)) + K144((k - j)) = 1 ) assume that A18: [m,k] in Indices M and A19: [i,j] in Indices M and A20: (f ^' g) /. n = M * (m,k) and A21: (f ^' g) /. (n + 1) = M * (i,j) ; ::_thesis: K144((m - i)) + K144((k - j)) = 1 percases ( n < len f or n > len f or n = len f ) by XXREAL_0:1; supposeA22: n < len f ; ::_thesis: K144((m - i)) + K144((k - j)) = 1 then A23: n + 1 <= len f by NAT_1:13; then A24: f /. (n + 1) = M * (i,j) by A21, GRAPH_2:57, NAT_1:11; A25: 1 <= n by A16, FINSEQ_3:25; then A26: n in dom f by A22, FINSEQ_3:25; 1 <= n + 1 by NAT_1:11; then A27: n + 1 in dom f by A23, FINSEQ_3:25; f /. n = M * (m,k) by A20, A22, A25, GRAPH_2:57; hence K144((m - i)) + K144((k - j)) = 1 by A2, A18, A19, A26, A27, A24, GOBOARD1:def_9; ::_thesis: verum end; supposeA28: n > len f ; ::_thesis: K144((m - i)) + K144((k - j)) = 1 then consider k0 being Nat such that A29: n = (len f) + k0 by NAT_1:10; reconsider k0 = k0 as Element of NAT by ORDINAL1:def_12; A30: 1 <= k0 + 1 by NAT_1:11; n <= len (f ^' g) by A16, FINSEQ_3:25; then n < (len f) + (len g) by A4, NAT_1:13; then A31: k0 < len g by A29, XREAL_1:6; then k0 + 1 <= len g by NAT_1:13; then A32: k0 + 1 in dom g by A30, FINSEQ_3:25; A33: 1 <= (k0 + 1) + 1 by NAT_1:11; n + 1 <= len (f ^' g) by A17, FINSEQ_3:25; then (len f) + (k0 + 1) < (len f) + (len g) by A4, A29, NAT_1:13; then A34: k0 + 1 < len g by XREAL_1:6; then (k0 + 1) + 1 <= len g by NAT_1:13; then A35: (k0 + 1) + 1 in dom g by A33, FINSEQ_3:25; (len f) + 1 <= n by A28, NAT_1:13; then 1 <= k0 by A29, XREAL_1:6; then A36: g /. (k0 + 1) = M * (m,k) by A20, A29, A31, GRAPH_2:58; g /. ((k0 + 1) + 1) = (f ^' g) /. ((len f) + (k0 + 1)) by A34, GRAPH_2:58, NAT_1:11 .= M * (i,j) by A21, A29 ; hence K144((m - i)) + K144((k - j)) = 1 by A3, A18, A19, A32, A35, A36, GOBOARD1:def_9; ::_thesis: verum end; supposeA37: n = len f ; ::_thesis: K144((m - i)) + K144((k - j)) = 1 n + 1 <= len (f ^' g) by A17, FINSEQ_3:25; then (len f) + 1 < (len f) + (len g) by A4, A37, NAT_1:13; then A38: 1 < len g by XREAL_1:6; then 1 + 1 <= len g by NAT_1:13; then A39: 1 + 1 in dom g by FINSEQ_3:25; 1 <= n by A16, FINSEQ_3:25; then A40: g /. 1 = M * (m,k) by A1, A20, A37, GRAPH_2:57; A41: 1 in dom g by FINSEQ_5:6; g /. (1 + 1) = M * (i,j) by A21, A37, A38, GRAPH_2:58; hence K144((m - i)) + K144((k - j)) = 1 by A3, A18, A19, A40, A39, A41, GOBOARD1:def_9; ::_thesis: verum end; end; end; Lm1: for p being FinSequence for m, n being Element of NAT st 1 <= m & m <= n + 1 & n <= len p holds ( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Element of NAT st i < len ((m,n) -cut p) holds ((m,n) -cut p) . (i + 1) = p . (m + i) ) ) proof let p be FinSequence; ::_thesis: for m, n being Element of NAT st 1 <= m & m <= n + 1 & n <= len p holds ( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Element of NAT st i < len ((m,n) -cut p) holds ((m,n) -cut p) . (i + 1) = p . (m + i) ) ) let m, n be Element of NAT ; ::_thesis: ( 1 <= m & m <= n + 1 & n <= len p implies ( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Element of NAT st i < len ((m,n) -cut p) holds ((m,n) -cut p) . (i + 1) = p . (m + i) ) ) ) assume that A1: 1 <= m and A2: m <= n + 1 and A3: n <= len p ; ::_thesis: ( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Element of NAT st i < len ((m,n) -cut p) holds ((m,n) -cut p) . (i + 1) = p . (m + i) ) ) A4: ( m = n + 1 or m < n + 1 ) by A2, XXREAL_0:1; percases ( m = n + 1 or m <= n ) by A4, NAT_1:13; supposeA5: m = n + 1 ; ::_thesis: ( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Element of NAT st i < len ((m,n) -cut p) holds ((m,n) -cut p) . (i + 1) = p . (m + i) ) ) then n < m by XREAL_1:29; then (m,n) -cut p = {} by GRAPH_2:def_1; hence (len ((m,n) -cut p)) + m = n + 1 by A5, CARD_1:27; ::_thesis: for i being Element of NAT st i < len ((m,n) -cut p) holds ((m,n) -cut p) . (i + 1) = p . (m + i) ( not 1 <= m or not m <= n or not n <= len p ) by A5, XREAL_1:29; hence for i being Element of NAT st i < len ((m,n) -cut p) holds ((m,n) -cut p) . (i + 1) = p . (m + i) by CARD_1:27, GRAPH_2:def_1; ::_thesis: verum end; suppose m <= n ; ::_thesis: ( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Element of NAT st i < len ((m,n) -cut p) holds ((m,n) -cut p) . (i + 1) = p . (m + i) ) ) hence ( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Element of NAT st i < len ((m,n) -cut p) holds ((m,n) -cut p) . (i + 1) = p . (m + i) ) ) by A1, A3, GRAPH_2:def_1; ::_thesis: verum end; end; end; theorem Th13: :: TOPREAL8:13 for k being Element of NAT for D being set for f being FinSequence of D st 1 <= k holds ((k + 1),(len f)) -cut f = f /^ k proof let k be Element of NAT ; ::_thesis: for D being set for f being FinSequence of D st 1 <= k holds ((k + 1),(len f)) -cut f = f /^ k let D be set ; ::_thesis: for f being FinSequence of D st 1 <= k holds ((k + 1),(len f)) -cut f = f /^ k let f be FinSequence of D; ::_thesis: ( 1 <= k implies ((k + 1),(len f)) -cut f = f /^ k ) assume A1: 1 <= k ; ::_thesis: ((k + 1),(len f)) -cut f = f /^ k percases ( len f < k or f = {} or k <= len f ) ; supposeA2: len f < k ; ::_thesis: ((k + 1),(len f)) -cut f = f /^ k k <= k + 1 by NAT_1:11; then len f < k + 1 by A2, XXREAL_0:2; hence ((k + 1),(len f)) -cut f = {} by GRAPH_2:def_1 .= f /^ k by A2, FINSEQ_5:32 ; ::_thesis: verum end; supposeA3: f = {} ; ::_thesis: ((k + 1),(len f)) -cut f = f /^ k then A4: len f = 0 ; thus ((k + 1),(len f)) -cut f = <*> D by A3, GRAPH_2:def_1 .= f /^ k by A1, A4, RFINSEQ:def_1 ; ::_thesis: verum end; supposeA5: k <= len f ; ::_thesis: ((k + 1),(len f)) -cut f = f /^ k set IT = ((k + 1),(len f)) -cut f; A6: 1 <= k + 1 by NAT_1:11; A7: k + 1 <= (len f) + 1 by A5, XREAL_1:6; A8: for m being Nat st m in dom (((k + 1),(len f)) -cut f) holds (((k + 1),(len f)) -cut f) . m = f . (m + k) proof let m be Nat; ::_thesis: ( m in dom (((k + 1),(len f)) -cut f) implies (((k + 1),(len f)) -cut f) . m = f . (m + k) ) assume A9: m in dom (((k + 1),(len f)) -cut f) ; ::_thesis: (((k + 1),(len f)) -cut f) . m = f . (m + k) 1 <= m by A9, FINSEQ_3:25; then consider i being Nat such that A10: m = 1 + i by NAT_1:10; reconsider i = i as Element of NAT by ORDINAL1:def_12; m <= len (((k + 1),(len f)) -cut f) by A9, FINSEQ_3:25; then i < len (((k + 1),(len f)) -cut f) by A10, NAT_1:13; hence (((k + 1),(len f)) -cut f) . m = f . ((k + 1) + i) by A6, A7, A10, Lm1 .= f . (m + k) by A10 ; ::_thesis: verum end; (len f) + 1 = (len (((k + 1),(len f)) -cut f)) + (k + 1) by A6, A7, Lm1 .= ((len (((k + 1),(len f)) -cut f)) + k) + 1 ; then len (((k + 1),(len f)) -cut f) = (len f) - k ; hence ((k + 1),(len f)) -cut f = f /^ k by A5, A8, RFINSEQ:def_1; ::_thesis: verum end; end; end; theorem Th14: :: TOPREAL8:14 for k being Element of NAT for D being set for f being FinSequence of D st k <= len f holds (1,k) -cut f = f | k proof let k be Element of NAT ; ::_thesis: for D being set for f being FinSequence of D st k <= len f holds (1,k) -cut f = f | k let D be set ; ::_thesis: for f being FinSequence of D st k <= len f holds (1,k) -cut f = f | k let f be FinSequence of D; ::_thesis: ( k <= len f implies (1,k) -cut f = f | k ) assume A1: k <= len f ; ::_thesis: (1,k) -cut f = f | k percases ( 0 + 1 > k or 1 <= k ) ; supposeA2: 0 + 1 > k ; ::_thesis: (1,k) -cut f = f | k A3: f | 0 = {} ; k = 0 by A2, NAT_1:13; hence (1,k) -cut f = f | k by A3, GRAPH_2:def_1; ::_thesis: verum end; supposeA4: 1 <= k ; ::_thesis: (1,k) -cut f = f | k A5: (len (f | k)) + 1 = k + 1 by A1, FINSEQ_1:59; for i being Nat st i < len (f | k) holds (f | k) . (i + 1) = f . (1 + i) proof let i be Nat; ::_thesis: ( i < len (f | k) implies (f | k) . (i + 1) = f . (1 + i) ) assume i < len (f | k) ; ::_thesis: (f | k) . (i + 1) = f . (1 + i) then i + 1 <= k by A5, NAT_1:13; hence (f | k) . (i + 1) = f . (1 + i) by FINSEQ_3:112; ::_thesis: verum end; hence (1,k) -cut f = f | k by A1, A4, A5, GRAPH_2:def_1; ::_thesis: verum end; end; end; theorem Th15: :: TOPREAL8:15 for p being set for D being non empty set for f being non empty FinSequence of D for g being FinSequence of D st p .. f = len f holds (f ^ g) -| p = (1,((len f) -' 1)) -cut f proof let p be set ; ::_thesis: for D being non empty set for f being non empty FinSequence of D for g being FinSequence of D st p .. f = len f holds (f ^ g) -| p = (1,((len f) -' 1)) -cut f let D be non empty set ; ::_thesis: for f being non empty FinSequence of D for g being FinSequence of D st p .. f = len f holds (f ^ g) -| p = (1,((len f) -' 1)) -cut f let f be non empty FinSequence of D; ::_thesis: for g being FinSequence of D st p .. f = len f holds (f ^ g) -| p = (1,((len f) -' 1)) -cut f let g be FinSequence of D; ::_thesis: ( p .. f = len f implies (f ^ g) -| p = (1,((len f) -' 1)) -cut f ) assume A1: p .. f = len f ; ::_thesis: (f ^ g) -| p = (1,((len f) -' 1)) -cut f p in rng f by A1, Th4; then A2: p .. (f ^ g) = p .. f by FINSEQ_6:6; reconsider i = (len f) - 1 as Element of NAT by INT_1:5, NAT_1:14; A3: (len f) -' 1 = i by NAT_1:14, XREAL_1:233; len (f ^ g) = (len f) + (len g) by FINSEQ_1:22; then A4: len f <= len (f ^ g) by NAT_1:11; rng f c= rng (f ^ g) by FINSEQ_1:29; hence (f ^ g) -| p = (f ^ g) | (Seg i) by A1, A2, Th4, FINSEQ_4:33 .= (f ^ g) | i by FINSEQ_1:def_15 .= (1,((len f) -' 1)) -cut (f ^ g) by A4, A3, Th14, NAT_D:44 .= (1,((len f) -' 1)) -cut f by MSSCYC_1:2, NAT_D:44 ; ::_thesis: verum end; theorem Th16: :: TOPREAL8:16 for D being non empty set for f, g being non empty FinSequence of D st (g /. 1) .. f = len f holds (f ^' g) :- (g /. 1) = g proof let D be non empty set ; ::_thesis: for f, g being non empty FinSequence of D st (g /. 1) .. f = len f holds (f ^' g) :- (g /. 1) = g let f, g be non empty FinSequence of D; ::_thesis: ( (g /. 1) .. f = len f implies (f ^' g) :- (g /. 1) = g ) assume A1: (g /. 1) .. f = len f ; ::_thesis: (f ^' g) :- (g /. 1) = g A2: g /. 1 in rng f by A1, Th4; A3: 1 <= len g by NAT_1:14; A4: f ^' g = f ^ ((2,(len g)) -cut g) by GRAPH_2:def_2; then rng f c= rng (f ^' g) by FINSEQ_1:29; hence (f ^' g) :- (g /. 1) = <*(g /. 1)*> ^ ((f ^' g) |-- (g /. 1)) by A2, FINSEQ_6:41 .= <*(g /. 1)*> ^ ((2,(len g)) -cut g) by A1, A4, Th5 .= <*(g . 1)*> ^ ((2,(len g)) -cut g) by A3, FINSEQ_4:15 .= ((1,1) -cut g) ^ (((1 + 1),(len g)) -cut g) by A3, GRAPH_2:6 .= g by GRAPH_2:9, NAT_1:14 ; ::_thesis: verum end; theorem Th17: :: TOPREAL8:17 for D being non empty set for f, g being non empty FinSequence of D st (g /. 1) .. f = len f holds (f ^' g) -: (g /. 1) = f proof let D be non empty set ; ::_thesis: for f, g being non empty FinSequence of D st (g /. 1) .. f = len f holds (f ^' g) -: (g /. 1) = f let f, g be non empty FinSequence of D; ::_thesis: ( (g /. 1) .. f = len f implies (f ^' g) -: (g /. 1) = f ) assume A1: (g /. 1) .. f = len f ; ::_thesis: (f ^' g) -: (g /. 1) = f A2: g /. 1 in rng f by A1, Th4; g /. 1 in rng f by A1, Th4; then A3: g /. 1 = f . (len f) by A1, FINSEQ_4:19; A4: 1 <= len f by NAT_1:14; A5: ((len f) -' 1) + 1 = len f by NAT_1:14, XREAL_1:235; A6: f ^' g = f ^ ((2,(len g)) -cut g) by GRAPH_2:def_2; then rng f c= rng (f ^' g) by FINSEQ_1:29; hence (f ^' g) -: (g /. 1) = ((f ^' g) -| (g /. 1)) ^ <*(g /. 1)*> by A2, FINSEQ_6:40 .= ((1,((len f) -' 1)) -cut f) ^ <*(g /. 1)*> by A1, A6, Th15 .= ((1,((len f) -' 1)) -cut f) ^ (((len f),(len f)) -cut f) by A4, A3, GRAPH_2:6 .= f by A5, GRAPH_2:9, NAT_D:44 ; ::_thesis: verum end; theorem Th18: :: TOPREAL8:18 for D being non trivial set for f being non empty FinSequence of D for g being non trivial FinSequence of D st g /. 1 = f /. (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds f /. i <> g /. 1 ) holds Rotate ((f ^' g),(g /. 1)) = g ^' f proof let D be non trivial set ; ::_thesis: for f being non empty FinSequence of D for g being non trivial FinSequence of D st g /. 1 = f /. (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds f /. i <> g /. 1 ) holds Rotate ((f ^' g),(g /. 1)) = g ^' f let f be non empty FinSequence of D; ::_thesis: for g being non trivial FinSequence of D st g /. 1 = f /. (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds f /. i <> g /. 1 ) holds Rotate ((f ^' g),(g /. 1)) = g ^' f let g be non trivial FinSequence of D; ::_thesis: ( g /. 1 = f /. (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds f /. i <> g /. 1 ) implies Rotate ((f ^' g),(g /. 1)) = g ^' f ) assume that A1: g /. 1 = f /. (len f) and A2: for i being Element of NAT st 1 <= i & i < len f holds f /. i <> g /. 1 ; ::_thesis: Rotate ((f ^' g),(g /. 1)) = g ^' f A3: g /. 1 in rng f by A1, REVROT_1:3; A4: len f in dom f by FINSEQ_5:6; then A5: f . (len f) = f /. (len f) by PARTFUN1:def_6; for i being Nat st 1 <= i & i < len f holds f . i <> f . (len f) proof let i be Nat; ::_thesis: ( 1 <= i & i < len f implies f . i <> f . (len f) ) assume that A6: 1 <= i and A7: i < len f ; ::_thesis: f . i <> f . (len f) A8: i in NAT by ORDINAL1:def_12; f . i = f /. i by A6, A7, FINSEQ_4:15; hence f . i <> f . (len f) by A1, A2, A5, A6, A7, A8; ::_thesis: verum end; then A9: (g /. 1) .. f = len f by A1, A4, A5, FINSEQ_6:2; then A10: (f ^' g) :- (g /. 1) = g by Th16; (f ^' g) -: (g /. 1) = f by A9, Th17; then A11: ((f ^' g) -: (g /. 1)) /^ 1 = ((1 + 1),(len f)) -cut f by Th13; rng f c= rng (f ^' g) by Th10; hence Rotate ((f ^' g),(g /. 1)) = ((f ^' g) :- (g /. 1)) ^ (((f ^' g) -: (g /. 1)) /^ 1) by A3, FINSEQ_6:def_2 .= g ^' f by A10, A11, GRAPH_2:def_2 ; ::_thesis: verum end; begin theorem Th19: :: TOPREAL8:19 for f being non trivial FinSequence of (TOP-REAL 2) holds LSeg (f,1) = L~ (f | 2) proof let f be non trivial FinSequence of (TOP-REAL 2); ::_thesis: LSeg (f,1) = L~ (f | 2) A1: 1 + 1 <= len f by NAT_D:60; then A2: f | 2 = <*(f /. 1),(f /. 2)*> by FINSEQ_5:81; thus LSeg (f,1) = LSeg ((f /. 1),(f /. (1 + 1))) by A1, TOPREAL1:def_3 .= L~ (f | 2) by A2, SPPOL_2:21 ; ::_thesis: verum end; theorem Th20: :: TOPREAL8:20 for f being s.c.c. FinSequence of (TOP-REAL 2) for n being Element of NAT st n < len f holds f | n is s.n.c. proof let f be s.c.c. FinSequence of (TOP-REAL 2); ::_thesis: for n being Element of NAT st n < len f holds f | n is s.n.c. let n be Element of NAT ; ::_thesis: ( n < len f implies f | n is s.n.c. ) assume A1: n < len f ; ::_thesis: f | n is s.n.c. let i, j be Nat; :: according to TOPREAL1:def_7 ::_thesis: ( j <= i + 1 or LSeg ((f | n),i) misses LSeg ((f | n),j) ) assume A2: i + 1 < j ; ::_thesis: LSeg ((f | n),i) misses LSeg ((f | n),j) A3: j in NAT by ORDINAL1:def_12; A4: i in NAT by ORDINAL1:def_12; A5: len (f | n) <= n by FINSEQ_5:17; percases ( n < j + 1 or len (f | n) < j + 1 or ( j + 1 <= n & j + 1 <= len (f | n) ) ) ; suppose n < j + 1 ; ::_thesis: LSeg ((f | n),i) misses LSeg ((f | n),j) then len (f | n) < j + 1 by A5, XXREAL_0:2; then LSeg ((f | n),j) = {} by TOPREAL1:def_3; then (LSeg ((f | n),i)) /\ (LSeg ((f | n),j)) = {} ; hence LSeg ((f | n),i) misses LSeg ((f | n),j) by XBOOLE_0:def_7; ::_thesis: verum end; suppose len (f | n) < j + 1 ; ::_thesis: LSeg ((f | n),i) misses LSeg ((f | n),j) then LSeg ((f | n),j) = {} by TOPREAL1:def_3; then (LSeg ((f | n),i)) /\ (LSeg ((f | n),j)) = {} ; hence LSeg ((f | n),i) misses LSeg ((f | n),j) by XBOOLE_0:def_7; ::_thesis: verum end; supposethat A6: j + 1 <= n and A7: j + 1 <= len (f | n) ; ::_thesis: LSeg ((f | n),i) misses LSeg ((f | n),j) j + 1 < len f by A1, A6, XXREAL_0:2; then A8: LSeg (f,i) misses LSeg (f,j) by A2, A4, A3, GOBOARD5:def_4; j <= j + 1 by NAT_1:11; then A9: i + 1 <= j + 1 by A2, XXREAL_0:2; LSeg (f,j) = LSeg ((f | n),j) by A7, SPPOL_2:3; hence LSeg ((f | n),i) misses LSeg ((f | n),j) by A7, A8, A9, SPPOL_2:3, XXREAL_0:2; ::_thesis: verum end; end; end; theorem Th21: :: TOPREAL8:21 for f being s.c.c. FinSequence of (TOP-REAL 2) for n being Element of NAT st 1 <= n holds f /^ n is s.n.c. proof let f be s.c.c. FinSequence of (TOP-REAL 2); ::_thesis: for n being Element of NAT st 1 <= n holds f /^ n is s.n.c. let n be Element of NAT ; ::_thesis: ( 1 <= n implies f /^ n is s.n.c. ) assume A1: 1 <= n ; ::_thesis: f /^ n is s.n.c. let i, j be Nat; :: according to TOPREAL1:def_7 ::_thesis: ( j <= i + 1 or LSeg ((f /^ n),i) misses LSeg ((f /^ n),j) ) assume A2: i + 1 < j ; ::_thesis: LSeg ((f /^ n),i) misses LSeg ((f /^ n),j) percases ( i < 1 or n > len f or len (f /^ n) <= j or ( n <= len f & 1 <= i & j < len (f /^ n) ) ) ; suppose i < 1 ; ::_thesis: LSeg ((f /^ n),i) misses LSeg ((f /^ n),j) then LSeg ((f /^ n),i) = {} by TOPREAL1:def_3; then (LSeg ((f /^ n),i)) /\ (LSeg ((f /^ n),j)) = {} ; hence LSeg ((f /^ n),i) misses LSeg ((f /^ n),j) by XBOOLE_0:def_7; ::_thesis: verum end; suppose n > len f ; ::_thesis: LSeg ((f /^ n),i) misses LSeg ((f /^ n),j) then f /^ n = <*> the carrier of (TOP-REAL 2) by RFINSEQ:def_1; then ( not 1 <= i or not i + 1 <= len (f /^ n) ) ; then LSeg ((f /^ n),i) = {} by TOPREAL1:def_3; then (LSeg ((f /^ n),i)) /\ (LSeg ((f /^ n),j)) = {} ; hence LSeg ((f /^ n),i) misses LSeg ((f /^ n),j) by XBOOLE_0:def_7; ::_thesis: verum end; suppose len (f /^ n) <= j ; ::_thesis: LSeg ((f /^ n),i) misses LSeg ((f /^ n),j) then len (f /^ n) < j + 1 by NAT_1:13; then LSeg ((f /^ n),j) = {} by TOPREAL1:def_3; then (LSeg ((f /^ n),i)) /\ (LSeg ((f /^ n),j)) = {} ; hence LSeg ((f /^ n),i) misses LSeg ((f /^ n),j) by XBOOLE_0:def_7; ::_thesis: verum end; supposethat A3: n <= len f and A4: 1 <= i and A5: j < len (f /^ n) ; ::_thesis: LSeg ((f /^ n),i) misses LSeg ((f /^ n),j) A6: j < (len f) - n by A3, A5, RFINSEQ:def_1; then A7: j + 1 <= (len f) - n by INT_1:7; 1 + 1 <= i + 1 by A4, XREAL_1:6; then 1 + 1 <= j by A2, XXREAL_0:2; then 1 < j by NAT_1:13; then A8: LSeg (f,(j + n)) = LSeg ((f /^ n),j) by A7, SPPOL_2:5; (i + 1) + n < j + n by A2, XREAL_1:6; then A9: (i + n) + 1 < j + n ; j <= j + 1 by NAT_1:11; then i + 1 <= j + 1 by A2, XXREAL_0:2; then A10: i + 1 <= (len f) - n by A7, XXREAL_0:2; 1 + 1 <= i + n by A1, A4, XREAL_1:7; then A11: 1 < i + n by NAT_1:13; j + n < len f by A6, XREAL_1:20; then LSeg (f,(i + n)) misses LSeg (f,(j + n)) by A11, A9, GOBOARD5:def_4; hence LSeg ((f /^ n),i) misses LSeg ((f /^ n),j) by A4, A8, A10, SPPOL_2:5; ::_thesis: verum end; end; end; theorem Th22: :: TOPREAL8:22 for f being circular s.c.c. FinSequence of (TOP-REAL 2) for n being Element of NAT st n < len f & len f > 4 holds f | n is one-to-one proof let f be circular s.c.c. FinSequence of (TOP-REAL 2); ::_thesis: for n being Element of NAT st n < len f & len f > 4 holds f | n is one-to-one let n be Element of NAT ; ::_thesis: ( n < len f & len f > 4 implies f | n is one-to-one ) assume that A1: n < len f and A2: len f > 4 ; ::_thesis: f | n is one-to-one for c1, c2 being Element of NAT st c1 in dom (f | n) & c2 in dom (f | n) & (f | n) /. c1 = (f | n) /. c2 holds c1 = c2 proof A3: len (f | n) <= n by FINSEQ_5:17; A4: len (f | n) <= n by FINSEQ_5:17; let c1, c2 be Element of NAT ; ::_thesis: ( c1 in dom (f | n) & c2 in dom (f | n) & (f | n) /. c1 = (f | n) /. c2 implies c1 = c2 ) assume that A5: c1 in dom (f | n) and A6: c2 in dom (f | n) and A7: (f | n) /. c1 = (f | n) /. c2 ; ::_thesis: c1 = c2 A8: 1 <= c1 by A5, FINSEQ_3:25; c1 <= len (f | n) by A5, FINSEQ_3:25; then c1 <= n by A3, XXREAL_0:2; then A9: c1 < len f by A1, XXREAL_0:2; A10: 1 <= c2 by A6, FINSEQ_3:25; A11: (f | n) /. c1 = f /. c1 by A5, FINSEQ_4:70; c2 <= len (f | n) by A6, FINSEQ_3:25; then c2 <= n by A4, XXREAL_0:2; then A12: c2 < len f by A1, XXREAL_0:2; A13: (f | n) /. c2 = f /. c2 by A6, FINSEQ_4:70; assume A14: c1 <> c2 ; ::_thesis: contradiction percases ( c1 < c2 or c2 < c1 ) by A14, XXREAL_0:1; suppose c1 < c2 ; ::_thesis: contradiction hence contradiction by A2, A7, A8, A12, A11, A13, GOBOARD7:35; ::_thesis: verum end; suppose c2 < c1 ; ::_thesis: contradiction hence contradiction by A2, A7, A10, A9, A11, A13, GOBOARD7:35; ::_thesis: verum end; end; end; hence f | n is one-to-one by PARTFUN2:9; ::_thesis: verum end; theorem Th23: :: TOPREAL8:23 for f being circular s.c.c. FinSequence of (TOP-REAL 2) st len f > 4 holds for i, j being Element of NAT st 1 < i & i < j & j <= len f holds f /. i <> f /. j proof let f be circular s.c.c. FinSequence of (TOP-REAL 2); ::_thesis: ( len f > 4 implies for i, j being Element of NAT st 1 < i & i < j & j <= len f holds f /. i <> f /. j ) assume A1: len f > 4 ; ::_thesis: for i, j being Element of NAT st 1 < i & i < j & j <= len f holds f /. i <> f /. j let i, j be Element of NAT ; ::_thesis: ( 1 < i & i < j & j <= len f implies f /. i <> f /. j ) assume that A2: 1 < i and A3: i < j and A4: j <= len f ; ::_thesis: f /. i <> f /. j percases ( j < len f or j = len f ) by A4, XXREAL_0:1; suppose j < len f ; ::_thesis: f /. i <> f /. j hence f /. i <> f /. j by A1, A2, A3, GOBOARD7:35; ::_thesis: verum end; suppose j = len f ; ::_thesis: f /. i <> f /. j then A5: f /. j = f /. 1 by FINSEQ_6:def_1; i < len f by A3, A4, XXREAL_0:2; hence f /. i <> f /. j by A1, A2, A5, GOBOARD7:35; ::_thesis: verum end; end; end; theorem Th24: :: TOPREAL8:24 for f being circular s.c.c. FinSequence of (TOP-REAL 2) for n being Element of NAT st 1 <= n & len f > 4 holds f /^ n is one-to-one proof let f be circular s.c.c. FinSequence of (TOP-REAL 2); ::_thesis: for n being Element of NAT st 1 <= n & len f > 4 holds f /^ n is one-to-one let n be Element of NAT ; ::_thesis: ( 1 <= n & len f > 4 implies f /^ n is one-to-one ) assume that A1: 1 <= n and A2: len f > 4 ; ::_thesis: f /^ n is one-to-one for c1, c2 being Element of NAT st c1 in dom (f /^ n) & c2 in dom (f /^ n) & (f /^ n) /. c1 = (f /^ n) /. c2 holds c1 = c2 proof let c1, c2 be Element of NAT ; ::_thesis: ( c1 in dom (f /^ n) & c2 in dom (f /^ n) & (f /^ n) /. c1 = (f /^ n) /. c2 implies c1 = c2 ) assume that A3: c1 in dom (f /^ n) and A4: c2 in dom (f /^ n) and A5: (f /^ n) /. c1 = (f /^ n) /. c2 ; ::_thesis: c1 = c2 A6: (f /^ n) /. c1 = f /. (c1 + n) by A3, FINSEQ_5:27; A7: n <= len f by A3, RELAT_1:38, RFINSEQ:def_1; then len (f /^ n) = (len f) - n by RFINSEQ:def_1; then A8: (len (f /^ n)) + n = len f ; len (f /^ n) = (len f) - n by A7, RFINSEQ:def_1; then A9: (len (f /^ n)) + n = len f ; c1 <= len (f /^ n) by A3, FINSEQ_3:25; then A10: c1 + n <= len f by A9, XREAL_1:6; 0 + 1 <= c1 by A3, FINSEQ_3:25; then A11: 1 + 0 < c1 + n by A1, XREAL_1:8; A12: (f /^ n) /. c2 = f /. (c2 + n) by A4, FINSEQ_5:27; c2 <= len (f /^ n) by A4, FINSEQ_3:25; then A13: c2 + n <= len f by A8, XREAL_1:6; 0 + 1 <= c2 by A4, FINSEQ_3:25; then A14: 1 + 0 < c2 + n by A1, XREAL_1:8; assume A15: c1 <> c2 ; ::_thesis: contradiction percases ( c1 < c2 or c2 < c1 ) by A15, XXREAL_0:1; suppose c1 < c2 ; ::_thesis: contradiction then c1 + n < c2 + n by XREAL_1:6; hence contradiction by A2, A5, A11, A13, A6, A12, Th23; ::_thesis: verum end; suppose c2 < c1 ; ::_thesis: contradiction then c2 + n < c1 + n by XREAL_1:6; hence contradiction by A2, A5, A14, A10, A6, A12, Th23; ::_thesis: verum end; end; end; hence f /^ n is one-to-one by PARTFUN2:9; ::_thesis: verum end; theorem Th25: :: TOPREAL8:25 for m, n being Element of NAT for f being non empty special FinSequence of (TOP-REAL 2) holds (m,n) -cut f is special proof let m, n be Element of NAT ; ::_thesis: for f being non empty special FinSequence of (TOP-REAL 2) holds (m,n) -cut f is special let f be non empty special FinSequence of (TOP-REAL 2); ::_thesis: (m,n) -cut f is special set h = (m,n) -cut f; let i be Nat; :: according to TOPREAL1:def_5 ::_thesis: ( not 1 <= i or not i + 1 <= len ((m,n) -cut f) or (((m,n) -cut f) /. i) `1 = (((m,n) -cut f) /. (i + 1)) `1 or (((m,n) -cut f) /. i) `2 = (((m,n) -cut f) /. (i + 1)) `2 ) assume that A1: 1 <= i and A2: i + 1 <= len ((m,n) -cut f) ; ::_thesis: ( (((m,n) -cut f) /. i) `1 = (((m,n) -cut f) /. (i + 1)) `1 or (((m,n) -cut f) /. i) `2 = (((m,n) -cut f) /. (i + 1)) `2 ) percases ( not 1 <= m or not m <= n or not n <= len f or ( 1 <= m & m <= n & n <= len f ) ) ; suppose ( not 1 <= m or not m <= n or not n <= len f ) ; ::_thesis: ( (((m,n) -cut f) /. i) `1 = (((m,n) -cut f) /. (i + 1)) `1 or (((m,n) -cut f) /. i) `2 = (((m,n) -cut f) /. (i + 1)) `2 ) then (m,n) -cut f = {} by GRAPH_2:def_1; hence ( (((m,n) -cut f) /. i) `1 = (((m,n) -cut f) /. (i + 1)) `1 or (((m,n) -cut f) /. i) `2 = (((m,n) -cut f) /. (i + 1)) `2 ) by A2; ::_thesis: verum end; supposeA3: ( 1 <= m & m <= n & n <= len f ) ; ::_thesis: ( (((m,n) -cut f) /. i) `1 = (((m,n) -cut f) /. (i + 1)) `1 or (((m,n) -cut f) /. i) `2 = (((m,n) -cut f) /. (i + 1)) `2 ) then A4: 1 + 1 <= i + m by A1, XREAL_1:7; then A5: 1 <= i + m by XXREAL_0:2; A6: (i -' 1) + m = (i + m) -' 1 by A1, NAT_D:38; then A7: 1 <= (i -' 1) + m by A4, NAT_D:55; A8: ((i -' 1) + m) + 1 = ((i + m) -' 1) + 1 by A1, NAT_D:38 .= i + m by A4, XREAL_1:235, XXREAL_0:2 ; A9: i < len ((m,n) -cut f) by A2, NAT_1:13; (len ((m,n) -cut f)) + m = n + 1 by A3, GRAPH_2:def_1; then i + m < n + 1 by A9, XREAL_1:6; then i + m <= n by NAT_1:13; then A10: i + m <= len f by A3, XXREAL_0:2; then A11: (i -' 1) + m <= len f by A6, NAT_D:44; i -' 1 <= i by NAT_D:44; then A12: i -' 1 < len ((m,n) -cut f) by A9, XXREAL_0:2; A13: ((m,n) -cut f) /. (i + 1) = ((m,n) -cut f) . (i + 1) by A2, FINSEQ_4:15, NAT_1:11 .= f . (i + m) by A3, A9, GRAPH_2:def_1 .= f /. (i + m) by A5, A10, FINSEQ_4:15 ; (i -' 1) + 1 = i by A1, XREAL_1:235; then ((m,n) -cut f) /. i = ((m,n) -cut f) . ((i -' 1) + 1) by A1, A9, FINSEQ_4:15 .= f . ((i -' 1) + m) by A3, A12, GRAPH_2:def_1 .= f /. ((i -' 1) + m) by A6, A4, A11, FINSEQ_4:15, NAT_D:55 ; hence ( (((m,n) -cut f) /. i) `1 = (((m,n) -cut f) /. (i + 1)) `1 or (((m,n) -cut f) /. i) `2 = (((m,n) -cut f) /. (i + 1)) `2 ) by A7, A10, A13, A8, TOPREAL1:def_5; ::_thesis: verum end; end; end; theorem Th26: :: TOPREAL8:26 for f being non empty special FinSequence of (TOP-REAL 2) for g being non trivial special FinSequence of (TOP-REAL 2) st f /. (len f) = g /. 1 holds f ^' g is special proof let f be non empty special FinSequence of (TOP-REAL 2); ::_thesis: for g being non trivial special FinSequence of (TOP-REAL 2) st f /. (len f) = g /. 1 holds f ^' g is special let g be non trivial special FinSequence of (TOP-REAL 2); ::_thesis: ( f /. (len f) = g /. 1 implies f ^' g is special ) assume A1: f /. (len f) = g /. 1 ; ::_thesis: f ^' g is special set h = (2,(len g)) -cut g; A2: f ^' g = f ^ ((2,(len g)) -cut g) by GRAPH_2:def_2; A3: 1 + 1 <= len g by NAT_D:60; then A4: ( (g /. 1) `1 = (g /. (1 + 1)) `1 or (g /. 1) `2 = (g /. (1 + 1)) `2 ) by TOPREAL1:def_5; len g <= (len g) + 1 by NAT_1:11; then A5: 2 <= (len g) + 1 by A3, XXREAL_0:2; ((len ((2,(len g)) -cut g)) + 1) + 1 = (len ((2,(len g)) -cut g)) + (1 + 1) .= (len g) + 1 by A5, Lm1 ; then 1 <= len ((2,(len g)) -cut g) by A3, XREAL_1:6; then A6: ((2,(len g)) -cut g) /. 1 = ((2,(len g)) -cut g) . 1 by FINSEQ_4:15 .= g . (1 + 1) by A3, GRAPH_2:12 .= g /. (1 + 1) by A3, FINSEQ_4:15 ; (2,(len g)) -cut g is special by Th25; hence f ^' g is special by A1, A2, A6, A4, GOBOARD2:8; ::_thesis: verum end; theorem Th27: :: TOPREAL8:27 for f being circular unfolded s.c.c. FinSequence of (TOP-REAL 2) st len f > 4 holds (LSeg (f,1)) /\ (L~ (f /^ 1)) = {(f /. 1),(f /. 2)} proof let f be circular unfolded s.c.c. FinSequence of (TOP-REAL 2); ::_thesis: ( len f > 4 implies (LSeg (f,1)) /\ (L~ (f /^ 1)) = {(f /. 1),(f /. 2)} ) assume A1: len f > 4 ; ::_thesis: (LSeg (f,1)) /\ (L~ (f /^ 1)) = {(f /. 1),(f /. 2)} A2: 1 + 2 <= len f by A1, XXREAL_0:2; set h2 = f /^ 1; A3: 1 <= len f by A1, XXREAL_0:2; then A4: len (f /^ 1) = (len f) - 1 by RFINSEQ:def_1; then A5: (len (f /^ 1)) + 1 = len f ; len f > 3 + 1 by A1; then A6: len (f /^ 1) > 2 + 1 by A5, XREAL_1:6; then A7: 1 + 1 <= len (f /^ 1) by XXREAL_0:2; set SFY = { (LSeg ((f /^ 1),i)) where i is Element of NAT : ( 1 < i & i + 1 < len (f /^ 1) ) } ; set Reszta = union { (LSeg ((f /^ 1),i)) where i is Element of NAT : ( 1 < i & i + 1 < len (f /^ 1) ) } ; A8: ((len (f /^ 1)) -' 1) + 1 <= len (f /^ 1) by A6, XREAL_1:235, XXREAL_0:2; A9: 1 < len f by A1, XXREAL_0:2; for Z being set holds ( Z in {{}} iff ex X, Y being set st ( X in {(LSeg (f,1))} & Y in { (LSeg ((f /^ 1),i)) where i is Element of NAT : ( 1 < i & i + 1 < len (f /^ 1) ) } & Z = X /\ Y ) ) proof let Z be set ; ::_thesis: ( Z in {{}} iff ex X, Y being set st ( X in {(LSeg (f,1))} & Y in { (LSeg ((f /^ 1),i)) where i is Element of NAT : ( 1 < i & i + 1 < len (f /^ 1) ) } & Z = X /\ Y ) ) thus ( Z in {{}} implies ex X, Y being set st ( X in {(LSeg (f,1))} & Y in { (LSeg ((f /^ 1),i)) where i is Element of NAT : ( 1 < i & i + 1 < len (f /^ 1) ) } & Z = X /\ Y ) ) ::_thesis: ( ex X, Y being set st ( X in {(LSeg (f,1))} & Y in { (LSeg ((f /^ 1),i)) where i is Element of NAT : ( 1 < i & i + 1 < len (f /^ 1) ) } & Z = X /\ Y ) implies Z in {{}} ) proof assume A10: Z in {{}} ; ::_thesis: ex X, Y being set st ( X in {(LSeg (f,1))} & Y in { (LSeg ((f /^ 1),i)) where i is Element of NAT : ( 1 < i & i + 1 < len (f /^ 1) ) } & Z = X /\ Y ) take X = LSeg (f,1); ::_thesis: ex Y being set st ( X in {(LSeg (f,1))} & Y in { (LSeg ((f /^ 1),i)) where i is Element of NAT : ( 1 < i & i + 1 < len (f /^ 1) ) } & Z = X /\ Y ) take Y = LSeg (f,(2 + 1)); ::_thesis: ( X in {(LSeg (f,1))} & Y in { (LSeg ((f /^ 1),i)) where i is Element of NAT : ( 1 < i & i + 1 < len (f /^ 1) ) } & Z = X /\ Y ) thus X in {(LSeg (f,1))} by TARSKI:def_1; ::_thesis: ( Y in { (LSeg ((f /^ 1),i)) where i is Element of NAT : ( 1 < i & i + 1 < len (f /^ 1) ) } & Z = X /\ Y ) Y = LSeg ((f /^ 1),2) by A3, SPPOL_2:4; hence Y in { (LSeg ((f /^ 1),i)) where i is Element of NAT : ( 1 < i & i + 1 < len (f /^ 1) ) } by A6; ::_thesis: Z = X /\ Y A11: 1 + 1 < 3 ; 3 + 1 < len f by A1; then X misses Y by A11, GOBOARD5:def_4; then X /\ Y = {} by XBOOLE_0:def_7; hence Z = X /\ Y by A10, TARSKI:def_1; ::_thesis: verum end; given X, Y being set such that A12: X in {(LSeg (f,1))} and A13: Y in { (LSeg ((f /^ 1),i)) where i is Element of NAT : ( 1 < i & i + 1 < len (f /^ 1) ) } and A14: Z = X /\ Y ; ::_thesis: Z in {{}} A15: X = LSeg (f,1) by A12, TARSKI:def_1; consider i being Element of NAT such that A16: Y = LSeg ((f /^ 1),i) and A17: 1 < i and A18: i + 1 < len (f /^ 1) by A13; A19: 1 + 1 < i + 1 by A17, XREAL_1:6; A20: (i + 1) + 1 < len f by A5, A18, XREAL_1:6; LSeg ((f /^ 1),i) = LSeg (f,(i + 1)) by A9, A17, SPPOL_2:4; then X misses Y by A15, A16, A20, A19, GOBOARD5:def_4; then Z = {} by A14, XBOOLE_0:def_7; hence Z in {{}} by TARSKI:def_1; ::_thesis: verum end; then INTERSECTION ({(LSeg (f,1))}, { (LSeg ((f /^ 1),i)) where i is Element of NAT : ( 1 < i & i + 1 < len (f /^ 1) ) } ) = {{}} by SETFAM_1:def_5; then A21: (LSeg (f,1)) /\ (union { (LSeg ((f /^ 1),i)) where i is Element of NAT : ( 1 < i & i + 1 < len (f /^ 1) ) } ) = union {{}} by SETFAM_1:25 .= {} by ZFMISC_1:25 ; A22: L~ (f /^ 1) c= ((LSeg ((f /^ 1),1)) \/ (LSeg ((f /^ 1),((len (f /^ 1)) -' 1)))) \/ (union { (LSeg ((f /^ 1),i)) where i is Element of NAT : ( 1 < i & i + 1 < len (f /^ 1) ) } ) proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in L~ (f /^ 1) or u in ((LSeg ((f /^ 1),1)) \/ (LSeg ((f /^ 1),((len (f /^ 1)) -' 1)))) \/ (union { (LSeg ((f /^ 1),i)) where i is Element of NAT : ( 1 < i & i + 1 < len (f /^ 1) ) } ) ) assume u in L~ (f /^ 1) ; ::_thesis: u in ((LSeg ((f /^ 1),1)) \/ (LSeg ((f /^ 1),((len (f /^ 1)) -' 1)))) \/ (union { (LSeg ((f /^ 1),i)) where i is Element of NAT : ( 1 < i & i + 1 < len (f /^ 1) ) } ) then consider e being set such that A23: u in e and A24: e in { (LSeg ((f /^ 1),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f /^ 1) ) } by TARSKI:def_4; consider i being Element of NAT such that A25: e = LSeg ((f /^ 1),i) and A26: 1 <= i and A27: i + 1 <= len (f /^ 1) by A24; percases ( i = 1 or i + 1 = len (f /^ 1) or ( 1 < i & i + 1 < len (f /^ 1) ) ) by A26, A27, XXREAL_0:1; suppose i = 1 ; ::_thesis: u in ((LSeg ((f /^ 1),1)) \/ (LSeg ((f /^ 1),((len (f /^ 1)) -' 1)))) \/ (union { (LSeg ((f /^ 1),i)) where i is Element of NAT : ( 1 < i & i + 1 < len (f /^ 1) ) } ) then u in (LSeg ((f /^ 1),1)) \/ (LSeg ((f /^ 1),((len (f /^ 1)) -' 1))) by A23, A25, XBOOLE_0:def_3; hence u in ((LSeg ((f /^ 1),1)) \/ (LSeg ((f /^ 1),((len (f /^ 1)) -' 1)))) \/ (union { (LSeg ((f /^ 1),i)) where i is Element of NAT : ( 1 < i & i + 1 < len (f /^ 1) ) } ) by XBOOLE_0:def_3; ::_thesis: verum end; suppose i + 1 = len (f /^ 1) ; ::_thesis: u in ((LSeg ((f /^ 1),1)) \/ (LSeg ((f /^ 1),((len (f /^ 1)) -' 1)))) \/ (union { (LSeg ((f /^ 1),i)) where i is Element of NAT : ( 1 < i & i + 1 < len (f /^ 1) ) } ) then i = (len (f /^ 1)) -' 1 by NAT_D:34; then u in (LSeg ((f /^ 1),1)) \/ (LSeg ((f /^ 1),((len (f /^ 1)) -' 1))) by A23, A25, XBOOLE_0:def_3; hence u in ((LSeg ((f /^ 1),1)) \/ (LSeg ((f /^ 1),((len (f /^ 1)) -' 1)))) \/ (union { (LSeg ((f /^ 1),i)) where i is Element of NAT : ( 1 < i & i + 1 < len (f /^ 1) ) } ) by XBOOLE_0:def_3; ::_thesis: verum end; suppose ( 1 < i & i + 1 < len (f /^ 1) ) ; ::_thesis: u in ((LSeg ((f /^ 1),1)) \/ (LSeg ((f /^ 1),((len (f /^ 1)) -' 1)))) \/ (union { (LSeg ((f /^ 1),i)) where i is Element of NAT : ( 1 < i & i + 1 < len (f /^ 1) ) } ) then e in { (LSeg ((f /^ 1),i)) where i is Element of NAT : ( 1 < i & i + 1 < len (f /^ 1) ) } by A25; then u in union { (LSeg ((f /^ 1),i)) where i is Element of NAT : ( 1 < i & i + 1 < len (f /^ 1) ) } by A23, TARSKI:def_4; hence u in ((LSeg ((f /^ 1),1)) \/ (LSeg ((f /^ 1),((len (f /^ 1)) -' 1)))) \/ (union { (LSeg ((f /^ 1),i)) where i is Element of NAT : ( 1 < i & i + 1 < len (f /^ 1) ) } ) by XBOOLE_0:def_3; ::_thesis: verum end; end; end; A28: union { (LSeg ((f /^ 1),i)) where i is Element of NAT : ( 1 < i & i + 1 < len (f /^ 1) ) } c= L~ (f /^ 1) proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in union { (LSeg ((f /^ 1),i)) where i is Element of NAT : ( 1 < i & i + 1 < len (f /^ 1) ) } or u in L~ (f /^ 1) ) assume u in union { (LSeg ((f /^ 1),i)) where i is Element of NAT : ( 1 < i & i + 1 < len (f /^ 1) ) } ; ::_thesis: u in L~ (f /^ 1) then consider e being set such that A29: u in e and A30: e in { (LSeg ((f /^ 1),i)) where i is Element of NAT : ( 1 < i & i + 1 < len (f /^ 1) ) } by TARSKI:def_4; ex i being Element of NAT st ( e = LSeg ((f /^ 1),i) & 1 < i & i + 1 < len (f /^ 1) ) by A30; then e in { (LSeg ((f /^ 1),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f /^ 1) ) } ; hence u in L~ (f /^ 1) by A29, TARSKI:def_4; ::_thesis: verum end; 1 + ((len (f /^ 1)) -' 1) = len (f /^ 1) by A6, XREAL_1:235, XXREAL_0:2 .= (len f) -' 1 by A1, A4, XREAL_1:233, XXREAL_0:2 ; then A31: (LSeg (f,1)) /\ (LSeg ((f /^ 1),((len (f /^ 1)) -' 1))) = (LSeg (f,1)) /\ (LSeg (f,((len f) -' 1))) by A3, A7, NAT_D:55, SPPOL_2:4 .= {(f /. 1)} by A1, REVROT_1:30 ; 1 + 1 <= len (f /^ 1) by A6, NAT_1:13; then LSeg ((f /^ 1),1) in { (LSeg ((f /^ 1),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f /^ 1) ) } ; then A32: LSeg ((f /^ 1),1) c= L~ (f /^ 1) by ZFMISC_1:74; A33: (LSeg (f,1)) /\ (LSeg ((f /^ 1),1)) = (LSeg (f,1)) /\ (LSeg (f,(1 + 1))) by A3, SPPOL_2:4 .= {(f /. (1 + 1))} by A2, TOPREAL1:def_6 ; 1 <= (len (f /^ 1)) -' 1 by A7, NAT_D:55; then LSeg ((f /^ 1),((len (f /^ 1)) -' 1)) in { (LSeg ((f /^ 1),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f /^ 1) ) } by A8; then LSeg ((f /^ 1),((len (f /^ 1)) -' 1)) c= L~ (f /^ 1) by ZFMISC_1:74; then (LSeg ((f /^ 1),1)) \/ (LSeg ((f /^ 1),((len (f /^ 1)) -' 1))) c= L~ (f /^ 1) by A32, XBOOLE_1:8; then ((LSeg ((f /^ 1),1)) \/ (LSeg ((f /^ 1),((len (f /^ 1)) -' 1)))) \/ (union { (LSeg ((f /^ 1),i)) where i is Element of NAT : ( 1 < i & i + 1 < len (f /^ 1) ) } ) c= L~ (f /^ 1) by A28, XBOOLE_1:8; then L~ (f /^ 1) = ((LSeg ((f /^ 1),1)) \/ (LSeg ((f /^ 1),((len (f /^ 1)) -' 1)))) \/ (union { (LSeg ((f /^ 1),i)) where i is Element of NAT : ( 1 < i & i + 1 < len (f /^ 1) ) } ) by A22, XBOOLE_0:def_10; hence (LSeg (f,1)) /\ (L~ (f /^ 1)) = ((LSeg (f,1)) /\ ((LSeg ((f /^ 1),1)) \/ (LSeg ((f /^ 1),((len (f /^ 1)) -' 1))))) \/ {} by A21, XBOOLE_1:23 .= {(f /. 1)} \/ {(f /. 2)} by A33, A31, XBOOLE_1:23 .= {(f /. 1),(f /. 2)} by ENUMSET1:1 ; ::_thesis: verum end; theorem Th28: :: TOPREAL8:28 for j being Element of NAT for f, g being FinSequence of (TOP-REAL 2) st j < len f holds LSeg ((f ^' g),j) = LSeg (f,j) proof let j be Element of NAT ; ::_thesis: for f, g being FinSequence of (TOP-REAL 2) st j < len f holds LSeg ((f ^' g),j) = LSeg (f,j) let f, g be FinSequence of (TOP-REAL 2); ::_thesis: ( j < len f implies LSeg ((f ^' g),j) = LSeg (f,j) ) assume A1: j < len f ; ::_thesis: LSeg ((f ^' g),j) = LSeg (f,j) percases ( j < 1 or 1 <= j ) ; supposeA2: j < 1 ; ::_thesis: LSeg ((f ^' g),j) = LSeg (f,j) hence LSeg ((f ^' g),j) = {} by TOPREAL1:def_3 .= LSeg (f,j) by A2, TOPREAL1:def_3 ; ::_thesis: verum end; supposeA3: 1 <= j ; ::_thesis: LSeg ((f ^' g),j) = LSeg (f,j) then A4: (f ^' g) /. j = f /. j by A1, GRAPH_2:57; A5: j + 1 <= len f by A1, NAT_1:13; then A6: (f ^' g) /. (j + 1) = f /. (j + 1) by GRAPH_2:57, NAT_1:11; len f <= len (f ^' g) by Th7; then j + 1 <= len (f ^' g) by A5, XXREAL_0:2; hence LSeg ((f ^' g),j) = LSeg (((f ^' g) /. j),((f ^' g) /. (j + 1))) by A3, TOPREAL1:def_3 .= LSeg (f,j) by A3, A4, A5, A6, TOPREAL1:def_3 ; ::_thesis: verum end; end; end; theorem Th29: :: TOPREAL8:29 for j being Element of NAT for f, g being non empty FinSequence of (TOP-REAL 2) st 1 <= j & j + 1 < len g holds LSeg ((f ^' g),((len f) + j)) = LSeg (g,(j + 1)) proof let j be Element of NAT ; ::_thesis: for f, g being non empty FinSequence of (TOP-REAL 2) st 1 <= j & j + 1 < len g holds LSeg ((f ^' g),((len f) + j)) = LSeg (g,(j + 1)) let f, g be non empty FinSequence of (TOP-REAL 2); ::_thesis: ( 1 <= j & j + 1 < len g implies LSeg ((f ^' g),((len f) + j)) = LSeg (g,(j + 1)) ) assume that A1: 1 <= j and A2: j + 1 < len g ; ::_thesis: LSeg ((f ^' g),((len f) + j)) = LSeg (g,(j + 1)) A3: (f ^' g) /. (((len f) + j) + 1) = (f ^' g) /. ((len f) + (j + 1)) .= g /. ((j + 1) + 1) by A2, GRAPH_2:58, NAT_1:11 ; j + 0 <= j + 1 by XREAL_1:6; then j < len g by A2, XXREAL_0:2; then A4: (f ^' g) /. ((len f) + j) = g /. (j + 1) by A1, GRAPH_2:58; A5: 1 <= j + 1 by NAT_1:11; (len f) + (j + 1) < (len f) + (len g) by A2, XREAL_1:6; then ((len f) + j) + 1 < (len (f ^' g)) + 1 by GRAPH_2:13; then A6: ((len f) + j) + 1 <= len (f ^' g) by NAT_1:13; A7: (j + 1) + 1 <= len g by A2, NAT_1:13; j <= (len f) + j by NAT_1:11; then 1 <= (len f) + j by A1, XXREAL_0:2; hence LSeg ((f ^' g),((len f) + j)) = LSeg (((f ^' g) /. ((len f) + j)),((f ^' g) /. (((len f) + j) + 1))) by A6, TOPREAL1:def_3 .= LSeg (g,(j + 1)) by A4, A5, A3, A7, TOPREAL1:def_3 ; ::_thesis: verum end; theorem Th30: :: TOPREAL8:30 for f being non empty FinSequence of (TOP-REAL 2) for g being non trivial FinSequence of (TOP-REAL 2) st f /. (len f) = g /. 1 holds LSeg ((f ^' g),(len f)) = LSeg (g,1) proof let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: for g being non trivial FinSequence of (TOP-REAL 2) st f /. (len f) = g /. 1 holds LSeg ((f ^' g),(len f)) = LSeg (g,1) A1: 1 <= len f by NAT_1:14; let g be non trivial FinSequence of (TOP-REAL 2); ::_thesis: ( f /. (len f) = g /. 1 implies LSeg ((f ^' g),(len f)) = LSeg (g,1) ) assume f /. (len f) = g /. 1 ; ::_thesis: LSeg ((f ^' g),(len f)) = LSeg (g,1) then A2: (f ^' g) /. ((len f) + 0) = g /. (0 + 1) by A1, GRAPH_2:57; A3: 1 < len g by Th2; then A4: (f ^' g) /. (((len f) + 0) + 1) = g /. ((0 + 1) + 1) by GRAPH_2:58; A5: 1 + 1 <= len g by A3, NAT_1:13; ((len f) + 0) + 1 < (len f) + (len g) by A3, XREAL_1:6; then ((len f) + 0) + 1 < (len (f ^' g)) + 1 by GRAPH_2:13; then ((len f) + 0) + 1 <= len (f ^' g) by NAT_1:13; hence LSeg ((f ^' g),(len f)) = LSeg (((f ^' g) /. ((len f) + 0)),((f ^' g) /. (((len f) + 0) + 1))) by A1, TOPREAL1:def_3 .= LSeg (g,1) by A2, A4, A5, TOPREAL1:def_3 ; ::_thesis: verum end; theorem Th31: :: TOPREAL8:31 for j being Element of NAT for f being non empty FinSequence of (TOP-REAL 2) for g being non trivial FinSequence of (TOP-REAL 2) st j + 1 < len g & f /. (len f) = g /. 1 holds LSeg ((f ^' g),((len f) + j)) = LSeg (g,(j + 1)) proof let j be Element of NAT ; ::_thesis: for f being non empty FinSequence of (TOP-REAL 2) for g being non trivial FinSequence of (TOP-REAL 2) st j + 1 < len g & f /. (len f) = g /. 1 holds LSeg ((f ^' g),((len f) + j)) = LSeg (g,(j + 1)) let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: for g being non trivial FinSequence of (TOP-REAL 2) st j + 1 < len g & f /. (len f) = g /. 1 holds LSeg ((f ^' g),((len f) + j)) = LSeg (g,(j + 1)) let g be non trivial FinSequence of (TOP-REAL 2); ::_thesis: ( j + 1 < len g & f /. (len f) = g /. 1 implies LSeg ((f ^' g),((len f) + j)) = LSeg (g,(j + 1)) ) assume that A1: j + 1 < len g and A2: f /. (len f) = g /. 1 ; ::_thesis: LSeg ((f ^' g),((len f) + j)) = LSeg (g,(j + 1)) percases ( j = 0 or 1 <= j ) by NAT_1:14; suppose j = 0 ; ::_thesis: LSeg ((f ^' g),((len f) + j)) = LSeg (g,(j + 1)) hence LSeg ((f ^' g),((len f) + j)) = LSeg (g,(j + 1)) by A2, Th30; ::_thesis: verum end; suppose 1 <= j ; ::_thesis: LSeg ((f ^' g),((len f) + j)) = LSeg (g,(j + 1)) hence LSeg ((f ^' g),((len f) + j)) = LSeg (g,(j + 1)) by A1, Th29; ::_thesis: verum end; end; end; theorem Th32: :: TOPREAL8:32 for f being non empty unfolded s.n.c. FinSequence of (TOP-REAL 2) for i being Element of NAT st 1 <= i & i < len f holds (LSeg (f,i)) /\ (rng f) = {(f /. i),(f /. (i + 1))} proof let f be non empty unfolded s.n.c. FinSequence of (TOP-REAL 2); ::_thesis: for i being Element of NAT st 1 <= i & i < len f holds (LSeg (f,i)) /\ (rng f) = {(f /. i),(f /. (i + 1))} let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len f implies (LSeg (f,i)) /\ (rng f) = {(f /. i),(f /. (i + 1))} ) assume that A1: 1 <= i and A2: i < len f ; ::_thesis: (LSeg (f,i)) /\ (rng f) = {(f /. i),(f /. (i + 1))} A3: i in dom f by A1, A2, FINSEQ_3:25; then f /. i = f . i by PARTFUN1:def_6; then A4: f /. i in rng f by A3, FUNCT_1:3; assume A5: (LSeg (f,i)) /\ (rng f) <> {(f /. i),(f /. (i + 1))} ; ::_thesis: contradiction A6: i + 1 <= len f by A2, NAT_1:13; then f /. i in LSeg (f,i) by A1, TOPREAL1:21; then A7: f /. i in (LSeg (f,i)) /\ (rng f) by A4, XBOOLE_0:def_4; A8: 1 < i + 1 by A1, XREAL_1:29; then A9: i + 1 in dom f by A6, FINSEQ_3:25; then f /. (i + 1) = f . (i + 1) by PARTFUN1:def_6; then A10: f /. (i + 1) in rng f by A9, FUNCT_1:3; f /. (i + 1) in LSeg (f,i) by A1, A6, TOPREAL1:21; then f /. (i + 1) in (LSeg (f,i)) /\ (rng f) by A10, XBOOLE_0:def_4; then {(f /. i),(f /. (i + 1))} c= (LSeg (f,i)) /\ (rng f) by A7, ZFMISC_1:32; then not (LSeg (f,i)) /\ (rng f) c= {(f /. i),(f /. (i + 1))} by A5, XBOOLE_0:def_10; then consider x being set such that A11: x in (LSeg (f,i)) /\ (rng f) and A12: not x in {(f /. i),(f /. (i + 1))} by TARSKI:def_3; reconsider x = x as Point of (TOP-REAL 2) by A11; A13: x in LSeg (f,i) by A11, XBOOLE_0:def_4; x in rng f by A11, XBOOLE_0:def_4; then consider j being set such that A14: j in dom f and A15: x = f . j by FUNCT_1:def_3; A16: x = f /. j by A14, A15, PARTFUN1:def_6; reconsider j = j as Element of NAT by A14; A17: 1 <= j by A14, FINSEQ_3:25; reconsider j = j as Element of NAT ; A18: x <> f /. i by A12, TARSKI:def_2; then A19: j <> i by A14, A15, PARTFUN1:def_6; A20: x <> f /. (i + 1) by A12, TARSKI:def_2; then A21: j <> i + 1 by A14, A15, PARTFUN1:def_6; now__::_thesis:_contradiction percases ( j + 1 > len f or ( i < j & j + 1 <= len f ) or j < i ) by A19, XXREAL_0:1; supposeA22: j + 1 > len f ; ::_thesis: contradiction A23: j <= len f by A14, FINSEQ_3:25; len f <= j by A22, NAT_1:13; then A24: j = len f by A23, XXREAL_0:1; consider k being Nat such that A25: len f = 1 + k by A6, A8, NAT_1:10, XXREAL_0:2; reconsider k = k as Element of NAT by ORDINAL1:def_12; 1 < len f by A6, A8, XXREAL_0:2; then 1 <= k by A25, NAT_1:13; then A26: x in LSeg (f,k) by A16, A24, A25, TOPREAL1:21; i <= k by A2, A25, NAT_1:13; then i < k by A20, A16, A24, A25, XXREAL_0:1; then A27: i + 1 <= k by NAT_1:13; now__::_thesis:_contradiction percases ( i + 1 = k or i + 1 < k ) by A27, XXREAL_0:1; supposeA28: i + 1 = k ; ::_thesis: contradiction then i + (1 + 1) <= len f by A25; then (LSeg (f,i)) /\ (LSeg (f,k)) = {(f /. (i + 1))} by A1, A28, TOPREAL1:def_6; then x in {(f /. (i + 1))} by A13, A26, XBOOLE_0:def_4; hence contradiction by A20, TARSKI:def_1; ::_thesis: verum end; suppose i + 1 < k ; ::_thesis: contradiction then LSeg (f,i) misses LSeg (f,k) by TOPREAL1:def_7; hence contradiction by A13, A26, XBOOLE_0:3; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; supposethat A29: i < j and A30: j + 1 <= len f ; ::_thesis: contradiction i + 1 <= j by A29, NAT_1:13; then i + 1 < j by A21, XXREAL_0:1; then A31: LSeg (f,i) misses LSeg (f,j) by TOPREAL1:def_7; x in LSeg (f,j) by A16, A17, A30, TOPREAL1:21; hence contradiction by A13, A31, XBOOLE_0:3; ::_thesis: verum end; supposeA32: j < i ; ::_thesis: contradiction then j + 1 <= i + 1 by XREAL_1:6; then j + 1 <= len f by A6, XXREAL_0:2; then x in LSeg (f,j) by A16, A17, TOPREAL1:21; then A33: x in (LSeg (f,i)) /\ (LSeg (f,j)) by A13, XBOOLE_0:def_4; A34: j + 1 <= i by A32, NAT_1:13; now__::_thesis:_contradiction percases ( j + 1 = i or j + 1 < i ) by A34, XXREAL_0:1; supposeA35: j + 1 = i ; ::_thesis: contradiction then (j + 1) + 1 <= len f by A2, NAT_1:13; then j + (1 + 1) <= len f ; then (LSeg (f,i)) /\ (LSeg (f,j)) = {(f /. i)} by A17, A35, TOPREAL1:def_6; hence contradiction by A18, A33, TARSKI:def_1; ::_thesis: verum end; suppose j + 1 < i ; ::_thesis: contradiction then LSeg (f,j) misses LSeg (f,i) by TOPREAL1:def_7; hence contradiction by A33, XBOOLE_0:4; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; Lm2: for f being non empty one-to-one unfolded s.n.c. FinSequence of (TOP-REAL 2) for g being non trivial one-to-one unfolded s.n.c. FinSequence of (TOP-REAL 2) for i, j being Element of NAT st i < len f & 1 < i holds for x being Point of (TOP-REAL 2) st x in (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) holds x <> f /. 1 proof let f be non empty one-to-one unfolded s.n.c. FinSequence of (TOP-REAL 2); ::_thesis: for g being non trivial one-to-one unfolded s.n.c. FinSequence of (TOP-REAL 2) for i, j being Element of NAT st i < len f & 1 < i holds for x being Point of (TOP-REAL 2) st x in (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) holds x <> f /. 1 let g be non trivial one-to-one unfolded s.n.c. FinSequence of (TOP-REAL 2); ::_thesis: for i, j being Element of NAT st i < len f & 1 < i holds for x being Point of (TOP-REAL 2) st x in (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) holds x <> f /. 1 let i, j be Element of NAT ; ::_thesis: ( i < len f & 1 < i implies for x being Point of (TOP-REAL 2) st x in (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) holds x <> f /. 1 ) assume that A1: i < len f and A2: 1 < i ; ::_thesis: for x being Point of (TOP-REAL 2) st x in (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) holds x <> f /. 1 A3: 1 < i + 1 by A2, XREAL_1:29; A4: (LSeg (f,i)) /\ (rng f) = {(f /. i),(f /. (i + 1))} by A1, A2, Th32; i + 1 <= len f by A1, NAT_1:13; then A5: i + 1 in dom f by A3, FINSEQ_3:25; A6: LSeg ((f ^' g),i) = LSeg (f,i) by A1, Th28; let x be Point of (TOP-REAL 2); ::_thesis: ( x in (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) implies x <> f /. 1 ) assume x in (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) ; ::_thesis: x <> f /. 1 then A7: x in LSeg (f,i) by A6, XBOOLE_0:def_4; A8: 1 in dom f by FINSEQ_5:6; assume A9: x = f /. 1 ; ::_thesis: contradiction x = f . 1 by A9, A8, PARTFUN1:def_6; then x in rng f by A8, FUNCT_1:3; then x in (LSeg (f,i)) /\ (rng f) by A7, XBOOLE_0:def_4; then A10: ( x = f /. i or x = f /. (i + 1) ) by A4, TARSKI:def_2; i in dom f by A1, A2, FINSEQ_3:25; hence contradiction by A2, A9, A8, A10, A3, A5, PARTFUN2:10; ::_thesis: verum end; Lm3: for f being non empty one-to-one unfolded s.n.c. FinSequence of (TOP-REAL 2) for g being non trivial one-to-one unfolded s.n.c. FinSequence of (TOP-REAL 2) for i, j being Element of NAT st j > len f & j + 1 < len (f ^' g) holds for x being Point of (TOP-REAL 2) st x in (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) holds x <> g /. (len g) proof let f be non empty one-to-one unfolded s.n.c. FinSequence of (TOP-REAL 2); ::_thesis: for g being non trivial one-to-one unfolded s.n.c. FinSequence of (TOP-REAL 2) for i, j being Element of NAT st j > len f & j + 1 < len (f ^' g) holds for x being Point of (TOP-REAL 2) st x in (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) holds x <> g /. (len g) let g be non trivial one-to-one unfolded s.n.c. FinSequence of (TOP-REAL 2); ::_thesis: for i, j being Element of NAT st j > len f & j + 1 < len (f ^' g) holds for x being Point of (TOP-REAL 2) st x in (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) holds x <> g /. (len g) let i, j be Element of NAT ; ::_thesis: ( j > len f & j + 1 < len (f ^' g) implies for x being Point of (TOP-REAL 2) st x in (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) holds x <> g /. (len g) ) assume that A1: j > len f and A2: j + 1 < len (f ^' g) ; ::_thesis: for x being Point of (TOP-REAL 2) st x in (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) holds x <> g /. (len g) consider k being Nat such that A3: j = (len f) + k by A1, NAT_1:10; (len (f ^' g)) + 1 = (len f) + (len g) by GRAPH_2:13; then A4: (j + 1) + 1 < (len f) + (len g) by A2, XREAL_1:6; reconsider k = k as Element of NAT by ORDINAL1:def_12; (j + 1) + 1 = (len f) + ((k + 1) + 1) by A3; then A5: (k + 1) + 1 < len g by A4, XREAL_1:6; 1 <= (k + 1) + 1 by NAT_1:11; then A6: (k + 1) + 1 in dom g by A5, FINSEQ_3:25; let x be Point of (TOP-REAL 2); ::_thesis: ( x in (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) implies x <> g /. (len g) ) assume A7: x in (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) ; ::_thesis: x <> g /. (len g) A8: len g in dom g by FINSEQ_5:6; A9: k + 1 <= (k + 1) + 1 by NAT_1:11; then A10: k + 1 < len g by A5, XXREAL_0:2; then A11: (LSeg (g,(k + 1))) /\ (rng g) = {(g /. (k + 1)),(g /. ((k + 1) + 1))} by Th32, NAT_1:11; assume A12: x = g /. (len g) ; ::_thesis: contradiction x = g . (len g) by A12, A8, PARTFUN1:def_6; then A13: x in rng g by A8, FUNCT_1:3; 1 <= k + 1 by NAT_1:11; then A14: k + 1 in dom g by A10, FINSEQ_3:25; (len f) + 0 < (len f) + k by A1, A3; then 0 < k ; then 0 + 1 <= k by NAT_1:13; then LSeg ((f ^' g),j) = LSeg (g,(k + 1)) by A3, A10, Th29; then x in LSeg (g,(k + 1)) by A7, XBOOLE_0:def_4; then x in (LSeg (g,(k + 1))) /\ (rng g) by A13, XBOOLE_0:def_4; then ( x = g /. (k + 1) or x = g /. ((k + 1) + 1) ) by A11, TARSKI:def_2; hence contradiction by A12, A5, A9, A8, A14, A6, PARTFUN2:10; ::_thesis: verum end; theorem Th33: :: TOPREAL8:33 for f, g being non trivial one-to-one unfolded s.n.c. FinSequence of (TOP-REAL 2) st (L~ f) /\ (L~ g) = {(f /. 1),(g /. 1)} & f /. 1 = g /. (len g) & g /. 1 = f /. (len f) holds f ^' g is s.c.c. proof let f, g be non trivial one-to-one unfolded s.n.c. FinSequence of (TOP-REAL 2); ::_thesis: ( (L~ f) /\ (L~ g) = {(f /. 1),(g /. 1)} & f /. 1 = g /. (len g) & g /. 1 = f /. (len f) implies f ^' g is s.c.c. ) assume that A1: (L~ f) /\ (L~ g) = {(f /. 1),(g /. 1)} and A2: f /. 1 = g /. (len g) and A3: g /. 1 = f /. (len f) ; ::_thesis: f ^' g is s.c.c. A4: for i being Element of NAT st 1 <= i & i < len f holds f /. i <> g /. 1 proof A5: len f in dom f by FINSEQ_5:6; then A6: f /. (len f) = f . (len f) by PARTFUN1:def_6; let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len f implies f /. i <> g /. 1 ) assume that A7: 1 <= i and A8: i < len f ; ::_thesis: f /. i <> g /. 1 A9: i in dom f by A7, A8, FINSEQ_3:25; then f /. i = f . i by PARTFUN1:def_6; hence f /. i <> g /. 1 by A3, A8, A9, A5, A6, FUNCT_1:def_4; ::_thesis: verum end; A10: (len (f ^' g)) + 1 = (len f) + (len g) by GRAPH_2:13; A11: (len (g ^' f)) + 1 = (len f) + (len g) by GRAPH_2:13; let i be Element of NAT ; :: according to GOBOARD5:def_4 ::_thesis: for b1 being Element of NAT holds ( b1 <= i + 1 or ( ( i <= 1 or len (f ^' g) <= b1 ) & len (f ^' g) <= b1 + 1 ) or LSeg ((f ^' g),i) misses LSeg ((f ^' g),b1) ) let j be Element of NAT ; ::_thesis: ( j <= i + 1 or ( ( i <= 1 or len (f ^' g) <= j ) & len (f ^' g) <= j + 1 ) or LSeg ((f ^' g),i) misses LSeg ((f ^' g),j) ) assume that A12: i + 1 < j and A13: ( ( i > 1 & j < len (f ^' g) ) or j + 1 < len (f ^' g) ) ; ::_thesis: LSeg ((f ^' g),i) misses LSeg ((f ^' g),j) A14: i < j by A12, NAT_1:13; j <= j + 1 by NAT_1:11; then A15: j < len (f ^' g) by A13, XXREAL_0:2; percases ( i = 0 or j < len f or i >= len f or ( j >= len f & i < len f & 1 <= i ) ) by NAT_1:14; suppose i = 0 ; ::_thesis: LSeg ((f ^' g),i) misses LSeg ((f ^' g),j) then LSeg ((f ^' g),i) = {} by TOPREAL1:def_3; then (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) = {} ; hence LSeg ((f ^' g),i) misses LSeg ((f ^' g),j) by XBOOLE_0:def_7; ::_thesis: verum end; supposeA16: j < len f ; ::_thesis: LSeg ((f ^' g),i) misses LSeg ((f ^' g),j) then i < len f by A14, XXREAL_0:2; then A17: LSeg ((f ^' g),i) = LSeg (f,i) by Th28; LSeg ((f ^' g),j) = LSeg (f,j) by A16, Th28; hence LSeg ((f ^' g),i) misses LSeg ((f ^' g),j) by A12, A17, TOPREAL1:def_7; ::_thesis: verum end; supposeA18: i >= len f ; ::_thesis: LSeg ((f ^' g),i) misses LSeg ((f ^' g),j) then consider m being Nat such that A19: i = (len f) + m by NAT_1:10; consider n being Nat such that A20: j = (len f) + n by A14, A18, NAT_1:10, XXREAL_0:2; reconsider m = m, n = n as Element of NAT by ORDINAL1:def_12; A21: 1 <= m + 1 by NAT_1:11; j + 1 < (len f) + (len g) by A15, A10, XREAL_1:6; then (len f) + (n + 1) < (len f) + (len g) by A20; then A22: n + 1 < len g by XREAL_1:6; A23: m < n by A14, A19, A20, XREAL_1:6; then m + 1 <= n by NAT_1:13; then 1 <= n by A21, XXREAL_0:2; then A24: LSeg ((f ^' g),j) = LSeg (g,(n + 1)) by A20, A22, Th29; (i + 1) + 1 < j + 1 by A12, XREAL_1:6; then (len f) + (m + (1 + 1)) < (len f) + (n + 1) by A19, A20; then A25: (m + 1) + 1 < n + 1 by XREAL_1:6; m + 1 < n + 1 by A23, XREAL_1:6; then m + 1 < len g by A22, XXREAL_0:2; then LSeg ((f ^' g),i) = LSeg (g,(m + 1)) by A3, A19, Th31; hence LSeg ((f ^' g),i) misses LSeg ((f ^' g),j) by A24, A25, TOPREAL1:def_7; ::_thesis: verum end; supposethat A26: j >= len f and A27: i < len f and A28: 1 <= i ; ::_thesis: LSeg ((f ^' g),i) misses LSeg ((f ^' g),j) consider k being Nat such that A29: j = (len f) + k by A26, NAT_1:10; reconsider k = k as Element of NAT by ORDINAL1:def_12; j + 1 < (len f) + (len g) by A15, A10, XREAL_1:6; then (len f) + (k + 1) < (len f) + (len g) by A29; then k + 1 < len g by XREAL_1:6; then LSeg ((f ^' g),j) = LSeg (g,(k + 1)) by A3, A29, Th31; then A30: LSeg ((f ^' g),j) c= L~ g by TOPREAL3:19; assume LSeg ((f ^' g),i) meets LSeg ((f ^' g),j) ; ::_thesis: contradiction then consider x being set such that A31: x in (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) by XBOOLE_0:4; LSeg ((f ^' g),i) = LSeg (f,i) by A27, Th28; then LSeg ((f ^' g),i) c= L~ f by TOPREAL3:19; then A32: (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) c= {(f /. 1),(g /. 1)} by A1, A30, XBOOLE_1:27; now__::_thesis:_contradiction percases ( ( 1 < i & x = f /. 1 ) or ( j > (len f) + 0 & x = g /. 1 ) or ( j = len f & x = g /. 1 ) or ( j > len f & x = f /. 1 & j + 1 < len (f ^' g) ) or ( j = len f & x = f /. 1 & j + 1 < len (f ^' g) ) ) by A13, A26, A31, A32, TARSKI:def_2, XXREAL_0:1; suppose ( 1 < i & x = f /. 1 ) ; ::_thesis: contradiction hence contradiction by A27, A31, Lm2; ::_thesis: verum end; supposethat A33: j > (len f) + 0 and A34: x = g /. 1 ; ::_thesis: contradiction j + 0 < j + 1 by XREAL_1:6; then A35: len f < j + 1 by A33, XXREAL_0:2; j + 1 < (len (g ^' f)) + 1 by A15, A10, A11, XREAL_1:6; then (j + 1) -' (len f) < len g by A11, A35, NAT_D:54; then A36: (j -' (len f)) + 1 < len g by A33, NAT_D:38; A37: Rotate ((f ^' g),(g /. 1)) = g ^' f by A3, A4, Th18; 0 < j -' (len f) by A33, NAT_D:52; then A38: 0 + 1 < (j -' (len f)) + 1 by XREAL_1:6; A39: len f in dom f by FINSEQ_5:6; then f . (len f) = f /. (len f) by PARTFUN1:def_6; then A40: g /. 1 in rng f by A3, A39, FUNCT_1:3; then A41: (g /. 1) .. (f ^' g) = (g /. 1) .. f by Th8 .= len f by A3, Th6 ; A42: rng f c= rng (f ^' g) by Th10; then A43: LSeg ((f ^' g),j) = LSeg ((Rotate ((f ^' g),(g /. 1))),((j -' ((g /. 1) .. (f ^' g))) + 1)) by A15, A33, A40, A41, REVROT_1:25; f ^' g is circular by A2, Th11; then LSeg ((f ^' g),i) = LSeg ((Rotate ((f ^' g),(g /. 1))),((i + (len (f ^' g))) -' ((g /. 1) .. (f ^' g)))) by A27, A28, A40, A41, A42, REVROT_1:32; hence contradiction by A31, A34, A37, A41, A43, A36, A38, Lm2; ::_thesis: verum end; supposethat A44: j = len f and A45: x = g /. 1 ; ::_thesis: contradiction i <= i + 1 by NAT_1:11; then i < j by A12, XXREAL_0:2; then LSeg ((f ^' g),i) = LSeg (f,i) by A44, Th28; then A46: f /. (len f) in LSeg (f,i) by A3, A31, A45, XBOOLE_0:def_4; i <= i + 1 by NAT_1:11; then i < len f by A12, A44, XXREAL_0:2; then A47: i in dom f by A28, FINSEQ_3:25; 1 <= i + 1 by NAT_1:11; then i + 1 in dom f by A12, A44, FINSEQ_3:25; hence contradiction by A12, A44, A47, A46, GOBOARD2:2; ::_thesis: verum end; supposethat A48: j > len f and A49: x = f /. 1 and A50: j + 1 < len (f ^' g) ; ::_thesis: contradiction thus contradiction by A2, A31, A48, A49, A50, Lm3; ::_thesis: verum end; supposethat A51: j = len f and A52: x = f /. 1 and A53: j + 1 < len (f ^' g) ; ::_thesis: contradiction 0 + 1 < len g by Th2; then LSeg ((f ^' g),((len f) + 0)) = LSeg (g,(0 + 1)) by A3, Th31; then A54: g /. (len g) in LSeg (g,1) by A2, A31, A51, A52, XBOOLE_0:def_4; (j + 1) + 1 < (len f) + (len g) by A10, A53, XREAL_1:6; then A55: j + (1 + 1) < (len f) + (len g) ; then 1 + 1 < len g by A51, XREAL_1:6; then A56: 1 + 1 in dom g by FINSEQ_3:25; 1 in dom g by FINSEQ_5:6; hence contradiction by A51, A55, A54, A56, GOBOARD2:2; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; end; end; theorem Th34: :: TOPREAL8:34 for f, g being FinSequence of (TOP-REAL 2) st f is unfolded & g is unfolded & f /. (len f) = g /. 1 & (LSeg (f,((len f) -' 1))) /\ (LSeg (g,1)) = {(f /. (len f))} holds f ^' g is unfolded proof let f, g be FinSequence of (TOP-REAL 2); ::_thesis: ( f is unfolded & g is unfolded & f /. (len f) = g /. 1 & (LSeg (f,((len f) -' 1))) /\ (LSeg (g,1)) = {(f /. (len f))} implies f ^' g is unfolded ) assume that A1: f is unfolded and A2: g is unfolded and A3: f /. (len f) = g /. 1 and A4: (LSeg (f,((len f) -' 1))) /\ (LSeg (g,1)) = {(f /. (len f))} ; ::_thesis: f ^' g is unfolded set c = ((1 + 1),(len g)) -cut g; set k = (len f) -' 1; reconsider g9 = g as unfolded FinSequence of (TOP-REAL 2) by A2; A5: ((1 + 1),(len g)) -cut g = g9 /^ 1 by Th13; A6: f ^' g = f ^ (((1 + 1),(len g)) -cut g) by GRAPH_2:def_2; percases ( f is empty or len g = 0 or len g = 1 or ( not f is empty & len g = 1 + 1 ) or ( not f is empty & 2 < len g ) ) by NAT_1:26; suppose f is empty ; ::_thesis: f ^' g is unfolded hence f ^' g is unfolded by A6, A5, FINSEQ_1:34; ::_thesis: verum end; suppose len g = 0 ; ::_thesis: f ^' g is unfolded then g = {} ; then ((1 + 1),(len g)) -cut g = <*> the carrier of (TOP-REAL 2) by A5, FINSEQ_6:80; hence f ^' g is unfolded by A1, A6, FINSEQ_1:34; ::_thesis: verum end; suppose len g = 1 ; ::_thesis: f ^' g is unfolded then ((1 + 1),(len g)) -cut g = {} by A5, REVROT_1:2; hence f ^' g is unfolded by A1, A6, FINSEQ_1:34; ::_thesis: verum end; supposethat A7: not f is empty and A8: len g = 1 + 1 ; ::_thesis: f ^' g is unfolded A9: ((len f) -' 1) + 1 = len f by A7, NAT_1:14, XREAL_1:235; g | (len g) = g by FINSEQ_1:58; then g = <*(g /. 1),(g /. 2)*> by A8, FINSEQ_5:81; then A10: f ^' g = f ^ <*(g /. 2)*> by A6, A5, FINSEQ_6:46; 1 <= (len g) - 1 by A8; then 1 <= len (g /^ 1) by A8, RFINSEQ:def_1; then A11: 1 in dom (g /^ 1) by FINSEQ_3:25; then A12: (((1 + 1),(len g)) -cut g) /. 1 = (g /^ 1) . 1 by A5, PARTFUN1:def_6 .= g . (1 + 1) by A8, A11, RFINSEQ:def_1 .= g /. (1 + 1) by A8, FINSEQ_4:15 ; then LSeg (g,1) = LSeg ((f /. (len f)),((((1 + 1),(len g)) -cut g) /. 1)) by A3, A8, TOPREAL1:def_3; hence f ^' g is unfolded by A1, A4, A9, A10, A12, SPPOL_2:30; ::_thesis: verum end; supposethat A13: not f is empty and A14: 2 < len g ; ::_thesis: f ^' g is unfolded A15: 1 <= len g by A14, XXREAL_0:2; then A16: LSeg ((g /^ 1),1) = LSeg (g,(1 + 1)) by SPPOL_2:4; 1 + 1 <= len g by A14; then 1 <= (len g) - 1 by XREAL_1:19; then 1 <= len (g /^ 1) by A15, RFINSEQ:def_1; then A17: 1 in dom (g /^ 1) by FINSEQ_3:25; then A18: (((1 + 1),(len g)) -cut g) /. 1 = (g /^ 1) . 1 by A5, PARTFUN1:def_6 .= g . (1 + 1) by A15, A17, RFINSEQ:def_1 .= g /. (1 + 1) by A14, FINSEQ_4:15 ; then A19: LSeg (g,1) = LSeg ((f /. (len f)),((((1 + 1),(len g)) -cut g) /. 1)) by A3, A14, TOPREAL1:def_3; A20: ((len f) -' 1) + 1 = len f by A13, NAT_1:14, XREAL_1:235; 1 + 2 <= len g by A14, NAT_1:13; then (LSeg (g,1)) /\ (LSeg ((((1 + 1),(len g)) -cut g),1)) = {((((1 + 1),(len g)) -cut g) /. 1)} by A5, A18, A16, TOPREAL1:def_6; hence f ^' g is unfolded by A1, A4, A6, A5, A20, A19, SPPOL_2:31; ::_thesis: verum end; end; end; theorem Th35: :: TOPREAL8:35 for f, g being FinSequence of (TOP-REAL 2) st not f is empty & not g is trivial & f /. (len f) = g /. 1 holds L~ (f ^' g) = (L~ f) \/ (L~ g) proof let f, g be FinSequence of (TOP-REAL 2); ::_thesis: ( not f is empty & not g is trivial & f /. (len f) = g /. 1 implies L~ (f ^' g) = (L~ f) \/ (L~ g) ) assume that A1: not f is empty and A2: not g is trivial and A3: f /. (len f) = g /. 1 ; ::_thesis: L~ (f ^' g) = (L~ f) \/ (L~ g) set c = ((1 + 1),(len g)) -cut g; A4: ((1 + 1),(len g)) -cut g = g /^ 1 by Th13; A5: len g > 1 by A2, Th2; then len (((1 + 1),(len g)) -cut g) = (len g) - 1 by A4, RFINSEQ:def_1; then len (((1 + 1),(len g)) -cut g) > 1 - 1 by A5, XREAL_1:9; then A6: not ((1 + 1),(len g)) -cut g is empty ; not g is empty by A2; then g = <*(g /. 1)*> ^ (((1 + 1),(len g)) -cut g) by A4, FINSEQ_5:29; then A7: (LSeg ((g /. 1),((((1 + 1),(len g)) -cut g) /. 1))) \/ (L~ (((1 + 1),(len g)) -cut g)) = L~ g by A6, SPPOL_2:20; L~ (f ^ (((1 + 1),(len g)) -cut g)) = ((L~ f) \/ (LSeg ((f /. (len f)),((((1 + 1),(len g)) -cut g) /. 1)))) \/ (L~ (((1 + 1),(len g)) -cut g)) by A1, A6, SPPOL_2:23 .= (L~ f) \/ ((LSeg ((g /. 1),((((1 + 1),(len g)) -cut g) /. 1))) \/ (L~ (((1 + 1),(len g)) -cut g))) by A3, XBOOLE_1:4 ; hence L~ (f ^' g) = (L~ f) \/ (L~ g) by A7, GRAPH_2:def_2; ::_thesis: verum end; theorem :: TOPREAL8:36 for G being Go-board for f being FinSequence of (TOP-REAL 2) st ( for n being Nat st n in dom f holds ex i, j being Nat st ( [i,j] in Indices G & f /. n = G * (i,j) ) ) & not f is constant & f is circular & f is unfolded & f is s.c.c. & f is special & len f > 4 holds ex g being FinSequence of (TOP-REAL 2) st ( g is_sequence_on G & g is unfolded & g is s.c.c. & g is special & L~ f = L~ g & f /. 1 = g /. 1 & f /. (len f) = g /. (len g) & len f <= len g ) proof let G be Go-board; ::_thesis: for f being FinSequence of (TOP-REAL 2) st ( for n being Nat st n in dom f holds ex i, j being Nat st ( [i,j] in Indices G & f /. n = G * (i,j) ) ) & not f is constant & f is circular & f is unfolded & f is s.c.c. & f is special & len f > 4 holds ex g being FinSequence of (TOP-REAL 2) st ( g is_sequence_on G & g is unfolded & g is s.c.c. & g is special & L~ f = L~ g & f /. 1 = g /. 1 & f /. (len f) = g /. (len g) & len f <= len g ) let f be FinSequence of (TOP-REAL 2); ::_thesis: ( ( for n being Nat st n in dom f holds ex i, j being Nat st ( [i,j] in Indices G & f /. n = G * (i,j) ) ) & not f is constant & f is circular & f is unfolded & f is s.c.c. & f is special & len f > 4 implies ex g being FinSequence of (TOP-REAL 2) st ( g is_sequence_on G & g is unfolded & g is s.c.c. & g is special & L~ f = L~ g & f /. 1 = g /. 1 & f /. (len f) = g /. (len g) & len f <= len g ) ) assume that A1: for n being Nat st n in dom f holds ex i, j being Nat st ( [i,j] in Indices G & f /. n = G * (i,j) ) and A2: ( not f is constant & f is circular & f is unfolded ) and A3: f is s.c.c. and A4: f is special and A5: len f > 4 ; ::_thesis: ex g being FinSequence of (TOP-REAL 2) st ( g is_sequence_on G & g is unfolded & g is s.c.c. & g is special & L~ f = L~ g & f /. 1 = g /. 1 & f /. (len f) = g /. (len g) & len f <= len g ) reconsider f9 = f as non constant circular special unfolded s.c.c. FinSequence of (TOP-REAL 2) by A2, A3, A4; reconsider f9 = f9 as non empty non constant circular special unfolded s.c.c. FinSequence of (TOP-REAL 2) ; set h1 = f9 | 2; set h2 = f9 /^ 1; A6: len f > 1 + 1 by A2, Th3; then A7: len (f9 | 2) = 1 + 1 by FINSEQ_1:59; then reconsider h1 = f9 | 2 as non trivial FinSequence of (TOP-REAL 2) by NAT_D:60; A8: h1 is s.n.c. by A6, Th20; len h1 in dom h1 by A7, FINSEQ_3:25; then A9: h1 /. (len h1) = f /. (1 + 1) by A7, FINSEQ_4:70; 1 <= len f by A2, Th3, XXREAL_0:2; then A10: len (f9 /^ 1) = (len f) - 1 by RFINSEQ:def_1; then A11: (len (f9 /^ 1)) + 1 = len f ; A12: dom h1 c= dom f by FINSEQ_5:18; A13: for n being Element of NAT st n in dom h1 holds ex i, j being Element of NAT st ( [i,j] in Indices G & h1 /. n = G * (i,j) ) proof let n be Element of NAT ; ::_thesis: ( n in dom h1 implies ex i, j being Element of NAT st ( [i,j] in Indices G & h1 /. n = G * (i,j) ) ) assume A14: n in dom h1 ; ::_thesis: ex i, j being Element of NAT st ( [i,j] in Indices G & h1 /. n = G * (i,j) ) then consider i, j being Nat such that A15: [i,j] in Indices G and A16: f /. n = G * (i,j) by A1, A12; 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 G & h1 /. n = G * (i,j) ) take j ; ::_thesis: ( [i,j] in Indices G & h1 /. n = G * (i,j) ) thus [i,j] in Indices G by A15; ::_thesis: h1 /. n = G * (i,j) thus h1 /. n = G * (i,j) by A14, A16, FINSEQ_4:70; ::_thesis: verum end; h1 is one-to-one by A5, Th3, Th22; then consider g1 being FinSequence of (TOP-REAL 2) such that A17: g1 is_sequence_on G and A18: ( g1 is one-to-one & g1 is unfolded & g1 is s.n.c. & g1 is special ) and A19: L~ h1 = L~ g1 and A20: h1 /. 1 = g1 /. 1 and A21: h1 /. (len h1) = g1 /. (len g1) and A22: len h1 <= len g1 by A13, A8, GOBOARD3:1; reconsider g1 = g1 as non trivial FinSequence of (TOP-REAL 2) by A7, A22, NAT_D:60; A23: 1 <= (len g1) -' 1 by A7, A22, NAT_D:55; ((len g1) -' 1) + 1 = len g1 by A7, A22, XREAL_1:235, XXREAL_0:2; then A24: g1 /. (len g1) in LSeg (g1,((len g1) -' 1)) by A23, TOPREAL1:21; A25: LSeg (g1,((len g1) -' 1)) c= L~ g1 by TOPREAL3:19; A26: len (f9 /^ 1) > (1 + 1) - 1 by A6, A10, XREAL_1:9; then A27: len (f9 /^ 1) >= 2 by NAT_1:13; then reconsider h2 = f9 /^ 1 as non trivial FinSequence of (TOP-REAL 2) by NAT_D:60; A28: h2 is s.n.c. by Th21; A29: len h2 in dom h2 by FINSEQ_5:6; A30: 1 in dom h1 by FINSEQ_5:6; then A31: h1 /. 1 = f /. 1 by FINSEQ_4:70; then A32: h1 /. 1 = f /. (len f) by FINSEQ_6:def_1 .= h2 /. (len h2) by A11, A29, FINSEQ_5:27 ; A33: for n being Element of NAT st n in dom h2 holds ex i, j being Element of NAT st ( [i,j] in Indices G & h2 /. n = G * (i,j) ) proof let n be Element of NAT ; ::_thesis: ( n in dom h2 implies ex i, j being Element of NAT st ( [i,j] in Indices G & h2 /. n = G * (i,j) ) ) assume A34: n in dom h2 ; ::_thesis: ex i, j being Element of NAT st ( [i,j] in Indices G & h2 /. n = G * (i,j) ) then consider i, j being Nat such that A35: [i,j] in Indices G and A36: f /. (n + 1) = G * (i,j) by A1, FINSEQ_5:26; 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 G & h2 /. n = G * (i,j) ) take j ; ::_thesis: ( [i,j] in Indices G & h2 /. n = G * (i,j) ) thus [i,j] in Indices G by A35; ::_thesis: h2 /. n = G * (i,j) thus h2 /. n = G * (i,j) by A34, A36, FINSEQ_5:27; ::_thesis: verum end; h2 is one-to-one by A5, Th24; then consider g2 being FinSequence of (TOP-REAL 2) such that A37: g2 is_sequence_on G and A38: ( g2 is one-to-one & g2 is unfolded & g2 is s.n.c. & g2 is special ) and A39: L~ h2 = L~ g2 and A40: h2 /. 1 = g2 /. 1 and A41: h2 /. (len h2) = g2 /. (len g2) and A42: len h2 <= len g2 by A33, A28, GOBOARD3:1; A43: len g2 >= 1 + 1 by A27, A42, XXREAL_0:2; then reconsider g2 = g2 as non trivial FinSequence of (TOP-REAL 2) by NAT_D:60; A44: ((len g2) -' 1) + 1 = len g2 by A43, XREAL_1:235, XXREAL_0:2; A45: LSeg (g2,1) c= L~ g2 by TOPREAL3:19; take g = g1 ^' g2; ::_thesis: ( g is_sequence_on G & g is unfolded & g is s.c.c. & g is special & L~ f = L~ g & f /. 1 = g /. 1 & f /. (len f) = g /. (len g) & len f <= len g ) 1 in dom h2 by A26, FINSEQ_3:25; then A46: h1 /. (len h1) = h2 /. 1 by A9, FINSEQ_5:27; hence g is_sequence_on G by A17, A21, A37, A40, Th12; ::_thesis: ( g is unfolded & g is s.c.c. & g is special & L~ f = L~ g & f /. 1 = g /. 1 & f /. (len f) = g /. (len g) & len f <= len g ) (LSeg (f,1)) /\ (L~ h2) = {(h1 /. 1),(h2 /. 1)} by A5, A9, A46, A31, Th27; then A47: (L~ g1) /\ (L~ g2) = {(g1 /. 1),(g2 /. 1)} by A19, A20, A39, A40, Th19; len h2 > (3 + 1) - 1 by A5, A10, XREAL_1:9; then 2 + 1 < len g2 by A42, XXREAL_0:2; then A48: 1 + 1 < (len g2) -' 1 by NAT_D:52; then 1 <= (len g2) -' 1 by NAT_1:13; then A49: g2 /. (len g2) in LSeg (g2,((len g2) -' 1)) by A44, TOPREAL1:21; LSeg (g2,1) misses LSeg (g2,((len g2) -' 1)) by A38, A48, TOPREAL1:def_7; then not g2 /. (len g2) in LSeg (g2,1) by A49, XBOOLE_0:3; then A50: not g2 /. (len g2) in (LSeg (g1,((len g1) -' 1))) /\ (LSeg (g2,1)) by XBOOLE_0:def_4; g2 /. 1 in LSeg (g2,1) by A43, TOPREAL1:21; then g2 /. 1 in (LSeg (g1,((len g1) -' 1))) /\ (LSeg (g2,1)) by A21, A40, A46, A24, XBOOLE_0:def_4; then (LSeg (g1,((len g1) -' 1))) /\ (LSeg (g2,1)) = {(g2 /. 1)} by A20, A41, A32, A47, A50, A25, A45, Th1, XBOOLE_1:27; hence g is unfolded by A18, A21, A38, A40, A46, Th34; ::_thesis: ( g is s.c.c. & g is special & L~ f = L~ g & f /. 1 = g /. 1 & f /. (len f) = g /. (len g) & len f <= len g ) thus g is s.c.c. by A18, A20, A21, A38, A40, A41, A46, A32, A47, Th33; ::_thesis: ( g is special & L~ f = L~ g & f /. 1 = g /. 1 & f /. (len f) = g /. (len g) & len f <= len g ) thus g is special by A18, A21, A38, A40, A46, Th26; ::_thesis: ( L~ f = L~ g & f /. 1 = g /. 1 & f /. (len f) = g /. (len g) & len f <= len g ) A51: ((1 + 1),(len h2)) -cut h2 = h2 /^ 1 by Th13; A52: f = h1 ^ (f /^ (1 + 1)) by RFINSEQ:8 .= h1 ^ ((2,(len h2)) -cut h2) by A51, FINSEQ_6:81 .= h1 ^' h2 by GRAPH_2:def_2 ; then A53: (len f) + 1 = (len h1) + (len h2) by GRAPH_2:13; thus L~ f = (L~ h1) \/ (L~ h2) by A52, A46, Th35 .= L~ g by A19, A21, A39, A40, A46, Th35 ; ::_thesis: ( f /. 1 = g /. 1 & f /. (len f) = g /. (len g) & len f <= len g ) thus f /. 1 = h1 /. 1 by A30, FINSEQ_4:70 .= g /. 1 by A20, GRAPH_2:53 ; ::_thesis: ( f /. (len f) = g /. (len g) & len f <= len g ) thus f /. (len f) = h2 /. (len h2) by A11, A29, FINSEQ_5:27 .= g /. (len g) by A41, GRAPH_2:54 ; ::_thesis: len f <= len g (len g) + 1 = (len g1) + (len g2) by GRAPH_2:13; then (len f) + 1 <= (len g) + 1 by A22, A42, A53, XREAL_1:7; hence len f <= len g by XREAL_1:6; ::_thesis: verum end;