:: TOPREAL8 semantic presentation

theorem Th1: :: TOPREAL8:1
for b1, b2, b3 being set st b1 c= {b2,b3} & b2 in b1 & not b3 in b1 holds
b1 = {b2}
proof end;

registration
cluster trivial set ;
existence
ex b1 being Function st b1 is trivial
proof end;
end;

registration
cluster non constant set ;
existence
not for b1 being FinSequence holds b1 is constant
proof end;
end;

theorem Th2: :: TOPREAL8:2
for b1 being non trivial FinSequence holds 1 < len b1
proof end;

theorem Th3: :: TOPREAL8:3
for b1 being non trivial set
for b2 being non constant circular FinSequence of b1 holds len b2 > 2
proof end;

theorem Th4: :: TOPREAL8:4
for b1 being FinSequence
for b2 being set holds
( b2 in rng b1 or b2 .. b1 = 0 )
proof end;

theorem Th5: :: TOPREAL8:5
for b1 being set
for b2 being non empty set
for b3 being non empty FinSequence of b2
for b4 being FinSequence of b2 st b1 .. b3 = len b3 holds
(b3 ^ b4) |-- b1 = b4
proof end;

theorem Th6: :: TOPREAL8:6
for b1 being non empty set
for b2 being non empty one-to-one FinSequence of b1 holds (b2 /. (len b2)) .. b2 = len b2
proof end;

theorem Th7: :: TOPREAL8:7
for b1, b2 being FinSequence holds len b1 <= len (b1 ^' b2)
proof end;

theorem Th8: :: TOPREAL8:8
for b1, b2 being FinSequence
for b3 being set st b3 in rng b1 holds
b3 .. b1 = b3 .. (b1 ^' b2)
proof end;

theorem Th9: :: TOPREAL8:9
for b1 being non empty FinSequence
for b2 being FinSequence holds len b2 <= len (b1 ^' b2)
proof end;

theorem Th10: :: TOPREAL8:10
for b1, b2 being FinSequence holds rng b1 c= rng (b1 ^' b2)
proof end;

theorem Th11: :: TOPREAL8:11
for b1 being non empty set
for b2 being non empty FinSequence of b1
for b3 being non trivial FinSequence of b1 st b3 /. (len b3) = b2 /. 1 holds
b2 ^' b3 is circular
proof end;

theorem Th12: :: TOPREAL8:12
for b1 being non empty set
for b2 being Matrix of b1
for b3 being FinSequence of b1
for b4 being non empty FinSequence of b1 st b3 /. (len b3) = b4 /. 1 & b3 is_sequence_on b2 & b4 is_sequence_on b2 holds
b3 ^' b4 is_sequence_on b2
proof end;

theorem Th13: :: TOPREAL8:13
for b1 being Nat
for b2 being set
for b3 being FinSequence of b2 st 1 <= b1 holds
(b1 + 1),(len b3) -cut b3 = b3 /^ b1
proof end;

theorem Th14: :: TOPREAL8:14
for b1 being Nat
for b2 being set
for b3 being FinSequence of b2 st b1 <= len b3 holds
1,b1 -cut b3 = b3 | b1
proof end;

theorem Th15: :: TOPREAL8:15
for b1 being set
for b2 being non empty set
for b3 being non empty FinSequence of b2
for b4 being FinSequence of b2 st b1 .. b3 = len b3 holds
(b3 ^ b4) -| b1 = 1,((len b3) -' 1) -cut b3
proof end;

theorem Th16: :: TOPREAL8:16
for b1 being non empty set
for b2, b3 being non empty FinSequence of b1 st (b3 /. 1) .. b2 = len b2 holds
(b2 ^' b3) :- (b3 /. 1) = b3
proof end;

theorem Th17: :: TOPREAL8:17
for b1 being non empty set
for b2, b3 being non empty FinSequence of b1 st (b3 /. 1) .. b2 = len b2 holds
(b2 ^' b3) -: (b3 /. 1) = b2
proof end;

theorem Th18: :: TOPREAL8:18
for b1 being non trivial set
for b2 being non empty FinSequence of b1
for b3 being non trivial FinSequence of b1 st b3 /. 1 = b2 /. (len b2) & ( for b4 being Nat st 1 <= b4 & b4 < len b2 holds
b2 /. b4 <> b3 /. 1 ) holds
Rotate (b2 ^' b3),(b3 /. 1) = b3 ^' b2
proof end;

theorem Th19: :: TOPREAL8:19
for b1 being non trivial FinSequence of (TOP-REAL 2) holds LSeg b1,1 = L~ (b1 | 2)
proof end;

theorem Th20: :: TOPREAL8:20
for b1 being s.c.c. FinSequence of (TOP-REAL 2)
for b2 being Nat st b2 < len b1 holds
b1 | b2 is s.n.c.
proof end;

theorem Th21: :: TOPREAL8:21
for b1 being s.c.c. FinSequence of (TOP-REAL 2)
for b2 being Nat st 1 <= b2 holds
b1 /^ b2 is s.n.c.
proof end;

theorem Th22: :: TOPREAL8:22
for b1 being circular s.c.c. FinSequence of (TOP-REAL 2)
for b2 being Nat st b2 < len b1 & len b1 > 4 holds
b1 | b2 is one-to-one
proof end;

theorem Th23: :: TOPREAL8:23
for b1 being circular s.c.c. FinSequence of (TOP-REAL 2) st len b1 > 4 holds
for b2, b3 being Nat st 1 < b2 & b2 < b3 & b3 <= len b1 holds
b1 /. b2 <> b1 /. b3
proof end;

theorem Th24: :: TOPREAL8:24
for b1 being circular s.c.c. FinSequence of (TOP-REAL 2)
for b2 being Nat st 1 <= b2 & len b1 > 4 holds
b1 /^ b2 is one-to-one
proof end;

theorem Th25: :: TOPREAL8:25
for b1, b2 being Nat
for b3 being non empty special FinSequence of (TOP-REAL 2) holds b1,b2 -cut b3 is special
proof end;

theorem Th26: :: TOPREAL8:26
for b1 being non empty special FinSequence of (TOP-REAL 2)
for b2 being non trivial special FinSequence of (TOP-REAL 2) st b1 /. (len b1) = b2 /. 1 holds
b1 ^' b2 is special
proof end;

theorem Th27: :: TOPREAL8:27
for b1 being unfolded circular s.c.c. FinSequence of (TOP-REAL 2) st len b1 > 4 holds
(LSeg b1,1) /\ (L~ (b1 /^ 1)) = {(b1 /. 1),(b1 /. 2)}
proof end;

registration
cluster non empty one-to-one special unfolded s.n.c. FinSequence of the carrier of (TOP-REAL 2);
existence
ex b1 being FinSequence of (TOP-REAL 2) st
( b1 is one-to-one & b1 is special & b1 is unfolded & b1 is s.n.c. & not b1 is empty )
proof end;
end;

theorem Th28: :: TOPREAL8:28
for b1 being Nat
for b2, b3 being FinSequence of (TOP-REAL 2) st b1 < len b2 holds
LSeg (b2 ^' b3),b1 = LSeg b2,b1
proof end;

theorem Th29: :: TOPREAL8:29
for b1 being Nat
for b2, b3 being non empty FinSequence of (TOP-REAL 2) st 1 <= b1 & b1 + 1 < len b3 holds
LSeg (b2 ^' b3),((len b2) + b1) = LSeg b3,(b1 + 1)
proof end;

theorem Th30: :: TOPREAL8:30
for b1 being non empty FinSequence of (TOP-REAL 2)
for b2 being non trivial FinSequence of (TOP-REAL 2) st b1 /. (len b1) = b2 /. 1 holds
LSeg (b1 ^' b2),(len b1) = LSeg b2,1
proof end;

theorem Th31: :: TOPREAL8:31
for b1 being Nat
for b2 being non empty FinSequence of (TOP-REAL 2)
for b3 being non trivial FinSequence of (TOP-REAL 2) st b1 + 1 < len b3 & b2 /. (len b2) = b3 /. 1 holds
LSeg (b2 ^' b3),((len b2) + b1) = LSeg b3,(b1 + 1)
proof end;

theorem Th32: :: TOPREAL8:32
for b1 being non empty unfolded s.n.c. FinSequence of (TOP-REAL 2)
for b2 being Nat st 1 <= b2 & b2 < len b1 holds
(LSeg b1,b2) /\ (rng b1) = {(b1 /. b2),(b1 /. (b2 + 1))}
proof end;

Lemma32: for b1 being non empty one-to-one unfolded s.n.c. FinSequence of (TOP-REAL 2)
for b2 being one-to-one non trivial unfolded s.n.c. FinSequence of (TOP-REAL 2)
for b3, b4 being Nat st b3 < len b1 & 1 < b3 holds
for b5 being Point of (TOP-REAL 2) st b5 in (LSeg (b1 ^' b2),b3) /\ (LSeg (b1 ^' b2),b4) holds
b5 <> b1 /. 1
proof end;

Lemma33: for b1 being non empty one-to-one unfolded s.n.c. FinSequence of (TOP-REAL 2)
for b2 being one-to-one non trivial unfolded s.n.c. FinSequence of (TOP-REAL 2)
for b3, b4 being Nat st b4 > len b1 & b4 + 1 < len (b1 ^' b2) holds
for b5 being Point of (TOP-REAL 2) st b5 in (LSeg (b1 ^' b2),b3) /\ (LSeg (b1 ^' b2),b4) holds
b5 <> b2 /. (len b2)
proof end;

theorem Th33: :: TOPREAL8:33
for b1, b2 being one-to-one non trivial unfolded s.n.c. FinSequence of (TOP-REAL 2) st (L~ b1) /\ (L~ b2) = {(b1 /. 1),(b2 /. 1)} & b1 /. 1 = b2 /. (len b2) & b2 /. 1 = b1 /. (len b1) holds
b1 ^' b2 is s.c.c.
proof end;

theorem Th34: :: TOPREAL8:34
for b1, b2 being FinSequence of (TOP-REAL 2) st b1 is unfolded & b2 is unfolded & b1 /. (len b1) = b2 /. 1 & (LSeg b1,((len b1) -' 1)) /\ (LSeg b2,1) = {(b1 /. (len b1))} holds
b1 ^' b2 is unfolded
proof end;

theorem Th35: :: TOPREAL8:35
for b1, b2 being FinSequence of (TOP-REAL 2) st not b1 is empty & not b2 is trivial & b1 /. (len b1) = b2 /. 1 holds
L~ (b1 ^' b2) = (L~ b1) \/ (L~ b2)
proof end;

theorem Th36: :: TOPREAL8:36
for b1 being Go-board
for b2 being FinSequence of (TOP-REAL 2) st ( for b3 being Nat st b3 in dom b2 holds
ex b4, b5 being Nat st
( [b4,b5] in Indices b1 & b2 /. b3 = b1 * b4,b5 ) ) & not b2 is constant & b2 is circular & b2 is unfolded & b2 is s.c.c. & b2 is special & len b2 > 4 holds
ex b3 being FinSequence of (TOP-REAL 2) st
( b3 is_sequence_on b1 & b3 is unfolded & b3 is s.c.c. & b3 is special & L~ b2 = L~ b3 & b2 /. 1 = b3 /. 1 & b2 /. (len b2) = b3 /. (len b3) & len b2 <= len b3 )
proof end;