let f be non constant standard special_circular_sequence; :: thesis: for i1, i2 being Element of 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 Element of NAT ; :: thesis: 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); :: thesis: ( 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) ; :: thesis: ( (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, Th47;
A9: 1 < i2 by A1, A2, XXREAL_0:2;
then A10: len (mid f,i1,i2) = (i2 -' i1) + 1 by A1, A2, A3, A6, JORDAN3:27;
A11: i2 + 1 <= len f by A3, NAT_1:13;
then A12: (i2 + 1) - 1 <= (len f) - 1 by XREAL_1:11;
then A13: i2 <= (len f) -' 1 by A1, A6, XREAL_1:235, XXREAL_0:2;
then A14: (((len f) -' 1) -' i2) + 1 = (((len f) -' 1) - i2) + 1 by XREAL_1:235
.= (((len f) - 1) - i2) + 1 by A1, A6, XREAL_1:235, XXREAL_0:2
.= (len f) - i2 ;
A15: 0 < i2 - i1 by A2, XREAL_1:52;
then 0 < i2 -' i1 by A2, XREAL_1:235;
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
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(f . i1)} or x in L~ g1 )
assume x in {(f . i1)} ; :: thesis: x in L~ g1
then A18: x = f . i1 by TARSKI:def 1;
g1 . 1 = f . i1 by A1, A3, A4, A9, A6, JORDAN3:27;
hence x in L~ g1 by A16, A18, JORDAN3:34; :: thesis: verum
end;
A19: 0 + 1 <= (((len f) -' 1) -' i2) + 1 by NAT_1:13;
A20: len (mid f,i1,1) = (i1 -' 1) + 1 by A1, A6, Th21;
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:237, XXREAL_0:2;
then A24: len (mid f,((len f) -' 1),i2) = (((len f) -' 1) -' i2) + 1 by A9, A13, Th21;
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:24
.= (mid f,((len f) -' 1),i2) . 1 by A3, A9, A26, A23, JORDAN3:27
.= (mid f,((len f) -' 1),i2) /. 1 by A25, FINSEQ_4:24 ;
((len f) -' 1) + 1 = len f by A1, A6, XREAL_1:237, XXREAL_0:2;
then A28: LSeg f,((len f) -' 1) = LSeg (f /. (((len f) -' 1) + 1)),(f /. ((len f) -' 1)) by A26, TOPREAL1:def 5;
A29: f /. (((len f) -' 1) + 1) = f /. (len f) by A1, A6, XREAL_1:237, XXREAL_0:2
.= f /. 1 by FINSEQ_6:def 1
.= f . 1 by A7, FINSEQ_4:24
.= (mid f,i1,1) . (len (mid f,i1,1)) by A1, A6, A7, Th23
.= (mid f,i1,1) /. (len (mid f,i1,1)) by A21, FINSEQ_4:24 ;
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:26;
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 set ; :: according to TARSKI:def 3 :: thesis: ( not x in L~ f or x in (L~ g1) \/ (L~ g2) )
assume A34: x in L~ f ; :: thesis: x in (L~ g1) \/ (L~ g2)
then reconsider p = x as Point of (TOP-REAL 2) ;
consider i being Element of 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
per cases ( ( i1 <= i & i < i2 ) or i < i1 or i2 <= i ) ;
case A38: ( i1 <= i & i < i2 ) ; :: thesis: x in (L~ g1) \/ (L~ g2)
then i - i1 < i2 - i1 by XREAL_1:11;
then (i - i1) + 1 < (i2 - i1) + 1 by XREAL_1:8;
then (i -' i1) + 1 < (i2 - i1) + 1 by A38, XREAL_1:235;
then A39: (i -' i1) + 1 < (i2 -' i1) + 1 by A2, XREAL_1:235;
0 <= i - i1 by A38, XREAL_1:50;
then 0 + 1 <= (i - i1) + 1 by XREAL_1:8;
then A40: 1 <= (i -' i1) + 1 by A38, XREAL_1:235;
(((i -' i1) + 1) + i1) -' 1 = (((i -' i1) + 1) + i1) - 1 by A1, NAT_D:37
.= (i -' i1) + i1
.= i by A38, XREAL_1:237 ;
then x in LSeg (mid f,i1,i2),((i -' i1) + 1) by A1, A2, A3, A37, A40, A39, Th31;
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; :: thesis: verum
end;
case A41: i < i1 ; :: thesis: x in (L~ g1) \/ (L~ g2)
i1 + 1 <= i1 + i by A35, XREAL_1:8;
then i1 < i1 + i by NAT_1:13;
then i1 - i < (i1 + i) - i by XREAL_1:11;
then i1 -' i < (i1 - 1) + 1 by A41, XREAL_1:235;
then A42: i1 -' i < (i1 -' 1) + 1 by A1, XREAL_1:235;
i1 <= i1 + i by NAT_1:11;
then i1 - i <= (i1 + i) - i by XREAL_1:11;
then i1 -' i <= i1 by A41, XREAL_1:235;
then A43: i1 -' (i1 -' i) = i1 - (i1 -' i) by XREAL_1:235
.= i1 - (i1 - i) by A41, XREAL_1:235
.= i ;
i + 1 <= i1 by A41, NAT_1:13;
then (i + 1) - i <= i1 - i by XREAL_1:11;
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, Th32;
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; :: thesis: verum
end;
case A45: i2 <= i ; :: thesis: x in (L~ g1) \/ (L~ g2)
now
per cases ( i + 1 = len f or i + 1 < len f ) by A36, XXREAL_0:1;
case i + 1 = len f ; :: thesis: 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:235, 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; :: thesis: verum
end;
case i + 1 < len f ; :: thesis: 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:11;
then A46: i + 1 <= (len f) -' 1 by A1, A6, XREAL_1:235, 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:235
.= 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:8;
then (((len f) -' 1) + i2) - i2 < (((len f) -' 1) + (i + 1)) - i2 by XREAL_1:11;
then ((len f) -' 1) - i < (((((len f) -' 1) + 1) + i) - i2) - i by XREAL_1:11;
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:235, XXREAL_0:2;
then A49: ((len f) -' 1) -' i < (((len f) -' 1) -' i2) + 1 by A47, XREAL_1:235;
(i + 1) - i <= ((len f) -' 1) - i by A46, XREAL_1:11;
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, Th32;
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; :: thesis: 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; :: thesis: verum
end;
end;
end;
hence x in (L~ g1) \/ (L~ g2) ; :: thesis: verum
end;
A51: i1 + 1 <= len f by A6, NAT_1:13;
(i2 + 1) - i2 <= (len f) - i2 by A11, XREAL_1:11;
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:35
.= ((i1 -' 1) + 1) + ((((len f) -' 1) -' i2) + 1) by A1, A6, A24, Th21
.= i1 + ((((len f) -' 1) -' i2) + 1) by A1, XREAL_1:237 ;
then A54: 1 + 1 <= len g2 by A1, A19, XREAL_1:9;
A55: {(f . i1)} c= L~ g2
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(f . i1)} or x in L~ g2 )
assume x in {(f . i1)} ; :: thesis: x in L~ g2
then A56: x = f . i1 by TARSKI:def 1;
g2 . 1 = (mid f,i1,1) . 1 by A5, A21, FINSEQ_1:85
.= f . i1 by A1, A6, A7, JORDAN3:27 ;
hence x in L~ g2 by A54, A56, JORDAN3:34; :: thesis: verum
end;
A57: ((len f) -' 1) + 1 = len f by A1, A6, XREAL_1:237, XXREAL_0:2;
A58: (L~ g1) /\ (L~ g2) c= {(f . i1),(f . i2)}
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (L~ g1) /\ (L~ g2) or x in {(f . i1),(f . i2)} )
assume A59: x in (L~ g1) /\ (L~ g2) ; :: thesis: 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 Element of 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, Th31;
i + 1 <= (i2 -' i1) + 1 by A1, A2, A3, A9, A6, A61, JORDAN3:27;
then A65: (i + 1) - 1 <= ((i2 -' i1) + 1) - 1 by XREAL_1:11;
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
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) ; :: thesis: x in {(f . i1),(f . i2)}
then consider k being Element of 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
per cases ( i1 <> 1 or i1 = 1 ) ;
case i1 <> 1 ; :: thesis: 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:11;
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:237;
then A74: i1 -' k = i1 - k by A73, XREAL_1:235;
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, Th32;
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:9;
then 1 < i + k by XXREAL_0:2;
then 1 - k < (i + k) - k by XREAL_1:11;
then (1 - k) - 1 < i - 1 by XREAL_1:11;
then i1 + ((1 - k) - 1) < i1 + (i - 1) by XREAL_1:8;
then A78: (i1 -' k) + 1 <= (i + i1) -' 1 by A74, A72, NAT_1:13;
A79: now
i < (i2 - i1) + 1 by A2, A63, XREAL_1:235;
then A80: i + i1 < ((i2 - i1) + 1) + i1 by XREAL_1:8;
assume (i1 -' k) + 1 <> (i + i1) -' 1 ; :: thesis: contradiction
then A81: (i1 -' k) + 1 < (i + i1) -' 1 by A78, XXREAL_0:1;
i2 + 1 <= len f by A3, NAT_1:13;
then ((i + i1) - 1) + 1 < len f by A80, XXREAL_0:2;
hence contradiction by A72, A77, A81, GOBOARD5:def 4; :: thesis: verum
end;
then A82: 1 + 1 = ((i + k) - 1) + 1 by A74, A72;
A83: now
assume A84: ( not i = 1 or not k = 1 ) ; :: thesis: contradiction
hence contradiction ; :: thesis: 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:237 ;
then x in {(f /. ((i1 -' k) + 1))} by A51, A76, A79, A71, TOPREAL1:def 8;
then A86: x = f /. i1 by A79, A85, TARSKI:def 1;
f /. i1 = f . i1 by A1, A6, FINSEQ_4:24;
hence x in {(f . i1),(f . i2)} by A86, TARSKI:def 2; :: thesis: verum
end;
case A87: i1 = 1 ; :: thesis: contradiction
A88: 1 + 1 <= k + 1 by A67, XREAL_1:8;
len (mid f,1,1) = 1 by A7, Th27;
hence contradiction by A68, A87, A88, XXREAL_0:2; :: thesis: verum
end;
end;
end;
hence x in {(f . i1),(f . i2)} ; :: thesis: verum
end;
case A89: x in LSeg ((mid f,i1,1) /. (len (mid f,i1,1))),((mid f,((len f) -' 1),i2) /. 1) ; :: thesis: x in {(f . i1),(f . i2)}
(i2 + 1) - i2 <= (len f) - i2 by A11, XREAL_1:11;
then A90: (mid f,((len f) -' 1),i2) /. 1 = (mid f,((len f) -' 1),i2) . 1 by A24, A14, FINSEQ_4:24
.= f . ((len f) -' 1) by A3, A9, A26, A23, JORDAN3:27
.= f /. ((len f) -' 1) by A26, A23, FINSEQ_4:24 ;
(mid f,i1,1) /. (len (mid f,i1,1)) = (mid f,i1,1) . (len (mid f,i1,1)) by A21, FINSEQ_4:24
.= f . 1 by A1, A6, A7, Th23
.= f /. 1 by A7, FINSEQ_4:24
.= f /. (len f) by FINSEQ_6:def 1 ;
then x in LSeg f,((len f) -' 1) by A26, A57, A89, A90, TOPREAL1:def 5;
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
per cases ( 1 < i1 or 1 < i or ( not 1 < i1 & not 1 < i ) ) ;
case A93: ( 1 < i1 or 1 < i ) ; :: thesis: x in {(f . i1),(f . i2)}
A94: now
1 + 1 < i + i1 by A1, A60, A93, XREAL_1:10;
then 1 + 1 < ((i + i1) -' 1) + 1 by XREAL_1:237, XXREAL_0:2;
then A95: (1 + 1) - 1 < (((i + i1) -' 1) + 1) - 1 by XREAL_1:11;
assume A96: ((i + i1) -' 1) + 1 < (len f) -' 1 ; :: thesis: contradiction
(len f) -' 1 < len f by A1, A6, A22, XREAL_1:237, XXREAL_0:2;
hence contradiction by A92, A96, A95, GOBOARD5:def 4; :: thesis: 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:235, XXREAL_0:2;
1 + 1 <= i + i1 by A1, A60, XREAL_1:9;
then (1 + 1) - 1 <= (i + i1) - 1 by XREAL_1:11;
then A98: 1 <= (i + i1) -' 1 by A1, NAT_D:37;
i <= i2 - i1 by A2, A65, XREAL_1:235;
then i + i1 <= (i2 - i1) + i1 by XREAL_1:8;
then i + i1 < len f by A3, XXREAL_0:2;
then (i + i1) - 1 < (len f) - 1 by XREAL_1:11;
then (i + i1) -' 1 < (len f) - 1 by A1, NAT_D:37;
then (i + i1) -' 1 < (len f) -' 1 by A1, A6, XREAL_1:235, 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;
now
i + i1 <= (i2 -' i1) + i1 by A65, XREAL_1:8;
then A102: i + i1 <= (i2 - i1) + i1 by A15, XREAL_0:def 2;
assume i2 < (len f) -' 1 ; :: thesis: contradiction
hence contradiction by A99, A94, A101, A102, XXREAL_0:1; :: thesis: verum
end;
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 8;
then A104: x = f /. i2 by A103, TARSKI:def 1;
f /. i2 = f . i2 by A3, A9, FINSEQ_4:24;
hence x in {(f . i1),(f . i2)} by A104, TARSKI:def 2; :: thesis: verum
end;
case A105: ( not 1 < i1 & not 1 < i ) ; :: thesis: 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 Th54;
then x = f . 1 by A91, A106, TARSKI:def 1;
hence x in {(f . i1),(f . i2)} by A107, TARSKI:def 2; :: thesis: verum
end;
end;
end;
hence x in {(f . i1),(f . i2)} ; :: thesis: verum
end;
case x in L~ (mid f,((len f) -' 1),i2) ; :: thesis: x in {(f . i1),(f . i2)}
then consider k being Element of 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:235;
then k + 1 <= (len f) -' i2 by NAT_1:13;
then (k + 1) - 1 <= ((len f) -' i2) - 1 by XREAL_1:11;
then A113: k <= ((len f) -' i2) -' 1 by A52, XREAL_1:235;
A114: ((len f) -' i2) -' 1 = ((len f) -' i2) - 1 by A52, XREAL_1:235
.= ((len f) - i2) - 1 by A3, XREAL_1:235
.= ((len f) - 1) - i2
.= ((len f) -' 1) - i2 by A1, A6, XREAL_1:235, XXREAL_0:2
.= ((len f) -' 1) -' i2 by A13, XREAL_1:235 ;
A115: k < (len f) - i2 by A24, A14, A109, NAT_1:13;
then k + i2 < ((len f) - i2) + i2 by XREAL_1:8;
then A116: (k + i2) - k < (len f) - k by XREAL_1:11;
then A117: 1 < (len f) - k by A9, XXREAL_0:2;
then 1 + k < ((len f) - k) + k by XREAL_1:8;
then (1 + k) - 1 < (len f) - 1 by XREAL_1:11;
then A118: k < (len f) -' 1 by A1, A6, XREAL_1:235, 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:235
.= ((len f) - k) - 1 by A116, XREAL_0:def 2
.= ((len f) - 1) - k
.= ((len f) -' 1) - k by A1, A6, XREAL_1:235, XXREAL_0:2
.= ((len f) -' 1) -' k by A118, XREAL_1:235 ;
now
per cases ( i2 <> (len f) -' 1 or i2 = (len f) -' 1 ) ;
case i2 <> (len f) -' 1 ; :: thesis: 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:8;
then A122: k + (i2 -' 1) < (len f) - 1 by A1, A2, XREAL_1:235, 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:8;
then (k + 1) - k < (len f) - k by XREAL_1:11;
then A124: 1 < (len f) -' k by NAT_D:39;
i2 + (((len f) -' 1) - i2) < len f by A1, A6, A22, XREAL_1:237, XXREAL_0:2;
then ((i2 - i1) + i1) + (((len f) -' 1) -' i2) < len f by A13, XREAL_1:235;
then A125: ((i2 -' i1) + i1) + (((len f) -' 1) -' i2) < len f by A2, XREAL_1:235;
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:8;
then A127: (i + i1) + k <= ((i2 -' i1) + i1) + k by XREAL_1:8;
((i2 -' i1) + i1) + k <= ((i2 -' i1) + i1) + (((len f) -' 1) -' i2) by A112, XREAL_1:8;
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:11;
k < (len f) -' 1 by A1, A6, A123, XREAL_1:235, XXREAL_0:2;
then A129: ((len f) -' 1) -' k = ((len f) -' 1) - k by XREAL_1:235;
len f < (len f) + 1 by NAT_1:13;
then (len f) - 1 < ((len f) + 1) - 1 by XREAL_1:11;
then (len f) -' k = (len f) - k by A123, XREAL_1:235, XXREAL_0:2;
then (i + i1) - 1 < ((len f) -' k) - 1 by A128, XREAL_1:11;
then (i + i1) - 1 < ((len f) -' k) -' 1 by A124, XREAL_1:235;
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:237, XXREAL_0:2;
then A131: LSeg (mid f,((len f) -' 1),i2),k = LSeg f,(((len f) -' 1) -' k) by A108, A126, A120, A121, Th32;
then A132: LSeg f,((i + i1) -' 1) meets LSeg f,(((len f) -' 1) -' k) by A62, A64, A110, XBOOLE_0:3;
A133: now
((len f) -' 1) + 1 <= ((len f) -' 1) + k by A108, XREAL_1:8;
then (((len f) -' 1) + 1) - k <= (((len f) -' 1) + k) - k by XREAL_1:11;
then A134: (((len f) -' 1) -' k) + 1 < len f by A23, A129, XXREAL_0:2;
assume not ((i + i1) -' 1) + 1 = ((len f) -' 1) -' k ; :: thesis: contradiction
then ((i + i1) -' 1) + 1 < ((len f) -' 1) -' k by A130, XXREAL_0:1;
hence contradiction by A132, A134, GOBOARD5:def 4; :: thesis: verum
end;
(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:235, XXREAL_0:2;
A136: now
assume A137: ( not i = i2 -' i1 or not k = ((len f) -' 1) -' i2 ) ; :: thesis: contradiction
now
per cases ( i <> i2 -' i1 or k <> ((len f) -' 1) -' i2 ) by A137;
case i <> i2 -' i1 ; :: thesis: contradiction
then i < i2 -' i1 by A65, XXREAL_0:1;
then i + k < (i2 -' i1) + (((len f) -' i2) -' 1) by A113, XREAL_1:10;
then i + k < (i2 - i1) + (((len f) -' i2) -' 1) by A2, XREAL_1:235;
then i + k < (i2 - i1) + (((len f) -' i2) - 1) by A52, XREAL_1:235;
then i + k < (i2 - i1) + (((len f) - i2) - 1) by A3, XREAL_1:235;
hence contradiction by A135; :: thesis: verum
end;
case k <> ((len f) -' 1) -' i2 ; :: thesis: contradiction
then k < ((len f) -' 1) -' i2 by A112, XXREAL_0:1;
then i + k < (i2 -' i1) + (((len f) -' i2) -' 1) by A65, A114, XREAL_1:10;
then i + k < (i2 - i1) + (((len f) -' i2) -' 1) by A2, XREAL_1:235;
then i + k < (i2 - i1) + (((len f) -' i2) - 1) by A52, XREAL_1:235;
then i + k < (i2 - i1) + (((len f) - i2) - 1) by A3, XREAL_1:235;
hence contradiction by A135; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
then (i + i1) -' 1 = ((i2 -' i1) + i1) - 1 by A1, NAT_D:37
.= ((i2 - i1) + i1) - 1 by A2, XREAL_1:235
.= 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:11;
A140: (len f) -' 1 = (len f) - 1 by A1, A6, XREAL_1:235, 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:237, XXREAL_0:2;
then (((len f) -' 1) + 1) - i2 <= ((len f) + i2) - i2 by XREAL_1:11;
then ((((len f) -' 1) + 1) - i2) - 1 <= (len f) - 1 by XREAL_1:11;
then ((len f) -' 1) - i2 <= (len f) - 1 ;
then ((len f) -' 1) -' i2 <= (len f) -' 1 by A12, A140, XREAL_1:235;
then A141: ((len f) -' 1) -' k = ((len f) -' 1) - (((len f) -' 1) -' i2) by A136, XREAL_1:235
.= ((len f) - 1) - (((len f) - 1) - i2) by A12, A140, XREAL_1:235
.= 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 8;
then x = f /. i2 by A133, A141, TARSKI:def 1;
then x = f . i2 by A3, A9, FINSEQ_4:24;
hence x in {(f . i1),(f . i2)} by TARSKI:def 2; :: thesis: verum
end;
case A142: i2 = (len f) -' 1 ; :: thesis: contradiction
A143: 1 + 1 <= k + 1 by A108, XREAL_1:8;
len (mid f,((len f) -' 1),((len f) -' 1)) = 1 by A26, A23, Th27;
hence contradiction by A109, A142, A143, XXREAL_0:2; :: thesis: verum
end;
end;
end;
hence x in {(f . i1),(f . i2)} ; :: thesis: verum
end;
end;
end;
hence x in {(f . i1),(f . i2)} ; :: thesis: verum
end;
A144: len (mid f,i1,1) = i1 by A1, A20, XREAL_1:237;
{(f . i2)} c= L~ g2
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(f . i2)} or x in L~ g2 )
assume x in {(f . i2)} ; :: thesis: 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:86
.= f . i2 by A3, A9, A26, A23, A24, Th23 ;
hence x in L~ g2 by A54, A145, JORDAN3:34; :: thesis: 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:41;
{(f . i2)} c= L~ g1
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(f . i2)} or x in L~ g1 )
assume x in {(f . i2)} ; :: thesis: x in L~ g1
then A147: x = f . i2 by TARSKI:def 1;
g1 . (len g1) = f . i2 by A1, A3, A4, A9, A6, Th23;
hence x in L~ g1 by A16, A147, JORDAN3:34; :: thesis: verum
end;
then {(f . i1)} \/ {(f . i2)} c= L~ g1 by A17, XBOOLE_1:8;
then {(f . i1),(f . i2)} c= L~ g1 by ENUMSET1:41;
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, Th47;
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, Th47;
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; :: thesis: verum