consider F being Subset-Family of (Tunit_circle 2) such that

A1: F = {(CircleMap .: ].0,1.[),(CircleMap .: ].(1 / 2),(3 / 2).[)} and

A2: ( F is Cover of (Tunit_circle 2) & F is open ) and

A3: 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 ) ) ) ) by TOPREALB:45;

take F ; :: thesis: ( F is Cover of (Tunit_circle 2) & F is open & ( for U being Subset of (Tunit_circle 2) st U in F holds

ex D being mutually-disjoint open Subset-Family of R^1 st

( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds

for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds

f is being_homeomorphism ) ) ) )

thus ( F is Cover of (Tunit_circle 2) & F is open ) by A2; :: thesis: for U being Subset of (Tunit_circle 2) st U in F holds

ex D being mutually-disjoint open Subset-Family of R^1 st

( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds

for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds

f is being_homeomorphism ) )

let U be Subset of (Tunit_circle 2); :: thesis: ( U in F implies ex D being mutually-disjoint open Subset-Family of R^1 st

( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds

for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds

f is being_homeomorphism ) ) )

assume A4: U in F ; :: thesis: ex D being mutually-disjoint open Subset-Family of R^1 st

( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds

for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds

f is being_homeomorphism ) )

A1: F = {(CircleMap .: ].0,1.[),(CircleMap .: ].(1 / 2),(3 / 2).[)} and

A2: ( F is Cover of (Tunit_circle 2) & F is open ) and

A3: 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 ) ) ) ) by TOPREALB:45;

take F ; :: thesis: ( F is Cover of (Tunit_circle 2) & F is open & ( for U being Subset of (Tunit_circle 2) st U in F holds

ex D being mutually-disjoint open Subset-Family of R^1 st

( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds

for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds

f is being_homeomorphism ) ) ) )

thus ( F is Cover of (Tunit_circle 2) & F is open ) by A2; :: thesis: for U being Subset of (Tunit_circle 2) st U in F holds

ex D being mutually-disjoint open Subset-Family of R^1 st

( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds

for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds

f is being_homeomorphism ) )

let U be Subset of (Tunit_circle 2); :: thesis: ( U in F implies ex D being mutually-disjoint open Subset-Family of R^1 st

( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds

for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds

f is being_homeomorphism ) ) )

assume A4: U in F ; :: thesis: ex D being mutually-disjoint open Subset-Family of R^1 st

( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds

for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds

f is being_homeomorphism ) )

per cases
( U = CircleMap .: ].0,1.[ or U = CircleMap .: ].(1 / 2),(3 / 2).[ )
by A1, A4, TARSKI:def 2;

end;

suppose A5:
U = CircleMap .: ].0,1.[
; :: thesis: ex D being mutually-disjoint open Subset-Family of R^1 st

( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds

for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds

f is being_homeomorphism ) )

( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds

for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds

f is being_homeomorphism ) )

reconsider D = IntIntervals (0,1) as mutually-disjoint open Subset-Family of R^1 by Lm8, TOPREALB:4;

take D ; :: thesis: ( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds

for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds

f is being_homeomorphism ) )

thus ( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds

for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds

f is being_homeomorphism ) ) by A3, A5; :: thesis: verum

end;take D ; :: thesis: ( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds

for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds

f is being_homeomorphism ) )

thus ( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds

for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds

f is being_homeomorphism ) ) by A3, A5; :: thesis: verum

suppose A6:
U = CircleMap .: ].(1 / 2),(3 / 2).[
; :: thesis: ex D being mutually-disjoint open Subset-Family of R^1 st

( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds

for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds

f is being_homeomorphism ) )

( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds

for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds

f is being_homeomorphism ) )

reconsider D = IntIntervals ((1 / 2),(3 / 2)) as mutually-disjoint open Subset-Family of R^1 by Lm9, TOPREALB:4;

take D ; :: thesis: ( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds

for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds

f is being_homeomorphism ) )

thus ( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds

for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds

f is being_homeomorphism ) ) by A3, A6; :: thesis: verum

end;take D ; :: thesis: ( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds

for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds

f is being_homeomorphism ) )

thus ( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds

for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds

f is being_homeomorphism ) ) by A3, A6; :: thesis: verum