let P0, P1, P01, P11, K0, K1, K01, K11 be Subset of (TOP-REAL 2); :: thesis:
let P be non empty compact Subset of (TOP-REAL 2); :: thesis:
let f be Function of (TOP-REAL 2),(TOP-REAL 2); :: thesis:
assume that
A1: P = circle (0,0,1) and
A2: P0 = inside_of_circle (0,0,1) and
A3: P1 = outside_of_circle (0,0,1) and
A4: P01 = closed_inside_of_circle (0,0,1) and
A5: P11 = closed_outside_of_circle (0,0,1) and
A6: K0 = inside_of_rectangle ((- 1),1,(- 1),1) and
A7: K1 = outside_of_rectangle ((- 1),1,(- 1),1) and
A8: K01 = closed_inside_of_rectangle ((- 1),1,(- 1),1) and
A9: K11 = closed_outside_of_rectangle ((- 1),1,(- 1),1) and
A10: f = Sq_Circ ; :: thesis:
set K = rectangle ((- 1),1,(- 1),1);
A11: P0 = { p where p is Point of (TOP-REAL 2) : |.p.| < 1 } by A2, Th24;
A12: P01 = { p where p is Point of (TOP-REAL 2) : |.p.| <= 1 } by A4, Th24;
A13: P1 = { p where p is Point of (TOP-REAL 2) : |.p.| > 1 } by A3, Th24;
A14: P11 = { p where p is Point of (TOP-REAL 2) : |.p.| >= 1 } by A5, Th24;
defpred S₁[ Point of (TOP-REAL 2)] means ( ( $1 `1 = - 1 & $1 `2 <= 1 & $1 `2 >= - 1 ) or ( $1 `1 <= 1 & $1 `1 >= - 1 & $1 `2 = 1 ) or ( $1 `1 <= 1 & $1 `1 >= - 1 & $1 `2 = - 1 ) or ( $1 `1 = 1 & $1 `2 <= 1 & $1 `2 >= - 1 ) );
defpred S₂[ Point of (TOP-REAL 2)] means ( ( - 1 = $1 `1 & - 1 <= $1 `2 & $1 `2 <= 1 ) or ( $1 `1 = 1 & - 1 <= $1 `2 & $1 `2 <= 1 ) or ( - 1 = $1 `2 & - 1 <= $1 `1 & $1 `1 <= 1 ) or ( 1 = $1 `2 & - 1 <= $1 `1 & $1 `1 <= 1 ) );
deffunc H₁( set ) -> set = $1;
A15: for p being Element of (TOP-REAL 2) holds
( S₁[p] iff S₂[p] ) ;
A16: rectangle ((- 1),1,(- 1),1) = { H₁(p) where p is Point of (TOP-REAL 2) : S₁[p] } by SPPOL_2:54
.= { H₁(q) where q is Point of (TOP-REAL 2) : S₂[q] } from FRAENKEL:sch 3(A15) ;
defpred S₃[ Point of (TOP-REAL 2)] means |.$1.| = 1;
defpred S₄[ Point of (TOP-REAL 2)] means |.($1 - |[0,0]|).| = 1;
A17: for p being Point of (TOP-REAL 2) holds
( S₄[p] iff S₃[p] ) by EUCLID:54, RLVECT_1:13;
P = { H₁(p) where p is Point of (TOP-REAL 2) : S₄[p] } by A1
.= { H₁(p2) where p2 is Point of (TOP-REAL 2) : S₃[p2] } from FRAENKEL:sch 3(A17) ;
then A18: f .: (rectangle ((- 1),1,(- 1),1)) = P by A10, A16, JGRAPH_3:23;
A19: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
A20: f .: K0 = P0 by A6, A10, A11, Th25;
f .: K1 = P1 by A7, A10, A13, Th26;
hence ( f .: (rectangle ((- 1),1,(- 1),1)) = P & (f ") .: P = rectangle ((- 1),1,(- 1),1) & f .: K0 = P0 & (f ") .: P0 = K0 & f .: K1 = P1 & (f ") .: P1 = K1 ) by A10, A18, A19, A20, FUNCT_1:107; :: thesis:
A21: f .: K01 = P01 by A8, A10, A12, Th27;
f .: K11 = P11 by A9, A10, A14, Th28;
hence ( f .: K01 = P01 & f .: K11 = P11 & (f ") .: P01 = K01 & (f ") .: P11 = K11 ) by A10, A19, A21, FUNCT_1:107; :: thesis: