let P0, P1, P01, P11, K0, K1, K01, K11 be Subset of (TOP-REAL 2); :: thesis: for P being non empty compact Subset of (TOP-REAL 2)

for f being Function of (TOP-REAL 2),(TOP-REAL 2) st P = circle (0,0,1) & P0 = inside_of_circle (0,0,1) & P1 = outside_of_circle (0,0,1) & P01 = closed_inside_of_circle (0,0,1) & P11 = closed_outside_of_circle (0,0,1) & K0 = inside_of_rectangle ((- 1),1,(- 1),1) & K1 = outside_of_rectangle ((- 1),1,(- 1),1) & K01 = closed_inside_of_rectangle ((- 1),1,(- 1),1) & K11 = closed_outside_of_rectangle ((- 1),1,(- 1),1) & f = Sq_Circ holds

( 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 & f .: K01 = P01 & f .: K11 = P11 & (f ") .: P01 = K01 & (f ") .: P11 = K11 )

let P be non empty compact Subset of (TOP-REAL 2); :: thesis: for f being Function of (TOP-REAL 2),(TOP-REAL 2) st P = circle (0,0,1) & P0 = inside_of_circle (0,0,1) & P1 = outside_of_circle (0,0,1) & P01 = closed_inside_of_circle (0,0,1) & P11 = closed_outside_of_circle (0,0,1) & K0 = inside_of_rectangle ((- 1),1,(- 1),1) & K1 = outside_of_rectangle ((- 1),1,(- 1),1) & K01 = closed_inside_of_rectangle ((- 1),1,(- 1),1) & K11 = closed_outside_of_rectangle ((- 1),1,(- 1),1) & f = Sq_Circ holds

( 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 & f .: K01 = P01 & f .: K11 = P11 & (f ") .: P01 = K01 & (f ") .: P11 = K11 )

let f be Function of (TOP-REAL 2),(TOP-REAL 2); :: thesis: ( P = circle (0,0,1) & P0 = inside_of_circle (0,0,1) & P1 = outside_of_circle (0,0,1) & P01 = closed_inside_of_circle (0,0,1) & P11 = closed_outside_of_circle (0,0,1) & K0 = inside_of_rectangle ((- 1),1,(- 1),1) & K1 = outside_of_rectangle ((- 1),1,(- 1),1) & K01 = closed_inside_of_rectangle ((- 1),1,(- 1),1) & K11 = closed_outside_of_rectangle ((- 1),1,(- 1),1) & f = Sq_Circ implies ( 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 & f .: K01 = P01 & f .: K11 = P11 & (f ") .: P01 = K01 & (f ") .: P11 = K11 ) )

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: ( 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 & f .: K01 = P01 & f .: K11 = P11 & (f ") .: P01 = K01 & (f ") .: P11 = K11 )

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_{1}[ 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_{2}[ 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_{1}( set ) -> set = $1;

A15: for p being Element of (TOP-REAL 2) holds

( S_{1}[p] iff S_{2}[p] )
;

A16: rectangle ((- 1),1,(- 1),1) = { H_{1}(p) where p is Point of (TOP-REAL 2) : S_{1}[p] }
by SPPOL_2:54

.= { H_{1}(q) where q is Point of (TOP-REAL 2) : S_{2}[q] }
from FRAENKEL:sch 3(A15)
;

defpred S_{3}[ Point of (TOP-REAL 2)] means |.$1.| = 1;

defpred S_{4}[ Point of (TOP-REAL 2)] means |.($1 - |[0,0]|).| = 1;

A17: for p being Point of (TOP-REAL 2) holds

( S_{4}[p] iff S_{3}[p] )
by EUCLID:54, RLVECT_1:13;

P = { H_{1}(p) where p is Point of (TOP-REAL 2) : S_{4}[p] }
by A1

.= { H_{1}(p2) where p2 is Point of (TOP-REAL 2) : S_{3}[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: ( f .: K01 = P01 & f .: K11 = P11 & (f ") .: P01 = K01 & (f ") .: P11 = K11 )

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

for f being Function of (TOP-REAL 2),(TOP-REAL 2) st P = circle (0,0,1) & P0 = inside_of_circle (0,0,1) & P1 = outside_of_circle (0,0,1) & P01 = closed_inside_of_circle (0,0,1) & P11 = closed_outside_of_circle (0,0,1) & K0 = inside_of_rectangle ((- 1),1,(- 1),1) & K1 = outside_of_rectangle ((- 1),1,(- 1),1) & K01 = closed_inside_of_rectangle ((- 1),1,(- 1),1) & K11 = closed_outside_of_rectangle ((- 1),1,(- 1),1) & f = Sq_Circ holds

( 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 & f .: K01 = P01 & f .: K11 = P11 & (f ") .: P01 = K01 & (f ") .: P11 = K11 )

let P be non empty compact Subset of (TOP-REAL 2); :: thesis: for f being Function of (TOP-REAL 2),(TOP-REAL 2) st P = circle (0,0,1) & P0 = inside_of_circle (0,0,1) & P1 = outside_of_circle (0,0,1) & P01 = closed_inside_of_circle (0,0,1) & P11 = closed_outside_of_circle (0,0,1) & K0 = inside_of_rectangle ((- 1),1,(- 1),1) & K1 = outside_of_rectangle ((- 1),1,(- 1),1) & K01 = closed_inside_of_rectangle ((- 1),1,(- 1),1) & K11 = closed_outside_of_rectangle ((- 1),1,(- 1),1) & f = Sq_Circ holds

( 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 & f .: K01 = P01 & f .: K11 = P11 & (f ") .: P01 = K01 & (f ") .: P11 = K11 )

let f be Function of (TOP-REAL 2),(TOP-REAL 2); :: thesis: ( P = circle (0,0,1) & P0 = inside_of_circle (0,0,1) & P1 = outside_of_circle (0,0,1) & P01 = closed_inside_of_circle (0,0,1) & P11 = closed_outside_of_circle (0,0,1) & K0 = inside_of_rectangle ((- 1),1,(- 1),1) & K1 = outside_of_rectangle ((- 1),1,(- 1),1) & K01 = closed_inside_of_rectangle ((- 1),1,(- 1),1) & K11 = closed_outside_of_rectangle ((- 1),1,(- 1),1) & f = Sq_Circ implies ( 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 & f .: K01 = P01 & f .: K11 = P11 & (f ") .: P01 = K01 & (f ") .: P11 = K11 ) )

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: ( 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 & f .: K01 = P01 & f .: K11 = P11 & (f ") .: P01 = K01 & (f ") .: P11 = K11 )

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

defpred S

deffunc H

A15: for p being Element of (TOP-REAL 2) holds

( S

A16: rectangle ((- 1),1,(- 1),1) = { H

.= { H

defpred S

defpred S

A17: for p being Point of (TOP-REAL 2) holds

( S

P = { H

.= { H

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: ( f .: K01 = P01 & f .: K11 = P11 & (f ") .: P01 = K01 & (f ") .: P11 = K11 )

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