:: BORSUK_2 semantic presentation begin Lm1: for r being real number holds ( ( 0 <= r & r <= 1 ) iff r in the carrier of I[01] ) proof let r be real number ; ::_thesis: ( ( 0 <= r & r <= 1 ) iff r in the carrier of I[01] ) A1: [.0,1.] = { r1 where r1 is Real : ( 0 <= r1 & r1 <= 1 ) } by RCOMP_1:def_1; r is Real by XREAL_0:def_1; hence ( 0 <= r & r <= 1 implies r in the carrier of I[01] ) by A1, BORSUK_1:40; ::_thesis: ( r in the carrier of I[01] implies ( 0 <= r & r <= 1 ) ) assume r in the carrier of I[01] ; ::_thesis: ( 0 <= r & r <= 1 ) then ex r2 being Real st ( r2 = r & 0 <= r2 & r2 <= 1 ) by A1, BORSUK_1:40; hence ( 0 <= r & r <= 1 ) ; ::_thesis: verum end; scheme :: BORSUK_2:sch 1 FrCard{ F1() -> non empty set , F2() -> set , F3( set ) -> set , P1[ set ] } : card { F3(w) where w is Element of F1() : ( w in F2() & P1[w] ) } c= card F2() proof consider f being Function such that A1: ( dom f = F2() & ( for x being set st x in F2() holds f . x = F3(x) ) ) from FUNCT_1:sch_3(); { F3(w) where w is Element of F1() : ( w in F2() & P1[w] ) } c= rng f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { F3(w) where w is Element of F1() : ( w in F2() & P1[w] ) } or x in rng f ) assume x in { F3(w) where w is Element of F1() : ( w in F2() & P1[w] ) } ; ::_thesis: x in rng f then consider w being Element of F1() such that A2: x = F3(w) and A3: w in F2() and P1[w] ; f . w = x by A1, A2, A3; hence x in rng f by A1, A3, FUNCT_1:def_3; ::_thesis: verum end; hence card { F3(w) where w is Element of F1() : ( w in F2() & P1[w] ) } c= card F2() by A1, CARD_1:12; ::_thesis: verum end; theorem :: BORSUK_2:1 for T1, S, T2, T being non empty TopSpace for f being Function of T1,S for g being Function of T2,S st T1 is SubSpace of T & T2 is SubSpace of T & ([#] T1) \/ ([#] T2) = [#] T & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & ( for p being set st p in ([#] T1) /\ ([#] T2) holds f . p = g . p ) holds ex h being Function of T,S st ( h = f +* g & h is continuous ) proof let T1, S, T2, T be non empty TopSpace; ::_thesis: for f being Function of T1,S for g being Function of T2,S st T1 is SubSpace of T & T2 is SubSpace of T & ([#] T1) \/ ([#] T2) = [#] T & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & ( for p being set st p in ([#] T1) /\ ([#] T2) holds f . p = g . p ) holds ex h being Function of T,S st ( h = f +* g & h is continuous ) let f be Function of T1,S; ::_thesis: for g being Function of T2,S st T1 is SubSpace of T & T2 is SubSpace of T & ([#] T1) \/ ([#] T2) = [#] T & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & ( for p being set st p in ([#] T1) /\ ([#] T2) holds f . p = g . p ) holds ex h being Function of T,S st ( h = f +* g & h is continuous ) let g be Function of T2,S; ::_thesis: ( T1 is SubSpace of T & T2 is SubSpace of T & ([#] T1) \/ ([#] T2) = [#] T & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & ( for p being set st p in ([#] T1) /\ ([#] T2) holds f . p = g . p ) implies ex h being Function of T,S st ( h = f +* g & h is continuous ) ) assume that A1: T1 is SubSpace of T and A2: T2 is SubSpace of T and A3: ([#] T1) \/ ([#] T2) = [#] T and A4: T1 is compact and A5: T2 is compact and A6: T is T_2 and A7: f is continuous and A8: g is continuous and A9: for p being set st p in ([#] T1) /\ ([#] T2) holds f . p = g . p ; ::_thesis: ex h being Function of T,S st ( h = f +* g & h is continuous ) set h = f +* g; A10: dom g = [#] T2 by FUNCT_2:def_1; A11: dom f = [#] T1 by FUNCT_2:def_1; then A12: dom (f +* g) = the carrier of T by A3, A10, FUNCT_4:def_1; rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17; then reconsider h = f +* g as Function of T,S by A12, FUNCT_2:2, XBOOLE_1:1; take h ; ::_thesis: ( h = f +* g & h is continuous ) thus h = f +* g ; ::_thesis: h is continuous for P being Subset of S st P is closed holds h " P is closed proof let P be Subset of S; ::_thesis: ( P is closed implies h " P is closed ) reconsider P3 = f " P as Subset of T1 ; reconsider P4 = g " P as Subset of T2 ; [#] T1 c= [#] T by A3, XBOOLE_1:7; then reconsider P1 = f " P as Subset of T by XBOOLE_1:1; [#] T2 c= [#] T by A3, XBOOLE_1:7; then reconsider P2 = g " P as Subset of T by XBOOLE_1:1; A13: dom h = (dom f) \/ (dom g) by FUNCT_4:def_1; A14: now__::_thesis:_for_x_being_set_holds_ (_(_x_in_(h_"_P)_/\_([#]_T2)_implies_x_in_g_"_P_)_&_(_x_in_g_"_P_implies_x_in_(h_"_P)_/\_([#]_T2)_)_) let x be set ; ::_thesis: ( ( x in (h " P) /\ ([#] T2) implies x in g " P ) & ( x in g " P implies x in (h " P) /\ ([#] T2) ) ) thus ( x in (h " P) /\ ([#] T2) implies x in g " P ) ::_thesis: ( x in g " P implies x in (h " P) /\ ([#] T2) ) proof assume A15: x in (h " P) /\ ([#] T2) ; ::_thesis: x in g " P then x in h " P by XBOOLE_0:def_4; then A16: h . x in P by FUNCT_1:def_7; g . x = h . x by A10, A15, FUNCT_4:13; hence x in g " P by A10, A15, A16, FUNCT_1:def_7; ::_thesis: verum end; assume A17: x in g " P ; ::_thesis: x in (h " P) /\ ([#] T2) then A18: x in dom g by FUNCT_1:def_7; g . x in P by A17, FUNCT_1:def_7; then A19: h . x in P by A18, FUNCT_4:13; x in dom h by A13, A18, XBOOLE_0:def_3; then x in h " P by A19, FUNCT_1:def_7; hence x in (h " P) /\ ([#] T2) by A17, XBOOLE_0:def_4; ::_thesis: verum end; A20: for x being set st x in [#] T1 holds h . x = f . x proof let x be set ; ::_thesis: ( x in [#] T1 implies h . x = f . x ) assume A21: x in [#] T1 ; ::_thesis: h . x = f . x now__::_thesis:_h_._x_=_f_._x percases ( x in [#] T2 or not x in [#] T2 ) ; supposeA22: x in [#] T2 ; ::_thesis: h . x = f . x then x in ([#] T1) /\ ([#] T2) by A21, XBOOLE_0:def_4; then f . x = g . x by A9; hence h . x = f . x by A10, A22, FUNCT_4:13; ::_thesis: verum end; suppose not x in [#] T2 ; ::_thesis: h . x = f . x hence h . x = f . x by A10, FUNCT_4:11; ::_thesis: verum end; end; end; hence h . x = f . x ; ::_thesis: verum end; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_(h_"_P)_/\_([#]_T1)_implies_x_in_f_"_P_)_&_(_x_in_f_"_P_implies_x_in_(h_"_P)_/\_([#]_T1)_)_) let x be set ; ::_thesis: ( ( x in (h " P) /\ ([#] T1) implies x in f " P ) & ( x in f " P implies x in (h " P) /\ ([#] T1) ) ) thus ( x in (h " P) /\ ([#] T1) implies x in f " P ) ::_thesis: ( x in f " P implies x in (h " P) /\ ([#] T1) ) proof assume A23: x in (h " P) /\ ([#] T1) ; ::_thesis: x in f " P then x in h " P by XBOOLE_0:def_4; then A24: h . x in P by FUNCT_1:def_7; f . x = h . x by A20, A23; hence x in f " P by A11, A23, A24, FUNCT_1:def_7; ::_thesis: verum end; assume A25: x in f " P ; ::_thesis: x in (h " P) /\ ([#] T1) then x in dom f by FUNCT_1:def_7; then A26: x in dom h by A13, XBOOLE_0:def_3; f . x in P by A25, FUNCT_1:def_7; then h . x in P by A20, A25; then x in h " P by A26, FUNCT_1:def_7; hence x in (h " P) /\ ([#] T1) by A25, XBOOLE_0:def_4; ::_thesis: verum end; then A27: (h " P) /\ ([#] T1) = f " P by TARSKI:1; assume A28: P is closed ; ::_thesis: h " P is closed then P3 is closed by A7, PRE_TOPC:def_6; then P3 is compact by A4, COMPTS_1:8; then A29: P1 is compact by A1, COMPTS_1:19; P4 is closed by A8, A28, PRE_TOPC:def_6; then P4 is compact by A5, COMPTS_1:8; then A30: P2 is compact by A2, COMPTS_1:19; h " P = (h " P) /\ (([#] T1) \/ ([#] T2)) by A11, A10, A13, RELAT_1:132, XBOOLE_1:28 .= ((h " P) /\ ([#] T1)) \/ ((h " P) /\ ([#] T2)) by XBOOLE_1:23 ; then h " P = (f " P) \/ (g " P) by A27, A14, TARSKI:1; hence h " P is closed by A6, A29, A30; ::_thesis: verum end; hence h is continuous by PRE_TOPC:def_6; ::_thesis: verum end; registration let T be TopStruct ; cluster id T -> continuous open ; coherence ( id T is open & id T is continuous ) proof thus id T is open ::_thesis: id T is continuous proof let A be Subset of T; :: according to T_0TOPSP:def_2 ::_thesis: ( not A is open or (id T) .: A is open ) assume A is open ; ::_thesis: (id T) .: A is open hence (id T) .: A is open by FUNCT_1:92; ::_thesis: verum end; let V be Subset of T; :: according to PRE_TOPC:def_6 ::_thesis: ( not V is closed or (id T) " V is closed ) assume V is closed ; ::_thesis: (id T) " V is closed hence (id T) " V is closed by FUNCT_2:94; ::_thesis: verum end; end; registration let T be TopStruct ; cluster Relation-like the carrier of T -defined the carrier of T -valued Function-like one-to-one V17( the carrier of T) V21( the carrier of T, the carrier of T) continuous for Element of bool [: the carrier of T, the carrier of T:]; existence ex b1 being Function of T,T st ( b1 is continuous & b1 is one-to-one ) proof take id T ; ::_thesis: ( id T is continuous & id T is one-to-one ) thus ( id T is continuous & id T is one-to-one ) ; ::_thesis: verum end; end; theorem :: BORSUK_2:2 for S, T being non empty TopSpace for f being Function of S,T st f is being_homeomorphism holds f " is open proof let S, T be non empty TopSpace; ::_thesis: for f being Function of S,T st f is being_homeomorphism holds f " is open let f be Function of S,T; ::_thesis: ( f is being_homeomorphism implies f " is open ) assume f is being_homeomorphism ; ::_thesis: f " is open then A1: ( rng f = [#] T & f is one-to-one & f is continuous ) by TOPS_2:def_5; let P be Subset of T; :: according to T_0TOPSP:def_2 ::_thesis: ( not P is open or (f ") .: P is open ) f " P = (f ") .: P by A1, TOPS_2:55; hence ( not P is open or (f ") .: P is open ) by A1, TOPS_2:43; ::_thesis: verum end; begin theorem Th3: :: BORSUK_2:3 for T being non empty TopSpace for a being Point of T ex f being Function of I[01],T st ( f is continuous & f . 0 = a & f . 1 = a ) proof let T be non empty TopSpace; ::_thesis: for a being Point of T ex f being Function of I[01],T st ( f is continuous & f . 0 = a & f . 1 = a ) let a be Point of T; ::_thesis: ex f being Function of I[01],T st ( f is continuous & f . 0 = a & f . 1 = a ) take I[01] --> a ; ::_thesis: ( I[01] --> a is continuous & (I[01] --> a) . 0 = a & (I[01] --> a) . 1 = a ) thus ( I[01] --> a is continuous & (I[01] --> a) . 0 = a & (I[01] --> a) . 1 = a ) by BORSUK_1:def_14, BORSUK_1:def_15, FUNCOP_1:7; ::_thesis: verum end; definition let T be TopStruct ; let a, b be Point of T; preda,b are_connected means :Def1: :: BORSUK_2:def 1 ex f being Function of I[01],T st ( f is continuous & f . 0 = a & f . 1 = b ); end; :: deftheorem Def1 defines are_connected BORSUK_2:def_1_:_ for T being TopStruct for a, b being Point of T holds ( a,b are_connected iff ex f being Function of I[01],T st ( f is continuous & f . 0 = a & f . 1 = b ) ); definition let T be non empty TopSpace; let a, b be Point of T; :: original: are_connected redefine preda,b are_connected ; reflexivity for a being Point of T holds (T,b1,b1) proof let a be Point of T; ::_thesis: (T,a,a) thus ex f being Function of I[01],T st ( f is continuous & f . 0 = a & f . 1 = a ) by Th3; :: according to BORSUK_2:def_1 ::_thesis: verum end; end; definition let T be TopStruct ; let a, b be Point of T; assume A1: a,b are_connected ; mode Path of a,b -> Function of I[01],T means :Def2: :: BORSUK_2:def 2 ( it is continuous & it . 0 = a & it . 1 = b ); existence ex b1 being Function of I[01],T st ( b1 is continuous & b1 . 0 = a & b1 . 1 = b ) by A1, Def1; end; :: deftheorem Def2 defines Path BORSUK_2:def_2_:_ for T being TopStruct for a, b being Point of T st a,b are_connected holds for b4 being Function of I[01],T holds ( b4 is Path of a,b iff ( b4 is continuous & b4 . 0 = a & b4 . 1 = b ) ); registration let T be non empty TopSpace; let a be Point of T; cluster non empty Relation-like the carrier of I[01] -defined the carrier of T -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of T) continuous for Path of a,a; existence ex b1 being Path of a,a st b1 is continuous proof set IT = I[01] --> a; A1: a,a are_connected ; ( (I[01] --> a) . 0 = a & (I[01] --> a) . 1 = a ) by BORSUK_1:def_14, BORSUK_1:def_15, FUNCOP_1:7; then I[01] --> a is Path of a,a by A1, Def2; hence ex b1 being Path of a,a st b1 is continuous ; ::_thesis: verum end; end; definition let T be TopStruct ; attrT is pathwise_connected means :Def3: :: BORSUK_2:def 3 for a, b being Point of T holds a,b are_connected ; correctness ; end; :: deftheorem Def3 defines pathwise_connected BORSUK_2:def_3_:_ for T being TopStruct holds ( T is pathwise_connected iff for a, b being Point of T holds a,b are_connected ); registration cluster non empty strict TopSpace-like pathwise_connected for TopStruct ; existence ex b1 being TopSpace st ( b1 is strict & b1 is pathwise_connected & not b1 is empty ) proof set T = I[01] | {0[01]}; 0[01] in {0[01]} by TARSKI:def_1; then reconsider nl = 0[01] as Point of (I[01] | {0[01]}) by PRE_TOPC:8; A1: the carrier of (I[01] | {0[01]}) = {0[01]} by PRE_TOPC:8; for a, b being Point of (I[01] | {0[01]}) holds a,b are_connected proof reconsider f = I[01] --> nl as Function of I[01],(I[01] | {0[01]}) ; let a, b be Point of (I[01] | {0[01]}); ::_thesis: a,b are_connected take f ; :: according to BORSUK_2:def_1 ::_thesis: ( f is continuous & f . 0 = a & f . 1 = b ) thus f is continuous ; ::_thesis: ( f . 0 = a & f . 1 = b ) ( a = nl & b = nl ) by A1, TARSKI:def_1; hence ( f . 0 = a & f . 1 = b ) by BORSUK_1:def_15, FUNCOP_1:7; ::_thesis: verum end; then I[01] | {0[01]} is pathwise_connected by Def3; hence ex b1 being TopSpace st ( b1 is strict & b1 is pathwise_connected & not b1 is empty ) ; ::_thesis: verum end; end; definition let T be pathwise_connected TopStruct ; let a, b be Point of T; redefine mode Path of a,b means :Def4: :: BORSUK_2:def 4 ( it is continuous & it . 0 = a & it . 1 = b ); compatibility for b1 being Function of I[01],T holds ( b1 is Path of a,b iff ( b1 is continuous & b1 . 0 = a & b1 . 1 = b ) ) proof a,b are_connected by Def3; hence for b1 being Function of I[01],T holds ( b1 is Path of a,b iff ( b1 is continuous & b1 . 0 = a & b1 . 1 = b ) ) by Def2; ::_thesis: verum end; end; :: deftheorem Def4 defines Path BORSUK_2:def_4_:_ for T being pathwise_connected TopStruct for a, b being Point of T for b4 being Function of I[01],T holds ( b4 is Path of a,b iff ( b4 is continuous & b4 . 0 = a & b4 . 1 = b ) ); registration let T be pathwise_connected TopStruct ; let a, b be Point of T; cluster -> continuous for Path of a,b; coherence for b1 being Path of a,b holds b1 is continuous by Def4; end; Lm2: ( 0 in [.0,1.] & 1 in [.0,1.] ) by XXREAL_1:1; registration cluster non empty TopSpace-like pathwise_connected -> non empty connected for TopStruct ; coherence for b1 being non empty TopSpace st b1 is pathwise_connected holds b1 is connected proof let GX be non empty TopSpace; ::_thesis: ( GX is pathwise_connected implies GX is connected ) assume A1: for x, y being Point of GX holds x,y are_connected ; :: according to BORSUK_2:def_3 ::_thesis: GX is connected for x, y being Point of GX ex GY being non empty TopSpace st ( GY is connected & ex f being Function of GY,GX st ( f is continuous & x in rng f & y in rng f ) ) proof let x, y be Point of GX; ::_thesis: ex GY being non empty TopSpace st ( GY is connected & ex f being Function of GY,GX st ( f is continuous & x in rng f & y in rng f ) ) x,y are_connected by A1; then consider h being Function of I[01],GX such that A2: h is continuous and A3: x = h . 0 and A4: y = h . 1 by Def1; 1 in dom h by Lm2, BORSUK_1:40, FUNCT_2:def_1; then A5: y in rng h by A4, FUNCT_1:def_3; 0 in dom h by Lm2, BORSUK_1:40, FUNCT_2:def_1; then x in rng h by A3, FUNCT_1:def_3; hence ex GY being non empty TopSpace st ( GY is connected & ex f being Function of GY,GX st ( f is continuous & x in rng f & y in rng f ) ) by A2, A5, TREAL_1:19; ::_thesis: verum end; hence GX is connected by TOPS_2:63; ::_thesis: verum end; end; begin Lm3: for G being non empty TopSpace for w1, w2, w3 being Point of G for h1, h2 being Function of I[01],G st h1 is continuous & w1 = h1 . 0 & w2 = h1 . 1 & h2 is continuous & w2 = h2 . 0 & w3 = h2 . 1 holds ex h3 being Function of I[01],G st ( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 & rng h3 c= (rng h1) \/ (rng h2) ) proof let G be non empty TopSpace; ::_thesis: for w1, w2, w3 being Point of G for h1, h2 being Function of I[01],G st h1 is continuous & w1 = h1 . 0 & w2 = h1 . 1 & h2 is continuous & w2 = h2 . 0 & w3 = h2 . 1 holds ex h3 being Function of I[01],G st ( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 & rng h3 c= (rng h1) \/ (rng h2) ) let w1, w2, w3 be Point of G; ::_thesis: for h1, h2 being Function of I[01],G st h1 is continuous & w1 = h1 . 0 & w2 = h1 . 1 & h2 is continuous & w2 = h2 . 0 & w3 = h2 . 1 holds ex h3 being Function of I[01],G st ( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 & rng h3 c= (rng h1) \/ (rng h2) ) let h1, h2 be Function of I[01],G; ::_thesis: ( h1 is continuous & w1 = h1 . 0 & w2 = h1 . 1 & h2 is continuous & w2 = h2 . 0 & w3 = h2 . 1 implies ex h3 being Function of I[01],G st ( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 & rng h3 c= (rng h1) \/ (rng h2) ) ) assume that A1: h1 is continuous and A2: w1 = h1 . 0 and A3: w2 = h1 . 1 and A4: h2 is continuous and A5: w2 = h2 . 0 and A6: w3 = h2 . 1 ; ::_thesis: ex h3 being Function of I[01],G st ( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 & rng h3 c= (rng h1) \/ (rng h2) ) w2,w3 are_connected by A4, A5, A6, Def1; then reconsider g2 = h2 as Path of w2,w3 by A4, A5, A6, Def2; w1,w2 are_connected by A1, A2, A3, Def1; then reconsider g1 = h1 as Path of w1,w2 by A1, A2, A3, Def2; set P1 = g1; set P2 = g2; set p1 = w1; set p3 = w3; ex P0 being Path of w1,w3 st ( P0 is continuous & P0 . 0 = w1 & P0 . 1 = w3 & ( for t being Point of I[01] for t9 being Real st t = t9 holds ( ( 0 <= t9 & t9 <= 1 / 2 implies P0 . t = g1 . (2 * t9) ) & ( 1 / 2 <= t9 & t9 <= 1 implies P0 . t = g2 . ((2 * t9) - 1) ) ) ) ) proof 1 / 2 in { r where r is Real : ( 0 <= r & r <= 1 ) } ; then reconsider pol = 1 / 2 as Point of I[01] by BORSUK_1:40, RCOMP_1:def_1; reconsider T1 = Closed-Interval-TSpace (0,(1 / 2)), T2 = Closed-Interval-TSpace ((1 / 2),1) as SubSpace of I[01] by TOPMETR:20, TREAL_1:3; set e2 = P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))); set e1 = P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))); set E1 = g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))); set E2 = g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))); set f = (g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))); A7: dom (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) = the carrier of (Closed-Interval-TSpace (0,(1 / 2))) by FUNCT_2:def_1 .= [.0,(1 / 2).] by TOPMETR:18 ; A8: dom (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) = the carrier of (Closed-Interval-TSpace ((1 / 2),1)) by FUNCT_2:def_1 .= [.(1 / 2),1.] by TOPMETR:18 ; reconsider gg = g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) as Function of T2,G by TOPMETR:20; reconsider ff = g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) as Function of T1,G by TOPMETR:20; A9: for t9 being Real st 1 / 2 <= t9 & t9 <= 1 holds (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t9 = g2 . ((2 * t9) - 1) proof reconsider r1 = (#) (0,1), r2 = (0,1) (#) as Real by TREAL_1:5; dom (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) = the carrier of (Closed-Interval-TSpace ((1 / 2),1)) by FUNCT_2:def_1; then A10: dom (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) = [.(1 / 2),1.] by TOPMETR:18 .= { r where r is Real : ( 1 / 2 <= r & r <= 1 ) } by RCOMP_1:def_1 ; let t9 be Real; ::_thesis: ( 1 / 2 <= t9 & t9 <= 1 implies (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t9 = g2 . ((2 * t9) - 1) ) assume ( 1 / 2 <= t9 & t9 <= 1 ) ; ::_thesis: (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t9 = g2 . ((2 * t9) - 1) then A11: t9 in dom (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) by A10; then reconsider s = t9 as Point of (Closed-Interval-TSpace ((1 / 2),1)) ; (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) . s = (((r2 - r1) / (1 - (1 / 2))) * t9) + (((1 * r1) - ((1 / 2) * r2)) / (1 - (1 / 2))) by TREAL_1:11 .= (2 * t9) - 1 by TREAL_1:5 ; hence (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t9 = g2 . ((2 * t9) - 1) by A11, FUNCT_1:13; ::_thesis: verum end; A12: for t9 being Real st 0 <= t9 & t9 <= 1 / 2 holds (g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t9 = g1 . (2 * t9) proof reconsider r1 = (#) (0,1), r2 = (0,1) (#) as Real by TREAL_1:5; dom (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) = the carrier of (Closed-Interval-TSpace (0,(1 / 2))) by FUNCT_2:def_1; then A13: dom (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) = [.0,(1 / 2).] by TOPMETR:18 .= { r where r is Real : ( 0 <= r & r <= 1 / 2 ) } by RCOMP_1:def_1 ; let t9 be Real; ::_thesis: ( 0 <= t9 & t9 <= 1 / 2 implies (g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t9 = g1 . (2 * t9) ) assume ( 0 <= t9 & t9 <= 1 / 2 ) ; ::_thesis: (g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t9 = g1 . (2 * t9) then A14: t9 in dom (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) by A13; then reconsider s = t9 as Point of (Closed-Interval-TSpace (0,(1 / 2))) ; (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) . s = (((r2 - r1) / ((1 / 2) - 0)) * t9) + ((((1 / 2) * r1) - (0 * r2)) / ((1 / 2) - 0)) by TREAL_1:11 .= 2 * t9 by TREAL_1:5 ; hence (g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t9 = g1 . (2 * t9) by A14, FUNCT_1:13; ::_thesis: verum end; then A15: ff . (1 / 2) = g2 . ((2 * (1 / 2)) - 1) by A3, A5 .= gg . pol by A9 ; ( [#] T1 = [.0,(1 / 2).] & [#] T2 = [.(1 / 2),1.] ) by TOPMETR:18; then A16: ( ([#] T1) \/ ([#] T2) = [#] I[01] & ([#] T1) /\ ([#] T2) = {pol} ) by BORSUK_1:40, XXREAL_1:174, XXREAL_1:418; A17: T2 is compact by HEINE:4; dom g1 = the carrier of I[01] by FUNCT_2:def_1; then A18: rng (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) c= dom g1 by TOPMETR:20; ( dom g2 = the carrier of I[01] & rng (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) c= the carrier of (Closed-Interval-TSpace (0,1)) ) by FUNCT_2:def_1; then A19: dom (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) = dom (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) by RELAT_1:27, TOPMETR:20; not 0 in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) } proof assume 0 in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) } ; ::_thesis: contradiction then ex rr being Real st ( rr = 0 & 1 / 2 <= rr & rr <= 1 ) ; hence contradiction ; ::_thesis: verum end; then not 0 in dom (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) by A8, A19, RCOMP_1:def_1; then A20: ((g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) . 0 = (g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . 0 by FUNCT_4:11 .= g1 . (2 * 0) by A12 .= w1 by A2 ; A21: dom ((g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) = (dom (g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))))) \/ (dom (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) by FUNCT_4:def_1 .= [.0,(1 / 2).] \/ [.(1 / 2),1.] by A7, A8, A18, A19, RELAT_1:27 .= the carrier of I[01] by BORSUK_1:40, XXREAL_1:174 ; rng ((g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) c= (rng (g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))))) \/ (rng (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) by FUNCT_4:17; then A22: rng ((g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) c= the carrier of G by XBOOLE_1:1; A23: ( R^1 is T_2 & T1 is compact ) by HEINE:4, PCOMPS_1:34, TOPMETR:def_6; reconsider f = (g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) as Function of I[01],G by A21, A22, FUNCT_2:def_1, RELSET_1:4; ( P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))) is continuous & P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))) is continuous ) by TREAL_1:12; then reconsider f = f as continuous Function of I[01],G by A1, A4, A15, A16, A23, A17, COMPTS_1:20, TOPMETR:20; 1 in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) } ; then 1 in dom (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) by A8, A19, RCOMP_1:def_1; then A24: f . 1 = (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . 1 by FUNCT_4:13 .= g2 . ((2 * 1) - 1) by A9 .= w3 by A6 ; then w1,w3 are_connected by A20, Def1; then reconsider f = f as Path of w1,w3 by A20, A24, Def2; for t being Point of I[01] for t9 being Real st t = t9 holds ( ( 0 <= t9 & t9 <= 1 / 2 implies f . t = g1 . (2 * t9) ) & ( 1 / 2 <= t9 & t9 <= 1 implies f . t = g2 . ((2 * t9) - 1) ) ) proof let t be Point of I[01]; ::_thesis: for t9 being Real st t = t9 holds ( ( 0 <= t9 & t9 <= 1 / 2 implies f . t = g1 . (2 * t9) ) & ( 1 / 2 <= t9 & t9 <= 1 implies f . t = g2 . ((2 * t9) - 1) ) ) let t9 be Real; ::_thesis: ( t = t9 implies ( ( 0 <= t9 & t9 <= 1 / 2 implies f . t = g1 . (2 * t9) ) & ( 1 / 2 <= t9 & t9 <= 1 implies f . t = g2 . ((2 * t9) - 1) ) ) ) assume A25: t = t9 ; ::_thesis: ( ( 0 <= t9 & t9 <= 1 / 2 implies f . t = g1 . (2 * t9) ) & ( 1 / 2 <= t9 & t9 <= 1 implies f . t = g2 . ((2 * t9) - 1) ) ) thus ( 0 <= t9 & t9 <= 1 / 2 implies f . t = g1 . (2 * t9) ) ::_thesis: ( 1 / 2 <= t9 & t9 <= 1 implies f . t = g2 . ((2 * t9) - 1) ) proof assume A26: ( 0 <= t9 & t9 <= 1 / 2 ) ; ::_thesis: f . t = g1 . (2 * t9) then t9 in { r where r is Real : ( 0 <= r & r <= 1 / 2 ) } ; then A27: t9 in [.0,(1 / 2).] by RCOMP_1:def_1; percases ( t9 <> 1 / 2 or t9 = 1 / 2 ) ; supposeA28: t9 <> 1 / 2 ; ::_thesis: f . t = g1 . (2 * t9) not t9 in dom (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) proof assume t9 in dom (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) ; ::_thesis: contradiction then t9 in [.0,(1 / 2).] /\ [.(1 / 2),1.] by A8, A19, A27, XBOOLE_0:def_4; then t9 in {(1 / 2)} by XXREAL_1:418; hence contradiction by A28, TARSKI:def_1; ::_thesis: verum end; then f . t = (g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t by A25, FUNCT_4:11 .= g1 . (2 * t9) by A12, A25, A26 ; hence f . t = g1 . (2 * t9) ; ::_thesis: verum end; supposeA29: t9 = 1 / 2 ; ::_thesis: f . t = g1 . (2 * t9) 1 / 2 in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) } ; then 1 / 2 in [.(1 / 2),1.] by RCOMP_1:def_1; then 1 / 2 in the carrier of (Closed-Interval-TSpace ((1 / 2),1)) by TOPMETR:18; then t in dom (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) by A25, A29, FUNCT_2:def_1, TOPMETR:20; then f . t = (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . (1 / 2) by A25, A29, FUNCT_4:13 .= g1 . (2 * t9) by A12, A15, A29 ; hence f . t = g1 . (2 * t9) ; ::_thesis: verum end; end; end; thus ( 1 / 2 <= t9 & t9 <= 1 implies f . t = g2 . ((2 * t9) - 1) ) ::_thesis: verum proof assume A30: ( 1 / 2 <= t9 & t9 <= 1 ) ; ::_thesis: f . t = g2 . ((2 * t9) - 1) then t9 in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) } ; then t9 in [.(1 / 2),1.] by RCOMP_1:def_1; then f . t = (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t by A8, A19, A25, FUNCT_4:13 .= g2 . ((2 * t9) - 1) by A9, A25, A30 ; hence f . t = g2 . ((2 * t9) - 1) ; ::_thesis: verum end; end; hence ex P0 being Path of w1,w3 st ( P0 is continuous & P0 . 0 = w1 & P0 . 1 = w3 & ( for t being Point of I[01] for t9 being Real st t = t9 holds ( ( 0 <= t9 & t9 <= 1 / 2 implies P0 . t = g1 . (2 * t9) ) & ( 1 / 2 <= t9 & t9 <= 1 implies P0 . t = g2 . ((2 * t9) - 1) ) ) ) ) by A20, A24; ::_thesis: verum end; then consider P0 being Path of w1,w3 such that A31: ( P0 is continuous & P0 . 0 = w1 & P0 . 1 = w3 ) and A32: for t being Point of I[01] for t9 being Real st t = t9 holds ( ( 0 <= t9 & t9 <= 1 / 2 implies P0 . t = g1 . (2 * t9) ) & ( 1 / 2 <= t9 & t9 <= 1 implies P0 . t = g2 . ((2 * t9) - 1) ) ) ; rng P0 c= (rng g1) \/ (rng g2) proof A33: dom g2 = the carrier of I[01] by FUNCT_2:def_1; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng P0 or x in (rng g1) \/ (rng g2) ) A34: dom g1 = the carrier of I[01] by FUNCT_2:def_1; assume x in rng P0 ; ::_thesis: x in (rng g1) \/ (rng g2) then consider z being set such that A35: z in dom P0 and A36: x = P0 . z by FUNCT_1:def_3; dom P0 = the carrier of I[01] by FUNCT_2:def_1; then reconsider r = z as Real by A35, BORSUK_1:40; A37: 0 <= r by A35, BORSUK_1:40, XXREAL_1:1; A38: r <= 1 by A35, BORSUK_1:40, XXREAL_1:1; percases ( r <= 1 / 2 or r > 1 / 2 ) ; supposeA39: r <= 1 / 2 ; ::_thesis: x in (rng g1) \/ (rng g2) then A40: 2 * r <= 2 * (1 / 2) by XREAL_1:64; 0 <= 2 * r by A37, XREAL_1:127; then A41: 2 * r in the carrier of I[01] by A40, BORSUK_1:40, XXREAL_1:1; P0 . z = g1 . (2 * r) by A32, A35, A37, A39; then P0 . z in rng g1 by A34, A41, FUNCT_1:def_3; hence x in (rng g1) \/ (rng g2) by A36, XBOOLE_0:def_3; ::_thesis: verum end; supposeA42: r > 1 / 2 ; ::_thesis: x in (rng g1) \/ (rng g2) 2 * r <= 2 * 1 by A38, XREAL_1:64; then 2 * r <= 1 + 1 ; then A43: (2 * r) - 1 <= 1 by XREAL_1:20; 2 * (1 / 2) = 1 ; then 0 + 1 <= 2 * r by A42, XREAL_1:64; then 0 <= (2 * r) - 1 by XREAL_1:19; then A44: (2 * r) - 1 in the carrier of I[01] by A43, BORSUK_1:40, XXREAL_1:1; P0 . z = g2 . ((2 * r) - 1) by A32, A35, A38, A42; then P0 . z in rng g2 by A33, A44, FUNCT_1:def_3; hence x in (rng g1) \/ (rng g2) by A36, XBOOLE_0:def_3; ::_thesis: verum end; end; end; hence ex h3 being Function of I[01],G st ( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 & rng h3 c= (rng h1) \/ (rng h2) ) by A31; ::_thesis: verum end; definition let T be non empty TopSpace; let a, b, c be Point of T; let P be Path of a,b; let Q be Path of b,c; assume that B1: a,b are_connected and B2: b,c are_connected ; funcP + Q -> Path of a,c means :Def5: :: BORSUK_2:def 5 for t being Point of I[01] holds ( ( t <= 1 / 2 implies it . t = P . (2 * t) ) & ( 1 / 2 <= t implies it . t = Q . ((2 * t) - 1) ) ); existence ex b1 being Path of a,c st for t being Point of I[01] holds ( ( t <= 1 / 2 implies b1 . t = P . (2 * t) ) & ( 1 / 2 <= t implies b1 . t = Q . ((2 * t) - 1) ) ) proof 1 / 2 in { r where r is Real : ( 0 <= r & r <= 1 ) } ; then reconsider pol = 1 / 2 as Point of I[01] by BORSUK_1:40, RCOMP_1:def_1; reconsider T1 = Closed-Interval-TSpace (0,(1 / 2)), T2 = Closed-Interval-TSpace ((1 / 2),1) as SubSpace of I[01] by TOPMETR:20, TREAL_1:3; set e2 = P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))); set e1 = P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))); set E1 = P * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))); set E2 = Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))); set f = (P * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))); A1: dom (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) = the carrier of (Closed-Interval-TSpace (0,(1 / 2))) by FUNCT_2:def_1 .= [.0,(1 / 2).] by TOPMETR:18 ; A2: dom (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) = the carrier of (Closed-Interval-TSpace ((1 / 2),1)) by FUNCT_2:def_1 .= [.(1 / 2),1.] by TOPMETR:18 ; A3: for t9 being Real st 1 / 2 <= t9 & t9 <= 1 holds (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t9 = Q . ((2 * t9) - 1) proof reconsider r1 = (#) (0,1), r2 = (0,1) (#) as Real by TREAL_1:5; dom (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) = the carrier of (Closed-Interval-TSpace ((1 / 2),1)) by FUNCT_2:def_1; then A4: dom (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) = [.(1 / 2),1.] by TOPMETR:18 .= { r where r is Real : ( 1 / 2 <= r & r <= 1 ) } by RCOMP_1:def_1 ; let t9 be Real; ::_thesis: ( 1 / 2 <= t9 & t9 <= 1 implies (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t9 = Q . ((2 * t9) - 1) ) assume ( 1 / 2 <= t9 & t9 <= 1 ) ; ::_thesis: (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t9 = Q . ((2 * t9) - 1) then A5: t9 in dom (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) by A4; then reconsider s = t9 as Point of (Closed-Interval-TSpace ((1 / 2),1)) ; (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) . s = (((r2 - r1) / (1 - (1 / 2))) * t9) + (((1 * r1) - ((1 / 2) * r2)) / (1 - (1 / 2))) by TREAL_1:11 .= (2 * t9) - 1 by TREAL_1:5 ; hence (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t9 = Q . ((2 * t9) - 1) by A5, FUNCT_1:13; ::_thesis: verum end; reconsider gg = Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) as Function of T2,T by TOPMETR:20; reconsider ff = P * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) as Function of T1,T by TOPMETR:20; A6: ( P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))) is continuous Function of (Closed-Interval-TSpace (0,(1 / 2))),(Closed-Interval-TSpace (0,1)) & P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))) is continuous ) by TREAL_1:12; rng ((P * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) c= (rng (P * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))))) \/ (rng (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) by FUNCT_4:17; then A7: rng ((P * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) c= the carrier of T by XBOOLE_1:1; A8: ( R^1 is T_2 & T1 is compact ) by HEINE:4, PCOMPS_1:34, TOPMETR:def_6; A9: for t9 being Real st 0 <= t9 & t9 <= 1 / 2 holds (P * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t9 = P . (2 * t9) proof reconsider r1 = (#) (0,1), r2 = (0,1) (#) as Real by TREAL_1:5; dom (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) = the carrier of (Closed-Interval-TSpace (0,(1 / 2))) by FUNCT_2:def_1; then A10: dom (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) = [.0,(1 / 2).] by TOPMETR:18 .= { r where r is Real : ( 0 <= r & r <= 1 / 2 ) } by RCOMP_1:def_1 ; let t9 be Real; ::_thesis: ( 0 <= t9 & t9 <= 1 / 2 implies (P * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t9 = P . (2 * t9) ) assume ( 0 <= t9 & t9 <= 1 / 2 ) ; ::_thesis: (P * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t9 = P . (2 * t9) then A11: t9 in dom (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) by A10; then reconsider s = t9 as Point of (Closed-Interval-TSpace (0,(1 / 2))) ; (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) . s = (((r2 - r1) / ((1 / 2) - 0)) * t9) + ((((1 / 2) * r1) - (0 * r2)) / (1 / 2)) by TREAL_1:11 .= 2 * t9 by TREAL_1:5 ; hence (P * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t9 = P . (2 * t9) by A11, FUNCT_1:13; ::_thesis: verum end; then A12: ff . (1 / 2) = P . (2 * (1 / 2)) .= b by B1, Def2 .= Q . ((2 * (1 / 2)) - 1) by B2, Def2 .= gg . pol by A3 ; dom P = the carrier of I[01] by FUNCT_2:def_1; then A13: rng (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) c= dom P by TOPMETR:20; ( dom Q = the carrier of I[01] & rng (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) c= the carrier of (Closed-Interval-TSpace (0,1)) ) by FUNCT_2:def_1; then A14: dom (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) = dom (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) by RELAT_1:27, TOPMETR:20; not 0 in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) } proof assume 0 in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) } ; ::_thesis: contradiction then ex rr being Real st ( rr = 0 & 1 / 2 <= rr & rr <= 1 ) ; hence contradiction ; ::_thesis: verum end; then not 0 in dom (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) by A2, A14, RCOMP_1:def_1; then A15: ((P * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) . 0 = (P * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . 0 by FUNCT_4:11 .= P . (2 * 0) by A9 .= a by B1, Def2 ; A16: dom ((P * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) = (dom (P * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))))) \/ (dom (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) by FUNCT_4:def_1 .= [.0,(1 / 2).] \/ [.(1 / 2),1.] by A1, A2, A13, A14, RELAT_1:27 .= the carrier of I[01] by BORSUK_1:40, XXREAL_1:174 ; ( [#] T1 = [.0,(1 / 2).] & [#] T2 = [.(1 / 2),1.] ) by TOPMETR:18; then A17: ( ([#] T1) \/ ([#] T2) = [#] I[01] & ([#] T1) /\ ([#] T2) = {pol} ) by BORSUK_1:40, XXREAL_1:174, XXREAL_1:418; A18: T2 is compact by HEINE:4; reconsider f = (P * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) as Function of I[01],T by A16, A7, FUNCT_2:def_1, RELSET_1:4; ( P is continuous & Q is continuous ) by B1, B2, Def2; then reconsider f = f as continuous Function of I[01],T by A6, A12, A17, A8, A18, COMPTS_1:20, TOPMETR:20; 1 in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) } ; then 1 in dom (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) by A2, A14, RCOMP_1:def_1; then A19: f . 1 = (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . 1 by FUNCT_4:13 .= Q . ((2 * 1) - 1) by A3 .= c by B2, Def2 ; then a,c are_connected by A15, Def1; then reconsider f = f as Path of a,c by A15, A19, Def2; for t being Point of I[01] holds ( ( t <= 1 / 2 implies f . t = P . (2 * t) ) & ( 1 / 2 <= t implies f . t = Q . ((2 * t) - 1) ) ) proof let t be Point of I[01]; ::_thesis: ( ( t <= 1 / 2 implies f . t = P . (2 * t) ) & ( 1 / 2 <= t implies f . t = Q . ((2 * t) - 1) ) ) A20: t is Real by XREAL_0:def_1; A21: 0 <= t by Lm1; thus ( t <= 1 / 2 implies f . t = P . (2 * t) ) ::_thesis: ( 1 / 2 <= t implies f . t = Q . ((2 * t) - 1) ) proof assume A22: t <= 1 / 2 ; ::_thesis: f . t = P . (2 * t) then t in { r where r is Real : ( 0 <= r & r <= 1 / 2 ) } by A21, A20; then A23: t in [.0,(1 / 2).] by RCOMP_1:def_1; percases ( t <> 1 / 2 or t = 1 / 2 ) ; supposeA24: t <> 1 / 2 ; ::_thesis: f . t = P . (2 * t) not t in dom (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) proof assume t in dom (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) ; ::_thesis: contradiction then t in [.0,(1 / 2).] /\ [.(1 / 2),1.] by A2, A14, A23, XBOOLE_0:def_4; then t in {(1 / 2)} by XXREAL_1:418; hence contradiction by A24, TARSKI:def_1; ::_thesis: verum end; then f . t = (P * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t by FUNCT_4:11 .= P . (2 * t) by A9, A21, A20, A22 ; hence f . t = P . (2 * t) ; ::_thesis: verum end; supposeA25: t = 1 / 2 ; ::_thesis: f . t = P . (2 * t) 1 / 2 in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) } ; then 1 / 2 in [.(1 / 2),1.] by RCOMP_1:def_1; then 1 / 2 in the carrier of (Closed-Interval-TSpace ((1 / 2),1)) by TOPMETR:18; then t in dom (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) by A25, FUNCT_2:def_1, TOPMETR:20; then f . t = (P * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t by A12, A25, FUNCT_4:13 .= P . (2 * t) by A9, A21, A20, A22 ; hence f . t = P . (2 * t) ; ::_thesis: verum end; end; end; A26: t <= 1 by Lm1; thus ( 1 / 2 <= t implies f . t = Q . ((2 * t) - 1) ) ::_thesis: verum proof assume A27: 1 / 2 <= t ; ::_thesis: f . t = Q . ((2 * t) - 1) then t in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) } by A26, A20; then t in [.(1 / 2),1.] by RCOMP_1:def_1; then f . t = (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t by A2, A14, FUNCT_4:13 .= Q . ((2 * t) - 1) by A3, A26, A20, A27 ; hence f . t = Q . ((2 * t) - 1) ; ::_thesis: verum end; end; hence ex b1 being Path of a,c st for t being Point of I[01] holds ( ( t <= 1 / 2 implies b1 . t = P . (2 * t) ) & ( 1 / 2 <= t implies b1 . t = Q . ((2 * t) - 1) ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Path of a,c st ( for t being Point of I[01] holds ( ( t <= 1 / 2 implies b1 . t = P . (2 * t) ) & ( 1 / 2 <= t implies b1 . t = Q . ((2 * t) - 1) ) ) ) & ( for t being Point of I[01] holds ( ( t <= 1 / 2 implies b2 . t = P . (2 * t) ) & ( 1 / 2 <= t implies b2 . t = Q . ((2 * t) - 1) ) ) ) holds b1 = b2 proof let A, B be Path of a,c; ::_thesis: ( ( for t being Point of I[01] holds ( ( t <= 1 / 2 implies A . t = P . (2 * t) ) & ( 1 / 2 <= t implies A . t = Q . ((2 * t) - 1) ) ) ) & ( for t being Point of I[01] holds ( ( t <= 1 / 2 implies B . t = P . (2 * t) ) & ( 1 / 2 <= t implies B . t = Q . ((2 * t) - 1) ) ) ) implies A = B ) assume that A28: for t being Point of I[01] holds ( ( t <= 1 / 2 implies A . t = P . (2 * t) ) & ( 1 / 2 <= t implies A . t = Q . ((2 * t) - 1) ) ) and A29: for t being Point of I[01] holds ( ( t <= 1 / 2 implies B . t = P . (2 * t) ) & ( 1 / 2 <= t implies B . t = Q . ((2 * t) - 1) ) ) ; ::_thesis: A = B A30: for x being set st x in dom A holds A . x = B . x proof let x be set ; ::_thesis: ( x in dom A implies A . x = B . x ) assume A31: x in dom A ; ::_thesis: A . x = B . x then reconsider y = x as Point of I[01] ; x in the carrier of I[01] by A31; then x in { r where r is Real : ( 0 <= r & r <= 1 ) } by BORSUK_1:40, RCOMP_1:def_1; then consider r9 being Real such that A32: r9 = x and 0 <= r9 and r9 <= 1 ; percases ( r9 <= 1 / 2 or 1 / 2 < r9 ) ; supposeA33: r9 <= 1 / 2 ; ::_thesis: A . x = B . x then A . y = P . (2 * r9) by A28, A32 .= B . y by A29, A32, A33 ; hence A . x = B . x ; ::_thesis: verum end; supposeA34: 1 / 2 < r9 ; ::_thesis: A . x = B . x then A . y = Q . ((2 * r9) - 1) by A28, A32 .= B . y by A29, A32, A34 ; hence A . x = B . x ; ::_thesis: verum end; end; end; dom B = the carrier of I[01] by FUNCT_2:def_1; then dom A = dom B by FUNCT_2:def_1; hence A = B by A30, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def5 defines + BORSUK_2:def_5_:_ for T being non empty TopSpace for a, b, c being Point of T for P being Path of a,b for Q being Path of b,c st a,b are_connected & b,c are_connected holds for b7 being Path of a,c holds ( b7 = P + Q iff for t being Point of I[01] holds ( ( t <= 1 / 2 implies b7 . t = P . (2 * t) ) & ( 1 / 2 <= t implies b7 . t = Q . ((2 * t) - 1) ) ) ); registration let T be non empty TopSpace; let a be Point of T; cluster non empty Relation-like the carrier of I[01] -defined the carrier of T -valued Function-like constant V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of T) for Path of a,a; existence ex b1 being Path of a,a st b1 is constant proof set IT = I[01] --> a; A1: ( (I[01] --> a) . 0 = a & (I[01] --> a) . 1 = a ) by BORSUK_1:def_14, BORSUK_1:def_15, FUNCOP_1:7; a,a are_connected ; then reconsider IT = I[01] --> a as Path of a,a by A1, Def2; for n1, n2 being set st n1 in dom IT & n2 in dom IT holds IT . n1 = IT . n2 proof let n1, n2 be set ; ::_thesis: ( n1 in dom IT & n2 in dom IT implies IT . n1 = IT . n2 ) assume that A2: n1 in dom IT and A3: n2 in dom IT ; ::_thesis: IT . n1 = IT . n2 IT . n1 = a by A2, FUNCOP_1:7 .= IT . n2 by A3, FUNCOP_1:7 ; hence IT . n1 = IT . n2 ; ::_thesis: verum end; then IT is constant by FUNCT_1:def_10; hence ex b1 being Path of a,a st b1 is constant ; ::_thesis: verum end; end; theorem :: BORSUK_2:4 canceled; theorem :: BORSUK_2:5 for T being non empty TopSpace for a being Point of T for P being constant Path of a,a holds P = I[01] --> a proof let T be non empty TopSpace; ::_thesis: for a being Point of T for P being constant Path of a,a holds P = I[01] --> a let a be Point of T; ::_thesis: for P being constant Path of a,a holds P = I[01] --> a let P be constant Path of a,a; ::_thesis: P = I[01] --> a set IT = I[01] --> a; A1: dom P = the carrier of I[01] by FUNCT_2:def_1; A2: a,a are_connected ; A3: for x being set st x in the carrier of I[01] holds P . x = (I[01] --> a) . x proof 0 in { r where r is Real : ( 0 <= r & r <= 1 ) } ; then A4: 0 in the carrier of I[01] by BORSUK_1:40, RCOMP_1:def_1; let x be set ; ::_thesis: ( x in the carrier of I[01] implies P . x = (I[01] --> a) . x ) assume A5: x in the carrier of I[01] ; ::_thesis: P . x = (I[01] --> a) . x P . 0 = a by A2, Def2; then P . x = a by A1, A5, A4, FUNCT_1:def_10 .= (I[01] --> a) . x by A5, FUNCOP_1:7 ; hence P . x = (I[01] --> a) . x ; ::_thesis: verum end; dom (I[01] --> a) = the carrier of I[01] by FUNCT_2:def_1; hence P = I[01] --> a by A1, A3, FUNCT_1:2; ::_thesis: verum end; theorem Th6: :: BORSUK_2:6 for T being non empty TopSpace for a being Point of T for P being constant Path of a,a holds P + P = P proof let T be non empty TopSpace; ::_thesis: for a being Point of T for P being constant Path of a,a holds P + P = P let a be Point of T; ::_thesis: for P being constant Path of a,a holds P + P = P let P be constant Path of a,a; ::_thesis: P + P = P A1: the carrier of I[01] = dom P by FUNCT_2:def_1; A2: for x being set st x in the carrier of I[01] holds P . x = (P + P) . x proof let x be set ; ::_thesis: ( x in the carrier of I[01] implies P . x = (P + P) . x ) assume A3: x in the carrier of I[01] ; ::_thesis: P . x = (P + P) . x then reconsider p = x as Point of I[01] ; x in { r where r is Real : ( 0 <= r & r <= 1 ) } by A3, BORSUK_1:40, RCOMP_1:def_1; then consider r being Real such that A4: r = x and A5: 0 <= r and A6: r <= 1 ; percases ( r < 1 / 2 or r >= 1 / 2 ) ; supposeA7: r < 1 / 2 ; ::_thesis: P . x = (P + P) . x then A8: r * 2 < (1 / 2) * 2 by XREAL_1:68; 2 * r >= 0 by A5, XREAL_1:127; then 2 * r in { e where e is Real : ( 0 <= e & e <= 1 ) } by A8; then 2 * r in the carrier of I[01] by BORSUK_1:40, RCOMP_1:def_1; then P . (2 * r) = P . p by A1, FUNCT_1:def_10; hence P . x = (P + P) . x by A4, A7, Def5; ::_thesis: verum end; supposeA9: r >= 1 / 2 ; ::_thesis: P . x = (P + P) . x then r * 2 >= (1 / 2) * 2 by XREAL_1:64; then 2 * r >= 1 + 0 ; then A10: (2 * r) - 1 >= 0 by XREAL_1:19; r * 2 <= 1 * 2 by A6, XREAL_1:64; then (2 * r) - 1 <= 2 - 1 by XREAL_1:13; then (2 * r) - 1 in { e where e is Real : ( 0 <= e & e <= 1 ) } by A10; then (2 * r) - 1 in the carrier of I[01] by BORSUK_1:40, RCOMP_1:def_1; then P . ((2 * r) - 1) = P . p by A1, FUNCT_1:def_10; hence P . x = (P + P) . x by A4, A9, Def5; ::_thesis: verum end; end; end; dom (P + P) = the carrier of I[01] by FUNCT_2:def_1; hence P + P = P by A1, A2, FUNCT_1:2; ::_thesis: verum end; registration let T be non empty TopSpace; let a be Point of T; let P be constant Path of a,a; clusterP + P -> constant ; coherence P + P is constant by Th6; end; definition let T be non empty TopSpace; let a, b be Point of T; let P be Path of a,b; assume A1: a,b are_connected ; func - P -> Path of b,a means :Def6: :: BORSUK_2:def 6 for t being Point of I[01] holds it . t = P . (1 - t); existence ex b1 being Path of b,a st for t being Point of I[01] holds b1 . t = P . (1 - t) proof set e = L[01] (((0,1) (#)),((#) (0,1))); reconsider f = P * (L[01] (((0,1) (#)),((#) (0,1)))) as Function of I[01],T by TOPMETR:20; A2: for t being Point of I[01] holds f . t = P . (1 - t) proof let t be Point of I[01]; ::_thesis: f . t = P . (1 - t) reconsider ee = t as Point of (Closed-Interval-TSpace (0,1)) by TOPMETR:20; A3: ( (0,1) (#) = 1 & (#) (0,1) = 0 ) by TREAL_1:def_1, TREAL_1:def_2; t in the carrier of (Closed-Interval-TSpace (0,1)) by TOPMETR:20; then t in dom (L[01] (((0,1) (#)),((#) (0,1)))) by FUNCT_2:def_1; then f . t = P . ((L[01] (((0,1) (#)),((#) (0,1)))) . ee) by FUNCT_1:13 .= P . (((0 - 1) * t) + 1) by A3, TREAL_1:7 .= P . (1 - (1 * t)) ; hence f . t = P . (1 - t) ; ::_thesis: verum end; 0 in { r where r is Real : ( 0 <= r & r <= 1 ) } ; then 0 in [.0,1.] by RCOMP_1:def_1; then 0 in the carrier of (Closed-Interval-TSpace (0,1)) by TOPMETR:18; then A4: 0 in dom (L[01] (((0,1) (#)),((#) (0,1)))) by FUNCT_2:def_1; (L[01] (((0,1) (#)),((#) (0,1)))) . 0 = (L[01] (((0,1) (#)),((#) (0,1)))) . ((#) (0,1)) by TREAL_1:def_1 .= (0,1) (#) by TREAL_1:9 .= 1 by TREAL_1:def_2 ; then A5: f . 0 = P . 1 by A4, FUNCT_1:13 .= b by A1, Def2 ; 1 in { r where r is Real : ( 0 <= r & r <= 1 ) } ; then 1 in [.0,1.] by RCOMP_1:def_1; then 1 in the carrier of (Closed-Interval-TSpace (0,1)) by TOPMETR:18; then A6: 1 in dom (L[01] (((0,1) (#)),((#) (0,1)))) by FUNCT_2:def_1; (L[01] (((0,1) (#)),((#) (0,1)))) . 1 = (L[01] (((0,1) (#)),((#) (0,1)))) . ((0,1) (#)) by TREAL_1:def_2 .= (#) (0,1) by TREAL_1:9 .= 0 by TREAL_1:def_1 ; then A7: f . 1 = P . 0 by A6, FUNCT_1:13 .= a by A1, Def2 ; A8: ( P is continuous & L[01] (((0,1) (#)),((#) (0,1))) is continuous Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (0,1)) ) by A1, Def2, TREAL_1:8; then b,a are_connected by A5, A7, Def1, TOPMETR:20; then reconsider f = f as Path of b,a by A5, A7, A8, Def2, TOPMETR:20; take f ; ::_thesis: for t being Point of I[01] holds f . t = P . (1 - t) thus for t being Point of I[01] holds f . t = P . (1 - t) by A2; ::_thesis: verum end; uniqueness for b1, b2 being Path of b,a st ( for t being Point of I[01] holds b1 . t = P . (1 - t) ) & ( for t being Point of I[01] holds b2 . t = P . (1 - t) ) holds b1 = b2 proof let R, Q be Path of b,a; ::_thesis: ( ( for t being Point of I[01] holds R . t = P . (1 - t) ) & ( for t being Point of I[01] holds Q . t = P . (1 - t) ) implies R = Q ) assume that A9: for t being Point of I[01] holds R . t = P . (1 - t) and A10: for t being Point of I[01] holds Q . t = P . (1 - t) ; ::_thesis: R = Q A11: for x being set st x in the carrier of I[01] holds R . x = Q . x proof let x be set ; ::_thesis: ( x in the carrier of I[01] implies R . x = Q . x ) assume x in the carrier of I[01] ; ::_thesis: R . x = Q . x then reconsider x9 = x as Point of I[01] ; R . x9 = P . (1 - x9) by A9 .= Q . x9 by A10 ; hence R . x = Q . x ; ::_thesis: verum end; ( dom R = the carrier of I[01] & the carrier of I[01] = dom Q ) by FUNCT_2:def_1; hence R = Q by A11, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def6 defines - BORSUK_2:def_6_:_ for T being non empty TopSpace for a, b being Point of T for P being Path of a,b st a,b are_connected holds for b5 being Path of b,a holds ( b5 = - P iff for t being Point of I[01] holds b5 . t = P . (1 - t) ); Lm4: for r being Real st 0 <= r & r <= 1 holds ( 0 <= 1 - r & 1 - r <= 1 ) proof let r be Real; ::_thesis: ( 0 <= r & r <= 1 implies ( 0 <= 1 - r & 1 - r <= 1 ) ) assume ( 0 <= r & r <= 1 ) ; ::_thesis: ( 0 <= 1 - r & 1 - r <= 1 ) then ( 1 - 1 <= 1 - r & 1 - r <= 1 - 0 ) by XREAL_1:13; hence ( 0 <= 1 - r & 1 - r <= 1 ) ; ::_thesis: verum end; Lm5: for r being Real st r in the carrier of I[01] holds 1 - r in the carrier of I[01] proof let r be Real; ::_thesis: ( r in the carrier of I[01] implies 1 - r in the carrier of I[01] ) assume r in the carrier of I[01] ; ::_thesis: 1 - r in the carrier of I[01] then ( 0 <= r & r <= 1 ) by Lm1; then ( 0 <= 1 - r & 1 - r <= 1 ) by Lm4; hence 1 - r in the carrier of I[01] by Lm1; ::_thesis: verum end; theorem Th7: :: BORSUK_2:7 for T being non empty TopSpace for a being Point of T for P being constant Path of a,a holds - P = P proof let T be non empty TopSpace; ::_thesis: for a being Point of T for P being constant Path of a,a holds - P = P let a be Point of T; ::_thesis: for P being constant Path of a,a holds - P = P let P be constant Path of a,a; ::_thesis: - P = P A1: dom P = the carrier of I[01] by FUNCT_2:def_1; A2: for x being set st x in the carrier of I[01] holds P . x = (- P) . x proof let x be set ; ::_thesis: ( x in the carrier of I[01] implies P . x = (- P) . x ) assume A3: x in the carrier of I[01] ; ::_thesis: P . x = (- P) . x then reconsider x2 = x as Real by BORSUK_1:40; reconsider x3 = 1 - x2 as Point of I[01] by A3, Lm5; (- P) . x = P . x3 by A3, Def6 .= P . x by A1, A3, FUNCT_1:def_10 ; hence P . x = (- P) . x ; ::_thesis: verum end; dom (- P) = the carrier of I[01] by FUNCT_2:def_1; hence - P = P by A1, A2, FUNCT_1:2; ::_thesis: verum end; registration let T be non empty TopSpace; let a be Point of T; let P be constant Path of a,a; cluster - P -> constant ; coherence - P is constant by Th7; end; begin theorem Th8: :: BORSUK_2:8 for X, Y being non empty TopSpace for A being Subset-Family of Y for f being Function of X,Y holds f " (union A) = union (f " A) proof let X, Y be non empty TopSpace; ::_thesis: for A being Subset-Family of Y for f being Function of X,Y holds f " (union A) = union (f " A) let A be Subset-Family of Y; ::_thesis: for f being Function of X,Y holds f " (union A) = union (f " A) let f be Function of X,Y; ::_thesis: f " (union A) = union (f " A) thus f " (union A) c= union (f " A) :: according to XBOOLE_0:def_10 ::_thesis: union (f " A) c= f " (union A) proof reconsider uA = union A as Subset of Y ; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f " (union A) or x in union (f " A) ) assume A1: x in f " (union A) ; ::_thesis: x in union (f " A) then f . x in uA by FUNCT_2:38; then consider YY being set such that A2: f . x in YY and A3: YY in A by TARSKI:def_4; reconsider fY = f " YY as Subset of X ; A4: fY in f " A by A3, FUNCT_2:def_9; x in f " YY by A1, A2, FUNCT_2:38; hence x in union (f " A) by A4, TARSKI:def_4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (f " A) or x in f " (union A) ) assume x in union (f " A) ; ::_thesis: x in f " (union A) then consider YY being set such that A5: x in YY and A6: YY in f " A by TARSKI:def_4; x in the carrier of X by A5, A6; then A7: x in dom f by FUNCT_2:def_1; reconsider B1 = YY as Subset of X by A6; consider B being Subset of Y such that A8: B in A and A9: B1 = f " B by A6, FUNCT_2:def_9; f . x in B by A5, A9, FUNCT_1:def_7; then f . x in union A by A8, TARSKI:def_4; hence x in f " (union A) by A7, FUNCT_1:def_7; ::_thesis: verum end; definition let S1, S2, T1, T2 be non empty TopSpace; let f be Function of S1,S2; let g be Function of T1,T2; :: original: [: redefine func[:f,g:] -> Function of [:S1,T1:],[:S2,T2:]; coherence [:f,g:] is Function of [:S1,T1:],[:S2,T2:] proof set h = [:f,g:]; rng [:f,g:] c= [: the carrier of S2, the carrier of T2:] ; then A1: rng [:f,g:] c= the carrier of [:S2,T2:] by BORSUK_1:def_2; dom [:f,g:] = [: the carrier of S1, the carrier of T1:] by FUNCT_2:def_1 .= the carrier of [:S1,T1:] by BORSUK_1:def_2 ; hence [:f,g:] is Function of [:S1,T1:],[:S2,T2:] by A1, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum end; end; theorem Th9: :: BORSUK_2:9 for S1, S2, T1, T2 being non empty TopSpace for f being continuous Function of S1,T1 for g being continuous Function of S2,T2 for P1, P2 being Subset of [:T1,T2:] st P2 in Base-Appr P1 holds [:f,g:] " P2 is open proof let S1, S2, T1, T2 be non empty TopSpace; ::_thesis: for f being continuous Function of S1,T1 for g being continuous Function of S2,T2 for P1, P2 being Subset of [:T1,T2:] st P2 in Base-Appr P1 holds [:f,g:] " P2 is open let f be continuous Function of S1,T1; ::_thesis: for g being continuous Function of S2,T2 for P1, P2 being Subset of [:T1,T2:] st P2 in Base-Appr P1 holds [:f,g:] " P2 is open let g be continuous Function of S2,T2; ::_thesis: for P1, P2 being Subset of [:T1,T2:] st P2 in Base-Appr P1 holds [:f,g:] " P2 is open let P1, P2 be Subset of [:T1,T2:]; ::_thesis: ( P2 in Base-Appr P1 implies [:f,g:] " P2 is open ) assume P2 in Base-Appr P1 ; ::_thesis: [:f,g:] " P2 is open then consider X11 being Subset of T1, Y11 being Subset of T2 such that A1: P2 = [:X11,Y11:] and [:X11,Y11:] c= P1 and A2: X11 is open and A3: Y11 is open ; [#] T1 <> {} ; then A4: f " X11 is open by A2, TOPS_2:43; [#] T2 <> {} ; then A5: g " Y11 is open by A3, TOPS_2:43; [:f,g:] " P2 = [:(f " X11),(g " Y11):] by A1, FUNCT_3:73; hence [:f,g:] " P2 is open by A4, A5, BORSUK_1:6; ::_thesis: verum end; theorem Th10: :: BORSUK_2:10 for S1, S2, T1, T2 being non empty TopSpace for f being continuous Function of S1,T1 for g being continuous Function of S2,T2 for P2 being Subset of [:T1,T2:] st P2 is open holds [:f,g:] " P2 is open proof let S1, S2, T1, T2 be non empty TopSpace; ::_thesis: for f being continuous Function of S1,T1 for g being continuous Function of S2,T2 for P2 being Subset of [:T1,T2:] st P2 is open holds [:f,g:] " P2 is open let f be continuous Function of S1,T1; ::_thesis: for g being continuous Function of S2,T2 for P2 being Subset of [:T1,T2:] st P2 is open holds [:f,g:] " P2 is open let g be continuous Function of S2,T2; ::_thesis: for P2 being Subset of [:T1,T2:] st P2 is open holds [:f,g:] " P2 is open let P2 be Subset of [:T1,T2:]; ::_thesis: ( P2 is open implies [:f,g:] " P2 is open ) reconsider Kill = [:f,g:] " (Base-Appr P2) as Subset-Family of [:S1,S2:] ; for P being Subset of [:S1,S2:] st P in Kill holds P is open proof let P be Subset of [:S1,S2:]; ::_thesis: ( P in Kill implies P is open ) assume P in Kill ; ::_thesis: P is open then ex B being Subset of [:T1,T2:] st ( B in Base-Appr P2 & P = [:f,g:] " B ) by FUNCT_2:def_9; hence P is open by Th9; ::_thesis: verum end; then A1: Kill is open by TOPS_2:def_1; assume P2 is open ; ::_thesis: [:f,g:] " P2 is open then P2 = union (Base-Appr P2) by BORSUK_1:13; then [:f,g:] " P2 = union ([:f,g:] " (Base-Appr P2)) by Th8; hence [:f,g:] " P2 is open by A1, TOPS_2:19; ::_thesis: verum end; registration let S1, S2, T1, T2 be non empty TopSpace; let f be continuous Function of S1,T1; let g be continuous Function of S2,T2; cluster[:f,g:] -> continuous for Function of [:S1,S2:],[:T1,T2:]; coherence for b1 being Function of [:S1,S2:],[:T1,T2:] st b1 = [:f,g:] holds b1 is continuous proof ( [#] [:T1,T2:] <> {} & ( for P1 being Subset of [:T1,T2:] st P1 is open holds [:f,g:] " P1 is open ) ) by Th10; hence for b1 being Function of [:S1,S2:],[:T1,T2:] st b1 = [:f,g:] holds b1 is continuous by TOPS_2:43; ::_thesis: verum end; end; registration let T1, T2 be T_0 TopSpace; cluster[:T1,T2:] -> T_0 ; coherence [:T1,T2:] is T_0 proof set T = [:T1,T2:]; percases ( T1 is empty or T2 is empty or ( not T1 is empty & not T2 is empty ) ) ; suppose ( T1 is empty or T2 is empty ) ; ::_thesis: [:T1,T2:] is T_0 hence [:T1,T2:] is T_0 ; ::_thesis: verum end; supposethat A1: not T1 is empty and A2: not T2 is empty ; ::_thesis: [:T1,T2:] is T_0 A3: not the carrier of [:T1,T2:] is empty by A1, A2; now__::_thesis:_for_p,_q_being_Point_of_[:T1,T2:]_st_p_<>_q_holds_ ex_X_being_Subset_of_[:T1,T2:]_st_ (_X_is_open_&_(_(_p_in_X_&_not_q_in_X_)_or_(_q_in_X_&_not_p_in_X_)_)_) let p, q be Point of [:T1,T2:]; ::_thesis: ( p <> q implies ex X being Subset of [:T1,T2:] st ( b3 is open & ( ( X in b3 & not b2 in b3 ) or ( b2 in b3 & not X in b3 ) ) ) ) assume A4: p <> q ; ::_thesis: ex X being Subset of [:T1,T2:] st ( b3 is open & ( ( X in b3 & not b2 in b3 ) or ( b2 in b3 & not X in b3 ) ) ) q in the carrier of [:T1,T2:] by A3; then q in [: the carrier of T1, the carrier of T2:] by BORSUK_1:def_2; then consider z, v being set such that A5: z in the carrier of T1 and A6: v in the carrier of T2 and A7: q = [z,v] by ZFMISC_1:def_2; p in the carrier of [:T1,T2:] by A3; then p in [: the carrier of T1, the carrier of T2:] by BORSUK_1:def_2; then consider x, y being set such that A8: x in the carrier of T1 and A9: y in the carrier of T2 and A10: p = [x,y] by ZFMISC_1:def_2; reconsider y = y, v = v as Point of T2 by A9, A6; reconsider x = x, z = z as Point of T1 by A8, A5; percases ( x <> z or x = z ) ; suppose x <> z ; ::_thesis: ex X being Subset of [:T1,T2:] st ( b3 is open & ( ( X in b3 & not b2 in b3 ) or ( b2 in b3 & not X in b3 ) ) ) then consider V1 being Subset of T1 such that A11: V1 is open and A12: ( ( x in V1 & not z in V1 ) or ( z in V1 & not x in V1 ) ) by T_0TOPSP:def_7, A1; set X = [:V1,([#] T2):]; A13: now__::_thesis:_(_(_p_in_[:V1,([#]_T2):]_&_not_q_in_[:V1,([#]_T2):]_)_or_(_q_in_[:V1,([#]_T2):]_&_not_p_in_[:V1,([#]_T2):]_)_) percases ( ( x in V1 & not z in V1 ) or ( z in V1 & not x in V1 ) ) by A12; suppose ( x in V1 & not z in V1 ) ; ::_thesis: ( ( p in [:V1,([#] T2):] & not q in [:V1,([#] T2):] ) or ( q in [:V1,([#] T2):] & not p in [:V1,([#] T2):] ) ) hence ( ( p in [:V1,([#] T2):] & not q in [:V1,([#] T2):] ) or ( q in [:V1,([#] T2):] & not p in [:V1,([#] T2):] ) ) by A9, A10, A7, ZFMISC_1:87; ::_thesis: verum end; suppose ( z in V1 & not x in V1 ) ; ::_thesis: ( ( p in [:V1,([#] T2):] & not q in [:V1,([#] T2):] ) or ( q in [:V1,([#] T2):] & not p in [:V1,([#] T2):] ) ) hence ( ( p in [:V1,([#] T2):] & not q in [:V1,([#] T2):] ) or ( q in [:V1,([#] T2):] & not p in [:V1,([#] T2):] ) ) by A10, A6, A7, ZFMISC_1:87; ::_thesis: verum end; end; end; [:V1,([#] T2):] is open by A11, BORSUK_1:6; hence ex X being Subset of [:T1,T2:] st ( X is open & ( ( p in X & not q in X ) or ( q in X & not p in X ) ) ) by A13; ::_thesis: verum end; suppose x = z ; ::_thesis: ex X being Subset of [:T1,T2:] st ( b3 is open & ( ( X in b3 & not b2 in b3 ) or ( b2 in b3 & not X in b3 ) ) ) then consider V1 being Subset of T2 such that A14: V1 is open and A15: ( ( y in V1 & not v in V1 ) or ( v in V1 & not y in V1 ) ) by A4, A10, A7, T_0TOPSP:def_7, A2; set X = [:([#] T1),V1:]; A16: now__::_thesis:_(_(_p_in_[:([#]_T1),V1:]_&_not_q_in_[:([#]_T1),V1:]_)_or_(_q_in_[:([#]_T1),V1:]_&_not_p_in_[:([#]_T1),V1:]_)_) percases ( ( y in V1 & not v in V1 ) or ( v in V1 & not y in V1 ) ) by A15; suppose ( y in V1 & not v in V1 ) ; ::_thesis: ( ( p in [:([#] T1),V1:] & not q in [:([#] T1),V1:] ) or ( q in [:([#] T1),V1:] & not p in [:([#] T1),V1:] ) ) hence ( ( p in [:([#] T1),V1:] & not q in [:([#] T1),V1:] ) or ( q in [:([#] T1),V1:] & not p in [:([#] T1),V1:] ) ) by A8, A10, A7, ZFMISC_1:87; ::_thesis: verum end; suppose ( v in V1 & not y in V1 ) ; ::_thesis: ( ( p in [:([#] T1),V1:] & not q in [:([#] T1),V1:] ) or ( q in [:([#] T1),V1:] & not p in [:([#] T1),V1:] ) ) hence ( ( p in [:([#] T1),V1:] & not q in [:([#] T1),V1:] ) or ( q in [:([#] T1),V1:] & not p in [:([#] T1),V1:] ) ) by A10, A5, A7, ZFMISC_1:87; ::_thesis: verum end; end; end; [:([#] T1),V1:] is open by A14, BORSUK_1:6; hence ex X being Subset of [:T1,T2:] st ( X is open & ( ( p in X & not q in X ) or ( q in X & not p in X ) ) ) by A16; ::_thesis: verum end; end; end; hence [:T1,T2:] is T_0 by T_0TOPSP:def_7; ::_thesis: verum end; end; end; end; registration let T1, T2 be T_1 TopSpace; cluster[:T1,T2:] -> T_1 ; coherence [:T1,T2:] is T_1 proof set T = [:T1,T2:]; percases ( T1 is empty or T2 is empty or ( not T1 is empty & not T2 is empty ) ) ; suppose ( T1 is empty or T2 is empty ) ; ::_thesis: [:T1,T2:] is T_1 hence [:T1,T2:] is T_1 ; ::_thesis: verum end; suppose ( not T1 is empty & not T2 is empty ) ; ::_thesis: [:T1,T2:] is T_1 then A1: not the carrier of [:T1,T2:] is empty ; let p, q be Point of [:T1,T2:]; :: according to URYSOHN1:def_7 ::_thesis: ( p = q or ex b1, b2 being Element of bool the carrier of [:T1,T2:] st ( b1 is open & b2 is open & p in b1 & not q in b1 & q in b2 & not p in b2 ) ) assume A2: p <> q ; ::_thesis: ex b1, b2 being Element of bool the carrier of [:T1,T2:] st ( b1 is open & b2 is open & p in b1 & not q in b1 & q in b2 & not p in b2 ) q in the carrier of [:T1,T2:] by A1; then q in [: the carrier of T1, the carrier of T2:] by BORSUK_1:def_2; then consider z, v being set such that A3: z in the carrier of T1 and A4: v in the carrier of T2 and A5: q = [z,v] by ZFMISC_1:def_2; p in the carrier of [:T1,T2:] by A1; then p in [: the carrier of T1, the carrier of T2:] by BORSUK_1:def_2; then consider x, y being set such that A6: x in the carrier of T1 and A7: y in the carrier of T2 and A8: p = [x,y] by ZFMISC_1:def_2; reconsider y = y, v = v as Point of T2 by A7, A4; reconsider x = x, z = z as Point of T1 by A6, A3; percases ( x <> z or x = z ) ; suppose x <> z ; ::_thesis: ex b1, b2 being Element of bool the carrier of [:T1,T2:] st ( b1 is open & b2 is open & p in b1 & not q in b1 & q in b2 & not p in b2 ) then consider Y, V being Subset of T1 such that A9: ( Y is open & V is open ) and A10: x in Y and A11: not z in Y and A12: z in V and A13: not x in V by URYSOHN1:def_7; set X = [:Y,([#] T2):]; set Z = [:V,([#] T2):]; A14: ( not q in [:Y,([#] T2):] & not p in [:V,([#] T2):] ) by A8, A5, A11, A13, ZFMISC_1:87; A15: ( [:Y,([#] T2):] is open & [:V,([#] T2):] is open ) by A9, BORSUK_1:6; ( p in [:Y,([#] T2):] & q in [:V,([#] T2):] ) by A7, A8, A4, A5, A10, A12, ZFMISC_1:87; hence ex b1, b2 being Element of bool the carrier of [:T1,T2:] st ( b1 is open & b2 is open & p in b1 & not q in b1 & q in b2 & not p in b2 ) by A15, A14; ::_thesis: verum end; suppose x = z ; ::_thesis: ex b1, b2 being Element of bool the carrier of [:T1,T2:] st ( b1 is open & b2 is open & p in b1 & not q in b1 & q in b2 & not p in b2 ) then consider Y, V being Subset of T2 such that A16: ( Y is open & V is open ) and A17: y in Y and A18: not v in Y and A19: v in V and A20: not y in V by A2, A8, A5, URYSOHN1:def_7; reconsider Y = Y, V = V as Subset of T2 ; set X = [:([#] T1),Y:]; set Z = [:([#] T1),V:]; A21: ( not p in [:([#] T1),V:] & not q in [:([#] T1),Y:] ) by A8, A5, A18, A20, ZFMISC_1:87; A22: ( [:([#] T1),Y:] is open & [:([#] T1),V:] is open ) by A16, BORSUK_1:6; ( p in [:([#] T1),Y:] & q in [:([#] T1),V:] ) by A6, A8, A3, A5, A17, A19, ZFMISC_1:87; hence ex b1, b2 being Element of bool the carrier of [:T1,T2:] st ( b1 is open & b2 is open & p in b1 & not q in b1 & q in b2 & not p in b2 ) by A22, A21; ::_thesis: verum end; end; end; end; end; end; registration let T1, T2 be T_2 TopSpace; cluster[:T1,T2:] -> T_2 ; coherence [:T1,T2:] is T_2 proof set T = [:T1,T2:]; percases ( T1 is empty or T2 is empty or ( not T1 is empty & not T2 is empty ) ) ; suppose ( T1 is empty or T2 is empty ) ; ::_thesis: [:T1,T2:] is T_2 hence [:T1,T2:] is T_2 ; ::_thesis: verum end; suppose ( not T1 is empty & not T2 is empty ) ; ::_thesis: [:T1,T2:] is T_2 then A1: not the carrier of [:T1,T2:] is empty ; let p, q be Point of [:T1,T2:]; :: according to PRE_TOPC:def_10 ::_thesis: ( p = q or ex b1, b2 being Element of bool the carrier of [:T1,T2:] st ( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) ) assume A2: p <> q ; ::_thesis: ex b1, b2 being Element of bool the carrier of [:T1,T2:] st ( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) q in the carrier of [:T1,T2:] by A1; then q in [: the carrier of T1, the carrier of T2:] by BORSUK_1:def_2; then consider z, v being set such that A3: z in the carrier of T1 and A4: v in the carrier of T2 and A5: q = [z,v] by ZFMISC_1:def_2; p in the carrier of [:T1,T2:] by A1; then p in [: the carrier of T1, the carrier of T2:] by BORSUK_1:def_2; then consider x, y being set such that A6: x in the carrier of T1 and A7: y in the carrier of T2 and A8: p = [x,y] by ZFMISC_1:def_2; reconsider y = y, v = v as Point of T2 by A7, A4; reconsider x = x, z = z as Point of T1 by A6, A3; percases ( x <> z or x = z ) ; suppose x <> z ; ::_thesis: ex b1, b2 being Element of bool the carrier of [:T1,T2:] st ( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) then consider Y, V being Subset of T1 such that A9: ( Y is open & V is open ) and A10: ( x in Y & z in V ) and A11: Y misses V by PRE_TOPC:def_10; reconsider Y = Y, V = V as Subset of T1 ; reconsider X = [:Y,([#] T2):], Z = [:V,([#] T2):] as Subset of [:T1,T2:] ; A12: X misses Z by A11, ZFMISC_1:104; A13: ( X is open & Z is open ) by A9, BORSUK_1:6; ( p in X & q in Z ) by A7, A8, A4, A5, A10, ZFMISC_1:87; hence ex b1, b2 being Element of bool the carrier of [:T1,T2:] st ( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) by A13, A12; ::_thesis: verum end; suppose x = z ; ::_thesis: ex b1, b2 being Element of bool the carrier of [:T1,T2:] st ( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) then consider Y, V being Subset of T2 such that A14: ( Y is open & V is open ) and A15: ( y in Y & v in V ) and A16: Y misses V by A2, A8, A5, PRE_TOPC:def_10; reconsider Y = Y, V = V as Subset of T2 ; reconsider X = [:([#] T1),Y:], Z = [:([#] T1),V:] as Subset of [:T1,T2:] ; A17: X misses Z by A16, ZFMISC_1:104; A18: ( X is open & Z is open ) by A14, BORSUK_1:6; ( p in X & q in Z ) by A6, A8, A3, A5, A15, ZFMISC_1:87; hence ex b1, b2 being Element of bool the carrier of [:T1,T2:] st ( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) by A18, A17; ::_thesis: verum end; end; end; end; end; end; registration cluster I[01] -> T_2 compact ; coherence ( I[01] is compact & I[01] is T_2 ) proof I[01] = TopSpaceMetr (Closed-Interval-MSpace (0,1)) by TOPMETR:20, TOPMETR:def_7; hence ( I[01] is compact & I[01] is T_2 ) by HEINE:4, PCOMPS_1:34, TOPMETR:20; ::_thesis: verum end; end; definition let T be non empty TopStruct ; let a, b be Point of T; let P, Q be Path of a,b; predP,Q are_homotopic means :: BORSUK_2:def 7 ex f being Function of [:I[01],I[01]:],T st ( f is continuous & ( for t being Point of I[01] holds ( f . (t,0) = P . t & f . (t,1) = Q . t & f . (0,t) = a & f . (1,t) = b ) ) ); symmetry for P, Q being Path of a,b st ex f being Function of [:I[01],I[01]:],T st ( f is continuous & ( for t being Point of I[01] holds ( f . (t,0) = P . t & f . (t,1) = Q . t & f . (0,t) = a & f . (1,t) = b ) ) ) holds ex f being Function of [:I[01],I[01]:],T st ( f is continuous & ( for t being Point of I[01] holds ( f . (t,0) = Q . t & f . (t,1) = P . t & f . (0,t) = a & f . (1,t) = b ) ) ) proof id the carrier of I[01] = id I[01] ; then reconsider fA = id the carrier of I[01] as continuous Function of I[01],I[01] ; set LL = L[01] (((0,1) (#)),((#) (0,1))); reconsider fB = L[01] (((0,1) (#)),((#) (0,1))) as continuous Function of I[01],I[01] by TOPMETR:20, TREAL_1:8; let P, Q be Path of a,b; ::_thesis: ( ex f being Function of [:I[01],I[01]:],T st ( f is continuous & ( for t being Point of I[01] holds ( f . (t,0) = P . t & f . (t,1) = Q . t & f . (0,t) = a & f . (1,t) = b ) ) ) implies ex f being Function of [:I[01],I[01]:],T st ( f is continuous & ( for t being Point of I[01] holds ( f . (t,0) = Q . t & f . (t,1) = P . t & f . (0,t) = a & f . (1,t) = b ) ) ) ) given f being Function of [:I[01],I[01]:],T such that A1: f is continuous and A2: for s being Point of I[01] holds ( f . (s,0) = P . s & f . (s,1) = Q . s & f . (0,s) = a & f . (1,s) = b ) ; ::_thesis: ex f being Function of [:I[01],I[01]:],T st ( f is continuous & ( for t being Point of I[01] holds ( f . (t,0) = Q . t & f . (t,1) = P . t & f . (0,t) = a & f . (1,t) = b ) ) ) set F = [:fA,fB:]; reconsider ff = f * [:fA,fB:] as Function of [:I[01],I[01]:],T ; A3: dom (L[01] (((0,1) (#)),((#) (0,1)))) = the carrier of I[01] by FUNCT_2:def_1, TOPMETR:20; A4: for s being Point of I[01] holds ( ff . (s,0) = Q . s & ff . (s,1) = P . s ) proof let s be Point of I[01]; ::_thesis: ( ff . (s,0) = Q . s & ff . (s,1) = P . s ) A5: for t being Point of I[01] for t9 being Real st t = t9 holds (L[01] (((0,1) (#)),((#) (0,1)))) . t = 1 - t9 proof let t be Point of I[01]; ::_thesis: for t9 being Real st t = t9 holds (L[01] (((0,1) (#)),((#) (0,1)))) . t = 1 - t9 let t9 be Real; ::_thesis: ( t = t9 implies (L[01] (((0,1) (#)),((#) (0,1)))) . t = 1 - t9 ) assume A6: t = t9 ; ::_thesis: (L[01] (((0,1) (#)),((#) (0,1)))) . t = 1 - t9 reconsider ee = t as Point of (Closed-Interval-TSpace (0,1)) by TOPMETR:20; A7: ( (0,1) (#) = 1 & (#) (0,1) = 0 ) by TREAL_1:def_1, TREAL_1:def_2; (L[01] (((0,1) (#)),((#) (0,1)))) . t = (L[01] (((0,1) (#)),((#) (0,1)))) . ee .= ((0 - 1) * t9) + 1 by A6, A7, TREAL_1:7 .= 1 - (1 * t9) ; hence (L[01] (((0,1) (#)),((#) (0,1)))) . t = 1 - t9 ; ::_thesis: verum end; A8: dom (id the carrier of I[01]) = the carrier of I[01] ; A9: dom [:fA,fB:] = [:(dom (id the carrier of I[01])),(dom (L[01] (((0,1) (#)),((#) (0,1))))):] by FUNCT_3:def_8; A10: 1 in dom (L[01] (((0,1) (#)),((#) (0,1)))) by A3, Lm1; then A11: [s,1] in dom [:fA,fB:] by A9, ZFMISC_1:87; A12: 0 in dom (L[01] (((0,1) (#)),((#) (0,1)))) by A3, Lm1; then A13: [s,0] in dom [:fA,fB:] by A9, ZFMISC_1:87; [:fA,fB:] . (s,1) = [((id the carrier of I[01]) . s),((L[01] (((0,1) (#)),((#) (0,1)))) . 1)] by A8, A10, FUNCT_3:def_8 .= [s,((L[01] (((0,1) (#)),((#) (0,1)))) . 1[01])] by FUNCT_1:18 .= [s,(1 - 1)] by A5 .= [s,0] ; then A14: ff . (s,1) = f . (s,0) by A11, FUNCT_1:13 .= P . s by A2 ; [:fA,fB:] . (s,0) = [((id the carrier of I[01]) . s),((L[01] (((0,1) (#)),((#) (0,1)))) . 0)] by A8, A12, FUNCT_3:def_8 .= [s,((L[01] (((0,1) (#)),((#) (0,1)))) . 0[01])] by FUNCT_1:18 .= [s,(1 - 0)] by A5 .= [s,1] ; then ff . (s,0) = f . (s,1) by A13, FUNCT_1:13 .= Q . s by A2 ; hence ( ff . (s,0) = Q . s & ff . (s,1) = P . s ) by A14; ::_thesis: verum end; A15: for t being Point of I[01] holds ( ff . (0,t) = a & ff . (1,t) = b ) proof let t be Point of I[01]; ::_thesis: ( ff . (0,t) = a & ff . (1,t) = b ) t in the carrier of I[01] ; then reconsider tt = t as Real by BORSUK_1:40; for t being Point of I[01] for t9 being Real st t = t9 holds (L[01] (((0,1) (#)),((#) (0,1)))) . t = 1 - t9 proof let t be Point of I[01]; ::_thesis: for t9 being Real st t = t9 holds (L[01] (((0,1) (#)),((#) (0,1)))) . t = 1 - t9 let t9 be Real; ::_thesis: ( t = t9 implies (L[01] (((0,1) (#)),((#) (0,1)))) . t = 1 - t9 ) assume A16: t = t9 ; ::_thesis: (L[01] (((0,1) (#)),((#) (0,1)))) . t = 1 - t9 reconsider ee = t as Point of (Closed-Interval-TSpace (0,1)) by TOPMETR:20; A17: ( (0,1) (#) = 1 & (#) (0,1) = 0 ) by TREAL_1:def_1, TREAL_1:def_2; (L[01] (((0,1) (#)),((#) (0,1)))) . t = (L[01] (((0,1) (#)),((#) (0,1)))) . ee .= ((0 - 1) * t9) + 1 by A16, A17, TREAL_1:7 .= 1 - (1 * t9) ; hence (L[01] (((0,1) (#)),((#) (0,1)))) . t = 1 - t9 ; ::_thesis: verum end; then A18: (L[01] (((0,1) (#)),((#) (0,1)))) . t = 1 - tt ; reconsider t9 = 1 - tt as Point of I[01] by Lm5; A19: dom (L[01] (((0,1) (#)),((#) (0,1)))) = the carrier of I[01] by FUNCT_2:def_1, TOPMETR:20; A20: 0 in dom (id the carrier of I[01]) by Lm1; A21: dom [:fA,fB:] = [:(dom (id the carrier of I[01])),(dom (L[01] (((0,1) (#)),((#) (0,1))))):] by FUNCT_3:def_8; then A22: [0,t] in dom [:fA,fB:] by A19, A20, ZFMISC_1:87; A23: 1 in dom (id the carrier of I[01]) by Lm1; then A24: [1,t] in dom [:fA,fB:] by A19, A21, ZFMISC_1:87; [:fA,fB:] . (1,t) = [((id the carrier of I[01]) . 1),((L[01] (((0,1) (#)),((#) (0,1)))) . t)] by A19, A23, FUNCT_3:def_8 .= [1,(1 - tt)] by A18, A23, FUNCT_1:18 ; then A25: ff . (1,t) = f . (1,t9) by A24, FUNCT_1:13 .= b by A2 ; [:fA,fB:] . (0,t) = [((id the carrier of I[01]) . 0),((L[01] (((0,1) (#)),((#) (0,1)))) . t)] by A19, A20, FUNCT_3:def_8 .= [0,(1 - tt)] by A18, A20, FUNCT_1:18 ; then ff . (0,t) = f . (0,t9) by A22, FUNCT_1:13 .= a by A2 ; hence ( ff . (0,t) = a & ff . (1,t) = b ) by A25; ::_thesis: verum end; ff is continuous by A1, TOPS_2:46; hence ex f being Function of [:I[01],I[01]:],T st ( f is continuous & ( for t being Point of I[01] holds ( f . (t,0) = Q . t & f . (t,1) = P . t & f . (0,t) = a & f . (1,t) = b ) ) ) by A4, A15; ::_thesis: verum end; end; :: deftheorem defines are_homotopic BORSUK_2:def_7_:_ for T being non empty TopStruct for a, b being Point of T for P, Q being Path of a,b holds ( P,Q are_homotopic iff ex f being Function of [:I[01],I[01]:],T st ( f is continuous & ( for t being Point of I[01] holds ( f . (t,0) = P . t & f . (t,1) = Q . t & f . (0,t) = a & f . (1,t) = b ) ) ) ); theorem :: BORSUK_2:11 canceled; theorem Th12: :: BORSUK_2:12 for T being non empty TopSpace for a, b being Point of T for P being Path of a,b st a,b are_connected holds P,P are_homotopic proof let T be non empty TopSpace; ::_thesis: for a, b being Point of T for P being Path of a,b st a,b are_connected holds P,P are_homotopic let a, b be Point of T; ::_thesis: for P being Path of a,b st a,b are_connected holds P,P are_homotopic let P be Path of a,b; ::_thesis: ( a,b are_connected implies P,P are_homotopic ) defpred S1[ set , set ] means $2 = P . ($1 `1); A1: for x being set st x in [: the carrier of I[01], the carrier of I[01]:] holds ex y being set st ( y in the carrier of T & S1[x,y] ) proof let x be set ; ::_thesis: ( x in [: the carrier of I[01], the carrier of I[01]:] implies ex y being set st ( y in the carrier of T & S1[x,y] ) ) assume x in [: the carrier of I[01], the carrier of I[01]:] ; ::_thesis: ex y being set st ( y in the carrier of T & S1[x,y] ) then x `1 in the carrier of I[01] by MCART_1:10; hence ex y being set st ( y in the carrier of T & S1[x,y] ) by FUNCT_2:5; ::_thesis: verum end; consider f being Function of [: the carrier of I[01], the carrier of I[01]:], the carrier of T such that A2: for x being set st x in [: the carrier of I[01], the carrier of I[01]:] holds S1[x,f . x] from FUNCT_2:sch_1(A1); the carrier of [:I[01],I[01]:] = [: the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def_2; then reconsider f = f as Function of the carrier of [:I[01],I[01]:], the carrier of T ; reconsider f = f as Function of [:I[01],I[01]:],T ; assume A3: a,b are_connected ; ::_thesis: P,P are_homotopic A4: for t being Point of I[01] holds ( f . (0,t) = a & f . (1,t) = b ) proof let t be Point of I[01]; ::_thesis: ( f . (0,t) = a & f . (1,t) = b ) set t0 = [0,t]; set t1 = [1,t]; 0 in the carrier of I[01] by Lm1; then [0,t] in [: the carrier of I[01], the carrier of I[01]:] by ZFMISC_1:87; then A5: f . [0,t] = P . ([0,t] `1) by A2; 1 in the carrier of I[01] by Lm1; then [1,t] in [: the carrier of I[01], the carrier of I[01]:] by ZFMISC_1:87; then A6: f . [1,t] = P . ([1,t] `1) by A2; ( P . 0 = a & P . 1 = b ) by A3, Def2; hence ( f . (0,t) = a & f . (1,t) = b ) by A5, A6; ::_thesis: verum end; A7: for W being Point of [:I[01],I[01]:] for G being a_neighborhood of f . W ex H being a_neighborhood of W st f .: H c= G proof let W be Point of [:I[01],I[01]:]; ::_thesis: for G being a_neighborhood of f . W ex H being a_neighborhood of W st f .: H c= G let G be a_neighborhood of f . W; ::_thesis: ex H being a_neighborhood of W st f .: H c= G W in the carrier of [:I[01],I[01]:] ; then A8: W in [: the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def_2; then reconsider W1 = W `1 as Point of I[01] by MCART_1:10; A9: ex x, y being set st [x,y] = W by A8, RELAT_1:def_1; reconsider G9 = G as a_neighborhood of P . W1 by A2, A8; the carrier of I[01] c= the carrier of I[01] ; then reconsider AI = the carrier of I[01] as Subset of I[01] ; AI = [#] I[01] ; then Int AI = the carrier of I[01] by TOPS_1:15; then A10: W `2 in Int AI by A8, MCART_1:10; P is continuous by A3, Def2; then consider H being a_neighborhood of W1 such that A11: P .: H c= G9 by BORSUK_1:def_1; set HH = [:H, the carrier of I[01]:]; [:H, the carrier of I[01]:] c= [: the carrier of I[01], the carrier of I[01]:] by ZFMISC_1:95; then reconsider HH = [:H, the carrier of I[01]:] as Subset of [:I[01],I[01]:] by BORSUK_1:def_2; ( W1 in Int H & Int HH = [:(Int H),(Int AI):] ) by BORSUK_1:7, CONNSP_2:def_1; then W in Int HH by A9, A10, MCART_1:11; then reconsider HH = HH as a_neighborhood of W by CONNSP_2:def_1; take HH ; ::_thesis: f .: HH c= G f .: HH c= G proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in f .: HH or a in G ) assume a in f .: HH ; ::_thesis: a in G then consider b being set such that A12: b in dom f and A13: b in HH and A14: a = f . b by FUNCT_1:def_6; reconsider b = b as Point of [:I[01],I[01]:] by A12; A15: ( dom P = the carrier of I[01] & b `1 in H ) by A13, FUNCT_2:def_1, MCART_1:10; dom f = [: the carrier of I[01], the carrier of I[01]:] by FUNCT_2:def_1; then f . b = P . (b `1) by A2, A12; then f . b in P .: H by A15, FUNCT_1:def_6; hence a in G by A11, A14; ::_thesis: verum end; hence f .: HH c= G ; ::_thesis: verum end; take f ; :: according to BORSUK_2:def_7 ::_thesis: ( f is continuous & ( for t being Point of I[01] holds ( f . (t,0) = P . t & f . (t,1) = P . t & f . (0,t) = a & f . (1,t) = b ) ) ) for s being Point of I[01] holds ( f . (s,0) = P . s & f . (s,1) = P . s ) proof let s be Point of I[01]; ::_thesis: ( f . (s,0) = P . s & f . (s,1) = P . s ) reconsider s0 = [s,0], s1 = [s,1] as set ; 1 in the carrier of I[01] by Lm1; then s1 in [: the carrier of I[01], the carrier of I[01]:] by ZFMISC_1:87; then A16: S1[s1,f . s1] by A2; 0 in the carrier of I[01] by Lm1; then s0 in [: the carrier of I[01], the carrier of I[01]:] by ZFMISC_1:87; then S1[s0,f . s0] by A2; hence ( f . (s,0) = P . s & f . (s,1) = P . s ) by A16, MCART_1:7; ::_thesis: verum end; hence ( f is continuous & ( for t being Point of I[01] holds ( f . (t,0) = P . t & f . (t,1) = P . t & f . (0,t) = a & f . (1,t) = b ) ) ) by A7, A4, BORSUK_1:def_1; ::_thesis: verum end; definition let T be non empty pathwise_connected TopSpace; let a, b be Point of T; let P, Q be Path of a,b; :: original: are_homotopic redefine predP,Q are_homotopic ; reflexivity for P being Path of a,b holds (T,a,b,b1,b1) proof a,b are_connected by Def3; hence for P being Path of a,b holds (T,a,b,b1,b1) by Th12; ::_thesis: verum end; end; theorem :: BORSUK_2:13 for G being non empty TopSpace for w1, w2, w3 being Point of G for h1, h2 being Function of I[01],G st h1 is continuous & w1 = h1 . 0 & w2 = h1 . 1 & h2 is continuous & w2 = h2 . 0 & w3 = h2 . 1 holds ex h3 being Function of I[01],G st ( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 & rng h3 c= (rng h1) \/ (rng h2) ) by Lm3; theorem :: BORSUK_2:14 for T being non empty TopSpace for a, b, c being Point of T for G1 being Path of a,b for G2 being Path of b,c st G1 is continuous & G2 is continuous & G1 . 0 = a & G1 . 1 = b & G2 . 0 = b & G2 . 1 = c holds ( G1 + G2 is continuous & (G1 + G2) . 0 = a & (G1 + G2) . 1 = c ) proof let T be non empty TopSpace; ::_thesis: for a, b, c being Point of T for G1 being Path of a,b for G2 being Path of b,c st G1 is continuous & G2 is continuous & G1 . 0 = a & G1 . 1 = b & G2 . 0 = b & G2 . 1 = c holds ( G1 + G2 is continuous & (G1 + G2) . 0 = a & (G1 + G2) . 1 = c ) let a, b, c be Point of T; ::_thesis: for G1 being Path of a,b for G2 being Path of b,c st G1 is continuous & G2 is continuous & G1 . 0 = a & G1 . 1 = b & G2 . 0 = b & G2 . 1 = c holds ( G1 + G2 is continuous & (G1 + G2) . 0 = a & (G1 + G2) . 1 = c ) let G1 be Path of a,b; ::_thesis: for G2 being Path of b,c st G1 is continuous & G2 is continuous & G1 . 0 = a & G1 . 1 = b & G2 . 0 = b & G2 . 1 = c holds ( G1 + G2 is continuous & (G1 + G2) . 0 = a & (G1 + G2) . 1 = c ) let G2 be Path of b,c; ::_thesis: ( G1 is continuous & G2 is continuous & G1 . 0 = a & G1 . 1 = b & G2 . 0 = b & G2 . 1 = c implies ( G1 + G2 is continuous & (G1 + G2) . 0 = a & (G1 + G2) . 1 = c ) ) assume ( G1 is continuous & G2 is continuous & G1 . 0 = a & G1 . 1 = b & G2 . 0 = b & G2 . 1 = c ) ; ::_thesis: ( G1 + G2 is continuous & (G1 + G2) . 0 = a & (G1 + G2) . 1 = c ) then ex h being Function of I[01],T st ( h is continuous & h . 0 = a & h . 1 = c & rng h c= (rng G1) \/ (rng G2) ) by Lm3; then a,c are_connected by Def1; hence ( G1 + G2 is continuous & (G1 + G2) . 0 = a & (G1 + G2) . 1 = c ) by Def2; ::_thesis: verum end; registration let T be non empty TopSpace; cluster non empty connected compact for Element of bool the carrier of T; existence ex b1 being Subset of T st ( not b1 is empty & b1 is compact & b1 is connected ) proof take { the Element of T} ; ::_thesis: ( not { the Element of T} is empty & { the Element of T} is compact & { the Element of T} is connected ) thus ( not { the Element of T} is empty & { the Element of T} is compact & { the Element of T} is connected ) ; ::_thesis: verum end; end; theorem Th15: :: BORSUK_2:15 for T being non empty TopSpace for a, b being Point of T st ex f being Function of I[01],T st ( f is continuous & f . 0 = a & f . 1 = b ) holds ex g being Function of I[01],T st ( g is continuous & g . 0 = b & g . 1 = a ) proof set e = L[01] (((0,1) (#)),((#) (0,1))); let T be non empty TopSpace; ::_thesis: for a, b being Point of T st ex f being Function of I[01],T st ( f is continuous & f . 0 = a & f . 1 = b ) holds ex g being Function of I[01],T st ( g is continuous & g . 0 = b & g . 1 = a ) let a, b be Point of T; ::_thesis: ( ex f being Function of I[01],T st ( f is continuous & f . 0 = a & f . 1 = b ) implies ex g being Function of I[01],T st ( g is continuous & g . 0 = b & g . 1 = a ) ) given P being Function of I[01],T such that A1: P is continuous and A2: ( P . 0 = a & P . 1 = b ) ; ::_thesis: ex g being Function of I[01],T st ( g is continuous & g . 0 = b & g . 1 = a ) set f = P * (L[01] (((0,1) (#)),((#) (0,1)))); reconsider f = P * (L[01] (((0,1) (#)),((#) (0,1)))) as Function of I[01],T by TOPMETR:20; take f ; ::_thesis: ( f is continuous & f . 0 = b & f . 1 = a ) L[01] (((0,1) (#)),((#) (0,1))) is continuous Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (0,1)) by TREAL_1:8; hence f is continuous by A1, TOPMETR:20; ::_thesis: ( f . 0 = b & f . 1 = a ) A3: (L[01] (((0,1) (#)),((#) (0,1)))) . 1 = (L[01] (((0,1) (#)),((#) (0,1)))) . ((0,1) (#)) by TREAL_1:def_2 .= (#) (0,1) by TREAL_1:9 .= 0 by TREAL_1:def_1 ; 1 in [.0,1.] by XXREAL_1:1; then 1 in the carrier of (Closed-Interval-TSpace (0,1)) by TOPMETR:18; then A4: 1 in dom (L[01] (((0,1) (#)),((#) (0,1)))) by FUNCT_2:def_1; 0 in [.0,1.] by XXREAL_1:1; then 0 in the carrier of (Closed-Interval-TSpace (0,1)) by TOPMETR:18; then A5: 0 in dom (L[01] (((0,1) (#)),((#) (0,1)))) by FUNCT_2:def_1; (L[01] (((0,1) (#)),((#) (0,1)))) . 0 = (L[01] (((0,1) (#)),((#) (0,1)))) . ((#) (0,1)) by TREAL_1:def_1 .= (0,1) (#) by TREAL_1:9 .= 1 by TREAL_1:def_2 ; hence ( f . 0 = b & f . 1 = a ) by A2, A3, A5, A4, FUNCT_1:13; ::_thesis: verum end; registration cluster I[01] -> pathwise_connected ; coherence I[01] is pathwise_connected proof let a, b be Point of I[01]; :: according to BORSUK_2:def_3 ::_thesis: a,b are_connected percases ( a <= b or b <= a ) ; supposeA1: a <= b ; ::_thesis: a,b are_connected then reconsider B = [.a,b.] as non empty Subset of I[01] by BORSUK_1:40, XXREAL_1:1, XXREAL_2:def_12; ( 0 <= a & b <= 1 ) by BORSUK_1:43; then A2: Closed-Interval-TSpace (a,b) = I[01] | B by A1, TOPMETR:24; the carrier of (I[01] | B) c= the carrier of I[01] by BORSUK_1:1; then reconsider g = L[01] (((#) (a,b)),((a,b) (#))) as Function of the carrier of I[01], the carrier of I[01] by A2, FUNCT_2:7, TOPMETR:20; reconsider g = g as Function of I[01],I[01] ; take g ; :: according to BORSUK_2:def_1 ::_thesis: ( g is continuous & g . 0 = a & g . 1 = b ) thus g is continuous by PRE_TOPC:26, A1, A2, TOPMETR:20, TREAL_1:8; ::_thesis: ( g . 0 = a & g . 1 = b ) 0 = (#) (0,1) by TREAL_1:def_1; hence g . 0 = (#) (a,b) by A1, TREAL_1:9 .= a by A1, TREAL_1:def_1 ; ::_thesis: g . 1 = b 1 = (0,1) (#) by TREAL_1:def_2; hence g . 1 = (a,b) (#) by A1, TREAL_1:9 .= b by A1, TREAL_1:def_2 ; ::_thesis: verum end; supposeA3: b <= a ; ::_thesis: a,b are_connected then reconsider B = [.b,a.] as non empty Subset of I[01] by BORSUK_1:40, XXREAL_1:1, XXREAL_2:def_12; ( 0 <= b & a <= 1 ) by BORSUK_1:43; then A4: Closed-Interval-TSpace (b,a) = I[01] | B by A3, TOPMETR:24; the carrier of (I[01] | B) c= the carrier of I[01] by BORSUK_1:1; then reconsider g = L[01] (((#) (b,a)),((b,a) (#))) as Function of the carrier of I[01], the carrier of I[01] by A4, FUNCT_2:7, TOPMETR:20; reconsider g = g as Function of I[01],I[01] ; 0 = (#) (0,1) by TREAL_1:def_1; then A5: g . 0 = (#) (b,a) by A3, TREAL_1:9 .= b by A3, TREAL_1:def_1 ; 1 = (0,1) (#) by TREAL_1:def_2; then A6: g . 1 = (b,a) (#) by A3, TREAL_1:9 .= a by A3, TREAL_1:def_2 ; A7: g is continuous by PRE_TOPC:26, A3, A4, TOPMETR:20, TREAL_1:8; then b,a are_connected by A5, A6, Def1; then reconsider P = g as Path of b,a by A7, A5, A6, Def2; take - P ; :: according to BORSUK_2:def_1 ::_thesis: ( - P is continuous & (- P) . 0 = a & (- P) . 1 = b ) ex t being Function of I[01],I[01] st ( t is continuous & t . 0 = a & t . 1 = b ) by A7, A5, A6, Th15; then a,b are_connected by Def1; hence ( - P is continuous & (- P) . 0 = a & (- P) . 1 = b ) by Def2; ::_thesis: verum end; end; end; end;