let P0, P1, P01, P11, K0, K1, K01, K11 be Subset of (TOP-REAL 2); 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); 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); ( 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
; ( 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, Th33;
A12:
P01 = { p where p is Point of (TOP-REAL 2) : |.p.| <= 1 }
by A4, Th33;
A13:
P1 = { p where p is Point of (TOP-REAL 2) : |.p.| > 1 }
by A3, Th33;
A14:
P11 = { p where p is Point of (TOP-REAL 2) : |.p.| >= 1 }
by A5, Th33;
defpred S1[ 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 S2[ 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 H1( set ) -> set = $1;
A15:
for p being Element of (TOP-REAL 2) holds
( S1[p] iff S2[p] )
;
A16: rectangle (- 1),1,(- 1),1 =
{ H1(p) where p is Point of (TOP-REAL 2) : S1[p] }
by SPPOL_2:58
.=
{ H1(q) where q is Point of (TOP-REAL 2) : S2[q] }
from FRAENKEL:sch 3(A15)
;
defpred S3[ Point of (TOP-REAL 2)] means |.$1.| = 1;
defpred S4[ Point of (TOP-REAL 2)] means |.($1 - |[0 ,0 ]|).| = 1;
A17:
for p being Point of (TOP-REAL 2) holds
( S4[p] iff S3[p] )
by EUCLID:58, RLVECT_1:26;
P =
{ H1(p) where p is Point of (TOP-REAL 2) : S4[p] }
by A1
.=
{ H1(p2) where p2 is Point of (TOP-REAL 2) : S3[p2] }
from FRAENKEL:sch 3(A17)
;
then A18:
f .: (rectangle (- 1),1,(- 1),1) = P
by A10, A16, JGRAPH_3:33;
A19:
dom f = the carrier of (TOP-REAL 2)
by FUNCT_2:def 1;
A20:
f .: K0 = P0
by A6, A10, A11, Th34;
f .: K1 = P1
by A7, A10, A13, Th35;
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, Th22; ( f .: K01 = P01 & f .: K11 = P11 & (f " ) .: P01 = K01 & (f " ) .: P11 = K11 )
A21:
f .: K01 = P01
by A8, A10, A12, Th36;
f .: K11 = P11
by A9, A10, A14, Th37;
hence
( f .: K01 = P01 & f .: K11 = P11 & (f " ) .: P01 = K01 & (f " ) .: P11 = K11 )
by A10, A19, A21, Th22; verum