:: The Fundamental Group of the Circle :: by Artur Korni{\l}owicz :: :: Received February 22, 2005 :: Copyright (c) 2005-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, EUCLID, CARD_1, STRUCT_0, BORSUK_1, TOPMETR, TARSKI, ZFMISC_1, PRE_TOPC, SUBSET_1, RELAT_1, ARYTM_1, XXREAL_0, ARYTM_3, GR_CY_1, FINSET_1, ORDINAL1, METRIC_1, XXREAL_1, XBOOLE_0, REAL_1, RLVECT_3, PBOOLE, FUNCT_1, CARD_3, RELAT_2, PCOMPS_1, FRECHET, CONNSP_1, CONNSP_3, RCOMP_1, CONNSP_2, TOPS_1, TOPS_2, ORDINAL2, T_0TOPSP, CANTOR_1, SETFAM_1, GRAPH_1, BORSUK_6, TOPREALB, SUPINF_2, SIN_COS, COMPLEX1, SQUARE_1, MCART_1, INT_1, ALGSTR_1, TAXONOM2, TEX_2, RCOMP_3, FINSEQ_1, FUNCT_4, COMPTS_1, FUNCOP_1, BORSUK_2, TOPALG_1, EQREL_1, WAYBEL20, TOPALG_2, GROUP_6, ALGSTR_0, JGRAPH_2, FUNCT_2, WELLORD1, TOPREAL2, TOPALG_5, MSSUBFAM, MEASURE5, NAT_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, ORDINAL1, RELAT_1, EQREL_1, FUNCT_1, PBOOLE, CARD_3, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FINSET_1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, SQUARE_1, INT_1, NAT_1, SEQM_3, FINSEQ_1, FUNCT_4, RCOMP_1, DOMAIN_1, STRUCT_0, ALGSTR_0, PRE_TOPC, TOPS_1, GR_CY_1, GROUP_6, METRIC_1, CANTOR_1, YELLOW_8, BORSUK_1, TOPS_2, COMPTS_1, CONNSP_1, CONNSP_2, CONNSP_3, TEX_2, TSEP_1, TOPMETR, EUCLID, PCOMPS_1, FRECHET, BORSUK_2, SIN_COS, BORSUK_3, FCONT_1, TAXONOM2, BORSUK_6, TOPALG_1, TOPREAL9, TOPALG_2, TOPREALB, RCOMP_3, XXREAL_0; constructors SQUARE_1, BINARITH, SIN_COS, TOPS_1, CONNSP_1, FUNCOP_1, COMPTS_1, GRCAT_1, TSEP_1, TEX_2, CANTOR_1, MONOID_0, CONNSP_3, YELLOW_8, TAXONOM2, BORSUK_3, FCONT_1, TOPALG_1, TOPREAL9, TOPREALB, RCOMP_3, BORSUK_6, SEQ_4, FRECHET, GROUP_6, FUNCT_4, REAL_1, BINOP_2; registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, NUMBERS, XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, STRUCT_0, PRE_TOPC, TOPS_1, COMPTS_1, METRIC_1, BORSUK_1, TSEP_1, GR_CY_1, MONOID_0, EUCLID, TOPMETR, BORSUK_2, YELLOW13, TOPALG_1, TOPALG_2, TOPALG_3, TOPREALB, RCOMP_3, VALUED_0, XXREAL_2, FRECHET, CONNSP_1, GROUP_6, SQUARE_1, SIN_COS, ORDINAL1; requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL; definitions FUNCT_1, FUNCT_2, GROUP_6, TOPS_2, TSEP_1, BORSUK_2, TARSKI, XBOOLE_0, CONNSP_1, T_0TOPSP, CONNSP_2, RCOMP_3, SETFAM_1; equalities COMPTS_1, BINOP_1, GR_CY_1, STRUCT_0, BORSUK_1, ALGSTR_0, TOPALG_1; expansions FUNCT_1, FUNCT_2, GROUP_6, TOPS_2, TSEP_1, BORSUK_2, COMPTS_1, TARSKI, XBOOLE_0, CONNSP_1, CONNSP_2; theorems GROUP_6, PRE_TOPC, XREAL_0, FUNCT_2, BORSUK_1, INT_1, SIN_COS, EUCLID, JGRAPH_1, SQUARE_1, TOPREAL9, TOPALG_1, TOPS_2, BORSUK_3, FUNCT_1, TOPMETR, JGRAPH_2, BORSUK_4, RELAT_1, FUNCOP_1, FCONT_1, BORSUK_6, BORSUK_2, TOPALG_2, BINOP_1, TARSKI, ZFMISC_1, FUNCT_4, TSEP_1, XBOOLE_1, COMPLEX2, SETFAM_1, XBOOLE_0, TAXONOM2, FINSEQ_3, NAT_1, SEQM_3, FINSEQ_5, TEX_2, DOMAIN_1, TOPS_1, GOBOARD9, CONNSP_1, TOPALG_3, TOPREALA, TOPREALB, FINSET_1, TOPS_3, CONNSP_3, CONNSP_2, TOPGRP_1, XREAL_1, CANTOR_1, FRECHET, TOPGEN_2, CARD_3, RCOMP_3, XXREAL_0, CARD_1, XXREAL_1, RLVECT_1, JORDAN16, XTUPLE_0; schemes FUNCT_2, NAT_1, PBOOLE, BINOP_1; begin :: Preliminaries set o = |[0,0]|; set I = the carrier of I[01]; set R = the carrier of R^1; Lm1: 0 in INT by INT_1:def 1; Lm2: 0 in I by BORSUK_1:43; then Lm3: {0} c= I by ZFMISC_1:31; Lm4: 0 in {0} by TARSKI:def 1; Lm5: the carrier of [:I[01],I[01]:] = [:I,I:] by BORSUK_1:def 2; reconsider j0 = 0, j1 = 1 as Point of I[01] by BORSUK_1:def 14,def 15; Lm6: [#]I[01] = I; Lm7: I[01] | [#]I[01] = I[01] by TSEP_1:3; Lm8: 1-0 <= 1; Lm9: 3/2-1/2 <= 1; registration cluster INT.Group -> infinite; coherence; end; reserve a, r, s for Real; theorem Th1: r <= s implies for p being Point of Closed-Interval-MSpace(r,s) holds Ball(p,a) = [.r,s.] or Ball(p,a) = [.r,p+a.[ or Ball(p,a) = ].p-a,s.] or Ball(p,a) = ].p-a,p+a.[ proof set M = Closed-Interval-MSpace(r,s); assume r <= s; then A1: the carrier of M = [.r,s.] by TOPMETR:10; let p be Point of M; set B = Ball(p,a); reconsider p1 = p as Point of RealSpace by TOPMETR:8; set B1 = Ball(p1,a); A2: B = B1 /\ the carrier of M by TOPMETR:9; A3: B1 = ].p1-a, p1+a.[ by FRECHET:7; per cases; suppose that A4: p1+a <= s and A5: p1-a < r; B = [.r,p1+a.[ proof thus B c= [.r,p1+a.[ proof let b be object; assume A6: b in B; then reconsider b as Element of B; b in B1 by A2,A6,XBOOLE_0:def 4; then A7: b < p1+a by A3,XXREAL_1:4; r <= b by A1,A6,XXREAL_1:1; hence thesis by A7,XXREAL_1:3; end; let b be object; assume A8: b in [.r,p1+a.[; then reconsider b as Real; A9: r <= b by A8,XXREAL_1:3; A10: b < p1+a by A8,XXREAL_1:3; then b <= s by A4,XXREAL_0:2; then A11: b in [.r,s.] by A9,XXREAL_1:1; p1-a < b by A5,A9,XXREAL_0:2; then b in B1 by A3,A10,XXREAL_1:4; hence thesis by A1,A2,A11,XBOOLE_0:def 4; end; hence thesis; end; suppose that A12: p1+a <= s and A13: p1-a >= r; B = ].p1-a,p1+a.[ proof thus B c= ].p1-a,p1+a.[ by A2,A3,XBOOLE_1:17; let b be object; assume A14: b in ].p1-a,p1+a.[; then reconsider b as Real; b < p1+a by A14,XXREAL_1:4; then A15: b <= s by A12,XXREAL_0:2; p1-a <= b by A14,XXREAL_1:4; then r <= b by A13,XXREAL_0:2; then b in [.r,s.] by A15,XXREAL_1:1; hence thesis by A1,A2,A3,A14,XBOOLE_0:def 4; end; hence thesis; end; suppose that A16: p1+a > s and A17: p1-a < r; B = [.r,s.] proof thus B c= [.r,s.] by A1; let b be object; assume A18: b in [.r,s.]; then reconsider b as Real; b <= s by A18,XXREAL_1:1; then A19: b < p1+a by A16,XXREAL_0:2; r <= b by A18,XXREAL_1:1; then p1-a < b by A17,XXREAL_0:2; then b in B1 by A3,A19,XXREAL_1:4; hence thesis by A1,A2,A18,XBOOLE_0:def 4; end; hence thesis; end; suppose that A20: p1+a > s and A21: p1-a >= r; B = ].p1-a,s.] proof thus B c= ].p1-a,s.] proof let b be object; assume A22: b in B; then reconsider b as Element of B; b in B1 by A2,A22,XBOOLE_0:def 4; then A23: p1-a < b by A3,XXREAL_1:4; b <= s by A1,A22,XXREAL_1:1; hence thesis by A23,XXREAL_1:2; end; let b be object; assume A24: b in ].p1-a,s.]; then reconsider b as Real; A25: b <= s by A24,XXREAL_1:2; A26: p1-a < b by A24,XXREAL_1:2; then r <= b by A21,XXREAL_0:2; then A27: b in [.r,s.] by A25,XXREAL_1:1; b < p1+a by A20,A25,XXREAL_0:2; then b in B1 by A3,A26,XXREAL_1:4; hence thesis by A1,A2,A27,XBOOLE_0:def 4; end; hence thesis; end; end; theorem Th2: r <= s implies ex B being Basis of Closed-Interval-TSpace(r,s) st (ex f being ManySortedSet of Closed-Interval-TSpace(r,s) st for y being Point of Closed-Interval-MSpace(r,s) holds f.y = {Ball(y,1/n) where n is Nat: n <> 0} & B = Union f) & for X being Subset of Closed-Interval-TSpace(r,s) st X in B holds X is connected proof set L = Closed-Interval-TSpace(r,s), M = Closed-Interval-MSpace(r,s); assume A1: r <= s; defpred P[object,object] means ex x being Point of L, y being Point of M, B being Basis of x st \$1 = x & x = y & \$2 = B & B = {Ball(y,1/n) where n is Nat: n <> 0}; A2: L = TopSpaceMetr(M) by TOPMETR:def 7; A3: for i being object st i in the carrier of L ex j being object st P[i,j] proof let i be object; assume i in the carrier of L; then reconsider i as Point of L; reconsider m = i as Point of M by A2,TOPMETR:12; reconsider j = i as Element of TopSpaceMetr(M) by A2; set B = Balls(j); A4: ex y being Point of M st y = j & B = { Ball(y,1/n) where n is Nat: n <> 0 } by FRECHET:def 1; reconsider B1 = B as Basis of i by A2; take B, i, m, B1; thus thesis by A4; end; consider f being ManySortedSet of the carrier of L such that A5: for i being object st i in the carrier of L holds P[i,f.i] from PBOOLE: sch 3(A3); for x being Element of L holds f.x is Basis of x proof let x be Element of L; P[x,f.x] by A5; hence thesis; end; then reconsider B = Union f as Basis of L by TOPGEN_2:2; take B; hereby take f; let x be Point of M; the carrier of M = [.r,s.] by A1,TOPMETR:10 .= the carrier of L by A1,TOPMETR:18; then P[x,f.x] by A5; hence f.x = {Ball(x,1/n) where n is Nat: n <> 0} & B = Union f; end; let X be Subset of L; assume X in B; then X in union rng f by CARD_3:def 4; then consider Z being set such that A6: X in Z and A7: Z in rng f by TARSKI:def 4; consider x being object such that A8: x in dom f and A9: f.x = Z by A7,FUNCT_1:def 3; consider x1 being Point of L, y being Point of M, B1 being Basis of x1 such that x = x1 and x1 = y and A10: f.x = B1 & B1 = {Ball(y,1/n) where n is Nat: n <> 0} by A5,A8; consider n being Nat such that A11: X = Ball(y,1/n) and n <> 0 by A6,A9,A10; reconsider X1 = X as Subset of R^1 by PRE_TOPC:11; Ball(y,1/n) = [.r,s.] or Ball(y,1/n) = [.r,y+1/n.[ or Ball(y,1/n) = ].y -1/n,s.] or Ball(y,1/n) = ].y-1/n,y+1/n.[ by A1,Th1; then X1 is connected by A11; hence thesis by CONNSP_1:23; end; theorem Th3: for T being TopStruct, A being Subset of T, t be Point of T st t in A holds Component_of(t,A) c= A proof let T be TopStruct, A be Subset of T, t be Point of T; assume A1: t in A; then Down(t,A) = t by CONNSP_3:def 3; then A2: Component_of(t,A) = Component_of Down(t,A) by A1,CONNSP_3:def 7; the carrier of (T|A) = A by PRE_TOPC:8; hence thesis by A2; end; registration let T be TopSpace, A be open Subset of T; cluster T|A -> open; coherence by PRE_TOPC:8; end; theorem Th4: for T being TopSpace, S being SubSpace of T, A being Subset of T, B being Subset of S st A = B holds T|A = S|B proof let T be TopSpace, S be SubSpace of T, A be Subset of T, B be Subset of S; assume A = B; then S|B is SubSpace of T & [#](S|B) = A by PRE_TOPC:def 5,TSEP_1:7; hence thesis by PRE_TOPC:def 5; end; theorem Th5: for S, T being TopSpace, A, B being Subset of T, C, D being Subset of S st the TopStruct of S = the TopStruct of T & A = C & B = D & A,B are_separated holds C,D are_separated by TOPS_3:80; theorem for S, T being TopSpace st the TopStruct of S = the TopStruct of T & S is connected holds T is connected proof let S, T be TopSpace such that A1: the TopStruct of S = the TopStruct of T and A2: S is connected; let A, B be Subset of T such that A3: [#]T = A \/ B and A4: A,B are_separated; reconsider A1 = A, B1 = B as Subset of S by A1; [#]S = the carrier of S & A1,B1 are_separated by A1,A4,Th5; then A1 = {}S or B1 = {}S by A1,A2,A3; hence thesis; end; theorem Th7: for S, T being TopSpace, A being Subset of S, B being Subset of T st the TopStruct of S = the TopStruct of T & A = B & A is connected holds B is connected proof let S, T be TopSpace, A be Subset of S, B be Subset of T such that A1: the TopStruct of S = the TopStruct of T and A2: A = B & A is connected; now let P, Q be Subset of T such that A3: B = P \/ Q and A4: P,Q are_separated; reconsider P1 = P, Q1 = Q as Subset of S by A1; P1,Q1 are_separated by A1,A4,Th5; then P1 = {}S or Q1 = {}S by A2,A3,CONNSP_1:15; hence P = {}T or Q = {}T; end; hence thesis by CONNSP_1:15; end; theorem Th8: for S, T being non empty TopSpace, s being Point of S, t being Point of T, A being a_neighborhood of s st the TopStruct of S = the TopStruct of T & s = t holds A is a_neighborhood of t proof let S, T be non empty TopSpace, s be Point of S, t be Point of T, A be a_neighborhood of s such that A1: the TopStruct of S = the TopStruct of T and A2: s = t; reconsider B = A as Subset of T by A1; A3: s in Int A by CONNSP_2:def 1; Int A = Int B by A1,TOPS_3:77; hence thesis by A2,A3,CONNSP_2:def 1; end; theorem for S, T being non empty TopSpace, A being Subset of S, B being Subset of T, N being a_neighborhood of A st the TopStruct of S = the TopStruct of T & A = B holds N is a_neighborhood of B proof let S, T be non empty TopSpace, A be Subset of S, B be Subset of T, N be a_neighborhood of A such that A1: the TopStruct of S = the TopStruct of T and A2: A = B; reconsider M = N as Subset of T by A1; A3: A c= Int N by CONNSP_2:def 2; Int M = Int N by A1,TOPS_3:77; hence thesis by A2,A3,CONNSP_2:def 2; end; theorem Th10: for S, T being non empty TopSpace, A, B being Subset of T, f being Function of S,T st f is being_homeomorphism & A is_a_component_of B holds f"A is_a_component_of f"B proof let S, T be non empty TopSpace, A, B being Subset of T, f be Function of S,T such that A1: f is being_homeomorphism; A2: rng f = [#]T by A1 .= the carrier of T; set Y = f"A; given X being Subset of T|B such that A3: X = A and A4: X is a_component; A5: the carrier of (T|B) = B by PRE_TOPC:8; then f"X c= f"B by RELAT_1:143; then reconsider Y as Subset of S|(f"B) by A3,PRE_TOPC:8; take Y; thus Y = f"A; X is connected by A4; then A is connected by A3,CONNSP_1:23; then f"A is connected by A1,TOPS_2:62; hence Y is connected by CONNSP_1:23; let Z being Subset of S|(f"B) such that A6: Z is connected and A7: Y c= Z; A8: f.:Y c= f.:Z by A7,RELAT_1:123; A9: f is one-to-one by A1; A10: f is continuous by A1; the carrier of S|(f"B) = f"B by PRE_TOPC:8; then f.:Z c= f.:(f"B) by RELAT_1:123; then reconsider R = f.:Z as Subset of T|B by A5,A2,FUNCT_1:77; reconsider Z1 = Z as Subset of S by PRE_TOPC:11; dom f = the carrier of S by FUNCT_2:def 1; then A11: Z1 c= dom f; Z1 is connected by A6,CONNSP_1:23; then f.:Z1 is connected by A10,TOPS_2:61; then A12: R is connected by CONNSP_1:23; X = f.:Y by A3,A2,FUNCT_1:77; then X = R by A4,A12,A8; hence thesis by A3,A9,A11,FUNCT_1:94; end; begin :: Locally connectedness theorem Th11: for T being non empty TopSpace, S being non empty SubSpace of T, A being non empty Subset of T, B being non empty Subset of S st A = B & A is locally_connected holds B is locally_connected by Th4; theorem Th12: for S, T being non empty TopSpace st the TopStruct of S = the TopStruct of T & S is locally_connected holds T is locally_connected proof let S, T be non empty TopSpace such that A1: the TopStruct of S = the TopStruct of T and A2: S is locally_connected; let t be Point of T; reconsider s = t as Point of S by A1; let U be Subset of T; reconsider U1 = U as Subset of S by A1; assume U is a_neighborhood of t; then A3: U1 is a_neighborhood of s by A1,Th8; S is_locally_connected_in s by A2; then consider V1 being Subset of S such that A4: V1 is a_neighborhood of s and A5: V1 is connected and A6: V1 c= U1 by A3; reconsider V = V1 as Subset of T by A1; take V; thus V is a_neighborhood of t by A1,A4,Th8; thus V is connected by A1,A5,Th7; thus thesis by A6; end; theorem Th13: for T being non empty TopSpace holds T is locally_connected iff [#]T is locally_connected proof let T be non empty TopSpace; T is SubSpace of T by TSEP_1:2; then A1: the TopStruct of T = the TopStruct of (T| [#]T) by PRE_TOPC:8,TSEP_1:5; hence T is locally_connected implies [#]T is locally_connected by Th12; assume [#]T is locally_connected; then T| [#]T is locally_connected; hence thesis by A1,Th12; end; Lm10: for T being non empty TopSpace, S being non empty open SubSpace of T st T is locally_connected holds the TopStruct of S is locally_connected proof let T be non empty TopSpace; let S be non empty open SubSpace of T; reconsider A = [#]S as non empty Subset of T by TSEP_1:1; A1: A is open by TSEP_1:def 1; assume T is locally_connected; then [#]S is locally_connected by A1,Th11,CONNSP_2:17; then S is locally_connected by Th13; then the TopStruct of S is locally_connected by Th12; then [#]the TopStruct of S is locally_connected by Th13; then (the TopStruct of S)| [#]the TopStruct of S is locally_connected; hence thesis by TSEP_1:3; end; theorem Th14: for T being non empty TopSpace, S being non empty open SubSpace of T st T is locally_connected holds S is locally_connected proof let T be non empty TopSpace; let S be non empty open SubSpace of T; assume T is locally_connected; then the TopStruct of S is locally_connected by Lm10; hence thesis by Th12; end; theorem for S, T being non empty TopSpace st S,T are_homeomorphic & S is locally_connected holds T is locally_connected proof let S, T be non empty TopSpace; given f being Function of S,T such that A1: f is being_homeomorphism; assume A2: S is locally_connected; now let A be non empty Subset of T, B being Subset of T; assume A is open & B is_a_component_of A; then A3: f"A is open & f"B is_a_component_of f"A by A1,Th10,TOPGRP_1:26; rng f = [#]T by A1; then f"A is non empty by RELAT_1:139; then f"B is open by A2,A3,CONNSP_2:18; hence B is open by A1,TOPGRP_1:26; end; hence thesis by CONNSP_2:18; end; theorem Th16: for T being non empty TopSpace st ex B being Basis of T st for X being Subset of T st X in B holds X is connected holds T is locally_connected proof let T be non empty TopSpace; given B being Basis of T such that A1: for X being Subset of T st X in B holds X is connected; let x be Point of T; let U be Subset of T such that A2: x in Int U; Int U in the topology of T & the topology of T c= UniCl B by CANTOR_1:def 2 ,PRE_TOPC:def 2; then consider Y being Subset-Family of T such that A3: Y c= B and A4: Int U = union Y by CANTOR_1:def 1; consider V being set such that A5: x in V and A6: V in Y by A2,A4,TARSKI:def 4; reconsider V as Subset of T by A6; take V; B c= the topology of T & V in B by A3,A6,TOPS_2:64; then V is open by PRE_TOPC:def 2; hence x in Int V by A5,TOPS_1:23; thus V is connected by A1,A3,A6; A7: Int U c= U by TOPS_1:16; V c= union Y by A6,ZFMISC_1:74; hence thesis by A4,A7; end; theorem Th17: r <= s implies Closed-Interval-TSpace(r,s) is locally_connected proof assume r <= s; then ex B being Basis of Closed-Interval-TSpace(r,s) st (ex f being ManySortedSet of Closed-Interval-TSpace(r,s) st for y being Point of Closed-Interval-MSpace(r,s) holds f.y = {Ball(y,1/n) where n is Nat: n <> 0} & B = Union f) & for X being Subset of Closed-Interval-TSpace(r,s) st X in B holds X is connected by Th2; hence thesis by Th16; end; registration cluster I[01] -> locally_connected; coherence by Th17,TOPMETR:20; end; registration let A be non empty open Subset of I[01]; cluster I[01] | A -> locally_connected; coherence by Th14; end; begin :: Some useful functions definition let r be Real; func ExtendInt(r) -> Function of I[01], R^1 means :Def1: for x being Point of I[01] holds it.x = r*x; existence proof defpred P[Real,set] means \$2 = r*\$1; A1: for x being Element of I[01] ex y being Element of R st P[x,y] proof let x be Element of I[01]; take r*x; thus thesis by TOPMETR:17,XREAL_0:def 1; end; ex f being Function of I, R st for x being Element of I[01] holds P[x, f.x] from FUNCT_2:sch 3(A1); hence thesis; end; uniqueness proof let f, g be Function of I[01], R^1 such that A2: for x being Point of I[01] holds f.x = r*x and A3: for x being Point of I[01] holds g.x = r*x; for x being Point of I[01] holds f.x = g.x proof let x be Point of I[01]; thus f.x = r*x by A2 .= g.x by A3; end; hence f = g; end; end; registration let r be Real; cluster ExtendInt(r) -> continuous; coherence proof reconsider f1 = id I[01] as Function of I[01],R^1 by BORSUK_1:40,FUNCT_2:7 ,TOPMETR:17; f1 is continuous by PRE_TOPC:26; then consider g being Function of I[01],R^1 such that A1: for p being Point of I[01], r1 being Real st f1.p=r1 holds g.p=r*r1 and A2: g is continuous by JGRAPH_2:23; for x being Point of I[01] holds g.x = (ExtendInt(r)).x proof let x be Point of I[01]; thus g.x = r*f1.x by A1 .= r*x .= (ExtendInt(r)).x by Def1; end; hence thesis by A2,FUNCT_2:63; end; end; definition let r be Real; redefine func ExtendInt(r) -> Path of R^1(0),R^1(r); coherence proof thus ExtendInt(r) is continuous; thus (ExtendInt(r)).0 = r * 0 by Def1,BORSUK_1:def 14 .= R^1(0) by TOPREALB:def 2; thus (ExtendInt(r)).1 = r * 1 by Def1,BORSUK_1:def 15 .= R^1(r) by TOPREALB:def 2; end; end; definition let S, T, Y be non empty TopSpace, H be Function of [:S,T:],Y, t be Point of T; func Prj1(t,H) -> Function of S,Y means :Def2: for s being Point of S holds it.s = H.(s,t); existence proof deffunc F(Point of S) = H. [\$1,t]; consider f being Function of the carrier of S, the carrier of Y such that A1: for x being Element of S holds f.x = F(x) from FUNCT_2:sch 4; take f; let x be Point of S; thus thesis by A1; end; uniqueness proof let f, g be Function of S,Y such that A2: for s being Point of S holds f.s = H.(s,t) and A3: for s being Point of S holds g.s = H.(s,t); now let s be Point of S; thus f.s = H.(s,t) by A2 .= g.s by A3; end; hence thesis; end; end; definition let S, T, Y be non empty TopSpace, H be Function of [:S,T:],Y, s be Point of S; func Prj2(s,H) -> Function of T,Y means :Def3: for t being Point of T holds it.t = H.(s,t); existence proof deffunc F(Point of T) = H. [s,\$1]; consider f being Function of the carrier of T, the carrier of Y such that A1: for x being Element of T holds f.x = F(x) from FUNCT_2:sch 4; take f; let x be Point of T; thus thesis by A1; end; uniqueness proof let f, g be Function of T,Y such that A2: for t being Point of T holds f.t = H.(s,t) and A3: for t being Point of T holds g.t = H.(s,t); now let t be Point of T; thus f.t = H.(s,t) by A2 .= g.t by A3; end; hence thesis; end; end; registration let S, T, Y be non empty TopSpace, H be continuous Function of [:S,T:],Y, t be Point of T; cluster Prj1(t,H) -> continuous; coherence proof for p being Point of S, V being Subset of Y st Prj1(t,H).p in V & V is open holds ex W being Subset of S st p in W & W is open & Prj1(t,H).:W c= V proof let p be Point of S, V be Subset of Y such that A1: Prj1(t,H).p in V & V is open; Prj1(t,H).p = H.(p,t) by Def2; then consider W being Subset of [:S,T:] such that A2: [p,t] in W and A3: W is open and A4: H.:W c= V by A1,JGRAPH_2:10; consider A being Subset-Family of [:S,T:] such that A5: W = union A and A6: for e being set st e in A ex X1 being Subset of S, Y1 being Subset of T st e = [:X1,Y1:] & X1 is open & Y1 is open by A3,BORSUK_1:5; consider e being set such that A7: [p,t] in e and A8: e in A by A2,A5,TARSKI:def 4; consider X1 being Subset of S, Y1 being Subset of T such that A9: e = [:X1,Y1:] and A10: X1 is open and Y1 is open by A6,A8; take X1; thus p in X1 by A7,A9,ZFMISC_1:87; thus X1 is open by A10; let x be object; assume x in Prj1(t,H).:X1; then consider c being Point of S such that A11: c in X1 and A12: x = Prj1(t,H).c by FUNCT_2:65; t in Y1 by A7,A9,ZFMISC_1:87; then [c,t] in [:X1,Y1:] by A11,ZFMISC_1:87; then [c,t] in W by A5,A8,A9,TARSKI:def 4; then A13: H. [c,t] in H.:W by FUNCT_2:35; Prj1(t,H).c = H.(c,t) by Def2 .= H. [c,t]; hence thesis by A4,A12,A13; end; hence thesis by JGRAPH_2:10; end; end; registration let S, T, Y be non empty TopSpace, H be continuous Function of [:S,T:],Y, s be Point of S; cluster Prj2(s,H) -> continuous; coherence proof for p being Point of T, V being Subset of Y st Prj2(s,H).p in V & V is open holds ex W being Subset of T st p in W & W is open & Prj2(s,H).:W c= V proof let p be Point of T, V be Subset of Y such that A1: Prj2(s,H).p in V & V is open; Prj2(s,H).p = H.(s,p) by Def3; then consider W being Subset of [:S,T:] such that A2: [s,p] in W and A3: W is open and A4: H.:W c= V by A1,JGRAPH_2:10; consider A being Subset-Family of [:S,T:] such that A5: W = union A and A6: for e being set st e in A ex X1 being Subset of S, Y1 being Subset of T st e = [:X1,Y1:] & X1 is open & Y1 is open by A3,BORSUK_1:5; consider e being set such that A7: [s,p] in e and A8: e in A by A2,A5,TARSKI:def 4; consider X1 being Subset of S, Y1 being Subset of T such that A9: e = [:X1,Y1:] and X1 is open and A10: Y1 is open by A6,A8; take Y1; thus p in Y1 by A7,A9,ZFMISC_1:87; thus Y1 is open by A10; let x be object; assume x in Prj2(s,H).:Y1; then consider c being Point of T such that A11: c in Y1 and A12: x = Prj2(s,H).c by FUNCT_2:65; s in X1 by A7,A9,ZFMISC_1:87; then [s,c] in [:X1,Y1:] by A11,ZFMISC_1:87; then [s,c] in W by A5,A8,A9,TARSKI:def 4; then A13: H. [s,c] in H.:W by FUNCT_2:35; Prj2(s,H).c = H.(s,c) by Def3 .= H. [s,c]; hence thesis by A4,A12,A13; end; hence thesis by JGRAPH_2:10; end; end; theorem for T being non empty TopSpace, a, b being Point of T, P, Q being Path of a,b, H being Homotopy of P,Q, t being Point of I[01] st H is continuous holds Prj1(t,H) is continuous; theorem for T being non empty TopSpace, a, b being Point of T, P, Q being Path of a,b, H being Homotopy of P,Q, s being Point of I[01] st H is continuous holds Prj2(s,H) is continuous; set TUC = Tunit_circle(2); set cS1 = the carrier of TUC; Lm11: now TUC = Tcircle(0.TOP-REAL 2,1) by TOPREALB:def 7; hence cS1 = Sphere(|[0,0]|,1) by EUCLID:54,TOPREALB:9; end; Lm12: dom CircleMap = REAL by FUNCT_2:def 1,TOPMETR:17; definition let r be Real; func cLoop(r) -> Function of I[01], Tunit_circle(2) means :Def4: for x being Point of I[01] holds it.x = |[ cos(2*PI*r*x), sin(2*PI*r*x) ]|; existence proof defpred P[Real,set] means \$2 = |[ cos(2*PI*r*\$1), sin(2*PI*r*\$1) ]|; A1: for x being Element of I[01] ex y being Element of cS1 st P[x,y] proof let x be Element of I[01]; set y = |[ cos(2*PI*r*x), sin(2*PI*r*x) ]|; |. y - o .| = |. y .| by EUCLID:54,RLVECT_1:13 .= sqrt((y`1)^2+(y`2)^2) by JGRAPH_1:30 .= sqrt((cos(2*PI*r*x))^2+(y`2)^2) by EUCLID:52 .= sqrt((cos(2*PI*r*x))^2+(sin(2*PI*r*x))^2) by EUCLID:52 .= 1 by SIN_COS:29,SQUARE_1:18; then reconsider y as Element of cS1 by Lm11,TOPREAL9:9; take y; thus thesis; end; ex f being Function of I, cS1 st for x being Element of I[01] holds P[ x,f.x] from FUNCT_2:sch 3(A1); hence thesis; end; uniqueness proof let f, g be Function of I[01], TUC such that A2: for x being Point of I[01] holds f.x = |[cos(2*PI*r*x),sin(2*PI*r* x)]| and A3: for x being Point of I[01] holds g.x = |[cos(2*PI*r*x),sin(2*PI*r* x)]|; for x being Point of I[01] holds f.x = g.x proof let x be Point of I[01]; thus f.x = |[cos(2*PI*r*x),sin(2*PI*r*x)]| by A2 .= g.x by A3; end; hence f = g; end; end; theorem Th20: cLoop(r) = CircleMap * ExtendInt(r) proof for x being Point of I[01] holds (cLoop(r)).x = (CircleMap * ExtendInt(r )). x proof let x be Point of I[01]; A1: (ExtendInt(r)).x = r*x by Def1; thus (cLoop(r)).x = |[ cos(2*PI*r*x), sin(2*PI*r*x) ]| by Def4 .= |[ cos(2*PI*(ExtendInt(r)).x), sin(2*PI*(ExtendInt(r)).x) ]| by A1 .= CircleMap.((ExtendInt(r)).x) by TOPREALB:def 11 .= (CircleMap * ExtendInt(r)).x by FUNCT_2:15; end; hence thesis; end; definition let n be Integer; redefine func cLoop(n) -> Loop of c[10]; coherence proof set f = cLoop(n); f = CircleMap * ExtendInt(n) by Th20; hence f is continuous; thus f.0 = |[ cos(2*PI*n*j0), sin(2*PI*n*j0) ]| by Def4 .= c[10] by SIN_COS:31,TOPREALB:def 8; thus f.1 = |[ cos(2*PI*n*j1), sin(2*PI*n*j1) ]| by Def4 .= |[ cos(0), sin(2*PI*n+0) ]| by COMPLEX2:9 .= c[10] by COMPLEX2:8,SIN_COS:31,TOPREALB:def 8; end; end; begin :: Main theorems Lm13: ex F being Subset-Family of Tunit_circle(2) st F is Cover of Tunit_circle(2) & F is open & for U being Subset of Tunit_circle(2) st 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 for f being Function of R^1 | d, ( Tunit_circle(2)) | U st f = CircleMap|d holds f is being_homeomorphism proof 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) 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) 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; thus F is Cover of Tunit_circle(2) & F is open by A2; let U be Subset of Tunit_circle(2); assume A4: U in F; per cases by A1,A4,TARSKI:def 2; suppose A5: U = (CircleMap).:].0,1.[; reconsider D = IntIntervals(0,1) as mutually-disjoint open Subset-Family of R^1 by Lm8,TOPREALB:4; take D; thus thesis by A3,A5; end; suppose A6: U = (CircleMap).:].1/2,3/2.[; reconsider D = IntIntervals(1/2,3/2) as mutually-disjoint open Subset-Family of R^1 by Lm9,TOPREALB:4; take D; thus thesis by A3,A6; end; end; Lm14: [#]Sspace(0[01]) = {0} by TEX_2:def 2; Lm15: for F being Subset-Family of Closed-Interval-TSpace(r,s), C being IntervalCover of F, G being IntervalCoverPts of C holds F is Cover of Closed-Interval-TSpace(r,s) & F is open connected & r <= s implies G is non empty proof let F be Subset-Family of Closed-Interval-TSpace(r,s), C be IntervalCover of F, G be IntervalCoverPts of C; assume F is Cover of Closed-Interval-TSpace(r,s) & F is open connected & r <= s; then len G = len C + 1 by RCOMP_3:def 3; hence thesis by CARD_1:27; end; theorem Th21: for UL being Subset-Family of Tunit_circle(2) st UL is Cover of Tunit_circle(2) & UL is open for Y being non empty TopSpace, F being continuous Function of [:Y,I[01]:], Tunit_circle(2), y being Point of Y ex T being non empty FinSequence of REAL st T.1 = 0 & T.len T = 1 & T is increasing & ex N being open Subset of Y st y in N & for i being Nat st i in dom T & i +1 in dom T ex Ui being non empty Subset of Tunit_circle(2) st Ui in UL & F.:[: N,[.T.i,T.(i+1).]:] c= Ui proof set L = Closed-Interval-TSpace(0,1); let UL be Subset-Family of TUC such that A1: UL is Cover of TUC and A2: UL is open; let Y be non empty TopSpace, F be continuous Function of [:Y,I[01]:], TUC, y be Point of Y; A3: [#]TUC = union UL by A1,SETFAM_1:45; A4: for i being Point of I[01] ex U being non empty open Subset of TUC st F. [y,i] in U & U in UL proof let i be Point of I[01]; consider U being set such that A5: F. [y,i] in U & U in UL by A3,TARSKI:def 4; reconsider U as non empty open Subset of TUC by A2,A5; take U; thus thesis by A5; end; then ex U being non empty open Subset of TUC st F. [y,0[01]] in U & U in UL; then reconsider UL1 = UL as non empty set; set C = the carrier of Y; defpred I0[set,set] means ex V being open Subset of TUC st V in UL1 & F. [y, \$1] in V & \$2 = V; A6: for i being Element of I ex z being Element of UL1 st I0[i,z] proof let i be Element of I; ex U being non empty open Subset of TUC st F. [y,i] in U & U in UL by A4; hence thesis; end; consider I0 being Function of I, UL1 such that A7: for i being Element of I holds I0[i,I0.i] from FUNCT_2:sch 3(A6); defpred I1[object,object] means ex M being open Subset of Y, O being open connected Subset of I[01] st y in M & \$1 in O & F.:[:M,O:] c= I0.\$1 & \$2 = [:M, O:]; A8: for i being Element of I ex z being Subset of [:C,I:] st I1[i,z] proof let i be Element of I; consider V being open Subset of TUC such that V in UL1 and A9: F. [y,i] in V and A10: I0.i = V by A7; consider W being Subset of [:Y,I[01]:] such that A11: [y,i] in W and A12: W is open and A13: F.:W c= V by A9,JGRAPH_2:10; consider Q being Subset-Family of [:Y,I[01]:] such that A14: W = union Q and A15: for e being set st e in Q ex A being Subset of Y, B being Subset of I[01] st e = [:A,B:] & A is open & B is open by A12,BORSUK_1:5; consider Z being set such that A16: [y,i] in Z and A17: Z in Q by A11,A14,TARSKI:def 4; consider A being Subset of Y, B being Subset of I[01] such that A18: Z = [:A,B:] and A19: A is open and A20: B is open by A15,A17; reconsider A as open Subset of Y by A19; A21: i in B by A16,A18,ZFMISC_1:87; reconsider B as non empty open Subset of I[01] by A16,A18,A20; reconsider i1 = i as Point of I[01]|B by A21,PRE_TOPC:8; Component_of i1 is a_component by CONNSP_1:40; then A22: Component_of i1 is open by CONNSP_2:15; Component_of(i,B) = Component_of i1 by A21,CONNSP_3:def 7; then reconsider D = Component_of(i,B) as open connected Subset of I[01] by A21,A22, CONNSP_3:33,TSEP_1:17; reconsider z = [:A,D:] as Subset of [:C,I:] by BORSUK_1:def 2; take z, A, D; thus y in A by A16,A18,ZFMISC_1:87; thus i in D by A21,CONNSP_3:26; D c= B by A21,Th3; then A23: z c= [:A,B:] by ZFMISC_1:95; [:A,B:] c= W by A14,A17,A18,ZFMISC_1:74; then z c= W by A23; then F.:z c= F.:W by RELAT_1:123; hence F.:[:A,D:] c= I0.i by A10,A13; thus thesis; end; consider I1 being Function of I, bool [:C,I:] such that A24: for i being Element of I holds I1[i,I1.i] from FUNCT_2:sch 3(A8); reconsider C1 = rng I1 as Subset-Family of [:Y,I[01]:] by BORSUK_1:def 2; A25: C1 is open proof let P be Subset of [:Y,I[01]:]; assume P in C1; then consider i being object such that A26: i in dom I1 and A27: I1.i = P by FUNCT_1:def 3; I1[i,I1.i] by A24,A26; hence thesis by A27,BORSUK_1:6; end; A28: dom I1 = I by FUNCT_2:def 1; [:{y},[#]I[01]:] c= union C1 proof let a be object; assume a in [:{y},[#]I[01]:]; then consider a1, a2 being object such that A29: a1 in {y} and A30: a2 in [#]I[01] and A31: a = [a1,a2] by ZFMISC_1:def 2; A32: a1 = y by A29,TARSKI:def 1; reconsider a2 as Point of I[01] by A30; consider M being open Subset of Y, O being open connected Subset of I[01] such that A33: y in M & a2 in O and F.:[:M,O:] c= I0.a2 and A34: I1.a2 = [:M,O:] by A24; [y,a2] in [:M,O:] & [:M,O:] in C1 by A28,A33,A34,FUNCT_1:def 3,ZFMISC_1:87; hence thesis by A31,A32,TARSKI:def 4; end; then A35: C1 is Cover of [:{y},[#]I[01]:] by SETFAM_1:def 11; [:{y},[#]I[01]:] is compact by BORSUK_3:23; then consider G being Subset-Family of [:Y,I[01]:] such that A36: G c= C1 and A37: G is Cover of [:{y},[#]I[01]:] and A38: G is finite by A35,A25; set NN = {M where M is open Subset of Y: y in M & ex O being open Subset of I[01] st [:M,O:] in G}; NN c= bool C proof let a be object; assume a in NN; then ex M being open Subset of Y st a = M & y in M & ex O being open Subset of I[01] st [:M,O:] in G; hence thesis; end; then reconsider NN as Subset-Family of Y; consider p being Function such that A39: rng p = G and A40: dom p in omega by A38,FINSET_1:def 1; defpred F[object,object] means ex M being open Subset of Y, O being non empty open Subset of I[01] st y in M & p.\$1 = [:M,O:] & \$2 = M; A41: for x being object st x in dom p ex y being object st y in NN & F[x,y] proof let x be object; assume x in dom p; then A42: p.x in rng p by FUNCT_1:def 3; then consider i being object such that A43: i in dom I1 and A44: I1.i = p.x by A36,A39,FUNCT_1:def 3; consider M being open Subset of Y, O being open connected Subset of I[01] such that A45: y in M & i in O and F.:[:M,O:] c= I0.i and A46: I1.i = [:M,O:] by A24,A43; take M; thus thesis by A39,A42,A44,A45,A46; end; consider p1 being Function of dom p, NN such that A47: for x being object st x in dom p holds F[x,p1.x] from FUNCT_2:sch 1( A41); set ICOV = {O where O is open connected Subset of I[01]: ex M being open Subset of Y st [:M,O:] in G}; A48: [:{y},[#]I[01]:] c= union G by A37,SETFAM_1:def 11; A49: y in {y} by TARSKI:def 1; then [y,0[01]] in [:{y},[#]I[01]:] by ZFMISC_1:def 2; then consider Z being set such that [y,0[01]] in Z and A50: Z in G by A48,TARSKI:def 4; consider i being object such that A51: i in dom I1 and A52: I1.i = Z by A36,A50,FUNCT_1:def 3; consider M being open Subset of Y, O being open connected Subset of I[01] such that A53: y in M and i in O and F.:[:M,O:] c= I0.i and A54: I1.i = [:M,O:] by A24,A51; A55: M in NN by A50,A52,A53,A54; then A56: dom p1 = dom p by FUNCT_2:def 1; rng p1 = NN proof thus rng p1 c= NN; let a be object; assume a in NN; then consider M being open Subset of Y such that A57: a = M and y in M and A58: ex O being open Subset of I[01] st [:M,O:] in G; consider O being open Subset of I[01] such that A59: [:M,O:] in G by A58; consider b being object such that A60: b in dom p and A61: p.b = [:M,O:] by A39,A59,FUNCT_1:def 3; consider M1 being open Subset of Y, O1 being non empty open Subset of I[01] such that A62: y in M1 & p.b = [:M1,O1:] and A63: p1.b = M1 by A47,A60; M1 = M by A61,A62,ZFMISC_1:110; hence thesis by A56,A57,A60,A63,FUNCT_1:def 3; end; then A64: NN is finite by A40,A56,FINSET_1:def 1; NN is open proof let a be Subset of Y; assume a in NN; then ex M being open Subset of Y st a = M & y in M & ex O being open Subset of I[01] st [:M,O:] in G; hence thesis; end; then reconsider N = meet NN as open Subset of Y by A64,TOPS_2:20; ICOV c= bool I proof let a be object; assume a in ICOV; then ex O being open connected Subset of I[01] st a = O & ex M being open Subset of Y st [:M,O:] in G; hence thesis; end; then reconsider ICOV as Subset-Family of L by TOPMETR:20; [#]L c= union ICOV proof let a be object; assume a in [#]L; then reconsider a as Point of I[01] by TOPMETR:20; [y,a] in [:{y},[#]I[01]:] by A49,ZFMISC_1:def 2; then consider Z being set such that A65: [y,a] in Z and A66: Z in G by A48,TARSKI:def 4; consider i being object such that A67: i in dom I1 and A68: I1.i = Z by A36,A66,FUNCT_1:def 3; consider M being open Subset of Y, O being open connected Subset of I[01] such that y in M and i in O and F.:[:M,O:] c= I0.i and A69: I1.i = [:M,O:] by A24,A67; a in O & O in ICOV by A65,A66,A68,A69,ZFMISC_1:87; hence thesis by TARSKI:def 4; end; then A70: ICOV is Cover of L by SETFAM_1:def 11; set NCOV = the IntervalCover of ICOV; set T = the IntervalCoverPts of NCOV; A71: ICOV is connected proof let X be Subset of L; assume X in ICOV; then ex O being open connected Subset of I[01] st X = O & ex M being open Subset of Y st [:M,O:] in G; hence thesis by TOPMETR:20; end; A72: ICOV is open proof let a be Subset of L; assume a in ICOV; then ex O being open connected Subset of I[01] st a = O & ex M being open Subset of Y st [:M,O:] in G; hence thesis by TOPMETR:20; end; then reconsider T as non empty FinSequence of REAL by A70,A71,Lm15; take T; thus T.1 = 0 & T.len T = 1 by A70,A72,A71,RCOMP_3:def 3; thus T is increasing by A70,A72,A71,RCOMP_3:65; take N; now let Z be set; assume Z in NN; then ex M being open Subset of Y st Z = M & y in M & ex O being open Subset of I[01] st [:M,O:] in G; hence y in Z; end; hence y in N by A55,SETFAM_1:def 1; let i be Nat; assume that A73: i in dom T and A74: i+1 in dom T; A75: 1 <= i by A73,FINSEQ_3:25; A76: i+1 <= len T by A74,FINSEQ_3:25; len T = len NCOV + 1 by A70,A72,A71,RCOMP_3:def 3; then i <= len NCOV by A76,XREAL_1:6; then i in dom NCOV by A75,FINSEQ_3:25; then A77: NCOV.i in rng NCOV by FUNCT_1:def 3; rng NCOV c= ICOV by A70,A72,A71,RCOMP_3:def 2; then NCOV.i in ICOV by A77; then consider O being open connected Subset of I[01] such that A78: NCOV.i = O and A79: ex M being open Subset of Y st [:M,O:] in G; consider M being open Subset of Y such that A80: [:M,O:] in G by A79; i < len T by A76,NAT_1:13; then A81: [.T.i,T.(i+1).] c= O by A70,A72,A71,A75,A78,RCOMP_3:66; consider j being object such that A82: j in dom I1 and A83: I1.j = [:M,O:] by A36,A80,FUNCT_1:def 3; consider V being open Subset of TUC such that A84: V in UL1 and A85: F. [y,j] in V and A86: I0.j = V by A7,A82; reconsider V as non empty open Subset of TUC by A85; take V; thus V in UL by A84; consider M1 being open Subset of Y, O1 being open connected Subset of I[01] such that A87: y in M1 and A88: j in O1 and A89: F.:[:M1,O1:] c= I0.j and A90: I1.j = [:M1,O1:] by A24,A82; M = M1 by A83,A87,A88,A90,ZFMISC_1:110; then M in NN by A80,A87; then N c= M by SETFAM_1:3; then [:N,[.T.i,T.(i+1).]:] c= [:M1,O1:] by A83,A90,A81,ZFMISC_1:96; then F.:[:N,[.T.i,T.(i+1).]:] c= F.:[:M1,O1:] by RELAT_1:123; hence thesis by A89,A86; end; theorem Th22: for Y being non empty TopSpace, F being Function of [:Y,I[01]:], Tunit_circle(2), Ft being Function of [:Y,Sspace(0[01]):], R^1 st F is continuous & Ft is continuous & F | [:the carrier of Y,{0}:] = CircleMap*Ft ex G being Function of [:Y,I[01]:], R^1 st G is continuous & F = CircleMap*G & G | [:the carrier of Y,{0}:] = Ft & for H being Function of [:Y,I[01]:], R^1 st H is continuous & F = CircleMap*H & H | [:the carrier of Y,{0}:] = Ft holds G = H proof consider UL being Subset-Family of TUC such that A1: UL is Cover of TUC & UL is open and A2: for U being Subset of TUC st U in UL 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 for f being Function of R^1 | d, TUC | U st f = CircleMap|d holds f is being_homeomorphism by Lm13; let Y be non empty TopSpace, F be Function of [:Y,I[01]:], TUC, Ft be Function of [:Y,Sspace(0[01]):], R^1 such that A3: F is continuous and A4: Ft is continuous and A5: F | [:the carrier of Y,{0}:] = CircleMap*Ft; defpred A[set,set] means ex y being Point of Y, t being Point of I[01], N being non empty open Subset of Y, Fn being Function of [:Y|N,I[01]:], R^1 st \$1 = [y,t] & \$2 = Fn.\$1 & y in N & Fn is continuous & F | [:N,I:] = CircleMap*Fn & Fn | [:the carrier of Y,{0}:] = Ft | [:N,I:] & for H being Function of [:Y|N, I[01]:], R^1 st H is continuous & F | [:N,I:] = CircleMap*H & H | [:the carrier of Y,{0}:] = Ft | [:N,I:] holds Fn = H; A6: dom F = the carrier of [:Y,I[01]:] by FUNCT_2:def 1 .= [:the carrier of Y,I:] by BORSUK_1:def 2; A7: the carrier of [:Y,Sspace(0[01]):] = [:the carrier of Y, the carrier of Sspace(0[01]):] by BORSUK_1:def 2; then A8: dom Ft = [:the carrier of Y,{0}:] by Lm14,FUNCT_2:def 1; A9: for x being Point of [:Y,I[01]:] ex z being Point of R^1 st A[x,z] proof let x be Point of [:Y,I[01]:]; consider y being Point of Y, t being Point of I[01] such that A10: x = [y,t] by BORSUK_1:10; consider TT being non empty FinSequence of REAL such that A11: TT.1 = 0 and A12: TT.len TT = 1 and A13: TT is increasing and A14: ex N being open Subset of Y st y in N & for i being Nat st i in dom TT & i+1 in dom TT ex Ui being non empty Subset of Tunit_circle(2) st Ui in UL & F.:[:N,[.TT.i,TT.(i+1).]:] c= Ui by A3,A1,Th21; consider N being open Subset of Y such that A15: y in N and A16: for i being Nat st i in dom TT & i+1 in dom TT ex Ui being non empty Subset of Tunit_circle(2) st Ui in UL & F.:[:N,[.TT.i,TT.(i+1) .]:] c= Ui by A14; reconsider N as non empty open Subset of Y by A15; defpred N[Nat] means \$1 in dom TT implies ex N2 being non empty open Subset of Y, S being non empty Subset of I[01], Fn being Function of [:Y| N2,I[01]|S:], R^1 st S = [.0,TT.\$1.] & y in N2 & N2 c= N & Fn is continuous & F | [:N2,S:] = CircleMap*Fn & Fn | [:the carrier of Y,{0}:] = Ft | [:N2,I:]; A17: len TT in dom TT by FINSEQ_5:6; A18: 1 in dom TT by FINSEQ_5:6; A19: now let i be Element of NAT such that A20: i in dom TT; 1 <= i by A20,FINSEQ_3:25; then 1 = i or 1 < i by XXREAL_0:1; hence A21: 0 <= TT.i by A11,A13,A18,A20,SEQM_3:def 1; assume A22: i+1 in dom TT; A23: i+0 < i+1 by XREAL_1:8; hence A24: TT.i < TT.(i+1) by A13,A20,A22,SEQM_3:def 1; i+1 <= len TT by A22,FINSEQ_3:25; then i+1 = len TT or i+1 < len TT by XXREAL_0:1; hence TT.(i+1) <= 1 by A12,A13,A17,A22,SEQM_3:def 1; hence TT.i < 1 by A24,XXREAL_0:2; thus 0 < TT.(i+1) by A13,A20,A21,A22,A23,SEQM_3:def 1; end; A25: now let i be Nat such that A26: 0 <= TT.i and A27: TT.(i+1) <= 1; thus [.TT.i,TT.(i+1).] c= I proof let a be object; assume A28: a in [.TT.i,TT.(i+1).]; then reconsider a as Real; a <= TT.(i+1) by A28,XXREAL_1:1; then A29: a <= 1 by A27,XXREAL_0:2; 0 <= a by A26,A28,XXREAL_1:1; hence thesis by A29,BORSUK_1:43; end; end; A30: for i being Nat st N[i] holds N[i+1] proof let i be Nat; assume that A31: N[i] and A32: i+1 in dom TT; per cases by A32,TOPREALA:2; suppose A33: i = 0; take N2 = N; set Fn = Ft | [:N2,{0}:]; set S = [.0,TT.(i+1).]; A34: S = {0} by A11,A33,XXREAL_1:17; reconsider S as non empty Subset of I[01] by A11,A33,Lm3,XXREAL_1:17; A35: dom Fn = [:N2,S:] by A8,A34,RELAT_1:62,ZFMISC_1:96; reconsider K0 = [:N2,S:] as non empty Subset of [:Y,Sspace(0[01]):] by A7,A34,Lm14,ZFMISC_1:96; A36: the carrier of [:Y|N2,I[01]|S:] = [:the carrier of (Y|N2), the carrier of ( I[01]|S):] & rng Fn c= R by BORSUK_1:def 2; the carrier of (Y|N2) = N2 & the carrier of (I[01]|S) = S by PRE_TOPC:8 ; then reconsider Fn as Function of [:Y|N2,I[01]|S:], R^1 by A35,A36, FUNCT_2:2; A37: dom (F | [:N2,S:]) = [:N2,S:] by A6,RELAT_1:62,ZFMISC_1:96; reconsider S1 = S as non empty Subset of Sspace(0[01]) by A11,A33,Lm14, XXREAL_1:17; take S, Fn; thus S = [.0,TT.(i+1).]; thus y in N2 by A15; thus N2 c= N; I[01]|S = Sspace(0[01]) by A34,TOPALG_3:5 .= (Sspace(0[01]))|S1 by A34,Lm14,TSEP_1:3; then [:Y|N2,I[01]|S:] = [:Y,Sspace(0[01]):]|K0 by BORSUK_3:22; hence Fn is continuous by A4,A34,TOPMETR:7; rng Fn c= dom CircleMap by Lm12,TOPMETR:17; then A38: dom (CircleMap*Fn) = dom Fn by RELAT_1:27; A39: [:N2,S:] c= dom Ft by A8,A34,ZFMISC_1:96; for x being object st x in dom (F | [:N2,S:]) holds (F | [:N2,S:]).x = (CircleMap*Fn).x proof let x be object such that A40: x in dom (F | [:N2,S:]); thus (F | [:N2,S:]).x = F.x by A37,A40,FUNCT_1:49 .= (CircleMap*Ft).x by A5,A7,A35,A37,A40,Lm14,FUNCT_1:49 .= CircleMap.(Ft.x) by A39,A37,A40,FUNCT_1:13 .= CircleMap.(Fn.x) by A34,A37,A40,FUNCT_1:49 .= (CircleMap*Fn).x by A35,A37,A40,FUNCT_1:13; end; hence F | [:N2,S:] = CircleMap*Fn by A35,A37,A38; A41: dom (Fn | [:the carrier of Y,{0}:]) = [:N2,S:] /\ [:the carrier of Y,{0}:] by A35,RELAT_1:61; A42: for x being object st x in dom (Fn | [:the carrier of Y,{0}:]) holds (Fn | [:the carrier of Y,{0}:]).x = (Ft | [:N2,I:]).x proof A43: [:N2,{0}:] c= [:N2,I:] by Lm3,ZFMISC_1:95; let x be object such that A44: x in dom (Fn | [:the carrier of Y,{0}:]); A45: x in [:N2,{0}:] by A34,A41,A44,XBOOLE_0:def 4; x in [:the carrier of Y,{0}:] by A41,A44,XBOOLE_0:def 4; hence (Fn | [:the carrier of Y,{0}:]).x = Fn.x by FUNCT_1:49 .= Ft.x by A45,FUNCT_1:49 .= (Ft | [:N2,I:]).x by A45,A43,FUNCT_1:49; end; dom (Ft | [:N2,I:]) = [:the carrier of Y,{0}:] /\ [:N2,I:] by A8, RELAT_1:61 .= [:N2,S:] by A34,ZFMISC_1:101; hence thesis by A34,A41,A42,ZFMISC_1:101; end; suppose A46: i in dom TT; set SS = [.TT.i,TT.(i+1).]; consider Ui being non empty Subset of TUC such that A47: Ui in UL and A48: F.:[:N,SS:] c= Ui by A16,A32,A46; consider D being mutually-disjoint open Subset-Family of R^1 such that A49: union D = (CircleMap)"Ui and A50: for d being Subset of R^1 st d in D for f being Function of R^1 | d, TUC | Ui st f = CircleMap|d holds f is being_homeomorphism by A2,A47; A51: the carrier of (TUC | Ui) = Ui by PRE_TOPC:8; A52: TT.i < TT.(i+1) by A19,A32,A46; then TT.i in SS by XXREAL_1:1; then A53: [y,TT.i] in [:N,SS:] by A15,ZFMISC_1:87; consider N2 being open Subset of Y, S being non empty Subset of I[01], Fn being Function of [:Y|N2,I[01]|S:], R^1 such that A54: S = [.0,TT.i.] and A55: y in N2 and A56: N2 c= N and A57: Fn is continuous and A58: F | [:N2,S:] = CircleMap*Fn and A59: Fn | [:the carrier of Y,{0}:] = Ft | [:N2,I:] by A31,A46; reconsider N2 as non empty open Subset of Y by A55; A60: the carrier of [:Y|N2,I[01]|S:] = [:the carrier of (Y|N2), the carrier of (I[01]|S):] by BORSUK_1:def 2; N2 c= N2; then reconsider N7 = N2 as non empty Subset of Y|N2 by PRE_TOPC:8; A61: dom Fn = the carrier of [:Y|N2,I[01]|S:] by FUNCT_2:def 1; A62: 0 <= TT.i by A19,A46; then A63: TT.i in S by A54,XXREAL_1:1; then reconsider Ti = {TT.i} as non empty Subset of I[01] by ZFMISC_1:31 ; A64: the carrier of I[01]|S = S by PRE_TOPC:8; then reconsider Ti2 = Ti as non empty Subset of I[01]|S by A63, ZFMISC_1:31; set FnT = Fn | [:N2,Ti:]; A65: the carrier of [:Y|N2,I[01]|Ti:] = [:the carrier of Y|N2, the carrier of I[01]|Ti:] & rng FnT c= REAL by BORSUK_1:def 2,TOPMETR:17; A66: [:N2,SS:] c= [:N,SS:] by A56,ZFMISC_1:96; A67: the carrier of (Y|N2) = N2 by PRE_TOPC:8; {TT.i} c= S by A63,ZFMISC_1:31; then A68: dom FnT = [:N2,{TT.i}:] by A64,A60,A67,A61,RELAT_1:62,ZFMISC_1:96; A69: [:Y|N2|N7,I[01]|S|Ti2:] = [:Y|N2,I[01]|S:] | [:N7,Ti2:] by BORSUK_3:22; A70: the carrier of I[01]|Ti = Ti by PRE_TOPC:8; then reconsider FnT as Function of [:Y|N2,I[01]|Ti:],R^1 by A67,A68,A65 ,FUNCT_2:2; Y|N2|N7 = Y|N2 & I[01]|S|Ti2 = I[01]|Ti by GOBOARD9:2; then A71: FnT is continuous by A57,A69,TOPMETR:7; A72: Fn. [y,TT.i] in REAL by XREAL_0:def 1; [y,TT.i] in dom F by A6,A63,ZFMISC_1:87; then A73: F. [y,TT.i] in F.:[:N,SS:] by A53,FUNCT_2:35; A74: [y,TT.i] in [:N2,S:] by A55,A63,ZFMISC_1:87; then F. [y,TT.i] = (CircleMap*Fn). [y,TT.i] by A58,FUNCT_1:49 .= CircleMap.(Fn. [y,TT.i]) by A64,A60,A67,A74,FUNCT_2:15; then Fn. [y,TT.i] in (CircleMap)"Ui by A48,A73,FUNCT_2:38,TOPMETR:17,A72; then consider Uit being set such that A75: Fn. [y,TT.i] in Uit and A76: Uit in D by A49,TARSKI:def 4; reconsider Uit as non empty Subset of R^1 by A75,A76; [#]R^1 <> {} & Uit is open by A76,TOPS_2:def 1; then FnT"Uit is open by A71,TOPS_2:43; then consider SF being Subset-Family of [:Y|N2,I[01]|Ti:] such that A77: FnT"Uit = union SF and A78: for e being set st e in SF ex X1 being Subset of Y|N2, Y1 being Subset of I[01]|Ti st e = [:X1,Y1:] & X1 is open & Y1 is open by BORSUK_1:5; A79: TT.i in {TT.i} by TARSKI:def 1; then A80: [y,TT.i] in [:N2,{TT.i}:] by A55,ZFMISC_1:def 2; then FnT. [y,TT.i] in Uit by A75,FUNCT_1:49; then [y,TT.i] in FnT"Uit by A80,A68,FUNCT_1:def 7; then consider N5 being set such that A81: [y,TT.i] in N5 and A82: N5 in SF by A77,TARSKI:def 4; set f = CircleMap|Uit; A83: dom f = Uit by Lm12,RELAT_1:62,TOPMETR:17; A84: rng f c= Ui proof let b be object; assume b in rng f; then consider a being object such that A85: a in dom f and A86: f.a = b by FUNCT_1:def 3; a in union D by A76,A83,A85,TARSKI:def 4; then CircleMap.a in Ui by A49,FUNCT_2:38; hence thesis by A83,A85,A86,FUNCT_1:49; end; consider X1 being Subset of Y|N2, Y1 being Subset of I[01]|Ti such that A87: N5 = [:X1,Y1:] and A88: X1 is open and Y1 is open by A78,A82; the carrier of (R^1 | Uit) = Uit by PRE_TOPC:8; then reconsider f as Function of R^1 | Uit, TUC | Ui by A51,A83,A84, FUNCT_2:2; consider NY being Subset of Y such that A89: NY is open and A90: NY /\ [#](Y|N2) = X1 by A88,TOPS_2:24; consider y1, y2 being object such that A91: y1 in X1 and A92: y2 in Y1 and A93: [y,TT.i] = [y1,y2] by A81,A87,ZFMISC_1:def 2; set N1 = NY /\ N2; y = y1 by A93,XTUPLE_0:1; then A94: y in NY by A90,A91,XBOOLE_0:def 4; then reconsider N1 as non empty open Subset of Y by A55,A89, XBOOLE_0:def 4; A95: N1 c= N2 by XBOOLE_1:17; then [:N1,SS:] c= [:N2,SS:] by ZFMISC_1:96; then [:N1,SS:] c= [:N,SS:] by A66; then A96: F.:[:N1,SS:] c= F.:[:N,SS:] by RELAT_1:123; TT.(i+1) <= 1 by A19,A32,A46; then reconsider SS as non empty Subset of I[01] by A25,A62,A52, XXREAL_1:1; A97: dom (F| [:N1,SS:]) = [:N1,SS:] by A6,RELAT_1:62,ZFMISC_1:96; set Fni1 = f"*(F| [:N1,SS:]); f" is being_homeomorphism by A50,A76,TOPS_2:56; then A98: dom (f") = [#](TUC | Ui); A99: rng (F| [:N1,SS:]) c= dom (f") proof let b be object; assume b in rng (F| [:N1,SS:]); then consider a being object such that A100: a in dom (F| [:N1,SS:]) and A101: (F| [:N1,SS:]).a = b by FUNCT_1:def 3; b = F.a by A97,A100,A101,FUNCT_1:49; then b in F.:[:N1,SS:] by A97,A100,FUNCT_2:35; then b in F.:[:N,SS:] by A96; then b in Ui by A48; hence thesis by A98,PRE_TOPC:8; end; then A102: dom Fni1 = dom (F| [:N1,SS:]) by RELAT_1:27; set Fn2 = Fn | [:N1,S:]; A103: the carrier of (Y|N1) = N1 by PRE_TOPC:8; then A104: [:N1,S:] = the carrier of [:Y|N1,I[01]|S:] by A64,BORSUK_1:def 2; then A105: dom Fn2 = the carrier of [:Y|N1,I[01]|S:] by A64,A60,A67,A61,A95, RELAT_1:62,ZFMISC_1:96; reconsider ff = f as Function; A106: f is being_homeomorphism by A50,A76; then A107: f is one-to-one; A108: rng Fn2 c= R; the carrier of (R^1 | Uit) is Subset of R^1 by TSEP_1:1; then A109: rng Fni1 c= R by XBOOLE_1:1; A110: the carrier of (I[01]|SS) = SS by PRE_TOPC:8; then A111: [:N1,SS:] = the carrier of [:Y|N1,I[01]|SS:] by A103,BORSUK_1:def 2; then reconsider Fni1 as Function of [:Y|N1,I[01]|SS:], R^1 by A97,A102,A109,FUNCT_2:2; set Fn1 = Fn2 +* Fni1; reconsider Fn2 as Function of [:Y|N1,I[01]|S:],R^1 by A105,A108, FUNCT_2:2; A112: rng Fn1 c= rng (Fn | [:N1,S:]) \/ rng Fni1 by FUNCT_4:17; dom (Fn | [:N1,S:]) = [:N1,S:] by A64,A60,A67,A61,A95,RELAT_1:62 ,ZFMISC_1:96; then A113: dom Fn1 = [:N1,S:] \/ [:N1,SS:] by A97,A102,FUNCT_4:def 1; A114: rng f = [#](TUC | Ui) by A106; then f is onto; then A115: f" = ff" by A107,TOPS_2:def 4; A116: Y1 = Ti proof thus Y1 c= Ti by A70; let a be object; assume a in Ti; then a = TT.i by TARSKI:def 1; hence thesis by A92,A93,XTUPLE_0:1; end; A117: Fn.:[:N1,{TT.i}:] c= Uit proof let b be object; assume b in Fn.:[:N1,{TT.i}:]; then consider a being Point of [:Y|N2,I[01]|S:] such that A118: a in [:N1,{TT.i}:] and A119: Fn.a = b by FUNCT_2:65; a in N5 by A87,A90,A116,A118,PRE_TOPC:def 5; then A120: a in union SF by A82,TARSKI:def 4; then a in dom FnT by A77,FUNCT_1:def 7; then Fn.a = FnT.a by FUNCT_1:47; hence thesis by A77,A119,A120,FUNCT_1:def 7; end; A121: for p being set st p in ([#][:Y|N1,I[01]|S:]) /\ [#][:Y|N1,I[01] |SS:] holds Fn2.p = Fni1.p proof A122: the carrier of (Y|N2) = N2 by PRE_TOPC:8; let p be set such that A123: p in ([#][:Y|N1,I[01]|S:]) /\ [#][:Y|N1,I[01]|SS:]; A124: p in ([#][:Y|N1,I[01]|SS:]) /\ [#][:Y|N1,I[01]|S:] by A123; then A125: Fn.p = Fn2.p by A104,FUNCT_1:49; [:N1,S:] /\ [:N1,SS:] = [:N1,S /\ SS:] by ZFMISC_1:99; then A126: p in [:N1,{TT.i}:] by A54,A62,A52,A111,A104,A123,XXREAL_1:418; then consider p1 being Element of N1, p2 being Element of {TT.i} such that A127: p = [p1,p2] by DOMAIN_1:1; A128: p1 in N1; S /\ SS = {TT.i} by A54,A62,A52,XXREAL_1:418; then p2 in S by XBOOLE_0:def 4; then A129: p in [:N2,S:] by A95,A127,A128,ZFMISC_1:def 2; then A130: Fn.p in Fn.:[:N1,{TT.i}:] by A64,A60,A67,A126,FUNCT_2:35; (F| [:N1,SS:]).p = F.p by A111,A123,FUNCT_1:49 .= (F | [:N2,S:]).p by A129,FUNCT_1:49 .= CircleMap.(Fn.p) by A58,A64,A60,A61,A122,A129,FUNCT_1:13 .= (CircleMap|Uit).(Fn.p) by A117,A130,FUNCT_1:49 .= ff.(Fn2.p) by A104,A124,FUNCT_1:49; hence Fn2.p = ff".((F| [:N1,SS:]).p) by A117,A83,A107,A125,A130, FUNCT_1:32 .= Fni1.p by A115,A97,A111,A123,FUNCT_1:13; end; A131: [:N1,S:] c= [:N2,S:] by A95,ZFMISC_1:96; then reconsider K0 = [:N1,S:] as Subset of [:Y|N2,I[01]|S:] by A64,A60,PRE_TOPC:8; A132: [:N1,SS:] c= dom F by A6,ZFMISC_1:96; reconsider gF = F| [:N1,SS:] as Function of [:Y|N1,I[01]|SS:], TUC by A97,A99,A111,FUNCT_2:2; reconsider fF = F| [:N1,SS:] as Function of [:Y|N1,I[01]|SS:], TUC | Ui by A98,A97,A99,A111,FUNCT_2:2; [:Y|N1,I[01]|SS:] = [:Y,I[01]:] | [:N1,SS:] by BORSUK_3:22; then gF is continuous by A3,TOPMETR:7; then A133: fF is continuous by TOPMETR:6; f" is continuous by A106; then f"*fF is continuous by A133; then A134: Fni1 is continuous by PRE_TOPC:26; reconsider aN1 = N1 as non empty Subset of Y|N2 by A95,PRE_TOPC:8; S c= S; then reconsider aS = S as non empty Subset of I[01]|S by PRE_TOPC:8; [:Y|N2,I[01]|S:] | K0 = [:Y|N2|aN1,I[01]|S|aS:] by BORSUK_3:22 .= [:Y|N1,I[01]|S|aS:] by GOBOARD9:2 .= [:Y|N1,I[01]|S:] by GOBOARD9:2; then A135: Fn2 is continuous by A57,TOPMETR:7; take N1; take S1 = S \/ SS; A136: [:N1,S:] \/ [:N1,SS:] = [:N1,S1:] by ZFMISC_1:97; A137: the carrier of (I[01]|S1) = S1 by PRE_TOPC:8; then [:N1,S1:] = the carrier of [:Y|N1,I[01]|S1:] by A103, BORSUK_1:def 2; then reconsider Fn1 as Function of [:Y|N1,I[01]|S1:], R^1 by A136,A113 ,A112,FUNCT_2:2,XBOOLE_1:1; take Fn1; thus A138: S1 = [.0,TT.(i+1).] by A54,A62,A52,XXREAL_1:165; 0 <= TT.(i+1) by A19,A32; then 0 in S1 by A138,XXREAL_1:1; then A139: {0} c= S1 by ZFMISC_1:31; A140: dom (Fn1 | [:the carrier of Y,{0}:]) = dom Fn1 /\ [:the carrier of Y,{0}:] by RELAT_1:61; then A141: dom (Fn1 | [:the carrier of Y,{0}:]) = [:N1 /\ the carrier of Y, S1 /\ {0}:] by A136,A113,ZFMISC_1:100 .= [:N1,S1 /\ {0}:] by XBOOLE_1:28 .= [:N1,{0}:] by A139,XBOOLE_1:28; A142: for a being object st a in dom (Fn1 | [:the carrier of Y,{0}:]) holds (Fn1 | [:the carrier of Y,{0}:]).a = (Ft | [:N1,I:]).a proof let a be object; A143: [:N1,I:] c= [:N2,I:] by A95,ZFMISC_1:96; assume A144: a in dom (Fn1 | [:the carrier of Y,{0}:]); then A145: a in [:the carrier of Y,{0}:] by A140,XBOOLE_0:def 4; then consider a1, a2 being object such that a1 in the carrier of Y and A146: a2 in {0} and A147: a = [a1,a2] by ZFMISC_1:def 2; A148: a2 = 0 by A146,TARSKI:def 1; 0 in S by A54,A62,XXREAL_1:1; then {0} c= S by ZFMISC_1:31; then A149: [:N1,{0}:] c= [:N1,S:] by ZFMISC_1:96; then A150: a in [:N1,S:] by A141,A144; A151: [:N1,S:] c= [:N1,I:] by ZFMISC_1:96; then A152: a in [:N1,I:] by A150; per cases; suppose A153: not a in dom Fni1; thus (Fn1 | [:the carrier of Y,{0}:]).a = Fn1.a by A145,FUNCT_1:49 .= (Fn | [:N1,S:]).a by A153,FUNCT_4:11 .= Fn.a by A141,A144,A149,FUNCT_1:49 .= (Ft | [:N2,I:]).a by A59,A145,FUNCT_1:49 .= Ft.a by A152,A143,FUNCT_1:49 .= (Ft | [:N1,I:]).a by A150,A151,FUNCT_1:49; end; suppose A154: a in dom Fni1; set e = (Ft | [:N1,I:]).a; a in [:N1,SS:] by A6,A102,A154,RELAT_1:62,ZFMISC_1:96; then consider b1, b2 being object such that A155: b1 in N1 and A156: b2 in SS and A157: a = [b1,b2] by ZFMISC_1:def 2; a2 = b2 by A147,A157,XTUPLE_0:1; then A158: a2 = TT.i by A62,A148,A156,XXREAL_1:1; a1 = b1 by A147,A157,XTUPLE_0:1; then A159: [a1,TT.i] in [:N1,S:] & [a1,TT.i] in [:N1,{TT.i}:] by A63,A79,A155, ZFMISC_1:87; e = Ft.a by A150,A151,FUNCT_1:49 .= (Ft | [:N2,I:]).a by A152,A143,FUNCT_1:49 .= Fn.a by A59,A145,FUNCT_1:49; then A160: e in Fn.:[:N1,{TT.i}:] by A64,A60,A67,A61,A131,A147,A158,A159, FUNCT_1:def 6; then A161: ff.e = CircleMap.e by A117,FUNCT_1:49 .= CircleMap.(Ft.a) by A150,A151,FUNCT_1:49 .= (CircleMap*Ft).a by A8,A145,FUNCT_1:13 .= F.a by A5,A145,FUNCT_1:49; thus (Fn1 | [:the carrier of Y,{0}:]).a = Fn1.a by A145,FUNCT_1:49 .= Fni1.a by A154,FUNCT_4:13 .= ff".((F| [:N1,SS:]).a) by A115,A102,A154,FUNCT_1:13 .= ff".(F.a) by A97,A102,A154,FUNCT_1:49 .= (Ft | [:N1,I:]).a by A117,A83,A107,A160,A161,FUNCT_1:32; end; end; A162: rng Fn1 c= dom CircleMap by Lm12,TOPMETR:17; then A163: dom (CircleMap*Fn1) = dom Fn1 by RELAT_1:27; A164: for a being object st a in dom (CircleMap*Fn1) holds (CircleMap*Fn1 ).a = F . a proof let a be object such that A165: a in dom (CircleMap*Fn1); per cases; suppose A166: a in dom Fni1; A167: [:N1,SS:] c= [:the carrier of Y,I:] by ZFMISC_1:96; A168: a in [:N1,SS:] by A6,A102,A166,RELAT_1:62,ZFMISC_1:96; then F.a in F.:[:N1,SS:] by A6,A167,FUNCT_1:def 6; then A169: F.a in F.:[:N,SS:] by A96; then a in F"(dom (ff")) by A6,A48,A51,A98,A115,A168,A167, FUNCT_1:def 7; then A170: a in dom (ff"*F) by RELAT_1:147; thus (CircleMap*Fn1).a = CircleMap.(Fn1.a) by A165,FUNCT_2:15 .= CircleMap.(Fni1.a) by A166,FUNCT_4:13 .= CircleMap.(f".((F| [:N1,SS:]).a)) by A102,A166,FUNCT_1:13 .= CircleMap.(f".(F.a)) by A97,A102,A166,FUNCT_1:49 .= CircleMap.((ff"*F).a) by A132,A115,A97,A102,A166,FUNCT_1:13 .= (CircleMap*(ff"*F)).a by A170,FUNCT_1:13 .= (CircleMap*ff"*F).a by RELAT_1:36 .= (CircleMap*ff").(F.a) by A132,A97,A102,A166,FUNCT_1:13 .= F.a by A48,A51,A114,A107,A169,TOPALG_3:2; end; suppose A171: not a in dom Fni1; then A172: a in [:N1,S:] by A97,A102,A113,A163,A165,XBOOLE_0:def 3; thus (CircleMap*Fn1).a = CircleMap.(Fn1.a) by A165,FUNCT_2:15 .= CircleMap.(Fn | [:N1,S:].a) by A171,FUNCT_4:11 .= CircleMap.(Fn.a) by A172,FUNCT_1:49 .= (CircleMap*Fn).a by A64,A60,A67,A131,A172,FUNCT_2:15 .= F.a by A58,A131,A172,FUNCT_1:49; end; end; A173: S c= S1 by XBOOLE_1:7; then A174: [#](I[01]|S1) = the carrier of (I[01]|S1) & I[01]|S is SubSpace of I[01]|S1 by A64,A137,TSEP_1:4; A175: SS c= S1 by XBOOLE_1:7; then reconsider F1 = [#](I[01]|S), F2 = [#](I[01]|SS) as Subset of I[01]|S1 by A137,A173,PRE_TOPC:8; reconsider hS = F1, hSS = F2 as Subset of I[01] by PRE_TOPC:8; hS is closed by A54,BORSUK_4:23,PRE_TOPC:8; then A176: F1 is closed by TSEP_1:8; thus y in N1 by A55,A94,XBOOLE_0:def 4; thus N1 c= N by A56,A95; hSS is closed by BORSUK_4:23,PRE_TOPC:8; then A177: F2 is closed by TSEP_1:8; I[01]|SS is SubSpace of I[01]|S1 by A110,A137,A175,TSEP_1:4; then ex h being Function of [:Y|N1,I[01]|S1:],R^1 st h = Fn2+*Fni1 & h is continuous by A64,A110,A137,A174,A176,A177,A135,A134,A121,TOPALG_3:19; hence Fn1 is continuous; dom Fn1 = dom F /\ [:N1,S1:] by A6,A136,A113,XBOOLE_1:28,ZFMISC_1:96; hence F | [:N1,S1:] = CircleMap*Fn1 by A162,A164,FUNCT_1:46,RELAT_1:27; dom (Ft | [:N1,I:]) = dom Ft /\ [:N1,I:] by RELAT_1:61 .= [:(the carrier of Y) /\ N1,{0} /\ I:] by A8,ZFMISC_1:100 .= [:N1,{0} /\ I:] by XBOOLE_1:28 .= [:N1,{0}:] by Lm3,XBOOLE_1:28; hence thesis by A141,A142; end; end; A178: N[ 0 ] by FINSEQ_3:24; for i being Nat holds N[i] from NAT_1:sch 2(A178,A30); then consider N2 being non empty open Subset of Y, S being non empty Subset of I[01], Fn1 being Function of [:Y|N2,I[01]|S:], R^1 such that A179: S = [.0,TT.len TT.] and A180: y in N2 and A181: N2 c= N and A182: Fn1 is continuous and A183: F | [:N2,S:] = CircleMap*Fn1 and A184: Fn1 | [:the carrier of Y,{0}:] = Ft | [:N2,I:] by A17; Fn1.x in REAL by XREAL_0:def 1; then reconsider z = Fn1.x as Point of R^1 by TOPMETR:17; A185: I[01]|S = I[01] by A12,A179,Lm6,BORSUK_1:40,TSEP_1:3; then reconsider Fn1 as Function of [:Y|N2,I[01]:], R^1; take z, y, t, N2; take Fn1; thus x = [y,t] & z = Fn1.x & y in N2 & Fn1 is continuous & F | [:N2,I:] = CircleMap*Fn1 & Fn1 | [:the carrier of Y,{0}:] = Ft | [:N2,I:] by A10,A12,A179 ,A180,A182,A183,A184,A185,BORSUK_1:40; let H be Function of [:Y|N2,I[01]:], R^1 such that A186: H is continuous and A187: F | [:N2,I:] = CircleMap*H and A188: H | [:the carrier of Y,{0}:] = Ft | [:N2,I:]; defpred M[Nat] means \$1 in dom TT implies ex Z being non empty Subset of I[01] st Z = [.0,TT.\$1.] & Fn1 | [:N2,Z:] = H | [:N2,Z:]; A189: dom Fn1 = the carrier of [:Y|N2,I[01]:] by FUNCT_2:def 1; A190: the carrier of [:Y|N2,I[01]:] = [:the carrier of Y|N2,I:] & the carrier of Y |N2 = N2 by BORSUK_1:def 2,PRE_TOPC:8; A191: dom H = the carrier of [:Y|N2,I[01]:] by FUNCT_2:def 1; A192: for i being Nat st M[i] holds M[i+1] proof let i be Nat such that A193: M[i] and A194: i+1 in dom TT; per cases by A194,TOPREALA:2; suppose A195: i = 0; set Z = [.0,TT.(i+1).]; A196: Z = {0} by A11,A195,XXREAL_1:17; reconsider Z as non empty Subset of I[01] by A11,A195,Lm3,XXREAL_1:17; A197: [:N2,Z:] c= [:N2,I:] by ZFMISC_1:95; then A198: dom (Fn1 | [:N2,Z:]) = [:N2,Z:] by A190,A189,RELAT_1:62; A199: for x being object st x in dom (Fn1 | [:N2,Z:]) holds (Fn1 | [:N2,Z :]).x = (H | [:N2,Z:]).x proof let x be object; A200: [:N2,Z:] c= [:the carrier of Y,Z:] by ZFMISC_1:95; assume A201: x in dom (Fn1 | [:N2,Z:]); hence (Fn1 | [:N2,Z:]).x = Fn1.x by A198,FUNCT_1:49 .= (Fn1 | [:the carrier of Y,{0}:]).x by A196,A198,A201,A200, FUNCT_1:49 .= H.x by A184,A188,A196,A198,A201,A200,FUNCT_1:49 .= (H | [:N2,Z:]).x by A198,A201,FUNCT_1:49; end; take Z; thus Z = [.0,TT.(i+1).]; dom (H | [:N2,Z:]) = [:N2,Z:] by A191,A190,A197,RELAT_1:62; hence thesis by A189,A199,RELAT_1:62; end; suppose A202: i in dom TT; set ZZ = [.TT.i,TT.(i+1).]; A203: 0 <= TT.i by A19,A202; A204: TT.(i+1) <= 1 by A19,A194,A202; then reconsider ZZ as Subset of I[01] by A25,A203; consider Z being non empty Subset of I[01] such that A205: Z = [.0,TT.i.] and A206: Fn1 | [:N2,Z:] = H | [:N2,Z:] by A193,A202; take Z1 = Z \/ ZZ; A207: TT.i < TT.(i+1) by A19,A194,A202; hence Z1 = [.0,TT.(i+1).] by A205,A203,XXREAL_1:165; A208: [:N2,Z1:] c= [:N2,I:] by ZFMISC_1:95; then A209: dom (Fn1 | [:N2,Z1:]) = [:N2,Z1:] by A190,A189,RELAT_1:62; A210: for x being object st x in dom (Fn1 | [:N2,Z1:]) holds (Fn1 | [:N2, Z1:]).x = (H | [:N2,Z1:]).x proof 0 <= TT.(i+1) by A19,A194; then A211: TT.(i+1) is Point of I[01] by A204,BORSUK_1:43; 0 <= TT.i & TT.i <= 1 by A19,A194,A202; then TT.i is Point of I[01] by BORSUK_1:43; then A212: ZZ is connected by A207,A211,BORSUK_4:24; consider Ui being non empty Subset of TUC such that A213: Ui in UL and A214: F.:[:N,ZZ:] c= Ui by A16,A194,A202; consider D being mutually-disjoint open Subset-Family of R^1 such that A215: union D = (CircleMap)"Ui and A216: for d being Subset of R^1 st d in D for f being Function of R^1 | d, TUC | Ui st f = CircleMap|d holds f is being_homeomorphism by A2 ,A213; let x be object such that A217: x in dom (Fn1 | [:N2,Z1:]); consider x1, x2 being object such that A218: x1 in N2 and A219: x2 in Z1 and A220: x = [x1,x2] by A209,A217,ZFMISC_1:def 2; A221: TT.i in ZZ by A207,XXREAL_1:1; then [x1,TT.i] in [:N,ZZ:] by A181,A218,ZFMISC_1:87; then A222: F. [x1,TT.i] in F.:[:N,ZZ:] by FUNCT_2:35; reconsider xy = {x1} as non empty Subset of Y by A218,ZFMISC_1:31; A223: xy c= N2 by A218,ZFMISC_1:31; then reconsider xZZ = [:xy,ZZ:] as Subset of [:Y|N2,I[01]:] by A190, ZFMISC_1:96; A224: dom (H | [:xy,ZZ:]) = [:xy,ZZ:] by A191,A190,A223,RELAT_1:62 ,ZFMISC_1:96; A225: D is Cover of Fn1.:xZZ proof let b be object; A226: [:N,ZZ:] c= [:the carrier of Y,I:] by ZFMISC_1:96; assume b in Fn1.:xZZ; then consider a being Point of [:Y|N2,I[01]:] such that A227: a in xZZ and A228: Fn1.a = b by FUNCT_2:65; xy c= N by A181,A218,ZFMISC_1:31; then [:xy,ZZ:] c= [:N,ZZ:] by ZFMISC_1:95; then a in [:N,ZZ:] by A227; then A229: F.a in F.:[:N,ZZ:] by A6,A226,FUNCT_1:def 6; CircleMap.(Fn1.a) = (CircleMap*Fn1).a by FUNCT_2:15 .= F.a by A12,A179,A183,A190,BORSUK_1:40,FUNCT_1:49; hence b in union D by A214,A215,A228,A229,Lm12,FUNCT_1:def 7 ,TOPMETR:17; end; A230: D is Cover of H.:xZZ proof let b be object; A231: [:N,ZZ:] c= [:the carrier of Y,I:] by ZFMISC_1:96; assume b in H.:xZZ; then consider a being Point of [:Y|N2,I[01]:] such that A232: a in xZZ and A233: H.a = b by FUNCT_2:65; A234: CircleMap.(H.a) = (CircleMap*H).a by FUNCT_2:15 .= F.a by A187,A190,FUNCT_1:49; xy c= N by A181,A218,ZFMISC_1:31; then [:xy,ZZ:] c= [:N,ZZ:] by ZFMISC_1:95; then a in [:N,ZZ:] by A232; then F.a in F.:[:N,ZZ:] by A6,A231,FUNCT_1:def 6; hence b in union D by A214,A215,A233,A234,Lm12,FUNCT_1:def 7 ,TOPMETR:17; end; A235: H. [x1,TT.i] in REAL by XREAL_0:def 1; TT.i in Z by A205,A203,XXREAL_1:1; then A236: [x1,TT.i] in [:N2,Z:] by A218,ZFMISC_1:87; then A237: Fn1. [x1,TT.i] = (Fn1 | [:N2,Z:]). [x1,TT.i] by FUNCT_1:49 .= H. [x1,TT.i] by A206,A236,FUNCT_1:49; A238: [:N2,Z:] c= [:N2,I:] by ZFMISC_1:95; then F. [x1,TT.i] = (CircleMap*H). [x1,TT.i] by A187,A236,FUNCT_1:49 .= CircleMap.(H. [x1,TT.i]) by A191,A190,A236,A238,FUNCT_1:13; then H. [x1,TT.i] in (CircleMap)"Ui by A214,A222,FUNCT_2:38,A235 ,TOPMETR:17; then consider Uith being set such that A239: H. [x1,TT.i] in Uith and A240: Uith in D by A215,TARSKI:def 4; A241: Fn1. [x1,TT.i] in REAL by XREAL_0:def 1; F. [x1,TT.i] = (CircleMap*Fn1). [x1,TT.i] by A12,A179,A183,A236,A238, BORSUK_1:40,FUNCT_1:49 .= CircleMap.(Fn1. [x1,TT.i]) by A190,A189,A236,A238,FUNCT_1:13; then Fn1. [x1,TT.i] in (CircleMap)"Ui by A214,A222,FUNCT_2:38,A241 ,TOPMETR:17; then consider Uit being set such that A242: Fn1. [x1,TT.i] in Uit and A243: Uit in D by A215,TARSKI:def 4; I[01] is SubSpace of I[01] by TSEP_1:2; then A244: [:Y|N2,I[01]:] is SubSpace of [:Y,I[01]:] by BORSUK_3:21; xy is connected by A218; then [:xy,ZZ:] is connected by A212,TOPALG_3:16; then A245: xZZ is connected by A244,CONNSP_1:23; reconsider Uith as non empty Subset of R^1 by A239,A240; A246: x1 in xy by TARSKI:def 1; then A247: [x1,TT.i] in xZZ by A221,ZFMISC_1:87; then H. [x1,TT.i] in H.:xZZ by FUNCT_2:35; then Uith meets H.:xZZ by A239,XBOOLE_0:3; then A248: H.:xZZ c= Uith by A186,A245,A240,A230,TOPALG_3:12,TOPS_2:61; reconsider Uit as non empty Subset of R^1 by A242,A243; set f = CircleMap|Uit; A249: dom f = Uit by Lm12,RELAT_1:62,TOPMETR:17; A250: rng f c= Ui proof let b be object; assume b in rng f; then consider a being object such that A251: a in dom f and A252: f.a = b by FUNCT_1:def 3; a in union D by A243,A249,A251,TARSKI:def 4; then CircleMap.a in Ui by A215,FUNCT_2:38; hence thesis by A249,A251,A252,FUNCT_1:49; end; the carrier of (TUC | Ui) = Ui & the carrier of (R^1 | Uit) = Uit by PRE_TOPC:8; then reconsider f as Function of R^1 | Uit, TUC | Ui by A249,A250, FUNCT_2:2; A253: dom (Fn1 | [:xy,ZZ:]) = [:xy,ZZ:] by A190,A189,A223,RELAT_1:62 ,ZFMISC_1:96; H. [x1,TT.i] in H.:xZZ by A191,A247,FUNCT_1:def 6; then Uit meets Uith by A242,A248,A237,XBOOLE_0:3; then A254: Uit = Uith by A243,A240,TAXONOM2:def 5; A255: rng (H | [:xy,ZZ:]) c= dom f proof let b be object; assume b in rng (H | [:xy,ZZ:]); then consider a being object such that A256: a in dom (H | [:xy,ZZ:]) and A257: (H | [:xy,ZZ:]).a = b by FUNCT_1:def 3; H.a = b by A224,A256,A257,FUNCT_1:49; then b in H.:xZZ by A191,A224,A256,FUNCT_1:def 6; hence thesis by A248,A254,A249; end; Fn1. [x1,TT.i] in Fn1.:xZZ by A247,FUNCT_2:35; then Uit meets Fn1.:xZZ by A242,XBOOLE_0:3; then A258: Fn1.:xZZ c= Uit by A182,A185,A243,A245,A225,TOPALG_3:12,TOPS_2:61; A259: rng (Fn1 | [:xy,ZZ:]) c= dom f proof let b be object; assume b in rng (Fn1 | [:xy,ZZ:]); then consider a being object such that A260: a in dom (Fn1 | [:xy,ZZ:]) and A261: (Fn1 | [:xy,ZZ:]).a = b by FUNCT_1:def 3; Fn1.a = b by A253,A260,A261,FUNCT_1:49; then b in Fn1.:xZZ by A189,A253,A260,FUNCT_1:def 6; hence thesis by A258,A249; end; then A262: dom (f*(Fn1 | [:xy,ZZ:])) = dom (Fn1 | [:xy,ZZ:]) by RELAT_1:27; A263: for x being object st x in dom (f*(Fn1 | [:xy,ZZ:])) holds (f*( Fn1 | [:xy,ZZ:])).x = (f*(H | [:xy,ZZ:])).x proof let x be object such that A264: x in dom (f*(Fn1 | [:xy,ZZ:])); A265: Fn1.x in Fn1.:[:xy,ZZ:] by A189,A253,A262,A264,FUNCT_1:def 6; A266: H.x in H.:[:xy,ZZ:] by A191,A253,A262,A264,FUNCT_1:def 6; thus (f*(Fn1 | [:xy,ZZ:])).x = ((f*Fn1) | [:xy,ZZ:]).x by RELAT_1:83 .= (f*Fn1).x by A253,A262,A264,FUNCT_1:49 .= f.(Fn1.x) by A189,A264,FUNCT_1:13 .= CircleMap.(Fn1.x) by A258,A265,FUNCT_1:49 .= (CircleMap*Fn1).x by A189,A264,FUNCT_1:13 .= CircleMap.(H.x) by A12,A179,A183,A187,A191,A264,BORSUK_1:40 ,FUNCT_1:13 .= f.(H.x) by A248,A254,A266,FUNCT_1:49 .= (f*H).x by A191,A264,FUNCT_1:13 .= ((f*H) | [:xy,ZZ:]).x by A253,A262,A264,FUNCT_1:49 .= (f*(H | [:xy,ZZ:])).x by RELAT_1:83; end; f is being_homeomorphism by A216,A243; then A267: f is one-to-one; dom (f*(H | [:xy,ZZ:])) = dom (H | [:xy,ZZ:]) by A255,RELAT_1:27; then A268: f*(Fn1 | [:xy,ZZ:]) = f*(H | [:xy,ZZ:]) by A253,A224,A259,A263, RELAT_1:27; per cases; suppose x2 in ZZ; then A269: x in [:xy,ZZ:] by A220,A246,ZFMISC_1:87; thus (Fn1 | [:N2,Z1:]).x = Fn1.x by A209,A217,FUNCT_1:49 .= (Fn1 | [:xy,ZZ:]).x by A269,FUNCT_1:49 .= (H | [:xy,ZZ:]).x by A267,A253,A224,A259,A255,A268,FUNCT_1:27 .= H.x by A269,FUNCT_1:49 .= (H | [:N2,Z1:]).x by A209,A217,FUNCT_1:49; end; suppose not x2 in ZZ; then x2 in Z by A219,XBOOLE_0:def 3; then A270: x in [:N2,Z:] by A218,A220,ZFMISC_1:87; thus (Fn1 | [:N2,Z1:]).x = Fn1.x by A209,A217,FUNCT_1:49 .= (Fn1 | [:N2,Z:]).x by A270,FUNCT_1:49 .= H.x by A206,A270,FUNCT_1:49 .= (H | [:N2,Z1:]).x by A209,A217,FUNCT_1:49; end; end; dom (H | [:N2,Z1:]) = [:N2,Z1:] by A191,A190,A208,RELAT_1:62; hence thesis by A189,A210,RELAT_1:62; end; end; A271: M[ 0 ] by FINSEQ_3:24; for i being Nat holds M[i] from NAT_1:sch 2(A271,A192); then consider Z being non empty Subset of I[01] such that A272: Z = [.0,TT.len TT.] and A273: Fn1 | [:N2,Z:] = H | [:N2,Z:] by A17; thus Fn1 = Fn1 | [:N2,Z:] by A12,A190,A189,A272,BORSUK_1:40,RELAT_1:69 .= H by A12,A191,A190,A272,A273,BORSUK_1:40,RELAT_1:69; end; consider G being Function of [:Y,I[01]:],R^1 such that A274: for x being Point of [:Y,I[01]:] holds A[x,G.x] from FUNCT_2:sch 3 (A9 ); take G; A275: now let N be Subset of Y, F be Function of [:Y|N,I[01]:],R^1; thus dom F = the carrier of [:Y|N,I[01]:] by FUNCT_2:def 1 .= [:the carrier of Y|N,I:] by BORSUK_1:def 2 .= [:N,I:] by PRE_TOPC:8; end; A276: for p being Point of [:Y,I[01]:], y being Point of Y, t being Point of I[01], N1, N2 being non empty open Subset of Y, Fn1 being Function of [:Y|N1, I[01]:],R^1, Fn2 being Function of [:Y|N2,I[01]:],R^1 st p = [y,t] & y in N1 & y in N2 & Fn2 is continuous & Fn1 is continuous & F | [:N2,I:] = CircleMap*Fn2 & Fn2 | [:the carrier of Y,{0}:] = Ft | [:N2,I:] & F | [:N1,I:] = CircleMap*Fn1 & Fn1 | [:the carrier of Y,{0}:] = Ft | [:N1,I:] holds Fn1 | [:{y},I:] = Fn2 | [:{y},I:] proof let p be Point of [:Y,I[01]:], y be Point of Y, t be Point of I[01], N1, N2 be non empty open Subset of Y, Fn1 be Function of [:Y|N1,I[01]:],R^1, Fn2 be Function of [:Y|N2,I[01]:],R^1 such that p = [y,t] and A277: y in N1 and A278: y in N2 and A279: Fn2 is continuous and A280: Fn1 is continuous and A281: F | [:N2,I:] = CircleMap*Fn2 and A282: Fn2 | [:the carrier of Y,{0}:] = Ft | [:N2,I:] and A283: F | [:N1,I:] = CircleMap*Fn1 and A284: Fn1 | [:the carrier of Y,{0}:] = Ft | [:N1,I:]; A285: {y} c= N1 by A277,ZFMISC_1:31; consider TT being non empty FinSequence of REAL such that A286: TT.1 = 0 and A287: TT.len TT = 1 and A288: TT is increasing and A289: ex N being open Subset of Y st y in N & for i being Nat st i in dom TT & i+1 in dom TT ex Ui being non empty Subset of Tunit_circle(2) st Ui in UL & F.:[:N,[.TT.i,TT.(i+1).]:] c= Ui by A3,A1,Th21; consider N being open Subset of Y such that A290: y in N and A291: for i being Nat st i in dom TT & i+1 in dom TT ex Ui being non empty Subset of Tunit_circle(2) st Ui in UL & F.:[:N,[.TT.i,TT.(i+1) .]:] c= Ui by A289; reconsider N as non empty open Subset of Y by A290; defpred M[Nat] means \$1 in dom TT implies ex Z being non empty Subset of I[01] st Z = [.0,TT.\$1.] & Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:]; A292: len TT in dom TT by FINSEQ_5:6; A293: dom Fn2 = the carrier of [:Y|N2,I[01]:] by FUNCT_2:def 1; A294: dom Fn2 = [:N2,I:] by A275; A295: {y} c= N2 by A278,ZFMISC_1:31; A296: the carrier of [:Y|N1,I[01]:] = [:the carrier of Y|N1,I:] & the carrier of Y |N1 = N1 by BORSUK_1:def 2,PRE_TOPC:8; A297: the carrier of [:Y|N2,I[01]:] = [:the carrier of Y|N2,I:] & the carrier of Y |N2 = N2 by BORSUK_1:def 2,PRE_TOPC:8; A298: dom Fn1 = [:N1,I:] by A275; A299: dom Fn1 = the carrier of [:Y|N1,I[01]:] by FUNCT_2:def 1; A300: 1 in dom TT by FINSEQ_5:6; A301: for i being Nat st M[i] holds M[i+1] proof let i be Nat such that A302: M[i] and A303: i+1 in dom TT; per cases by A303,TOPREALA:2; suppose A304: i = 0; set Z = [.0,TT.(i+1).]; A305: Z = {0} by A286,A304,XXREAL_1:17; reconsider Z as non empty Subset of I[01] by A286,A304,Lm3,XXREAL_1:17; A306: [:{y},Z:] c= [:N2,I:] by A295,ZFMISC_1:96; A307: dom (Fn1 | [:{y},Z:]) = [:{y},Z:] by A285,A298,RELAT_1:62,ZFMISC_1:96; A308: [:{y},Z:] c= [:N1,I:] by A285,ZFMISC_1:96; A309: for x being object st x in dom (Fn1 | [:{y},Z:]) holds (Fn1 | [:{y} ,Z:]).x = (Fn2 | [:{y},Z:]).x proof let x be object; A310: [:{y},Z:] c= [:the carrier of Y,Z:] by ZFMISC_1:95; assume A311: x in dom (Fn1 | [:{y},Z:]); hence (Fn1 | [:{y},Z:]).x = Fn1.x by A307,FUNCT_1:49 .= (Fn1 | [:the carrier of Y,{0}:]).x by A305,A307,A311,A310, FUNCT_1:49 .= Ft.x by A284,A308,A307,A311,FUNCT_1:49 .= (Ft | [:N2,I:]).x by A307,A306,A311,FUNCT_1:49 .= Fn2.x by A282,A305,A307,A311,A310,FUNCT_1:49 .= (Fn2 | [:{y},Z:]).x by A307,A311,FUNCT_1:49; end; take Z; thus Z = [.0,TT.(i+1).]; dom (Fn2 | [:{y},Z:]) = [:{y},Z:] by A295,A294,RELAT_1:62,ZFMISC_1:96; hence thesis by A307,A309; end; suppose A312: i in dom TT; A313: now let i be Element of NAT such that A314: i in dom TT; 1 <= i by A314,FINSEQ_3:25; then 1 = i or 1 < i by XXREAL_0:1; hence A315: 0 <= TT.i by A286,A288,A300,A314,SEQM_3:def 1; assume A316: i+1 in dom TT; A317: i+0 < i+1 by XREAL_1:8; hence A318: TT.i < TT.(i+1) by A288,A314,A316,SEQM_3:def 1; i+1 <= len TT by A316,FINSEQ_3:25; then i+1 = len TT or i+1 < len TT by XXREAL_0:1; hence TT.(i+1) <= 1 by A287,A288,A292,A316,SEQM_3:def 1; hence TT.i < 1 by A318,XXREAL_0:2; thus 0 < TT.(i+1) by A288,A314,A315,A316,A317,SEQM_3:def 1; end; then A319: 0 <= TT.i by A312; A320: TT.(i+1) <= 1 by A303,A312,A313; set ZZ = [.TT.i,TT.(i+1).]; consider Z being non empty Subset of I[01] such that A321: Z = [.0,TT.i.] and A322: Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:] by A302,A312; now let i be Nat such that A323: 0 <= TT.i and A324: TT.(i+1) <= 1; thus [.TT.i,TT.(i+1).] c= I proof let a be object; assume A325: a in [.TT.i,TT.(i+1).]; then reconsider a as Real; a <= TT.(i+1) by A325,XXREAL_1:1; then A326: a <= 1 by A324,XXREAL_0:2; 0 <= a by A323,A325,XXREAL_1:1; hence thesis by A326,BORSUK_1:43; end; end; then reconsider ZZ as Subset of I[01] by A319,A320; take Z1 = Z \/ ZZ; A327: TT.i < TT.(i+1) by A303,A312,A313; hence Z1 = [.0,TT.(i+1).] by A321,A319,XXREAL_1:165; A328: dom (Fn1 | [:{y},Z1:]) = [:{y},Z1:] by A285,A298,RELAT_1:62,ZFMISC_1:96 ; A329: for x being object st x in dom (Fn1 | [:{y},Z1:]) holds (Fn1 | [:{y },Z1:]).x = (Fn2 | [:{y},Z1:]).x proof 0 <= TT.(i+1) by A303,A313; then A330: TT.(i+1) is Point of I[01] by A320,BORSUK_1:43; 0 <= TT.i & TT.i <= 1 by A303,A312,A313; then TT.i is Point of I[01] by BORSUK_1:43; then A331: ZZ is connected by A327,A330,BORSUK_4:24; A332: TT.i in ZZ by A327,XXREAL_1:1; consider Ui being non empty Subset of TUC such that A333: Ui in UL and A334: F.:[:N,ZZ:] c= Ui by A291,A303,A312; consider D being mutually-disjoint open Subset-Family of R^1 such that A335: union D = (CircleMap)"Ui and A336: for d being Subset of R^1 st d in D for f being Function of R^1 | d, TUC | Ui st f = CircleMap|d holds f is being_homeomorphism by A2 ,A333; let x be object such that A337: x in dom (Fn1 | [:{y},Z1:]); consider x1, x2 being object such that A338: x1 in {y} and A339: x2 in Z1 and A340: x = [x1,x2] by A328,A337,ZFMISC_1:def 2; reconsider xy = {x1} as non empty Subset of Y by A338,ZFMISC_1:31; A341: xy c= N2 by A295,A338,ZFMISC_1:31; then A342: [:xy,ZZ:] c= [:N2,I:] by ZFMISC_1:96; A343: x1 = y by A338,TARSKI:def 1; then [x1,TT.i] in [:N,ZZ:] by A290,A332,ZFMISC_1:87; then A344: F. [x1,TT.i] in F.:[:N,ZZ:] by FUNCT_2:35; A345: xy c= N1 by A285,A338,ZFMISC_1:31; then reconsider xZZ = [:xy,ZZ:] as Subset of [:Y|N1,I[01]:] by A296, ZFMISC_1:96; xy is connected by A338; then A346: [:xy,ZZ:] is connected by A331,TOPALG_3:16; A347: xy c= N by A290,A343,ZFMISC_1:31; A348: D is Cover of Fn1.:xZZ proof let b be object; A349: [:N,ZZ:] c= [:the carrier of Y,I:] by ZFMISC_1:96; assume b in Fn1.:xZZ; then consider a being Point of [:Y|N1,I[01]:] such that A350: a in xZZ and A351: Fn1.a = b by FUNCT_2:65; A352: CircleMap.(Fn1.a) = (CircleMap*Fn1).a by FUNCT_2:15 .= F.a by A283,A296,FUNCT_1:49; [:xy,ZZ:] c= [:N,ZZ:] by A347,ZFMISC_1:95; then a in [:N,ZZ:] by A350; then F.a in F.:[:N,ZZ:] by A6,A349,FUNCT_1:def 6; hence b in union D by A334,A335,A351,A352,Lm12,FUNCT_1:def 7 ,TOPMETR:17; end; A353: I[01] is SubSpace of I[01] by TSEP_1:2; then [:Y|N1,I[01]:] is SubSpace of [:Y,I[01]:] by BORSUK_3:21; then A354: xZZ is connected by A346,CONNSP_1:23; reconsider XZZ = [:xy,ZZ:] as Subset of [:Y|N2,I[01]:] by A297,A341, ZFMISC_1:96; [:Y|N2,I[01]:] is SubSpace of [:Y,I[01]:] by A353,BORSUK_3:21; then A355: XZZ is connected by A346,CONNSP_1:23; A356: D is Cover of Fn2.:xZZ proof let b be object; A357: [:N,ZZ:] c= [:the carrier of Y,I:] by ZFMISC_1:96; assume b in Fn2.:xZZ; then consider a being Point of [:Y|N2,I[01]:] such that A358: a in xZZ and A359: Fn2.a = b by FUNCT_2:65; A360: CircleMap.(Fn2.a) = (CircleMap*Fn2).a by FUNCT_2:15 .= F.a by A281,A297,FUNCT_1:49; [:xy,ZZ:] c= [:N,ZZ:] by A347,ZFMISC_1:95; then a in [:N,ZZ:] by A358; then F.a in F.:[:N,ZZ:] by A6,A357,FUNCT_1:def 6; hence b in union D by A334,A335,A359,A360,Lm12,FUNCT_1:def 7 ,TOPMETR:17; end; A361: TT.i in Z by A321,A319,XXREAL_1:1; then A362: [x1,TT.i] in [:{y},Z:] by A338,ZFMISC_1:87; A363: Fn1. [x1,TT.i] in REAL by XREAL_0:def 1; A364: [:{y},Z:] c= [:N1,I:] by A285,ZFMISC_1:96; then F. [x1,TT.i] = (CircleMap*Fn1). [x1,TT.i] by A283,A362, FUNCT_1:49 .= CircleMap.(Fn1. [x1,TT.i]) by A298,A362,A364,FUNCT_1:13; then Fn1. [x1,TT.i] in (CircleMap)"Ui by A334,A344,FUNCT_2:38,A363 ,TOPMETR:17; then consider Uit being set such that A365: Fn1. [x1,TT.i] in Uit and A366: Uit in D by A335,TARSKI:def 4; reconsider Uit as non empty Subset of R^1 by A365,A366; set f = CircleMap|Uit; A367: dom f = Uit by Lm12,RELAT_1:62,TOPMETR:17; A368: rng f c= Ui proof let b be object; assume b in rng f; then consider a being object such that A369: a in dom f and A370: f.a = b by FUNCT_1:def 3; a in union D by A366,A367,A369,TARSKI:def 4; then CircleMap.a in Ui by A335,FUNCT_2:38; hence thesis by A367,A369,A370,FUNCT_1:49; end; the carrier of (TUC | Ui) = Ui & the carrier of (R^1 | Uit) = Uit by PRE_TOPC:8; then reconsider f as Function of R^1 | Uit, TUC | Ui by A367,A368, FUNCT_2:2; A371: [:N2,Z:] c= [:N2,I:] by ZFMISC_1:95; A372: Fn2. [x1,TT.i] in REAL by XREAL_0:def 1; A373: [x1,TT.i] in [:N2,Z:] by A295,A338,A361,ZFMISC_1:87; then F. [x1,TT.i] = (CircleMap*Fn2). [x1,TT.i] by A281,A371, FUNCT_1:49 .= CircleMap.(Fn2. [x1,TT.i]) by A293,A297,A373,A371,FUNCT_1:13; then Fn2. [x1,TT.i] in (CircleMap)"Ui by A334,A344,FUNCT_2:38,A372 ,TOPMETR:17; then consider Uith being set such that A374: Fn2. [x1,TT.i] in Uith and A375: Uith in D by A335,TARSKI:def 4; reconsider Uith as non empty Subset of R^1 by A374,A375; A376: dom (Fn1 | [:xy,ZZ:]) = [:xy,ZZ:] by A296,A299,A345,RELAT_1:62 ,ZFMISC_1:96; A377: x1 in xy by TARSKI:def 1; then A378: [x1,TT.i] in xZZ by A332,ZFMISC_1:87; then Fn1. [x1,TT.i] in Fn1.:xZZ by FUNCT_2:35; then Uit meets Fn1.:xZZ by A365,XBOOLE_0:3; then A379: Fn1.:xZZ c= Uit by A280,A366,A354,A348,TOPALG_3:12,TOPS_2:61; A380: rng (Fn1 | [:xy,ZZ:]) c= dom f proof let b be object; assume b in rng (Fn1 | [:xy,ZZ:]); then consider a being object such that A381: a in dom (Fn1 | [:xy,ZZ:]) and A382: (Fn1 | [:xy,ZZ:]).a = b by FUNCT_1:def 3; Fn1.a = b by A376,A381,A382,FUNCT_1:49; then b in Fn1.:xZZ by A299,A376,A381,FUNCT_1:def 6; hence thesis by A379,A367; end; then A383: dom (f*(Fn1 | [:xy,ZZ:])) = dom (Fn1 | [:xy,ZZ:]) by RELAT_1:27; [x1,TT.i] in [:xy,ZZ:] by A338,A343,A332,ZFMISC_1:87; then [x1,TT.i] in dom Fn2 by A294,A342; then A384: Fn2. [x1,TT.i] in Fn2.:xZZ by A378,FUNCT_2:35; then Uith meets Fn2.:xZZ by A374,XBOOLE_0:3; then A385: Fn2.:xZZ c= Uith by A279,A375,A355,A356,TOPALG_3:12,TOPS_2:61; Fn1. [x1,TT.i] = (Fn1 | [:{y},Z:]). [x1,TT.i] by A362,FUNCT_1:49 .= Fn2. [x1,TT.i] by A322,A362,FUNCT_1:49; then Uit meets Uith by A365,A384,A385,XBOOLE_0:3; then A386: Uit = Uith by A366,A375,TAXONOM2:def 5; A387: for x being object st x in dom (f*(Fn1 | [:xy,ZZ:])) holds (f*( Fn1 | [:xy,ZZ:])).x = (f*(Fn2 | [:xy,ZZ:])).x proof A388: dom (Fn1 | [:xy,ZZ:]) c= dom Fn1 by RELAT_1:60; let x be object such that A389: x in dom (f*(Fn1 | [:xy,ZZ:])); A390: Fn1.x in Fn1.:[:xy,ZZ:] by A299,A376,A383,A389,FUNCT_1:def 6; A391: Fn2.x in Fn2.:[:xy,ZZ:] by A294,A342,A376,A383,A389,FUNCT_1:def 6; dom (Fn1 | [:xy,ZZ:]) = dom Fn1 /\ [:xy,ZZ:] by RELAT_1:61; then A392: x in [:xy,ZZ:] by A383,A389,XBOOLE_0:def 4; thus (f*(Fn1 | [:xy,ZZ:])).x = ((f*Fn1) | [:xy,ZZ:]).x by RELAT_1:83 .= (f*Fn1).x by A376,A383,A389,FUNCT_1:49 .= f.(Fn1.x) by A299,A389,FUNCT_1:13 .= CircleMap.(Fn1.x) by A379,A390,FUNCT_1:49 .= (CircleMap*Fn1).x by A299,A389,FUNCT_1:13 .= F.x by A283,A298,A383,A389,A388,FUNCT_1:49 .= (CircleMap*Fn2).x by A281,A342,A392,FUNCT_1:49 .= CircleMap.(Fn2.x) by A294,A342,A392,FUNCT_1:13 .= f.(Fn2.x) by A385,A386,A391,FUNCT_1:49 .= (f*Fn2).x by A294,A342,A392,FUNCT_1:13 .= ((f*Fn2) | [:xy,ZZ:]).x by A376,A383,A389,FUNCT_1:49 .= (f*(Fn2 | [:xy,ZZ:])).x by RELAT_1:83; end; A393: dom (Fn2 | [:xy,ZZ:]) = [:xy,ZZ:] by A293,A297,A341,RELAT_1:62 ,ZFMISC_1:96; A394: rng (Fn2 | [:xy,ZZ:]) c= dom f proof let b be object; assume b in rng (Fn2 | [:xy,ZZ:]); then consider a being object such that A395: a in dom (Fn2 | [:xy,ZZ:]) and A396: (Fn2 | [:xy,ZZ:]).a = b by FUNCT_1:def 3; Fn2.a = b by A393,A395,A396,FUNCT_1:49; then b in Fn2.:xZZ by A293,A393,A395,FUNCT_1:def 6; hence thesis by A385,A386,A367; end; then dom (f*(Fn2 | [:xy,ZZ:])) = dom (Fn2 | [:xy,ZZ:]) by RELAT_1:27; then A397: f*(Fn1 | [:xy,ZZ:]) = f*(Fn2 | [:xy,ZZ:]) by A376,A393,A380,A387, RELAT_1:27; f is being_homeomorphism by A336,A366; then A398: f is one-to-one; per cases; suppose x2 in ZZ; then A399: x in [:xy,ZZ:] by A340,A377,ZFMISC_1:87; thus (Fn1 | [:{y},Z1:]).x = Fn1.x by A328,A337,FUNCT_1:49 .= (Fn1 | [:xy,ZZ:]).x by A399,FUNCT_1:49 .= (Fn2 | [:xy,ZZ:]).x by A398,A376,A393,A380,A394,A397, FUNCT_1:27 .= Fn2.x by A399,FUNCT_1:49 .= (Fn2 | [:{y},Z1:]).x by A328,A337,FUNCT_1:49; end; suppose not x2 in ZZ; then x2 in Z by A339,XBOOLE_0:def 3; then A400: x in [:{y},Z:] by A338,A340,ZFMISC_1:87; thus (Fn1 | [:{y},Z1:]).x = Fn1.x by A328,A337,FUNCT_1:49 .= (Fn1 | [:{y},Z:]).x by A400,FUNCT_1:49 .= Fn2.x by A322,A400,FUNCT_1:49 .= (Fn2 | [:{y},Z1:]).x by A328,A337,FUNCT_1:49; end; end; dom (Fn2 | [:{y},Z1:]) = [:{y},Z1:] by A295,A293,A297,RELAT_1:62 ,ZFMISC_1:96; hence thesis by A328,A329; end; end; A401: M[ 0 ] by FINSEQ_3:24; for i being Nat holds M[i] from NAT_1:sch 2(A401,A301); then ex Z being non empty Subset of I[01] st Z = [.0,TT.len TT.] & Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:] by A292; hence thesis by A287,BORSUK_1:40; end; for p being Point of [:Y,I[01]:], V being Subset of R^1 st G.p in V & V is open holds ex W being Subset of [:Y,I[01]:] st p in W & W is open & G.:W c= V proof let p be Point of [:Y,I[01]:], V be Subset of R^1 such that A402: G.p in V & V is open; consider y being Point of Y, t being Point of I[01], N being non empty open Subset of Y, Fn being Function of [:Y|N,I[01]:], R^1 such that A403: p = [y,t] and A404: G.p = Fn.p and A405: y in N and A406: Fn is continuous and A407: F | [:N,I:] = CircleMap*Fn & Fn | [:the carrier of Y,{0}:] = Ft | [:N,I:] and for H being Function of [:Y|N,I[01]:], R^1 st H is continuous & F | [: N,I:] = CircleMap*H & H | [:the carrier of Y,{0}:] = Ft | [:N,I:] holds Fn = H by A274; A408: the carrier of [:Y|N,I[01]:] = [:the carrier of (Y|N),I:] by BORSUK_1:def 2 .= [:N,I:] by PRE_TOPC:8; then p in the carrier of [:Y|N,I[01]:] by A403,A405,ZFMISC_1:87; then consider W being Subset of [:Y|N,I[01]:] such that A409: p in W and A410: W is open and A411: Fn.:W c= V by A402,A404,A406,JGRAPH_2:10; A412: dom Fn = [:N,I:] by A408,FUNCT_2:def 1; A413: [#](Y|N) = N by PRE_TOPC:def 5; then A414: [#][:Y|N,I[01]:] = [:N,[#]I[01]:] by BORSUK_3:1; [:Y|N,I[01]:] = [:Y,I[01]:] | [:N,[#]I[01]:] by Lm7,BORSUK_3:22; then consider C being Subset of [:Y,I[01]:] such that A415: C is open and A416: C /\ [#][:Y|N,I[01]:] = W by A410,TOPS_2:24; take WW = C /\ [:N,[#]I[01]:]; thus p in WW by A409,A416,A413,BORSUK_3:1; [:N,[#]I[01]:] is open by BORSUK_1:6; hence WW is open by A415; let y be object; assume y in G.:WW; then consider x being Point of [:Y,I[01]:] such that A417: x in WW and A418: y = G.x by FUNCT_2:65; consider y0 being Point of Y, t0 being Point of I[01], N0 being non empty open Subset of Y, Fn0 being Function of [:Y|N0,I[01]:], R^1 such that A419: x = [y0,t0] and A420: G.x = Fn0.x and A421: y0 in N0 & Fn0 is continuous & F | [:N0,I:] = CircleMap*Fn0 & Fn0 | [:the carrier of Y,{0}:] = Ft | [:N0,I :] and for H being Function of [:Y|N0,I[01]:], R^1 st H is continuous & F | [:N0,I:] = CircleMap*H & H | [:the carrier of Y,{0}:] = Ft | [:N0,I:] holds Fn0 = H by A274; x in [:N,[#]I[01]:] by A417,XBOOLE_0:def 4; then A422: y0 in N by A419,ZFMISC_1:87; A423: x in [:{y0},I:] by A419,ZFMISC_1:105; then Fn.x = (Fn | [:{y0},I:]).x by FUNCT_1:49 .= (Fn0 | [:{y0},I:]).x by A276,A406,A407,A419,A421,A422 .= Fn0.x by A423,FUNCT_1:49; then y in Fn.:W by A412,A416,A414,A417,A418,A420,FUNCT_1:def 6; hence thesis by A411; end; hence G is continuous by JGRAPH_2:10; for x being Point of [:Y,I[01]:] holds F.x = (CircleMap*G).x proof let x be Point of [:Y,I[01]:]; consider y being Point of Y, t being Point of I[01], N being non empty open Subset of Y, Fn being Function of [:Y|N,I[01]:], R^1 such that A424: x = [y,t] and A425: G.x = Fn.x and A426: y in N and Fn is continuous and A427: F | [:N,I:] = CircleMap*Fn and Fn | [:the carrier of Y,{0}:] = Ft | [:N,I:] and for H being Function of [:Y|N,I[01]:], R^1 st H is continuous & F | [: N,I:] = CircleMap*H & H | [:the carrier of Y,{0}:] = Ft | [:N,I:] holds Fn = H by A274; A428: the carrier of [:Y|N,I[01]:] = [:the carrier of (Y|N),I:] by BORSUK_1:def 2 .= [:N,I:] by PRE_TOPC:8; then A429: x in the carrier of [:Y|N,I[01]:] by A424,A426,ZFMISC_1:87; thus (CircleMap*G).x = CircleMap.(G.x) by FUNCT_2:15 .= (CircleMap*Fn).x by A425,A429,FUNCT_2:15 .= F.x by A427,A428,A429,FUNCT_1:49; end; hence F = CircleMap*G; A430: [:the carrier of Y,{0}:] c= [:the carrier of Y,I:] by Lm3,ZFMISC_1:95; A431: the carrier of [:Y,I[01]:] = [:the carrier of Y,I:] by BORSUK_1:def 2; then A432: dom G = [:the carrier of Y,I:] by FUNCT_2:def 1; A433: for x being object st x in dom Ft holds Ft.x = G.x proof let x be object; assume A434: x in dom Ft; then x in dom G by A8,A432,A430; then consider y being Point of Y, t being Point of I[01], N being non empty open Subset of Y, Fn being Function of [:Y|N,I[01]:], R^1 such that A435: x = [y,t] and A436: G.x = Fn.x and A437: y in N and Fn is continuous and F | [:N,I:] = CircleMap*Fn and A438: Fn | [:the carrier of Y,{0}:] = Ft | [:N,I:] and for H being Function of [:Y|N,I[01]:], R^1 st H is continuous & F | [: N,I:] = CircleMap*H & H | [:the carrier of Y,{0}:] = Ft | [:N,I:] holds Fn = H by A274; x in [:N,I:] by A435,A437,ZFMISC_1:87; hence Ft.x = (Ft | [:N,I:]).x by FUNCT_1:49 .= G.x by A7,A434,A436,A438,Lm14,FUNCT_1:49; end; dom Ft = dom G /\ [:the carrier of Y,{0}:] by A8,A432,A430,XBOOLE_1:28; hence G | [:the carrier of Y,{0}:] = Ft by A433,FUNCT_1:46; let H be Function of [:Y,I[01]:], R^1 such that A439: H is continuous & F = CircleMap*H and A440: H | [:the carrier of Y,{0}:] = Ft; for x being Point of [:Y,I[01]:] holds G.x = H.x proof let x be Point of [:Y,I[01]:]; consider y being Point of Y, t being Point of I[01], N being non empty open Subset of Y, Fn being Function of [:Y|N,I[01]:], R^1 such that A441: x = [y,t] and A442: G.x = Fn.x and A443: y in N and Fn is continuous and F | [:N,I:] = CircleMap*Fn and Fn | [:the carrier of Y,{0}:] = Ft | [:N,I:] and A444: for H being Function of [:Y|N,I[01]:], R^1 st H is continuous & F | [:N,I:] = CircleMap*H & H | [:the carrier of Y,{0}:] = Ft | [:N,I:] holds Fn = H by A274; A445: the carrier of [:Y|N,I[01]:] = [:the carrier of (Y|N),I:] by BORSUK_1:def 2 .= [:N,I:] by PRE_TOPC:8; then A446: x in the carrier of [:Y|N,I[01]:] by A441,A443,ZFMISC_1:87; dom H = the carrier of [:Y,I[01]:] by FUNCT_2:def 1; then [:N,I:] c= dom H by A431,ZFMISC_1:95; then A447: dom (H | [:N,I:]) = [:N,I:] by RELAT_1:62; rng (H | [:N,I:]) c= R; then reconsider H1 = H | [:N,I:] as Function of [:Y|N,I[01]:], R^1 by A445,A447,FUNCT_2:2; A448: H | [:N,I:] | [:the carrier of Y,{0}:] = H | ([:the carrier of Y,{0} :] /\ [:N,I:]) by RELAT_1:71 .= Ft | [:N,I:] by A440,RELAT_1:71; H1 is continuous & F | [:N,I:] = CircleMap*(H| [:N,I:]) by A439,RELAT_1:83 ,TOPALG_3:17; hence G.x = (H| [:N,I:]).x by A442,A444,A448 .= H.x by A445,A446,FUNCT_1:49; end; hence thesis; end; theorem Th23: for x0, y0 being Point of Tunit_circle(2), xt being Point of R^1 , f being Path of x0,y0 st xt in (CircleMap)"{x0} ex ft being Function of I[01] , R^1 st ft.0 = xt & f = CircleMap*ft & ft is continuous & for f1 being Function of I[01], R^1 st f1 is continuous & f = CircleMap*f1 & f1.0 = xt holds ft = f1 proof set Y = 1TopSp{1}; let x0, y0 be Point of TUC; let xt be Point of R^1; let f be Path of x0,y0; deffunc F(set,Element of I) = f.\$2; consider F being Function of [:the carrier of Y,I:], cS1 such that A1: for y being Element of Y, i being Element of I holds F.(y,i) = F(y,i ) from BINOP_1:sch 4; reconsider j = 1 as Point of Y by TARSKI:def 1; A2: [j,j0] in [:the carrier of Y,{0}:] by Lm4,ZFMISC_1:87; A3: the carrier of [:Y,I[01]:] = [:the carrier of Y, I:] by BORSUK_1:def 2; then reconsider F as Function of [:Y,I[01]:], TUC; set Ft = [:Y,Sspace(0[01]):] --> xt; A4: the carrier of [:Y,Sspace(0[01]):] = [:the carrier of Y, the carrier of Sspace(0[01]):] by BORSUK_1:def 2; then A5: for y being Element of Y, i being Element of {0} holds Ft. [y,i] = xt by Lm14,FUNCOP_1:7; A6: [#]Y = the carrier of Y; for p being Point of [:Y,I[01]:], V being Subset of TUC st F.p in V & V is open holds ex W being Subset of [:Y,I[01]:] st p in W & W is open & F.:W c= V proof let p be Point of [:Y,I[01]:], V be Subset of TUC such that A7: F.p in V & V is open; consider p1 being Point of Y, p2 being Point of I[01] such that A8: p = [p1,p2] by BORSUK_1:10; F.(p1,p2) = f.p2 by A1; then consider S being Subset of I[01] such that A9: p2 in S and A10: S is open and A11: f.:S c= V by A7,A8,JGRAPH_2:10; set W = [:{1},S:]; W c= [:the carrier of Y,I:] by ZFMISC_1:95; then reconsider W as Subset of [:Y,I[01]:] by BORSUK_1:def 2; take W; thus p in W by A8,A9,ZFMISC_1:87; thus W is open by A6,A10,BORSUK_1:6; let y be object; assume y in F.:W; then consider x being object such that A12: x in the carrier of [:Y,I[01]:] and A13: x in W and A14: y = F.x by FUNCT_2:64; consider x1 being Point of Y, x2 being Point of I[01] such that A15: x = [x1,x2] by A12,BORSUK_1:10; x2 in S by A13,A15,ZFMISC_1:87; then A16: f.x2 in f.:S by FUNCT_2:35; y = F.(x1,x2) by A14,A15 .= f.x2 by A1; hence thesis by A11,A16; end; then A17: F is continuous by JGRAPH_2:10; assume xt in (CircleMap)"{x0}; then A18: CircleMap.xt in {x0} by FUNCT_2:38; A19: for x being object st x in dom (CircleMap*Ft) holds (F | [:the carrier of Y,{0}:]).x = (CircleMap*Ft).x proof let x be object such that A20: x in dom (CircleMap*Ft); consider x1, x2 being object such that A21: x1 in the carrier of Y and A22: x2 in {0} and A23: x = [x1,x2] by A4,A20,Lm14,ZFMISC_1:def 2; A24: x2 = 0 by A22,TARSKI:def 1; thus (F | [:the carrier of Y,{0}:]).x = F.(x1,x2) by A4,A20,A23,Lm14, FUNCT_1:49 .= f.x2 by A1,A21,A24,Lm2 .= x0 by A24,BORSUK_2:def 4 .= CircleMap.xt by A18,TARSKI:def 1 .= CircleMap.(Ft.x) by A5,A21,A22,A23 .= (CircleMap*Ft).x by A20,FUNCT_1:12; end; A25: dom (CircleMap*Ft) = [:the carrier of Y,{0}:] by A4,Lm14,FUNCT_2:def 1; A26: dom F = the carrier of [:Y,I[01]:] by FUNCT_2:def 1; then A27: [:the carrier of Y,{0}:] c= dom F by A3,Lm3,ZFMISC_1:95; then dom (F | [:the carrier of Y,{0}:]) = [:the carrier of Y,{0}:] by RELAT_1:62; then consider G being Function of [:Y,I[01]:], R^1 such that A28: G is continuous and A29: F = CircleMap*G and A30: G | [:the carrier of Y,{0}:] = Ft and A31: for H being Function of [:Y,I[01]:], R^1 st H is continuous & F = CircleMap*H & H | [:the carrier of Y,{0}:] = Ft holds G = H by A17,A25,A19 ,Th22,FUNCT_1:2; take ft = Prj2(j,G); thus ft.0 = G.(j,j0) by Def3 .= Ft. [j,j0] by A30,A2,FUNCT_1:49 .= xt by A5,Lm4; for i being Point of I[01] holds f.i = (CircleMap*ft).i proof let i be Point of I[01]; A32: the carrier of [:Y,I[01]:] = [:the carrier of Y, the carrier of I[01] :] by BORSUK_1:def 2; thus (CircleMap*ft).i = CircleMap.(ft.i) by FUNCT_2:15 .= CircleMap.(G.(j,i)) by Def3 .= (CircleMap*G).(j,i) by A32,BINOP_1:18 .= f.i by A1,A29; end; hence f = CircleMap*ft; thus ft is continuous by A28; let f1 be Function of I[01], R^1; deffunc H(set,Element of I) = f1.\$2; consider H being Function of [:the carrier of Y,I:], R such that A33: for y being Element of Y, i being Element of I holds H.(y,i) = H(y, i) from BINOP_1:sch 4; reconsider H as Function of [:Y,I[01]:], R^1 by A3; assume that A34: f1 is continuous and A35: f = CircleMap*f1 and A36: f1.0 = xt; for p being Point of [:Y,I[01]:], V being Subset of R^1 st H.p in V & V is open holds ex W being Subset of [:Y,I[01]:] st p in W & W is open & H.:W c= V proof let p be Point of [:Y,I[01]:], V be Subset of R^1 such that A37: H.p in V & V is open; consider p1 being Point of Y, p2 being Point of I[01] such that A38: p = [p1,p2] by BORSUK_1:10; H.p = H.(p1,p2) by A38 .= f1.p2 by A33; then consider W being Subset of I[01] such that A39: p2 in W and A40: W is open and A41: f1.:W c= V by A34,A37,JGRAPH_2:10; take W1 = [:[#]Y,W:]; thus p in W1 by A38,A39,ZFMISC_1:87; thus W1 is open by A40,BORSUK_1:6; let y be object; assume y in H.:W1; then consider c being Element of [:Y,I[01]:] such that A42: c in W1 and A43: y = H.c by FUNCT_2:65; consider c1, c2 being object such that A44: c1 in [#]Y and A45: c2 in W and A46: c = [c1,c2] by A42,ZFMISC_1:def 2; A47: f1.c2 in f1.:W by A45,FUNCT_2:35; H.c = H.(c1,c2) by A46 .= f1.c2 by A33,A44,A45; hence thesis by A41,A43,A47; end; then A48: H is continuous by JGRAPH_2:10; for x being Point of [:Y,I[01]:] holds F.x = (CircleMap*H).x proof let x be Point of [:Y,I[01]:]; consider x1 being Point of Y, x2 being Point of I[01] such that A49: x = [x1,x2] by BORSUK_1:10; thus (CircleMap*H).x = CircleMap.(H.(x1,x2)) by A49,FUNCT_2:15 .= CircleMap.(f1.x2) by A33 .= (CircleMap*f1).x2 by FUNCT_2:15 .= F.(x1,x2) by A1,A35 .= F.x by A49; end; then A50: F = CircleMap*H; for i being Point of I[01] holds ft.i = f1.i proof let i be Point of I[01]; A51: dom H = the carrier of [:Y,I[01]:] by FUNCT_2:def 1; then A52: dom (H | [:the carrier of Y,{0}:]) = [:the carrier of Y,{0}:] by A26,A27, RELAT_1:62; A53: for x being object st x in dom (H | [:the carrier of Y,{0}:]) holds (H | [:the carrier of Y,{0}:]).x = Ft.x proof let x be object; assume A54: x in dom (H | [:the carrier of Y,{0}:]); then consider x1, x2 being object such that A55: x1 in the carrier of Y and A56: x2 in {0} and A57: x = [x1,x2] by A52,ZFMISC_1:def 2; A58: x2 = j0 by A56,TARSKI:def 1; thus (H | [:the carrier of Y,{0}:]).x = H.(x1,x2) by A54,A57,FUNCT_1:47 .= f1.x2 by A33,A55,A58 .= Ft.x by A5,A36,A55,A56,A57,A58; end; dom Ft = [:the carrier of Y,{0}:] by A4,Lm14,FUNCT_2:def 1; then A59: H | [:the carrier of Y,{0}:] = Ft by A26,A27,A51,A53,RELAT_1:62; thus ft.i = G.(j,i) by Def3 .= H.(j,i) by A31,A50,A48,A59 .= f1.i by A33; end; hence thesis; end; theorem Th24: for x0, y0 being Point of Tunit_circle(2), P, Q being Path of x0 ,y0, F being Homotopy of P,Q, xt being Point of R^1 st P,Q are_homotopic & xt in (CircleMap)"{x0} ex yt being Point of R^1, Pt, Qt being Path of xt,yt, Ft being Homotopy of Pt,Qt st Pt,Qt are_homotopic & F = CircleMap*Ft & yt in ( CircleMap)"{y0} & for F1 being Homotopy of Pt,Qt st F = CircleMap*F1 holds Ft = F1 proof let x0, y0 be Point of TUC; let P, Q be Path of x0,y0; let F be Homotopy of P,Q; let xt be Point of R^1; set cP1 = the constant Loop of x0; set g1 = I[01] --> xt; set cP2 = the constant Loop of y0; assume A1: P,Q are_homotopic; then A2: F is continuous by BORSUK_6:def 11; assume A3: xt in (CircleMap)"{x0}; then consider ft being Function of I[01], R^1 such that A4: ft.0 = xt and A5: P = CircleMap*ft and A6: ft is continuous and for f1 being Function of I[01], R^1 st f1 is continuous & P = CircleMap* f1 & f1.0 = xt holds ft = f1 by Th23; defpred P[set,set,set] means \$3 = ft.\$1; A7: for x being Element of I for y being Element of {0} ex z being Element of REAL st P[x,y,z] proof let x be Element of I; ft.x in REAL by XREAL_0:def 1; hence thesis; end; consider Ft being Function of [:I,{0}:], REAL such that A8: for y being Element of I, i being Element of {0} holds P[y,i, Ft.(y ,i)] from BINOP_1:sch 3(A7); CircleMap.xt in {x0} by A3,FUNCT_2:38; then A9: CircleMap.xt = x0 by TARSKI:def 1; A10: for x being Point of I[01] holds cP1.x = (CircleMap*g1).x proof let x be Point of I[01]; thus cP1.x = x0 by TOPALG_3:21 .= CircleMap.(g1.x) by A9,TOPALG_3:4 .= (CircleMap*g1).x by FUNCT_2:15; end; consider ft1 being Function of I[01], R^1 such that ft1.0 = xt and cP1 = CircleMap*ft1 and ft1 is continuous and A11: for f1 being Function of I[01], R^1 st f1 is continuous & cP1 = CircleMap*f1 & f1.0 = xt holds ft1 = f1 by A3,Th23; g1.j0 = xt by TOPALG_3:4; then A12: ft1 = g1 by A11,A10,FUNCT_2:63; A13: rng Ft c= REAL; A14: dom Ft = [:I,{0}:] by FUNCT_2:def 1; A15: the carrier of [:I[01],Sspace(0[01]):] = [:I, the carrier of Sspace( 0[01]):] by BORSUK_1:def 2; then reconsider Ft as Function of [:I[01],Sspace(0[01]):], R^1 by Lm14, TOPMETR:17; A16: for x being object st x in dom (CircleMap*Ft) holds (F | [:I,{0}:]).x = ( CircleMap*Ft).x proof let x be object such that A17: x in dom (CircleMap*Ft); consider x1, x2 being object such that A18: x1 in I and A19: x2 in {0} and A20: x = [x1,x2] by A15,A17,Lm14,ZFMISC_1:def 2; x2 = 0 by A19,TARSKI:def 1; hence (F | [:I,{0}:]).x = F.(x1,0) by A15,A17,A20,Lm14,FUNCT_1:49 .= (CircleMap*ft).x1 by A1,A5,A18,BORSUK_6:def 11 .= CircleMap.(ft.x1) by A18,FUNCT_2:15 .= CircleMap.(Ft.(x1,x2)) by A8,A18,A19 .= (CircleMap*Ft).x by A17,A20,FUNCT_1:12; end; for p being Point of [:I[01],Sspace(0[01]):], V being Subset of R^1 st Ft.p in V & V is open holds ex W being Subset of [:I[01],Sspace(0[01]):] st p in W & W is open & Ft.:W c= V proof let p be Point of [:I[01],Sspace(0[01]):], V be Subset of R^1 such that A21: Ft.p in V & V is open; consider p1 being Point of I[01], p2 being Point of Sspace(0[01]) such that A22: p = [p1,p2] by A15,DOMAIN_1:1; P[p1,p2,Ft.(p1,p2)] by A8,Lm14; then consider W1 being Subset of I[01] such that A23: p1 in W1 and A24: W1 is open and A25: ft.:W1 c= V by A6,A21,A22,JGRAPH_2:10; reconsider W1 as non empty Subset of I[01] by A23; take W = [:W1,[#]Sspace(0[01]):]; thus p in W by A22,A23,ZFMISC_1:def 2; thus W is open by A24,BORSUK_1:6; let y be object; assume y in Ft.:W; then consider x being Element of [:I[01],Sspace(0[01]):] such that A26: x in W and A27: y = Ft.x by FUNCT_2:65; consider x1 being Element of W1, x2 being Point of Sspace(0[01]) such that A28: x = [x1,x2] by A26,DOMAIN_1:1; ( P[x1,x2,Ft.(x1,x2)])& ft.x1 in ft.:W1 by A8,Lm14,FUNCT_2:35; hence thesis by A25,A27,A28; end; then A29: Ft is continuous by JGRAPH_2:10; take yt = ft.j1; A30: [j1,j0] in [:I,{0}:] by Lm4,ZFMISC_1:87; reconsider ft as Path of xt,yt by A4,A6,BORSUK_2:def 4; A31: [j0,j0] in [:I,{0}:] by Lm4,ZFMISC_1:87; A32: dom F = the carrier of [:I[01],I[01]:] by FUNCT_2:def 1; then A33: [:I,{0}:] c= dom F by Lm3,Lm5,ZFMISC_1:95; then dom (F | [:I,{0}:]) = [:I,{0}:] by RELAT_1:62; then F | [:I,{0}:] = CircleMap*Ft by A14,A13,A16,Lm12,FUNCT_1:2,RELAT_1:27; then consider G being Function of [:I[01],I[01]:], R^1 such that A34: G is continuous and A35: F = CircleMap*G and A36: G | [:I,{0}:] = Ft and A37: for H being Function of [:I[01],I[01]:], R^1 st H is continuous & F = CircleMap*H & H | [:the carrier of I[01],{0}:] = Ft holds G = H by A2,A29 ,Th22; set sM0 = Prj2(j0,G); A38: for x being Point of I[01] holds cP1.x = (CircleMap*sM0).x proof let x be Point of I[01]; thus (CircleMap*sM0).x = CircleMap.(sM0.x) by FUNCT_2:15 .= CircleMap.(G.(j0,x)) by Def3 .= (CircleMap*G).(j0,x) by Lm5,BINOP_1:18 .= x0 by A1,A35,BORSUK_6:def 11 .= cP1.x by TOPALG_3:21; end; set g2 = I[01] --> yt; A39: CircleMap.yt = P.j1 by A5,FUNCT_2:15 .= y0 by BORSUK_2:def 4; A40: for x being Point of I[01] holds cP2.x = (CircleMap*g2).x proof let x be Point of I[01]; thus cP2.x = y0 by TOPALG_3:21 .= CircleMap.(g2.x) by A39,TOPALG_3:4 .= (CircleMap*g2).x by FUNCT_2:15; end; A41: CircleMap.yt in {y0} by A39,TARSKI:def 1; then yt in (CircleMap)"{y0} by FUNCT_2:38; then consider ft2 being Function of I[01], R^1 such that ft2.0 = yt and cP2 = CircleMap*ft2 and ft2 is continuous and A42: for f1 being Function of I[01], R^1 st f1 is continuous & cP2 = CircleMap*f1 & f1.0 = yt holds ft2 = f1 by Th23; g2.j0 = yt by TOPALG_3:4; then A43: ft2 = g2 by A42,A40,FUNCT_2:63; set sM1 = Prj2(j1,G); A44: for x being Point of I[01] holds cP2.x = (CircleMap*sM1).x proof let x be Point of I[01]; thus (CircleMap*sM1).x = CircleMap.(sM1.x) by FUNCT_2:15 .= CircleMap.(G.(j1,x)) by Def3 .= (CircleMap*G).(j1,x) by Lm5,BINOP_1:18 .= y0 by A1,A35,BORSUK_6:def 11 .= cP2.x by TOPALG_3:21; end; sM1.0 = G.(j1,j0) by Def3 .= Ft.(j1,j0) by A36,A30,FUNCT_1:49 .= yt by A8,Lm4; then A45: ft2 = sM1 by A34,A42,A44,FUNCT_2:63; sM0.0 = G.(j0,j0) by Def3 .= Ft.(j0,j0) by A36,A31,FUNCT_1:49 .= xt by A4,A8,Lm4; then A46: ft1 = sM0 by A34,A11,A38,FUNCT_2:63; set Qt = Prj1(j1,G); A47: Qt.0 = G.(j0,j1) by Def2 .= sM0.j1 by Def3 .= xt by A46,A12,TOPALG_3:4; Qt.1 = G.(j1,j1) by Def2 .= sM1.j1 by Def3 .= yt by A45,A43,TOPALG_3:4; then reconsider Qt as Path of xt,yt by A34,A47,BORSUK_2:def 4; A48: now let s be Point of I[01]; [s,0] in [:I,{0}:] by Lm4,ZFMISC_1:87; hence G.(s,0) = Ft.(s,j0) by A36,FUNCT_1:49 .= ft.s by A8,Lm4; thus G.(s,1) = Qt.s by Def2; let t be Point of I[01]; thus G.(0,t) = sM0.t by Def3 .= xt by A46,A12,TOPALG_3:4; thus G.(1,t) = sM1.t by Def3 .= yt by A45,A43,TOPALG_3:4; end; then ft,Qt are_homotopic by A34; then reconsider G as Homotopy of ft,Qt by A34,A48,BORSUK_6:def 11; take ft, Qt; take G; thus A49: ft,Qt are_homotopic by A34,A48; thus F = CircleMap*G by A35; thus yt in (CircleMap)"{y0} by A41,FUNCT_2:38; let F1 be Homotopy of ft,Qt such that A50: F = CircleMap*F1; A51: dom F1 = the carrier of [:I[01],I[01]:] by FUNCT_2:def 1; then A52: dom (F1 | [:I,{0}:]) = [:I,{0}:] by A32,A33,RELAT_1:62; for x being object st x in dom (F1 | [:I,{0}:]) holds (F1 | [:I,{0}:]).x = Ft.x proof let x be object; assume A53: x in dom (F1 | [:I,{0}:]); then consider x1, x2 being object such that A54: x1 in I and A55: x2 in {0} and A56: x = [x1,x2] by A52,ZFMISC_1:def 2; A57: x2 = 0 by A55,TARSKI:def 1; thus (F1 | [:I,{0}:]).x = F1.(x1,x2) by A53,A56,FUNCT_1:47 .= ft.x1 by A49,A54,A57,BORSUK_6:def 11 .= Ft.(x1,x2) by A8,A54,A55 .= Ft.x by A56; end; then F1 | [:I,{0}:] = Ft by A32,A33,A14,A51,RELAT_1:62; hence thesis by A37,A50; end; definition func Ciso -> Function of INT.Group, pi_1(Tunit_circle(2),c[10]) means :Def5: for n being Integer holds it.n = Class(EqRel(Tunit_circle(2),c[10]),cLoop(n)); existence proof defpred P[Integer,set] means \$2 = Class(EqRel(TUC,c[10]),cLoop(\$1)); A1: for x being Element of INT ex y being Element of pi_1(TUC,c[10]) st P[ x,y] proof let x be Element of INT; reconsider y = Class(EqRel(TUC,c[10]),cLoop(x)) as Element of pi_1(TUC, c[10]) by TOPALG_1:47; take y; thus thesis; end; consider f being Function of INT,the carrier of pi_1(TUC,c[10]) such that A2: for x being Element of INT holds P[x,f.x] from FUNCT_2:sch 3(A1); reconsider f as Function of INT.Group, pi_1(TUC,c[10]); take f; let n be Integer; n in INT by INT_1:def 2; hence thesis by A2; end; uniqueness proof let f, g be Function of INT.Group, pi_1(TUC,c[10]) such that A3: for n being Integer holds f.n = Class(EqRel(TUC,c[10]),cLoop(n)) and A4: for n being Integer holds g.n = Class(EqRel(TUC,c[10]),cLoop(n)); for x being Element of INT.Group holds f.x = g.x proof let x be Element of INT.Group; thus f.x = Class(EqRel(TUC,c[10]),cLoop(x)) by A3 .= g.x by A4; end; hence thesis; end; end; theorem Th25: for i being Integer, f being Path of R^1(0),R^1(i) holds Ciso.i = Class(EqRel(Tunit_circle(2),c[10]),CircleMap*f) proof let i be Integer; let f be Path of R^1(0),R^1(i); set P = CircleMap*f; A1: P.0 = CircleMap.(f.j0) by FUNCT_2:15 .= CircleMap.R^1(0) by BORSUK_2:def 4 .= CircleMap.0 by TOPREALB:def 2 .= |[ cos(2*PI*0), sin(2*PI*0) ]| by TOPREALB:def 11 .= c[10] by SIN_COS:31,TOPREALB:def 8; P.1 = CircleMap.(f.j1) by FUNCT_2:15 .= CircleMap.R^1(i) by BORSUK_2:def 4 .= CircleMap.i by TOPREALB:def 2 .= |[ cos(2*PI*i+0), sin(2*PI*i+0) ]| by TOPREALB:def 11 .= |[ cos(0), sin(2*PI*i+0) ]| by COMPLEX2:9 .= c[10] by COMPLEX2:8,SIN_COS:31,TOPREALB:def 8; then reconsider P as Loop of c[10] by A1,BORSUK_2:def 4; A2: cLoop(i) = CircleMap * ExtendInt(i) by Th20; A3: cLoop(i),P are_homotopic proof reconsider J = R^1 as non empty interval SubSpace of R^1; reconsider r0 = R^1(0), ri = R^1(i) as Point of J; reconsider O = ExtendInt(i), ff = f as Path of r0,ri; reconsider G = R1Homotopy(O,ff) as Function of [:I[01],I[01]:],R^1; take F = CircleMap*G; thus F is continuous; let s be Point of I[01]; thus F.(s,0) = CircleMap.(G.(s,j0)) by Lm5,BINOP_1:18 .= CircleMap.((1-j0) * (ExtendInt(i)).s + j0 * f.s) by TOPALG_2:def 4 .= (cLoop(i)).s by A2,FUNCT_2:15; thus F.(s,1) = CircleMap.(G.(s,j1)) by Lm5,BINOP_1:18 .= CircleMap.((1-j1) * (ExtendInt(i)).s + j1 * f.s) by TOPALG_2:def 4 .= P.s by FUNCT_2:15; thus F.(0,s) = CircleMap.(G.(j0,s)) by Lm5,BINOP_1:18 .= CircleMap.((1-s) * (ExtendInt(i)).j0 + s * f.j0) by TOPALG_2:def 4 .= CircleMap.((1-s) * R^1(0) + s * f.j0) by BORSUK_2:def 4 .= CircleMap.((1-s) * R^1(0) + s * R^1(0)) by BORSUK_2:def 4 .= CircleMap.((1-s) * 0 + s * 0) by TOPREALB:def 2 .= c[10] by TOPREALB:32; thus F.(1,s) = CircleMap.(G.(j1,s)) by Lm5,BINOP_1:18 .= CircleMap.((1-s) * (ExtendInt(i)).j1 + s * f.j1) by TOPALG_2:def 4 .= CircleMap.((1-s) * R^1(i) + s * f.j1) by BORSUK_2:def 4 .= CircleMap.((1-s) * R^1(i) + s * R^1(i)) by BORSUK_2:def 4 .= CircleMap.i by TOPREALB:def 2 .= c[10] by TOPREALB:32; end; thus Ciso.i = Class(EqRel(TUC,c[10]),cLoop(i)) by Def5 .= Class(EqRel(TUC,c[10]),CircleMap*f) by A3,TOPALG_1:46; end; registration cluster Ciso -> multiplicative; coherence proof set f = Ciso; let x, y be Element of INT.Group; consider fX, fY being Loop of c[10] such that A1: f.x = Class(EqRel(TUC,c[10]),fX) and A2: f.y = Class(EqRel(TUC,c[10]),fY) and A3: (the multF of pi_1(TUC,c[10])).(f.x,f.y) = Class(EqRel(TUC,c[10] ),fX+fY) by TOPALG_1:def 5; f.y = Class(EqRel(TUC,c[10]),cLoop(y)) by Def5; then A4: fY,cLoop(y) are_homotopic by A2,TOPALG_1:46; reconsider tx = AffineMap(1,x) as Function of R^1,R^1 by TOPMETR:17; set p = tx*ExtendInt(y); A5: p.0 = tx.((ExtendInt(y)).j0) by FUNCT_2:15 .= tx.(y*j0) by Def1 .= 1*0+x by FCONT_1:def 4 .= R^1(x) by TOPREALB:def 2; A6: p.1 = tx.((ExtendInt(y)).j1) by FUNCT_2:15 .= tx.(y*j1) by Def1 .= 1*y+x by FCONT_1:def 4 .= R^1(x+y) by TOPREALB:def 2; tx is being_homeomorphism by JORDAN16:20; then tx is continuous; then reconsider p as Path of R^1(x),R^1(x+y) by A5,A6,BORSUK_2:def 4; A7: for a being Point of I[01] holds (CircleMap * (ExtendInt(x)+p)).a = (cLoop(x)+cLoop(y)).a proof let a be Point of I[01]; per cases; suppose A8: a <= 1/2; then A9: 2*a is Point of I[01] by BORSUK_6:3; thus (CircleMap * (ExtendInt(x)+p)).a = CircleMap.((ExtendInt(x)+p). a) by FUNCT_2:15 .= CircleMap.((ExtendInt(x)).(2*a)) by A8,BORSUK_6:def 2 .= CircleMap.(x*(2*a)) by A9,Def1 .= |[ cos(2*PI*(x*(2*a))), sin(2*PI*(x*(2*a))) ]| by TOPREALB:def 11 .= |[ cos(2*PI*x*(2*a)), sin(2*PI*x*(2*a)) ]| .= (cLoop(x)).(2*a) by A9,Def4 .= (cLoop(x)+cLoop(y)).a by A8,BORSUK_6:def 2; end; suppose A10: 1/2 <= a; then A11: 2*a-1 is Point of I[01] by BORSUK_6:4; thus (CircleMap * (ExtendInt(x)+p)).a = CircleMap.((ExtendInt(x)+p). a) by FUNCT_2:15 .= CircleMap.(p.(2*a-1)) by A10,BORSUK_6:def 2 .= CircleMap.(tx.((ExtendInt(y)).(2*a-1))) by A11,FUNCT_2:15 .= CircleMap.(tx.(y*(2*a-1))) by A11,Def1 .= CircleMap.(1*(y*(2*a-1))+x) by FCONT_1:def 4 .= |[ cos(2*PI*((y*(2*a-1))+x)), sin(2*PI*((y*(2*a-1))+x)) ]| by TOPREALB:def 11 .= |[ cos(2*PI*(y*(2*a-1))), sin(2*PI*(y*(2*a-1))+2*PI*x) ]| by COMPLEX2:9 .= |[ cos(2*PI*y*(2*a-1)), sin(2*PI*y*(2*a-1)) ]| by COMPLEX2:8 .= (cLoop(y)).(2*a-1) by A11,Def4 .= (cLoop(x)+cLoop(y)).a by A10,BORSUK_6:def 2; end; end; f.x = Class(EqRel(TUC,c[10]),cLoop(x)) by Def5; then fX,cLoop(x) are_homotopic by A1,TOPALG_1:46; then A12: fX+fY,cLoop(x)+cLoop(y) are_homotopic by A4,BORSUK_6:76; thus f.(x*y) = Class(EqRel(TUC,c[10]),CircleMap*(ExtendInt(x)+p)) by Th25 .= Class(EqRel(TUC,c[10]),cLoop(x)+cLoop(y)) by A7,FUNCT_2:63 .= f.x * f.y by A3,A12,TOPALG_1:46; end; end; registration cluster Ciso -> one-to-one onto; coherence proof thus Ciso is one-to-one proof set xt = R^1(0); let m, n be object; assume that A1: m in dom Ciso & n in dom Ciso and A2: Ciso.m = Ciso.n; reconsider m, n as Integer by A1; Ciso.m = Class(EqRel(TUC,c[10]),cLoop(m)) & Ciso.n = Class(EqRel(TUC ,c[10]), cLoop(n)) by Def5; then A3: cLoop(m),cLoop(n) are_homotopic by A2,TOPALG_1:46; then consider F being Function of [:I[01],I[01]:], TUC such that A4: F is continuous and A5: for s being Point of I[01] holds F.(s,0) = (cLoop(m)).s & F.(s,1 ) = (cLoop(n)).s & for t being Point of I[01] holds F.(0,t) = c[10] & F.(1,t) = c[10]; A6: xt in (CircleMap)"{c[10]} by Lm1,TOPREALB:33,def 2; then consider ftm being Function of I[01], R^1 such that ftm.0 = xt and cLoop(m) = CircleMap*ftm and ftm is continuous and A7: for f1 being Function of I[01], R^1 st f1 is continuous & cLoop (m) = CircleMap*f1 & f1.0 = xt holds ftm = f1 by Th23; F is Homotopy of cLoop(m),cLoop(n) by A3,A4,A5,BORSUK_6:def 11; then consider yt being Point of R^1, Pt, Qt being Path of xt,yt, Ft being Homotopy of Pt,Qt such that A8: Pt,Qt are_homotopic and A9: F = CircleMap*Ft and yt in (CircleMap)"{c[10]} and for F1 being Homotopy of Pt,Qt st F = CircleMap*F1 holds Ft = F1 by A3,A6 ,Th24; A10: cLoop(n) = CircleMap*ExtendInt(n) by Th20; set ft0 = Prj1(j0,Ft); A11: now let x be Point of I[01]; thus (CircleMap*ft0).x = CircleMap.(ft0.x) by FUNCT_2:15 .= CircleMap.(Ft.(x,j0)) by Def2 .= F.(x,j0) by A9,Lm5,BINOP_1:18 .= (cLoop(m)).x by A5; end; ft0.0 = Ft.(j0,j0) by Def2 .= xt by A8,BORSUK_6:def 11; then A12: ft0 = ftm by A7,A11,FUNCT_2:63; set ft1 = Prj1(j1,Ft); A13: now let x be Point of I[01]; thus (CircleMap*ft1).x = CircleMap.(ft1.x) by FUNCT_2:15 .= CircleMap.(Ft.(x,j1)) by Def2 .= F.(x,j1) by A9,Lm5,BINOP_1:18 .= (cLoop(n)).x by A5; end; consider ftn being Function of I[01], R^1 such that ftn.0 = xt and cLoop(n) = CircleMap*ftn and ftn is continuous and A14: for f1 being Function of I[01], R^1 st f1 is continuous & cLoop (n) = CircleMap*f1 & f1.0 = xt holds ftn = f1 by A6,Th23; A15: cLoop(m) = CircleMap*ExtendInt(m) by Th20; ft1.0 = Ft.(j0,j1) by Def2 .= xt by A8,BORSUK_6:def 11; then A16: ft1 = ftn by A14,A13,FUNCT_2:63; (ExtendInt(n)).0 = n*j0 by Def1 .= xt by TOPREALB:def 2; then ExtendInt(n) = ftn by A14,A10; then A17: ft1.j1 = n*1 by A16,Def1; (ExtendInt(m)).0 = m*j0 by Def1 .= xt by TOPREALB:def 2; then ExtendInt(m) = ftm by A7,A15; then A18: ft0.j1 = m*1 by A12,Def1; ft0.j1 = Ft.(j1,j0) by Def2 .= yt by A8,BORSUK_6:def 11 .= Ft.(j1,j1) by A8,BORSUK_6:def 11 .= ft1.j1 by Def2; hence thesis by A18,A17; end; thus rng Ciso c= the carrier of pi_1(TUC,c[10]); let q be object; assume q in the carrier of pi_1(TUC,c[10]); then consider f being Loop of c[10] such that A19: q = Class(EqRel(TUC,c[10]),f) by TOPALG_1:47; R^1(0) in (CircleMap)"{c[10]} by Lm1,TOPREALB:33,def 2; then consider ft being Function of I[01], R^1 such that A20: ft.0 = R^1(0) and A21: f = CircleMap*ft and A22: ft is continuous and for f1 being Function of I[01], R^1 st f1 is continuous & f = CircleMap*f1 & f1.0 = R^1(0) holds ft = f1 by Th23; A23: ft.1 in REAL by XREAL_0:def 1; CircleMap.(ft.j1) = (CircleMap*ft).j1 by FUNCT_2:15 .= c[10] by A21,BORSUK_2:def 4; then CircleMap.(ft.1) in {c[10]} by TARSKI:def 1; then A24: ft.1 in INT by Lm12,FUNCT_1:def 7,TOPREALB:33,A23; ft.1 = R^1(ft.1) by TOPREALB:def 2; then ft is Path of R^1(0),R^1(ft.1) by A20,A22,BORSUK_2:def 4; then dom Ciso = INT & Ciso.(ft.1) = Class(EqRel(TUC,c[10]),CircleMap*ft) by A24,Th25,FUNCT_2:def 1; hence thesis by A19,A21,A24,FUNCT_1:def 3; end; end; theorem Ciso is bijective; Lm16: for r being positive Real, o being Point of TOP-REAL 2, x being Point of Tcircle(o,r) holds INT.Group,pi_1(Tcircle(o,r),x) are_isomorphic proof let r be positive Real, o be Point of TOP-REAL 2, x be Point of Tcircle(o,r); TUC = Tcircle(0.TOP-REAL 2,1) by TOPREALB:def 7; then pi_1(TUC,c[10]),pi_1(Tcircle(o,r),x) are_isomorphic by TOPALG_3:33 ,TOPREALB:20; then consider h being Homomorphism of pi_1(TUC,c[10]), pi_1(Tcircle(o,r),x) such that A1: h is bijective; take h*Ciso; thus thesis by A1,GROUP_6:64; end; theorem Th27: for S being being_simple_closed_curve SubSpace of TOP-REAL 2, x being Point of S holds INT.Group, pi_1(S,x) are_isomorphic proof set r = the positive Real,o = the Point of TOP-REAL 2,y = the Point of Tcircle(o,r); let S be being_simple_closed_curve SubSpace of TOP-REAL 2, x be Point of S; INT.Group,pi_1(Tcircle(o,r),y) are_isomorphic & pi_1(Tcircle(o,r),y), pi_1(S,x) are_isomorphic by Lm16,TOPALG_3:33,TOPREALB:11; hence thesis by GROUP_6:67; end; registration let S be being_simple_closed_curve SubSpace of TOP-REAL 2, x be Point of S; cluster pi_1(S,x) -> infinite; coherence proof INT.Group, pi_1(S,x) are_isomorphic by Th27; hence thesis by GROUP_6:74; end; end;