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 Circle2IntervalR | ((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: Circle2IntervalR | ((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, Lm25, 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 (Circle2IntervalR | ((Topen_unit_circle c[10]) | aX1)) . a = (Af * (c * f)) . a

hence Circle2IntervalR | ((Topen_unit_circle c[10]) | aX1) is continuous by A13, A14, Lm39, 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 Circle2IntervalR | ((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: Circle2IntervalR | ((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, Th27;

A12: q `1 < 1 by A10, Th27;

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:3; :: 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, Th27;

A12: q `1 < 1 by A10, Th27;

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:3; :: thesis: verum

then reconsider f = p | B as Function of ((TOP-REAL 2) | B),(R^1 | (R^1 Q)) by A4, A6, Lm25, 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 (Circle2IntervalR | ((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: (Circle2IntervalR | ((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

A16: ( y >= 0 implies Circle2IntervalR . b = (arccos x) / (2 * PI) ) and

( y <= 0 implies Circle2IntervalR . b = 1 - ((arccos x) / (2 * PI)) ) by Def13;

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

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

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

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

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

then A20: arccos . x in rng c by A19, Lm36, 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 (Circle2IntervalR | ((Topen_unit_circle c[10]) | aX1)) . a = (arccos x) / (2 * PI) by A15, A16, EUCLID:52, FUNCT_1:49

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

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

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

.= Af . (arccos . x) by A20, Lm37, 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

A16: ( y >= 0 implies Circle2IntervalR . b = (arccos x) / (2 * PI) ) and

( y <= 0 implies Circle2IntervalR . b = 1 - ((arccos x) / (2 * PI)) ) by Def13;

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

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

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

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

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

then A20: arccos . x in rng c by A19, Lm36, 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 (Circle2IntervalR | ((Topen_unit_circle c[10]) | aX1)) . a = (arccos x) / (2 * PI) by A15, A16, EUCLID:52, FUNCT_1:49

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

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

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

.= Af . (arccos . x) by A20, Lm37, 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 Circle2IntervalR | ((Topen_unit_circle c[10]) | aX1) is continuous by A13, A14, Lm39, FUNCT_2:63; :: thesis: verum