:: TOPALG_5 semantic presentation begin 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 the carrier of I[01] by BORSUK_1:43; then Lm3: {0} c= the carrier of I[01] by ZFMISC_1:31; Lm4: 0 in {0} by TARSKI:def_1; Lm5: the carrier of [:I[01],I[01]:] = [: the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def_2; reconsider j0 = 0 , j1 = 1 as Point of I[01] by BORSUK_1:def_14, BORSUK_1:def_15; Lm6: [#] I[01] = the carrier of I[01] ; 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 not INT.Group is finite ; end; theorem Th1: :: TOPALG_5:1 for r, s, a being real number st r <= s holds 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 let r, s, a be real number ; ::_thesis: ( 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).[ ) ) set M = Closed-Interval-MSpace (r,s); assume r <= s ; ::_thesis: 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).[ ) then A1: the carrier of (Closed-Interval-MSpace (r,s)) = [.r,s.] by TOPMETR:10; let p be Point of (Closed-Interval-MSpace (r,s)); ::_thesis: ( 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).[ ) set B = Ball (p,a); reconsider p1 = p as Point of RealSpace by TOPMETR:8; set B1 = Ball (p1,a); A2: Ball (p,a) = (Ball (p1,a)) /\ the carrier of (Closed-Interval-MSpace (r,s)) by TOPMETR:9; ( a is Real & p1 is Real ) by XREAL_0:def_1; then A3: Ball (p1,a) = ].(p1 - a),(p1 + a).[ by FRECHET:7; percases ( ( p1 + a <= s & p1 - a < r ) or ( p1 + a <= s & p1 - a >= r ) or ( p1 + a > s & p1 - a < r ) or ( p1 + a > s & p1 - a >= r ) ) ; supposethat A4: p1 + a <= s and A5: p1 - a < r ; ::_thesis: ( 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).[ ) Ball (p,a) = [.r,(p1 + a).[ proof thus Ball (p,a) c= [.r,(p1 + a).[ :: according to XBOOLE_0:def_10 ::_thesis: [.r,(p1 + a).[ c= Ball (p,a) proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Ball (p,a) or b in [.r,(p1 + a).[ ) assume A6: b in Ball (p,a) ; ::_thesis: b in [.r,(p1 + a).[ then reconsider b = b as Element of Ball (p,a) ; b in Ball (p1,a) 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 b in [.r,(p1 + a).[ by A7, XXREAL_1:3; ::_thesis: verum end; let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in [.r,(p1 + a).[ or b in Ball (p,a) ) assume A8: b in [.r,(p1 + a).[ ; ::_thesis: b in Ball (p,a) then reconsider b = 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 Ball (p1,a) by A3, A10, XXREAL_1:4; hence b in Ball (p,a) by A1, A2, A11, XBOOLE_0:def_4; ::_thesis: verum end; hence ( 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).[ ) ; ::_thesis: verum end; supposethat A12: p1 + a <= s and A13: p1 - a >= r ; ::_thesis: ( 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).[ ) Ball (p,a) = ].(p1 - a),(p1 + a).[ proof thus Ball (p,a) c= ].(p1 - a),(p1 + a).[ by A2, A3, XBOOLE_1:17; :: according to XBOOLE_0:def_10 ::_thesis: ].(p1 - a),(p1 + a).[ c= Ball (p,a) let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in ].(p1 - a),(p1 + a).[ or b in Ball (p,a) ) assume A14: b in ].(p1 - a),(p1 + a).[ ; ::_thesis: b in Ball (p,a) then reconsider b = 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 b in Ball (p,a) by A1, A2, A3, A14, XBOOLE_0:def_4; ::_thesis: verum end; hence ( 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).[ ) ; ::_thesis: verum end; supposethat A16: p1 + a > s and A17: p1 - a < r ; ::_thesis: ( 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).[ ) Ball (p,a) = [.r,s.] proof thus Ball (p,a) c= [.r,s.] by A1; :: according to XBOOLE_0:def_10 ::_thesis: [.r,s.] c= Ball (p,a) let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in [.r,s.] or b in Ball (p,a) ) assume A18: b in [.r,s.] ; ::_thesis: b in Ball (p,a) then reconsider b = 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 Ball (p1,a) by A3, A19, XXREAL_1:4; hence b in Ball (p,a) by A1, A2, A18, XBOOLE_0:def_4; ::_thesis: verum end; hence ( 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).[ ) ; ::_thesis: verum end; supposethat A20: p1 + a > s and A21: p1 - a >= r ; ::_thesis: ( 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).[ ) Ball (p,a) = ].(p1 - a),s.] proof thus Ball (p,a) c= ].(p1 - a),s.] :: according to XBOOLE_0:def_10 ::_thesis: ].(p1 - a),s.] c= Ball (p,a) proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Ball (p,a) or b in ].(p1 - a),s.] ) assume A22: b in Ball (p,a) ; ::_thesis: b in ].(p1 - a),s.] then reconsider b = b as Element of Ball (p,a) ; b in Ball (p1,a) 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 b in ].(p1 - a),s.] by A23, XXREAL_1:2; ::_thesis: verum end; let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in ].(p1 - a),s.] or b in Ball (p,a) ) assume A24: b in ].(p1 - a),s.] ; ::_thesis: b in Ball (p,a) then reconsider b = 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 Ball (p1,a) by A3, A26, XXREAL_1:4; hence b in Ball (p,a) by A1, A2, A27, XBOOLE_0:def_4; ::_thesis: verum end; hence ( 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).[ ) ; ::_thesis: verum end; end; end; theorem Th2: :: TOPALG_5:2 for r, s being real number st r <= s holds 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 Element of 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 let r, s be real number ; ::_thesis: ( 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 Element of NAT : n <> 0 } & B = Union f ) & ( for X being Subset of (Closed-Interval-TSpace (r,s)) st X in B holds X is connected ) ) ) set L = Closed-Interval-TSpace (r,s); set M = Closed-Interval-MSpace (r,s); assume A1: r <= s ; ::_thesis: 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 Element of NAT : n <> 0 } & B = Union f ) & ( for X being Subset of (Closed-Interval-TSpace (r,s)) st X in B holds X is connected ) ) defpred S1[ set , set ] means ex x being Point of (Closed-Interval-TSpace (r,s)) ex y being Point of (Closed-Interval-MSpace (r,s)) ex B being Basis of st ( $1 = x & x = y & $2 = B & B = { (Ball (y,(1 / n))) where n is Element of NAT : n <> 0 } ); A2: Closed-Interval-TSpace (r,s) = TopSpaceMetr (Closed-Interval-MSpace (r,s)) by TOPMETR:def_7; A3: for i being set st i in the carrier of (Closed-Interval-TSpace (r,s)) holds ex j being set st S1[i,j] proof let i be set ; ::_thesis: ( i in the carrier of (Closed-Interval-TSpace (r,s)) implies ex j being set st S1[i,j] ) assume i in the carrier of (Closed-Interval-TSpace (r,s)) ; ::_thesis: ex j being set st S1[i,j] then reconsider i = i as Point of (Closed-Interval-TSpace (r,s)) ; reconsider m = i as Point of (Closed-Interval-MSpace (r,s)) by A2, TOPMETR:12; reconsider j = i as Element of (TopSpaceMetr (Closed-Interval-MSpace (r,s))) by A2; set B = Balls j; A4: ex y being Point of (Closed-Interval-MSpace (r,s)) st ( y = j & Balls j = { (Ball (y,(1 / n))) where n is Element of NAT : n <> 0 } ) by FRECHET:def_1; reconsider B1 = Balls j as Basis of by A2; take Balls j ; ::_thesis: S1[i, Balls j] take i ; ::_thesis: ex y being Point of (Closed-Interval-MSpace (r,s)) ex B being Basis of st ( i = i & i = y & Balls j = B & B = { (Ball (y,(1 / n))) where n is Element of NAT : n <> 0 } ) take m ; ::_thesis: ex B being Basis of st ( i = i & i = m & Balls j = B & B = { (Ball (m,(1 / n))) where n is Element of NAT : n <> 0 } ) take B1 ; ::_thesis: ( i = i & i = m & Balls j = B1 & B1 = { (Ball (m,(1 / n))) where n is Element of NAT : n <> 0 } ) thus ( i = i & i = m & Balls j = B1 & B1 = { (Ball (m,(1 / n))) where n is Element of NAT : n <> 0 } ) by A4; ::_thesis: verum end; consider f being ManySortedSet of the carrier of (Closed-Interval-TSpace (r,s)) such that A5: for i being set st i in the carrier of (Closed-Interval-TSpace (r,s)) holds S1[i,f . i] from PBOOLE:sch_3(A3); for x being Element of (Closed-Interval-TSpace (r,s)) holds f . x is Basis of proof let x be Element of (Closed-Interval-TSpace (r,s)); ::_thesis: f . x is Basis of S1[x,f . x] by A5; hence f . x is Basis of ; ::_thesis: verum end; then reconsider B = Union f as Basis of (Closed-Interval-TSpace (r,s)) by TOPGEN_2:2; take B ; ::_thesis: ( 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 Element of NAT : n <> 0 } & B = Union f ) & ( for X being Subset of (Closed-Interval-TSpace (r,s)) st X in B holds X is connected ) ) hereby ::_thesis: for X being Subset of (Closed-Interval-TSpace (r,s)) st X in B holds X is connected take f = f; ::_thesis: for x being Point of (Closed-Interval-MSpace (r,s)) holds ( f . x = { (Ball (x,(1 / n))) where n is Element of NAT : n <> 0 } & B = Union f ) let x be Point of (Closed-Interval-MSpace (r,s)); ::_thesis: ( f . x = { (Ball (x,(1 / n))) where n is Element of NAT : n <> 0 } & B = Union f ) the carrier of (Closed-Interval-MSpace (r,s)) = [.r,s.] by A1, TOPMETR:10 .= the carrier of (Closed-Interval-TSpace (r,s)) by A1, TOPMETR:18 ; then S1[x,f . x] by A5; hence ( f . x = { (Ball (x,(1 / n))) where n is Element of NAT : n <> 0 } & B = Union f ) ; ::_thesis: verum end; let X be Subset of (Closed-Interval-TSpace (r,s)); ::_thesis: ( X in B implies X is connected ) assume X in B ; ::_thesis: X is connected 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 set such that A8: x in dom f and A9: f . x = Z by A7, FUNCT_1:def_3; consider x1 being Point of (Closed-Interval-TSpace (r,s)), y being Point of (Closed-Interval-MSpace (r,s)), B1 being Basis of such that x = x1 and x1 = y and A10: ( f . x = B1 & B1 = { (Ball (y,(1 / n))) where n is Element of NAT : n <> 0 } ) by A5, A8; consider n being Element of 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 X is connected by CONNSP_1:23; ::_thesis: verum end; theorem Th3: :: TOPALG_5:3 for T being TopStruct for A being Subset of T for t being Point of T st t in A holds Component_of (t,A) c= A proof let T be TopStruct ; ::_thesis: for A being Subset of T for t being Point of T st t in A holds Component_of (t,A) c= A let A be Subset of T; ::_thesis: for t being Point of T st t in A holds Component_of (t,A) c= A let t be Point of T; ::_thesis: ( t in A implies Component_of (t,A) c= A ) assume A1: t in A ; ::_thesis: Component_of (t,A) c= 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 Component_of (t,A) c= A by A2; ::_thesis: verum end; registration let T be TopSpace; let A be open Subset of T; clusterT | A -> open ; coherence T | A is open proof let X be Subset of T; :: according to TSEP_1:def_1 ::_thesis: ( not X = the carrier of (T | A) or X is open ) thus ( not X = the carrier of (T | A) or X is open ) by PRE_TOPC:8; ::_thesis: verum end; end; theorem Th4: :: TOPALG_5:4 for T being TopSpace for S being SubSpace of T for A being Subset of T for B being Subset of S st A = B holds T | A = S | B proof let T be TopSpace; ::_thesis: for S being SubSpace of T for A being Subset of T for B being Subset of S st A = B holds T | A = S | B let S be SubSpace of T; ::_thesis: for A being Subset of T for B being Subset of S st A = B holds T | A = S | B let A be Subset of T; ::_thesis: for B being Subset of S st A = B holds T | A = S | B let B be Subset of S; ::_thesis: ( A = B implies T | A = S | B ) assume A = B ; ::_thesis: T | A = S | B then ( S | B is SubSpace of T & [#] (S | B) = A ) by PRE_TOPC:def_5, TSEP_1:7; hence T | A = S | B by PRE_TOPC:def_5; ::_thesis: verum end; theorem Th5: :: TOPALG_5:5 for S, T being TopSpace for A, B being Subset of T for C, D being Subset of S st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = C & B = D & A,B are_separated holds C,D are_separated proof let S, T be TopSpace; ::_thesis: for A, B being Subset of T for C, D being Subset of S st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = C & B = D & A,B are_separated holds C,D are_separated let A, B be Subset of T; ::_thesis: for C, D being Subset of S st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = C & B = D & A,B are_separated holds C,D are_separated let C, D be Subset of S; ::_thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = C & B = D & A,B are_separated implies C,D are_separated ) assume A1: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) ; ::_thesis: ( not A = C or not B = D or not A,B are_separated or C,D are_separated ) assume A2: ( A = C & B = D ) ; ::_thesis: ( not A,B are_separated or C,D are_separated ) assume A,B are_separated ; ::_thesis: C,D are_separated then A3: ( Cl A misses B & A misses Cl B ) by CONNSP_1:def_1; ( Cl A = Cl C & Cl B = Cl D ) by A1, A2, TOPS_3:80; hence C,D are_separated by A2, A3, CONNSP_1:def_1; ::_thesis: verum end; theorem :: TOPALG_5:6 for S, T being TopSpace st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & S is connected holds T is connected proof let S, T be TopSpace; ::_thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & S is connected implies T is connected ) assume that A1: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) and A2: S is connected ; ::_thesis: T is connected let A, B be Subset of T; :: according to CONNSP_1:def_2 ::_thesis: ( not [#] T = A \/ B or not A,B are_separated or A = {} T or B = {} T ) assume that A3: [#] T = A \/ B and A4: A,B are_separated ; ::_thesis: ( A = {} T or B = {} T ) 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, CONNSP_1:def_2; hence ( A = {} T or B = {} T ) ; ::_thesis: verum end; theorem Th7: :: TOPALG_5:7 for S, T being TopSpace for A being Subset of S for B being Subset of T st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = B & A is connected holds B is connected proof let S, T be TopSpace; ::_thesis: for A being Subset of S for B being Subset of T st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = B & A is connected holds B is connected let A be Subset of S; ::_thesis: for B being Subset of T st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = B & A is connected holds B is connected let B be Subset of T; ::_thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = B & A is connected implies B is connected ) assume that A1: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) and A2: ( A = B & A is connected ) ; ::_thesis: B is connected now__::_thesis:_for_P,_Q_being_Subset_of_T_st_B_=_P_\/_Q_&_P,Q_are_separated_&_not_P_=_{}_T_holds_ Q_=_{}_T let P, Q be Subset of T; ::_thesis: ( B = P \/ Q & P,Q are_separated & not P = {} T implies Q = {} T ) assume that A3: B = P \/ Q and A4: P,Q are_separated ; ::_thesis: ( P = {} T or Q = {} T ) 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 ) ; ::_thesis: verum end; hence B is connected by CONNSP_1:15; ::_thesis: verum end; theorem Th8: :: TOPALG_5:8 for S, T being non empty TopSpace for s being Point of S for t being Point of T for A being a_neighborhood of s st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & s = t holds A is a_neighborhood of t proof let S, T be non empty TopSpace; ::_thesis: for s being Point of S for t being Point of T for A being a_neighborhood of s st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & s = t holds A is a_neighborhood of t let s be Point of S; ::_thesis: for t being Point of T for A being a_neighborhood of s st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & s = t holds A is a_neighborhood of t let t be Point of T; ::_thesis: for A being a_neighborhood of s st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & s = t holds A is a_neighborhood of t let A be a_neighborhood of s; ::_thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & s = t implies A is a_neighborhood of t ) assume that A1: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) and A2: s = t ; ::_thesis: A is a_neighborhood of 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 A is a_neighborhood of t by A2, A3, CONNSP_2:def_1; ::_thesis: verum end; theorem :: TOPALG_5:9 for S, T being non empty TopSpace for A being Subset of S for B being Subset of T for N being a_neighborhood of A st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = B holds N is a_neighborhood of B proof let S, T be non empty TopSpace; ::_thesis: for A being Subset of S for B being Subset of T for N being a_neighborhood of A st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = B holds N is a_neighborhood of B let A be Subset of S; ::_thesis: for B being Subset of T for N being a_neighborhood of A st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = B holds N is a_neighborhood of B let B be Subset of T; ::_thesis: for N being a_neighborhood of A st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = B holds N is a_neighborhood of B let N be a_neighborhood of A; ::_thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = B implies N is a_neighborhood of B ) assume that A1: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) and A2: A = B ; ::_thesis: N is a_neighborhood of 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 N is a_neighborhood of B by A2, A3, CONNSP_2:def_2; ::_thesis: verum end; theorem Th10: :: TOPALG_5:10 for S, T being non empty TopSpace for A, B being Subset of T for 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; ::_thesis: for A, B being Subset of T for 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 let A, B be Subset of T; ::_thesis: for 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 let f be Function of S,T; ::_thesis: ( f is being_homeomorphism & A is_a_component_of B implies f " A is_a_component_of f " B ) assume A1: f is being_homeomorphism ; ::_thesis: ( not A is_a_component_of B or f " A is_a_component_of f " B ) A2: rng f = [#] T by A1, TOPS_2:def_5 .= 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 ; :: according to CONNSP_1:def_6 ::_thesis: f " A is_a_component_of f " B A5: the carrier of (T | B) = B by PRE_TOPC:8; then f " X c= f " B by RELAT_1:143; then reconsider Y = f " A as Subset of (S | (f " B)) by A3, PRE_TOPC:8; take Y ; :: according to CONNSP_1:def_6 ::_thesis: ( Y = f " A & Y is a_component ) thus Y = f " A ; ::_thesis: Y is a_component 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; :: according to CONNSP_1:def_5 ::_thesis: for b1 being Element of bool the carrier of (S | (f " B)) holds ( not b1 is connected or not Y c= b1 or Y = b1 ) let Z be Subset of (S | (f " B)); ::_thesis: ( not Z is connected or not Y c= Z or Y = Z ) assume that A6: Z is connected and A7: Y c= Z ; ::_thesis: Y = Z A8: f .: Y c= f .: Z by A7, RELAT_1:123; A9: f is one-to-one by A1, TOPS_2:def_5; A10: f is continuous by A1, TOPS_2:def_5; 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, CONNSP_1:def_5; hence Y = Z by A3, A9, A11, FUNCT_1:94; ::_thesis: verum end; begin theorem Th11: :: TOPALG_5:11 for T being non empty TopSpace for S being non empty SubSpace of T for A being non empty Subset of T for B being non empty Subset of S st A = B & A is locally_connected holds B is locally_connected proof let T be non empty TopSpace; ::_thesis: for S being non empty SubSpace of T for A being non empty Subset of T for B being non empty Subset of S st A = B & A is locally_connected holds B is locally_connected let S be non empty SubSpace of T; ::_thesis: for A being non empty Subset of T for B being non empty Subset of S st A = B & A is locally_connected holds B is locally_connected let A be non empty Subset of T; ::_thesis: for B being non empty Subset of S st A = B & A is locally_connected holds B is locally_connected let B be non empty Subset of S; ::_thesis: ( A = B & A is locally_connected implies B is locally_connected ) assume that A1: A = B and A2: A is locally_connected ; ::_thesis: B is locally_connected T | A = S | B by A1, Th4; hence S | B is locally_connected by A2, CONNSP_2:def_6; :: according to CONNSP_2:def_6 ::_thesis: verum end; theorem Th12: :: TOPALG_5:12 for S, T being non empty TopSpace st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & S is locally_connected holds T is locally_connected proof let S, T be non empty TopSpace; ::_thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & S is locally_connected implies T is locally_connected ) assume that A1: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) and A2: S is locally_connected ; ::_thesis: T is locally_connected let t be Point of T; :: according to CONNSP_2:def_4 ::_thesis: T is_locally_connected_in t reconsider s = t as Point of S by A1; let U be Subset of T; :: according to CONNSP_2:def_3 ::_thesis: ( not U is a_neighborhood of t or ex b1 being Element of bool the carrier of T st ( b1 is a_neighborhood of t & b1 is connected & b1 c= U ) ) reconsider U1 = U as Subset of S by A1; assume U is a_neighborhood of t ; ::_thesis: ex b1 being Element of bool the carrier of T st ( b1 is a_neighborhood of t & b1 is connected & b1 c= U ) then A3: U1 is a_neighborhood of s by A1, Th8; S is_locally_connected_in s by A2, CONNSP_2:def_4; 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, CONNSP_2:def_3; reconsider V = V1 as Subset of T by A1; take V ; ::_thesis: ( V is a_neighborhood of t & V is connected & V c= U ) thus V is a_neighborhood of t by A1, A4, Th8; ::_thesis: ( V is connected & V c= U ) thus V is connected by A1, A5, Th7; ::_thesis: V c= U thus V c= U by A6; ::_thesis: verum end; theorem Th13: :: TOPALG_5:13 for T being non empty TopSpace holds ( T is locally_connected iff [#] T is locally_connected ) proof let T be non empty TopSpace; ::_thesis: ( T is locally_connected iff [#] T is locally_connected ) T is SubSpace of T by TSEP_1:2; then A1: TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of (T | ([#] T)), the topology of (T | ([#] T)) #) by PRE_TOPC:8, TSEP_1:5; hereby ::_thesis: ( [#] T is locally_connected implies T is locally_connected ) assume T is locally_connected ; ::_thesis: [#] T is locally_connected then T | ([#] T) is locally_connected by A1, Th12; hence [#] T is locally_connected by CONNSP_2:def_6; ::_thesis: verum end; assume [#] T is locally_connected ; ::_thesis: T is locally_connected then T | ([#] T) is locally_connected by CONNSP_2:def_6; hence T is locally_connected by A1, Th12; ::_thesis: verum end; Lm10: for T being non empty TopSpace for S being non empty open SubSpace of T st T is locally_connected holds TopStruct(# the carrier of S, the topology of S #) is locally_connected proof let T be non empty TopSpace; ::_thesis: for S being non empty open SubSpace of T st T is locally_connected holds TopStruct(# the carrier of S, the topology of S #) is locally_connected let S be non empty open SubSpace of T; ::_thesis: ( T is locally_connected implies TopStruct(# the carrier of S, the topology of S #) is locally_connected ) 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 ; ::_thesis: TopStruct(# the carrier of S, the topology of S #) is locally_connected then [#] S is locally_connected by A1, Th11, CONNSP_2:17; then S is locally_connected by Th13; then TopStruct(# the carrier of S, the topology of S #) is locally_connected by Th12; then [#] TopStruct(# the carrier of S, the topology of S #) is locally_connected by Th13; then TopStruct(# the carrier of S, the topology of S #) | ([#] TopStruct(# the carrier of S, the topology of S #)) is locally_connected by CONNSP_2:def_6; hence TopStruct(# the carrier of S, the topology of S #) is locally_connected by TSEP_1:3; ::_thesis: verum end; theorem Th14: :: TOPALG_5:14 for T being non empty TopSpace for 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; ::_thesis: for S being non empty open SubSpace of T st T is locally_connected holds S is locally_connected let S be non empty open SubSpace of T; ::_thesis: ( T is locally_connected implies S is locally_connected ) assume T is locally_connected ; ::_thesis: S is locally_connected then TopStruct(# the carrier of S, the topology of S #) is locally_connected by Lm10; hence S is locally_connected by Th12; ::_thesis: verum end; theorem :: TOPALG_5:15 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; ::_thesis: ( S,T are_homeomorphic & S is locally_connected implies T is locally_connected ) given f being Function of S,T such that A1: f is being_homeomorphism ; :: according to T_0TOPSP:def_1 ::_thesis: ( not S is locally_connected or T is locally_connected ) assume A2: S is locally_connected ; ::_thesis: T is locally_connected now__::_thesis:_for_A_being_non_empty_Subset_of_T for_B_being_Subset_of_T_st_A_is_open_&_B_is_a_component_of_A_holds_ B_is_open let A be non empty Subset of T; ::_thesis: for B being Subset of T st A is open & B is_a_component_of A holds B is open let B be Subset of T; ::_thesis: ( A is open & B is_a_component_of A implies B is open ) assume ( A is open & B is_a_component_of A ) ; ::_thesis: B is open 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, TOPS_2:def_5; then not f " A is 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; ::_thesis: verum end; hence T is locally_connected by CONNSP_2:18; ::_thesis: verum end; theorem Th16: :: TOPALG_5:16 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; ::_thesis: ( ex B being Basis of T st for X being Subset of T st X in B holds X is connected implies T is locally_connected ) given B being Basis of T such that A1: for X being Subset of T st X in B holds X is connected ; ::_thesis: T is locally_connected let x be Point of T; :: according to CONNSP_2:def_4 ::_thesis: T is_locally_connected_in x let U be Subset of T; :: according to CONNSP_2:def_3 ::_thesis: ( not U is a_neighborhood of x or ex b1 being Element of bool the carrier of T st ( b1 is a_neighborhood of x & b1 is connected & b1 c= U ) ) assume A2: x in Int U ; :: according to CONNSP_2:def_1 ::_thesis: ex b1 being Element of bool the carrier of T st ( b1 is a_neighborhood of x & b1 is connected & b1 c= 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 = V as Subset of T by A6; take V ; ::_thesis: ( V is a_neighborhood of x & V is connected & V c= U ) ( 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; :: according to CONNSP_2:def_1 ::_thesis: ( V is connected & V c= U ) thus V is connected by A1, A3, A6; ::_thesis: V c= U A7: Int U c= U by TOPS_1:16; V c= union Y by A6, ZFMISC_1:74; hence V c= U by A4, A7, XBOOLE_1:1; ::_thesis: verum end; theorem Th17: :: TOPALG_5:17 for r, s being real number st r <= s holds Closed-Interval-TSpace (r,s) is locally_connected proof let r, s be real number ; ::_thesis: ( r <= s implies Closed-Interval-TSpace (r,s) is locally_connected ) assume r <= s ; ::_thesis: Closed-Interval-TSpace (r,s) is locally_connected 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 Element of 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 Closed-Interval-TSpace (r,s) is locally_connected by Th16; ::_thesis: verum end; registration cluster I[01] -> locally_connected ; coherence I[01] is locally_connected by Th17, TOPMETR:20; end; registration let A be non empty open Subset of I[01]; clusterI[01] | A -> locally_connected ; coherence I[01] | A is locally_connected by Th14; end; begin definition let r be real number ; func ExtendInt r -> Function of I[01],R^1 means :Def1: :: TOPALG_5:def 1 for x being Point of I[01] holds it . x = r * x; existence ex b1 being Function of I[01],R^1 st for x being Point of I[01] holds b1 . x = r * x proof defpred S1[ real number , set ] means $2 = r * $1; A1: for x being Element of I[01] ex y being Element of the carrier of R^1 st S1[x,y] proof let x be Element of I[01]; ::_thesis: ex y being Element of the carrier of R^1 st S1[x,y] take r * x ; ::_thesis: ( r * x is Element of the carrier of R^1 & S1[x,r * x] ) thus ( r * x is Element of the carrier of R^1 & S1[x,r * x] ) by TOPMETR:17, XREAL_0:def_1; ::_thesis: verum end; ex f being Function of the carrier of I[01], the carrier of R^1 st for x being Element of I[01] holds S1[x,f . x] from FUNCT_2:sch_3(A1); hence ex b1 being Function of I[01],R^1 st for x being Point of I[01] holds b1 . x = r * x ; ::_thesis: verum end; uniqueness for b1, b2 being Function of I[01],R^1 st ( for x being Point of I[01] holds b1 . x = r * x ) & ( for x being Point of I[01] holds b2 . x = r * x ) holds b1 = b2 proof let f, g be Function of I[01],R^1; ::_thesis: ( ( for x being Point of I[01] holds f . x = r * x ) & ( for x being Point of I[01] holds g . x = r * x ) implies f = g ) assume 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 ; ::_thesis: f = g for x being Point of I[01] holds f . x = g . x proof let x be Point of I[01]; ::_thesis: f . x = g . x thus f . x = r * x by A2 .= g . x by A3 ; ::_thesis: verum end; hence f = g by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def1 defines ExtendInt TOPALG_5:def_1_:_ for r being real number for b2 being Function of I[01],R^1 holds ( b2 = ExtendInt r iff for x being Point of I[01] holds b2 . x = r * x ); registration let r be real number ; cluster ExtendInt r -> continuous ; coherence ExtendInt r is continuous 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] for r1 being real number 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]; ::_thesis: g . x = (ExtendInt r) . x thus g . x = r * (f1 . x) by A1 .= r * x by FUNCT_1:18 .= (ExtendInt r) . x by Def1 ; ::_thesis: verum end; hence ExtendInt r is continuous by A2, FUNCT_2:63; ::_thesis: verum end; end; definition let r be real number ; :: original: ExtendInt redefine func ExtendInt r -> Path of R^1 0, R^1 r; coherence ExtendInt r is Path of R^1 0, R^1 r proof thus ExtendInt r is continuous ; :: according to BORSUK_2:def_4 ::_thesis: ( (ExtendInt r) . 0 = R^1 0 & (ExtendInt r) . 1 = R^1 r ) thus (ExtendInt r) . 0 = r * 0 by Def1, BORSUK_1:def_14 .= R^1 0 by TOPREALB:def_2 ; ::_thesis: (ExtendInt r) . 1 = R^1 r thus (ExtendInt r) . 1 = r * 1 by Def1, BORSUK_1:def_15 .= R^1 r by TOPREALB:def_2 ; ::_thesis: verum end; end; definition let S, T, Y be non empty TopSpace; let H be Function of [:S,T:],Y; let t be Point of T; func Prj1 (t,H) -> Function of S,Y means :Def2: :: TOPALG_5:def 2 for s being Point of S holds it . s = H . (s,t); existence ex b1 being Function of S,Y st for s being Point of S holds b1 . s = H . (s,t) proof deffunc H1( Point of S) -> Element of the carrier of Y = 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 = H1(x) from FUNCT_2:sch_4(); take f ; ::_thesis: for s being Point of S holds f . s = H . (s,t) let x be Point of S; ::_thesis: f . x = H . (x,t) thus f . x = H . (x,t) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Function of S,Y st ( for s being Point of S holds b1 . s = H . (s,t) ) & ( for s being Point of S holds b2 . s = H . (s,t) ) holds b1 = b2 proof let f, g be Function of S,Y; ::_thesis: ( ( for s being Point of S holds f . s = H . (s,t) ) & ( for s being Point of S holds g . s = H . (s,t) ) implies f = g ) assume 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) ; ::_thesis: f = g now__::_thesis:_for_s_being_Point_of_S_holds_f_._s_=_g_._s let s be Point of S; ::_thesis: f . s = g . s thus f . s = H . (s,t) by A2 .= g . s by A3 ; ::_thesis: verum end; hence f = g by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def2 defines Prj1 TOPALG_5:def_2_:_ for S, T, Y being non empty TopSpace for H being Function of [:S,T:],Y for t being Point of T for b6 being Function of S,Y holds ( b6 = Prj1 (t,H) iff for s being Point of S holds b6 . s = H . (s,t) ); definition let S, T, Y be non empty TopSpace; let H be Function of [:S,T:],Y; let s be Point of S; func Prj2 (s,H) -> Function of T,Y means :Def3: :: TOPALG_5:def 3 for t being Point of T holds it . t = H . (s,t); existence ex b1 being Function of T,Y st for t being Point of T holds b1 . t = H . (s,t) proof deffunc H1( Point of T) -> Element of the carrier of Y = 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 = H1(x) from FUNCT_2:sch_4(); take f ; ::_thesis: for t being Point of T holds f . t = H . (s,t) let x be Point of T; ::_thesis: f . x = H . (s,x) thus f . x = H . (s,x) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Function of T,Y st ( for t being Point of T holds b1 . t = H . (s,t) ) & ( for t being Point of T holds b2 . t = H . (s,t) ) holds b1 = b2 proof let f, g be Function of T,Y; ::_thesis: ( ( for t being Point of T holds f . t = H . (s,t) ) & ( for t being Point of T holds g . t = H . (s,t) ) implies f = g ) assume 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) ; ::_thesis: f = g now__::_thesis:_for_t_being_Point_of_T_holds_f_._t_=_g_._t let t be Point of T; ::_thesis: f . t = g . t thus f . t = H . (s,t) by A2 .= g . t by A3 ; ::_thesis: verum end; hence f = g by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def3 defines Prj2 TOPALG_5:def_3_:_ for S, T, Y being non empty TopSpace for H being Function of [:S,T:],Y for s being Point of S for b6 being Function of T,Y holds ( b6 = Prj2 (s,H) iff for t being Point of T holds b6 . t = H . (s,t) ); registration let S, T, Y be non empty TopSpace; let H be continuous Function of [:S,T:],Y; let t be Point of T; cluster Prj1 (t,H) -> continuous ; coherence Prj1 (t,H) is continuous proof for p being Point of S for 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; ::_thesis: for 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 ) let V be Subset of Y; ::_thesis: ( (Prj1 (t,H)) . p in V & V is open implies ex W being Subset of S st ( p in W & W is open & (Prj1 (t,H)) .: W c= V ) ) assume A1: ( (Prj1 (t,H)) . p in V & V is open ) ; ::_thesis: ex W being Subset of S st ( p in W & W is open & (Prj1 (t,H)) .: W c= V ) (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 holds ex X1 being Subset of S ex 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 ; ::_thesis: ( p in X1 & X1 is open & (Prj1 (t,H)) .: X1 c= V ) thus p in X1 by A7, A9, ZFMISC_1:87; ::_thesis: ( X1 is open & (Prj1 (t,H)) .: X1 c= V ) thus X1 is open by A10; ::_thesis: (Prj1 (t,H)) .: X1 c= V let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Prj1 (t,H)) .: X1 or x in V ) assume x in (Prj1 (t,H)) .: X1 ; ::_thesis: x in V 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 x in V by A4, A12, A13; ::_thesis: verum end; hence Prj1 (t,H) is continuous by JGRAPH_2:10; ::_thesis: verum end; end; registration let S, T, Y be non empty TopSpace; let H be continuous Function of [:S,T:],Y; let s be Point of S; cluster Prj2 (s,H) -> continuous ; coherence Prj2 (s,H) is continuous proof for p being Point of T for 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; ::_thesis: for 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 ) let V be Subset of Y; ::_thesis: ( (Prj2 (s,H)) . p in V & V is open implies ex W being Subset of T st ( p in W & W is open & (Prj2 (s,H)) .: W c= V ) ) assume A1: ( (Prj2 (s,H)) . p in V & V is open ) ; ::_thesis: ex W being Subset of T st ( p in W & W is open & (Prj2 (s,H)) .: W c= V ) (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 holds ex X1 being Subset of S ex 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 ; ::_thesis: ( p in Y1 & Y1 is open & (Prj2 (s,H)) .: Y1 c= V ) thus p in Y1 by A7, A9, ZFMISC_1:87; ::_thesis: ( Y1 is open & (Prj2 (s,H)) .: Y1 c= V ) thus Y1 is open by A10; ::_thesis: (Prj2 (s,H)) .: Y1 c= V let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Prj2 (s,H)) .: Y1 or x in V ) assume x in (Prj2 (s,H)) .: Y1 ; ::_thesis: x in V 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 x in V by A4, A12, A13; ::_thesis: verum end; hence Prj2 (s,H) is continuous by JGRAPH_2:10; ::_thesis: verum end; end; theorem :: TOPALG_5:18 for T being non empty TopSpace for a, b being Point of T for P, Q being Path of a,b for H being Homotopy of P,Q for t being Point of I[01] st H is continuous holds Prj1 (t,H) is continuous ; theorem :: TOPALG_5:19 for T being non empty TopSpace for a, b being Point of T for P, Q being Path of a,b for H being Homotopy of P,Q for 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 (Tunit_circle 2); Lm11: now__::_thesis:_the_carrier_of_(Tunit_circle_2)_=_Sphere_(|[0,0]|,1) Tunit_circle 2 = Tcircle ((0. (TOP-REAL 2)),1) by TOPREALB:def_7; hence the carrier of (Tunit_circle 2) = Sphere (|[0,0]|,1) by EUCLID:54, TOPREALB:9; ::_thesis: verum end; Lm12: dom CircleMap = REAL by FUNCT_2:def_1, TOPMETR:17; definition let r be real number ; func cLoop r -> Function of I[01],(Tunit_circle 2) means :Def4: :: TOPALG_5:def 4 for x being Point of I[01] holds it . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]|; existence ex b1 being Function of I[01],(Tunit_circle 2) st for x being Point of I[01] holds b1 . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]| proof defpred S1[ real number , 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 the carrier of (Tunit_circle 2) st S1[x,y] proof let x be Element of I[01]; ::_thesis: ex y being Element of the carrier of (Tunit_circle 2) st S1[x,y] set y = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]|; |.(|[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]| - |[0,0]|).| = |.|[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]|.| by EUCLID:54, RLVECT_1:13 .= sqrt (((|[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]| `1) ^2) + ((|[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]| `2) ^2)) by JGRAPH_1:30 .= sqrt (((cos (((2 * PI) * r) * x)) ^2) + ((|[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]| `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 = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]| as Element of the carrier of (Tunit_circle 2) by Lm11, TOPREAL9:9; take y ; ::_thesis: S1[x,y] thus S1[x,y] ; ::_thesis: verum end; ex f being Function of the carrier of I[01], the carrier of (Tunit_circle 2) st for x being Element of I[01] holds S1[x,f . x] from FUNCT_2:sch_3(A1); hence ex b1 being Function of I[01],(Tunit_circle 2) st for x being Point of I[01] holds b1 . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]| ; ::_thesis: verum end; uniqueness for b1, b2 being Function of I[01],(Tunit_circle 2) st ( for x being Point of I[01] holds b1 . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]| ) & ( for x being Point of I[01] holds b2 . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]| ) holds b1 = b2 proof let f, g be Function of I[01],(Tunit_circle 2); ::_thesis: ( ( for x being Point of I[01] holds f . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]| ) & ( for x being Point of I[01] holds g . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]| ) implies f = g ) assume 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))]| ; ::_thesis: f = g for x being Point of I[01] holds f . x = g . x proof let x be Point of I[01]; ::_thesis: f . x = g . x thus f . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]| by A2 .= g . x by A3 ; ::_thesis: verum end; hence f = g by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def4 defines cLoop TOPALG_5:def_4_:_ for r being real number for b2 being Function of I[01],(Tunit_circle 2) holds ( b2 = cLoop r iff for x being Point of I[01] holds b2 . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]| ); theorem Th20: :: TOPALG_5:20 for r being real number holds cLoop r = CircleMap * (ExtendInt r) proof let r be real number ; ::_thesis: cLoop r = CircleMap * (ExtendInt r) for x being Point of I[01] holds (cLoop r) . x = (CircleMap * (ExtendInt r)) . x proof let x be Point of I[01]; ::_thesis: (cLoop r) . x = (CircleMap * (ExtendInt r)) . x 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 ; ::_thesis: verum end; hence cLoop r = CircleMap * (ExtendInt r) by FUNCT_2:63; ::_thesis: verum end; definition let n be Integer; :: original: cLoop redefine func cLoop n -> Loop of c[10] ; coherence cLoop n is Loop of c[10] proof set f = cLoop n; cLoop n = CircleMap * (ExtendInt n) by Th20; hence cLoop n is continuous ; :: according to BORSUK_2:def_4 ::_thesis: ( (cLoop n) . 0 = c[10] & (cLoop n) . 1 = c[10] ) thus (cLoop n) . 0 = |[(cos (((2 * PI) * n) * j0)),(sin (((2 * PI) * n) * j0))]| by Def4 .= c[10] by SIN_COS:31, TOPREALB:def_8 ; ::_thesis: (cLoop n) . 1 = c[10] thus (cLoop n) . 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 ; ::_thesis: verum end; end; begin 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 holds ex D being mutually-disjoint open Subset-Family of R^1 st ( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds f is being_homeomorphism ) ) ) ) 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) holds for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds f is being_homeomorphism ) ) ) & ( U = CircleMap .: ].(1 / 2),(3 / 2).[ implies ( union (IntIntervals ((1 / 2),(3 / 2))) = CircleMap " U & ( for d being Subset of R^1 st d in IntIntervals ((1 / 2),(3 / 2)) holds for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds f is being_homeomorphism ) ) ) ) by TOPREALB:45; take F ; ::_thesis: ( F is Cover of (Tunit_circle 2) & F is open & ( for U being Subset of (Tunit_circle 2) st U in F holds ex D being mutually-disjoint open Subset-Family of R^1 st ( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds f is being_homeomorphism ) ) ) ) thus ( F is Cover of (Tunit_circle 2) & F is open ) by A2; ::_thesis: for U being Subset of (Tunit_circle 2) st U in F holds ex D being mutually-disjoint open Subset-Family of R^1 st ( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds f is being_homeomorphism ) ) let U be Subset of (Tunit_circle 2); ::_thesis: ( U in F implies ex D being mutually-disjoint open Subset-Family of R^1 st ( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds f is being_homeomorphism ) ) ) assume A4: U in F ; ::_thesis: ex D being mutually-disjoint open Subset-Family of R^1 st ( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds f is being_homeomorphism ) ) percases ( U = CircleMap .: ].0,1.[ or U = CircleMap .: ].(1 / 2),(3 / 2).[ ) by A1, A4, TARSKI:def_2; supposeA5: U = CircleMap .: ].0,1.[ ; ::_thesis: ex D being mutually-disjoint open Subset-Family of R^1 st ( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds f is being_homeomorphism ) ) reconsider D = IntIntervals (0,1) as mutually-disjoint open Subset-Family of R^1 by Lm8, TOPREALB:4; take D ; ::_thesis: ( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds f is being_homeomorphism ) ) thus ( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds f is being_homeomorphism ) ) by A3, A5; ::_thesis: verum end; supposeA6: U = CircleMap .: ].(1 / 2),(3 / 2).[ ; ::_thesis: ex D being mutually-disjoint open Subset-Family of R^1 st ( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds f is being_homeomorphism ) ) reconsider D = IntIntervals ((1 / 2),(3 / 2)) as mutually-disjoint open Subset-Family of R^1 by Lm9, TOPREALB:4; take D ; ::_thesis: ( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds f is being_homeomorphism ) ) thus ( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds f is being_homeomorphism ) ) by A3, A6; ::_thesis: verum end; end; end; Lm14: [#] (Sspace 0[01]) = {0} by TEX_2:def_2; Lm15: for r, s being real number for F being Subset-Family of (Closed-Interval-TSpace (r,s)) for C being IntervalCover of F for G being IntervalCoverPts of C st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s holds not G is empty proof let r, s be real number ; ::_thesis: for F being Subset-Family of (Closed-Interval-TSpace (r,s)) for C being IntervalCover of F for G being IntervalCoverPts of C st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s holds not G is empty let F be Subset-Family of (Closed-Interval-TSpace (r,s)); ::_thesis: for C being IntervalCover of F for G being IntervalCoverPts of C st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s holds not G is empty let C be IntervalCover of F; ::_thesis: for G being IntervalCoverPts of C st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s holds not G is empty let G be IntervalCoverPts of C; ::_thesis: ( F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s implies not G is empty ) assume ( F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s ) ; ::_thesis: not G is empty then len G = (len C) + 1 by RCOMP_3:def_3; hence not G is empty by CARD_1:27; ::_thesis: verum end; theorem Th21: :: TOPALG_5:21 for UL being Subset-Family of (Tunit_circle 2) st UL is Cover of (Tunit_circle 2) & UL is open holds for Y being non empty TopSpace for F being continuous Function of [:Y,I[01]:],(Tunit_circle 2) for 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 holds 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 (Tunit_circle 2); ::_thesis: ( UL is Cover of (Tunit_circle 2) & UL is open implies for Y being non empty TopSpace for F being continuous Function of [:Y,I[01]:],(Tunit_circle 2) for 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 holds ex Ui being non empty Subset of (Tunit_circle 2) st ( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) ) ) assume that A1: UL is Cover of (Tunit_circle 2) and A2: UL is open ; ::_thesis: for Y being non empty TopSpace for F being continuous Function of [:Y,I[01]:],(Tunit_circle 2) for 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 holds ex Ui being non empty Subset of (Tunit_circle 2) st ( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) ) let Y be non empty TopSpace; ::_thesis: for F being continuous Function of [:Y,I[01]:],(Tunit_circle 2) for 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 holds ex Ui being non empty Subset of (Tunit_circle 2) st ( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) ) let F be continuous Function of [:Y,I[01]:],(Tunit_circle 2); ::_thesis: for 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 holds ex Ui being non empty Subset of (Tunit_circle 2) st ( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) ) let y be Point of Y; ::_thesis: 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 holds ex Ui being non empty Subset of (Tunit_circle 2) st ( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) ) A3: [#] (Tunit_circle 2) = union UL by A1, SETFAM_1:45; A4: for i being Point of I[01] ex U being non empty open Subset of (Tunit_circle 2) st ( F . [y,i] in U & U in UL ) proof let i be Point of I[01]; ::_thesis: ex U being non empty open Subset of (Tunit_circle 2) st ( F . [y,i] in U & U in UL ) consider U being set such that A5: ( F . [y,i] in U & U in UL ) by A3, TARSKI:def_4; reconsider U = U as non empty open Subset of (Tunit_circle 2) by A2, A5, TOPS_2:def_1; take U ; ::_thesis: ( F . [y,i] in U & U in UL ) thus ( F . [y,i] in U & U in UL ) by A5; ::_thesis: verum end; then ex U being non empty open Subset of (Tunit_circle 2) 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 S1[ set , set ] means ex V being open Subset of (Tunit_circle 2) st ( V in UL1 & F . [y,$1] in V & $2 = V ); A6: for i being Element of the carrier of I[01] ex z being Element of UL1 st S1[i,z] proof let i be Element of the carrier of I[01]; ::_thesis: ex z being Element of UL1 st S1[i,z] ex U being non empty open Subset of (Tunit_circle 2) st ( F . [y,i] in U & U in UL ) by A4; hence ex z being Element of UL1 st S1[i,z] ; ::_thesis: verum end; consider I0 being Function of the carrier of I[01],UL1 such that A7: for i being Element of the carrier of I[01] holds S1[i,I0 . i] from FUNCT_2:sch_3(A6); defpred S2[ set , set ] means ex M being open Subset of Y ex 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 the carrier of I[01] ex z being Subset of [: the carrier of Y, the carrier of I[01]:] st S2[i,z] proof let i be Element of the carrier of I[01]; ::_thesis: ex z being Subset of [: the carrier of Y, the carrier of I[01]:] st S2[i,z] consider V being open Subset of (Tunit_circle 2) 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 holds ex A being Subset of Y ex 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 = A as open Subset of Y by A19; A21: i in B by A16, A18, ZFMISC_1:87; reconsider B = B as non empty open Subset of I[01] by A16, A18, A20, ZFMISC_1:87; 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 [: the carrier of Y, the carrier of I[01]:] by BORSUK_1:def_2; take z ; ::_thesis: S2[i,z] take A ; ::_thesis: ex O being open connected Subset of I[01] st ( y in A & i in O & F .: [:A,O:] c= I0 . i & z = [:A,O:] ) take D ; ::_thesis: ( y in A & i in D & F .: [:A,D:] c= I0 . i & z = [:A,D:] ) thus y in A by A16, A18, ZFMISC_1:87; ::_thesis: ( i in D & F .: [:A,D:] c= I0 . i & z = [:A,D:] ) thus i in D by A21, CONNSP_3:26; ::_thesis: ( F .: [:A,D:] c= I0 . i & z = [:A,D:] ) 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, XBOOLE_1:1; then F .: z c= F .: W by RELAT_1:123; hence F .: [:A,D:] c= I0 . i by A10, A13, XBOOLE_1:1; ::_thesis: z = [:A,D:] thus z = [:A,D:] ; ::_thesis: verum end; consider I1 being Function of the carrier of I[01],(bool [: the carrier of Y, the carrier of I[01]:]) such that A24: for i being Element of the carrier of I[01] holds S2[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]:]; :: according to TOPS_2:def_1 ::_thesis: ( not P in C1 or P is open ) assume P in C1 ; ::_thesis: P is open then consider i being set such that A26: i in dom I1 and A27: I1 . i = P by FUNCT_1:def_3; S2[i,I1 . i] by A24, A26; hence P is open by A27, BORSUK_1:6; ::_thesis: verum end; A28: dom I1 = the carrier of I[01] by FUNCT_2:def_1; [:{y},([#] I[01]):] c= union C1 proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in [:{y},([#] I[01]):] or a in union C1 ) assume a in [:{y},([#] I[01]):] ; ::_thesis: a in union C1 then consider a1, a2 being set 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 = 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 a in union C1 by A31, A32, TARSKI:def_4; ::_thesis: verum 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, COMPTS_1:def_4; 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 ) } ; { M where M is open Subset of Y : ( y in M & ex O being open Subset of I[01] st [:M,O:] in G ) } c= bool the carrier of Y proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { M where M is open Subset of Y : ( y in M & ex O being open Subset of I[01] st [:M,O:] in G ) } or a in bool the carrier of Y ) assume a in { M where M is open Subset of Y : ( y in M & ex O being open Subset of I[01] st [:M,O:] in G ) } ; ::_thesis: a in bool the carrier of Y 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 a in bool the carrier of Y ; ::_thesis: verum end; then reconsider 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 ) } 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 S3[ set , set ] means ex M being open Subset of Y ex O being non empty open Subset of I[01] st ( y in M & p . $1 = [:M,O:] & $2 = M ); A41: for x being set st x in dom p holds ex y being set st ( y in NN & S3[x,y] ) proof let x be set ; ::_thesis: ( x in dom p implies ex y being set st ( y in NN & S3[x,y] ) ) assume x in dom p ; ::_thesis: ex y being set st ( y in NN & S3[x,y] ) then A42: p . x in rng p by FUNCT_1:def_3; then consider i being set 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 ; ::_thesis: ( M in NN & S3[x,M] ) thus ( M in NN & S3[x,M] ) by A39, A42, A44, A45, A46; ::_thesis: verum end; consider p1 being Function of (dom p),NN such that A47: for x being set st x in dom p holds S3[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 set 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 ; :: according to XBOOLE_0:def_10 ::_thesis: NN c= rng p1 let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in NN or a in rng p1 ) assume a in NN ; ::_thesis: a in rng p1 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 set 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 a in rng p1 by A56, A57, A60, A63, FUNCT_1:def_3; ::_thesis: verum end; then A64: NN is finite by A40, A56, FINSET_1:def_1; NN is open proof let a be Subset of Y; :: according to TOPS_2:def_1 ::_thesis: ( not a in NN or a is open ) assume a in NN ; ::_thesis: a is open 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 a is open ; ::_thesis: verum end; then reconsider N = meet NN as open Subset of Y by A64, TOPS_2:20; { O where O is open connected Subset of I[01] : ex M being open Subset of Y st [:M,O:] in G } c= bool the carrier of I[01] proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { O where O is open connected Subset of I[01] : ex M being open Subset of Y st [:M,O:] in G } or a in bool the carrier of I[01] ) assume a in { O where O is open connected Subset of I[01] : ex M being open Subset of Y st [:M,O:] in G } ; ::_thesis: a in bool the carrier of I[01] 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 a in bool the carrier of I[01] ; ::_thesis: verum end; then reconsider ICOV = { O where O is open connected Subset of I[01] : ex M being open Subset of Y st [:M,O:] in G } as Subset-Family of (Closed-Interval-TSpace (0,1)) by TOPMETR:20; [#] (Closed-Interval-TSpace (0,1)) c= union ICOV proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in [#] (Closed-Interval-TSpace (0,1)) or a in union ICOV ) assume a in [#] (Closed-Interval-TSpace (0,1)) ; ::_thesis: a in union ICOV then reconsider a = 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 set 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 a in union ICOV by TARSKI:def_4; ::_thesis: verum end; then A70: ICOV is Cover of (Closed-Interval-TSpace (0,1)) by SETFAM_1:def_11; set NCOV = the IntervalCover of ICOV; set T = the IntervalCoverPts of the IntervalCover of ICOV; A71: ICOV is connected proof let X be Subset of (Closed-Interval-TSpace (0,1)); :: according to RCOMP_3:def_1 ::_thesis: ( not X in ICOV or X is connected ) assume X in ICOV ; ::_thesis: X is connected 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 X is connected by TOPMETR:20; ::_thesis: verum end; A72: ICOV is open proof let a be Subset of (Closed-Interval-TSpace (0,1)); :: according to TOPS_2:def_1 ::_thesis: ( not a in ICOV or a is open ) assume a in ICOV ; ::_thesis: a is open 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 a is open by TOPMETR:20; ::_thesis: verum end; then reconsider T = the IntervalCoverPts of the IntervalCover of ICOV as non empty FinSequence of REAL by A70, A71, Lm15; take T ; ::_thesis: ( 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 holds ex Ui being non empty Subset of (Tunit_circle 2) st ( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) ) thus ( T . 1 = 0 & T . (len T) = 1 ) by A70, A72, A71, RCOMP_3:def_3; ::_thesis: ( 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 holds ex Ui being non empty Subset of (Tunit_circle 2) st ( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) ) thus T is increasing by A70, A72, A71, RCOMP_3:65; ::_thesis: 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 holds ex Ui being non empty Subset of (Tunit_circle 2) st ( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) take N ; ::_thesis: ( y in N & ( for i being Nat st i in dom T & i + 1 in dom T holds ex Ui being non empty Subset of (Tunit_circle 2) st ( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) now__::_thesis:_for_Z_being_set_st_Z_in_NN_holds_ y_in_Z let Z be set ; ::_thesis: ( Z in NN implies y in Z ) assume Z in NN ; ::_thesis: y in Z 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 ; ::_thesis: verum end; hence y in N by A55, SETFAM_1:def_1; ::_thesis: for i being Nat st i in dom T & i + 1 in dom T holds ex Ui being non empty Subset of (Tunit_circle 2) st ( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) let i be Nat; ::_thesis: ( i in dom T & i + 1 in dom T implies ex Ui being non empty Subset of (Tunit_circle 2) st ( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) assume that A73: i in dom T and A74: i + 1 in dom T ; ::_thesis: ex Ui being non empty Subset of (Tunit_circle 2) st ( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) A75: 1 <= i by A73, FINSEQ_3:25; A76: i + 1 <= len T by A74, FINSEQ_3:25; len T = (len the IntervalCover of ICOV) + 1 by A70, A72, A71, RCOMP_3:def_3; then i <= len the IntervalCover of ICOV by A76, XREAL_1:6; then i in dom the IntervalCover of ICOV by A75, FINSEQ_3:25; then A77: the IntervalCover of ICOV . i in rng the IntervalCover of ICOV by FUNCT_1:def_3; rng the IntervalCover of ICOV c= ICOV by A70, A72, A71, RCOMP_3:def_2; then the IntervalCover of ICOV . i in ICOV by A77; then consider O being open connected Subset of I[01] such that A78: the IntervalCover of ICOV . 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 set 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 (Tunit_circle 2) such that A84: V in UL1 and A85: F . [y,j] in V and A86: I0 . j = V by A7, A82; reconsider V = V as non empty open Subset of (Tunit_circle 2) by A85; take V ; ::_thesis: ( V in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= V ) thus V in UL by A84; ::_thesis: F .: [:N,[.(T . i),(T . (i + 1)).]:] c= V 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 F .: [:N,[.(T . i),(T . (i + 1)).]:] c= V by A89, A86, XBOOLE_1:1; ::_thesis: verum end; theorem Th22: :: TOPALG_5:22 for Y being non empty TopSpace for F being Function of [:Y,I[01]:],(Tunit_circle 2) for 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 holds 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 (Tunit_circle 2) such that A1: ( UL is Cover of (Tunit_circle 2) & UL is open ) and A2: for U being Subset of (Tunit_circle 2) st U in UL holds ex D being mutually-disjoint open Subset-Family of R^1 st ( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds f is being_homeomorphism ) ) by Lm13; let Y be non empty TopSpace; ::_thesis: for F being Function of [:Y,I[01]:],(Tunit_circle 2) for 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 holds 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 ) ) let F be Function of [:Y,I[01]:],(Tunit_circle 2); ::_thesis: for 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 holds 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 ) ) let Ft be Function of [:Y,(Sspace 0[01]):],R^1; ::_thesis: ( F is continuous & Ft is continuous & F | [: the carrier of Y,{0}:] = CircleMap * Ft implies 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 ) ) ) assume that A3: F is continuous and A4: Ft is continuous and A5: F | [: the carrier of Y,{0}:] = CircleMap * Ft ; ::_thesis: 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 ) ) defpred S1[ set , set ] means ex y being Point of Y ex t being Point of I[01] ex N being non empty open Subset of Y ex 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, the carrier of I[01]:] = CircleMap * Fn & Fn | [: the carrier of Y,{0}:] = Ft | [:N, the carrier of I[01]:] & ( for H being Function of [:(Y | N),I[01]:],R^1 st H is continuous & F | [:N, the carrier of I[01]:] = CircleMap * H & H | [: the carrier of Y,{0}:] = Ft | [:N, the carrier of I[01]:] holds Fn = H ) ); A6: dom F = the carrier of [:Y,I[01]:] by FUNCT_2:def_1 .= [: the carrier of Y, the carrier of I[01]:] 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 S1[x,z] proof let x be Point of [:Y,I[01]:]; ::_thesis: ex z being Point of R^1 st S1[x,z] 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 holds 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 holds 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 = N as non empty open Subset of Y by A15; defpred S2[ Element of NAT ] means ( $1 in dom TT implies ex N2 being non empty open Subset of Y ex S being non empty Subset of I[01] ex 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, the carrier of I[01]:] ) ); A17: len TT in dom TT by FINSEQ_5:6; A18: 1 in dom TT by FINSEQ_5:6; A19: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_TT_holds_ (_0_<=_TT_._i_&_(_i_+_1_in_dom_TT_implies_(_TT_._i_<_TT_._(i_+_1)_&_TT_._(i_+_1)_<=_1_&_TT_._i_<_1_&_0_<_TT_._(i_+_1)_)_)_) let i be Element of NAT ; ::_thesis: ( i in dom TT implies ( 0 <= TT . i & ( i + 1 in dom TT implies ( TT . i < TT . (i + 1) & TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 1) ) ) ) ) assume A20: i in dom TT ; ::_thesis: ( 0 <= TT . i & ( i + 1 in dom TT implies ( TT . i < TT . (i + 1) & TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 1) ) ) ) 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; ::_thesis: ( i + 1 in dom TT implies ( TT . i < TT . (i + 1) & TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 1) ) ) assume A22: i + 1 in dom TT ; ::_thesis: ( TT . i < TT . (i + 1) & TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 1) ) A23: i + 0 < i + 1 by XREAL_1:8; hence A24: TT . i < TT . (i + 1) by A13, A20, A22, SEQM_3:def_1; ::_thesis: ( TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 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; ::_thesis: ( TT . i < 1 & 0 < TT . (i + 1) ) hence TT . i < 1 by A24, XXREAL_0:2; ::_thesis: 0 < TT . (i + 1) thus 0 < TT . (i + 1) by A13, A20, A21, A22, A23, SEQM_3:def_1; ::_thesis: verum end; A25: now__::_thesis:_for_i_being_Element_of_NAT_st_0_<=_TT_._i_&_TT_._(i_+_1)_<=_1_holds_ [.(TT_._i),(TT_._(i_+_1)).]_c=_the_carrier_of_I[01] let i be Element of NAT ; ::_thesis: ( 0 <= TT . i & TT . (i + 1) <= 1 implies [.(TT . i),(TT . (i + 1)).] c= the carrier of I[01] ) assume that A26: 0 <= TT . i and A27: TT . (i + 1) <= 1 ; ::_thesis: [.(TT . i),(TT . (i + 1)).] c= the carrier of I[01] thus [.(TT . i),(TT . (i + 1)).] c= the carrier of I[01] ::_thesis: verum proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in [.(TT . i),(TT . (i + 1)).] or a in the carrier of I[01] ) assume A28: a in [.(TT . i),(TT . (i + 1)).] ; ::_thesis: a in the carrier of I[01] then reconsider a = 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 a in the carrier of I[01] by A29, BORSUK_1:43; ::_thesis: verum end; end; A30: for i being Element of NAT st S2[i] holds S2[i + 1] proof let i be Element of NAT ; ::_thesis: ( S2[i] implies S2[i + 1] ) assume that A31: S2[i] and A32: i + 1 in dom TT ; ::_thesis: ex N2 being non empty open Subset of Y ex S being non empty Subset of I[01] ex Fn being Function of [:(Y | N2),(I[01] | S):],R^1 st ( S = [.0,(TT . (i + 1)).] & y in N2 & N2 c= N & Fn is continuous & F | [:N2,S:] = CircleMap * Fn & Fn | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] ) percases ( i = 0 or i in dom TT ) by A32, TOPREALA:2; supposeA33: i = 0 ; ::_thesis: ex N2 being non empty open Subset of Y ex S being non empty Subset of I[01] ex Fn being Function of [:(Y | N2),(I[01] | S):],R^1 st ( S = [.0,(TT . (i + 1)).] & y in N2 & N2 c= N & Fn is continuous & F | [:N2,S:] = CircleMap * Fn & Fn | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] ) take N2 = N; ::_thesis: ex S being non empty Subset of I[01] ex Fn being Function of [:(Y | N2),(I[01] | S):],R^1 st ( S = [.0,(TT . (i + 1)).] & y in N2 & N2 c= N & Fn is continuous & F | [:N2,S:] = CircleMap * Fn & Fn | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] ) set Fn = Ft | [:N2,{0}:]; set S = [.0,(TT . (i + 1)).]; A34: [.0,(TT . (i + 1)).] = {0} by A11, A33, XXREAL_1:17; reconsider S = [.0,(TT . (i + 1)).] as non empty Subset of I[01] by A11, A33, Lm3, XXREAL_1:17; A35: dom (Ft | [:N2,{0}:]) = [: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 (Ft | [:N2,{0}:]) c= the carrier of R^1 ) 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 = Ft | [:N2,{0}:] 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 ; ::_thesis: ex Fn being Function of [:(Y | N2),(I[01] | S):],R^1 st ( S = [.0,(TT . (i + 1)).] & y in N2 & N2 c= N & Fn is continuous & F | [:N2,S:] = CircleMap * Fn & Fn | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] ) take Fn ; ::_thesis: ( S = [.0,(TT . (i + 1)).] & y in N2 & N2 c= N & Fn is continuous & F | [:N2,S:] = CircleMap * Fn & Fn | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] ) thus S = [.0,(TT . (i + 1)).] ; ::_thesis: ( y in N2 & N2 c= N & Fn is continuous & F | [:N2,S:] = CircleMap * Fn & Fn | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] ) thus y in N2 by A15; ::_thesis: ( N2 c= N & Fn is continuous & F | [:N2,S:] = CircleMap * Fn & Fn | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] ) thus N2 c= N ; ::_thesis: ( Fn is continuous & F | [:N2,S:] = CircleMap * Fn & Fn | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] ) 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; ::_thesis: ( F | [:N2,S:] = CircleMap * Fn & Fn | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] ) 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 set st x in dom (F | [:N2,S:]) holds (F | [:N2,S:]) . x = (CircleMap * Fn) . x proof let x be set ; ::_thesis: ( x in dom (F | [:N2,S:]) implies (F | [:N2,S:]) . x = (CircleMap * Fn) . x ) assume A40: x in dom (F | [:N2,S:]) ; ::_thesis: (F | [:N2,S:]) . x = (CircleMap * Fn) . x 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 ; ::_thesis: verum end; hence F | [:N2,S:] = CircleMap * Fn by A35, A37, A38, FUNCT_1:2; ::_thesis: Fn | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] A41: dom (Fn | [: the carrier of Y,{0}:]) = [:N2,S:] /\ [: the carrier of Y,{0}:] by A35, RELAT_1:61; A42: for x being set st x in dom (Fn | [: the carrier of Y,{0}:]) holds (Fn | [: the carrier of Y,{0}:]) . x = (Ft | [:N2, the carrier of I[01]:]) . x proof A43: [:N2,{0}:] c= [:N2, the carrier of I[01]:] by Lm3, ZFMISC_1:95; let x be set ; ::_thesis: ( x in dom (Fn | [: the carrier of Y,{0}:]) implies (Fn | [: the carrier of Y,{0}:]) . x = (Ft | [:N2, the carrier of I[01]:]) . x ) assume A44: x in dom (Fn | [: the carrier of Y,{0}:]) ; ::_thesis: (Fn | [: the carrier of Y,{0}:]) . x = (Ft | [:N2, the carrier of I[01]:]) . x 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, the carrier of I[01]:]) . x by A45, A43, FUNCT_1:49 ; ::_thesis: verum end; dom (Ft | [:N2, the carrier of I[01]:]) = [: the carrier of Y,{0}:] /\ [:N2, the carrier of I[01]:] by A8, RELAT_1:61 .= [:N2,S:] by A34, ZFMISC_1:101 ; hence Fn | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] by A34, A41, A42, FUNCT_1:2, ZFMISC_1:101; ::_thesis: verum end; supposeA46: i in dom TT ; ::_thesis: ex N2 being non empty open Subset of Y ex S being non empty Subset of I[01] ex Fn being Function of [:(Y | N2),(I[01] | S):],R^1 st ( S = [.0,(TT . (i + 1)).] & y in N2 & N2 c= N & Fn is continuous & F | [:N2,S:] = CircleMap * Fn & Fn | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] ) set SS = [.(TT . i),(TT . (i + 1)).]; consider Ui being non empty Subset of (Tunit_circle 2) such that A47: Ui in UL and A48: F .: [:N,[.(TT . i),(TT . (i + 1)).]:] 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 holds for f being Function of (R^1 | d),((Tunit_circle 2) | Ui) st f = CircleMap | d holds f is being_homeomorphism by A2, A47; A51: the carrier of ((Tunit_circle 2) | Ui) = Ui by PRE_TOPC:8; A52: TT . i < TT . (i + 1) by A19, A32, A46; then TT . i in [.(TT . i),(TT . (i + 1)).] by XXREAL_1:1; then A53: [y,(TT . i)] in [:N,[.(TT . i),(TT . (i + 1)).]:] 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, the carrier of I[01]:] by A31, A46; reconsider N2 = 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 (Fn | [:N2,Ti:]) c= REAL ) by BORSUK_1:def_2, TOPMETR:17; A66: [:N2,[.(TT . i),(TT . (i + 1)).]:] c= [:N,[.(TT . i),(TT . (i + 1)).]:] 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 (Fn | [:N2,Ti:]) = [: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 = Fn | [:N2,Ti:] 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; [y,(TT . i)] in dom F by A6, A63, ZFMISC_1:87; then A72: F . [y,(TT . i)] in F .: [:N,[.(TT . i),(TT . (i + 1)).]:] by A53, FUNCT_2:35; A73: [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, A73, FUNCT_2:15 ; then Fn . [y,(TT . i)] in CircleMap " Ui by A48, A72, FUNCT_2:38, TOPMETR:17; then consider Uit being set such that A74: Fn . [y,(TT . i)] in Uit and A75: Uit in D by A49, TARSKI:def_4; reconsider Uit = Uit as non empty Subset of R^1 by A74, A75; ( [#] R^1 <> {} & Uit is open ) by A75, 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 A76: FnT " Uit = union SF and A77: for e being set st e in SF holds ex X1 being Subset of (Y | N2) ex Y1 being Subset of (I[01] | Ti) st ( e = [:X1,Y1:] & X1 is open & Y1 is open ) by BORSUK_1:5; A78: TT . i in {(TT . i)} by TARSKI:def_1; then A79: [y,(TT . i)] in [:N2,{(TT . i)}:] by A55, ZFMISC_1:def_2; then FnT . [y,(TT . i)] in Uit by A74, FUNCT_1:49; then [y,(TT . i)] in FnT " Uit by A79, A68, FUNCT_1:def_7; then consider N5 being set such that A80: [y,(TT . i)] in N5 and A81: N5 in SF by A76, TARSKI:def_4; set f = CircleMap | Uit; A82: dom (CircleMap | Uit) = Uit by Lm12, RELAT_1:62, TOPMETR:17; A83: rng (CircleMap | Uit) c= Ui proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in rng (CircleMap | Uit) or b in Ui ) assume b in rng (CircleMap | Uit) ; ::_thesis: b in Ui then consider a being set such that A84: a in dom (CircleMap | Uit) and A85: (CircleMap | Uit) . a = b by FUNCT_1:def_3; a in union D by A75, A82, A84, TARSKI:def_4; then CircleMap . a in Ui by A49, FUNCT_2:38; hence b in Ui by A82, A84, A85, FUNCT_1:49; ::_thesis: verum end; consider X1 being Subset of (Y | N2), Y1 being Subset of (I[01] | Ti) such that A86: N5 = [:X1,Y1:] and A87: X1 is open and Y1 is open by A77, A81; the carrier of (R^1 | Uit) = Uit by PRE_TOPC:8; then reconsider f = CircleMap | Uit as Function of (R^1 | Uit),((Tunit_circle 2) | Ui) by A51, A82, A83, FUNCT_2:2; consider NY being Subset of Y such that A88: NY is open and A89: NY /\ ([#] (Y | N2)) = X1 by A87, TOPS_2:24; consider y1, y2 being set such that A90: y1 in X1 and A91: y2 in Y1 and A92: [y,(TT . i)] = [y1,y2] by A80, A86, ZFMISC_1:def_2; set N1 = NY /\ N2; y = y1 by A92, XTUPLE_0:1; then A93: y in NY by A89, A90, XBOOLE_0:def_4; then reconsider N1 = NY /\ N2 as non empty open Subset of Y by A55, A88, XBOOLE_0:def_4; A94: N1 c= N2 by XBOOLE_1:17; then [:N1,[.(TT . i),(TT . (i + 1)).]:] c= [:N2,[.(TT . i),(TT . (i + 1)).]:] by ZFMISC_1:96; then [:N1,[.(TT . i),(TT . (i + 1)).]:] c= [:N,[.(TT . i),(TT . (i + 1)).]:] by A66, XBOOLE_1:1; then A95: F .: [:N1,[.(TT . i),(TT . (i + 1)).]:] c= F .: [:N,[.(TT . i),(TT . (i + 1)).]:] by RELAT_1:123; TT . (i + 1) <= 1 by A19, A32, A46; then reconsider SS = [.(TT . i),(TT . (i + 1)).] as non empty Subset of I[01] by A25, A62, A52, XXREAL_1:1; A96: 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, A75, TOPS_2:56; then A97: dom (f ") = [#] ((Tunit_circle 2) | Ui) by TOPS_2:def_5; A98: rng (F | [:N1,SS:]) c= dom (f ") proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in rng (F | [:N1,SS:]) or b in dom (f ") ) assume b in rng (F | [:N1,SS:]) ; ::_thesis: b in dom (f ") then consider a being set such that A99: a in dom (F | [:N1,SS:]) and A100: (F | [:N1,SS:]) . a = b by FUNCT_1:def_3; b = F . a by A96, A99, A100, FUNCT_1:49; then b in F .: [:N1,SS:] by A96, A99, FUNCT_2:35; then b in F .: [:N,SS:] by A95; then b in Ui by A48; hence b in dom (f ") by A97, PRE_TOPC:8; ::_thesis: verum end; then A101: dom ((f ") * (F | [:N1,SS:])) = dom (F | [:N1,SS:]) by RELAT_1:27; set Fn2 = Fn | [:N1,S:]; A102: the carrier of (Y | N1) = N1 by PRE_TOPC:8; then A103: [:N1,S:] = the carrier of [:(Y | N1),(I[01] | S):] by A64, BORSUK_1:def_2; then A104: dom (Fn | [:N1,S:]) = the carrier of [:(Y | N1),(I[01] | S):] by A64, A60, A67, A61, A94, RELAT_1:62, ZFMISC_1:96; reconsider ff = f as Function ; A105: f is being_homeomorphism by A50, A75; then A106: f is one-to-one by TOPS_2:def_5; A107: rng (Fn | [:N1,S:]) c= the carrier of R^1 ; the carrier of (R^1 | Uit) is Subset of R^1 by TSEP_1:1; then A108: rng ((f ") * (F | [:N1,SS:])) c= the carrier of R^1 by XBOOLE_1:1; A109: the carrier of (I[01] | SS) = SS by PRE_TOPC:8; then A110: [:N1,SS:] = the carrier of [:(Y | N1),(I[01] | SS):] by A102, BORSUK_1:def_2; then reconsider Fni1 = (f ") * (F | [:N1,SS:]) as Function of [:(Y | N1),(I[01] | SS):],R^1 by A96, A101, A108, FUNCT_2:2; set Fn1 = (Fn | [:N1,S:]) +* Fni1; reconsider Fn2 = Fn | [:N1,S:] as Function of [:(Y | N1),(I[01] | S):],R^1 by A104, A107, FUNCT_2:2; A111: rng ((Fn | [:N1,S:]) +* Fni1) c= (rng (Fn | [:N1,S:])) \/ (rng Fni1) by FUNCT_4:17; dom (Fn | [:N1,S:]) = [:N1,S:] by A64, A60, A67, A61, A94, RELAT_1:62, ZFMISC_1:96; then A112: dom ((Fn | [:N1,S:]) +* Fni1) = [:N1,S:] \/ [:N1,SS:] by A96, A101, FUNCT_4:def_1; A113: rng f = [#] ((Tunit_circle 2) | Ui) by A105, TOPS_2:def_5; then f is onto by FUNCT_2:def_3; then A114: f " = ff " by A106, TOPS_2:def_4; A115: Y1 = Ti proof thus Y1 c= Ti by A70; :: according to XBOOLE_0:def_10 ::_thesis: Ti c= Y1 let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Ti or a in Y1 ) assume a in Ti ; ::_thesis: a in Y1 then a = TT . i by TARSKI:def_1; hence a in Y1 by A91, A92, XTUPLE_0:1; ::_thesis: verum end; A116: Fn .: [:N1,{(TT . i)}:] c= Uit proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Fn .: [:N1,{(TT . i)}:] or b in Uit ) assume b in Fn .: [:N1,{(TT . i)}:] ; ::_thesis: b in Uit then consider a being Point of [:(Y | N2),(I[01] | S):] such that A117: a in [:N1,{(TT . i)}:] and A118: Fn . a = b by FUNCT_2:65; a in N5 by A86, A89, A115, A117, PRE_TOPC:def_5; then A119: a in union SF by A81, TARSKI:def_4; then a in dom FnT by A76, FUNCT_1:def_7; then Fn . a = FnT . a by FUNCT_1:47; hence b in Uit by A76, A118, A119, FUNCT_1:def_7; ::_thesis: verum end; A120: for p being set st p in ([#] [:(Y | N1),(I[01] | S):]) /\ ([#] [:(Y | N1),(I[01] | SS):]) holds Fn2 . p = Fni1 . p proof A121: the carrier of (Y | N2) = N2 by PRE_TOPC:8; let p be set ; ::_thesis: ( p in ([#] [:(Y | N1),(I[01] | S):]) /\ ([#] [:(Y | N1),(I[01] | SS):]) implies Fn2 . p = Fni1 . p ) assume A122: p in ([#] [:(Y | N1),(I[01] | S):]) /\ ([#] [:(Y | N1),(I[01] | SS):]) ; ::_thesis: Fn2 . p = Fni1 . p A123: p in ([#] [:(Y | N1),(I[01] | SS):]) /\ ([#] [:(Y | N1),(I[01] | S):]) by A122; then A124: Fn . p = Fn2 . p by A103, FUNCT_1:49; [:N1,S:] /\ [:N1,SS:] = [:N1,(S /\ SS):] by ZFMISC_1:99; then A125: p in [:N1,{(TT . i)}:] by A54, A62, A52, A110, A103, A122, XXREAL_1:418; then consider p1 being Element of N1, p2 being Element of {(TT . i)} such that A126: p = [p1,p2] by DOMAIN_1:1; A127: p1 in N1 ; S /\ SS = {(TT . i)} by A54, A62, A52, XXREAL_1:418; then p2 in S by XBOOLE_0:def_4; then A128: p in [:N2,S:] by A94, A126, A127, ZFMISC_1:def_2; then A129: Fn . p in Fn .: [:N1,{(TT . i)}:] by A64, A60, A67, A125, FUNCT_2:35; (F | [:N1,SS:]) . p = F . p by A110, A122, FUNCT_1:49 .= (F | [:N2,S:]) . p by A128, FUNCT_1:49 .= CircleMap . (Fn . p) by A58, A64, A60, A61, A121, A128, FUNCT_1:13 .= (CircleMap | Uit) . (Fn . p) by A116, A129, FUNCT_1:49 .= ff . (Fn2 . p) by A103, A123, FUNCT_1:49 ; hence Fn2 . p = (ff ") . ((F | [:N1,SS:]) . p) by A116, A82, A106, A124, A129, FUNCT_1:32 .= Fni1 . p by A114, A96, A110, A122, FUNCT_1:13 ; ::_thesis: verum end; A130: [:N1,S:] c= [:N2,S:] by A94, ZFMISC_1:96; then reconsider K0 = [:N1,S:] as Subset of [:(Y | N2),(I[01] | S):] by A64, A60, PRE_TOPC:8; A131: [:N1,SS:] c= dom F by A6, ZFMISC_1:96; reconsider gF = F | [:N1,SS:] as Function of [:(Y | N1),(I[01] | SS):],(Tunit_circle 2) by A96, A98, A110, FUNCT_2:2; reconsider fF = F | [:N1,SS:] as Function of [:(Y | N1),(I[01] | SS):],((Tunit_circle 2) | Ui) by A97, A96, A98, A110, 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 A132: fF is continuous by TOPMETR:6; f " is continuous by A105, TOPS_2:def_5; then (f ") * fF is continuous by A132; then A133: Fni1 is continuous by PRE_TOPC:26; reconsider aN1 = N1 as non empty Subset of (Y | N2) by A94, 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 A134: Fn2 is continuous by A57, TOPMETR:7; take N1 ; ::_thesis: ex S being non empty Subset of I[01] ex Fn being Function of [:(Y | N1),(I[01] | S):],R^1 st ( S = [.0,(TT . (i + 1)).] & y in N1 & N1 c= N & Fn is continuous & F | [:N1,S:] = CircleMap * Fn & Fn | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:] ) take S1 = S \/ SS; ::_thesis: ex Fn being Function of [:(Y | N1),(I[01] | S1):],R^1 st ( S1 = [.0,(TT . (i + 1)).] & y in N1 & N1 c= N & Fn is continuous & F | [:N1,S1:] = CircleMap * Fn & Fn | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:] ) A135: [:N1,S:] \/ [:N1,SS:] = [:N1,S1:] by ZFMISC_1:97; A136: the carrier of (I[01] | S1) = S1 by PRE_TOPC:8; then [:N1,S1:] = the carrier of [:(Y | N1),(I[01] | S1):] by A102, BORSUK_1:def_2; then reconsider Fn1 = (Fn | [:N1,S:]) +* Fni1 as Function of [:(Y | N1),(I[01] | S1):],R^1 by A135, A112, A111, FUNCT_2:2, XBOOLE_1:1; take Fn1 ; ::_thesis: ( S1 = [.0,(TT . (i + 1)).] & y in N1 & N1 c= N & Fn1 is continuous & F | [:N1,S1:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:] ) thus A137: S1 = [.0,(TT . (i + 1)).] by A54, A62, A52, XXREAL_1:165; ::_thesis: ( y in N1 & N1 c= N & Fn1 is continuous & F | [:N1,S1:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:] ) 0 <= TT . (i + 1) by A19, A32; then 0 in S1 by A137, XXREAL_1:1; then A138: {0} c= S1 by ZFMISC_1:31; A139: dom (Fn1 | [: the carrier of Y,{0}:]) = (dom Fn1) /\ [: the carrier of Y,{0}:] by RELAT_1:61; then A140: dom (Fn1 | [: the carrier of Y,{0}:]) = [:(N1 /\ the carrier of Y),(S1 /\ {0}):] by A135, A112, ZFMISC_1:100 .= [:N1,(S1 /\ {0}):] by XBOOLE_1:28 .= [:N1,{0}:] by A138, XBOOLE_1:28 ; A141: for a being set st a in dom (Fn1 | [: the carrier of Y,{0}:]) holds (Fn1 | [: the carrier of Y,{0}:]) . a = (Ft | [:N1, the carrier of I[01]:]) . a proof let a be set ; ::_thesis: ( a in dom (Fn1 | [: the carrier of Y,{0}:]) implies (Fn1 | [: the carrier of Y,{0}:]) . a = (Ft | [:N1, the carrier of I[01]:]) . a ) A142: [:N1, the carrier of I[01]:] c= [:N2, the carrier of I[01]:] by A94, ZFMISC_1:96; assume A143: a in dom (Fn1 | [: the carrier of Y,{0}:]) ; ::_thesis: (Fn1 | [: the carrier of Y,{0}:]) . a = (Ft | [:N1, the carrier of I[01]:]) . a then A144: a in [: the carrier of Y,{0}:] by A139, XBOOLE_0:def_4; then consider a1, a2 being set such that a1 in the carrier of Y and A145: a2 in {0} and A146: a = [a1,a2] by ZFMISC_1:def_2; A147: a2 = 0 by A145, TARSKI:def_1; 0 in S by A54, A62, XXREAL_1:1; then {0} c= S by ZFMISC_1:31; then A148: [:N1,{0}:] c= [:N1,S:] by ZFMISC_1:96; then A149: a in [:N1,S:] by A140, A143; A150: [:N1,S:] c= [:N1, the carrier of I[01]:] by ZFMISC_1:96; then A151: a in [:N1, the carrier of I[01]:] by A149; percases ( not a in dom Fni1 or a in dom Fni1 ) ; supposeA152: not a in dom Fni1 ; ::_thesis: (Fn1 | [: the carrier of Y,{0}:]) . a = (Ft | [:N1, the carrier of I[01]:]) . a thus (Fn1 | [: the carrier of Y,{0}:]) . a = Fn1 . a by A144, FUNCT_1:49 .= (Fn | [:N1,S:]) . a by A152, FUNCT_4:11 .= Fn . a by A140, A143, A148, FUNCT_1:49 .= (Ft | [:N2, the carrier of I[01]:]) . a by A59, A144, FUNCT_1:49 .= Ft . a by A151, A142, FUNCT_1:49 .= (Ft | [:N1, the carrier of I[01]:]) . a by A149, A150, FUNCT_1:49 ; ::_thesis: verum end; supposeA153: a in dom Fni1 ; ::_thesis: (Fn1 | [: the carrier of Y,{0}:]) . a = (Ft | [:N1, the carrier of I[01]:]) . a set e = (Ft | [:N1, the carrier of I[01]:]) . a; a in [:N1,SS:] by A6, A101, A153, RELAT_1:62, ZFMISC_1:96; then consider b1, b2 being set such that A154: b1 in N1 and A155: b2 in SS and A156: a = [b1,b2] by ZFMISC_1:def_2; a2 = b2 by A146, A156, XTUPLE_0:1; then A157: a2 = TT . i by A62, A147, A155, XXREAL_1:1; a1 = b1 by A146, A156, XTUPLE_0:1; then A158: ( [a1,(TT . i)] in [:N1,S:] & [a1,(TT . i)] in [:N1,{(TT . i)}:] ) by A63, A78, A154, ZFMISC_1:87; (Ft | [:N1, the carrier of I[01]:]) . a = Ft . a by A149, A150, FUNCT_1:49 .= (Ft | [:N2, the carrier of I[01]:]) . a by A151, A142, FUNCT_1:49 .= Fn . a by A59, A144, FUNCT_1:49 ; then A159: (Ft | [:N1, the carrier of I[01]:]) . a in Fn .: [:N1,{(TT . i)}:] by A64, A60, A67, A61, A130, A146, A157, A158, FUNCT_1:def_6; then A160: ff . ((Ft | [:N1, the carrier of I[01]:]) . a) = CircleMap . ((Ft | [:N1, the carrier of I[01]:]) . a) by A116, FUNCT_1:49 .= CircleMap . (Ft . a) by A149, A150, FUNCT_1:49 .= (CircleMap * Ft) . a by A8, A144, FUNCT_1:13 .= F . a by A5, A144, FUNCT_1:49 ; thus (Fn1 | [: the carrier of Y,{0}:]) . a = Fn1 . a by A144, FUNCT_1:49 .= Fni1 . a by A153, FUNCT_4:13 .= (ff ") . ((F | [:N1,SS:]) . a) by A114, A101, A153, FUNCT_1:13 .= (ff ") . (F . a) by A96, A101, A153, FUNCT_1:49 .= (Ft | [:N1, the carrier of I[01]:]) . a by A116, A82, A106, A159, A160, FUNCT_1:32 ; ::_thesis: verum end; end; end; A161: rng Fn1 c= dom CircleMap by Lm12, TOPMETR:17; then A162: dom (CircleMap * Fn1) = dom Fn1 by RELAT_1:27; A163: for a being set st a in dom (CircleMap * Fn1) holds (CircleMap * Fn1) . a = F . a proof let a be set ; ::_thesis: ( a in dom (CircleMap * Fn1) implies (CircleMap * Fn1) . a = F . a ) assume A164: a in dom (CircleMap * Fn1) ; ::_thesis: (CircleMap * Fn1) . a = F . a percases ( a in dom Fni1 or not a in dom Fni1 ) ; supposeA165: a in dom Fni1 ; ::_thesis: (CircleMap * Fn1) . a = F . a A166: [:N1,SS:] c= [: the carrier of Y, the carrier of I[01]:] by ZFMISC_1:96; A167: a in [:N1,SS:] by A6, A101, A165, RELAT_1:62, ZFMISC_1:96; then F . a in F .: [:N1,SS:] by A6, A166, FUNCT_1:def_6; then A168: F . a in F .: [:N,SS:] by A95; then a in F " (dom (ff ")) by A6, A48, A51, A97, A114, A167, A166, FUNCT_1:def_7; then A169: a in dom ((ff ") * F) by RELAT_1:147; thus (CircleMap * Fn1) . a = CircleMap . (Fn1 . a) by A164, FUNCT_2:15 .= CircleMap . (Fni1 . a) by A165, FUNCT_4:13 .= CircleMap . ((f ") . ((F | [:N1,SS:]) . a)) by A101, A165, FUNCT_1:13 .= CircleMap . ((f ") . (F . a)) by A96, A101, A165, FUNCT_1:49 .= CircleMap . (((ff ") * F) . a) by A131, A114, A96, A101, A165, FUNCT_1:13 .= (CircleMap * ((ff ") * F)) . a by A169, FUNCT_1:13 .= ((CircleMap * (ff ")) * F) . a by RELAT_1:36 .= (CircleMap * (ff ")) . (F . a) by A131, A96, A101, A165, FUNCT_1:13 .= F . a by A48, A51, A113, A106, A168, TOPALG_3:2 ; ::_thesis: verum end; supposeA170: not a in dom Fni1 ; ::_thesis: (CircleMap * Fn1) . a = F . a then A171: a in [:N1,S:] by A96, A101, A112, A162, A164, XBOOLE_0:def_3; thus (CircleMap * Fn1) . a = CircleMap . (Fn1 . a) by A164, FUNCT_2:15 .= CircleMap . ((Fn | [:N1,S:]) . a) by A170, FUNCT_4:11 .= CircleMap . (Fn . a) by A171, FUNCT_1:49 .= (CircleMap * Fn) . a by A64, A60, A67, A130, A171, FUNCT_2:15 .= F . a by A58, A130, A171, FUNCT_1:49 ; ::_thesis: verum end; end; end; A172: S c= S1 by XBOOLE_1:7; then A173: ( [#] (I[01] | S1) = the carrier of (I[01] | S1) & I[01] | S is SubSpace of I[01] | S1 ) by A64, A136, TSEP_1:4; A174: SS c= S1 by XBOOLE_1:7; then reconsider F1 = [#] (I[01] | S), F2 = [#] (I[01] | SS) as Subset of (I[01] | S1) by A136, A172, 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 A175: F1 is closed by TSEP_1:8; thus y in N1 by A55, A93, XBOOLE_0:def_4; ::_thesis: ( N1 c= N & Fn1 is continuous & F | [:N1,S1:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:] ) thus N1 c= N by A56, A94, XBOOLE_1:1; ::_thesis: ( Fn1 is continuous & F | [:N1,S1:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:] ) hSS is closed by BORSUK_4:23, PRE_TOPC:8; then A176: F2 is closed by TSEP_1:8; I[01] | SS is SubSpace of I[01] | S1 by A109, A136, A174, 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, A109, A136, A173, A175, A176, A134, A133, A120, TOPALG_3:19; hence Fn1 is continuous ; ::_thesis: ( F | [:N1,S1:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:] ) dom Fn1 = (dom F) /\ [:N1,S1:] by A6, A135, A112, XBOOLE_1:28, ZFMISC_1:96; hence F | [:N1,S1:] = CircleMap * Fn1 by A161, A163, FUNCT_1:46, RELAT_1:27; ::_thesis: Fn1 | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:] dom (Ft | [:N1, the carrier of I[01]:]) = (dom Ft) /\ [:N1, the carrier of I[01]:] by RELAT_1:61 .= [:( the carrier of Y /\ N1),({0} /\ the carrier of I[01]):] by A8, ZFMISC_1:100 .= [:N1,({0} /\ the carrier of I[01]):] by XBOOLE_1:28 .= [:N1,{0}:] by Lm3, XBOOLE_1:28 ; hence Fn1 | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:] by A140, A141, FUNCT_1:2; ::_thesis: verum end; end; end; A177: S2[ 0 ] by FINSEQ_3:24; for i being Element of NAT holds S2[i] from NAT_1:sch_1(A177, 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 A178: S = [.0,(TT . (len TT)).] and A179: y in N2 and A180: N2 c= N and A181: Fn1 is continuous and A182: F | [:N2,S:] = CircleMap * Fn1 and A183: Fn1 | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] by A17; reconsider z = Fn1 . x as Point of R^1 by TOPMETR:17; A184: I[01] | S = I[01] by A12, A178, Lm6, BORSUK_1:40, TSEP_1:3; then reconsider Fn1 = Fn1 as Function of [:(Y | N2),I[01]:],R^1 ; take z ; ::_thesis: S1[x,z] take y ; ::_thesis: ex t being Point of I[01] ex N being non empty open Subset of Y ex Fn being Function of [:(Y | N),I[01]:],R^1 st ( x = [y,t] & z = Fn . x & y in N & Fn is continuous & F | [:N, the carrier of I[01]:] = CircleMap * Fn & Fn | [: the carrier of Y,{0}:] = Ft | [:N, the carrier of I[01]:] & ( for H being Function of [:(Y | N),I[01]:],R^1 st H is continuous & F | [:N, the carrier of I[01]:] = CircleMap * H & H | [: the carrier of Y,{0}:] = Ft | [:N, the carrier of I[01]:] holds Fn = H ) ) take t ; ::_thesis: ex N being non empty open Subset of Y ex Fn being Function of [:(Y | N),I[01]:],R^1 st ( x = [y,t] & z = Fn . x & y in N & Fn is continuous & F | [:N, the carrier of I[01]:] = CircleMap * Fn & Fn | [: the carrier of Y,{0}:] = Ft | [:N, the carrier of I[01]:] & ( for H being Function of [:(Y | N),I[01]:],R^1 st H is continuous & F | [:N, the carrier of I[01]:] = CircleMap * H & H | [: the carrier of Y,{0}:] = Ft | [:N, the carrier of I[01]:] holds Fn = H ) ) take N2 ; ::_thesis: ex Fn being Function of [:(Y | N2),I[01]:],R^1 st ( x = [y,t] & z = Fn . x & y in N2 & Fn is continuous & F | [:N2, the carrier of I[01]:] = CircleMap * Fn & Fn | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] & ( for H being Function of [:(Y | N2),I[01]:],R^1 st H is continuous & F | [:N2, the carrier of I[01]:] = CircleMap * H & H | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] holds Fn = H ) ) take Fn1 ; ::_thesis: ( x = [y,t] & z = Fn1 . x & y in N2 & Fn1 is continuous & F | [:N2, the carrier of I[01]:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] & ( for H being Function of [:(Y | N2),I[01]:],R^1 st H is continuous & F | [:N2, the carrier of I[01]:] = CircleMap * H & H | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] holds Fn1 = H ) ) thus ( x = [y,t] & z = Fn1 . x & y in N2 & Fn1 is continuous & F | [:N2, the carrier of I[01]:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] ) by A10, A12, A178, A179, A181, A182, A183, A184, BORSUK_1:40; ::_thesis: for H being Function of [:(Y | N2),I[01]:],R^1 st H is continuous & F | [:N2, the carrier of I[01]:] = CircleMap * H & H | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] holds Fn1 = H let H be Function of [:(Y | N2),I[01]:],R^1; ::_thesis: ( H is continuous & F | [:N2, the carrier of I[01]:] = CircleMap * H & H | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] implies Fn1 = H ) assume that A185: H is continuous and A186: F | [:N2, the carrier of I[01]:] = CircleMap * H and A187: H | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] ; ::_thesis: Fn1 = H defpred S3[ Element of 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:] ) ); A188: dom Fn1 = the carrier of [:(Y | N2),I[01]:] by FUNCT_2:def_1; A189: ( the carrier of [:(Y | N2),I[01]:] = [: the carrier of (Y | N2), the carrier of I[01]:] & the carrier of (Y | N2) = N2 ) by BORSUK_1:def_2, PRE_TOPC:8; A190: dom H = the carrier of [:(Y | N2),I[01]:] by FUNCT_2:def_1; A191: for i being Element of NAT st S3[i] holds S3[i + 1] proof let i be Element of NAT ; ::_thesis: ( S3[i] implies S3[i + 1] ) assume that A192: S3[i] and A193: i + 1 in dom TT ; ::_thesis: ex Z being non empty Subset of I[01] st ( Z = [.0,(TT . (i + 1)).] & Fn1 | [:N2,Z:] = H | [:N2,Z:] ) percases ( i = 0 or i in dom TT ) by A193, TOPREALA:2; supposeA194: i = 0 ; ::_thesis: ex Z being non empty Subset of I[01] st ( Z = [.0,(TT . (i + 1)).] & Fn1 | [:N2,Z:] = H | [:N2,Z:] ) set Z = [.0,(TT . (i + 1)).]; A195: [.0,(TT . (i + 1)).] = {0} by A11, A194, XXREAL_1:17; reconsider Z = [.0,(TT . (i + 1)).] as non empty Subset of I[01] by A11, A194, Lm3, XXREAL_1:17; A196: [:N2,Z:] c= [:N2, the carrier of I[01]:] by ZFMISC_1:95; then A197: dom (Fn1 | [:N2,Z:]) = [:N2,Z:] by A189, A188, RELAT_1:62; A198: for x being set st x in dom (Fn1 | [:N2,Z:]) holds (Fn1 | [:N2,Z:]) . x = (H | [:N2,Z:]) . x proof let x be set ; ::_thesis: ( x in dom (Fn1 | [:N2,Z:]) implies (Fn1 | [:N2,Z:]) . x = (H | [:N2,Z:]) . x ) A199: [:N2,Z:] c= [: the carrier of Y,Z:] by ZFMISC_1:95; assume A200: x in dom (Fn1 | [:N2,Z:]) ; ::_thesis: (Fn1 | [:N2,Z:]) . x = (H | [:N2,Z:]) . x hence (Fn1 | [:N2,Z:]) . x = Fn1 . x by A197, FUNCT_1:49 .= (Fn1 | [: the carrier of Y,{0}:]) . x by A195, A197, A200, A199, FUNCT_1:49 .= H . x by A183, A187, A195, A197, A200, A199, FUNCT_1:49 .= (H | [:N2,Z:]) . x by A197, A200, FUNCT_1:49 ; ::_thesis: verum end; take Z ; ::_thesis: ( Z = [.0,(TT . (i + 1)).] & Fn1 | [:N2,Z:] = H | [:N2,Z:] ) thus Z = [.0,(TT . (i + 1)).] ; ::_thesis: Fn1 | [:N2,Z:] = H | [:N2,Z:] dom (H | [:N2,Z:]) = [:N2,Z:] by A190, A189, A196, RELAT_1:62; hence Fn1 | [:N2,Z:] = H | [:N2,Z:] by A188, A198, FUNCT_1:2, RELAT_1:62; ::_thesis: verum end; supposeA201: i in dom TT ; ::_thesis: ex Z being non empty Subset of I[01] st ( Z = [.0,(TT . (i + 1)).] & Fn1 | [:N2,Z:] = H | [:N2,Z:] ) set ZZ = [.(TT . i),(TT . (i + 1)).]; A202: 0 <= TT . i by A19, A201; A203: TT . (i + 1) <= 1 by A19, A193, A201; then reconsider ZZ = [.(TT . i),(TT . (i + 1)).] as Subset of I[01] by A25, A202; consider Z being non empty Subset of I[01] such that A204: Z = [.0,(TT . i).] and A205: Fn1 | [:N2,Z:] = H | [:N2,Z:] by A192, A201; take Z1 = Z \/ ZZ; ::_thesis: ( Z1 = [.0,(TT . (i + 1)).] & Fn1 | [:N2,Z1:] = H | [:N2,Z1:] ) A206: TT . i < TT . (i + 1) by A19, A193, A201; hence Z1 = [.0,(TT . (i + 1)).] by A204, A202, XXREAL_1:165; ::_thesis: Fn1 | [:N2,Z1:] = H | [:N2,Z1:] A207: [:N2,Z1:] c= [:N2, the carrier of I[01]:] by ZFMISC_1:95; then A208: dom (Fn1 | [:N2,Z1:]) = [:N2,Z1:] by A189, A188, RELAT_1:62; A209: for x being set st x in dom (Fn1 | [:N2,Z1:]) holds (Fn1 | [:N2,Z1:]) . x = (H | [:N2,Z1:]) . x proof 0 <= TT . (i + 1) by A19, A193; then A210: TT . (i + 1) is Point of I[01] by A203, BORSUK_1:43; ( 0 <= TT . i & TT . i <= 1 ) by A19, A193, A201; then TT . i is Point of I[01] by BORSUK_1:43; then A211: ZZ is connected by A206, A210, BORSUK_4:24; consider Ui being non empty Subset of (Tunit_circle 2) such that A212: Ui in UL and A213: F .: [:N,ZZ:] c= Ui by A16, A193, A201; consider D being mutually-disjoint open Subset-Family of R^1 such that A214: union D = CircleMap " Ui and A215: for d being Subset of R^1 st d in D holds for f being Function of (R^1 | d),((Tunit_circle 2) | Ui) st f = CircleMap | d holds f is being_homeomorphism by A2, A212; let x be set ; ::_thesis: ( x in dom (Fn1 | [:N2,Z1:]) implies (Fn1 | [:N2,Z1:]) . x = (H | [:N2,Z1:]) . x ) assume A216: x in dom (Fn1 | [:N2,Z1:]) ; ::_thesis: (Fn1 | [:N2,Z1:]) . x = (H | [:N2,Z1:]) . x consider x1, x2 being set such that A217: x1 in N2 and A218: x2 in Z1 and A219: x = [x1,x2] by A208, A216, ZFMISC_1:def_2; A220: TT . i in ZZ by A206, XXREAL_1:1; then [x1,(TT . i)] in [:N,ZZ:] by A180, A217, ZFMISC_1:87; then A221: F . [x1,(TT . i)] in F .: [:N,ZZ:] by FUNCT_2:35; reconsider xy = {x1} as non empty Subset of Y by A217, ZFMISC_1:31; A222: xy c= N2 by A217, ZFMISC_1:31; then reconsider xZZ = [:xy,ZZ:] as Subset of [:(Y | N2),I[01]:] by A189, ZFMISC_1:96; A223: dom (H | [:xy,ZZ:]) = [:xy,ZZ:] by A190, A189, A222, RELAT_1:62, ZFMISC_1:96; A224: D is Cover of Fn1 .: xZZ proof let b be set ; :: according to TARSKI:def_3,SETFAM_1:def_11 ::_thesis: ( not b in Fn1 .: xZZ or b in union D ) A225: [:N,ZZ:] c= [: the carrier of Y, the carrier of I[01]:] by ZFMISC_1:96; assume b in Fn1 .: xZZ ; ::_thesis: b in union D then consider a being Point of [:(Y | N2),I[01]:] such that A226: a in xZZ and A227: Fn1 . a = b by FUNCT_2:65; xy c= N by A180, A217, ZFMISC_1:31; then [:xy,ZZ:] c= [:N,ZZ:] by ZFMISC_1:95; then a in [:N,ZZ:] by A226; then A228: F . a in F .: [:N,ZZ:] by A6, A225, FUNCT_1:def_6; CircleMap . (Fn1 . a) = (CircleMap * Fn1) . a by FUNCT_2:15 .= F . a by A12, A178, A182, A189, BORSUK_1:40, FUNCT_1:49 ; hence b in union D by A213, A214, A227, A228, Lm12, FUNCT_1:def_7, TOPMETR:17; ::_thesis: verum end; A229: D is Cover of H .: xZZ proof let b be set ; :: according to TARSKI:def_3,SETFAM_1:def_11 ::_thesis: ( not b in H .: xZZ or b in union D ) A230: [:N,ZZ:] c= [: the carrier of Y, the carrier of I[01]:] by ZFMISC_1:96; assume b in H .: xZZ ; ::_thesis: b in union D then consider a being Point of [:(Y | N2),I[01]:] such that A231: a in xZZ and A232: H . a = b by FUNCT_2:65; A233: CircleMap . (H . a) = (CircleMap * H) . a by FUNCT_2:15 .= F . a by A186, A189, FUNCT_1:49 ; xy c= N by A180, A217, ZFMISC_1:31; then [:xy,ZZ:] c= [:N,ZZ:] by ZFMISC_1:95; then a in [:N,ZZ:] by A231; then F . a in F .: [:N,ZZ:] by A6, A230, FUNCT_1:def_6; hence b in union D by A213, A214, A232, A233, Lm12, FUNCT_1:def_7, TOPMETR:17; ::_thesis: verum end; TT . i in Z by A204, A202, XXREAL_1:1; then A234: [x1,(TT . i)] in [:N2,Z:] by A217, ZFMISC_1:87; then A235: Fn1 . [x1,(TT . i)] = (Fn1 | [:N2,Z:]) . [x1,(TT . i)] by FUNCT_1:49 .= H . [x1,(TT . i)] by A205, A234, FUNCT_1:49 ; A236: [:N2,Z:] c= [:N2, the carrier of I[01]:] by ZFMISC_1:95; then F . [x1,(TT . i)] = (CircleMap * H) . [x1,(TT . i)] by A186, A234, FUNCT_1:49 .= CircleMap . (H . [x1,(TT . i)]) by A190, A189, A234, A236, FUNCT_1:13 ; then H . [x1,(TT . i)] in CircleMap " Ui by A213, A221, FUNCT_2:38, TOPMETR:17; then consider Uith being set such that A237: H . [x1,(TT . i)] in Uith and A238: Uith in D by A214, TARSKI:def_4; F . [x1,(TT . i)] = (CircleMap * Fn1) . [x1,(TT . i)] by A12, A178, A182, A234, A236, BORSUK_1:40, FUNCT_1:49 .= CircleMap . (Fn1 . [x1,(TT . i)]) by A189, A188, A234, A236, FUNCT_1:13 ; then Fn1 . [x1,(TT . i)] in CircleMap " Ui by A213, A221, FUNCT_2:38, TOPMETR:17; then consider Uit being set such that A239: Fn1 . [x1,(TT . i)] in Uit and A240: Uit in D by A214, TARSKI:def_4; I[01] is SubSpace of I[01] by TSEP_1:2; then A241: [:(Y | N2),I[01]:] is SubSpace of [:Y,I[01]:] by BORSUK_3:21; xy is connected by A217; then [:xy,ZZ:] is connected by A211, TOPALG_3:16; then A242: xZZ is connected by A241, CONNSP_1:23; reconsider Uith = Uith as non empty Subset of R^1 by A237, A238; A243: x1 in xy by TARSKI:def_1; then A244: [x1,(TT . i)] in xZZ by A220, ZFMISC_1:87; then H . [x1,(TT . i)] in H .: xZZ by FUNCT_2:35; then Uith meets H .: xZZ by A237, XBOOLE_0:3; then A245: H .: xZZ c= Uith by A185, A242, A238, A229, TOPALG_3:12, TOPS_2:61; reconsider Uit = Uit as non empty Subset of R^1 by A239, A240; set f = CircleMap | Uit; A246: dom (CircleMap | Uit) = Uit by Lm12, RELAT_1:62, TOPMETR:17; A247: rng (CircleMap | Uit) c= Ui proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in rng (CircleMap | Uit) or b in Ui ) assume b in rng (CircleMap | Uit) ; ::_thesis: b in Ui then consider a being set such that A248: a in dom (CircleMap | Uit) and A249: (CircleMap | Uit) . a = b by FUNCT_1:def_3; a in union D by A240, A246, A248, TARSKI:def_4; then CircleMap . a in Ui by A214, FUNCT_2:38; hence b in Ui by A246, A248, A249, FUNCT_1:49; ::_thesis: verum end; ( the carrier of ((Tunit_circle 2) | Ui) = Ui & the carrier of (R^1 | Uit) = Uit ) by PRE_TOPC:8; then reconsider f = CircleMap | Uit as Function of (R^1 | Uit),((Tunit_circle 2) | Ui) by A246, A247, FUNCT_2:2; A250: dom (Fn1 | [:xy,ZZ:]) = [:xy,ZZ:] by A189, A188, A222, RELAT_1:62, ZFMISC_1:96; H . [x1,(TT . i)] in H .: xZZ by A190, A244, FUNCT_1:def_6; then Uit meets Uith by A239, A245, A235, XBOOLE_0:3; then A251: Uit = Uith by A240, A238, TAXONOM2:def_5; A252: rng (H | [:xy,ZZ:]) c= dom f proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in rng (H | [:xy,ZZ:]) or b in dom f ) assume b in rng (H | [:xy,ZZ:]) ; ::_thesis: b in dom f then consider a being set such that A253: a in dom (H | [:xy,ZZ:]) and A254: (H | [:xy,ZZ:]) . a = b by FUNCT_1:def_3; H . a = b by A223, A253, A254, FUNCT_1:49; then b in H .: xZZ by A190, A223, A253, FUNCT_1:def_6; hence b in dom f by A245, A251, A246; ::_thesis: verum end; Fn1 . [x1,(TT . i)] in Fn1 .: xZZ by A244, FUNCT_2:35; then Uit meets Fn1 .: xZZ by A239, XBOOLE_0:3; then A255: Fn1 .: xZZ c= Uit by A181, A184, A240, A242, A224, TOPALG_3:12, TOPS_2:61; A256: rng (Fn1 | [:xy,ZZ:]) c= dom f proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in rng (Fn1 | [:xy,ZZ:]) or b in dom f ) assume b in rng (Fn1 | [:xy,ZZ:]) ; ::_thesis: b in dom f then consider a being set such that A257: a in dom (Fn1 | [:xy,ZZ:]) and A258: (Fn1 | [:xy,ZZ:]) . a = b by FUNCT_1:def_3; Fn1 . a = b by A250, A257, A258, FUNCT_1:49; then b in Fn1 .: xZZ by A188, A250, A257, FUNCT_1:def_6; hence b in dom f by A255, A246; ::_thesis: verum end; then A259: dom (f * (Fn1 | [:xy,ZZ:])) = dom (Fn1 | [:xy,ZZ:]) by RELAT_1:27; A260: for x being set st x in dom (f * (Fn1 | [:xy,ZZ:])) holds (f * (Fn1 | [:xy,ZZ:])) . x = (f * (H | [:xy,ZZ:])) . x proof let x be set ; ::_thesis: ( x in dom (f * (Fn1 | [:xy,ZZ:])) implies (f * (Fn1 | [:xy,ZZ:])) . x = (f * (H | [:xy,ZZ:])) . x ) assume A261: x in dom (f * (Fn1 | [:xy,ZZ:])) ; ::_thesis: (f * (Fn1 | [:xy,ZZ:])) . x = (f * (H | [:xy,ZZ:])) . x A262: Fn1 . x in Fn1 .: [:xy,ZZ:] by A188, A250, A259, A261, FUNCT_1:def_6; A263: H . x in H .: [:xy,ZZ:] by A190, A250, A259, A261, FUNCT_1:def_6; thus (f * (Fn1 | [:xy,ZZ:])) . x = ((f * Fn1) | [:xy,ZZ:]) . x by RELAT_1:83 .= (f * Fn1) . x by A250, A259, A261, FUNCT_1:49 .= f . (Fn1 . x) by A188, A261, FUNCT_1:13 .= CircleMap . (Fn1 . x) by A255, A262, FUNCT_1:49 .= (CircleMap * Fn1) . x by A188, A261, FUNCT_1:13 .= CircleMap . (H . x) by A12, A178, A182, A186, A190, A261, BORSUK_1:40, FUNCT_1:13 .= f . (H . x) by A245, A251, A263, FUNCT_1:49 .= (f * H) . x by A190, A261, FUNCT_1:13 .= ((f * H) | [:xy,ZZ:]) . x by A250, A259, A261, FUNCT_1:49 .= (f * (H | [:xy,ZZ:])) . x by RELAT_1:83 ; ::_thesis: verum end; f is being_homeomorphism by A215, A240; then A264: f is one-to-one by TOPS_2:def_5; dom (f * (H | [:xy,ZZ:])) = dom (H | [:xy,ZZ:]) by A252, RELAT_1:27; then A265: f * (Fn1 | [:xy,ZZ:]) = f * (H | [:xy,ZZ:]) by A250, A223, A256, A260, FUNCT_1:2, RELAT_1:27; percases ( x2 in ZZ or not x2 in ZZ ) ; suppose x2 in ZZ ; ::_thesis: (Fn1 | [:N2,Z1:]) . x = (H | [:N2,Z1:]) . x then A266: x in [:xy,ZZ:] by A219, A243, ZFMISC_1:87; thus (Fn1 | [:N2,Z1:]) . x = Fn1 . x by A208, A216, FUNCT_1:49 .= (Fn1 | [:xy,ZZ:]) . x by A266, FUNCT_1:49 .= (H | [:xy,ZZ:]) . x by A264, A250, A223, A256, A252, A265, FUNCT_1:27 .= H . x by A266, FUNCT_1:49 .= (H | [:N2,Z1:]) . x by A208, A216, FUNCT_1:49 ; ::_thesis: verum end; suppose not x2 in ZZ ; ::_thesis: (Fn1 | [:N2,Z1:]) . x = (H | [:N2,Z1:]) . x then x2 in Z by A218, XBOOLE_0:def_3; then A267: x in [:N2,Z:] by A217, A219, ZFMISC_1:87; thus (Fn1 | [:N2,Z1:]) . x = Fn1 . x by A208, A216, FUNCT_1:49 .= (Fn1 | [:N2,Z:]) . x by A267, FUNCT_1:49 .= H . x by A205, A267, FUNCT_1:49 .= (H | [:N2,Z1:]) . x by A208, A216, FUNCT_1:49 ; ::_thesis: verum end; end; end; dom (H | [:N2,Z1:]) = [:N2,Z1:] by A190, A189, A207, RELAT_1:62; hence Fn1 | [:N2,Z1:] = H | [:N2,Z1:] by A188, A209, FUNCT_1:2, RELAT_1:62; ::_thesis: verum end; end; end; A268: S3[ 0 ] by FINSEQ_3:24; for i being Element of NAT holds S3[i] from NAT_1:sch_1(A268, A191); then consider Z being non empty Subset of I[01] such that A269: Z = [.0,(TT . (len TT)).] and A270: Fn1 | [:N2,Z:] = H | [:N2,Z:] by A17; thus Fn1 = Fn1 | [:N2,Z:] by A12, A189, A188, A269, BORSUK_1:40, RELAT_1:69 .= H by A12, A190, A189, A269, A270, BORSUK_1:40, RELAT_1:69 ; ::_thesis: verum end; consider G being Function of [:Y,I[01]:],R^1 such that A271: for x being Point of [:Y,I[01]:] holds S1[x,G . x] from FUNCT_2:sch_3(A9); take G ; ::_thesis: ( 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 ) ) A272: now__::_thesis:_for_N_being_Subset_of_Y for_F_being_Function_of_[:(Y_|_N),I[01]:],R^1_holds_dom_F_=_[:N,_the_carrier_of_I[01]:] let N be Subset of Y; ::_thesis: for F being Function of [:(Y | N),I[01]:],R^1 holds dom F = [:N, the carrier of I[01]:] let F be Function of [:(Y | N),I[01]:],R^1; ::_thesis: dom F = [:N, the carrier of I[01]:] thus dom F = the carrier of [:(Y | N),I[01]:] by FUNCT_2:def_1 .= [: the carrier of (Y | N), the carrier of I[01]:] by BORSUK_1:def_2 .= [:N, the carrier of I[01]:] by PRE_TOPC:8 ; ::_thesis: verum end; A273: for p being Point of [:Y,I[01]:] for y being Point of Y for t being Point of I[01] for N1, N2 being non empty open Subset of Y for Fn1 being Function of [:(Y | N1),I[01]:],R^1 for 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, the carrier of I[01]:] = CircleMap * Fn2 & Fn2 | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] & F | [:N1, the carrier of I[01]:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:] holds Fn1 | [:{y}, the carrier of I[01]:] = Fn2 | [:{y}, the carrier of I[01]:] proof let p be Point of [:Y,I[01]:]; ::_thesis: for y being Point of Y for t being Point of I[01] for N1, N2 being non empty open Subset of Y for Fn1 being Function of [:(Y | N1),I[01]:],R^1 for 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, the carrier of I[01]:] = CircleMap * Fn2 & Fn2 | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] & F | [:N1, the carrier of I[01]:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:] holds Fn1 | [:{y}, the carrier of I[01]:] = Fn2 | [:{y}, the carrier of I[01]:] let y be Point of Y; ::_thesis: for t being Point of I[01] for N1, N2 being non empty open Subset of Y for Fn1 being Function of [:(Y | N1),I[01]:],R^1 for 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, the carrier of I[01]:] = CircleMap * Fn2 & Fn2 | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] & F | [:N1, the carrier of I[01]:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:] holds Fn1 | [:{y}, the carrier of I[01]:] = Fn2 | [:{y}, the carrier of I[01]:] let t be Point of I[01]; ::_thesis: for N1, N2 being non empty open Subset of Y for Fn1 being Function of [:(Y | N1),I[01]:],R^1 for 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, the carrier of I[01]:] = CircleMap * Fn2 & Fn2 | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] & F | [:N1, the carrier of I[01]:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:] holds Fn1 | [:{y}, the carrier of I[01]:] = Fn2 | [:{y}, the carrier of I[01]:] let N1, N2 be non empty open Subset of Y; ::_thesis: for Fn1 being Function of [:(Y | N1),I[01]:],R^1 for 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, the carrier of I[01]:] = CircleMap * Fn2 & Fn2 | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] & F | [:N1, the carrier of I[01]:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:] holds Fn1 | [:{y}, the carrier of I[01]:] = Fn2 | [:{y}, the carrier of I[01]:] let Fn1 be Function of [:(Y | N1),I[01]:],R^1; ::_thesis: for 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, the carrier of I[01]:] = CircleMap * Fn2 & Fn2 | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] & F | [:N1, the carrier of I[01]:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:] holds Fn1 | [:{y}, the carrier of I[01]:] = Fn2 | [:{y}, the carrier of I[01]:] let Fn2 be Function of [:(Y | N2),I[01]:],R^1; ::_thesis: ( p = [y,t] & y in N1 & y in N2 & Fn2 is continuous & Fn1 is continuous & F | [:N2, the carrier of I[01]:] = CircleMap * Fn2 & Fn2 | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] & F | [:N1, the carrier of I[01]:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:] implies Fn1 | [:{y}, the carrier of I[01]:] = Fn2 | [:{y}, the carrier of I[01]:] ) assume that p = [y,t] and A274: y in N1 and A275: y in N2 and A276: Fn2 is continuous and A277: Fn1 is continuous and A278: F | [:N2, the carrier of I[01]:] = CircleMap * Fn2 and A279: Fn2 | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] and A280: F | [:N1, the carrier of I[01]:] = CircleMap * Fn1 and A281: Fn1 | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:] ; ::_thesis: Fn1 | [:{y}, the carrier of I[01]:] = Fn2 | [:{y}, the carrier of I[01]:] A282: {y} c= N1 by A274, ZFMISC_1:31; consider TT being non empty FinSequence of REAL such that A283: TT . 1 = 0 and A284: TT . (len TT) = 1 and A285: TT is increasing and A286: 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 holds 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 A287: y in N and A288: for i being Nat st i in dom TT & i + 1 in dom TT holds ex Ui being non empty Subset of (Tunit_circle 2) st ( Ui in UL & F .: [:N,[.(TT . i),(TT . (i + 1)).]:] c= Ui ) by A286; reconsider N = N as non empty open Subset of Y by A287; defpred S2[ Element of 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:] ) ); A289: len TT in dom TT by FINSEQ_5:6; A290: dom Fn2 = the carrier of [:(Y | N2),I[01]:] by FUNCT_2:def_1; A291: dom Fn2 = [:N2, the carrier of I[01]:] by A272; A292: {y} c= N2 by A275, ZFMISC_1:31; A293: ( the carrier of [:(Y | N1),I[01]:] = [: the carrier of (Y | N1), the carrier of I[01]:] & the carrier of (Y | N1) = N1 ) by BORSUK_1:def_2, PRE_TOPC:8; A294: ( the carrier of [:(Y | N2),I[01]:] = [: the carrier of (Y | N2), the carrier of I[01]:] & the carrier of (Y | N2) = N2 ) by BORSUK_1:def_2, PRE_TOPC:8; A295: dom Fn1 = [:N1, the carrier of I[01]:] by A272; A296: dom Fn1 = the carrier of [:(Y | N1),I[01]:] by FUNCT_2:def_1; A297: 1 in dom TT by FINSEQ_5:6; A298: for i being Element of NAT st S2[i] holds S2[i + 1] proof let i be Element of NAT ; ::_thesis: ( S2[i] implies S2[i + 1] ) assume that A299: S2[i] and A300: i + 1 in dom TT ; ::_thesis: ex Z being non empty Subset of I[01] st ( Z = [.0,(TT . (i + 1)).] & Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:] ) percases ( i = 0 or i in dom TT ) by A300, TOPREALA:2; supposeA301: i = 0 ; ::_thesis: ex Z being non empty Subset of I[01] st ( Z = [.0,(TT . (i + 1)).] & Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:] ) set Z = [.0,(TT . (i + 1)).]; A302: [.0,(TT . (i + 1)).] = {0} by A283, A301, XXREAL_1:17; reconsider Z = [.0,(TT . (i + 1)).] as non empty Subset of I[01] by A283, A301, Lm3, XXREAL_1:17; A303: [:{y},Z:] c= [:N2, the carrier of I[01]:] by A292, ZFMISC_1:96; A304: dom (Fn1 | [:{y},Z:]) = [:{y},Z:] by A282, A295, RELAT_1:62, ZFMISC_1:96; A305: [:{y},Z:] c= [:N1, the carrier of I[01]:] by A282, ZFMISC_1:96; A306: for x being set st x in dom (Fn1 | [:{y},Z:]) holds (Fn1 | [:{y},Z:]) . x = (Fn2 | [:{y},Z:]) . x proof let x be set ; ::_thesis: ( x in dom (Fn1 | [:{y},Z:]) implies (Fn1 | [:{y},Z:]) . x = (Fn2 | [:{y},Z:]) . x ) A307: [:{y},Z:] c= [: the carrier of Y,Z:] by ZFMISC_1:95; assume A308: x in dom (Fn1 | [:{y},Z:]) ; ::_thesis: (Fn1 | [:{y},Z:]) . x = (Fn2 | [:{y},Z:]) . x hence (Fn1 | [:{y},Z:]) . x = Fn1 . x by A304, FUNCT_1:49 .= (Fn1 | [: the carrier of Y,{0}:]) . x by A302, A304, A308, A307, FUNCT_1:49 .= Ft . x by A281, A305, A304, A308, FUNCT_1:49 .= (Ft | [:N2, the carrier of I[01]:]) . x by A304, A303, A308, FUNCT_1:49 .= Fn2 . x by A279, A302, A304, A308, A307, FUNCT_1:49 .= (Fn2 | [:{y},Z:]) . x by A304, A308, FUNCT_1:49 ; ::_thesis: verum end; take Z ; ::_thesis: ( Z = [.0,(TT . (i + 1)).] & Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:] ) thus Z = [.0,(TT . (i + 1)).] ; ::_thesis: Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:] dom (Fn2 | [:{y},Z:]) = [:{y},Z:] by A292, A291, RELAT_1:62, ZFMISC_1:96; hence Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:] by A304, A306, FUNCT_1:2; ::_thesis: verum end; supposeA309: i in dom TT ; ::_thesis: ex Z being non empty Subset of I[01] st ( Z = [.0,(TT . (i + 1)).] & Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:] ) A310: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_TT_holds_ (_0_<=_TT_._i_&_(_i_+_1_in_dom_TT_implies_(_TT_._i_<_TT_._(i_+_1)_&_TT_._(i_+_1)_<=_1_&_TT_._i_<_1_&_0_<_TT_._(i_+_1)_)_)_) let i be Element of NAT ; ::_thesis: ( i in dom TT implies ( 0 <= TT . i & ( i + 1 in dom TT implies ( TT . i < TT . (i + 1) & TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 1) ) ) ) ) assume A311: i in dom TT ; ::_thesis: ( 0 <= TT . i & ( i + 1 in dom TT implies ( TT . i < TT . (i + 1) & TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 1) ) ) ) 1 <= i by A311, FINSEQ_3:25; then ( 1 = i or 1 < i ) by XXREAL_0:1; hence A312: 0 <= TT . i by A283, A285, A297, A311, SEQM_3:def_1; ::_thesis: ( i + 1 in dom TT implies ( TT . i < TT . (i + 1) & TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 1) ) ) assume A313: i + 1 in dom TT ; ::_thesis: ( TT . i < TT . (i + 1) & TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 1) ) A314: i + 0 < i + 1 by XREAL_1:8; hence A315: TT . i < TT . (i + 1) by A285, A311, A313, SEQM_3:def_1; ::_thesis: ( TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 1) ) i + 1 <= len TT by A313, FINSEQ_3:25; then ( i + 1 = len TT or i + 1 < len TT ) by XXREAL_0:1; hence TT . (i + 1) <= 1 by A284, A285, A289, A313, SEQM_3:def_1; ::_thesis: ( TT . i < 1 & 0 < TT . (i + 1) ) hence TT . i < 1 by A315, XXREAL_0:2; ::_thesis: 0 < TT . (i + 1) thus 0 < TT . (i + 1) by A285, A311, A312, A313, A314, SEQM_3:def_1; ::_thesis: verum end; then A316: 0 <= TT . i by A309; A317: TT . (i + 1) <= 1 by A300, A309, A310; set ZZ = [.(TT . i),(TT . (i + 1)).]; consider Z being non empty Subset of I[01] such that A318: Z = [.0,(TT . i).] and A319: Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:] by A299, A309; now__::_thesis:_for_i_being_Element_of_NAT_st_0_<=_TT_._i_&_TT_._(i_+_1)_<=_1_holds_ [.(TT_._i),(TT_._(i_+_1)).]_c=_the_carrier_of_I[01] let i be Element of NAT ; ::_thesis: ( 0 <= TT . i & TT . (i + 1) <= 1 implies [.(TT . i),(TT . (i + 1)).] c= the carrier of I[01] ) assume that A320: 0 <= TT . i and A321: TT . (i + 1) <= 1 ; ::_thesis: [.(TT . i),(TT . (i + 1)).] c= the carrier of I[01] thus [.(TT . i),(TT . (i + 1)).] c= the carrier of I[01] ::_thesis: verum proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in [.(TT . i),(TT . (i + 1)).] or a in the carrier of I[01] ) assume A322: a in [.(TT . i),(TT . (i + 1)).] ; ::_thesis: a in the carrier of I[01] then reconsider a = a as Real ; a <= TT . (i + 1) by A322, XXREAL_1:1; then A323: a <= 1 by A321, XXREAL_0:2; 0 <= a by A320, A322, XXREAL_1:1; hence a in the carrier of I[01] by A323, BORSUK_1:43; ::_thesis: verum end; end; then reconsider ZZ = [.(TT . i),(TT . (i + 1)).] as Subset of I[01] by A316, A317; take Z1 = Z \/ ZZ; ::_thesis: ( Z1 = [.0,(TT . (i + 1)).] & Fn1 | [:{y},Z1:] = Fn2 | [:{y},Z1:] ) A324: TT . i < TT . (i + 1) by A300, A309, A310; hence Z1 = [.0,(TT . (i + 1)).] by A318, A316, XXREAL_1:165; ::_thesis: Fn1 | [:{y},Z1:] = Fn2 | [:{y},Z1:] A325: dom (Fn1 | [:{y},Z1:]) = [:{y},Z1:] by A282, A295, RELAT_1:62, ZFMISC_1:96; A326: for x being set st x in dom (Fn1 | [:{y},Z1:]) holds (Fn1 | [:{y},Z1:]) . x = (Fn2 | [:{y},Z1:]) . x proof 0 <= TT . (i + 1) by A300, A310; then A327: TT . (i + 1) is Point of I[01] by A317, BORSUK_1:43; ( 0 <= TT . i & TT . i <= 1 ) by A300, A309, A310; then TT . i is Point of I[01] by BORSUK_1:43; then A328: ZZ is connected by A324, A327, BORSUK_4:24; A329: TT . i in ZZ by A324, XXREAL_1:1; consider Ui being non empty Subset of (Tunit_circle 2) such that A330: Ui in UL and A331: F .: [:N,ZZ:] c= Ui by A288, A300, A309; consider D being mutually-disjoint open Subset-Family of R^1 such that A332: union D = CircleMap " Ui and A333: for d being Subset of R^1 st d in D holds for f being Function of (R^1 | d),((Tunit_circle 2) | Ui) st f = CircleMap | d holds f is being_homeomorphism by A2, A330; let x be set ; ::_thesis: ( x in dom (Fn1 | [:{y},Z1:]) implies (Fn1 | [:{y},Z1:]) . x = (Fn2 | [:{y},Z1:]) . x ) assume A334: x in dom (Fn1 | [:{y},Z1:]) ; ::_thesis: (Fn1 | [:{y},Z1:]) . x = (Fn2 | [:{y},Z1:]) . x consider x1, x2 being set such that A335: x1 in {y} and A336: x2 in Z1 and A337: x = [x1,x2] by A325, A334, ZFMISC_1:def_2; reconsider xy = {x1} as non empty Subset of Y by A335, ZFMISC_1:31; A338: xy c= N2 by A292, A335, ZFMISC_1:31; then A339: [:xy,ZZ:] c= [:N2, the carrier of I[01]:] by ZFMISC_1:96; A340: x1 = y by A335, TARSKI:def_1; then [x1,(TT . i)] in [:N,ZZ:] by A287, A329, ZFMISC_1:87; then A341: F . [x1,(TT . i)] in F .: [:N,ZZ:] by FUNCT_2:35; A342: xy c= N1 by A282, A335, ZFMISC_1:31; then reconsider xZZ = [:xy,ZZ:] as Subset of [:(Y | N1),I[01]:] by A293, ZFMISC_1:96; xy is connected by A335; then A343: [:xy,ZZ:] is connected by A328, TOPALG_3:16; A344: xy c= N by A287, A340, ZFMISC_1:31; A345: D is Cover of Fn1 .: xZZ proof let b be set ; :: according to TARSKI:def_3,SETFAM_1:def_11 ::_thesis: ( not b in Fn1 .: xZZ or b in union D ) A346: [:N,ZZ:] c= [: the carrier of Y, the carrier of I[01]:] by ZFMISC_1:96; assume b in Fn1 .: xZZ ; ::_thesis: b in union D then consider a being Point of [:(Y | N1),I[01]:] such that A347: a in xZZ and A348: Fn1 . a = b by FUNCT_2:65; A349: CircleMap . (Fn1 . a) = (CircleMap * Fn1) . a by FUNCT_2:15 .= F . a by A280, A293, FUNCT_1:49 ; [:xy,ZZ:] c= [:N,ZZ:] by A344, ZFMISC_1:95; then a in [:N,ZZ:] by A347; then F . a in F .: [:N,ZZ:] by A6, A346, FUNCT_1:def_6; hence b in union D by A331, A332, A348, A349, Lm12, FUNCT_1:def_7, TOPMETR:17; ::_thesis: verum end; A350: 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 A351: xZZ is connected by A343, CONNSP_1:23; reconsider XZZ = [:xy,ZZ:] as Subset of [:(Y | N2),I[01]:] by A294, A338, ZFMISC_1:96; [:(Y | N2),I[01]:] is SubSpace of [:Y,I[01]:] by A350, BORSUK_3:21; then A352: XZZ is connected by A343, CONNSP_1:23; A353: D is Cover of Fn2 .: xZZ proof let b be set ; :: according to TARSKI:def_3,SETFAM_1:def_11 ::_thesis: ( not b in Fn2 .: xZZ or b in union D ) A354: [:N,ZZ:] c= [: the carrier of Y, the carrier of I[01]:] by ZFMISC_1:96; assume b in Fn2 .: xZZ ; ::_thesis: b in union D then consider a being Point of [:(Y | N2),I[01]:] such that A355: a in xZZ and A356: Fn2 . a = b by FUNCT_2:65; A357: CircleMap . (Fn2 . a) = (CircleMap * Fn2) . a by FUNCT_2:15 .= F . a by A278, A294, FUNCT_1:49 ; [:xy,ZZ:] c= [:N,ZZ:] by A344, ZFMISC_1:95; then a in [:N,ZZ:] by A355; then F . a in F .: [:N,ZZ:] by A6, A354, FUNCT_1:def_6; hence b in union D by A331, A332, A356, A357, Lm12, FUNCT_1:def_7, TOPMETR:17; ::_thesis: verum end; A358: TT . i in Z by A318, A316, XXREAL_1:1; then A359: [x1,(TT . i)] in [:{y},Z:] by A335, ZFMISC_1:87; A360: [:{y},Z:] c= [:N1, the carrier of I[01]:] by A282, ZFMISC_1:96; then F . [x1,(TT . i)] = (CircleMap * Fn1) . [x1,(TT . i)] by A280, A359, FUNCT_1:49 .= CircleMap . (Fn1 . [x1,(TT . i)]) by A295, A359, A360, FUNCT_1:13 ; then Fn1 . [x1,(TT . i)] in CircleMap " Ui by A331, A341, FUNCT_2:38, TOPMETR:17; then consider Uit being set such that A361: Fn1 . [x1,(TT . i)] in Uit and A362: Uit in D by A332, TARSKI:def_4; reconsider Uit = Uit as non empty Subset of R^1 by A361, A362; set f = CircleMap | Uit; A363: dom (CircleMap | Uit) = Uit by Lm12, RELAT_1:62, TOPMETR:17; A364: rng (CircleMap | Uit) c= Ui proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in rng (CircleMap | Uit) or b in Ui ) assume b in rng (CircleMap | Uit) ; ::_thesis: b in Ui then consider a being set such that A365: a in dom (CircleMap | Uit) and A366: (CircleMap | Uit) . a = b by FUNCT_1:def_3; a in union D by A362, A363, A365, TARSKI:def_4; then CircleMap . a in Ui by A332, FUNCT_2:38; hence b in Ui by A363, A365, A366, FUNCT_1:49; ::_thesis: verum end; ( the carrier of ((Tunit_circle 2) | Ui) = Ui & the carrier of (R^1 | Uit) = Uit ) by PRE_TOPC:8; then reconsider f = CircleMap | Uit as Function of (R^1 | Uit),((Tunit_circle 2) | Ui) by A363, A364, FUNCT_2:2; A367: [:N2,Z:] c= [:N2, the carrier of I[01]:] by ZFMISC_1:95; A368: [x1,(TT . i)] in [:N2,Z:] by A292, A335, A358, ZFMISC_1:87; then F . [x1,(TT . i)] = (CircleMap * Fn2) . [x1,(TT . i)] by A278, A367, FUNCT_1:49 .= CircleMap . (Fn2 . [x1,(TT . i)]) by A290, A294, A368, A367, FUNCT_1:13 ; then Fn2 . [x1,(TT . i)] in CircleMap " Ui by A331, A341, FUNCT_2:38, TOPMETR:17; then consider Uith being set such that A369: Fn2 . [x1,(TT . i)] in Uith and A370: Uith in D by A332, TARSKI:def_4; reconsider Uith = Uith as non empty Subset of R^1 by A369, A370; A371: dom (Fn1 | [:xy,ZZ:]) = [:xy,ZZ:] by A293, A296, A342, RELAT_1:62, ZFMISC_1:96; A372: x1 in xy by TARSKI:def_1; then A373: [x1,(TT . i)] in xZZ by A329, ZFMISC_1:87; then Fn1 . [x1,(TT . i)] in Fn1 .: xZZ by FUNCT_2:35; then Uit meets Fn1 .: xZZ by A361, XBOOLE_0:3; then A374: Fn1 .: xZZ c= Uit by A277, A362, A351, A345, TOPALG_3:12, TOPS_2:61; A375: rng (Fn1 | [:xy,ZZ:]) c= dom f proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in rng (Fn1 | [:xy,ZZ:]) or b in dom f ) assume b in rng (Fn1 | [:xy,ZZ:]) ; ::_thesis: b in dom f then consider a being set such that A376: a in dom (Fn1 | [:xy,ZZ:]) and A377: (Fn1 | [:xy,ZZ:]) . a = b by FUNCT_1:def_3; Fn1 . a = b by A371, A376, A377, FUNCT_1:49; then b in Fn1 .: xZZ by A296, A371, A376, FUNCT_1:def_6; hence b in dom f by A374, A363; ::_thesis: verum end; then A378: dom (f * (Fn1 | [:xy,ZZ:])) = dom (Fn1 | [:xy,ZZ:]) by RELAT_1:27; [x1,(TT . i)] in [:xy,ZZ:] by A335, A340, A329, ZFMISC_1:87; then [x1,(TT . i)] in dom Fn2 by A291, A339; then A379: Fn2 . [x1,(TT . i)] in Fn2 .: xZZ by A373, FUNCT_2:35; then Uith meets Fn2 .: xZZ by A369, XBOOLE_0:3; then A380: Fn2 .: xZZ c= Uith by A276, A370, A352, A353, TOPALG_3:12, TOPS_2:61; Fn1 . [x1,(TT . i)] = (Fn1 | [:{y},Z:]) . [x1,(TT . i)] by A359, FUNCT_1:49 .= Fn2 . [x1,(TT . i)] by A319, A359, FUNCT_1:49 ; then Uit meets Uith by A361, A379, A380, XBOOLE_0:3; then A381: Uit = Uith by A362, A370, TAXONOM2:def_5; A382: for x being set st x in dom (f * (Fn1 | [:xy,ZZ:])) holds (f * (Fn1 | [:xy,ZZ:])) . x = (f * (Fn2 | [:xy,ZZ:])) . x proof A383: dom (Fn1 | [:xy,ZZ:]) c= dom Fn1 by RELAT_1:60; let x be set ; ::_thesis: ( x in dom (f * (Fn1 | [:xy,ZZ:])) implies (f * (Fn1 | [:xy,ZZ:])) . x = (f * (Fn2 | [:xy,ZZ:])) . x ) assume A384: x in dom (f * (Fn1 | [:xy,ZZ:])) ; ::_thesis: (f * (Fn1 | [:xy,ZZ:])) . x = (f * (Fn2 | [:xy,ZZ:])) . x A385: Fn1 . x in Fn1 .: [:xy,ZZ:] by A296, A371, A378, A384, FUNCT_1:def_6; A386: Fn2 . x in Fn2 .: [:xy,ZZ:] by A291, A339, A371, A378, A384, FUNCT_1:def_6; dom (Fn1 | [:xy,ZZ:]) = (dom Fn1) /\ [:xy,ZZ:] by RELAT_1:61; then A387: x in [:xy,ZZ:] by A378, A384, XBOOLE_0:def_4; thus (f * (Fn1 | [:xy,ZZ:])) . x = ((f * Fn1) | [:xy,ZZ:]) . x by RELAT_1:83 .= (f * Fn1) . x by A371, A378, A384, FUNCT_1:49 .= f . (Fn1 . x) by A296, A384, FUNCT_1:13 .= CircleMap . (Fn1 . x) by A374, A385, FUNCT_1:49 .= (CircleMap * Fn1) . x by A296, A384, FUNCT_1:13 .= F . x by A280, A295, A378, A384, A383, FUNCT_1:49 .= (CircleMap * Fn2) . x by A278, A339, A387, FUNCT_1:49 .= CircleMap . (Fn2 . x) by A291, A339, A387, FUNCT_1:13 .= f . (Fn2 . x) by A380, A381, A386, FUNCT_1:49 .= (f * Fn2) . x by A291, A339, A387, FUNCT_1:13 .= ((f * Fn2) | [:xy,ZZ:]) . x by A371, A378, A384, FUNCT_1:49 .= (f * (Fn2 | [:xy,ZZ:])) . x by RELAT_1:83 ; ::_thesis: verum end; A388: dom (Fn2 | [:xy,ZZ:]) = [:xy,ZZ:] by A290, A294, A338, RELAT_1:62, ZFMISC_1:96; A389: rng (Fn2 | [:xy,ZZ:]) c= dom f proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in rng (Fn2 | [:xy,ZZ:]) or b in dom f ) assume b in rng (Fn2 | [:xy,ZZ:]) ; ::_thesis: b in dom f then consider a being set such that A390: a in dom (Fn2 | [:xy,ZZ:]) and A391: (Fn2 | [:xy,ZZ:]) . a = b by FUNCT_1:def_3; Fn2 . a = b by A388, A390, A391, FUNCT_1:49; then b in Fn2 .: xZZ by A290, A388, A390, FUNCT_1:def_6; hence b in dom f by A380, A381, A363; ::_thesis: verum end; then dom (f * (Fn2 | [:xy,ZZ:])) = dom (Fn2 | [:xy,ZZ:]) by RELAT_1:27; then A392: f * (Fn1 | [:xy,ZZ:]) = f * (Fn2 | [:xy,ZZ:]) by A371, A388, A375, A382, FUNCT_1:2, RELAT_1:27; f is being_homeomorphism by A333, A362; then A393: f is one-to-one by TOPS_2:def_5; percases ( x2 in ZZ or not x2 in ZZ ) ; suppose x2 in ZZ ; ::_thesis: (Fn1 | [:{y},Z1:]) . x = (Fn2 | [:{y},Z1:]) . x then A394: x in [:xy,ZZ:] by A337, A372, ZFMISC_1:87; thus (Fn1 | [:{y},Z1:]) . x = Fn1 . x by A325, A334, FUNCT_1:49 .= (Fn1 | [:xy,ZZ:]) . x by A394, FUNCT_1:49 .= (Fn2 | [:xy,ZZ:]) . x by A393, A371, A388, A375, A389, A392, FUNCT_1:27 .= Fn2 . x by A394, FUNCT_1:49 .= (Fn2 | [:{y},Z1:]) . x by A325, A334, FUNCT_1:49 ; ::_thesis: verum end; suppose not x2 in ZZ ; ::_thesis: (Fn1 | [:{y},Z1:]) . x = (Fn2 | [:{y},Z1:]) . x then x2 in Z by A336, XBOOLE_0:def_3; then A395: x in [:{y},Z:] by A335, A337, ZFMISC_1:87; thus (Fn1 | [:{y},Z1:]) . x = Fn1 . x by A325, A334, FUNCT_1:49 .= (Fn1 | [:{y},Z:]) . x by A395, FUNCT_1:49 .= Fn2 . x by A319, A395, FUNCT_1:49 .= (Fn2 | [:{y},Z1:]) . x by A325, A334, FUNCT_1:49 ; ::_thesis: verum end; end; end; dom (Fn2 | [:{y},Z1:]) = [:{y},Z1:] by A292, A290, A294, RELAT_1:62, ZFMISC_1:96; hence Fn1 | [:{y},Z1:] = Fn2 | [:{y},Z1:] by A325, A326, FUNCT_1:2; ::_thesis: verum end; end; end; A396: S2[ 0 ] by FINSEQ_3:24; for i being Element of NAT holds S2[i] from NAT_1:sch_1(A396, A298); then ex Z being non empty Subset of I[01] st ( Z = [.0,(TT . (len TT)).] & Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:] ) by A289; hence Fn1 | [:{y}, the carrier of I[01]:] = Fn2 | [:{y}, the carrier of I[01]:] by A284, BORSUK_1:40; ::_thesis: verum end; for p being Point of [:Y,I[01]:] for 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]:]; ::_thesis: for 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 ) let V be Subset of R^1; ::_thesis: ( G . p in V & V is open implies ex W being Subset of [:Y,I[01]:] st ( p in W & W is open & G .: W c= V ) ) assume A397: ( G . p in V & V is open ) ; ::_thesis: ex W being Subset of [:Y,I[01]:] st ( p in W & W is open & G .: W c= V ) 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 A398: p = [y,t] and A399: G . p = Fn . p and A400: y in N and A401: Fn is continuous and A402: ( F | [:N, the carrier of I[01]:] = CircleMap * Fn & Fn | [: the carrier of Y,{0}:] = Ft | [:N, the carrier of I[01]:] ) and for H being Function of [:(Y | N),I[01]:],R^1 st H is continuous & F | [:N, the carrier of I[01]:] = CircleMap * H & H | [: the carrier of Y,{0}:] = Ft | [:N, the carrier of I[01]:] holds Fn = H by A271; A403: the carrier of [:(Y | N),I[01]:] = [: the carrier of (Y | N), the carrier of I[01]:] by BORSUK_1:def_2 .= [:N, the carrier of I[01]:] by PRE_TOPC:8 ; then p in the carrier of [:(Y | N),I[01]:] by A398, A400, ZFMISC_1:87; then consider W being Subset of [:(Y | N),I[01]:] such that A404: p in W and A405: W is open and A406: Fn .: W c= V by A397, A399, A401, JGRAPH_2:10; A407: dom Fn = [:N, the carrier of I[01]:] by A403, FUNCT_2:def_1; A408: [#] (Y | N) = N by PRE_TOPC:def_5; then A409: [#] [:(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 A410: C is open and A411: C /\ ([#] [:(Y | N),I[01]:]) = W by A405, TOPS_2:24; take WW = C /\ [:N,([#] I[01]):]; ::_thesis: ( p in WW & WW is open & G .: WW c= V ) thus p in WW by A404, A411, A408, BORSUK_3:1; ::_thesis: ( WW is open & G .: WW c= V ) [:N,([#] I[01]):] is open by BORSUK_1:6; hence WW is open by A410; ::_thesis: G .: WW c= V let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in G .: WW or y in V ) assume y in G .: WW ; ::_thesis: y in V then consider x being Point of [:Y,I[01]:] such that A412: x in WW and A413: 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 A414: x = [y0,t0] and A415: G . x = Fn0 . x and A416: ( y0 in N0 & Fn0 is continuous & F | [:N0, the carrier of I[01]:] = CircleMap * Fn0 & Fn0 | [: the carrier of Y,{0}:] = Ft | [:N0, the carrier of I[01]:] ) and for H being Function of [:(Y | N0),I[01]:],R^1 st H is continuous & F | [:N0, the carrier of I[01]:] = CircleMap * H & H | [: the carrier of Y,{0}:] = Ft | [:N0, the carrier of I[01]:] holds Fn0 = H by A271; x in [:N,([#] I[01]):] by A412, XBOOLE_0:def_4; then A417: y0 in N by A414, ZFMISC_1:87; A418: x in [:{y0}, the carrier of I[01]:] by A414, ZFMISC_1:105; then Fn . x = (Fn | [:{y0}, the carrier of I[01]:]) . x by FUNCT_1:49 .= (Fn0 | [:{y0}, the carrier of I[01]:]) . x by A273, A401, A402, A414, A416, A417 .= Fn0 . x by A418, FUNCT_1:49 ; then y in Fn .: W by A407, A411, A409, A412, A413, A415, FUNCT_1:def_6; hence y in V by A406; ::_thesis: verum end; hence G is continuous by JGRAPH_2:10; ::_thesis: ( 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 ) ) for x being Point of [:Y,I[01]:] holds F . x = (CircleMap * G) . x proof let x be Point of [:Y,I[01]:]; ::_thesis: F . x = (CircleMap * G) . x 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 A419: x = [y,t] and A420: G . x = Fn . x and A421: y in N and Fn is continuous and A422: F | [:N, the carrier of I[01]:] = CircleMap * Fn and Fn | [: the carrier of Y,{0}:] = Ft | [:N, the carrier of I[01]:] and for H being Function of [:(Y | N),I[01]:],R^1 st H is continuous & F | [:N, the carrier of I[01]:] = CircleMap * H & H | [: the carrier of Y,{0}:] = Ft | [:N, the carrier of I[01]:] holds Fn = H by A271; A423: the carrier of [:(Y | N),I[01]:] = [: the carrier of (Y | N), the carrier of I[01]:] by BORSUK_1:def_2 .= [:N, the carrier of I[01]:] by PRE_TOPC:8 ; then A424: x in the carrier of [:(Y | N),I[01]:] by A419, A421, ZFMISC_1:87; thus (CircleMap * G) . x = CircleMap . (G . x) by FUNCT_2:15 .= (CircleMap * Fn) . x by A420, A424, FUNCT_2:15 .= F . x by A422, A423, A424, FUNCT_1:49 ; ::_thesis: verum end; hence F = CircleMap * G by FUNCT_2:63; ::_thesis: ( 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 ) ) A425: [: the carrier of Y,{0}:] c= [: the carrier of Y, the carrier of I[01]:] by Lm3, ZFMISC_1:95; A426: the carrier of [:Y,I[01]:] = [: the carrier of Y, the carrier of I[01]:] by BORSUK_1:def_2; then A427: dom G = [: the carrier of Y, the carrier of I[01]:] by FUNCT_2:def_1; A428: for x being set st x in dom Ft holds Ft . x = G . x proof let x be set ; ::_thesis: ( x in dom Ft implies Ft . x = G . x ) assume A429: x in dom Ft ; ::_thesis: Ft . x = G . x then x in dom G by A8, A427, A425; 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 A430: x = [y,t] and A431: G . x = Fn . x and A432: y in N and Fn is continuous and F | [:N, the carrier of I[01]:] = CircleMap * Fn and A433: Fn | [: the carrier of Y,{0}:] = Ft | [:N, the carrier of I[01]:] and for H being Function of [:(Y | N),I[01]:],R^1 st H is continuous & F | [:N, the carrier of I[01]:] = CircleMap * H & H | [: the carrier of Y,{0}:] = Ft | [:N, the carrier of I[01]:] holds Fn = H by A271; x in [:N, the carrier of I[01]:] by A430, A432, ZFMISC_1:87; hence Ft . x = (Ft | [:N, the carrier of I[01]:]) . x by FUNCT_1:49 .= G . x by A7, A429, A431, A433, Lm14, FUNCT_1:49 ; ::_thesis: verum end; dom Ft = (dom G) /\ [: the carrier of Y,{0}:] by A8, A427, A425, XBOOLE_1:28; hence G | [: the carrier of Y,{0}:] = Ft by A428, FUNCT_1:46; ::_thesis: 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 let H be Function of [:Y,I[01]:],R^1; ::_thesis: ( H is continuous & F = CircleMap * H & H | [: the carrier of Y,{0}:] = Ft implies G = H ) assume that A434: ( H is continuous & F = CircleMap * H ) and A435: H | [: the carrier of Y,{0}:] = Ft ; ::_thesis: G = H for x being Point of [:Y,I[01]:] holds G . x = H . x proof let x be Point of [:Y,I[01]:]; ::_thesis: G . x = H . x 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 A436: x = [y,t] and A437: G . x = Fn . x and A438: y in N and Fn is continuous and F | [:N, the carrier of I[01]:] = CircleMap * Fn and Fn | [: the carrier of Y,{0}:] = Ft | [:N, the carrier of I[01]:] and A439: for H being Function of [:(Y | N),I[01]:],R^1 st H is continuous & F | [:N, the carrier of I[01]:] = CircleMap * H & H | [: the carrier of Y,{0}:] = Ft | [:N, the carrier of I[01]:] holds Fn = H by A271; A440: the carrier of [:(Y | N),I[01]:] = [: the carrier of (Y | N), the carrier of I[01]:] by BORSUK_1:def_2 .= [:N, the carrier of I[01]:] by PRE_TOPC:8 ; then A441: x in the carrier of [:(Y | N),I[01]:] by A436, A438, ZFMISC_1:87; dom H = the carrier of [:Y,I[01]:] by FUNCT_2:def_1; then [:N, the carrier of I[01]:] c= dom H by A426, ZFMISC_1:95; then A442: dom (H | [:N, the carrier of I[01]:]) = [:N, the carrier of I[01]:] by RELAT_1:62; rng (H | [:N, the carrier of I[01]:]) c= the carrier of R^1 ; then reconsider H1 = H | [:N, the carrier of I[01]:] as Function of [:(Y | N),I[01]:],R^1 by A440, A442, FUNCT_2:2; A443: (H | [:N, the carrier of I[01]:]) | [: the carrier of Y,{0}:] = H | ([: the carrier of Y,{0}:] /\ [:N, the carrier of I[01]:]) by RELAT_1:71 .= Ft | [:N, the carrier of I[01]:] by A435, RELAT_1:71 ; ( H1 is continuous & F | [:N, the carrier of I[01]:] = CircleMap * (H | [:N, the carrier of I[01]:]) ) by A434, RELAT_1:83, TOPALG_3:17; hence G . x = (H | [:N, the carrier of I[01]:]) . x by A437, A439, A443 .= H . x by A440, A441, FUNCT_1:49 ; ::_thesis: verum end; hence G = H by FUNCT_2:63; ::_thesis: verum end; theorem Th23: :: TOPALG_5:23 for x0, y0 being Point of (Tunit_circle 2) for xt being Point of R^1 for f being Path of x0,y0 st xt in CircleMap " {x0} holds 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 (Tunit_circle 2); ::_thesis: for xt being Point of R^1 for f being Path of x0,y0 st xt in CircleMap " {x0} holds 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 ) ) let xt be Point of R^1; ::_thesis: for f being Path of x0,y0 st xt in CircleMap " {x0} holds 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 ) ) let f be Path of x0,y0; ::_thesis: ( xt in CircleMap " {x0} implies 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 ) ) ) deffunc H1( set , Element of the carrier of I[01]) -> Element of the carrier of (Tunit_circle 2) = f . $2; consider F being Function of [: the carrier of (1TopSp {1}), the carrier of I[01]:], the carrier of (Tunit_circle 2) such that A1: for y being Element of (1TopSp {1}) for i being Element of the carrier of I[01] holds F . (y,i) = H1(y,i) from BINOP_1:sch_4(); reconsider j = 1 as Point of (1TopSp {1}) by TARSKI:def_1; A2: [j,j0] in [: the carrier of (1TopSp {1}),{0}:] by Lm4, ZFMISC_1:87; A3: the carrier of [:(1TopSp {1}),I[01]:] = [: the carrier of (1TopSp {1}), the carrier of I[01]:] by BORSUK_1:def_2; then reconsider F = F as Function of [:(1TopSp {1}),I[01]:],(Tunit_circle 2) ; set Ft = [:(1TopSp {1}),(Sspace 0[01]):] --> xt; A4: the carrier of [:(1TopSp {1}),(Sspace 0[01]):] = [: the carrier of (1TopSp {1}), the carrier of (Sspace 0[01]):] by BORSUK_1:def_2; then A5: for y being Element of (1TopSp {1}) for i being Element of {0} holds ([:(1TopSp {1}),(Sspace 0[01]):] --> xt) . [y,i] = xt by Lm14, FUNCOP_1:7; A6: [#] (1TopSp {1}) = the carrier of (1TopSp {1}) ; for p being Point of [:(1TopSp {1}),I[01]:] for V being Subset of (Tunit_circle 2) st F . p in V & V is open holds ex W being Subset of [:(1TopSp {1}),I[01]:] st ( p in W & W is open & F .: W c= V ) proof let p be Point of [:(1TopSp {1}),I[01]:]; ::_thesis: for V being Subset of (Tunit_circle 2) st F . p in V & V is open holds ex W being Subset of [:(1TopSp {1}),I[01]:] st ( p in W & W is open & F .: W c= V ) let V be Subset of (Tunit_circle 2); ::_thesis: ( F . p in V & V is open implies ex W being Subset of [:(1TopSp {1}),I[01]:] st ( p in W & W is open & F .: W c= V ) ) assume A7: ( F . p in V & V is open ) ; ::_thesis: ex W being Subset of [:(1TopSp {1}),I[01]:] st ( p in W & W is open & F .: W c= V ) consider p1 being Point of (1TopSp {1}), 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:]; [:{1},S:] c= [: the carrier of (1TopSp {1}), the carrier of I[01]:] by ZFMISC_1:95; then reconsider W = [:{1},S:] as Subset of [:(1TopSp {1}),I[01]:] by BORSUK_1:def_2; take W ; ::_thesis: ( p in W & W is open & F .: W c= V ) thus p in W by A8, A9, ZFMISC_1:87; ::_thesis: ( W is open & F .: W c= V ) thus W is open by A6, A10, BORSUK_1:6; ::_thesis: F .: W c= V let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in F .: W or y in V ) assume y in F .: W ; ::_thesis: y in V then consider x being set such that A12: x in the carrier of [:(1TopSp {1}),I[01]:] and A13: x in W and A14: y = F . x by FUNCT_2:64; consider x1 being Point of (1TopSp {1}), 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 y in V by A11, A16; ::_thesis: verum end; then A17: F is continuous by JGRAPH_2:10; assume xt in CircleMap " {x0} ; ::_thesis: 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 ) ) then A18: CircleMap . xt in {x0} by FUNCT_2:38; A19: for x being set st x in dom (CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt)) holds (F | [: the carrier of (1TopSp {1}),{0}:]) . x = (CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt)) . x proof let x be set ; ::_thesis: ( x in dom (CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt)) implies (F | [: the carrier of (1TopSp {1}),{0}:]) . x = (CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt)) . x ) assume A20: x in dom (CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt)) ; ::_thesis: (F | [: the carrier of (1TopSp {1}),{0}:]) . x = (CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt)) . x consider x1, x2 being set such that A21: x1 in the carrier of (1TopSp {1}) 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 (1TopSp {1}),{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 . (([:(1TopSp {1}),(Sspace 0[01]):] --> xt) . x) by A5, A21, A22, A23 .= (CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt)) . x by A20, FUNCT_1:12 ; ::_thesis: verum end; A25: dom (CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt)) = [: the carrier of (1TopSp {1}),{0}:] by A4, Lm14, FUNCT_2:def_1; A26: dom F = the carrier of [:(1TopSp {1}),I[01]:] by FUNCT_2:def_1; then A27: [: the carrier of (1TopSp {1}),{0}:] c= dom F by A3, Lm3, ZFMISC_1:95; then dom (F | [: the carrier of (1TopSp {1}),{0}:]) = [: the carrier of (1TopSp {1}),{0}:] by RELAT_1:62; then consider G being Function of [:(1TopSp {1}),I[01]:],R^1 such that A28: G is continuous and A29: F = CircleMap * G and A30: G | [: the carrier of (1TopSp {1}),{0}:] = [:(1TopSp {1}),(Sspace 0[01]):] --> xt and A31: for H being Function of [:(1TopSp {1}),I[01]:],R^1 st H is continuous & F = CircleMap * H & H | [: the carrier of (1TopSp {1}),{0}:] = [:(1TopSp {1}),(Sspace 0[01]):] --> xt holds G = H by A17, A25, A19, Th22, FUNCT_1:2; take ft = Prj2 (j,G); ::_thesis: ( 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 ) ) thus ft . 0 = G . (j,j0) by Def3 .= ([:(1TopSp {1}),(Sspace 0[01]):] --> xt) . [j,j0] by A30, A2, FUNCT_1:49 .= xt by A5, Lm4 ; ::_thesis: ( 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 ) ) for i being Point of I[01] holds f . i = (CircleMap * ft) . i proof let i be Point of I[01]; ::_thesis: f . i = (CircleMap * ft) . i A32: the carrier of [:(1TopSp {1}),I[01]:] = [: the carrier of (1TopSp {1}), 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 ; ::_thesis: verum end; hence f = CircleMap * ft by FUNCT_2:63; ::_thesis: ( 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 ) ) thus ft is continuous by A28; ::_thesis: for f1 being Function of I[01],R^1 st f1 is continuous & f = CircleMap * f1 & f1 . 0 = xt holds ft = f1 let f1 be Function of I[01],R^1; ::_thesis: ( f1 is continuous & f = CircleMap * f1 & f1 . 0 = xt implies ft = f1 ) deffunc H2( set , Element of the carrier of I[01]) -> Element of the carrier of R^1 = f1 . $2; consider H being Function of [: the carrier of (1TopSp {1}), the carrier of I[01]:], the carrier of R^1 such that A33: for y being Element of (1TopSp {1}) for i being Element of the carrier of I[01] holds H . (y,i) = H2(y,i) from BINOP_1:sch_4(); reconsider H = H as Function of [:(1TopSp {1}),I[01]:],R^1 by A3; assume that A34: f1 is continuous and A35: f = CircleMap * f1 and A36: f1 . 0 = xt ; ::_thesis: ft = f1 for p being Point of [:(1TopSp {1}),I[01]:] for V being Subset of R^1 st H . p in V & V is open holds ex W being Subset of [:(1TopSp {1}),I[01]:] st ( p in W & W is open & H .: W c= V ) proof let p be Point of [:(1TopSp {1}),I[01]:]; ::_thesis: for V being Subset of R^1 st H . p in V & V is open holds ex W being Subset of [:(1TopSp {1}),I[01]:] st ( p in W & W is open & H .: W c= V ) let V be Subset of R^1; ::_thesis: ( H . p in V & V is open implies ex W being Subset of [:(1TopSp {1}),I[01]:] st ( p in W & W is open & H .: W c= V ) ) assume A37: ( H . p in V & V is open ) ; ::_thesis: ex W being Subset of [:(1TopSp {1}),I[01]:] st ( p in W & W is open & H .: W c= V ) consider p1 being Point of (1TopSp {1}), 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 = [:([#] (1TopSp {1})),W:]; ::_thesis: ( p in W1 & W1 is open & H .: W1 c= V ) thus p in W1 by A38, A39, ZFMISC_1:87; ::_thesis: ( W1 is open & H .: W1 c= V ) thus W1 is open by A40, BORSUK_1:6; ::_thesis: H .: W1 c= V let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in H .: W1 or y in V ) assume y in H .: W1 ; ::_thesis: y in V then consider c being Element of [:(1TopSp {1}),I[01]:] such that A42: c in W1 and A43: y = H . c by FUNCT_2:65; consider c1, c2 being set such that A44: c1 in [#] (1TopSp {1}) 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 y in V by A41, A43, A47; ::_thesis: verum end; then A48: H is continuous by JGRAPH_2:10; for x being Point of [:(1TopSp {1}),I[01]:] holds F . x = (CircleMap * H) . x proof let x be Point of [:(1TopSp {1}),I[01]:]; ::_thesis: F . x = (CircleMap * H) . x consider x1 being Point of (1TopSp {1}), 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 ; ::_thesis: verum end; then A50: F = CircleMap * H by FUNCT_2:63; for i being Point of I[01] holds ft . i = f1 . i proof let i be Point of I[01]; ::_thesis: ft . i = f1 . i A51: dom H = the carrier of [:(1TopSp {1}),I[01]:] by FUNCT_2:def_1; then A52: dom (H | [: the carrier of (1TopSp {1}),{0}:]) = [: the carrier of (1TopSp {1}),{0}:] by A26, A27, RELAT_1:62; A53: for x being set st x in dom (H | [: the carrier of (1TopSp {1}),{0}:]) holds (H | [: the carrier of (1TopSp {1}),{0}:]) . x = ([:(1TopSp {1}),(Sspace 0[01]):] --> xt) . x proof let x be set ; ::_thesis: ( x in dom (H | [: the carrier of (1TopSp {1}),{0}:]) implies (H | [: the carrier of (1TopSp {1}),{0}:]) . x = ([:(1TopSp {1}),(Sspace 0[01]):] --> xt) . x ) assume A54: x in dom (H | [: the carrier of (1TopSp {1}),{0}:]) ; ::_thesis: (H | [: the carrier of (1TopSp {1}),{0}:]) . x = ([:(1TopSp {1}),(Sspace 0[01]):] --> xt) . x then consider x1, x2 being set such that A55: x1 in the carrier of (1TopSp {1}) 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 (1TopSp {1}),{0}:]) . x = H . (x1,x2) by A54, A57, FUNCT_1:47 .= f1 . x2 by A33, A55, A58 .= ([:(1TopSp {1}),(Sspace 0[01]):] --> xt) . x by A5, A36, A55, A56, A57, A58 ; ::_thesis: verum end; dom ([:(1TopSp {1}),(Sspace 0[01]):] --> xt) = [: the carrier of (1TopSp {1}),{0}:] by A4, Lm14, FUNCT_2:def_1; then A59: H | [: the carrier of (1TopSp {1}),{0}:] = [:(1TopSp {1}),(Sspace 0[01]):] --> xt by A26, A27, A51, A53, FUNCT_1:2, RELAT_1:62; thus ft . i = G . (j,i) by Def3 .= H . (j,i) by A31, A50, A48, A59 .= f1 . i by A33 ; ::_thesis: verum end; hence ft = f1 by FUNCT_2:63; ::_thesis: verum end; theorem Th24: :: TOPALG_5:24 for x0, y0 being Point of (Tunit_circle 2) for P, Q being Path of x0,y0 for F being Homotopy of P,Q for xt being Point of R^1 st P,Q are_homotopic & xt in CircleMap " {x0} holds ex yt being Point of R^1 ex Pt, Qt being Path of xt,yt ex 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 (Tunit_circle 2); ::_thesis: for P, Q being Path of x0,y0 for F being Homotopy of P,Q for xt being Point of R^1 st P,Q are_homotopic & xt in CircleMap " {x0} holds ex yt being Point of R^1 ex Pt, Qt being Path of xt,yt ex 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 ) ) let P, Q be Path of x0,y0; ::_thesis: for F being Homotopy of P,Q for xt being Point of R^1 st P,Q are_homotopic & xt in CircleMap " {x0} holds ex yt being Point of R^1 ex Pt, Qt being Path of xt,yt ex 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 ) ) let F be Homotopy of P,Q; ::_thesis: for xt being Point of R^1 st P,Q are_homotopic & xt in CircleMap " {x0} holds ex yt being Point of R^1 ex Pt, Qt being Path of xt,yt ex 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 ) ) let xt be Point of R^1; ::_thesis: ( P,Q are_homotopic & xt in CircleMap " {x0} implies ex yt being Point of R^1 ex Pt, Qt being Path of xt,yt ex 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 ) ) ) 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 ; ::_thesis: ( not xt in CircleMap " {x0} or ex yt being Point of R^1 ex Pt, Qt being Path of xt,yt ex 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 ) ) ) then A2: F is continuous by BORSUK_6:def_11; assume A3: xt in CircleMap " {x0} ; ::_thesis: ex yt being Point of R^1 ex Pt, Qt being Path of xt,yt ex 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 ) ) 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 S1[ set , set , set ] means $3 = ft . $1; A7: for x being Element of the carrier of I[01] for y being Element of {0} ex z being Element of REAL st S1[x,y,z] ; consider Ft being Function of [: the carrier of I[01],{0}:],REAL such that A8: for y being Element of the carrier of I[01] for i being Element of {0} holds S1[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 the constant Loop of x0 . x = (CircleMap * (I[01] --> xt)) . x proof let x be Point of I[01]; ::_thesis: the constant Loop of x0 . x = (CircleMap * (I[01] --> xt)) . x thus the constant Loop of x0 . x = x0 by TOPALG_3:21 .= CircleMap . ((I[01] --> xt) . x) by A9, TOPALG_3:4 .= (CircleMap * (I[01] --> xt)) . x by FUNCT_2:15 ; ::_thesis: verum end; consider ft1 being Function of I[01],R^1 such that ft1 . 0 = xt and the constant Loop of x0 = CircleMap * ft1 and ft1 is continuous and A11: for f1 being Function of I[01],R^1 st f1 is continuous & the constant Loop of x0 = CircleMap * f1 & f1 . 0 = xt holds ft1 = f1 by A3, Th23; (I[01] --> xt) . j0 = xt by TOPALG_3:4; then A12: ft1 = I[01] --> xt by A11, A10, FUNCT_2:63; A13: rng Ft c= REAL ; A14: dom Ft = [: the carrier of I[01],{0}:] by FUNCT_2:def_1; A15: the carrier of [:I[01],(Sspace 0[01]):] = [: the carrier of I[01], the carrier of (Sspace 0[01]):] by BORSUK_1:def_2; then reconsider Ft = Ft as Function of [:I[01],(Sspace 0[01]):],R^1 by Lm14, TOPMETR:17; A16: for x being set st x in dom (CircleMap * Ft) holds (F | [: the carrier of I[01],{0}:]) . x = (CircleMap * Ft) . x proof let x be set ; ::_thesis: ( x in dom (CircleMap * Ft) implies (F | [: the carrier of I[01],{0}:]) . x = (CircleMap * Ft) . x ) assume A17: x in dom (CircleMap * Ft) ; ::_thesis: (F | [: the carrier of I[01],{0}:]) . x = (CircleMap * Ft) . x consider x1, x2 being set such that A18: x1 in the carrier of I[01] 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 | [: the carrier of I[01],{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 ; ::_thesis: verum end; for p being Point of [:I[01],(Sspace 0[01]):] for 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]):]; ::_thesis: for 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 ) let V be Subset of R^1; ::_thesis: ( Ft . p in V & V is open implies ex W being Subset of [:I[01],(Sspace 0[01]):] st ( p in W & W is open & Ft .: W c= V ) ) assume A21: ( Ft . p in V & V is open ) ; ::_thesis: ex W being Subset of [:I[01],(Sspace 0[01]):] st ( p in W & W is open & Ft .: W c= V ) 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; S1[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 = W1 as non empty Subset of I[01] by A23; take W = [:W1,([#] (Sspace 0[01])):]; ::_thesis: ( p in W & W is open & Ft .: W c= V ) thus p in W by A22, A23, ZFMISC_1:def_2; ::_thesis: ( W is open & Ft .: W c= V ) thus W is open by A24, BORSUK_1:6; ::_thesis: Ft .: W c= V let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Ft .: W or y in V ) assume y in Ft .: W ; ::_thesis: y in V 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; ( S1[x1,x2,Ft . (x1,x2)] & ft . x1 in ft .: W1 ) by A8, Lm14, FUNCT_2:35; hence y in V by A25, A27, A28; ::_thesis: verum end; then A29: Ft is continuous by JGRAPH_2:10; take yt = ft . j1; ::_thesis: ex Pt, Qt being Path of xt,yt ex 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 ) ) A30: [j1,j0] in [: the carrier of I[01],{0}:] by Lm4, ZFMISC_1:87; reconsider ft = ft as Path of xt,yt by A4, A6, BORSUK_2:def_4; A31: [j0,j0] in [: the carrier of I[01],{0}:] by Lm4, ZFMISC_1:87; A32: dom F = the carrier of [:I[01],I[01]:] by FUNCT_2:def_1; then A33: [: the carrier of I[01],{0}:] c= dom F by Lm3, Lm5, ZFMISC_1:95; then dom (F | [: the carrier of I[01],{0}:]) = [: the carrier of I[01],{0}:] by RELAT_1:62; then F | [: the carrier of I[01],{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 | [: the carrier of I[01],{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 the constant Loop of x0 . x = (CircleMap * (Prj2 (j0,G))) . x proof let x be Point of I[01]; ::_thesis: the constant Loop of x0 . x = (CircleMap * (Prj2 (j0,G))) . x thus (CircleMap * (Prj2 (j0,G))) . x = CircleMap . ((Prj2 (j0,G)) . 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 .= the constant Loop of x0 . x by TOPALG_3:21 ; ::_thesis: verum 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 the constant Loop of y0 . x = (CircleMap * (I[01] --> yt)) . x proof let x be Point of I[01]; ::_thesis: the constant Loop of y0 . x = (CircleMap * (I[01] --> yt)) . x thus the constant Loop of y0 . x = y0 by TOPALG_3:21 .= CircleMap . ((I[01] --> yt) . x) by A39, TOPALG_3:4 .= (CircleMap * (I[01] --> yt)) . x by FUNCT_2:15 ; ::_thesis: verum 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 the constant Loop of y0 = CircleMap * ft2 and ft2 is continuous and A42: for f1 being Function of I[01],R^1 st f1 is continuous & the constant Loop of y0 = CircleMap * f1 & f1 . 0 = yt holds ft2 = f1 by Th23; (I[01] --> yt) . j0 = yt by TOPALG_3:4; then A43: ft2 = I[01] --> yt by A42, A40, FUNCT_2:63; set sM1 = Prj2 (j1,G); A44: for x being Point of I[01] holds the constant Loop of y0 . x = (CircleMap * (Prj2 (j1,G))) . x proof let x be Point of I[01]; ::_thesis: the constant Loop of y0 . x = (CircleMap * (Prj2 (j1,G))) . x thus (CircleMap * (Prj2 (j1,G))) . x = CircleMap . ((Prj2 (j1,G)) . 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 .= the constant Loop of y0 . x by TOPALG_3:21 ; ::_thesis: verum end; (Prj2 (j1,G)) . 0 = G . (j1,j0) by Def3 .= Ft . (j1,j0) by A36, A30, FUNCT_1:49 .= yt by A8, Lm4 ; then A45: ft2 = Prj2 (j1,G) by A34, A42, A44, FUNCT_2:63; (Prj2 (j0,G)) . 0 = G . (j0,j0) by Def3 .= Ft . (j0,j0) by A36, A31, FUNCT_1:49 .= xt by A4, A8, Lm4 ; then A46: ft1 = Prj2 (j0,G) by A34, A11, A38, FUNCT_2:63; set Qt = Prj1 (j1,G); A47: (Prj1 (j1,G)) . 0 = G . (j0,j1) by Def2 .= (Prj2 (j0,G)) . j1 by Def3 .= xt by A46, A12, TOPALG_3:4 ; (Prj1 (j1,G)) . 1 = G . (j1,j1) by Def2 .= (Prj2 (j1,G)) . j1 by Def3 .= yt by A45, A43, TOPALG_3:4 ; then reconsider Qt = Prj1 (j1,G) as Path of xt,yt by A34, A47, BORSUK_2:def_4; A48: now__::_thesis:_for_s_being_Point_of_I[01]_holds_ (_G_._(s,0)_=_ft_._s_&_G_._(s,1)_=_Qt_._s_&_(_for_t_being_Point_of_I[01]_holds_ (_G_._(0,t)_=_xt_&_G_._(1,t)_=_yt_)_)_) let s be Point of I[01]; ::_thesis: ( G . (s,0) = ft . s & G . (s,1) = Qt . s & ( for t being Point of I[01] holds ( G . (0,t) = xt & G . (1,t) = yt ) ) ) [s,0] in [: the carrier of I[01],{0}:] by Lm4, ZFMISC_1:87; hence G . (s,0) = Ft . (s,j0) by A36, FUNCT_1:49 .= ft . s by A8, Lm4 ; ::_thesis: ( G . (s,1) = Qt . s & ( for t being Point of I[01] holds ( G . (0,t) = xt & G . (1,t) = yt ) ) ) thus G . (s,1) = Qt . s by Def2; ::_thesis: for t being Point of I[01] holds ( G . (0,t) = xt & G . (1,t) = yt ) let t be Point of I[01]; ::_thesis: ( G . (0,t) = xt & G . (1,t) = yt ) thus G . (0,t) = (Prj2 (j0,G)) . t by Def3 .= xt by A46, A12, TOPALG_3:4 ; ::_thesis: G . (1,t) = yt thus G . (1,t) = (Prj2 (j1,G)) . t by Def3 .= yt by A45, A43, TOPALG_3:4 ; ::_thesis: verum end; then ft,Qt are_homotopic by A34, BORSUK_2:def_7; then reconsider G = G as Homotopy of ft,Qt by A34, A48, BORSUK_6:def_11; take ft ; ::_thesis: ex Qt being Path of xt,yt ex Ft being Homotopy of ft,Qt st ( ft,Qt are_homotopic & F = CircleMap * Ft & yt in CircleMap " {y0} & ( for F1 being Homotopy of ft,Qt st F = CircleMap * F1 holds Ft = F1 ) ) take Qt ; ::_thesis: ex Ft being Homotopy of ft,Qt st ( ft,Qt are_homotopic & F = CircleMap * Ft & yt in CircleMap " {y0} & ( for F1 being Homotopy of ft,Qt st F = CircleMap * F1 holds Ft = F1 ) ) take G ; ::_thesis: ( ft,Qt are_homotopic & F = CircleMap * G & yt in CircleMap " {y0} & ( for F1 being Homotopy of ft,Qt st F = CircleMap * F1 holds G = F1 ) ) thus A49: ft,Qt are_homotopic by A34, A48, BORSUK_2:def_7; ::_thesis: ( F = CircleMap * G & yt in CircleMap " {y0} & ( for F1 being Homotopy of ft,Qt st F = CircleMap * F1 holds G = F1 ) ) thus F = CircleMap * G by A35; ::_thesis: ( yt in CircleMap " {y0} & ( for F1 being Homotopy of ft,Qt st F = CircleMap * F1 holds G = F1 ) ) thus yt in CircleMap " {y0} by A41, FUNCT_2:38; ::_thesis: for F1 being Homotopy of ft,Qt st F = CircleMap * F1 holds G = F1 let F1 be Homotopy of ft,Qt; ::_thesis: ( F = CircleMap * F1 implies G = F1 ) assume A50: F = CircleMap * F1 ; ::_thesis: G = F1 A51: dom F1 = the carrier of [:I[01],I[01]:] by FUNCT_2:def_1; then A52: dom (F1 | [: the carrier of I[01],{0}:]) = [: the carrier of I[01],{0}:] by A32, A33, RELAT_1:62; for x being set st x in dom (F1 | [: the carrier of I[01],{0}:]) holds (F1 | [: the carrier of I[01],{0}:]) . x = Ft . x proof let x be set ; ::_thesis: ( x in dom (F1 | [: the carrier of I[01],{0}:]) implies (F1 | [: the carrier of I[01],{0}:]) . x = Ft . x ) assume A53: x in dom (F1 | [: the carrier of I[01],{0}:]) ; ::_thesis: (F1 | [: the carrier of I[01],{0}:]) . x = Ft . x then consider x1, x2 being set such that A54: x1 in the carrier of I[01] 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 | [: the carrier of I[01],{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 ; ::_thesis: verum end; then F1 | [: the carrier of I[01],{0}:] = Ft by A32, A33, A14, A51, FUNCT_1:2, RELAT_1:62; hence G = F1 by A37, A50; ::_thesis: verum end; definition func Ciso -> Function of INT.Group,(pi_1 ((Tunit_circle 2),c[10])) means :Def5: :: TOPALG_5:def 5 for n being Integer holds it . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n)); existence ex b1 being Function of INT.Group,(pi_1 ((Tunit_circle 2),c[10])) st for n being Integer holds b1 . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n)) proof defpred S1[ Integer, set ] means $2 = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop $1)); A1: for x being Element of INT ex y being Element of (pi_1 ((Tunit_circle 2),c[10])) st S1[x,y] proof let x be Element of INT ; ::_thesis: ex y being Element of (pi_1 ((Tunit_circle 2),c[10])) st S1[x,y] reconsider y = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop x)) as Element of (pi_1 ((Tunit_circle 2),c[10])) by TOPALG_1:47; take y ; ::_thesis: S1[x,y] thus S1[x,y] ; ::_thesis: verum end; consider f being Function of INT, the carrier of (pi_1 ((Tunit_circle 2),c[10])) such that A2: for x being Element of INT holds S1[x,f . x] from FUNCT_2:sch_3(A1); reconsider f = f as Function of INT.Group,(pi_1 ((Tunit_circle 2),c[10])) ; take f ; ::_thesis: for n being Integer holds f . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n)) let n be Integer; ::_thesis: f . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n)) n in INT by INT_1:def_2; hence f . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n)) by A2; ::_thesis: verum end; uniqueness for b1, b2 being Function of INT.Group,(pi_1 ((Tunit_circle 2),c[10])) st ( for n being Integer holds b1 . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n)) ) & ( for n being Integer holds b2 . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n)) ) holds b1 = b2 proof let f, g be Function of INT.Group,(pi_1 ((Tunit_circle 2),c[10])); ::_thesis: ( ( for n being Integer holds f . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n)) ) & ( for n being Integer holds g . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n)) ) implies f = g ) assume that A3: for n being Integer holds f . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n)) and A4: for n being Integer holds g . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n)) ; ::_thesis: f = g for x being Element of INT.Group holds f . x = g . x proof let x be Element of INT.Group; ::_thesis: f . x = g . x thus f . x = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop x)) by A3 .= g . x by A4 ; ::_thesis: verum end; hence f = g by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def5 defines Ciso TOPALG_5:def_5_:_ for b1 being Function of INT.Group,(pi_1 ((Tunit_circle 2),c[10])) holds ( b1 = Ciso iff for n being Integer holds b1 . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n)) ); theorem Th25: :: TOPALG_5:25 for i being Integer for 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; ::_thesis: for f being Path of R^1 0, R^1 i holds Ciso . i = Class ((EqRel ((Tunit_circle 2),c[10])),(CircleMap * f)) let f be Path of R^1 0, R^1 i; ::_thesis: Ciso . i = Class ((EqRel ((Tunit_circle 2),c[10])),(CircleMap * f)) set P = CircleMap * f; A1: (CircleMap * f) . 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 ; (CircleMap * f) . 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 = CircleMap * f 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; :: according to BORSUK_2:def_7 ::_thesis: ( F is continuous & ( for b1 being Element of the carrier of I[01] holds ( F . (b1,0) = (cLoop i) . b1 & F . (b1,1) = P . b1 & F . (0,b1) = c[10] & F . (1,b1) = c[10] ) ) ) thus F is continuous ; ::_thesis: for b1 being Element of the carrier of I[01] holds ( F . (b1,0) = (cLoop i) . b1 & F . (b1,1) = P . b1 & F . (0,b1) = c[10] & F . (1,b1) = c[10] ) let s be Point of I[01]; ::_thesis: ( F . (s,0) = (cLoop i) . s & F . (s,1) = P . s & F . (0,s) = c[10] & F . (1,s) = c[10] ) 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 ; ::_thesis: ( F . (s,1) = P . s & F . (0,s) = c[10] & F . (1,s) = c[10] ) 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 ; ::_thesis: ( F . (0,s) = c[10] & F . (1,s) = c[10] ) 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 ; ::_thesis: F . (1,s) = c[10] 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 ; ::_thesis: verum end; thus Ciso . i = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop i)) by Def5 .= Class ((EqRel ((Tunit_circle 2),c[10])),(CircleMap * f)) by A3, TOPALG_1:46 ; ::_thesis: verum end; registration cluster Ciso -> multiplicative ; coherence Ciso is multiplicative proof set f = Ciso ; let x, y be Element of INT.Group; :: according to GROUP_6:def_6 ::_thesis: Ciso . (x * y) = (Ciso . x) * (Ciso . y) consider fX, fY being Loop of c[10] such that A1: Ciso . x = Class ((EqRel ((Tunit_circle 2),c[10])),fX) and A2: Ciso . y = Class ((EqRel ((Tunit_circle 2),c[10])),fY) and A3: the multF of (pi_1 ((Tunit_circle 2),c[10])) . ((Ciso . x),(Ciso . y)) = Class ((EqRel ((Tunit_circle 2),c[10])),(fX + fY)) by TOPALG_1:def_5; Ciso . y = Class ((EqRel ((Tunit_circle 2),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: (tx * (ExtendInt y)) . 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: (tx * (ExtendInt y)) . 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 ; x is Real by XREAL_0:def_1; then tx is being_homeomorphism by JORDAN16:20; then tx is continuous by TOPS_2:def_5; then reconsider p = tx * (ExtendInt y) 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]; ::_thesis: (CircleMap * ((ExtendInt x) + p)) . a = ((cLoop x) + (cLoop y)) . a percases ( a <= 1 / 2 or 1 / 2 <= a ) ; supposeA8: a <= 1 / 2 ; ::_thesis: (CircleMap * ((ExtendInt x) + p)) . a = ((cLoop x) + (cLoop y)) . a 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 ; ::_thesis: verum end; supposeA10: 1 / 2 <= a ; ::_thesis: (CircleMap * ((ExtendInt x) + p)) . a = ((cLoop x) + (cLoop y)) . 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 ; ::_thesis: verum end; end; end; Ciso . x = Class ((EqRel ((Tunit_circle 2),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 Ciso . (x * y) = Class ((EqRel ((Tunit_circle 2),c[10])),(CircleMap * ((ExtendInt x) + p))) by Th25 .= Class ((EqRel ((Tunit_circle 2),c[10])),((cLoop x) + (cLoop y))) by A7, FUNCT_2:63 .= (Ciso . x) * (Ciso . y) by A3, A12, TOPALG_1:46 ; ::_thesis: verum end; end; registration cluster Ciso -> one-to-one onto ; coherence ( Ciso is one-to-one & Ciso is onto ) proof thus Ciso is one-to-one ::_thesis: Ciso is onto proof set xt = R^1 0; let m, n be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not m in dom Ciso or not n in dom Ciso or not Ciso . m = Ciso . n or m = n ) assume that A1: ( m in dom Ciso & n in dom Ciso ) and A2: Ciso . m = Ciso . n ; ::_thesis: m = n reconsider m = m, n = n as Integer by A1; ( Ciso . m = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop m)) & Ciso . n = Class ((EqRel ((Tunit_circle 2),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]:],(Tunit_circle 2) 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] ) ) ) by BORSUK_2:def_7; A6: R^1 0 in CircleMap " {c[10]} by Lm1, TOPREALB:33, TOPREALB:def_2; then consider ftm being Function of I[01],R^1 such that ftm . 0 = R^1 0 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 = R^1 0 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 R^1 0,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__::_thesis:_for_x_being_Point_of_I[01]_holds_(CircleMap_*_(Prj1_(j0,Ft)))_._x_=_(cLoop_m)_._x let x be Point of I[01]; ::_thesis: (CircleMap * (Prj1 (j0,Ft))) . x = (cLoop m) . x thus (CircleMap * (Prj1 (j0,Ft))) . x = CircleMap . ((Prj1 (j0,Ft)) . 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 ; ::_thesis: verum end; (Prj1 (j0,Ft)) . 0 = Ft . (j0,j0) by Def2 .= R^1 0 by A8, BORSUK_6:def_11 ; then A12: Prj1 (j0,Ft) = ftm by A7, A11, FUNCT_2:63; set ft1 = Prj1 (j1,Ft); A13: now__::_thesis:_for_x_being_Point_of_I[01]_holds_(CircleMap_*_(Prj1_(j1,Ft)))_._x_=_(cLoop_n)_._x let x be Point of I[01]; ::_thesis: (CircleMap * (Prj1 (j1,Ft))) . x = (cLoop n) . x thus (CircleMap * (Prj1 (j1,Ft))) . x = CircleMap . ((Prj1 (j1,Ft)) . 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 ; ::_thesis: verum end; consider ftn being Function of I[01],R^1 such that ftn . 0 = R^1 0 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 = R^1 0 holds ftn = f1 by A6, Th23; A15: cLoop m = CircleMap * (ExtendInt m) by Th20; (Prj1 (j1,Ft)) . 0 = Ft . (j0,j1) by Def2 .= R^1 0 by A8, BORSUK_6:def_11 ; then A16: Prj1 (j1,Ft) = ftn by A14, A13, FUNCT_2:63; (ExtendInt n) . 0 = n * j0 by Def1 .= R^1 0 by TOPREALB:def_2 ; then ExtendInt n = ftn by A14, A10; then A17: (Prj1 (j1,Ft)) . j1 = n * 1 by A16, Def1; (ExtendInt m) . 0 = m * j0 by Def1 .= R^1 0 by TOPREALB:def_2 ; then ExtendInt m = ftm by A7, A15; then A18: (Prj1 (j0,Ft)) . j1 = m * 1 by A12, Def1; (Prj1 (j0,Ft)) . j1 = Ft . (j1,j0) by Def2 .= yt by A8, BORSUK_6:def_11 .= Ft . (j1,j1) by A8, BORSUK_6:def_11 .= (Prj1 (j1,Ft)) . j1 by Def2 ; hence m = n by A18, A17; ::_thesis: verum end; thus rng Ciso c= the carrier of (pi_1 ((Tunit_circle 2),c[10])) ; :: according to FUNCT_2:def_3,XBOOLE_0:def_10 ::_thesis: the carrier of (pi_1 ((Tunit_circle 2),c[10])) c= rng Ciso let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in the carrier of (pi_1 ((Tunit_circle 2),c[10])) or q in rng Ciso ) assume q in the carrier of (pi_1 ((Tunit_circle 2),c[10])) ; ::_thesis: q in rng Ciso then consider f being Loop of c[10] such that A19: q = Class ((EqRel ((Tunit_circle 2),c[10])),f) by TOPALG_1:47; R^1 0 in CircleMap " {c[10]} by Lm1, TOPREALB:33, TOPREALB: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; 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 A23: ft . 1 in INT by Lm12, FUNCT_1:def_7, TOPREALB:33; 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 ((Tunit_circle 2),c[10])),(CircleMap * ft)) ) by A23, Th25, FUNCT_2:def_1; hence q in rng Ciso by A19, A21, A23, FUNCT_1:def_3; ::_thesis: verum end; end; theorem :: TOPALG_5:26 Ciso is bijective ; Lm16: for r being positive real number for o being Point of (TOP-REAL 2) for x being Point of (Tcircle (o,r)) holds INT.Group , pi_1 ((Tcircle (o,r)),x) are_isomorphic proof let r be positive real number ; ::_thesis: for o being Point of (TOP-REAL 2) for x being Point of (Tcircle (o,r)) holds INT.Group , pi_1 ((Tcircle (o,r)),x) are_isomorphic let o be Point of (TOP-REAL 2); ::_thesis: for x being Point of (Tcircle (o,r)) holds INT.Group , pi_1 ((Tcircle (o,r)),x) are_isomorphic let x be Point of (Tcircle (o,r)); ::_thesis: INT.Group , pi_1 ((Tcircle (o,r)),x) are_isomorphic Tunit_circle 2 = Tcircle ((0. (TOP-REAL 2)),1) by TOPREALB:def_7; then pi_1 ((Tunit_circle 2),c[10]), pi_1 ((Tcircle (o,r)),x) are_isomorphic by TOPALG_3:33, TOPREALB:20; then consider h being Homomorphism of (pi_1 ((Tunit_circle 2),c[10])),(pi_1 ((Tcircle (o,r)),x)) such that A1: h is bijective by GROUP_6:def_11; take h * Ciso ; :: according to GROUP_6:def_11 ::_thesis: h * Ciso is bijective thus h * Ciso is bijective by A1, GROUP_6:64; ::_thesis: verum end; theorem Th27: :: TOPALG_5:27 for S being being_simple_closed_curve SubSpace of TOP-REAL 2 for x being Point of S holds INT.Group , pi_1 (S,x) are_isomorphic proof set r = the positive real number ; set o = the Point of (TOP-REAL 2); set y = the Point of (Tcircle ( the Point of (TOP-REAL 2), the positive real number )); let S be being_simple_closed_curve SubSpace of TOP-REAL 2; ::_thesis: for x being Point of S holds INT.Group , pi_1 (S,x) are_isomorphic let x be Point of S; ::_thesis: INT.Group , pi_1 (S,x) are_isomorphic ( INT.Group , pi_1 ((Tcircle ( the Point of (TOP-REAL 2), the positive real number )), the Point of (Tcircle ( the Point of (TOP-REAL 2), the positive real number ))) are_isomorphic & pi_1 ((Tcircle ( the Point of (TOP-REAL 2), the positive real number )), the Point of (Tcircle ( the Point of (TOP-REAL 2), the positive real number ))), pi_1 (S,x) are_isomorphic ) by Lm16, TOPALG_3:33, TOPREALB:11; hence INT.Group , pi_1 (S,x) are_isomorphic by GROUP_6:67; ::_thesis: verum end; registration let S be being_simple_closed_curve SubSpace of TOP-REAL 2; let x be Point of S; cluster FundamentalGroup (S,x) -> infinite ; coherence not pi_1 (S,x) is finite proof INT.Group , pi_1 (S,x) are_isomorphic by Th27; hence not pi_1 (S,x) is finite by GROUP_6:74; ::_thesis: verum end; end;