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
; ( 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; 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); ( 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
; 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 ) )