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 A1: ( 1 <= i1 & i1 < i2 & i2 < len f & g1 = mid f,i1,i2 & 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 )
then A2: 1 < i2 by XXREAL_0:2;
A3: i1 < len f by A1, XXREAL_0:2;
then A4: 1 < len f by A1, XXREAL_0:2;
A5: i1 + 1 <= len f by A3, NAT_1:13;
A6: i2 + 1 <= len f by A1, NAT_1:13;
then A7: (i2 + 1) - 1 <= (len f) - 1 by XREAL_1:11;
then A8: i2 <= (len f) -' 1 by A1, A3, XREAL_1:235, XXREAL_0:2;
then A9: 1 < (len f) -' 1 by A2, XXREAL_0:2;
(i2 + 1) - i2 <= (len f) - i2 by A6, XREAL_1:11;
then A10: 1 <= (len f) -' i2 by NAT_D:39;
A11: ((len f) -' 1) + 1 = len f by A1, A3, XREAL_1:237, XXREAL_0:2;
A12: (len f) -' 1 < ((len f) -' 1) + 1 by NAT_1:13;
then A13: (len f) -' 1 < len f by A1, A3, XREAL_1:237, XXREAL_0:2;
A14: len (mid f,i1,i2) = (i2 -' i1) + 1 by A1, A2, A3, JORDAN3:27;
A15: 0 < i2 - i1 by A1, XREAL_1:52;
then 0 < i2 -' i1 by A1, XREAL_1:235;
then 0 + 1 <= i2 -' i1 by NAT_1:13;
then 1 < len g1 by A1, A14, NAT_1:13;
then A16: 1 + 1 <= len g1 by NAT_1:13;
A17: len (mid f,i1,1) = (i1 -' 1) + 1 by A1, A3, Th21;
then A18: len (mid f,i1,1) = i1 by A1, XREAL_1:237;
A19: mid f,i1,1 <> <*> (TOP-REAL 2) by A17, FINSEQ_1:32;
A20: 0 + 1 <= len (mid f,i1,1) by A17, NAT_1:13;
A21: len (mid f,((len f) -' 1),i2) = (((len f) -' 1) -' i2) + 1 by A2, A8, A13, Th21;
A22: (((len f) -' 1) -' i2) + 1 = (((len f) -' 1) - i2) + 1 by A8, XREAL_1:235
.= (((len f) - 1) - i2) + 1 by A1, A3, XREAL_1:235, XXREAL_0:2
.= (len f) - i2 ;
A23: mid f,((len f) -' 1),i2 <> <*> (TOP-REAL 2) by A21, FINSEQ_1:32;
A24: 0 + 1 <= (((len f) -' 1) -' i2) + 1 by NAT_1:13;
A25: len g2 = (len (mid f,i1,1)) + (len (mid f,((len f) -' 1),i2)) by A1, FINSEQ_1:35
.= ((i1 -' 1) + 1) + ((((len f) -' 1) -' i2) + 1) by A1, A3, A21, Th21
.= i1 + ((((len f) -' 1) -' i2) + 1) by A1, XREAL_1:237 ;
then A26: 1 + 1 <= len g2 by A1, A24, XREAL_1:9;
A27: 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 A19, A23, SPPOL_2:23;
A28: (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 A29: x in (L~ g1) /\ (L~ g2) ; :: thesis: x in {(f . i1),(f . i2)}
then A30: ( x in L~ g1 & x in L~ g2 ) by XBOOLE_0:def 4;
reconsider p = x as Point of (TOP-REAL 2) by A29;
A31: ( x in L~ (mid f,i1,i2) & x in L~ ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) ) by A1, A29, XBOOLE_0:def 4;
consider i being Element of NAT such that
A32: ( 1 <= i & i + 1 <= len (mid f,i1,i2) & p in LSeg (mid f,i1,i2),i ) by A1, A30, SPPOL_2:13;
A33: i < (i2 -' i1) + 1 by A14, A32, NAT_1:13;
then A34: LSeg (mid f,i1,i2),i = LSeg f,((i + i1) -' 1) by A1, A32, Th31;
i + 1 <= (i2 -' i1) + 1 by A1, A2, A3, A32, JORDAN3:27;
then A35: (i + 1) - 1 <= ((i2 -' i1) + 1) - 1 by XREAL_1:11;
A36: ( 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 A27, A31, 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 A36, 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
A37: ( 1 <= k & k + 1 <= len (mid f,i1,1) & 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 A38: ( 1 <= 1 & 1 < i1 & i1 <= len f & 1 <= k & k < (i1 -' 1) + 1 ) by A1, A17, A37, NAT_1:13, XXREAL_0:1, XXREAL_0:2;
then A39: LSeg (mid f,i1,1),k = LSeg f,(i1 -' k) by Th32;
(i1 -' 1) + 1 = i1 by A1, XREAL_1:237;
then A40: i1 -' k = i1 - k by A38, XREAL_1:235;
A41: (i + i1) -' 1 = (i + i1) - 1 by A1, NAT_D:37;
set k3 = i1 -' k;
set i3 = (i + i1) -' 1;
A42: x in (LSeg f,(i1 -' k)) /\ (LSeg f,((i + i1) -' 1)) by A32, A34, A37, A39, XBOOLE_0:def 4;
A43: LSeg f,(i1 -' k) meets LSeg f,((i + i1) -' 1) by A32, A34, A37, A39, XBOOLE_0:3;
1 + 1 <= i + k by A32, A37, 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 A44: (i1 -' k) + 1 <= (i + i1) -' 1 by A40, A41, NAT_1:13;

A45: now

assume (i1 -' k) + 1 <> (i + i1) -' 1 ; :: thesis: contradiction
then A46: (i1 -' k) + 1 < (i + i1) -' 1 by A44, XXREAL_0:1;
i < (i2 - i1) + 1 by A1, A33, XREAL_1:235;
then A47: i + i1 < ((i2 - i1) + 1) + i1 by XREAL_1:8;
i2 + 1 <= len f by A1, NAT_1:13;
then ((i + i1) - 1) + 1 < len f by A47, XXREAL_0:2;
hence contradiction by A41, A43, A46, GOBOARD5:def 4; :: thesis: verum

end;

then A48: 1 + 1 = ((i + k) - 1) + 1 by A40, A41;

A49: now

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

now

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

case i <> 1 ; :: thesis: contradiction

then 1 < i by A32, XXREAL_0:1;
hence contradiction by A37, A48, XREAL_1:10; :: thesis: verum

end;

case k <> 1 ; :: thesis: contradiction

then 1 < k by A37, XXREAL_0:1;
hence contradiction by A32, A48, XREAL_1:10; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

then A51: (i + i1) -' 1 = i1 by NAT_D:34;
1 + 1 <= i1 by A38, NAT_1:13;
then A52: (1 + 1) - 1 <= i1 - 1 by XREAL_1:11;
(i1 -' k) + 2 = ((i1 -' 1) + 1) + 1 by A49
.= i1 + 1 by A1, XREAL_1:237 ;
then x in {(f /. ((i1 -' k) + 1))} by A5, A42, A45, A52, TOPREAL1:def 8;
then A53: x = f /. i1 by A45, A51, TARSKI:def 1;
f /. i1 = f . i1 by A1, A3, FINSEQ_4:24;
hence x in {(f . i1),(f . i2)} by A53, TARSKI:def 2; :: thesis: verum

end;

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

A55: len (mid f,1,1) = 1 by A4, Th27;
1 + 1 <= k + 1 by A37, XREAL_1:8;
hence contradiction by A37, A54, A55, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence x in {(f . i1),(f . i2)} ; :: thesis: verum

end;

case A56: 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)}

A57: (mid f,i1,1) /. (len (mid f,i1,1)) = (mid f,i1,1) . (len (mid f,i1,1)) by A20, FINSEQ_4:24
.= f . 1 by A1, A3, A4, Th23
.= f /. 1 by A4, FINSEQ_4:24
.= f /. (len f) by FINSEQ_6:def 1 ;
(i2 + 1) - i2 <= (len f) - i2 by A6, XREAL_1:11;
then (mid f,((len f) -' 1),i2) /. 1 = (mid f,((len f) -' 1),i2) . 1 by A21, A22, FINSEQ_4:24
.= f . ((len f) -' 1) by A1, A2, A9, A13, JORDAN3:27
.= f /. ((len f) -' 1) by A9, A13, FINSEQ_4:24 ;
then x in LSeg f,((len f) -' 1) by A9, A11, A56, A57, TOPREAL1:def 5;
then A58: x in (LSeg f,((i + i1) -' 1)) /\ (LSeg f,((len f) -' 1)) by A32, A34, XBOOLE_0:def 4;
then A59: 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 A60: ( 1 < i1 or 1 < i ) ; :: thesis: x in {(f . i1),(f . i2)}

i <= i2 - i1 by A1, A35, XREAL_1:235;
then i + i1 <= (i2 - i1) + i1 by XREAL_1:8;
then i + i1 < len f by A1, 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, A3, XREAL_1:235, XXREAL_0:2;
then A61: ((i + i1) -' 1) + 1 <= (len f) -' 1 by NAT_1:13;

A62: now

assume A63: ((i + i1) -' 1) + 1 < (len f) -' 1 ; :: thesis: contradiction
1 + 1 < i + i1 by A1, A32, A60, XREAL_1:10;
then 1 + 1 < ((i + i1) -' 1) + 1 by XREAL_1:237, XXREAL_0:2;
then (1 + 1) - 1 < (((i + i1) -' 1) + 1) - 1 by XREAL_1:11;
then ( (i + i1) -' 1 > 1 & (len f) -' 1 < len f ) by A1, A3, A12, XREAL_1:237, XXREAL_0:2;
hence contradiction by A59, A63, GOBOARD5:def 4; :: thesis: verum

end;

then A64: ((i + i1) -' 1) + 1 = (len f) -' 1 by A61, XXREAL_0:1;
set i3 = (i + i1) -' 1;
1 + 1 <= i + i1 by A1, A32, XREAL_1:9;
then A65: (1 + 1) - 1 <= (i + i1) - 1 by XREAL_1:11;
((len f) - 1) + 1 <= len f ;
then ((len f) -' 1) + 1 <= len f by A1, A3, XREAL_1:235, XXREAL_0:2;
then A66: ( 1 <= (i + i1) -' 1 & ((i + i1) -' 1) + 2 <= len f ) by A1, A64, A65, NAT_D:37;
A67: ((i + i1) -' 1) + 1 = (len f) -' 1 by A61, A62, XXREAL_0:1;
A68: (i + i1) -' 1 = (i + i1) - 1 by A1, NAT_D:37;

now

assume A69: i2 < (len f) -' 1 ; :: thesis: contradiction
i + i1 <= (i2 -' i1) + i1 by A35, XREAL_1:8;
then i + i1 <= (i2 - i1) + i1 by A15, XREAL_0:def 2;
hence contradiction by A61, A62, A68, A69, XXREAL_0:1; :: thesis: verum

end;

then A70: ((i + i1) -' 1) + 1 = i2 by A8, A67, XXREAL_0:1;
x in {(f /. (((i + i1) -' 1) + 1))} by A58, A66, A67, TOPREAL1:def 8;
then A71: x = f /. i2 by A70, TARSKI:def 1;
f /. i2 = f . i2 by A1, A2, FINSEQ_4:24;
hence x in {(f . i1),(f . i2)} by A71, TARSKI:def 2; :: thesis: verum

end;

case A72: ( not 1 < i1 & not 1 < i ) ; :: thesis: x in {(f . i1),(f . i2)}

then A73: i1 = 1 by A1, XXREAL_0:1;
i = 1 by A32, A72, XXREAL_0:1;
then A74: (i + i1) -' 1 = (1 + 1) -' 1 by A1, A72, XXREAL_0:1
.= 1 by NAT_D:34 ;
(LSeg f,1) /\ (LSeg f,((len f) -' 1)) = {(f . 1)} by Th54;
then x = f . 1 by A58, A74, TARSKI:def 1;
hence x in {(f . i1),(f . i2)} by A73, 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
A75: ( 1 <= k & k + 1 <= len (mid f,((len f) -' 1),i2) & p in LSeg (mid f,((len f) -' 1),i2),k ) by SPPOL_2:13;
A76: k < (((len f) -' 1) -' i2) + 1 by A21, A75, NAT_1:13;
A77: k < (len f) - i2 by A21, A22, A75, NAT_1:13;
k < (len f) -' i2 by A1, A22, A76, 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 A78: k <= ((len f) -' i2) -' 1 by A10, XREAL_1:235;
A79: ((len f) -' i2) -' 1 = ((len f) -' i2) - 1 by A10, XREAL_1:235
.= ((len f) - i2) - 1 by A1, XREAL_1:235
.= ((len f) - 1) - i2
.= ((len f) -' 1) - i2 by A1, A3, XREAL_1:235, XXREAL_0:2
.= ((len f) -' 1) -' i2 by A8, XREAL_1:235 ;
k + i2 < ((len f) - i2) + i2 by A77, XREAL_1:8;
then A80: (k + i2) - k < (len f) - k by XREAL_1:11;
then A81: 1 < (len f) - k by A2, 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 A82: k < (len f) -' 1 by A1, A3, XREAL_1:235, XXREAL_0:2;
1 < (len f) -' k by A81, XREAL_0:def 2;
then A83: ((len f) -' k) -' 1 = ((len f) -' k) - 1 by XREAL_1:235
.= ((len f) - k) - 1 by A80, XREAL_0:def 2
.= ((len f) - 1) - k
.= ((len f) -' 1) - k by A1, A3, XREAL_1:235, XXREAL_0:2
.= ((len f) -' 1) -' k by A82, XREAL_1:235 ;
A84: k <= ((len f) -' 1) -' i2 by A76, NAT_1:13;

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 ( 1 <= i2 & i2 < (len f) -' 1 & (len f) -' 1 <= len f & 1 <= k & k < (((len f) -' 1) -' i2) + 1 ) by A1, A4, A8, A12, A21, A75, NAT_1:13, XREAL_1:237, XXREAL_0:1, XXREAL_0:2;
then A85: LSeg (mid f,((len f) -' 1),i2),k = LSeg f,(((len f) -' 1) -' k) by Th32;
k + (i2 - 1) < ((len f) - i2) + (i2 - 1) by A77, XREAL_1:8;
then A86: k + (i2 -' 1) < (len f) - 1 by A1, XREAL_1:235, XXREAL_0:2;
k <= k + (i2 -' 1) by NAT_1:11;
then A87: k < (len f) - 1 by A86, XXREAL_0:2;
then k < (len f) -' 1 by A1, A3, XREAL_1:235, XXREAL_0:2;
then A88: ((len f) -' 1) -' k = ((len f) -' 1) - k by XREAL_1:235;
k + 1 < ((len f) - 1) + 1 by A87, XREAL_1:8;
then A89: (k + 1) - k < (len f) - k by XREAL_1:11;
len f < (len f) + 1 by NAT_1:13;
then (len f) - 1 < ((len f) + 1) - 1 by XREAL_1:11;
then A90: (len f) -' k = (len f) - k by A87, XREAL_1:235, XXREAL_0:2;
A91: 1 < (len f) -' k by A89, NAT_D:39;
A92: (i + i1) -' 1 = (i + i1) - 1 by A1, NAT_D:37;
set k3 = ((len f) -' 1) -' k;
set i3 = (i + i1) -' 1;
A93: x in (LSeg f,((i + i1) -' 1)) /\ (LSeg f,(((len f) -' 1) -' k)) by A32, A34, A75, A85, XBOOLE_0:def 4;
A94: LSeg f,((i + i1) -' 1) meets LSeg f,(((len f) -' 1) -' k) by A32, A34, A75, A85, XBOOLE_0:3;
i2 + (((len f) -' 1) - i2) < len f by A1, A3, A12, XREAL_1:237, XXREAL_0:2;
then ((i2 - i1) + i1) + (((len f) -' 1) -' i2) < len f by A8, XREAL_1:235;
then A95: ((i2 -' i1) + i1) + (((len f) -' 1) -' i2) < len f by A1, XREAL_1:235;
i + i1 <= (i2 -' i1) + i1 by A35, XREAL_1:8;
then A96: (i + i1) + k <= ((i2 -' i1) + i1) + k by XREAL_1:8;
((i2 -' i1) + i1) + k <= ((i2 -' i1) + i1) + (((len f) -' 1) -' i2) by A84, XREAL_1:8;
then (i + i1) + k <= ((i2 -' i1) + i1) + (((len f) -' 1) -' i2) by A96, XXREAL_0:2;
then (i + i1) + k < len f by A95, XXREAL_0:2;
then ((i + i1) + k) - k < (len f) - k by XREAL_1:11;
then (i + i1) - 1 < ((len f) -' k) - 1 by A90, XREAL_1:11;
then (i + i1) - 1 < ((len f) -' k) -' 1 by A91, XREAL_1:235;
then (i + i1) -' 1 < ((len f) -' 1) -' k by A32, A83, NAT_D:37;
then A97: ((i + i1) -' 1) + 1 <= ((len f) -' 1) -' k by NAT_1:13;

A98: now

assume not ((i + i1) -' 1) + 1 = ((len f) -' 1) -' k ; :: thesis: contradiction
then A99: ((i + i1) -' 1) + 1 < ((len f) -' 1) -' k by A97, XXREAL_0:1;
((len f) -' 1) + 1 <= ((len f) -' 1) + k by A75, XREAL_1:8;
then (((len f) -' 1) + 1) - k <= (((len f) -' 1) + k) - k by XREAL_1:11;
then (((len f) -' 1) -' k) + 1 < len f by A13, A88, XXREAL_0:2;
hence contradiction by A94, A99, GOBOARD5:def 4; :: thesis: verum

end;

then A100: ((len f) - 1) - k = ((i1 + i) - 1) + 1 by A1, A3, A88, A92, XREAL_1:235, XXREAL_0:2;

A101: now

assume A102: ( 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 A102;

case i <> i2 -' i1 ; :: thesis: contradiction

then i < i2 -' i1 by A35, XXREAL_0:1;
then i + k < (i2 -' i1) + (((len f) -' i2) -' 1) by A78, XREAL_1:10;
then i + k < (i2 - i1) + (((len f) -' i2) -' 1) by A1, XREAL_1:235;
then i + k < (i2 - i1) + (((len f) -' i2) - 1) by A10, XREAL_1:235;
then i + k < (i2 - i1) + (((len f) - i2) - 1) by A1, XREAL_1:235;
hence contradiction by A100; :: thesis: verum

end;

case k <> ((len f) -' 1) -' i2 ; :: thesis: contradiction

then k < ((len f) -' 1) -' i2 by A84, XXREAL_0:1;
then i + k < (i2 -' i1) + (((len f) -' i2) -' 1) by A35, A79, XREAL_1:10;
then i + k < (i2 - i1) + (((len f) -' i2) -' 1) by A1, XREAL_1:235;
then i + k < (i2 - i1) + (((len f) -' i2) - 1) by A10, XREAL_1:235;
then i + k < (i2 - i1) + (((len f) - i2) - 1) by A1, XREAL_1:235;
hence contradiction by A100; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

A103: (len f) -' 1 = (len f) - 1 by A1, A3, 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, A3, 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 A7, A103, XREAL_1:235;
then A104: ((len f) -' 1) -' k = ((len f) -' 1) - (((len f) -' 1) -' i2) by A101, XREAL_1:235
.= ((len f) - 1) - (((len f) - 1) - i2) by A7, A103, XREAL_1:235
.= i2 ;
(i + i1) -' 1 = ((i2 -' i1) + i1) - 1 by A1, A101, NAT_D:37
.= ((i2 - i1) + i1) - 1 by A1, XREAL_1:235
.= i2 - 1 ;
then A105: ((i + i1) -' 1) + 2 = i2 + 1 ;
1 + 1 <= i2 by A2, NAT_1:13;
then (1 + 1) - 1 <= i2 - 1 by XREAL_1:11;
then x in {(f /. (((i + i1) -' 1) + 1))} by A6, A93, A98, A105, TOPREAL1:def 8;
then x = f /. i2 by A98, A104, TARSKI:def 1;
then x = f . i2 by A1, A2, FINSEQ_4:24;
hence x in {(f . i1),(f . i2)} by TARSKI:def 2; :: thesis: verum

end;

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

A107: len (mid f,((len f) -' 1),((len f) -' 1)) = 1 by A9, A13, Th27;
1 + 1 <= k + 1 by A75, XREAL_1:8;
hence contradiction by A75, A106, A107, 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;

A108: {(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 A109: x = f . i1 by TARSKI:def 1;
g1 . 1 = f . i1 by A1, A2, A3, JORDAN3:27;
hence x in L~ g1 by A16, A109, JORDAN3:34; :: thesis: verum

end;

{(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 A110: x = f . i2 by TARSKI:def 1;
g1 . (len g1) = f . i2 by A1, A2, A3, Th23;
hence x in L~ g1 by A16, A110, JORDAN3:34; :: thesis: verum

end;

then {(f . i1)} \/ {(f . i2)} c= L~ g1 by A108, XBOOLE_1:8;
then A111: {(f . i1),(f . i2)} c= L~ g1 by ENUMSET1:41;
A112: {(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 A113: x = f . i1 by TARSKI:def 1;
g2 . 1 = (mid f,i1,1) . 1 by A1, A20, FINSEQ_1:85
.= f . i1 by A1, A3, A4, JORDAN3:27 ;
hence x in L~ g2 by A26, A113, JORDAN3:34; :: thesis: verum

end;

{(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 A114: x = f . i2 by TARSKI:def 1;
g2 . (len g2) = (mid f,((len f) -' 1),i2) . ((((len f) -' 1) -' i2) + 1) by A1, A18, A21, A24, A25, FINSEQ_1:86
.= f . i2 by A1, A2, A9, A13, A21, Th23 ;
hence x in L~ g2 by A26, A114, JORDAN3:34; :: thesis: verum

end;

then {(f . i1)} \/ {(f . i2)} c= L~ g2 by A112, XBOOLE_1:8;
then {(f . i1),(f . i2)} c= L~ g2 by ENUMSET1:41;
then A115: {(f . i1),(f . i2)} c= (L~ g1) /\ (L~ g2) by A111, XBOOLE_1:19;
A116: L~ g1 c= L~ f by A1, A2, A3, Th47;
A117: L~ (mid f,i1,1) c= L~ f by A1, A3, A4, Th47;
A118: L~ (mid f,((len f) -' 1),i2) c= L~ f by A1, A2, A9, A13, Th47;
((len f) -' 1) + 1 = len f by A1, A3, XREAL_1:237, XXREAL_0:2;
then A119: LSeg f,((len f) -' 1) = LSeg (f /. (((len f) -' 1) + 1)),(f /. ((len f) -' 1)) by A9, TOPREAL1:def 5;
A120: f /. (((len f) -' 1) + 1) = f /. (len f) by A1, A3, XREAL_1:237, XXREAL_0:2
.= f /. 1 by FINSEQ_6:def 1
.= f . 1 by A4, FINSEQ_4:24
.= (mid f,i1,1) . (len (mid f,i1,1)) by A1, A3, A4, Th23
.= (mid f,i1,1) /. (len (mid f,i1,1)) by A20, FINSEQ_4:24 ;
A121: 1 <= len (mid f,((len f) -' 1),i2) by A21, NAT_1:11;
A122: f /. ((len f) -' 1) = f . ((len f) -' 1) by A9, A13, FINSEQ_4:24
.= (mid f,((len f) -' 1),i2) . 1 by A1, A2, A9, A13, JORDAN3:27
.= (mid f,((len f) -' 1),i2) /. 1 by A121, 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 A119, A120, TOPREAL3:26;
then (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 A117, XBOOLE_1:8;
then L~ g2 c= L~ f by A1, A27, A118, XBOOLE_1:8;
then A123: (L~ g1) \/ (L~ g2) c= L~ f by A116, XBOOLE_1:8;
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 A124: 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
A125: ( 1 <= i & i + 1 <= len f & p in LSeg f,i ) by A124, SPPOL_2:13;

now

per cases ( ( i1 <= i & i < i2 ) or i < i1 or i2 <= i ) ;

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

then 0 <= i - i1 by XREAL_1:50;
then A127: 0 + 1 <= (i - i1) + 1 by XREAL_1:8;
i - i1 < i2 - i1 by A126, XREAL_1:11;
then (i - i1) + 1 < (i2 - i1) + 1 by XREAL_1:8;
then (i -' i1) + 1 < (i2 - i1) + 1 by A126, XREAL_1:235;
then A128: ( 1 <= (i -' i1) + 1 & (i -' i1) + 1 < (i2 -' i1) + 1 ) by A1, A126, A127, XREAL_1:235;
(((i -' i1) + 1) + i1) -' 1 = (((i -' i1) + 1) + i1) - 1 by A1, NAT_D:37
.= (i -' i1) + i1
.= i by A126, XREAL_1:237 ;
then x in LSeg (mid f,i1,i2),((i -' i1) + 1) by A1, A125, A128, Th31;
then x in L~ (mid f,i1,i2) by SPPOL_2:17;
hence x in (L~ g1) \/ (L~ g2) by A1, XBOOLE_0:def 3; :: thesis: verum

end;

case A129: i < i1 ; :: thesis: x in (L~ g1) \/ (L~ g2)

then A130: 1 < i1 by A125, XXREAL_0:2;
i1 + 1 <= i1 + i by A125, 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 A129, XREAL_1:235;
then A131: i1 -' i < (i1 -' 1) + 1 by A1, XREAL_1:235;
i + 1 <= i1 by A129, NAT_1:13;
then (i + 1) - i <= i1 - i by XREAL_1:11;
then A132: 1 <= i1 -' i by NAT_D:39;
i1 <= i1 + i by NAT_1:11;
then i1 - i <= (i1 + i) - i by XREAL_1:11;
then i1 -' i <= i1 by A129, XREAL_1:235;
then i1 -' (i1 -' i) = i1 - (i1 -' i) by XREAL_1:235
.= i1 - (i1 - i) by A129, XREAL_1:235
.= i ;
then x in LSeg (mid f,i1,1),(i1 -' i) by A3, A125, A130, A131, A132, 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 A27, XBOOLE_0:def 3;
hence x in (L~ g1) \/ (L~ g2) by A1, XBOOLE_0:def 3; :: thesis: verum

end;

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

now

per cases ( i + 1 = len f or i + 1 < len f ) by A125, 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, A3, 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 A119, A120, A122, A125, 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 A134: i + 1 <= (len f) -' 1 by A1, A3, XREAL_1:235, XXREAL_0:2;
then A135: i < (len f) -' 1 by NAT_1:13;
then A136: i2 < (len f) -' 1 by A133, XXREAL_0:2;
(i + 1) - i <= ((len f) -' 1) - i by A134, XREAL_1:11;
then A137: 1 <= ((len f) -' 1) -' i by NAT_D:39;
i2 < i + 1 by A133, 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 A133, A135, XREAL_1:235, XXREAL_0:2;
then A138: ((len f) -' 1) -' i < (((len f) -' 1) -' i2) + 1 by A135, XREAL_1:235;
((len f) -' 1) - (((len f) -' 1) -' i) = ((len f) -' 1) - (((len f) -' 1) - i) by A135, XREAL_1:235
.= i ;
then ((len f) -' 1) -' (((len f) -' 1) -' i) = i by XREAL_0:def 2;
then x in LSeg (mid f,((len f) -' 1),i2),(((len f) -' 1) -' i) by A2, A13, A125, A136, A137, A138, 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 A27, XBOOLE_1:4;
hence x in (L~ g1) \/ (L~ g2) by A1, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence x in (L~ g1) \/ (L~ g2) ; :: thesis: verum

end;

hence ( (L~ g1) /\ (L~ g2) = {(f . i1),(f . i2)} & (L~ g1) \/ (L~ g2) = L~ f ) by A28, A115, A123, XBOOLE_0:def 10; :: thesis: verum