reconsider c1 = c[10] as Point of (TOP-REAL 2) ;

let aX1 be Subset of (Topen_unit_circle c[-10]); :: thesis: ( aX1 = { q where q is Point of (TOP-REAL 2) : ( q in the carrier of (Topen_unit_circle c[-10]) & 0 >= q `2 ) } implies Circle2IntervalL | ((Topen_unit_circle c[-10]) | aX1) is continuous )

assume A1: aX1 = { q where q is Point of (TOP-REAL 2) : ( q in the carrier of (Topen_unit_circle c[-10]) & 0 >= q `2 ) } ; :: thesis: Circle2IntervalL | ((Topen_unit_circle c[-10]) | aX1) is continuous

A2: c1 `2 = 0 by EUCLID:52;

c[10] is Point of (Topen_unit_circle c[-10]) by Lm15, Th23;

then c[10] in aX1 by A1, A2;

then reconsider aX1 = aX1 as non empty Subset of (Topen_unit_circle c[-10]) ;

set X1 = (Topen_unit_circle c[-10]) | aX1;

A3: the carrier of (Tunit_circle 2) is Subset of (TOP-REAL 2) by TSEP_1:1;

[#] ((Topen_unit_circle c[-10]) | aX1) is Subset of (Tunit_circle 2) by Lm9;

then reconsider B = [#] ((Topen_unit_circle c[-10]) | aX1) as non empty Subset of (TOP-REAL 2) by A3, XBOOLE_1:1;

set f = p | B;

A4: dom (p | B) = B by Lm40, RELAT_1:62;

A5: aX1 = the carrier of ((Topen_unit_circle c[-10]) | aX1) by PRE_TOPC:8;

A6: rng (p | B) c= Q

then reconsider f = p | B as Function of ((TOP-REAL 2) | B),(R^1 | (R^1 Q)) by A4, A6, Lm46, FUNCT_2:2;

(Topen_unit_circle c[-10]) | aX1 is SubSpace of Tunit_circle 2 by TSEP_1:7;

then (Topen_unit_circle c[-10]) | aX1 is SubSpace of TOP-REAL 2 by TSEP_1:7;

then A13: (TOP-REAL 2) | B = (Topen_unit_circle c[-10]) | aX1 by PRE_TOPC:def 5;

A14: for a being Point of ((Topen_unit_circle c[-10]) | aX1) holds (Circle2IntervalL | ((Topen_unit_circle c[-10]) | aX1)) . a = (Af * (c * f)) . a

hence Circle2IntervalL | ((Topen_unit_circle c[-10]) | aX1) is continuous by A13, A14, Lm58, FUNCT_2:63; :: thesis: verum

let aX1 be Subset of (Topen_unit_circle c[-10]); :: thesis: ( aX1 = { q where q is Point of (TOP-REAL 2) : ( q in the carrier of (Topen_unit_circle c[-10]) & 0 >= q `2 ) } implies Circle2IntervalL | ((Topen_unit_circle c[-10]) | aX1) is continuous )

assume A1: aX1 = { q where q is Point of (TOP-REAL 2) : ( q in the carrier of (Topen_unit_circle c[-10]) & 0 >= q `2 ) } ; :: thesis: Circle2IntervalL | ((Topen_unit_circle c[-10]) | aX1) is continuous

A2: c1 `2 = 0 by EUCLID:52;

c[10] is Point of (Topen_unit_circle c[-10]) by Lm15, Th23;

then c[10] in aX1 by A1, A2;

then reconsider aX1 = aX1 as non empty Subset of (Topen_unit_circle c[-10]) ;

set X1 = (Topen_unit_circle c[-10]) | aX1;

A3: the carrier of (Tunit_circle 2) is Subset of (TOP-REAL 2) by TSEP_1:1;

[#] ((Topen_unit_circle c[-10]) | aX1) is Subset of (Tunit_circle 2) by Lm9;

then reconsider B = [#] ((Topen_unit_circle c[-10]) | aX1) as non empty Subset of (TOP-REAL 2) by A3, XBOOLE_1:1;

set f = p | B;

A4: dom (p | B) = B by Lm40, RELAT_1:62;

A5: aX1 = the carrier of ((Topen_unit_circle c[-10]) | aX1) by PRE_TOPC:8;

A6: rng (p | B) c= Q

proof

the carrier of ((TOP-REAL 2) | B) = B
by PRE_TOPC:8;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (p | B) or y in Q )

assume y in rng (p | B) ; :: thesis: y in Q

then consider x being object such that

A7: x in dom (p | B) and

A8: (p | B) . x = y by FUNCT_1:def 3;

consider q being Point of (TOP-REAL 2) such that

A9: q = x and

A10: q in the carrier of (Topen_unit_circle c[-10]) and

0 >= q `2 by A1, A5, A4, A7;

A11: - 1 < q `1 by A10, Th28;

A12: q `1 <= 1 by A10, Th28;

y = p . x by A4, A7, A8, FUNCT_1:49

.= q `1 by A9, PSCOMP_1:def 5 ;

hence y in Q by A11, A12, XXREAL_1:2; :: thesis: verum

end;assume y in rng (p | B) ; :: thesis: y in Q

then consider x being object such that

A7: x in dom (p | B) and

A8: (p | B) . x = y by FUNCT_1:def 3;

consider q being Point of (TOP-REAL 2) such that

A9: q = x and

A10: q in the carrier of (Topen_unit_circle c[-10]) and

0 >= q `2 by A1, A5, A4, A7;

A11: - 1 < q `1 by A10, Th28;

A12: q `1 <= 1 by A10, Th28;

y = p . x by A4, A7, A8, FUNCT_1:49

.= q `1 by A9, PSCOMP_1:def 5 ;

hence y in Q by A11, A12, XXREAL_1:2; :: thesis: verum

then reconsider f = p | B as Function of ((TOP-REAL 2) | B),(R^1 | (R^1 Q)) by A4, A6, Lm46, FUNCT_2:2;

(Topen_unit_circle c[-10]) | aX1 is SubSpace of Tunit_circle 2 by TSEP_1:7;

then (Topen_unit_circle c[-10]) | aX1 is SubSpace of TOP-REAL 2 by TSEP_1:7;

then A13: (TOP-REAL 2) | B = (Topen_unit_circle c[-10]) | aX1 by PRE_TOPC:def 5;

A14: for a being Point of ((Topen_unit_circle c[-10]) | aX1) holds (Circle2IntervalL | ((Topen_unit_circle c[-10]) | aX1)) . a = (Af * (c * f)) . a

proof

f is continuous
by Lm41, TOPREALA:8;
let a be Point of ((Topen_unit_circle c[-10]) | aX1); :: thesis: (Circle2IntervalL | ((Topen_unit_circle c[-10]) | aX1)) . a = (Af * (c * f)) . a

reconsider b = a as Point of (Topen_unit_circle c[-10]) by PRE_TOPC:25;

consider x, y being Real such that

A15: b = |[x,y]| and

( y >= 0 implies Circle2IntervalL . b = 1 + ((arccos x) / (2 * PI)) ) and

A16: ( y <= 0 implies Circle2IntervalL . b = 1 - ((arccos x) / (2 * PI)) ) by Def14;

A17: |[x,y]| `1 <= 1 by A15, Th28;

A18: |[x,y]| `1 = x by EUCLID:52;

- 1 < |[x,y]| `1 by A15, Th28;

then A19: x in Q by A18, A17, XXREAL_1:2;

then arccos . x = c . x by FUNCT_1:49;

then A20: arccos . x in rng c by A19, Lm55, FUNCT_1:def 3;

a in aX1 by A5;

then ex q being Point of (TOP-REAL 2) st

( a = q & q in the carrier of (Topen_unit_circle c[-10]) & 0 >= q `2 ) by A1;

hence (Circle2IntervalL | ((Topen_unit_circle c[-10]) | aX1)) . a = 1 - ((arccos x) / (2 * PI)) by A15, A16, EUCLID:52, FUNCT_1:49

.= 1 - ((arccos . x) / (2 * PI)) by SIN_COS6:def 4

.= 1 - ((1 / (2 * PI)) * (arccos . x)) by XCMPLX_1:99

.= ((- (1 / (2 * PI))) * (arccos . x)) + 1

.= (AffineMap ((- (1 / (2 * PI))),1)) . (arccos . x) by FCONT_1:def 4

.= Af . (arccos . x) by A20, Lm56, FUNCT_1:49

.= Af . (c . x) by A19, FUNCT_1:49

.= Af . (c . (|[x,y]| `1)) by EUCLID:52

.= Af . (c . (p . a)) by A15, PSCOMP_1:def 5

.= Af . (c . (f . a)) by FUNCT_1:49

.= Af . ((c * f) . a) by A13, FUNCT_2:15

.= (Af * (c * f)) . a by A13, FUNCT_2:15 ;

:: thesis: verum

end;reconsider b = a as Point of (Topen_unit_circle c[-10]) by PRE_TOPC:25;

consider x, y being Real such that

A15: b = |[x,y]| and

( y >= 0 implies Circle2IntervalL . b = 1 + ((arccos x) / (2 * PI)) ) and

A16: ( y <= 0 implies Circle2IntervalL . b = 1 - ((arccos x) / (2 * PI)) ) by Def14;

A17: |[x,y]| `1 <= 1 by A15, Th28;

A18: |[x,y]| `1 = x by EUCLID:52;

- 1 < |[x,y]| `1 by A15, Th28;

then A19: x in Q by A18, A17, XXREAL_1:2;

then arccos . x = c . x by FUNCT_1:49;

then A20: arccos . x in rng c by A19, Lm55, FUNCT_1:def 3;

a in aX1 by A5;

then ex q being Point of (TOP-REAL 2) st

( a = q & q in the carrier of (Topen_unit_circle c[-10]) & 0 >= q `2 ) by A1;

hence (Circle2IntervalL | ((Topen_unit_circle c[-10]) | aX1)) . a = 1 - ((arccos x) / (2 * PI)) by A15, A16, EUCLID:52, FUNCT_1:49

.= 1 - ((arccos . x) / (2 * PI)) by SIN_COS6:def 4

.= 1 - ((1 / (2 * PI)) * (arccos . x)) by XCMPLX_1:99

.= ((- (1 / (2 * PI))) * (arccos . x)) + 1

.= (AffineMap ((- (1 / (2 * PI))),1)) . (arccos . x) by FCONT_1:def 4

.= Af . (arccos . x) by A20, Lm56, FUNCT_1:49

.= Af . (c . x) by A19, FUNCT_1:49

.= Af . (c . (|[x,y]| `1)) by EUCLID:52

.= Af . (c . (p . a)) by A15, PSCOMP_1:def 5

.= Af . (c . (f . a)) by FUNCT_1:49

.= Af . ((c * f) . a) by A13, FUNCT_2:15

.= (Af * (c * f)) . a by A13, FUNCT_2:15 ;

:: thesis: verum

hence Circle2IntervalL | ((Topen_unit_circle c[-10]) | aX1) is continuous by A13, A14, Lm58, FUNCT_2:63; :: thesis: verum