let f be constant standard special_circular_sequence; :: thesis: 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; :: 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, 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

proof

let x be object ; :: 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, FINSEQ_6:118;
hence x in L~ g1 by A16, A18, JORDAN3:1; :: 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, FINSEQ_6:187;
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, FINSEQ_6:187;
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, FINSEQ_6:189
.= (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 ; :: 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 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 :: thesis: ( ( 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 ) ; :: thesis: 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; :: thesis: verum

end;

case A41: i < i1 ; :: thesis: 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; :: thesis: verum

end;

case A45: i2 <= i ; :: thesis: x in (L~ g1) \/ (L~ g2)

now :: thesis: ( ( 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 ; :: 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: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; :: 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: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; :: 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: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, FINSEQ_6:187
.= 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

proof

let x be object ; :: 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:64
.= f . i1 by A1, A6, A7, FINSEQ_6:118 ;
hence x in L~ g2 by A54, A56, JORDAN3:1; :: thesis: verum

end;

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 ; :: 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 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 :: thesis: ( ( 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)) ; :: thesis: 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 :: thesis: ( ( i1 <> 1 & x in {(f . i1),(f . i2)} ) or ( i1 = 1 & contradiction ) )

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

A79: now :: thesis: not (i1 -' k) + 1 <> (i + i1) -' 1

i < (i2 - i1) + 1 by A2, A63, XREAL_1:233;
then A80: i + i1 < ((i2 - i1) + 1) + i1 by XREAL_1:6;
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 :: thesis: ( i = 1 & k = 1 )

assume A84: ( not i = 1 or not k = 1 ) ; :: thesis: contradiction

now :: thesis: ( ( i <> 1 & contradiction ) or ( k <> 1 & contradiction ) )

per cases ( i <> 1 or k <> 1 ) by A84;

case i <> 1 ; :: thesis: contradiction

then 1 < i by A60, XXREAL_0:1;
hence contradiction by A67, A82, XREAL_1:8; :: thesis: verum

end;

case k <> 1 ; :: thesis: contradiction

then 1 < k by A67, XXREAL_0:1;
hence contradiction by A60, A82, XREAL_1:8; :: thesis: verum

end;

end;

end;

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

end;

case A87: i1 = 1 ; :: thesis: contradiction

A88: 1 + 1 <= k + 1 by A67, XREAL_1:6;
1 <= len f by A6, A87;
then 1 in dom f by FINSEQ_3:25;
then len (mid (f,1,1)) = 1 by FINSEQ_6:193;
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: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, FINSEQ_6:189
.= 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 :: thesis: ( ( ( 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 ) ; :: thesis: x in {(f . i1),(f . i2)}

A94: now :: thesis: 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 ; :: thesis: 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; :: 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: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;

now :: thesis: not i2 < (len f) -' 1

i + i1 <= (i2 -' i1) + i1 by A65, XREAL_1:6;
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 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; :: 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 Th42;
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 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 :: thesis: ( ( 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 ; :: 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: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;

A133: now :: thesis: ((i + i1) -' 1) + 1 = ((len f) -' 1) -' k

((len f) -' 1) + 1 <= ((len f) -' 1) + k by A108, XREAL_1:6;
then (((len f) -' 1) + 1) - k <= (((len f) -' 1) + k) - k by XREAL_1:9;
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:233, XXREAL_0:2;

A136: now :: thesis: ( i = i2 -' i1 & k = ((len f) -' 1) -' i2 )

assume A137: ( not i = i2 -' i1 or not k = ((len f) -' 1) -' i2 ) ; :: thesis: contradiction

now :: thesis: ( ( i <> i2 -' i1 & contradiction ) or ( k <> ((len f) -' 1) -' i2 & contradiction ) )

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:8;
then i + k < (i2 - i1) + (((len f) -' i2) -' 1) by A2, XREAL_1:233;
then i + k < (i2 - i1) + (((len f) -' i2) - 1) by A52, XREAL_1:233;
then i + k < (i2 - i1) + (((len f) - i2) - 1) by A3, XREAL_1:233;
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:8;
then i + k < (i2 - i1) + (((len f) -' i2) -' 1) by A2, XREAL_1:233;
then i + k < (i2 - i1) + (((len f) -' i2) - 1) by A52, XREAL_1:233;
then i + k < (i2 - i1) + (((len f) - i2) - 1) by A3, XREAL_1:233;
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: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; :: thesis: verum

end;

case A142: i2 = (len f) -' 1 ; :: thesis: contradiction

A143: 1 + 1 <= k + 1 by A108, XREAL_1:6;
1 <= i2 by A26, A142;
then i2 in dom f by A3, FINSEQ_3:25;
then len (mid (f,((len f) -' 1),((len f) -' 1))) = 1 by A142, FINSEQ_6:193;
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:235;
{(f . i2)} c= L~ g2

proof

let x be object ; :: 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:65
.= f . i2 by A3, A9, A26, A23, A24, FINSEQ_6:189 ;
hence x in L~ g2 by A54, A145, JORDAN3:1; :: 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:1;
{(f . i2)} c= L~ g1

proof

let x be object ; :: 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, FINSEQ_6:189;
hence x in L~ g1 by A16, A147, JORDAN3:1; :: 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: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; :: thesis: verum