for P0, P1, P01, P11, K0, K1, K01, K11 being 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 )