let P0, P1, P01, P11, K0, K1, K01, K11 be Subset of (); :: thesis: for P being non empty compact Subset of ()
for f being Function of (),() 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 (); :: thesis: for f being Function of (),() 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 (),(); :: 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 () : |.p.| < 1 } by ;
A12: P01 = { p where p is Point of () : |.p.| <= 1 } by ;
A13: P1 = { p where p is Point of () : |.p.| > 1 } by ;
A14: P11 = { p where p is Point of () : |.p.| >= 1 } by ;
defpred S1[ Point of ()] 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 S2[ Point of ()] 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 H1( set ) -> set = \$1;
A15: for p being Element of () holds
( S1[p] iff S2[p] ) ;
A16: rectangle ((- 1),1,(- 1),1) = { H1(p) where p is Point of () : S1[p] } by SPPOL_2:54
.= { H1(q) where q is Point of () : S2[q] } from ;
defpred S3[ Point of ()] means |.\$1.| = 1;
defpred S4[ Point of ()] means |.(\$1 - ).| = 1;
A17: for p being Point of () holds
( S4[p] iff S3[p] ) by ;
P = { H1(p) where p is Point of () : S4[p] } by A1
.= { H1(p2) where p2 is Point of () : S3[p2] } from ;
then A18: f .: (rectangle ((- 1),1,(- 1),1)) = P by ;
A19: dom f = the carrier of () 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 ; :: 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 ; :: thesis: verum