theorem
ex
F being
Subset-Family of
(Tunit_circle 2) st
(
F = {(CircleMap .: ].0,1.[),(CircleMap .: ].(1 / 2),(3 / 2).[)} &
F is
Cover of
(Tunit_circle 2) &
F is
open & ( for
U being
Subset of
(Tunit_circle 2) holds
( (
U = CircleMap .: ].0,1.[ implies (
union (IntIntervals (0,1)) = CircleMap " U & ( for
d being
Subset of
R^1 st
d in IntIntervals (
0,1) holds
for
f being
Function of
(R^1 | d),
((Tunit_circle 2) | U) st
f = CircleMap | d holds
f is
being_homeomorphism ) ) ) & (
U = CircleMap .: ].(1 / 2),(3 / 2).[ implies (
union (IntIntervals ((1 / 2),(3 / 2))) = CircleMap " U & ( for
d being
Subset of
R^1 st
d in IntIntervals (
(1 / 2),
(3 / 2)) holds
for
f being
Function of
(R^1 | d),
((Tunit_circle 2) | U) st
f = CircleMap | d holds
f is
being_homeomorphism ) ) ) ) ) )