let f be rectangular special_circular_sequence; :: thesis: ( LeftComp f = { p where p is Point of (TOP-REAL 2) : ( not W-bound (L~ f) <= p `1 or not p `1 <= E-bound (L~ f) or not S-bound (L~ f) <= p `2 or not p `2 <= N-bound (L~ f) ) } & RightComp f = { q where q is Point of (TOP-REAL 2) : ( W-bound (L~ f) < q `1 & q `1 < E-bound (L~ f) & S-bound (L~ f) < q `2 & q `2 < N-bound (L~ f) ) } )
defpred S1[ Element of (TOP-REAL 2)] means ( not W-bound (L~ f) <= $1 `1 or not $1 `1 <= E-bound (L~ f) or not S-bound (L~ f) <= $1 `2 or not $1 `2 <= N-bound (L~ f) );
defpred S2[ Element of (TOP-REAL 2)] means ( W-bound (L~ f) < $1 `1 & $1 `1 < E-bound (L~ f) & S-bound (L~ f) < $1 `2 & $1 `2 < N-bound (L~ f) );
defpred S3[ Element of (TOP-REAL 2)] means ( ( $1 `1 = W-bound (L~ f) & $1 `2 <= N-bound (L~ f) & $1 `2 >= S-bound (L~ f) ) or ( $1 `1 <= E-bound (L~ f) & $1 `1 >= W-bound (L~ f) & $1 `2 = N-bound (L~ f) ) or ( $1 `1 <= E-bound (L~ f) & $1 `1 >= W-bound (L~ f) & $1 `2 = S-bound (L~ f) ) or ( $1 `1 = E-bound (L~ f) & $1 `2 <= N-bound (L~ f) & $1 `2 >= S-bound (L~ f) ) );
set LC = { p where p is Point of (TOP-REAL 2) : S1[p] } ;
set RC = { q where q is Point of (TOP-REAL 2) : S2[q] } ;
set Lf = { p where p is Point of (TOP-REAL 2) : S3[p] } ;
A1: S-bound (L~ f) < N-bound (L~ f) by SPRECT_1:32;
A2: { p where p is Point of (TOP-REAL 2) : S3[p] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch 7();
 A3: { q where q is Point of (TOP-REAL 2) : S2[q] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch 7();
 A4: L~ f = { p where p is Point of (TOP-REAL 2) : S3[p] } by Th35;
{ p where p is Point of (TOP-REAL 2) : S1[p] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch 7();
 then reconsider Lc9 = { p where p is Point of (TOP-REAL 2) : S1[p] } , Rc9 = { q where q is Point of (TOP-REAL 2) : S2[q] } , Lf = { p where p is Point of (TOP-REAL 2) : S3[p] } as Subset of (TOP-REAL 2) by A3, A2;
reconsider Lf = Lf as Subset of (TOP-REAL 2) ;
reconsider Lc9 = Lc9, Rc9 = Rc9 as Subset of (TOP-REAL 2) ;
A5: W-bound (L~ f) < E-bound (L~ f) by SPRECT_1:31;
then reconsider Lc = Lc9, Rc = Rc9 as Subset of ((TOP-REAL 2) | (Lf `)) by A1, JORDAN1:39, JORDAN1:41;
reconsider Lc = Lc, Rc = Rc as Subset of ((TOP-REAL 2) | (Lf `)) ;
A6: ((1 / 2) * (S-bound (L~ f))) + ((1 / 2) * (S-bound (L~ f))) = S-bound (L~ f) ;
Rc = Rc9 ;
then Lc is a_component by A5, A1, JORDAN1:36;
then A7: Lc9 is_a_component_of Lf ` by CONNSP_1:def 6;
set p = ((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) + |[0,1]|;
set q = (1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))));
A8: 1 + 1 <= len f by GOBOARD7:34, XXREAL_0:2;
A9: (((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) + |[0,1]|) `2 = (((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) `2) + (|[0,1]| `2) by TOPREAL3:2
.= (((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) `2) + 1 by EUCLID:52 ;
A10: GoB f = ((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2)) by Th36;
then A11: 1 + 1 = width (GoB f) by MATRIX_0:47;
then ((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) `2 = ((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + (f /. 2))) `2 by A10, MATRIX_0:50
.= ((1 / 2) * ((f /. 1) + (f /. 2))) `2 by A10, A11, MATRIX_0:50
.= (1 / 2) * (((f /. 1) + (f /. 2)) `2) by TOPREAL3:4
.= (1 / 2) * (((f /. 1) `2) + ((f /. 2) `2)) by TOPREAL3:2
.= (1 / 2) * (((N-min (L~ f)) `2) + ((f /. 2) `2)) by SPRECT_1:83
.= (1 / 2) * (((N-min (L~ f)) `2) + ((N-max (L~ f)) `2)) by SPRECT_1:84
.= (1 / 2) * ((N-bound (L~ f)) + ((N-max (L~ f)) `2)) by EUCLID:52
.= (1 / 2) * ((N-bound (L~ f)) + (N-bound (L~ f))) by EUCLID:52
.= N-bound (L~ f) ;
then (((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) + |[0,1]|) `2 > 0 + (N-bound (L~ f)) by A9, XREAL_1:8;
then A12: ((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) + |[0,1]| in { p where p is Point of (TOP-REAL 2) : S1[p] } ;
A13: 1 + 1 = len (GoB f) by A10, MATRIX_0:47;
then A14: ((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) + |[0,1]| in Int (cell ((GoB f),1,(1 + 1))) by A11, GOBOARD6:32;
A15: f /. (1 + 1) = (GoB f) * ((1 + 1),(1 + 1)) by A10, MATRIX_0:50;
1 < width (GoB f) by GOBOARD7:33;
then A16: 1 + 1 <= width (GoB f) by NAT_1:13;
then A17: [(1 + 1),(1 + 1)] in Indices (GoB f) by A13, MATRIX_0:30;
1 <= len (GoB f) by GOBOARD7:32;
then A18: [1,(1 + 1)] in Indices (GoB f) by A16, MATRIX_0:30;
A19: f /. 1 = (GoB f) * (1,(1 + 1)) by A10, MATRIX_0:50;
then right_cell (f,1) = cell ((GoB f),1,1) by A8, A18, A17, A15, GOBOARD5:28;
then A20: Int (cell ((GoB f),1,1)) c= RightComp f by GOBOARD9:def 2;
left_cell (f,1) = cell ((GoB f),1,(1 + 1)) by A8, A18, A19, A17, A15, GOBOARD5:28;
then Int (cell ((GoB f),1,(1 + 1))) c= LeftComp f by GOBOARD9:def 1;
then A21: { p where p is Point of (TOP-REAL 2) : S1[p] } meets LeftComp f by A14, A12, XBOOLE_0:3;
A22: (f /. 2) `1 = (E-max (L~ f)) `1 by SPRECT_1:84
.= E-bound (L~ f) by EUCLID:52 ;
set p = (1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2)));
A23: (1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2))) in Int (cell ((GoB f),1,1)) by A13, A11, GOBOARD6:31;
A24: (1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2))) = (1 / 2) * (((GoB f) * (1,1)) + (f /. 2)) by A10, MATRIX_0:50
.= (1 / 2) * ((f /. 4) + (f /. 2)) by A10, MATRIX_0:50 ;
then A25: ((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2)))) `1 = (1 / 2) * (((f /. 4) + (f /. 2)) `1) by TOPREAL3:4
.= (1 / 2) * (((f /. 4) `1) + ((f /. 2) `1)) by TOPREAL3:2
.= ((1 / 2) * ((f /. 4) `1)) + ((1 / 2) * ((f /. 2) `1)) ;
LeftComp f is_a_component_of (L~ f) ` by GOBOARD9:def 1;
hence LeftComp f = { p where p is Point of (TOP-REAL 2) : S1[p] } by A4, A7, A21, GOBOARD9:1; :: thesis: RightComp f = { q where q is Point of (TOP-REAL 2) : ( W-bound (L~ f) < q `1 & q `1 < E-bound (L~ f) & S-bound (L~ f) < q `2 & q `2 < N-bound (L~ f) ) }
A26: ((1 / 2) * (W-bound (L~ f))) + ((1 / 2) * (W-bound (L~ f))) = W-bound (L~ f) ;
A27: ((1 / 2) * (E-bound (L~ f))) + ((1 / 2) * (E-bound (L~ f))) = E-bound (L~ f) ;
A28: ((1 / 2) * (N-bound (L~ f))) + ((1 / 2) * (N-bound (L~ f))) = N-bound (L~ f) ;
A29: (f /. 4) `1 = (W-min (L~ f)) `1 by SPRECT_1:86
.= W-bound (L~ f) by EUCLID:52 ;
then (1 / 2) * ((f /. 4) `1) < (1 / 2) * (E-bound (L~ f)) by SPRECT_1:31, XREAL_1:68;
then A30: ((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2)))) `1 < E-bound (L~ f) by A27, A25, A22, XREAL_1:6;
A31: ((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2)))) `2 = (1 / 2) * (((f /. 4) + (f /. 2)) `2) by A24, TOPREAL3:4
.= (1 / 2) * (((f /. 4) `2) + ((f /. 2) `2)) by TOPREAL3:2
.= ((1 / 2) * ((f /. 4) `2)) + ((1 / 2) * ((f /. 2) `2)) ;
Lc = Lc9 ;
then Rc is a_component by A5, A1, JORDAN1:36;
then A32: Rc9 is_a_component_of Lf ` by CONNSP_1:def 6;
A33: (f /. 2) `2 = (N-max (L~ f)) `2 by SPRECT_1:84
.= N-bound (L~ f) by EUCLID:52 ;
A34: (f /. 4) `2 = (S-min (L~ f)) `2 by SPRECT_1:86
.= S-bound (L~ f) by EUCLID:52 ;
then (1 / 2) * ((f /. 4) `2) < (1 / 2) * (N-bound (L~ f)) by SPRECT_1:32, XREAL_1:68;
then A35: ((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2)))) `2 < N-bound (L~ f) by A28, A31, A33, XREAL_1:6;
(1 / 2) * ((f /. 2) `2) > (1 / 2) * (S-bound (L~ f)) by A33, SPRECT_1:32, XREAL_1:68;
then A36: S-bound (L~ f) < ((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2)))) `2 by A6, A31, A34, XREAL_1:6;
(1 / 2) * ((f /. 2) `1) > (1 / 2) * (W-bound (L~ f)) by A22, SPRECT_1:31, XREAL_1:68;
then W-bound (L~ f) < ((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2)))) `1 by A26, A25, A29, XREAL_1:6;
then (1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2))) in { q where q is Point of (TOP-REAL 2) : S2[q] } by A30, A36, A35;
then A37: { q where q is Point of (TOP-REAL 2) : S2[q] } meets RightComp f by A23, A20, XBOOLE_0:3;
RightComp f is_a_component_of (L~ f) ` by GOBOARD9:def 2;
hence RightComp f = { q where q is Point of (TOP-REAL 2) : ( W-bound (L~ f) < q `1 & q `1 < E-bound (L~ f) & S-bound (L~ f) < q `2 & q `2 < N-bound (L~ f) ) } by A4, A32, A37, GOBOARD9:1; :: thesis: verum