:: TOPREAL8 semantic presentation

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

registration

cluster trivial set ;
existence

proof end;

end;

registration

cluster non constant set ;
existence

proof end;

end;

theorem Th2: :: TOPREAL8:2

for f being non trivial FinSequence holds 1 < len f

proof 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 end;

theorem Th4: :: TOPREAL8:4

for f being FinSequence
for x being set holds
( x in rng f or x .. f = 0 )

proof 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 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 end;

theorem Th7: :: TOPREAL8:7

for f, g being FinSequence holds len f <= len (f ^' g)

proof 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 end;

theorem :: TOPREAL8:9

for f being non empty FinSequence
for g being FinSequence holds len g <= len (f ^' g)

proof end;

theorem Th10: :: TOPREAL8:10

for f, g being FinSequence holds rng f c= rng (f ^' g)

proof 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 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 end;

theorem Th13: :: TOPREAL8:13

for k being Nat
for D being set
for f being FinSequence of D st 1 <= k holds
(k + 1),(len f) -cut f = f /^ k

proof end;

theorem Th14: :: TOPREAL8:14

for k being Nat
for D being set
for f being FinSequence of D st k <= len f holds
1,k -cut f = f | k

proof 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 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 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 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 Nat st 1 <= i & i < len f holds
f /. i <> g /. 1 ) holds
Rotate (f ^' g),(g /. 1) = g ^' f

proof end;

theorem Th19: :: TOPREAL8:19

for f being non trivial FinSequence of (TOP-REAL 2) holds LSeg f,1 = L~ (f | 2)

proof end;

theorem Th20: :: TOPREAL8:20

for f being s.c.c. FinSequence of (TOP-REAL 2)
for n being Nat st n < len f holds
f | n is s.n.c.

proof end;

theorem Th21: :: TOPREAL8:21

for f being s.c.c. FinSequence of (TOP-REAL 2)
for n being Nat st 1 <= n holds
f /^ n is s.n.c.

proof end;

theorem Th22: :: TOPREAL8:22

for f being circular s.c.c. FinSequence of (TOP-REAL 2)
for n being Nat st n < len f & len f > 4 holds
f | n is one-to-one

proof 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 Nat st 1 < i & i < j & j <= len f holds
f /. i <> f /. j

proof end;

theorem Th24: :: TOPREAL8:24

for f being circular s.c.c. FinSequence of (TOP-REAL 2)
for n being Nat st 1 <= n & len f > 4 holds
f /^ n is one-to-one

proof end;

theorem Th25: :: TOPREAL8:25

for m, n being Nat
for f being non empty special FinSequence of (TOP-REAL 2) holds m,n -cut f is special

proof 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 end;

theorem Th27: :: TOPREAL8:27

for f being unfolded circular s.c.c. FinSequence of (TOP-REAL 2) st len f > 4 holds
(LSeg f,1) /\ (L~ (f /^ 1)) = {(f /. 1),(f /. 2)}

proof end;

registration

cluster non empty one-to-one special unfolded s.n.c. FinSequence of the carrier of (TOP-REAL 2);
existence

proof end;

end;

theorem Th28: :: TOPREAL8:28

for j being Nat
for f, g being FinSequence of (TOP-REAL 2) st j < len f holds
LSeg (f ^' g),j = LSeg f,j

proof end;

theorem Th29: :: TOPREAL8:29

for j being 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 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 end;

theorem Th31: :: TOPREAL8:31

for j being 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 end;

theorem Th32: :: TOPREAL8:32

for f being non empty unfolded s.n.c. FinSequence of (TOP-REAL 2)
for i being Nat st 1 <= i & i < len f holds
(LSeg f,i) /\ (rng f) = {(f /. i),(f /. (i + 1))}

proof end;

Lm1: for f being non empty one-to-one unfolded s.n.c. FinSequence of (TOP-REAL 2)
for g being one-to-one non trivial unfolded s.n.c. FinSequence of (TOP-REAL 2)
for i, j being 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 end;

Lm2: for f being non empty one-to-one unfolded s.n.c. FinSequence of (TOP-REAL 2)
for g being one-to-one non trivial unfolded s.n.c. FinSequence of (TOP-REAL 2)
for i, j being 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 end;

theorem Th33: :: TOPREAL8:33

for f, g being one-to-one non trivial 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 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 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 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 end;