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