let f be V26() standard special_circular_sequence; for i1, i2 being Nat
for g1, g2 being FinSequence of (TOP-REAL 2) st 1 <= i1 & i1 < i2 & i2 < len f & g1 = mid (f,i1,i2) & g2 = (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) holds
( (L~ g1) /\ (L~ g2) = {(f . i1),(f . i2)} & (L~ g1) \/ (L~ g2) = L~ f )
let i1, i2 be Nat; for g1, g2 being FinSequence of (TOP-REAL 2) st 1 <= i1 & i1 < i2 & i2 < len f & g1 = mid (f,i1,i2) & g2 = (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) holds
( (L~ g1) /\ (L~ g2) = {(f . i1),(f . i2)} & (L~ g1) \/ (L~ g2) = L~ f )
let g1, g2 be FinSequence of (TOP-REAL 2); ( 1 <= i1 & i1 < i2 & i2 < len f & g1 = mid (f,i1,i2) & g2 = (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) implies ( (L~ g1) /\ (L~ g2) = {(f . i1),(f . i2)} & (L~ g1) \/ (L~ g2) = L~ f ) )
assume that
A1:
1 <= i1
and
A2:
i1 < i2
and
A3:
i2 < len f
and
A4:
g1 = mid (f,i1,i2)
and
A5:
g2 = (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))
; ( (L~ g1) /\ (L~ g2) = {(f . i1),(f . i2)} & (L~ g1) \/ (L~ g2) = L~ f )
A6:
i1 < len f
by A2, A3, XXREAL_0:2;
then A7:
1 < len f
by A1, XXREAL_0:2;
then A8:
L~ (mid (f,i1,1)) c= L~ f
by A1, A6, Th35;
A9:
1 < i2
by A1, A2, XXREAL_0:2;
then A10:
len (mid (f,i1,i2)) = (i2 -' i1) + 1
by A1, A2, A3, A6, FINSEQ_6:118;
A11:
i2 + 1 <= len f
by A3, NAT_1:13;
then A12:
(i2 + 1) - 1 <= (len f) - 1
by XREAL_1:9;
then A13:
i2 <= (len f) -' 1
by A1, A6, XREAL_1:233, XXREAL_0:2;
then A14: (((len f) -' 1) -' i2) + 1 =
(((len f) -' 1) - i2) + 1
by XREAL_1:233
.=
(((len f) - 1) - i2) + 1
by A1, A6, XREAL_1:233, XXREAL_0:2
.=
(len f) - i2
;
A15:
0 < i2 - i1
by A2, XREAL_1:50;
then
0 < i2 -' i1
by A2, XREAL_1:233;
then
0 + 1 <= i2 -' i1
by NAT_1:13;
then
1 < len g1
by A4, A10, NAT_1:13;
then A16:
1 + 1 <= len g1
by NAT_1:13;
A17:
{(f . i1)} c= L~ g1
A19:
0 + 1 <= (((len f) -' 1) -' i2) + 1
by NAT_1:13;
A20:
len (mid (f,i1,1)) = (i1 -' 1) + 1
by A1, A6, Th9;
then A21:
0 + 1 <= len (mid (f,i1,1))
by NAT_1:13;
A22:
(len f) -' 1 < ((len f) -' 1) + 1
by NAT_1:13;
then A23:
(len f) -' 1 < len f
by A1, A6, XREAL_1:235, XXREAL_0:2;
then A24:
len (mid (f,((len f) -' 1),i2)) = (((len f) -' 1) -' i2) + 1
by A9, A13, Th9;
then A25:
1 <= len (mid (f,((len f) -' 1),i2))
by NAT_1:11;
A26:
1 < (len f) -' 1
by A9, A13, XXREAL_0:2;
then A27: f /. ((len f) -' 1) =
f . ((len f) -' 1)
by A23, FINSEQ_4:15
.=
(mid (f,((len f) -' 1),i2)) . 1
by A3, A9, A26, A23, FINSEQ_6:118
.=
(mid (f,((len f) -' 1),i2)) /. 1
by A25, FINSEQ_4:15
;
((len f) -' 1) + 1 = len f
by A1, A6, XREAL_1:235, XXREAL_0:2;
then A28:
LSeg (f,((len f) -' 1)) = LSeg ((f /. (((len f) -' 1) + 1)),(f /. ((len f) -' 1)))
by A26, TOPREAL1:def 3;
A29: f /. (((len f) -' 1) + 1) =
f /. (len f)
by A1, A6, XREAL_1:235, XXREAL_0:2
.=
f /. 1
by FINSEQ_6:def 1
.=
f . 1
by A7, FINSEQ_4:15
.=
(mid (f,i1,1)) . (len (mid (f,i1,1)))
by A1, A6, A7, Th11
.=
(mid (f,i1,1)) /. (len (mid (f,i1,1)))
by A21, FINSEQ_4:15
;
then
LSeg (((mid (f,i1,1)) /. (len (mid (f,i1,1)))),((mid (f,((len f) -' 1),i2)) /. 1)) c= L~ f
by A28, A27, TOPREAL3:19;
then A30:
(L~ (mid (f,i1,1))) \/ (LSeg (((mid (f,i1,1)) /. (len (mid (f,i1,1)))),((mid (f,((len f) -' 1),i2)) /. 1))) c= L~ f
by A8, XBOOLE_1:8;
A31:
mid (f,i1,1) <> <*> (TOP-REAL 2)
by A20;
mid (f,((len f) -' 1),i2) <> <*> (TOP-REAL 2)
by A24;
then A32:
L~ ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) = ((L~ (mid (f,i1,1))) \/ (LSeg (((mid (f,i1,1)) /. (len (mid (f,i1,1)))),((mid (f,((len f) -' 1),i2)) /. 1)))) \/ (L~ (mid (f,((len f) -' 1),i2)))
by A31, SPPOL_2:23;
A33:
L~ f c= (L~ g1) \/ (L~ g2)
proof
let x be
object ;
TARSKI:def 3 ( not x in L~ f or x in (L~ g1) \/ (L~ g2) )
assume A34:
x in L~ f
;
x in (L~ g1) \/ (L~ g2)
then reconsider p =
x as
Point of
(TOP-REAL 2) ;
consider i being
Nat such that A35:
1
<= i
and A36:
i + 1
<= len f
and A37:
p in LSeg (
f,
i)
by A34, SPPOL_2:13;
now ( ( i1 <= i & i < i2 & x in (L~ g1) \/ (L~ g2) ) or ( i < i1 & x in (L~ g1) \/ (L~ g2) ) or ( i2 <= i & x in (L~ g1) \/ (L~ g2) ) )per cases
( ( i1 <= i & i < i2 ) or i < i1 or i2 <= i )
;
case A38:
(
i1 <= i &
i < i2 )
;
x in (L~ g1) \/ (L~ g2)then
i - i1 < i2 - i1
by XREAL_1:9;
then
(i - i1) + 1
< (i2 - i1) + 1
by XREAL_1:6;
then
(i -' i1) + 1
< (i2 - i1) + 1
by A38, XREAL_1:233;
then A39:
(i -' i1) + 1
< (i2 -' i1) + 1
by A2, XREAL_1:233;
0 <= i - i1
by A38, XREAL_1:48;
then
0 + 1
<= (i - i1) + 1
by XREAL_1:6;
then A40:
1
<= (i -' i1) + 1
by A38, XREAL_1:233;
(((i -' i1) + 1) + i1) -' 1 =
(((i -' i1) + 1) + i1) - 1
by A1, NAT_D:37
.=
(i -' i1) + i1
.=
i
by A38, XREAL_1:235
;
then
x in LSeg (
(mid (f,i1,i2)),
((i -' i1) + 1))
by A1, A2, A3, A37, A40, A39, Th19;
then
x in L~ (mid (f,i1,i2))
by SPPOL_2:17;
hence
x in (L~ g1) \/ (L~ g2)
by A4, XBOOLE_0:def 3;
verum end; case A41:
i < i1
;
x in (L~ g1) \/ (L~ g2)
i1 + 1
<= i1 + i
by A35, XREAL_1:6;
then
i1 < i1 + i
by NAT_1:13;
then
i1 - i < (i1 + i) - i
by XREAL_1:9;
then
i1 -' i < (i1 - 1) + 1
by A41, XREAL_1:233;
then A42:
i1 -' i < (i1 -' 1) + 1
by A1, XREAL_1:233;
i1 <= i1 + i
by NAT_1:11;
then
i1 - i <= (i1 + i) - i
by XREAL_1:9;
then
i1 -' i <= i1
by A41, XREAL_1:233;
then A43:
i1 -' (i1 -' i) =
i1 - (i1 -' i)
by XREAL_1:233
.=
i1 - (i1 - i)
by A41, XREAL_1:233
.=
i
;
i + 1
<= i1
by A41, NAT_1:13;
then
(i + 1) - i <= i1 - i
by XREAL_1:9;
then A44:
1
<= i1 -' i
by NAT_D:39;
1
< i1
by A35, A41, XXREAL_0:2;
then
x in LSeg (
(mid (f,i1,1)),
(i1 -' i))
by A6, A37, A42, A44, A43, Th20;
then
x in L~ (mid (f,i1,1))
by SPPOL_2:17;
then
x in (L~ (mid (f,i1,1))) \/ (LSeg (((mid (f,i1,1)) /. (len (mid (f,i1,1)))),((mid (f,((len f) -' 1),i2)) /. 1)))
by XBOOLE_0:def 3;
then
x in L~ ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)))
by A32, XBOOLE_0:def 3;
hence
x in (L~ g1) \/ (L~ g2)
by A5, XBOOLE_0:def 3;
verum end; case A45:
i2 <= i
;
x in (L~ g1) \/ (L~ g2)now ( ( i + 1 = len f & x in (LSeg (((mid (f,i1,1)) /. (len (mid (f,i1,1)))),((mid (f,((len f) -' 1),i2)) /. 1))) \/ (L~ (mid (f,((len f) -' 1),i2))) ) or ( i + 1 < len f & x in (LSeg (((mid (f,i1,1)) /. (len (mid (f,i1,1)))),((mid (f,((len f) -' 1),i2)) /. 1))) \/ (L~ (mid (f,((len f) -' 1),i2))) ) )per cases
( i + 1 = len f or i + 1 < len f )
by A36, XXREAL_0:1;
case
i + 1
= len f
;
x in (LSeg (((mid (f,i1,1)) /. (len (mid (f,i1,1)))),((mid (f,((len f) -' 1),i2)) /. 1))) \/ (L~ (mid (f,((len f) -' 1),i2)))then
i = (len f) - 1
;
then
i = (len f) -' 1
by A1, A6, XREAL_1:233, XXREAL_0:2;
hence
x in (LSeg (((mid (f,i1,1)) /. (len (mid (f,i1,1)))),((mid (f,((len f) -' 1),i2)) /. 1))) \/ (L~ (mid (f,((len f) -' 1),i2)))
by A28, A29, A27, A37, XBOOLE_0:def 3;
verum end; case
i + 1
< len f
;
x in (LSeg (((mid (f,i1,1)) /. (len (mid (f,i1,1)))),((mid (f,((len f) -' 1),i2)) /. 1))) \/ (L~ (mid (f,((len f) -' 1),i2)))then
(i + 1) + 1
<= len f
by NAT_1:13;
then
((i + 1) + 1) - 1
<= (len f) - 1
by XREAL_1:9;
then A46:
i + 1
<= (len f) -' 1
by A1, A6, XREAL_1:233, XXREAL_0:2;
then A47:
i < (len f) -' 1
by NAT_1:13;
then ((len f) -' 1) - (((len f) -' 1) -' i) =
((len f) -' 1) - (((len f) -' 1) - i)
by XREAL_1:233
.=
i
;
then A48:
((len f) -' 1) -' (((len f) -' 1) -' i) = i
by XREAL_0:def 2;
i2 < i + 1
by A45, NAT_1:13;
then
((len f) -' 1) + i2 < ((len f) -' 1) + (i + 1)
by XREAL_1:6;
then
(((len f) -' 1) + i2) - i2 < (((len f) -' 1) + (i + 1)) - i2
by XREAL_1:9;
then
((len f) -' 1) - i < (((((len f) -' 1) + 1) + i) - i2) - i
by XREAL_1:9;
then
((len f) -' 1) - i < (((len f) -' 1) - i2) + 1
;
then
((len f) -' 1) - i < (((len f) -' 1) -' i2) + 1
by A45, A47, XREAL_1:233, XXREAL_0:2;
then A49:
((len f) -' 1) -' i < (((len f) -' 1) -' i2) + 1
by A47, XREAL_1:233;
(i + 1) - i <= ((len f) -' 1) - i
by A46, XREAL_1:9;
then A50:
1
<= ((len f) -' 1) -' i
by NAT_D:39;
i2 < (len f) -' 1
by A45, A47, XXREAL_0:2;
then
x in LSeg (
(mid (f,((len f) -' 1),i2)),
(((len f) -' 1) -' i))
by A9, A23, A37, A50, A49, A48, Th20;
then
x in L~ (mid (f,((len f) -' 1),i2))
by SPPOL_2:17;
hence
x in (LSeg (((mid (f,i1,1)) /. (len (mid (f,i1,1)))),((mid (f,((len f) -' 1),i2)) /. 1))) \/ (L~ (mid (f,((len f) -' 1),i2)))
by XBOOLE_0:def 3;
verum end; end; end; then
x in (L~ (mid (f,i1,1))) \/ ((LSeg (((mid (f,i1,1)) /. (len (mid (f,i1,1)))),((mid (f,((len f) -' 1),i2)) /. 1))) \/ (L~ (mid (f,((len f) -' 1),i2))))
by XBOOLE_0:def 3;
then
x in L~ ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)))
by A32, XBOOLE_1:4;
hence
x in (L~ g1) \/ (L~ g2)
by A5, XBOOLE_0:def 3;
verum end; end; end;
hence
x in (L~ g1) \/ (L~ g2)
;
verum
end;
A51:
i1 + 1 <= len f
by A6, NAT_1:13;
(i2 + 1) - i2 <= (len f) - i2
by A11, XREAL_1:9;
then A52:
1 <= (len f) -' i2
by NAT_D:39;
A53: len g2 =
(len (mid (f,i1,1))) + (len (mid (f,((len f) -' 1),i2)))
by A5, FINSEQ_1:22
.=
((i1 -' 1) + 1) + ((((len f) -' 1) -' i2) + 1)
by A1, A6, A24, Th9
.=
i1 + ((((len f) -' 1) -' i2) + 1)
by A1, XREAL_1:235
;
then A54:
1 + 1 <= len g2
by A1, A19, XREAL_1:7;
A55:
{(f . i1)} c= L~ g2
A57:
((len f) -' 1) + 1 = len f
by A1, A6, XREAL_1:235, XXREAL_0:2;
A58:
(L~ g1) /\ (L~ g2) c= {(f . i1),(f . i2)}
proof
let x be
object ;
TARSKI:def 3 ( not x in (L~ g1) /\ (L~ g2) or x in {(f . i1),(f . i2)} )
assume A59:
x in (L~ g1) /\ (L~ g2)
;
x in {(f . i1),(f . i2)}
then reconsider p =
x as
Point of
(TOP-REAL 2) ;
x in L~ g1
by A59, XBOOLE_0:def 4;
then consider i being
Nat such that A60:
1
<= i
and A61:
i + 1
<= len (mid (f,i1,i2))
and A62:
p in LSeg (
(mid (f,i1,i2)),
i)
by A4, SPPOL_2:13;
A63:
i < (i2 -' i1) + 1
by A10, A61, NAT_1:13;
then A64:
LSeg (
(mid (f,i1,i2)),
i)
= LSeg (
f,
((i + i1) -' 1))
by A1, A2, A3, A60, Th19;
i + 1
<= (i2 -' i1) + 1
by A1, A2, A3, A9, A6, A61, FINSEQ_6:118;
then A65:
(i + 1) - 1
<= ((i2 -' i1) + 1) - 1
by XREAL_1:9;
x in L~ ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)))
by A5, A59, XBOOLE_0:def 4;
then A66:
(
x in (L~ (mid (f,i1,1))) \/ (LSeg (((mid (f,i1,1)) /. (len (mid (f,i1,1)))),((mid (f,((len f) -' 1),i2)) /. 1))) or
x in L~ (mid (f,((len f) -' 1),i2)) )
by A32, XBOOLE_0:def 3;
now ( ( x in L~ (mid (f,i1,1)) & x in {(f . i1),(f . i2)} ) or ( x in LSeg (((mid (f,i1,1)) /. (len (mid (f,i1,1)))),((mid (f,((len f) -' 1),i2)) /. 1)) & x in {(f . i1),(f . i2)} ) or ( x in L~ (mid (f,((len f) -' 1),i2)) & x in {(f . i1),(f . i2)} ) )per cases
( x in L~ (mid (f,i1,1)) or x in LSeg (((mid (f,i1,1)) /. (len (mid (f,i1,1)))),((mid (f,((len f) -' 1),i2)) /. 1)) or x in L~ (mid (f,((len f) -' 1),i2)) )
by A66, XBOOLE_0:def 3;
case
x in L~ (mid (f,i1,1))
;
x in {(f . i1),(f . i2)}then consider k being
Nat such that A67:
1
<= k
and A68:
k + 1
<= len (mid (f,i1,1))
and A69:
p in LSeg (
(mid (f,i1,1)),
k)
by SPPOL_2:13;
now ( ( i1 <> 1 & x in {(f . i1),(f . i2)} ) or ( i1 = 1 & contradiction ) )per cases
( i1 <> 1 or i1 = 1 )
;
case
i1 <> 1
;
x in {(f . i1),(f . i2)}then A70:
1
< i1
by A1, XXREAL_0:1;
then
1
+ 1
<= i1
by NAT_1:13;
then A71:
(1 + 1) - 1
<= i1 - 1
by XREAL_1:9;
set k3 =
i1 -' k;
set i3 =
(i + i1) -' 1;
A72:
(i + i1) -' 1
= (i + i1) - 1
by A1, NAT_D:37;
A73:
k < (i1 -' 1) + 1
by A20, A68, NAT_1:13;
(i1 -' 1) + 1
= i1
by A1, XREAL_1:235;
then A74:
i1 -' k = i1 - k
by A73, XREAL_1:233;
i1 <= len f
by A2, A3, XXREAL_0:2;
then A75:
LSeg (
(mid (f,i1,1)),
k)
= LSeg (
f,
(i1 -' k))
by A67, A70, A73, Th20;
then A76:
x in (LSeg (f,(i1 -' k))) /\ (LSeg (f,((i + i1) -' 1)))
by A62, A64, A69, XBOOLE_0:def 4;
A77:
LSeg (
f,
(i1 -' k))
meets LSeg (
f,
((i + i1) -' 1))
by A62, A64, A69, A75, XBOOLE_0:3;
1
+ 1
<= i + k
by A60, A67, XREAL_1:7;
then
1
< i + k
by XXREAL_0:2;
then
1
- k < (i + k) - k
by XREAL_1:9;
then
(1 - k) - 1
< i - 1
by XREAL_1:9;
then
i1 + ((1 - k) - 1) < i1 + (i - 1)
by XREAL_1:6;
then A78:
(i1 -' k) + 1
<= (i + i1) -' 1
by A74, A72, NAT_1:13;
then A82:
1
+ 1
= ((i + k) - 1) + 1
by A74, A72;
A83:
now ( i = 1 & k = 1 )assume A84:
( not
i = 1 or not
k = 1 )
;
contradictionnow ( ( i <> 1 & contradiction ) or ( k <> 1 & contradiction ) )end; hence
contradiction
;
verum end; then A85:
(i + i1) -' 1
= i1
by NAT_D:34;
(i1 -' k) + 2 =
((i1 -' 1) + 1) + 1
by A83
.=
i1 + 1
by A1, XREAL_1:235
;
then
x in {(f /. ((i1 -' k) + 1))}
by A51, A76, A79, A71, TOPREAL1:def 6;
then A86:
x = f /. i1
by A79, A85, TARSKI:def 1;
f /. i1 = f . i1
by A1, A6, FINSEQ_4:15;
hence
x in {(f . i1),(f . i2)}
by A86, TARSKI:def 2;
verum end; case A87:
i1 = 1
;
contradictionend; end; end; hence
x in {(f . i1),(f . i2)}
;
verum end; case A89:
x in LSeg (
((mid (f,i1,1)) /. (len (mid (f,i1,1)))),
((mid (f,((len f) -' 1),i2)) /. 1))
;
x in {(f . i1),(f . i2)}
(i2 + 1) - i2 <= (len f) - i2
by A11, XREAL_1:9;
then A90:
(mid (f,((len f) -' 1),i2)) /. 1 =
(mid (f,((len f) -' 1),i2)) . 1
by A24, A14, FINSEQ_4:15
.=
f . ((len f) -' 1)
by A3, A9, A26, A23, FINSEQ_6:118
.=
f /. ((len f) -' 1)
by A26, A23, FINSEQ_4:15
;
(mid (f,i1,1)) /. (len (mid (f,i1,1))) =
(mid (f,i1,1)) . (len (mid (f,i1,1)))
by A21, FINSEQ_4:15
.=
f . 1
by A1, A6, A7, Th11
.=
f /. 1
by A7, FINSEQ_4:15
.=
f /. (len f)
by FINSEQ_6:def 1
;
then
x in LSeg (
f,
((len f) -' 1))
by A26, A57, A89, A90, TOPREAL1:def 3;
then A91:
x in (LSeg (f,((i + i1) -' 1))) /\ (LSeg (f,((len f) -' 1)))
by A62, A64, XBOOLE_0:def 4;
then A92:
LSeg (
f,
((i + i1) -' 1))
meets LSeg (
f,
((len f) -' 1))
by XBOOLE_0:4;
now ( ( ( 1 < i1 or 1 < i ) & x in {(f . i1),(f . i2)} ) or ( not 1 < i1 & not 1 < i & x in {(f . i1),(f . i2)} ) )per cases
( 1 < i1 or 1 < i or ( not 1 < i1 & not 1 < i ) )
;
case A93:
( 1
< i1 or 1
< i )
;
x in {(f . i1),(f . i2)}A94:
now not ((i + i1) -' 1) + 1 < (len f) -' 1
1
+ 1
< i + i1
by A1, A60, A93, XREAL_1:8;
then
1
+ 1
< ((i + i1) -' 1) + 1
by XREAL_1:235, XXREAL_0:2;
then A95:
(1 + 1) - 1
< (((i + i1) -' 1) + 1) - 1
by XREAL_1:9;
assume A96:
((i + i1) -' 1) + 1
< (len f) -' 1
;
contradiction
(len f) -' 1
< len f
by A1, A6, A22, XREAL_1:235, XXREAL_0:2;
hence
contradiction
by A92, A96, A95, GOBOARD5:def 4;
verum end; set i3 =
(i + i1) -' 1;
((len f) - 1) + 1
<= len f
;
then A97:
((len f) -' 1) + 1
<= len f
by A1, A6, XREAL_1:233, XXREAL_0:2;
1
+ 1
<= i + i1
by A1, A60, XREAL_1:7;
then
(1 + 1) - 1
<= (i + i1) - 1
by XREAL_1:9;
then A98:
1
<= (i + i1) -' 1
by A1, NAT_D:37;
i <= i2 - i1
by A2, A65, XREAL_1:233;
then
i + i1 <= (i2 - i1) + i1
by XREAL_1:6;
then
i + i1 < len f
by A3, XXREAL_0:2;
then
(i + i1) - 1
< (len f) - 1
by XREAL_1:9;
then
(i + i1) -' 1
< (len f) - 1
by A1, NAT_D:37;
then
(i + i1) -' 1
< (len f) -' 1
by A1, A6, XREAL_1:233, XXREAL_0:2;
then A99:
((i + i1) -' 1) + 1
<= (len f) -' 1
by NAT_1:13;
then A100:
((i + i1) -' 1) + 1
= (len f) -' 1
by A94, XXREAL_0:1;
A101:
(i + i1) -' 1
= (i + i1) - 1
by A1, NAT_D:37;
then A103:
((i + i1) -' 1) + 1
= i2
by A13, A100, XXREAL_0:1;
((i + i1) -' 1) + 1
= (len f) -' 1
by A99, A94, XXREAL_0:1;
then
((i + i1) -' 1) + 2
<= len f
by A97;
then
x in {(f /. (((i + i1) -' 1) + 1))}
by A91, A98, A100, TOPREAL1:def 6;
then A104:
x = f /. i2
by A103, TARSKI:def 1;
f /. i2 = f . i2
by A3, A9, FINSEQ_4:15;
hence
x in {(f . i1),(f . i2)}
by A104, TARSKI:def 2;
verum end; case A105:
( not 1
< i1 & not 1
< i )
;
x in {(f . i1),(f . i2)}then
i = 1
by A60, XXREAL_0:1;
then A106:
(i + i1) -' 1 =
(1 + 1) -' 1
by A1, A105, XXREAL_0:1
.=
1
by NAT_D:34
;
A107:
i1 = 1
by A1, A105, XXREAL_0:1;
(LSeg (f,1)) /\ (LSeg (f,((len f) -' 1))) = {(f . 1)}
by Th42;
then
x = f . 1
by A91, A106, TARSKI:def 1;
hence
x in {(f . i1),(f . i2)}
by A107, TARSKI:def 2;
verum end; end; end; hence
x in {(f . i1),(f . i2)}
;
verum end; case
x in L~ (mid (f,((len f) -' 1),i2))
;
x in {(f . i1),(f . i2)}then consider k being
Nat such that A108:
1
<= k
and A109:
k + 1
<= len (mid (f,((len f) -' 1),i2))
and A110:
p in LSeg (
(mid (f,((len f) -' 1),i2)),
k)
by SPPOL_2:13;
A111:
k < (((len f) -' 1) -' i2) + 1
by A24, A109, NAT_1:13;
then A112:
k <= ((len f) -' 1) -' i2
by NAT_1:13;
k < (len f) -' i2
by A3, A14, A111, XREAL_1:233;
then
k + 1
<= (len f) -' i2
by NAT_1:13;
then
(k + 1) - 1
<= ((len f) -' i2) - 1
by XREAL_1:9;
then A113:
k <= ((len f) -' i2) -' 1
by A52, XREAL_1:233;
A114:
((len f) -' i2) -' 1 =
((len f) -' i2) - 1
by A52, XREAL_1:233
.=
((len f) - i2) - 1
by A3, XREAL_1:233
.=
((len f) - 1) - i2
.=
((len f) -' 1) - i2
by A1, A6, XREAL_1:233, XXREAL_0:2
.=
((len f) -' 1) -' i2
by A13, XREAL_1:233
;
A115:
k < (len f) - i2
by A24, A14, A109, NAT_1:13;
then
k + i2 < ((len f) - i2) + i2
by XREAL_1:6;
then A116:
(k + i2) - k < (len f) - k
by XREAL_1:9;
then A117:
1
< (len f) - k
by A9, XXREAL_0:2;
then
1
+ k < ((len f) - k) + k
by XREAL_1:6;
then
(1 + k) - 1
< (len f) - 1
by XREAL_1:9;
then A118:
k < (len f) -' 1
by A1, A6, XREAL_1:233, XXREAL_0:2;
1
< (len f) -' k
by A117, XREAL_0:def 2;
then A119:
((len f) -' k) -' 1 =
((len f) -' k) - 1
by XREAL_1:233
.=
((len f) - k) - 1
by A116, XREAL_0:def 2
.=
((len f) - 1) - k
.=
((len f) -' 1) - k
by A1, A6, XREAL_1:233, XXREAL_0:2
.=
((len f) -' 1) -' k
by A118, XREAL_1:233
;
now ( ( i2 <> (len f) -' 1 & x in {(f . i1),(f . i2)} ) or ( i2 = (len f) -' 1 & contradiction ) )per cases
( i2 <> (len f) -' 1 or i2 = (len f) -' 1 )
;
case
i2 <> (len f) -' 1
;
x in {(f . i1),(f . i2)}then A120:
i2 < (len f) -' 1
by A13, XXREAL_0:1;
A121:
k < (((len f) -' 1) -' i2) + 1
by A24, A109, NAT_1:13;
k + (i2 - 1) < ((len f) - i2) + (i2 - 1)
by A115, XREAL_1:6;
then A122:
k + (i2 -' 1) < (len f) - 1
by A1, A2, XREAL_1:233, XXREAL_0:2;
k <= k + (i2 -' 1)
by NAT_1:11;
then A123:
k < (len f) - 1
by A122, XXREAL_0:2;
then
k + 1
< ((len f) - 1) + 1
by XREAL_1:6;
then
(k + 1) - k < (len f) - k
by XREAL_1:9;
then A124:
1
< (len f) -' k
by NAT_D:39;
i2 + (((len f) -' 1) - i2) < len f
by A1, A6, A22, XREAL_1:235, XXREAL_0:2;
then
((i2 - i1) + i1) + (((len f) -' 1) -' i2) < len f
by A13, XREAL_1:233;
then A125:
((i2 -' i1) + i1) + (((len f) -' 1) -' i2) < len f
by A2, XREAL_1:233;
set k3 =
((len f) -' 1) -' k;
set i3 =
(i + i1) -' 1;
A126:
1
<= i2
by A1, A2, XXREAL_0:2;
i + i1 <= (i2 -' i1) + i1
by A65, XREAL_1:6;
then A127:
(i + i1) + k <= ((i2 -' i1) + i1) + k
by XREAL_1:6;
((i2 -' i1) + i1) + k <= ((i2 -' i1) + i1) + (((len f) -' 1) -' i2)
by A112, XREAL_1:6;
then
(i + i1) + k <= ((i2 -' i1) + i1) + (((len f) -' 1) -' i2)
by A127, XXREAL_0:2;
then
(i + i1) + k < len f
by A125, XXREAL_0:2;
then A128:
((i + i1) + k) - k < (len f) - k
by XREAL_1:9;
k < (len f) -' 1
by A1, A6, A123, XREAL_1:233, XXREAL_0:2;
then A129:
((len f) -' 1) -' k = ((len f) -' 1) - k
by XREAL_1:233;
len f < (len f) + 1
by NAT_1:13;
then
(len f) - 1
< ((len f) + 1) - 1
by XREAL_1:9;
then
(len f) -' k = (len f) - k
by A123, XREAL_1:233, XXREAL_0:2;
then
(i + i1) - 1
< ((len f) -' k) - 1
by A128, XREAL_1:9;
then
(i + i1) - 1
< ((len f) -' k) -' 1
by A124, XREAL_1:233;
then
(i + i1) -' 1
< ((len f) -' 1) -' k
by A60, A119, NAT_D:37;
then A130:
((i + i1) -' 1) + 1
<= ((len f) -' 1) -' k
by NAT_1:13;
(len f) -' 1
<= len f
by A1, A6, A22, XREAL_1:235, XXREAL_0:2;
then A131:
LSeg (
(mid (f,((len f) -' 1),i2)),
k)
= LSeg (
f,
(((len f) -' 1) -' k))
by A108, A126, A120, A121, Th20;
then A132:
LSeg (
f,
((i + i1) -' 1))
meets LSeg (
f,
(((len f) -' 1) -' k))
by A62, A64, A110, XBOOLE_0:3;
(i + i1) -' 1
= (i + i1) - 1
by A1, NAT_D:37;
then A135:
((len f) - 1) - k = ((i1 + i) - 1) + 1
by A1, A6, A129, A133, XREAL_1:233, XXREAL_0:2;
A136:
now ( i = i2 -' i1 & k = ((len f) -' 1) -' i2 )assume A137:
( not
i = i2 -' i1 or not
k = ((len f) -' 1) -' i2 )
;
contradictionnow ( ( i <> i2 -' i1 & contradiction ) or ( k <> ((len f) -' 1) -' i2 & contradiction ) )end; hence
contradiction
;
verum end; then (i + i1) -' 1 =
((i2 -' i1) + i1) - 1
by A1, NAT_D:37
.=
((i2 - i1) + i1) - 1
by A2, XREAL_1:233
.=
i2 - 1
;
then A138:
((i + i1) -' 1) + 2
= i2 + 1
;
1
+ 1
<= i2
by A9, NAT_1:13;
then A139:
(1 + 1) - 1
<= i2 - 1
by XREAL_1:9;
A140:
(len f) -' 1
= (len f) - 1
by A1, A6, XREAL_1:233, XXREAL_0:2;
len f <= (len f) + i2
by NAT_1:11;
then
((len f) -' 1) + 1
<= (len f) + i2
by A1, A6, XREAL_1:235, XXREAL_0:2;
then
(((len f) -' 1) + 1) - i2 <= ((len f) + i2) - i2
by XREAL_1:9;
then
((((len f) -' 1) + 1) - i2) - 1
<= (len f) - 1
by XREAL_1:9;
then
((len f) -' 1) - i2 <= (len f) - 1
;
then
((len f) -' 1) -' i2 <= (len f) -' 1
by A12, A140, XREAL_1:233;
then A141:
((len f) -' 1) -' k =
((len f) -' 1) - (((len f) -' 1) -' i2)
by A136, XREAL_1:233
.=
((len f) - 1) - (((len f) - 1) - i2)
by A12, A140, XREAL_1:233
.=
i2
;
x in (LSeg (f,((i + i1) -' 1))) /\ (LSeg (f,(((len f) -' 1) -' k)))
by A62, A64, A110, A131, XBOOLE_0:def 4;
then
x in {(f /. (((i + i1) -' 1) + 1))}
by A11, A133, A138, A139, TOPREAL1:def 6;
then
x = f /. i2
by A133, A141, TARSKI:def 1;
then
x = f . i2
by A3, A9, FINSEQ_4:15;
hence
x in {(f . i1),(f . i2)}
by TARSKI:def 2;
verum end; end; end; hence
x in {(f . i1),(f . i2)}
;
verum end; end; end;
hence
x in {(f . i1),(f . i2)}
;
verum
end;
A144:
len (mid (f,i1,1)) = i1
by A1, A20, XREAL_1:235;
{(f . i2)} c= L~ g2
proof
let x be
object ;
TARSKI:def 3 ( not x in {(f . i2)} or x in L~ g2 )
assume
x in {(f . i2)}
;
x in L~ g2
then A145:
x = f . i2
by TARSKI:def 1;
g2 . (len g2) =
(mid (f,((len f) -' 1),i2)) . ((((len f) -' 1) -' i2) + 1)
by A5, A144, A24, A19, A53, FINSEQ_1:65
.=
f . i2
by A3, A9, A26, A23, A24, Th11
;
hence
x in L~ g2
by A54, A145, JORDAN3:1;
verum
end;
then
{(f . i1)} \/ {(f . i2)} c= L~ g2
by A55, XBOOLE_1:8;
then A146:
{(f . i1),(f . i2)} c= L~ g2
by ENUMSET1:1;
{(f . i2)} c= L~ g1
then
{(f . i1)} \/ {(f . i2)} c= L~ g1
by A17, XBOOLE_1:8;
then
{(f . i1),(f . i2)} c= L~ g1
by ENUMSET1:1;
then A148:
{(f . i1),(f . i2)} c= (L~ g1) /\ (L~ g2)
by A146, XBOOLE_1:19;
L~ (mid (f,((len f) -' 1),i2)) c= L~ f
by A3, A9, A26, A23, Th35;
then A149:
L~ g2 c= L~ f
by A5, A32, A30, XBOOLE_1:8;
L~ g1 c= L~ f
by A1, A3, A4, A9, A6, Th35;
then
(L~ g1) \/ (L~ g2) c= L~ f
by A149, XBOOLE_1:8;
hence
( (L~ g1) /\ (L~ g2) = {(f . i1),(f . i2)} & (L~ g1) \/ (L~ g2) = L~ f )
by A58, A148, A33, XBOOLE_0:def 10; verum