:: TOPALG_1 semantic presentation begin theorem :: TOPALG_1:1 for G, H being set for g being Function of G,H for h being Function of H,G st h * g = id G & g * h = id H holds h is bijective proof let G, H be set ; ::_thesis: for g being Function of G,H for h being Function of H,G st h * g = id G & g * h = id H holds h is bijective let g be Function of G,H; ::_thesis: for h being Function of H,G st h * g = id G & g * h = id H holds h is bijective let h be Function of H,G; ::_thesis: ( h * g = id G & g * h = id H implies h is bijective ) assume ( h * g = id G & g * h = id H ) ; ::_thesis: h is bijective then ( h is one-to-one & h is onto ) by FUNCT_2:23; hence h is bijective ; ::_thesis: verum end; theorem Th2: :: TOPALG_1:2 for X being Subset of I[01] for a being Point of I[01] st X = ].a,1.] holds X ` = [.0,a.] proof set I = the carrier of I[01]; let X be Subset of I[01]; ::_thesis: for a being Point of I[01] st X = ].a,1.] holds X ` = [.0,a.] let a be Point of I[01]; ::_thesis: ( X = ].a,1.] implies X ` = [.0,a.] ) assume A1: X = ].a,1.] ; ::_thesis: X ` = [.0,a.] set Y = [.0,a.]; A2: X ` = the carrier of I[01] \ X by SUBSET_1:def_4; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: [.0,a.] c= X ` let x be set ; ::_thesis: ( x in X ` implies x in [.0,a.] ) assume A3: x in X ` ; ::_thesis: x in [.0,a.] then reconsider y = x as Point of I[01] ; not x in X by A2, A3, XBOOLE_0:def_5; then A4: ( y <= a or y > 1 ) by A1, XXREAL_1:2; 0 <= y by BORSUK_1:43; hence x in [.0,a.] by A4, BORSUK_1:43, XXREAL_1:1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [.0,a.] or x in X ` ) assume A5: x in [.0,a.] ; ::_thesis: x in X ` then reconsider y = x as Real ; A6: 0 <= y by A5, XXREAL_1:1; A7: y <= a by A5, XXREAL_1:1; a <= 1 by BORSUK_1:43; then y <= 1 by A7, XXREAL_0:2; then A8: y in the carrier of I[01] by A6, BORSUK_1:43; not y in X by A1, A7, XXREAL_1:2; hence x in X ` by A2, A8, XBOOLE_0:def_5; ::_thesis: verum end; theorem Th3: :: TOPALG_1:3 for X being Subset of I[01] for a being Point of I[01] st X = [.0,a.[ holds X ` = [.a,1.] proof set I = the carrier of I[01]; let X be Subset of I[01]; ::_thesis: for a being Point of I[01] st X = [.0,a.[ holds X ` = [.a,1.] let a be Point of I[01]; ::_thesis: ( X = [.0,a.[ implies X ` = [.a,1.] ) assume A1: X = [.0,a.[ ; ::_thesis: X ` = [.a,1.] set Y = [.a,1.]; A2: X ` = the carrier of I[01] \ X by SUBSET_1:def_4; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: [.a,1.] c= X ` let x be set ; ::_thesis: ( x in X ` implies x in [.a,1.] ) assume A3: x in X ` ; ::_thesis: x in [.a,1.] then reconsider y = x as Point of I[01] ; not x in X by A2, A3, XBOOLE_0:def_5; then A4: ( y >= a or y < 0 ) by A1, XXREAL_1:3; y <= 1 by BORSUK_1:43; hence x in [.a,1.] by A4, BORSUK_1:43, XXREAL_1:1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [.a,1.] or x in X ` ) assume A5: x in [.a,1.] ; ::_thesis: x in X ` then reconsider y = x as Real ; A6: a <= y by A5, XXREAL_1:1; then A7: not y in X by A1, XXREAL_1:3; A8: 0 <= a by BORSUK_1:43; y <= 1 by A5, XXREAL_1:1; then y in the carrier of I[01] by A6, A8, BORSUK_1:43; hence x in X ` by A2, A7, XBOOLE_0:def_5; ::_thesis: verum end; theorem Th4: :: TOPALG_1:4 for X being Subset of I[01] for a being Point of I[01] st X = ].a,1.] holds X is open proof let X be Subset of I[01]; ::_thesis: for a being Point of I[01] st X = ].a,1.] holds X is open let a be Point of I[01]; ::_thesis: ( X = ].a,1.] implies X is open ) assume A1: X = ].a,1.] ; ::_thesis: X is open set Y = [.0,a.]; [.0,a.] c= the carrier of I[01] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [.0,a.] or x in the carrier of I[01] ) A2: a <= 1 by BORSUK_1:43; assume A3: x in [.0,a.] ; ::_thesis: x in the carrier of I[01] then reconsider x = x as Real ; A4: 0 <= x by A3, XXREAL_1:1; x <= a by A3, XXREAL_1:1; then x <= 1 by A2, XXREAL_0:2; hence x in the carrier of I[01] by A4, BORSUK_1:43; ::_thesis: verum end; then reconsider Y = [.0,a.] as Subset of I[01] ; ( Y is closed & X ` = Y ) by A1, Th2, BORSUK_4:23; hence X is open by TOPS_1:4; ::_thesis: verum end; theorem Th5: :: TOPALG_1:5 for X being Subset of I[01] for a being Point of I[01] st X = [.0,a.[ holds X is open proof let X be Subset of I[01]; ::_thesis: for a being Point of I[01] st X = [.0,a.[ holds X is open let a be Point of I[01]; ::_thesis: ( X = [.0,a.[ implies X is open ) assume A1: X = [.0,a.[ ; ::_thesis: X is open set Y = [.a,1.]; [.a,1.] c= the carrier of I[01] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [.a,1.] or x in the carrier of I[01] ) A2: 0 <= a by BORSUK_1:43; assume A3: x in [.a,1.] ; ::_thesis: x in the carrier of I[01] then reconsider x = x as Real ; ( x <= 1 & a <= x ) by A3, XXREAL_1:1; hence x in the carrier of I[01] by A2, BORSUK_1:43; ::_thesis: verum end; then reconsider Y = [.a,1.] as Subset of I[01] ; ( Y is closed & X ` = Y ) by A1, Th3, BORSUK_4:23; hence X is open by TOPS_1:4; ::_thesis: verum end; theorem :: TOPALG_1:6 for x being real number for f being real-valued FinSequence holds x * (- f) = - (x * f) proof let x be real number ; ::_thesis: for f being real-valued FinSequence holds x * (- f) = - (x * f) let f be real-valued FinSequence; ::_thesis: x * (- f) = - (x * f) thus x * (- f) = x * ((- 1) * f) .= ((- 1) * x) * f by RVSUM_1:49 .= - (x * f) by RVSUM_1:49 ; ::_thesis: verum end; theorem Th7: :: TOPALG_1:7 for x being real number for f, g being real-valued FinSequence holds x * (f - g) = (x * f) - (x * g) by RFUNCT_1:18; theorem Th8: :: TOPALG_1:8 for x, y being real number for f being real-valued FinSequence holds (x - y) * f = (x * f) - (y * f) proof let x, y be real number ; ::_thesis: for f being real-valued FinSequence holds (x - y) * f = (x * f) - (y * f) let f be real-valued FinSequence; ::_thesis: (x - y) * f = (x * f) - (y * f) A1: dom ((x - y) * f) = dom f by VALUED_1:def_5; A2: dom ((x * f) - (y * f)) = (dom (x * f)) /\ (dom (y * f)) by VALUED_1:12; A3: dom (x * f) = dom f by VALUED_1:def_5; A4: dom (y * f) = dom f by VALUED_1:def_5; now__::_thesis:_for_n_being_Nat_st_n_in_dom_((x_-_y)_*_f)_holds_ ((x_-_y)_*_f)_._n_=_((x_*_f)_-_(y_*_f))_._n let n be Nat; ::_thesis: ( n in dom ((x - y) * f) implies ((x - y) * f) . n = ((x * f) - (y * f)) . n ) assume A5: n in dom ((x - y) * f) ; ::_thesis: ((x - y) * f) . n = ((x * f) - (y * f)) . n thus ((x - y) * f) . n = (x - y) * (f . n) by VALUED_1:6 .= (x * (f . n)) - (y * (f . n)) .= (x * (f . n)) - ((y * f) . n) by VALUED_1:6 .= ((x * f) . n) - ((y * f) . n) by VALUED_1:6 .= ((x * f) - (y * f)) . n by A1, A2, A3, A4, A5, VALUED_1:13 ; ::_thesis: verum end; hence (x - y) * f = (x * f) - (y * f) by A1, A2, A3, A4, FINSEQ_1:13; ::_thesis: verum end; theorem Th9: :: TOPALG_1:9 for f, g, h, k being real-valued FinSequence holds (f + g) - (h + k) = (f - h) + (g - k) proof let f, g, h, k be real-valued FinSequence; ::_thesis: (f + g) - (h + k) = (f - h) + (g - k) thus (f + g) - (h + k) = f + (g + (- (h + k))) by RVSUM_1:15 .= f + (g + ((- h) + (- k))) by RVSUM_1:26 .= f + ((- h) + (g + (- k))) by RVSUM_1:15 .= (f + (- h)) + (g + (- k)) by RVSUM_1:15 .= (f - h) + (g + (- k)) .= (f - h) + (g - k) ; ::_thesis: verum end; theorem Th10: :: TOPALG_1:10 for x being real number for n being Nat for f being Element of REAL n st 0 <= x & x <= 1 holds |.(x * f).| <= |.f.| proof let x be real number ; ::_thesis: for n being Nat for f being Element of REAL n st 0 <= x & x <= 1 holds |.(x * f).| <= |.f.| let n be Nat; ::_thesis: for f being Element of REAL n st 0 <= x & x <= 1 holds |.(x * f).| <= |.f.| let f be Element of REAL n; ::_thesis: ( 0 <= x & x <= 1 implies |.(x * f).| <= |.f.| ) assume that A1: 0 <= x and A2: x <= 1 ; ::_thesis: |.(x * f).| <= |.f.| ( |.(x * f).| = (abs x) * |.f.| & x = abs x ) by A1, ABSVALUE:def_1, EUCLID:11; then |.(x * f).| <= 1 * |.f.| by A1, A2, XREAL_1:66; hence |.(x * f).| <= |.f.| ; ::_thesis: verum end; theorem :: TOPALG_1:11 for n being Nat for f being Element of REAL n for p being Point of I[01] holds |.(p * f).| <= |.f.| proof let n be Nat; ::_thesis: for f being Element of REAL n for p being Point of I[01] holds |.(p * f).| <= |.f.| let f be Element of REAL n; ::_thesis: for p being Point of I[01] holds |.(p * f).| <= |.f.| let p be Point of I[01]; ::_thesis: |.(p * f).| <= |.f.| ( [.0,1.] = { r where r is Real : ( 0 <= r & r <= 1 ) } & p in the carrier of I[01] ) by RCOMP_1:def_1; then ex r being Real st ( r = p & 0 <= r & r <= 1 ) by BORSUK_1:40; hence |.(p * f).| <= |.f.| by Th10; ::_thesis: verum end; theorem :: TOPALG_1:12 for x, y being real number for n being Nat for e1, e2, e3, e4, e5, e6 being Point of (Euclid n) for p1, p2, p3, p4 being Point of (TOP-REAL n) st e1 = p1 & e2 = p2 & e3 = p3 & e4 = p4 & e5 = p1 + p3 & e6 = p2 + p4 & dist (e1,e2) < x & dist (e3,e4) < y holds dist (e5,e6) < x + y proof let x, y be real number ; ::_thesis: for n being Nat for e1, e2, e3, e4, e5, e6 being Point of (Euclid n) for p1, p2, p3, p4 being Point of (TOP-REAL n) st e1 = p1 & e2 = p2 & e3 = p3 & e4 = p4 & e5 = p1 + p3 & e6 = p2 + p4 & dist (e1,e2) < x & dist (e3,e4) < y holds dist (e5,e6) < x + y let n be Nat; ::_thesis: for e1, e2, e3, e4, e5, e6 being Point of (Euclid n) for p1, p2, p3, p4 being Point of (TOP-REAL n) st e1 = p1 & e2 = p2 & e3 = p3 & e4 = p4 & e5 = p1 + p3 & e6 = p2 + p4 & dist (e1,e2) < x & dist (e3,e4) < y holds dist (e5,e6) < x + y let e1, e2, e3, e4, e5, e6 be Point of (Euclid n); ::_thesis: for p1, p2, p3, p4 being Point of (TOP-REAL n) st e1 = p1 & e2 = p2 & e3 = p3 & e4 = p4 & e5 = p1 + p3 & e6 = p2 + p4 & dist (e1,e2) < x & dist (e3,e4) < y holds dist (e5,e6) < x + y let p1, p2, p3, p4 be Point of (TOP-REAL n); ::_thesis: ( e1 = p1 & e2 = p2 & e3 = p3 & e4 = p4 & e5 = p1 + p3 & e6 = p2 + p4 & dist (e1,e2) < x & dist (e3,e4) < y implies dist (e5,e6) < x + y ) assume that A1: e1 = p1 and A2: e2 = p2 and A3: e3 = p3 and A4: e4 = p4 and A5: e5 = p1 + p3 and A6: e6 = p2 + p4 and A7: ( dist (e1,e2) < x & dist (e3,e4) < y ) ; ::_thesis: dist (e5,e6) < x + y reconsider f1 = e1, f2 = e2, f3 = e3, f4 = e4, f5 = e5, f6 = e6 as Element of REAL n by A1, A2, A3, A4, A5, A6, EUCLID:22; A8: ( |.((f1 - f2) + (f3 - f4)).| <= |.(f1 - f2).| + |.(f3 - f4).| & (dist (e1,e2)) + (dist (e3,e4)) < x + y ) by A7, EUCLID:12, XREAL_1:8; reconsider u1 = f1, u2 = f2, u3 = f3, u4 = f4, u6 = f6 as Element of n -tuples_on REAL by EUCLID:def_1; u2 + u4 = u6 by A2, A4, A6; then A9: (f1 + f3) - f6 = (u1 - u2) + (u3 - u4) by Th9 .= (f1 - f2) + (f3 - f4) ; A10: n in NAT by ORDINAL1:def_12; then A11: ( dist (e1,e2) = |.(f1 - f2).| & dist (e3,e4) = |.(f3 - f4).| ) by SPPOL_1:5; dist (e5,e6) = |.(f5 - f6).| by A10, SPPOL_1:5 .= |.((f1 - f2) + (f3 - f4)).| by A1, A3, A5, A9 ; hence dist (e5,e6) < x + y by A11, A8, XXREAL_0:2; ::_thesis: verum end; theorem Th13: :: TOPALG_1:13 for y, x being real number for n being Nat for e1, e2, e5, e6 being Point of (Euclid n) for p1, p2 being Point of (TOP-REAL n) st e1 = p1 & e2 = p2 & e5 = y * p1 & e6 = y * p2 & dist (e1,e2) < x & y <> 0 holds dist (e5,e6) < (abs y) * x proof let y, x be real number ; ::_thesis: for n being Nat for e1, e2, e5, e6 being Point of (Euclid n) for p1, p2 being Point of (TOP-REAL n) st e1 = p1 & e2 = p2 & e5 = y * p1 & e6 = y * p2 & dist (e1,e2) < x & y <> 0 holds dist (e5,e6) < (abs y) * x let n be Nat; ::_thesis: for e1, e2, e5, e6 being Point of (Euclid n) for p1, p2 being Point of (TOP-REAL n) st e1 = p1 & e2 = p2 & e5 = y * p1 & e6 = y * p2 & dist (e1,e2) < x & y <> 0 holds dist (e5,e6) < (abs y) * x let e1, e2, e5, e6 be Point of (Euclid n); ::_thesis: for p1, p2 being Point of (TOP-REAL n) st e1 = p1 & e2 = p2 & e5 = y * p1 & e6 = y * p2 & dist (e1,e2) < x & y <> 0 holds dist (e5,e6) < (abs y) * x let p1, p2 be Point of (TOP-REAL n); ::_thesis: ( e1 = p1 & e2 = p2 & e5 = y * p1 & e6 = y * p2 & dist (e1,e2) < x & y <> 0 implies dist (e5,e6) < (abs y) * x ) assume that A1: e1 = p1 and A2: e2 = p2 and A3: e5 = y * p1 and A4: e6 = y * p2 and A5: dist (e1,e2) < x and A6: y <> 0 ; ::_thesis: dist (e5,e6) < (abs y) * x reconsider f1 = e1, f2 = e2, f5 = e5, f6 = e6 as Element of REAL n by A1, A2, A3, A4, EUCLID:22; A7: n in NAT by ORDINAL1:def_12; then A8: dist (e1,e2) = |.(f1 - f2).| by SPPOL_1:5; A9: 0 < abs y by A6, COMPLEX1:47; dist (e5,e6) = |.(f5 - f6).| by A7, SPPOL_1:5 .= |.((y * f1) - f6).| by A1, A3 .= |.((y * f1) - (y * f2)).| by A2, A4 .= |.(y * (f1 - f2)).| by Th7 .= (abs y) * |.(f1 - f2).| by EUCLID:11 ; hence dist (e5,e6) < (abs y) * x by A5, A8, A9, XREAL_1:68; ::_thesis: verum end; theorem Th14: :: TOPALG_1:14 for x, y, p, q being real number for n being Nat for e1, e2, e3, e4, e5, e6 being Point of (Euclid n) for p1, p2, p3, p4 being Point of (TOP-REAL n) st e1 = p1 & e2 = p2 & e3 = p3 & e4 = p4 & e5 = (x * p1) + (y * p3) & e6 = (x * p2) + (y * p4) & dist (e1,e2) < p & dist (e3,e4) < q & x <> 0 & y <> 0 holds dist (e5,e6) < ((abs x) * p) + ((abs y) * q) proof let x, y, p, q be real number ; ::_thesis: for n being Nat for e1, e2, e3, e4, e5, e6 being Point of (Euclid n) for p1, p2, p3, p4 being Point of (TOP-REAL n) st e1 = p1 & e2 = p2 & e3 = p3 & e4 = p4 & e5 = (x * p1) + (y * p3) & e6 = (x * p2) + (y * p4) & dist (e1,e2) < p & dist (e3,e4) < q & x <> 0 & y <> 0 holds dist (e5,e6) < ((abs x) * p) + ((abs y) * q) let n be Nat; ::_thesis: for e1, e2, e3, e4, e5, e6 being Point of (Euclid n) for p1, p2, p3, p4 being Point of (TOP-REAL n) st e1 = p1 & e2 = p2 & e3 = p3 & e4 = p4 & e5 = (x * p1) + (y * p3) & e6 = (x * p2) + (y * p4) & dist (e1,e2) < p & dist (e3,e4) < q & x <> 0 & y <> 0 holds dist (e5,e6) < ((abs x) * p) + ((abs y) * q) let e1, e2, e3, e4, e5, e6 be Point of (Euclid n); ::_thesis: for p1, p2, p3, p4 being Point of (TOP-REAL n) st e1 = p1 & e2 = p2 & e3 = p3 & e4 = p4 & e5 = (x * p1) + (y * p3) & e6 = (x * p2) + (y * p4) & dist (e1,e2) < p & dist (e3,e4) < q & x <> 0 & y <> 0 holds dist (e5,e6) < ((abs x) * p) + ((abs y) * q) let p1, p2, p3, p4 be Point of (TOP-REAL n); ::_thesis: ( e1 = p1 & e2 = p2 & e3 = p3 & e4 = p4 & e5 = (x * p1) + (y * p3) & e6 = (x * p2) + (y * p4) & dist (e1,e2) < p & dist (e3,e4) < q & x <> 0 & y <> 0 implies dist (e5,e6) < ((abs x) * p) + ((abs y) * q) ) assume that A1: e1 = p1 and A2: e2 = p2 and A3: e3 = p3 and A4: e4 = p4 and A5: e5 = (x * p1) + (y * p3) and A6: e6 = (x * p2) + (y * p4) and A7: dist (e1,e2) < p and A8: dist (e3,e4) < q and A9: x <> 0 and A10: y <> 0 ; ::_thesis: dist (e5,e6) < ((abs x) * p) + ((abs y) * q) reconsider f1 = e1, f2 = e2, f3 = e3, f4 = e4, f5 = e5, f6 = e6 as Element of REAL n by A1, A2, A3, A4, A5, A6, EUCLID:22; A11: ( x * f2 = x * p2 & y * f4 = y * p4 ) by A2, A4; ( x * f1 = x * p1 & y * f3 = y * p3 ) by A1, A3; then A12: f5 = (x * f1) + (y * f3) by A5; A13: 0 < abs y by A10, COMPLEX1:47; A14: n in NAT by ORDINAL1:def_12; then dist (e3,e4) = |.(f3 - f4).| by SPPOL_1:5; then A15: (abs y) * |.(f3 - f4).| < (abs y) * q by A8, A13, XREAL_1:68; A16: 0 < abs x by A9, COMPLEX1:47; dist (e1,e2) = |.(f1 - f2).| by A14, SPPOL_1:5; then (abs x) * |.(f1 - f2).| < (abs x) * p by A7, A16, XREAL_1:68; then A17: ((abs x) * |.(f1 - f2).|) + ((abs y) * |.(f3 - f4).|) < ((abs x) * p) + ((abs y) * q) by A15, XREAL_1:8; |.((x * (f1 - f2)) + (y * (f3 - f4))).| <= |.(x * (f1 - f2)).| + |.(y * (f3 - f4)).| by EUCLID:12; then |.((x * (f1 - f2)) + (y * (f3 - f4))).| <= |.(x * (f1 - f2)).| + ((abs y) * |.(f3 - f4).|) by EUCLID:11; then A18: |.((x * (f1 - f2)) + (y * (f3 - f4))).| <= ((abs x) * |.(f1 - f2).|) + ((abs y) * |.(f3 - f4).|) by EUCLID:11; dist (e5,e6) = |.(f5 - f6).| by A14, SPPOL_1:5 .= |.(((x * f1) + (y * f3)) - ((x * f2) + (y * f4))).| by A6, A12, A11 .= |.(((x * f1) - (x * f2)) + ((y * f3) - (y * f4))).| by Th9 .= |.((x * (f1 - f2)) + ((y * f3) - (y * f4))).| by Th7 .= |.((x * (f1 - f2)) + (y * (f3 - f4))).| by Th7 ; hence dist (e5,e6) < ((abs x) * p) + ((abs y) * q) by A18, A17, XXREAL_0:2; ::_thesis: verum end; Lm1: for n being Nat for X being non empty TopSpace for f1, f2, g being Function of X,(TOP-REAL n) st f1 is continuous & f2 is continuous & ( for p being Point of X holds g . p = (f1 . p) + (f2 . p) ) holds g is continuous proof let n be Nat; ::_thesis: for X being non empty TopSpace for f1, f2, g being Function of X,(TOP-REAL n) st f1 is continuous & f2 is continuous & ( for p being Point of X holds g . p = (f1 . p) + (f2 . p) ) holds g is continuous let X be non empty TopSpace; ::_thesis: for f1, f2, g being Function of X,(TOP-REAL n) st f1 is continuous & f2 is continuous & ( for p being Point of X holds g . p = (f1 . p) + (f2 . p) ) holds g is continuous let f1, f2, g be Function of X,(TOP-REAL n); ::_thesis: ( f1 is continuous & f2 is continuous & ( for p being Point of X holds g . p = (f1 . p) + (f2 . p) ) implies g is continuous ) assume that A1: ( f1 is continuous & f2 is continuous ) and A2: for p being Point of X holds g . p = (f1 . p) + (f2 . p) ; ::_thesis: g is continuous n in NAT by ORDINAL1:def_12; then consider h being Function of X,(TOP-REAL n) such that A3: for r being Point of X holds h . r = (f1 . r) + (f2 . r) and A4: h is continuous by A1, JGRAPH_6:12; for x being Point of X holds g . x = h . x proof let x be Point of X; ::_thesis: g . x = h . x thus g . x = (f1 . x) + (f2 . x) by A2 .= h . x by A3 ; ::_thesis: verum end; hence g is continuous by A4, FUNCT_2:63; ::_thesis: verum end; theorem Th15: :: TOPALG_1:15 for y being real number for n being Nat for X being non empty TopSpace for f, g being Function of X,(TOP-REAL n) st f is continuous & ( for p being Point of X holds g . p = y * (f . p) ) holds g is continuous proof let y be real number ; ::_thesis: for n being Nat for X being non empty TopSpace for f, g being Function of X,(TOP-REAL n) st f is continuous & ( for p being Point of X holds g . p = y * (f . p) ) holds g is continuous let n be Nat; ::_thesis: for X being non empty TopSpace for f, g being Function of X,(TOP-REAL n) st f is continuous & ( for p being Point of X holds g . p = y * (f . p) ) holds g is continuous let X be non empty TopSpace; ::_thesis: for f, g being Function of X,(TOP-REAL n) st f is continuous & ( for p being Point of X holds g . p = y * (f . p) ) holds g is continuous let f, g be Function of X,(TOP-REAL n); ::_thesis: ( f is continuous & ( for p being Point of X holds g . p = y * (f . p) ) implies g is continuous ) assume that A1: f is continuous and A2: for p being Point of X holds g . p = y * (f . p) ; ::_thesis: g is continuous for p being Point of X for V being Subset of (TOP-REAL n) st g . p in V & V is open holds ex W being Subset of X st ( p in W & W is open & g .: W c= V ) proof let p be Point of X; ::_thesis: for V being Subset of (TOP-REAL n) st g . p in V & V is open holds ex W being Subset of X st ( p in W & W is open & g .: W c= V ) let V be Subset of (TOP-REAL n); ::_thesis: ( g . p in V & V is open implies ex W being Subset of X st ( p in W & W is open & g .: W c= V ) ) reconsider r = g . p as Point of (Euclid n) by TOPREAL3:8; reconsider r1 = f . p as Point of (Euclid n) by TOPREAL3:8; assume ( g . p in V & V is open ) ; ::_thesis: ex W being Subset of X st ( p in W & W is open & g .: W c= V ) then g . p in Int V by TOPS_1:23; then consider r0 being real number such that A3: r0 > 0 and A4: Ball (r,r0) c= V by GOBOARD6:5; reconsider G1 = Ball (r1,(r0 / (abs y))) as Subset of (TOP-REAL n) by TOPREAL3:8; percases ( y <> 0 or y = 0 ) ; supposeA5: y <> 0 ; ::_thesis: ex W being Subset of X st ( p in W & W is open & g .: W c= V ) A6: G1 is open by GOBOARD6:3; A7: 0 < abs y by A5, COMPLEX1:47; then r1 in G1 by A3, GOBOARD6:1, XREAL_1:139; then consider W1 being Subset of X such that A8: p in W1 and A9: W1 is open and A10: f .: W1 c= G1 by A1, A6, JGRAPH_2:10; take W1 ; ::_thesis: ( p in W1 & W1 is open & g .: W1 c= V ) thus p in W1 by A8; ::_thesis: ( W1 is open & g .: W1 c= V ) thus W1 is open by A9; ::_thesis: g .: W1 c= V g .: W1 c= Ball (r,r0) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in g .: W1 or x in Ball (r,r0) ) assume x in g .: W1 ; ::_thesis: x in Ball (r,r0) then consider z being set such that A11: z in dom g and A12: z in W1 and A13: g . z = x by FUNCT_1:def_6; reconsider z = z as Point of X by A11; A14: x = y * (f . z) by A2, A13; then reconsider e1x = x as Point of (Euclid n) by TOPREAL3:8; reconsider ea1 = f . z as Point of (Euclid n) by TOPREAL3:8; z in the carrier of X ; then z in dom f by FUNCT_2:def_1; then f . z in f .: W1 by A12, FUNCT_1:def_6; then A15: dist (r1,ea1) < r0 / (abs y) by A10, METRIC_1:11; r = y * (f . p) by A2; then dist (r,e1x) < (abs y) * (r0 / (abs y)) by A5, A14, A15, Th13; then dist (r,e1x) < r0 by A7, XCMPLX_1:87; hence x in Ball (r,r0) by METRIC_1:11; ::_thesis: verum end; hence g .: W1 c= V by A4, XBOOLE_1:1; ::_thesis: verum end; supposeA16: y = 0 ; ::_thesis: ex W being Subset of X st ( p in W & W is open & g .: W c= V ) A17: r = y * (f . p) by A2 .= 0. (TOP-REAL n) by A16, EUCLID:29 ; take W = [#] X; ::_thesis: ( p in W & W is open & g .: W c= V ) thus p in W ; ::_thesis: ( W is open & g .: W c= V ) thus W is open ; ::_thesis: g .: W c= V let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in g .: W or x in V ) assume x in g .: W ; ::_thesis: x in V then consider z being set such that z in dom g and A18: z in W and A19: g . z = x by FUNCT_1:def_6; reconsider z = z as Point of X by A18; x = y * (f . z) by A2, A19 .= 0. (TOP-REAL n) by A16, EUCLID:29 ; then x in Ball (r,r0) by A3, A17, GOBOARD6:1; hence x in V by A4; ::_thesis: verum end; end; end; hence g is continuous by JGRAPH_2:10; ::_thesis: verum end; theorem :: TOPALG_1:16 for x, y being real number for n being Nat for X being non empty TopSpace for f1, f2, g being Function of X,(TOP-REAL n) st f1 is continuous & f2 is continuous & ( for p being Point of X holds g . p = (x * (f1 . p)) + (y * (f2 . p)) ) holds g is continuous proof let x, y be real number ; ::_thesis: for n being Nat for X being non empty TopSpace for f1, f2, g being Function of X,(TOP-REAL n) st f1 is continuous & f2 is continuous & ( for p being Point of X holds g . p = (x * (f1 . p)) + (y * (f2 . p)) ) holds g is continuous let n be Nat; ::_thesis: for X being non empty TopSpace for f1, f2, g being Function of X,(TOP-REAL n) st f1 is continuous & f2 is continuous & ( for p being Point of X holds g . p = (x * (f1 . p)) + (y * (f2 . p)) ) holds g is continuous let X be non empty TopSpace; ::_thesis: for f1, f2, g being Function of X,(TOP-REAL n) st f1 is continuous & f2 is continuous & ( for p being Point of X holds g . p = (x * (f1 . p)) + (y * (f2 . p)) ) holds g is continuous let f1, f2, g be Function of X,(TOP-REAL n); ::_thesis: ( f1 is continuous & f2 is continuous & ( for p being Point of X holds g . p = (x * (f1 . p)) + (y * (f2 . p)) ) implies g is continuous ) assume that A1: f1 is continuous and A2: f2 is continuous and A3: for p being Point of X holds g . p = (x * (f1 . p)) + (y * (f2 . p)) ; ::_thesis: g is continuous percases ( ( x <> 0 & y <> 0 ) or x = 0 or y = 0 ) ; supposethat A4: x <> 0 and A5: y <> 0 ; ::_thesis: g is continuous for p being Point of X for V being Subset of (TOP-REAL n) st g . p in V & V is open holds ex W being Subset of X st ( p in W & W is open & g .: W c= V ) proof let p be Point of X; ::_thesis: for V being Subset of (TOP-REAL n) st g . p in V & V is open holds ex W being Subset of X st ( p in W & W is open & g .: W c= V ) let V be Subset of (TOP-REAL n); ::_thesis: ( g . p in V & V is open implies ex W being Subset of X st ( p in W & W is open & g .: W c= V ) ) reconsider r = g . p as Point of (Euclid n) by TOPREAL3:8; assume ( g . p in V & V is open ) ; ::_thesis: ex W being Subset of X st ( p in W & W is open & g .: W c= V ) then g . p in Int V by TOPS_1:23; then consider r0 being real number such that A6: r0 > 0 and A7: Ball (r,r0) c= V by GOBOARD6:5; A8: r0 / 2 > 0 by A6, XREAL_1:215; reconsider r2 = f2 . p as Point of (Euclid n) by TOPREAL3:8; reconsider G2 = Ball (r2,((r0 / 2) / (abs y))) as Subset of (TOP-REAL n) by TOPREAL3:8; A9: G2 is open by GOBOARD6:3; reconsider r1 = f1 . p as Point of (Euclid n) by TOPREAL3:8; reconsider G1 = Ball (r1,((r0 / 2) / (abs x))) as Subset of (TOP-REAL n) by TOPREAL3:8; A10: G1 is open by GOBOARD6:3; A11: abs y > 0 by A5, COMPLEX1:47; then r2 in G2 by A8, GOBOARD6:1, XREAL_1:139; then consider W2 being Subset of X such that A12: p in W2 and A13: W2 is open and A14: f2 .: W2 c= G2 by A2, A9, JGRAPH_2:10; A15: abs x > 0 by A4, COMPLEX1:47; then r1 in G1 by A8, GOBOARD6:1, XREAL_1:139; then consider W1 being Subset of X such that A16: p in W1 and A17: W1 is open and A18: f1 .: W1 c= G1 by A1, A10, JGRAPH_2:10; take W = W1 /\ W2; ::_thesis: ( p in W & W is open & g .: W c= V ) thus p in W by A16, A12, XBOOLE_0:def_4; ::_thesis: ( W is open & g .: W c= V ) thus W is open by A17, A13; ::_thesis: g .: W c= V g .: W c= Ball (r,r0) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in g .: W or a in Ball (r,r0) ) assume a in g .: W ; ::_thesis: a in Ball (r,r0) then consider z being set such that A19: z in dom g and A20: z in W and A21: g . z = a by FUNCT_1:def_6; A22: z in W1 by A20, XBOOLE_0:def_4; reconsider z = z as Point of X by A19; reconsider ea2 = f2 . z as Point of (Euclid n) by TOPREAL3:8; reconsider ea1 = f1 . z as Point of (Euclid n) by TOPREAL3:8; A23: z in the carrier of X ; then A24: z in dom f2 by FUNCT_2:def_1; z in W2 by A20, XBOOLE_0:def_4; then f2 . z in f2 .: W2 by A24, FUNCT_1:def_6; then A25: dist (r2,ea2) < (r0 / 2) / (abs y) by A14, METRIC_1:11; z in dom f1 by A23, FUNCT_2:def_1; then f1 . z in f1 .: W1 by A22, FUNCT_1:def_6; then A26: dist (r1,ea1) < (r0 / 2) / (abs x) by A18, METRIC_1:11; A27: a = (x * (f1 . z)) + (y * (f2 . z)) by A3, A21; then reconsider e1x = a as Point of (Euclid n) by TOPREAL3:8; r = (x * (f1 . p)) + (y * (f2 . p)) by A3; then dist (r,e1x) < ((abs x) * ((r0 / 2) / (abs x))) + ((abs y) * ((r0 / 2) / (abs y))) by A4, A5, A27, A26, A25, Th14; then dist (r,e1x) < ((abs x) * ((r0 / (abs x)) / 2)) + ((abs y) * ((r0 / 2) / (abs y))) by XCMPLX_1:48; then dist (r,e1x) < ((abs x) * ((r0 / (abs x)) / 2)) + ((abs y) * ((r0 / (abs y)) / 2)) by XCMPLX_1:48; then dist (r,e1x) < (r0 / 2) + ((abs y) * ((r0 / (abs y)) / 2)) by A15, XCMPLX_1:97; then dist (r,e1x) < (r0 / 2) + (r0 / 2) by A11, XCMPLX_1:97; hence a in Ball (r,r0) by METRIC_1:11; ::_thesis: verum end; hence g .: W c= V by A7, XBOOLE_1:1; ::_thesis: verum end; hence g is continuous by JGRAPH_2:10; ::_thesis: verum end; supposeA28: x = 0 ; ::_thesis: g is continuous for p being Point of X holds g . p = y * (f2 . p) proof let p be Point of X; ::_thesis: g . p = y * (f2 . p) thus g . p = (x * (f1 . p)) + (y * (f2 . p)) by A3 .= (0. (TOP-REAL n)) + (y * (f2 . p)) by A28, EUCLID:29 .= y * (f2 . p) by EUCLID:27 ; ::_thesis: verum end; hence g is continuous by A2, Th15; ::_thesis: verum end; supposeA29: y = 0 ; ::_thesis: g is continuous for p being Point of X holds g . p = x * (f1 . p) proof let p be Point of X; ::_thesis: g . p = x * (f1 . p) thus g . p = (x * (f1 . p)) + (y * (f2 . p)) by A3 .= (x * (f1 . p)) + (0. (TOP-REAL n)) by A29, EUCLID:29 .= x * (f1 . p) by EUCLID:27 ; ::_thesis: verum end; hence g is continuous by A1, Th15; ::_thesis: verum end; end; end; theorem Th17: :: TOPALG_1:17 for n being Nat for F being Function of [:(TOP-REAL n),I[01]:],(TOP-REAL n) st ( for x being Point of (TOP-REAL n) for i being Point of I[01] holds F . (x,i) = (1 - i) * x ) holds F is continuous proof let n be Nat; ::_thesis: for F being Function of [:(TOP-REAL n),I[01]:],(TOP-REAL n) st ( for x being Point of (TOP-REAL n) for i being Point of I[01] holds F . (x,i) = (1 - i) * x ) holds F is continuous set I = the carrier of I[01]; let F be Function of [:(TOP-REAL n),I[01]:],(TOP-REAL n); ::_thesis: ( ( for x being Point of (TOP-REAL n) for i being Point of I[01] holds F . (x,i) = (1 - i) * x ) implies F is continuous ) assume A1: for x being Point of (TOP-REAL n) for i being Point of I[01] holds F . (x,i) = (1 - i) * x ; ::_thesis: F is continuous A2: REAL n = n -tuples_on REAL by EUCLID:def_1; A3: [#] I[01] = the carrier of I[01] ; for p being Point of [:(TOP-REAL n),I[01]:] for V being Subset of (TOP-REAL n) st F . p in V & V is open holds ex W being Subset of [:(TOP-REAL n),I[01]:] st ( p in W & W is open & F .: W c= V ) proof let p be Point of [:(TOP-REAL n),I[01]:]; ::_thesis: for V being Subset of (TOP-REAL n) st F . p in V & V is open holds ex W being Subset of [:(TOP-REAL n),I[01]:] st ( p in W & W is open & F .: W c= V ) let V be Subset of (TOP-REAL n); ::_thesis: ( F . p in V & V is open implies ex W being Subset of [:(TOP-REAL n),I[01]:] st ( p in W & W is open & F .: W c= V ) ) reconsider ep = F . p as Point of (Euclid n) by TOPREAL3:8; consider x being Point of (TOP-REAL n), i being Point of I[01] such that A4: p = [x,i] by BORSUK_1:10; A5: ep = F . (x,i) by A4 .= (1 - i) * x by A1 ; reconsider fx = x as Element of REAL n by EUCLID:22; reconsider lx = x as Point of (Euclid n) by TOPREAL3:8; A6: n in NAT by ORDINAL1:def_12; assume ( F . p in V & V is open ) ; ::_thesis: ex W being Subset of [:(TOP-REAL n),I[01]:] st ( p in W & W is open & F .: W c= V ) then F . p in Int V by TOPS_1:23; then consider r0 being real number such that A7: r0 > 0 and A8: Ball (ep,r0) c= V by GOBOARD6:5; A9: r0 / 2 > 0 by A7, XREAL_1:139; percases ( 1 - i > 0 or 1 - i <= 0 ) ; supposeA10: 1 - i > 0 ; ::_thesis: ex W being Subset of [:(TOP-REAL n),I[01]:] st ( p in W & W is open & F .: W c= V ) then - (- (1 - i)) > - 0 ; then - (1 - i) < 0 ; then A11: (i - 1) * ((2 * (1 - i)) * |.fx.|) <= 0 by A10; set t = ((2 * (1 - i)) * |.fx.|) + r0; set c = ((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0); i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) = ((i * (((2 * (1 - i)) * |.fx.|) + r0)) / (((2 * (1 - i)) * |.fx.|) + r0)) + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) by A7, A10, XCMPLX_1:89 .= ((i * (((2 * (1 - i)) * |.fx.|) + r0)) + ((1 - i) * r0)) / (((2 * (1 - i)) * |.fx.|) + r0) by XCMPLX_1:62 .= ((((i * 2) * (1 - i)) * |.fx.|) + r0) / (((2 * (1 - i)) * |.fx.|) + r0) ; then (i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))) - 1 = (((((i * 2) * (1 - i)) * |.fx.|) + r0) / (((2 * (1 - i)) * |.fx.|) + r0)) - ((((2 * (1 - i)) * |.fx.|) + r0) / (((2 * (1 - i)) * |.fx.|) + r0)) by A7, A10, XCMPLX_1:60 .= (((((i * 2) * (1 - i)) * |.fx.|) + r0) - (((2 * (1 - i)) * |.fx.|) + r0)) / (((2 * (1 - i)) * |.fx.|) + r0) by XCMPLX_1:120 ; then A12: ((i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))) - 1) + 1 <= 0 + 1 by A7, A10, A11, XREAL_1:7; set X1 = ].(i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))),(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[; set X2 = ].(i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))),(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ /\ the carrier of I[01]; reconsider X2 = ].(i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))),(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ /\ the carrier of I[01] as Subset of I[01] by XBOOLE_1:17; reconsider B = Ball (lx,((r0 / 2) / (1 - i))) as Subset of (TOP-REAL n) by TOPREAL3:8; take W = [:B,X2:]; ::_thesis: ( p in W & W is open & F .: W c= V ) 0 < (1 - i) * r0 by A7, A10, XREAL_1:129; then A13: 0 < ((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0) by A7, A10, XREAL_1:139; then abs (i - i) < ((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0) by ABSVALUE:def_1; then i in ].(i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))),(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ by RCOMP_1:1; then A14: i in X2 by XBOOLE_0:def_4; 0 <= i by BORSUK_1:43; then A15: i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) is Point of I[01] by A7, A10, A12, BORSUK_1:43; A16: now__::_thesis:_X2_is_open percases ( 0 <= i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) or i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) < 0 ) ; supposeA17: 0 <= i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) ; ::_thesis: X2 is open ].(i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))),(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ c= the carrier of I[01] proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in ].(i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))),(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ or a in the carrier of I[01] ) assume A18: a in ].(i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))),(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ ; ::_thesis: a in the carrier of I[01] then reconsider a = a as Real ; a < i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) by A18, XXREAL_1:4; then A19: a < 1 by A12, XXREAL_0:2; 0 < a by A17, A18, XXREAL_1:4; hence a in the carrier of I[01] by A19, BORSUK_1:43; ::_thesis: verum end; then reconsider X1 = ].(i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))),(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ as Subset of I[01] ; now__::_thesis:_X1_is_open percases ( i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) <= i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) or i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) > i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) ) ; suppose i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) <= i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) ; ::_thesis: X1 is open then i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) <= 1 by A12, XXREAL_0:2; then i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) is Point of I[01] by A17, BORSUK_1:43; hence X1 is open by A15, BORSUK_4:45; ::_thesis: verum end; suppose i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) > i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) ; ::_thesis: X1 is open then X1 = {} I[01] by XXREAL_1:28; hence X1 is open ; ::_thesis: verum end; end; end; hence X2 is open by A3; ::_thesis: verum end; supposeA20: i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) < 0 ; ::_thesis: X2 is open X2 = [.0,(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: [.0,(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ c= X2 let a be set ; ::_thesis: ( a in X2 implies a in [.0,(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ ) assume A21: a in X2 ; ::_thesis: a in [.0,(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ then reconsider b = a as Real ; a in ].(i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))),(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ by A21, XBOOLE_0:def_4; then A22: b < i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) by XXREAL_1:4; 0 <= b by A21, BORSUK_1:43; hence a in [.0,(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ by A22, XXREAL_1:3; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in [.0,(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ or a in X2 ) assume A23: a in [.0,(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ ; ::_thesis: a in X2 then reconsider b = a as Real ; A24: 0 <= b by A23, XXREAL_1:3; A25: b < i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) by A23, XXREAL_1:3; then b <= 1 by A12, XXREAL_0:2; then A26: a in the carrier of I[01] by A24, BORSUK_1:40, XXREAL_1:1; a in ].(i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))),(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ by A20, A25, A24, XXREAL_1:4; hence a in X2 by A26, XBOOLE_0:def_4; ::_thesis: verum end; hence X2 is open by A15, Th5; ::_thesis: verum end; end; end; x in B by A9, A10, GOBOARD6:1, XREAL_1:139; hence p in W by A4, A14, ZFMISC_1:87; ::_thesis: ( W is open & F .: W c= V ) B is open by GOBOARD6:3; hence W is open by A16, BORSUK_1:6; ::_thesis: F .: W c= V A27: 0 < 2 * (1 - i) by A10, XREAL_1:129; F .: W c= Ball (ep,r0) proof let m be set ; :: according to TARSKI:def_3 ::_thesis: ( not m in F .: W or m in Ball (ep,r0) ) assume m in F .: W ; ::_thesis: m in Ball (ep,r0) then consider z being set such that A28: z in dom F and A29: z in W and A30: F . z = m by FUNCT_1:def_6; reconsider z = z as Point of [:(TOP-REAL n),I[01]:] by A28; consider y being Point of (TOP-REAL n), j being Point of I[01] such that A31: z = [y,j] by BORSUK_1:10; reconsider ez = F . z, ey = y as Point of (Euclid n) by TOPREAL3:8; reconsider fp = ep, fz = ez, fe = (1 - i) * y, fy = y as Element of REAL n by EUCLID:22; A32: ( (1 - i) * ((r0 / (1 - i)) / 2) = r0 / 2 & (r0 / 2) / (1 - i) = (r0 / (1 - i)) / 2 ) by A10, XCMPLX_1:48, XCMPLX_1:97; fy in B by A29, A31, ZFMISC_1:87; then A33: dist (lx,ey) < (r0 / 2) / (1 - i) by METRIC_1:11; j in X2 by A29, A31, ZFMISC_1:87; then j in ].(i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))),(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ by XBOOLE_0:def_4; then abs (j - i) < ((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0) by RCOMP_1:1; then abs (i - j) < ((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0) by UNIFORM1:11; then A34: (abs (i - j)) * |.fy.| <= (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) * |.fy.| by XREAL_1:64; reconsider yy = ey as Element of n -tuples_on REAL by A2, EUCLID:22; ez = F . (y,j) by A31 .= (1 - j) * y by A1 ; then fe - fz = ((1 - i) * yy) - ((1 - j) * yy) ; then A35: |.(fe - fz).| = |.(((1 - i) - (1 - j)) * fy).| by Th8 .= (abs (j - i)) * |.fy.| by EUCLID:11 .= (abs (i - j)) * |.fy.| by UNIFORM1:11 ; reconsider gx = fx, gy = fy as Element of n -tuples_on REAL by EUCLID:def_1; A36: ( dist (ep,ez) = |.(fp - fz).| & |.(fp - fz).| <= |.(fp - fe).| + |.(fe - fz).| ) by A6, EUCLID:19, SPPOL_1:5; A37: (1 - i) * (fx - fy) = (1 - i) * (gx - gy) .= ((1 - i) * gx) - ((1 - i) * gy) by Th7 .= ((1 - i) * fx) - ((1 - i) * fy) .= ((1 - i) * fx) - fe ; A38: dist (lx,ey) = |.(fx - fy).| by A6, SPPOL_1:5; then (1 - i) * |.(fx - fy).| < (1 - i) * ((r0 / 2) / (1 - i)) by A10, A33, XREAL_1:68; then (abs (1 - i)) * |.(fx - fy).| < r0 / 2 by A10, A32, ABSVALUE:def_1; then A39: |.(((1 - i) * fx) - fe).| < r0 / 2 by A37, EUCLID:11; ( |.(fx - fy).| = |.(fy - fx).| & |.fy.| - |.fx.| <= |.(fy - fx).| ) by EUCLID:15, EUCLID:18; then |.fy.| - |.fx.| < (r0 / 2) / (1 - i) by A33, A38, XXREAL_0:2; then |.fy.| < |.fx.| + ((r0 / 2) / (1 - i)) by XREAL_1:19; then A40: (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) * |.fy.| < (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) * (|.fx.| + ((r0 / 2) / (1 - i))) by A13, XREAL_1:68; (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) * (|.fx.| + ((r0 / 2) / (1 - i))) = (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) * (|.fx.| + (r0 / (2 * (1 - i)))) by XCMPLX_1:78 .= (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) * (((|.fx.| * (2 * (1 - i))) / (2 * (1 - i))) + (r0 / (2 * (1 - i)))) by A27, XCMPLX_1:89 .= (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) * (((|.fx.| * (2 * (1 - i))) + r0) / (2 * (1 - i))) by XCMPLX_1:62 .= ((1 - i) * r0) / (2 * (1 - i)) by A7, A10, XCMPLX_1:98 .= r0 / 2 by A10, XCMPLX_1:91 ; then A41: (abs (i - j)) * |.fy.| <= r0 / 2 by A34, A40, XXREAL_0:2; fp = (1 - i) * x by A5 .= (1 - i) * fx ; then |.(fp - fe).| + |.(fe - fz).| < (r0 / 2) + (r0 / 2) by A35, A41, A39, XREAL_1:8; then dist (ep,ez) < r0 by A36, XXREAL_0:2; hence m in Ball (ep,r0) by A30, METRIC_1:11; ::_thesis: verum end; hence F .: W c= V by A8, XBOOLE_1:1; ::_thesis: verum end; supposeA42: 1 - i <= 0 ; ::_thesis: ex W being Subset of [:(TOP-REAL n),I[01]:] st ( p in W & W is open & F .: W c= V ) A43: i <= 1 by BORSUK_1:43; (1 - i) + i <= 0 + i by A42, XREAL_1:6; then A44: i = 1 by A43, XXREAL_0:1; set t = |.fx.| + r0; reconsider B = Ball (lx,r0) as Subset of (TOP-REAL n) by TOPREAL3:8; set c = r0 / (|.fx.| + r0); set X1 = ].(1 - (r0 / (|.fx.| + r0))),1.]; A45: x in B by A7, GOBOARD6:1; 0 + r0 <= |.fx.| + r0 by XREAL_1:7; then A46: r0 / (|.fx.| + r0) <= 1 by A7, XREAL_1:185; then A47: (r0 / (|.fx.| + r0)) - (r0 / (|.fx.| + r0)) <= 1 - (r0 / (|.fx.| + r0)) by XREAL_1:9; ].(1 - (r0 / (|.fx.| + r0))),1.] c= the carrier of I[01] proof let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in ].(1 - (r0 / (|.fx.| + r0))),1.] or s in the carrier of I[01] ) assume A48: s in ].(1 - (r0 / (|.fx.| + r0))),1.] ; ::_thesis: s in the carrier of I[01] then reconsider s = s as Real ; ( s <= 1 & 1 - (r0 / (|.fx.| + r0)) < s ) by A48, XXREAL_1:2; hence s in the carrier of I[01] by A47, BORSUK_1:43; ::_thesis: verum end; then reconsider X1 = ].(1 - (r0 / (|.fx.| + r0))),1.] as Subset of I[01] ; r0 / (|.fx.| + r0) is Point of I[01] by A7, A46, BORSUK_1:43; then 1 - (r0 / (|.fx.| + r0)) is Point of I[01] by JORDAN5B:4; then A49: X1 is open by Th4; take W = [:B,X1:]; ::_thesis: ( p in W & W is open & F .: W c= V ) A50: 0 < r0 / (|.fx.| + r0) by A7, XREAL_1:139; then 1 - (r0 / (|.fx.| + r0)) < 1 - 0 by XREAL_1:15; then i in X1 by A44, XXREAL_1:2; hence p in W by A4, A45, ZFMISC_1:87; ::_thesis: ( W is open & F .: W c= V ) r0 is Real by XREAL_0:def_1; then B is open by GOBOARD6:3; hence W is open by A49, BORSUK_1:6; ::_thesis: F .: W c= V F .: W c= Ball (ep,r0) proof let m be set ; :: according to TARSKI:def_3 ::_thesis: ( not m in F .: W or m in Ball (ep,r0) ) assume m in F .: W ; ::_thesis: m in Ball (ep,r0) then consider z being set such that A51: z in dom F and A52: z in W and A53: F . z = m by FUNCT_1:def_6; reconsider z = z as Point of [:(TOP-REAL n),I[01]:] by A51; consider y being Point of (TOP-REAL n), j being Point of I[01] such that A54: z = [y,j] by BORSUK_1:10; reconsider ez = F . z, ey = y as Point of (Euclid n) by TOPREAL3:8; reconsider fp = ep, fz = ez, fy = y as Element of REAL n by EUCLID:22; fy in B by A52, A54, ZFMISC_1:87; then A55: dist (lx,ey) < r0 by METRIC_1:11; A56: ez = F . (y,j) by A54 .= (1 - j) * y by A1 ; fp = (1 - i) * x by A5 .= 0. (TOP-REAL n) by A44, EUCLID:29 ; then A57: fz - fp = (F . z) - (0. (TOP-REAL n)) .= fz by RLVECT_1:13 ; A58: |.fy.| - |.fx.| <= |.(fy - fx).| by EUCLID:15; ( dist (lx,ey) = |.(fx - fy).| & |.(fx - fy).| = |.(fy - fx).| ) by A6, EUCLID:18, SPPOL_1:5; then |.fy.| - |.fx.| < r0 by A55, A58, XXREAL_0:2; then A59: |.fy.| < |.fx.| + r0 by XREAL_1:19; A60: now__::_thesis:_(1_-_j)_*_|.fy.|_<_r0 percases ( j < 1 or j >= 1 ) ; suppose j < 1 ; ::_thesis: (1 - j) * |.fy.| < r0 then A61: j - j < 1 - j by XREAL_1:14; j in X1 by A52, A54, ZFMISC_1:87; then 1 - (r0 / (|.fx.| + r0)) < j by XXREAL_1:2; then (1 - (r0 / (|.fx.| + r0))) + (r0 / (|.fx.| + r0)) < j + (r0 / (|.fx.| + r0)) by XREAL_1:8; then 1 - j < (j + (r0 / (|.fx.| + r0))) - j by XREAL_1:14; then r0 / (1 - j) > r0 / (r0 / (|.fx.| + r0)) by A7, A61, XREAL_1:76; then |.fx.| + r0 < r0 / (1 - j) by A50, XCMPLX_1:54; then |.fy.| < r0 / (1 - j) by A59, XXREAL_0:2; then (1 - j) * |.fy.| < (1 - j) * (r0 / (1 - j)) by A61, XREAL_1:68; hence (1 - j) * |.fy.| < r0 by A61, XCMPLX_1:87; ::_thesis: verum end; supposeA62: j >= 1 ; ::_thesis: (1 - j) * |.fy.| < r0 j <= 1 by BORSUK_1:43; then j = 1 by A62, XXREAL_0:1; hence (1 - j) * |.fy.| < r0 by A7; ::_thesis: verum end; end; end; 1 - j is Point of I[01] by JORDAN5B:4; then A63: 0 <= 1 - j by BORSUK_1:43; dist (ep,ez) = |.(fz - fp).| by A6, SPPOL_1:5 .= |.fz.| by A57 .= |.((1 - j) * fy).| by A56 .= (abs (1 - j)) * |.fy.| by EUCLID:11 .= (1 - j) * |.fy.| by A63, ABSVALUE:def_1 ; hence m in Ball (ep,r0) by A53, A60, METRIC_1:11; ::_thesis: verum end; hence F .: W c= V by A8, XBOOLE_1:1; ::_thesis: verum end; end; end; hence F is continuous by JGRAPH_2:10; ::_thesis: verum end; theorem Th18: :: TOPALG_1:18 for n being Nat for F being Function of [:(TOP-REAL n),I[01]:],(TOP-REAL n) st ( for x being Point of (TOP-REAL n) for i being Point of I[01] holds F . (x,i) = i * x ) holds F is continuous proof let n be Nat; ::_thesis: for F being Function of [:(TOP-REAL n),I[01]:],(TOP-REAL n) st ( for x being Point of (TOP-REAL n) for i being Point of I[01] holds F . (x,i) = i * x ) holds F is continuous set I = the carrier of I[01]; let F be Function of [:(TOP-REAL n),I[01]:],(TOP-REAL n); ::_thesis: ( ( for x being Point of (TOP-REAL n) for i being Point of I[01] holds F . (x,i) = i * x ) implies F is continuous ) assume A1: for x being Point of (TOP-REAL n) for i being Point of I[01] holds F . (x,i) = i * x ; ::_thesis: F is continuous A2: REAL n = n -tuples_on REAL by EUCLID:def_1; A3: [#] I[01] = the carrier of I[01] ; for p being Point of [:(TOP-REAL n),I[01]:] for V being Subset of (TOP-REAL n) st F . p in V & V is open holds ex W being Subset of [:(TOP-REAL n),I[01]:] st ( p in W & W is open & F .: W c= V ) proof let p be Point of [:(TOP-REAL n),I[01]:]; ::_thesis: for V being Subset of (TOP-REAL n) st F . p in V & V is open holds ex W being Subset of [:(TOP-REAL n),I[01]:] st ( p in W & W is open & F .: W c= V ) let V be Subset of (TOP-REAL n); ::_thesis: ( F . p in V & V is open implies ex W being Subset of [:(TOP-REAL n),I[01]:] st ( p in W & W is open & F .: W c= V ) ) reconsider ep = F . p as Point of (Euclid n) by TOPREAL3:8; consider x being Point of (TOP-REAL n), i being Point of I[01] such that A4: p = [x,i] by BORSUK_1:10; A5: ep = F . (x,i) by A4 .= i * x by A1 ; reconsider fx = x as Element of REAL n by EUCLID:22; reconsider lx = x as Point of (Euclid n) by TOPREAL3:8; A6: n in NAT by ORDINAL1:def_12; assume ( F . p in V & V is open ) ; ::_thesis: ex W being Subset of [:(TOP-REAL n),I[01]:] st ( p in W & W is open & F .: W c= V ) then F . p in Int V by TOPS_1:23; then consider r0 being real number such that A7: r0 > 0 and A8: Ball (ep,r0) c= V by GOBOARD6:5; A9: r0 / 2 > 0 by A7, XREAL_1:139; percases ( i > 0 or i <= 0 ) ; supposeA10: i > 0 ; ::_thesis: ex W being Subset of [:(TOP-REAL n),I[01]:] st ( p in W & W is open & F .: W c= V ) set t = ((2 * i) * |.fx.|) + r0; set c = (i * r0) / (((2 * i) * |.fx.|) + r0); i <= 1 by BORSUK_1:43; then 1 - 1 >= i - 1 by XREAL_1:9; then ((2 * i) * |.fx.|) * (i - 1) <= 0 by A10; then A11: ((i * ((2 * i) * |.fx.|)) - ((2 * i) * |.fx.|)) - r0 < r0 - r0 by A7; A12: i - ((i * r0) / (((2 * i) * |.fx.|) + r0)) = ((i * (((2 * i) * |.fx.|) + r0)) / (((2 * i) * |.fx.|) + r0)) - ((i * r0) / (((2 * i) * |.fx.|) + r0)) by A7, A10, XCMPLX_1:89 .= ((i * (((2 * i) * |.fx.|) + r0)) - (i * r0)) / (((2 * i) * |.fx.|) + r0) by XCMPLX_1:120 .= (i * ((2 * i) * |.fx.|)) / (((2 * i) * |.fx.|) + r0) ; then (i - ((i * r0) / (((2 * i) * |.fx.|) + r0))) - 1 = ((i * ((2 * i) * |.fx.|)) / (((2 * i) * |.fx.|) + r0)) - ((((2 * i) * |.fx.|) + r0) / (((2 * i) * |.fx.|) + r0)) by A7, A10, XCMPLX_1:60 .= ((i * ((2 * i) * |.fx.|)) - (((2 * i) * |.fx.|) + r0)) / (((2 * i) * |.fx.|) + r0) by XCMPLX_1:120 ; then (i - ((i * r0) / (((2 * i) * |.fx.|) + r0))) - 1 < 0 by A7, A10, A11, XREAL_1:141; then ((i - ((i * r0) / (((2 * i) * |.fx.|) + r0))) - 1) + 1 < 0 + 1 by XREAL_1:8; then A13: i - ((i * r0) / (((2 * i) * |.fx.|) + r0)) is Point of I[01] by A7, A10, A12, BORSUK_1:43; set X1 = ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),(i + ((i * r0) / (((2 * i) * |.fx.|) + r0))).[; set X2 = ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),(i + ((i * r0) / (((2 * i) * |.fx.|) + r0))).[ /\ the carrier of I[01]; reconsider X2 = ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),(i + ((i * r0) / (((2 * i) * |.fx.|) + r0))).[ /\ the carrier of I[01] as Subset of I[01] by XBOOLE_1:17; reconsider B = Ball (lx,((r0 / 2) / i)) as Subset of (TOP-REAL n) by TOPREAL3:8; take W = [:B,X2:]; ::_thesis: ( p in W & W is open & F .: W c= V ) 0 < i * r0 by A7, A10, XREAL_1:129; then A14: 0 < (i * r0) / (((2 * i) * |.fx.|) + r0) by A7, A10, XREAL_1:139; then abs (i - i) < (i * r0) / (((2 * i) * |.fx.|) + r0) by ABSVALUE:def_1; then i in ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),(i + ((i * r0) / (((2 * i) * |.fx.|) + r0))).[ by RCOMP_1:1; then A15: i in X2 by XBOOLE_0:def_4; A16: 0 <= i - ((i * r0) / (((2 * i) * |.fx.|) + r0)) by A7, A10, A12; A17: now__::_thesis:_X2_is_open percases ( i + ((i * r0) / (((2 * i) * |.fx.|) + r0)) <= 1 or i + ((i * r0) / (((2 * i) * |.fx.|) + r0)) > 1 ) ; supposeA18: i + ((i * r0) / (((2 * i) * |.fx.|) + r0)) <= 1 ; ::_thesis: X2 is open ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),(i + ((i * r0) / (((2 * i) * |.fx.|) + r0))).[ c= the carrier of I[01] proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),(i + ((i * r0) / (((2 * i) * |.fx.|) + r0))).[ or a in the carrier of I[01] ) assume A19: a in ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),(i + ((i * r0) / (((2 * i) * |.fx.|) + r0))).[ ; ::_thesis: a in the carrier of I[01] then reconsider a = a as Real ; a < i + ((i * r0) / (((2 * i) * |.fx.|) + r0)) by A19, XXREAL_1:4; then A20: a < 1 by A18, XXREAL_0:2; 0 < a by A7, A10, A12, A19, XXREAL_1:4; hence a in the carrier of I[01] by A20, BORSUK_1:43; ::_thesis: verum end; then reconsider X1 = ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),(i + ((i * r0) / (((2 * i) * |.fx.|) + r0))).[ as Subset of I[01] ; i + ((i * r0) / (((2 * i) * |.fx.|) + r0)) is Point of I[01] by A7, A10, A18, BORSUK_1:43; then X1 is open by A13, BORSUK_4:45; hence X2 is open by A3; ::_thesis: verum end; supposeA21: i + ((i * r0) / (((2 * i) * |.fx.|) + r0)) > 1 ; ::_thesis: X2 is open X2 = ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),1.] proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),1.] c= X2 let a be set ; ::_thesis: ( a in X2 implies a in ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),1.] ) assume A22: a in X2 ; ::_thesis: a in ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),1.] then reconsider b = a as Real ; a in ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),(i + ((i * r0) / (((2 * i) * |.fx.|) + r0))).[ by A22, XBOOLE_0:def_4; then A23: i - ((i * r0) / (((2 * i) * |.fx.|) + r0)) < b by XXREAL_1:4; b <= 1 by A22, BORSUK_1:43; hence a in ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),1.] by A23, XXREAL_1:2; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),1.] or a in X2 ) assume A24: a in ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),1.] ; ::_thesis: a in X2 then reconsider b = a as Real ; A25: i - ((i * r0) / (((2 * i) * |.fx.|) + r0)) < b by A24, XXREAL_1:2; A26: b <= 1 by A24, XXREAL_1:2; then b < i + ((i * r0) / (((2 * i) * |.fx.|) + r0)) by A21, XXREAL_0:2; then A27: a in ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),(i + ((i * r0) / (((2 * i) * |.fx.|) + r0))).[ by A25, XXREAL_1:4; a in the carrier of I[01] by A16, A25, A26, BORSUK_1:40, XXREAL_1:1; hence a in X2 by A27, XBOOLE_0:def_4; ::_thesis: verum end; hence X2 is open by A13, Th4; ::_thesis: verum end; end; end; x in B by A9, A10, GOBOARD6:1, XREAL_1:139; hence p in W by A4, A15, ZFMISC_1:87; ::_thesis: ( W is open & F .: W c= V ) B is open by GOBOARD6:3; hence W is open by A17, BORSUK_1:6; ::_thesis: F .: W c= V A28: 0 < 2 * i by A10, XREAL_1:129; F .: W c= Ball (ep,r0) proof let m be set ; :: according to TARSKI:def_3 ::_thesis: ( not m in F .: W or m in Ball (ep,r0) ) assume m in F .: W ; ::_thesis: m in Ball (ep,r0) then consider z being set such that A29: z in dom F and A30: z in W and A31: F . z = m by FUNCT_1:def_6; reconsider z = z as Point of [:(TOP-REAL n),I[01]:] by A29; consider y being Point of (TOP-REAL n), j being Point of I[01] such that A32: z = [y,j] by BORSUK_1:10; reconsider ez = F . z, ey = y as Point of (Euclid n) by TOPREAL3:8; reconsider fp = ep, fz = ez, fe = i * y, fy = y as Element of REAL n by EUCLID:22; A33: ( i * ((r0 / i) / 2) = r0 / 2 & (r0 / 2) / i = (r0 / i) / 2 ) by A10, XCMPLX_1:48, XCMPLX_1:97; fy in B by A30, A32, ZFMISC_1:87; then A34: dist (lx,ey) < (r0 / 2) / i by METRIC_1:11; j in X2 by A30, A32, ZFMISC_1:87; then j in ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),(i + ((i * r0) / (((2 * i) * |.fx.|) + r0))).[ by XBOOLE_0:def_4; then abs (j - i) < (i * r0) / (((2 * i) * |.fx.|) + r0) by RCOMP_1:1; then abs (i - j) < (i * r0) / (((2 * i) * |.fx.|) + r0) by UNIFORM1:11; then A35: (abs (i - j)) * |.fy.| <= ((i * r0) / (((2 * i) * |.fx.|) + r0)) * |.fy.| by XREAL_1:64; reconsider yy = ey as Element of n -tuples_on REAL by A2, EUCLID:22; ez = F . (y,j) by A32 .= j * y by A1 ; then fe - fz = (i * yy) - (j * yy) ; then A36: |.(fe - fz).| = |.((i - j) * fy).| by Th8 .= (abs (i - j)) * |.fy.| by EUCLID:11 ; reconsider yy = y as Element of n -tuples_on REAL by A2, EUCLID:22; A37: ( dist (ep,ez) = |.(fp - fz).| & |.(fp - fz).| <= |.(fp - fe).| + |.(fe - fz).| ) by A6, EUCLID:19, SPPOL_1:5; A38: dist (lx,ey) = |.(fx - fy).| by A6, SPPOL_1:5; then i * |.(fx - fy).| < i * ((r0 / 2) / i) by A10, A34, XREAL_1:68; then A39: (abs i) * |.(fx - fy).| < r0 / 2 by A10, A33, ABSVALUE:def_1; ( |.(fx - fy).| = |.(fy - fx).| & |.fy.| - |.fx.| <= |.(fy - fx).| ) by EUCLID:15, EUCLID:18; then |.fy.| - |.fx.| < (r0 / 2) / i by A34, A38, XXREAL_0:2; then |.fy.| < |.fx.| + ((r0 / 2) / i) by XREAL_1:19; then A40: ((i * r0) / (((2 * i) * |.fx.|) + r0)) * |.fy.| < ((i * r0) / (((2 * i) * |.fx.|) + r0)) * (|.fx.| + ((r0 / 2) / i)) by A14, XREAL_1:68; ((i * r0) / (((2 * i) * |.fx.|) + r0)) * (|.fx.| + ((r0 / 2) / i)) = ((i * r0) / (((2 * i) * |.fx.|) + r0)) * (|.fx.| + (r0 / (2 * i))) by XCMPLX_1:78 .= ((i * r0) / (((2 * i) * |.fx.|) + r0)) * (((|.fx.| * (2 * i)) / (2 * i)) + (r0 / (2 * i))) by A28, XCMPLX_1:89 .= ((i * r0) / (((2 * i) * |.fx.|) + r0)) * (((|.fx.| * (2 * i)) + r0) / (2 * i)) by XCMPLX_1:62 .= (i * r0) / (2 * i) by A7, A10, XCMPLX_1:98 .= r0 / 2 by A10, XCMPLX_1:91 ; then A41: (abs (i - j)) * |.fy.| <= r0 / 2 by A35, A40, XXREAL_0:2; (i * fx) - fe = (i * fx) - (i * yy) .= i * (fx - fy) by Th7 ; then A42: |.((i * fx) - fe).| < r0 / 2 by A39, EUCLID:11; (i * fx) - fe = fp - fe by A5; then |.(fp - fe).| + |.(fe - fz).| < (r0 / 2) + (r0 / 2) by A36, A41, A42, XREAL_1:8; then dist (ep,ez) < r0 by A37, XXREAL_0:2; hence m in Ball (ep,r0) by A31, METRIC_1:11; ::_thesis: verum end; hence F .: W c= V by A8, XBOOLE_1:1; ::_thesis: verum end; supposeA43: i <= 0 ; ::_thesis: ex W being Subset of [:(TOP-REAL n),I[01]:] st ( p in W & W is open & F .: W c= V ) set t = |.fx.| + r0; reconsider B = Ball (lx,r0) as Subset of (TOP-REAL n) by TOPREAL3:8; set c = r0 / (|.fx.| + r0); set X1 = [.0,(r0 / (|.fx.| + r0)).[; A44: 0 < r0 / (|.fx.| + r0) by A7, XREAL_1:139; 0 + r0 <= |.fx.| + r0 by XREAL_1:7; then A45: r0 / (|.fx.| + r0) <= 1 by A7, XREAL_1:185; A46: [.0,(r0 / (|.fx.| + r0)).[ c= the carrier of I[01] proof let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in [.0,(r0 / (|.fx.| + r0)).[ or s in the carrier of I[01] ) assume A47: s in [.0,(r0 / (|.fx.| + r0)).[ ; ::_thesis: s in the carrier of I[01] then reconsider s = s as Real ; s < r0 / (|.fx.| + r0) by A47, XXREAL_1:3; then A48: s <= 1 by A45, XXREAL_0:2; 0 <= s by A47, XXREAL_1:3; hence s in the carrier of I[01] by A48, BORSUK_1:43; ::_thesis: verum end; r0 is Real by XREAL_0:def_1; then A49: B is open by GOBOARD6:3; reconsider X1 = [.0,(r0 / (|.fx.| + r0)).[ as Subset of I[01] by A46; take W = [:B,X1:]; ::_thesis: ( p in W & W is open & F .: W c= V ) A50: x in B by A7, GOBOARD6:1; A51: i = 0 by A43, BORSUK_1:43; then i in X1 by A44, XXREAL_1:3; hence p in W by A4, A50, ZFMISC_1:87; ::_thesis: ( W is open & F .: W c= V ) r0 / (|.fx.| + r0) is Point of I[01] by A7, A45, BORSUK_1:43; then X1 is open by Th5; hence W is open by A49, BORSUK_1:6; ::_thesis: F .: W c= V F .: W c= Ball (ep,r0) proof let m be set ; :: according to TARSKI:def_3 ::_thesis: ( not m in F .: W or m in Ball (ep,r0) ) assume m in F .: W ; ::_thesis: m in Ball (ep,r0) then consider z being set such that A52: z in dom F and A53: z in W and A54: F . z = m by FUNCT_1:def_6; reconsider z = z as Point of [:(TOP-REAL n),I[01]:] by A52; consider y being Point of (TOP-REAL n), j being Point of I[01] such that A55: z = [y,j] by BORSUK_1:10; reconsider ez = F . z, ey = y as Point of (Euclid n) by TOPREAL3:8; reconsider fp = ep, fz = ez, fy = y as Element of REAL n by EUCLID:22; fy in B by A53, A55, ZFMISC_1:87; then A56: dist (lx,ey) < r0 by METRIC_1:11; A57: ez = F . (y,j) by A55 .= j * y by A1 ; fp = i * x by A5 .= 0. (TOP-REAL n) by A51, EUCLID:29 ; then A58: fz - fp = (F . z) - (0. (TOP-REAL n)) .= fz by RLVECT_1:13 ; A59: |.fy.| - |.fx.| <= |.(fy - fx).| by EUCLID:15; ( dist (lx,ey) = |.(fx - fy).| & |.(fx - fy).| = |.(fy - fx).| ) by A6, EUCLID:18, SPPOL_1:5; then |.fy.| - |.fx.| < r0 by A56, A59, XXREAL_0:2; then A60: |.fy.| < |.fx.| + r0 by XREAL_1:19; A61: now__::_thesis:_j_*_|.fy.|_<_r0 percases ( 0 < j or j <= 0 ) ; supposeA62: 0 < j ; ::_thesis: j * |.fy.| < r0 j in X1 by A53, A55, ZFMISC_1:87; then j < r0 / (|.fx.| + r0) by XXREAL_1:3; then r0 / j > r0 / (r0 / (|.fx.| + r0)) by A7, A62, XREAL_1:76; then |.fx.| + r0 < r0 / j by A44, XCMPLX_1:54; then |.fy.| < r0 / j by A60, XXREAL_0:2; then j * |.fy.| < j * (r0 / j) by A62, XREAL_1:68; hence j * |.fy.| < r0 by A62, XCMPLX_1:87; ::_thesis: verum end; suppose j <= 0 ; ::_thesis: j * |.fy.| < r0 hence j * |.fy.| < r0 by A7; ::_thesis: verum end; end; end; A63: 0 <= j by BORSUK_1:43; dist (ep,ez) = |.(fz - fp).| by A6, SPPOL_1:5 .= |.fz.| by A58 .= |.(j * fy).| by A57 .= (abs j) * |.fy.| by EUCLID:11 .= j * |.fy.| by A63, ABSVALUE:def_1 ; hence m in Ball (ep,r0) by A54, A61, METRIC_1:11; ::_thesis: verum end; hence F .: W c= V by A8, XBOOLE_1:1; ::_thesis: verum end; end; end; hence F is continuous by JGRAPH_2:10; ::_thesis: verum end; begin theorem Th19: :: TOPALG_1:19 for X being non empty TopSpace for a, b, c being Point of X st a,b are_connected & b,c are_connected holds for A1, A2 being Path of a,b for B being Path of b,c st A1,A2 are_homotopic holds A1,(A2 + B) + (- B) are_homotopic proof let X be non empty TopSpace; ::_thesis: for a, b, c being Point of X st a,b are_connected & b,c are_connected holds for A1, A2 being Path of a,b for B being Path of b,c st A1,A2 are_homotopic holds A1,(A2 + B) + (- B) are_homotopic let a, b, c be Point of X; ::_thesis: ( a,b are_connected & b,c are_connected implies for A1, A2 being Path of a,b for B being Path of b,c st A1,A2 are_homotopic holds A1,(A2 + B) + (- B) are_homotopic ) assume that A1: a,b are_connected and A2: b,c are_connected ; ::_thesis: for A1, A2 being Path of a,b for B being Path of b,c st A1,A2 are_homotopic holds A1,(A2 + B) + (- B) are_homotopic set X = the constant Path of b,b; let A1, A2 be Path of a,b; ::_thesis: for B being Path of b,c st A1,A2 are_homotopic holds A1,(A2 + B) + (- B) are_homotopic let B be Path of b,c; ::_thesis: ( A1,A2 are_homotopic implies A1,(A2 + B) + (- B) are_homotopic ) A3: A1,A1 + the constant Path of b,b are_homotopic by A1, BORSUK_6:80; assume A4: A1,A2 are_homotopic ; ::_thesis: A1,(A2 + B) + (- B) are_homotopic B + (- B), the constant Path of b,b are_homotopic by A2, BORSUK_6:84; then A2 + (B + (- B)),A1 + the constant Path of b,b are_homotopic by A1, A4, BORSUK_6:75; then A5: A2 + (B + (- B)),A1 are_homotopic by A3, BORSUK_6:79; A2 + (B + (- B)),(A2 + B) + (- B) are_homotopic by A1, A2, BORSUK_6:73; hence A1,(A2 + B) + (- B) are_homotopic by A5, BORSUK_6:79; ::_thesis: verum end; theorem :: TOPALG_1:20 for T being non empty pathwise_connected TopSpace for a1, b1, c1 being Point of T for A1, A2 being Path of a1,b1 for B being Path of b1,c1 st A1,A2 are_homotopic holds A1,(A2 + B) + (- B) are_homotopic proof let T be non empty pathwise_connected TopSpace; ::_thesis: for a1, b1, c1 being Point of T for A1, A2 being Path of a1,b1 for B being Path of b1,c1 st A1,A2 are_homotopic holds A1,(A2 + B) + (- B) are_homotopic let a1, b1, c1 be Point of T; ::_thesis: for A1, A2 being Path of a1,b1 for B being Path of b1,c1 st A1,A2 are_homotopic holds A1,(A2 + B) + (- B) are_homotopic let A1, A2 be Path of a1,b1; ::_thesis: for B being Path of b1,c1 st A1,A2 are_homotopic holds A1,(A2 + B) + (- B) are_homotopic ( a1,b1 are_connected & b1,c1 are_connected ) by BORSUK_2:def_3; hence for B being Path of b1,c1 st A1,A2 are_homotopic holds A1,(A2 + B) + (- B) are_homotopic by Th19; ::_thesis: verum end; theorem Th21: :: TOPALG_1:21 for X being non empty TopSpace for a, b, c being Point of X st a,b are_connected & c,b are_connected holds for A1, A2 being Path of a,b for B being Path of c,b st A1,A2 are_homotopic holds A1,(A2 + (- B)) + B are_homotopic proof let X be non empty TopSpace; ::_thesis: for a, b, c being Point of X st a,b are_connected & c,b are_connected holds for A1, A2 being Path of a,b for B being Path of c,b st A1,A2 are_homotopic holds A1,(A2 + (- B)) + B are_homotopic let a, b, c be Point of X; ::_thesis: ( a,b are_connected & c,b are_connected implies for A1, A2 being Path of a,b for B being Path of c,b st A1,A2 are_homotopic holds A1,(A2 + (- B)) + B are_homotopic ) assume that A1: a,b are_connected and A2: c,b are_connected ; ::_thesis: for A1, A2 being Path of a,b for B being Path of c,b st A1,A2 are_homotopic holds A1,(A2 + (- B)) + B are_homotopic set X = the constant Path of b,b; let A1, A2 be Path of a,b; ::_thesis: for B being Path of c,b st A1,A2 are_homotopic holds A1,(A2 + (- B)) + B are_homotopic let B be Path of c,b; ::_thesis: ( A1,A2 are_homotopic implies A1,(A2 + (- B)) + B are_homotopic ) A3: A1,A1 + the constant Path of b,b are_homotopic by A1, BORSUK_6:80; assume A4: A1,A2 are_homotopic ; ::_thesis: A1,(A2 + (- B)) + B are_homotopic (- B) + B, the constant Path of b,b are_homotopic by A2, BORSUK_6:86; then A2 + ((- B) + B),A1 + the constant Path of b,b are_homotopic by A1, A4, BORSUK_6:75; then A5: A2 + ((- B) + B),A1 are_homotopic by A3, BORSUK_6:79; A2 + ((- B) + B),(A2 + (- B)) + B are_homotopic by A1, A2, BORSUK_6:73; hence A1,(A2 + (- B)) + B are_homotopic by A5, BORSUK_6:79; ::_thesis: verum end; theorem :: TOPALG_1:22 for T being non empty pathwise_connected TopSpace for a1, b1, c1 being Point of T for A1, A2 being Path of a1,b1 for B being Path of c1,b1 st A1,A2 are_homotopic holds A1,(A2 + (- B)) + B are_homotopic proof let T be non empty pathwise_connected TopSpace; ::_thesis: for a1, b1, c1 being Point of T for A1, A2 being Path of a1,b1 for B being Path of c1,b1 st A1,A2 are_homotopic holds A1,(A2 + (- B)) + B are_homotopic let a1, b1, c1 be Point of T; ::_thesis: for A1, A2 being Path of a1,b1 for B being Path of c1,b1 st A1,A2 are_homotopic holds A1,(A2 + (- B)) + B are_homotopic ( a1,b1 are_connected & c1,b1 are_connected ) by BORSUK_2:def_3; hence for A1, A2 being Path of a1,b1 for B being Path of c1,b1 st A1,A2 are_homotopic holds A1,(A2 + (- B)) + B are_homotopic by Th21; ::_thesis: verum end; theorem Th23: :: TOPALG_1:23 for X being non empty TopSpace for a, b, c being Point of X st a,b are_connected & c,a are_connected holds for A1, A2 being Path of a,b for B being Path of c,a st A1,A2 are_homotopic holds A1,((- B) + B) + A2 are_homotopic proof let X be non empty TopSpace; ::_thesis: for a, b, c being Point of X st a,b are_connected & c,a are_connected holds for A1, A2 being Path of a,b for B being Path of c,a st A1,A2 are_homotopic holds A1,((- B) + B) + A2 are_homotopic let a, b, c be Point of X; ::_thesis: ( a,b are_connected & c,a are_connected implies for A1, A2 being Path of a,b for B being Path of c,a st A1,A2 are_homotopic holds A1,((- B) + B) + A2 are_homotopic ) assume that A1: a,b are_connected and A2: c,a are_connected ; ::_thesis: for A1, A2 being Path of a,b for B being Path of c,a st A1,A2 are_homotopic holds A1,((- B) + B) + A2 are_homotopic set X = the constant Path of a,a; let A1, A2 be Path of a,b; ::_thesis: for B being Path of c,a st A1,A2 are_homotopic holds A1,((- B) + B) + A2 are_homotopic let B be Path of c,a; ::_thesis: ( A1,A2 are_homotopic implies A1,((- B) + B) + A2 are_homotopic ) A3: A1, the constant Path of a,a + A1 are_homotopic by A1, BORSUK_6:82; assume A4: A1,A2 are_homotopic ; ::_thesis: A1,((- B) + B) + A2 are_homotopic (- B) + B, the constant Path of a,a are_homotopic by A2, BORSUK_6:86; then ((- B) + B) + A2, the constant Path of a,a + A1 are_homotopic by A1, A4, BORSUK_6:75; hence A1,((- B) + B) + A2 are_homotopic by A3, BORSUK_6:79; ::_thesis: verum end; theorem :: TOPALG_1:24 for T being non empty pathwise_connected TopSpace for a1, b1, c1 being Point of T for A1, A2 being Path of a1,b1 for B being Path of c1,a1 st A1,A2 are_homotopic holds A1,((- B) + B) + A2 are_homotopic proof let T be non empty pathwise_connected TopSpace; ::_thesis: for a1, b1, c1 being Point of T for A1, A2 being Path of a1,b1 for B being Path of c1,a1 st A1,A2 are_homotopic holds A1,((- B) + B) + A2 are_homotopic let a1, b1, c1 be Point of T; ::_thesis: for A1, A2 being Path of a1,b1 for B being Path of c1,a1 st A1,A2 are_homotopic holds A1,((- B) + B) + A2 are_homotopic ( a1,b1 are_connected & c1,a1 are_connected ) by BORSUK_2:def_3; hence for A1, A2 being Path of a1,b1 for B being Path of c1,a1 st A1,A2 are_homotopic holds A1,((- B) + B) + A2 are_homotopic by Th23; ::_thesis: verum end; theorem Th25: :: TOPALG_1:25 for X being non empty TopSpace for a, b, c being Point of X st a,b are_connected & a,c are_connected holds for A1, A2 being Path of a,b for B being Path of a,c st A1,A2 are_homotopic holds A1,(B + (- B)) + A2 are_homotopic proof let X be non empty TopSpace; ::_thesis: for a, b, c being Point of X st a,b are_connected & a,c are_connected holds for A1, A2 being Path of a,b for B being Path of a,c st A1,A2 are_homotopic holds A1,(B + (- B)) + A2 are_homotopic let a, b, c be Point of X; ::_thesis: ( a,b are_connected & a,c are_connected implies for A1, A2 being Path of a,b for B being Path of a,c st A1,A2 are_homotopic holds A1,(B + (- B)) + A2 are_homotopic ) assume that A1: a,b are_connected and A2: a,c are_connected ; ::_thesis: for A1, A2 being Path of a,b for B being Path of a,c st A1,A2 are_homotopic holds A1,(B + (- B)) + A2 are_homotopic set X = the constant Path of a,a; let A1, A2 be Path of a,b; ::_thesis: for B being Path of a,c st A1,A2 are_homotopic holds A1,(B + (- B)) + A2 are_homotopic let B be Path of a,c; ::_thesis: ( A1,A2 are_homotopic implies A1,(B + (- B)) + A2 are_homotopic ) A3: A1, the constant Path of a,a + A1 are_homotopic by A1, BORSUK_6:82; assume A4: A1,A2 are_homotopic ; ::_thesis: A1,(B + (- B)) + A2 are_homotopic B + (- B), the constant Path of a,a are_homotopic by A2, BORSUK_6:84; then (B + (- B)) + A2, the constant Path of a,a + A1 are_homotopic by A1, A4, BORSUK_6:75; hence A1,(B + (- B)) + A2 are_homotopic by A3, BORSUK_6:79; ::_thesis: verum end; theorem :: TOPALG_1:26 for T being non empty pathwise_connected TopSpace for a1, b1, c1 being Point of T for A1, A2 being Path of a1,b1 for B being Path of a1,c1 st A1,A2 are_homotopic holds A1,(B + (- B)) + A2 are_homotopic proof let T be non empty pathwise_connected TopSpace; ::_thesis: for a1, b1, c1 being Point of T for A1, A2 being Path of a1,b1 for B being Path of a1,c1 st A1,A2 are_homotopic holds A1,(B + (- B)) + A2 are_homotopic let a1, b1, c1 be Point of T; ::_thesis: for A1, A2 being Path of a1,b1 for B being Path of a1,c1 st A1,A2 are_homotopic holds A1,(B + (- B)) + A2 are_homotopic ( a1,b1 are_connected & a1,c1 are_connected ) by BORSUK_2:def_3; hence for A1, A2 being Path of a1,b1 for B being Path of a1,c1 st A1,A2 are_homotopic holds A1,(B + (- B)) + A2 are_homotopic by Th25; ::_thesis: verum end; theorem Th27: :: TOPALG_1:27 for X being non empty TopSpace for a, b, c being Point of X st a,b are_connected & c,b are_connected holds for A, B being Path of a,b for C being Path of b,c st A + C,B + C are_homotopic holds A,B are_homotopic proof let X be non empty TopSpace; ::_thesis: for a, b, c being Point of X st a,b are_connected & c,b are_connected holds for A, B being Path of a,b for C being Path of b,c st A + C,B + C are_homotopic holds A,B are_homotopic let a, b, c be Point of X; ::_thesis: ( a,b are_connected & c,b are_connected implies for A, B being Path of a,b for C being Path of b,c st A + C,B + C are_homotopic holds A,B are_homotopic ) assume that A1: a,b are_connected and A2: c,b are_connected ; ::_thesis: for A, B being Path of a,b for C being Path of b,c st A + C,B + C are_homotopic holds A,B are_homotopic let A, B be Path of a,b; ::_thesis: for C being Path of b,c st A + C,B + C are_homotopic holds A,B are_homotopic let C be Path of b,c; ::_thesis: ( A + C,B + C are_homotopic implies A,B are_homotopic ) A3: (A + C) + (- C),A are_homotopic by A1, A2, Th19, BORSUK_2:12; assume A4: A + C,B + C are_homotopic ; ::_thesis: A,B are_homotopic ( a,c are_connected & - C, - C are_homotopic ) by A1, A2, BORSUK_2:12, BORSUK_6:42; then (A + C) + (- C),(B + C) + (- C) are_homotopic by A2, A4, BORSUK_6:75; then A5: A,(B + C) + (- C) are_homotopic by A3, BORSUK_6:79; (B + C) + (- C),B are_homotopic by A1, A2, Th19, BORSUK_2:12; hence A,B are_homotopic by A5, BORSUK_6:79; ::_thesis: verum end; theorem :: TOPALG_1:28 for T being non empty pathwise_connected TopSpace for a1, b1, c1 being Point of T for A, B being Path of a1,b1 for C being Path of b1,c1 st A + C,B + C are_homotopic holds A,B are_homotopic proof let T be non empty pathwise_connected TopSpace; ::_thesis: for a1, b1, c1 being Point of T for A, B being Path of a1,b1 for C being Path of b1,c1 st A + C,B + C are_homotopic holds A,B are_homotopic let a1, b1, c1 be Point of T; ::_thesis: for A, B being Path of a1,b1 for C being Path of b1,c1 st A + C,B + C are_homotopic holds A,B are_homotopic ( a1,b1 are_connected & c1,b1 are_connected ) by BORSUK_2:def_3; hence for A, B being Path of a1,b1 for C being Path of b1,c1 st A + C,B + C are_homotopic holds A,B are_homotopic by Th27; ::_thesis: verum end; theorem Th29: :: TOPALG_1:29 for X being non empty TopSpace for a, b, c being Point of X st a,b are_connected & a,c are_connected holds for A, B being Path of a,b for C being Path of c,a st C + A,C + B are_homotopic holds A,B are_homotopic proof let X be non empty TopSpace; ::_thesis: for a, b, c being Point of X st a,b are_connected & a,c are_connected holds for A, B being Path of a,b for C being Path of c,a st C + A,C + B are_homotopic holds A,B are_homotopic let a, b, c be Point of X; ::_thesis: ( a,b are_connected & a,c are_connected implies for A, B being Path of a,b for C being Path of c,a st C + A,C + B are_homotopic holds A,B are_homotopic ) assume that A1: a,b are_connected and A2: a,c are_connected ; ::_thesis: for A, B being Path of a,b for C being Path of c,a st C + A,C + B are_homotopic holds A,B are_homotopic let A, B be Path of a,b; ::_thesis: for C being Path of c,a st C + A,C + B are_homotopic holds A,B are_homotopic let C be Path of c,a; ::_thesis: ( C + A,C + B are_homotopic implies A,B are_homotopic ) A3: ((- C) + C) + A,(- C) + (C + A) are_homotopic by A1, A2, BORSUK_6:73; assume A4: C + A,C + B are_homotopic ; ::_thesis: A,B are_homotopic ( b,c are_connected & - C, - C are_homotopic ) by A1, A2, BORSUK_2:12, BORSUK_6:42; then (- C) + (C + A),(- C) + (C + B) are_homotopic by A2, A4, BORSUK_6:75; then A5: ((- C) + C) + A,(- C) + (C + B) are_homotopic by A3, BORSUK_6:79; ((- C) + C) + B,(- C) + (C + B) are_homotopic by A1, A2, BORSUK_6:73; then A6: ((- C) + C) + A,((- C) + C) + B are_homotopic by A5, BORSUK_6:79; ((- C) + C) + A,A are_homotopic by A1, A2, Th23, BORSUK_2:12; then A7: A,((- C) + C) + B are_homotopic by A6, BORSUK_6:79; ((- C) + C) + B,B are_homotopic by A1, A2, Th23, BORSUK_2:12; hence A,B are_homotopic by A7, BORSUK_6:79; ::_thesis: verum end; theorem :: TOPALG_1:30 for T being non empty pathwise_connected TopSpace for a1, b1, c1 being Point of T for A, B being Path of a1,b1 for C being Path of c1,a1 st C + A,C + B are_homotopic holds A,B are_homotopic proof let T be non empty pathwise_connected TopSpace; ::_thesis: for a1, b1, c1 being Point of T for A, B being Path of a1,b1 for C being Path of c1,a1 st C + A,C + B are_homotopic holds A,B are_homotopic let a1, b1, c1 be Point of T; ::_thesis: for A, B being Path of a1,b1 for C being Path of c1,a1 st C + A,C + B are_homotopic holds A,B are_homotopic ( a1,b1 are_connected & a1,c1 are_connected ) by BORSUK_2:def_3; hence for A, B being Path of a1,b1 for C being Path of c1,a1 st C + A,C + B are_homotopic holds A,B are_homotopic by Th29; ::_thesis: verum end; theorem Th31: :: TOPALG_1:31 for X being non empty TopSpace for a, b, c, d, e being Point of X st a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected holds for A being Path of a,b for B being Path of b,c for C being Path of c,d for D being Path of d,e holds ((A + B) + C) + D,(A + (B + C)) + D are_homotopic proof let X be non empty TopSpace; ::_thesis: for a, b, c, d, e being Point of X st a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected holds for A being Path of a,b for B being Path of b,c for C being Path of c,d for D being Path of d,e holds ((A + B) + C) + D,(A + (B + C)) + D are_homotopic let a, b, c, d, e be Point of X; ::_thesis: ( a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected implies for A being Path of a,b for B being Path of b,c for C being Path of c,d for D being Path of d,e holds ((A + B) + C) + D,(A + (B + C)) + D are_homotopic ) assume that A1: ( a,b are_connected & b,c are_connected ) and A2: c,d are_connected and A3: d,e are_connected ; ::_thesis: for A being Path of a,b for B being Path of b,c for C being Path of c,d for D being Path of d,e holds ((A + B) + C) + D,(A + (B + C)) + D are_homotopic a,c are_connected by A1, BORSUK_6:42; then A4: a,d are_connected by A2, BORSUK_6:42; let A be Path of a,b; ::_thesis: for B being Path of b,c for C being Path of c,d for D being Path of d,e holds ((A + B) + C) + D,(A + (B + C)) + D are_homotopic let B be Path of b,c; ::_thesis: for C being Path of c,d for D being Path of d,e holds ((A + B) + C) + D,(A + (B + C)) + D are_homotopic let C be Path of c,d; ::_thesis: for D being Path of d,e holds ((A + B) + C) + D,(A + (B + C)) + D are_homotopic let D be Path of d,e; ::_thesis: ((A + B) + C) + D,(A + (B + C)) + D are_homotopic ( (A + B) + C,A + (B + C) are_homotopic & D,D are_homotopic ) by A1, A2, A3, BORSUK_2:12, BORSUK_6:73; hence ((A + B) + C) + D,(A + (B + C)) + D are_homotopic by A3, A4, BORSUK_6:75; ::_thesis: verum end; theorem :: TOPALG_1:32 for T being non empty pathwise_connected TopSpace for a1, b1, c1, d1, e1 being Point of T for A being Path of a1,b1 for B being Path of b1,c1 for C being Path of c1,d1 for D being Path of d1,e1 holds ((A + B) + C) + D,(A + (B + C)) + D are_homotopic proof let T be non empty pathwise_connected TopSpace; ::_thesis: for a1, b1, c1, d1, e1 being Point of T for A being Path of a1,b1 for B being Path of b1,c1 for C being Path of c1,d1 for D being Path of d1,e1 holds ((A + B) + C) + D,(A + (B + C)) + D are_homotopic let a1, b1, c1, d1, e1 be Point of T; ::_thesis: for A being Path of a1,b1 for B being Path of b1,c1 for C being Path of c1,d1 for D being Path of d1,e1 holds ((A + B) + C) + D,(A + (B + C)) + D are_homotopic A1: ( c1,d1 are_connected & d1,e1 are_connected ) by BORSUK_2:def_3; ( a1,b1 are_connected & b1,c1 are_connected ) by BORSUK_2:def_3; hence for A being Path of a1,b1 for B being Path of b1,c1 for C being Path of c1,d1 for D being Path of d1,e1 holds ((A + B) + C) + D,(A + (B + C)) + D are_homotopic by A1, Th31; ::_thesis: verum end; theorem Th33: :: TOPALG_1:33 for X being non empty TopSpace for a, b, c, d, e being Point of X st a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected holds for A being Path of a,b for B being Path of b,c for C being Path of c,d for D being Path of d,e holds ((A + B) + C) + D,A + ((B + C) + D) are_homotopic proof let X be non empty TopSpace; ::_thesis: for a, b, c, d, e being Point of X st a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected holds for A being Path of a,b for B being Path of b,c for C being Path of c,d for D being Path of d,e holds ((A + B) + C) + D,A + ((B + C) + D) are_homotopic let a, b, c, d, e be Point of X; ::_thesis: ( a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected implies for A being Path of a,b for B being Path of b,c for C being Path of c,d for D being Path of d,e holds ((A + B) + C) + D,A + ((B + C) + D) are_homotopic ) assume that A1: a,b are_connected and A2: ( b,c are_connected & c,d are_connected ) and A3: d,e are_connected ; ::_thesis: for A being Path of a,b for B being Path of b,c for C being Path of c,d for D being Path of d,e holds ((A + B) + C) + D,A + ((B + C) + D) are_homotopic let A be Path of a,b; ::_thesis: for B being Path of b,c for C being Path of c,d for D being Path of d,e holds ((A + B) + C) + D,A + ((B + C) + D) are_homotopic let B be Path of b,c; ::_thesis: for C being Path of c,d for D being Path of d,e holds ((A + B) + C) + D,A + ((B + C) + D) are_homotopic let C be Path of c,d; ::_thesis: for D being Path of d,e holds ((A + B) + C) + D,A + ((B + C) + D) are_homotopic let D be Path of d,e; ::_thesis: ((A + B) + C) + D,A + ((B + C) + D) are_homotopic A4: ( A + (B + C),(A + B) + C are_homotopic & D,D are_homotopic ) by A1, A2, A3, BORSUK_2:12, BORSUK_6:73; A5: b,d are_connected by A2, BORSUK_6:42; then a,d are_connected by A1, BORSUK_6:42; then A6: (A + (B + C)) + D,((A + B) + C) + D are_homotopic by A3, A4, BORSUK_6:75; (A + (B + C)) + D,A + ((B + C) + D) are_homotopic by A1, A3, A5, BORSUK_6:73; hence ((A + B) + C) + D,A + ((B + C) + D) are_homotopic by A6, BORSUK_6:79; ::_thesis: verum end; theorem :: TOPALG_1:34 for T being non empty pathwise_connected TopSpace for a1, b1, c1, d1, e1 being Point of T for A being Path of a1,b1 for B being Path of b1,c1 for C being Path of c1,d1 for D being Path of d1,e1 holds ((A + B) + C) + D,A + ((B + C) + D) are_homotopic proof let T be non empty pathwise_connected TopSpace; ::_thesis: for a1, b1, c1, d1, e1 being Point of T for A being Path of a1,b1 for B being Path of b1,c1 for C being Path of c1,d1 for D being Path of d1,e1 holds ((A + B) + C) + D,A + ((B + C) + D) are_homotopic let a1, b1, c1, d1, e1 be Point of T; ::_thesis: for A being Path of a1,b1 for B being Path of b1,c1 for C being Path of c1,d1 for D being Path of d1,e1 holds ((A + B) + C) + D,A + ((B + C) + D) are_homotopic A1: ( c1,d1 are_connected & d1,e1 are_connected ) by BORSUK_2:def_3; ( a1,b1 are_connected & b1,c1 are_connected ) by BORSUK_2:def_3; hence for A being Path of a1,b1 for B being Path of b1,c1 for C being Path of c1,d1 for D being Path of d1,e1 holds ((A + B) + C) + D,A + ((B + C) + D) are_homotopic by A1, Th33; ::_thesis: verum end; theorem Th35: :: TOPALG_1:35 for X being non empty TopSpace for a, b, c, d, e being Point of X st a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected holds for A being Path of a,b for B being Path of b,c for C being Path of c,d for D being Path of d,e holds (A + (B + C)) + D,(A + B) + (C + D) are_homotopic proof let X be non empty TopSpace; ::_thesis: for a, b, c, d, e being Point of X st a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected holds for A being Path of a,b for B being Path of b,c for C being Path of c,d for D being Path of d,e holds (A + (B + C)) + D,(A + B) + (C + D) are_homotopic let a, b, c, d, e be Point of X; ::_thesis: ( a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected implies for A being Path of a,b for B being Path of b,c for C being Path of c,d for D being Path of d,e holds (A + (B + C)) + D,(A + B) + (C + D) are_homotopic ) assume that A1: ( a,b are_connected & b,c are_connected ) and A2: ( c,d are_connected & d,e are_connected ) ; ::_thesis: for A being Path of a,b for B being Path of b,c for C being Path of c,d for D being Path of d,e holds (A + (B + C)) + D,(A + B) + (C + D) are_homotopic let A be Path of a,b; ::_thesis: for B being Path of b,c for C being Path of c,d for D being Path of d,e holds (A + (B + C)) + D,(A + B) + (C + D) are_homotopic let B be Path of b,c; ::_thesis: for C being Path of c,d for D being Path of d,e holds (A + (B + C)) + D,(A + B) + (C + D) are_homotopic let C be Path of c,d; ::_thesis: for D being Path of d,e holds (A + (B + C)) + D,(A + B) + (C + D) are_homotopic let D be Path of d,e; ::_thesis: (A + (B + C)) + D,(A + B) + (C + D) are_homotopic a,c are_connected by A1, BORSUK_6:42; then A3: ((A + B) + C) + D,(A + B) + (C + D) are_homotopic by A2, BORSUK_6:73; ((A + B) + C) + D,(A + (B + C)) + D are_homotopic by A1, A2, Th31; hence (A + (B + C)) + D,(A + B) + (C + D) are_homotopic by A3, BORSUK_6:79; ::_thesis: verum end; theorem :: TOPALG_1:36 for T being non empty pathwise_connected TopSpace for a1, b1, c1, d1, e1 being Point of T for A being Path of a1,b1 for B being Path of b1,c1 for C being Path of c1,d1 for D being Path of d1,e1 holds (A + (B + C)) + D,(A + B) + (C + D) are_homotopic proof let T be non empty pathwise_connected TopSpace; ::_thesis: for a1, b1, c1, d1, e1 being Point of T for A being Path of a1,b1 for B being Path of b1,c1 for C being Path of c1,d1 for D being Path of d1,e1 holds (A + (B + C)) + D,(A + B) + (C + D) are_homotopic let a1, b1, c1, d1, e1 be Point of T; ::_thesis: for A being Path of a1,b1 for B being Path of b1,c1 for C being Path of c1,d1 for D being Path of d1,e1 holds (A + (B + C)) + D,(A + B) + (C + D) are_homotopic A1: ( c1,d1 are_connected & d1,e1 are_connected ) by BORSUK_2:def_3; ( a1,b1 are_connected & b1,c1 are_connected ) by BORSUK_2:def_3; hence for A being Path of a1,b1 for B being Path of b1,c1 for C being Path of c1,d1 for D being Path of d1,e1 holds (A + (B + C)) + D,(A + B) + (C + D) are_homotopic by A1, Th35; ::_thesis: verum end; theorem Th37: :: TOPALG_1:37 for X being non empty TopSpace for a, b, c, d being Point of X st a,b are_connected & b,c are_connected & b,d are_connected holds for A being Path of a,b for B being Path of d,b for C being Path of b,c holds ((A + (- B)) + B) + C,A + C are_homotopic proof let X be non empty TopSpace; ::_thesis: for a, b, c, d being Point of X st a,b are_connected & b,c are_connected & b,d are_connected holds for A being Path of a,b for B being Path of d,b for C being Path of b,c holds ((A + (- B)) + B) + C,A + C are_homotopic let a, b, c, d be Point of X; ::_thesis: ( a,b are_connected & b,c are_connected & b,d are_connected implies for A being Path of a,b for B being Path of d,b for C being Path of b,c holds ((A + (- B)) + B) + C,A + C are_homotopic ) assume that A1: a,b are_connected and A2: b,c are_connected and A3: b,d are_connected ; ::_thesis: for A being Path of a,b for B being Path of d,b for C being Path of b,c holds ((A + (- B)) + B) + C,A + C are_homotopic let A be Path of a,b; ::_thesis: for B being Path of d,b for C being Path of b,c holds ((A + (- B)) + B) + C,A + C are_homotopic let B be Path of d,b; ::_thesis: for C being Path of b,c holds ((A + (- B)) + B) + C,A + C are_homotopic let C be Path of b,c; ::_thesis: ((A + (- B)) + B) + C,A + C are_homotopic A4: ((A + (- B)) + B) + C,A + (((- B) + B) + C) are_homotopic by A1, A2, A3, Th33; set X = the constant Path of b,b; ( C,C are_homotopic & (- B) + B, the constant Path of b,b are_homotopic ) by A2, A3, BORSUK_2:12, BORSUK_6:86; then A5: ((- B) + B) + C, the constant Path of b,b + C are_homotopic by A2, BORSUK_6:75; the constant Path of b,b + C,C are_homotopic by A2, BORSUK_6:82; then A6: ((- B) + B) + C,C are_homotopic by A5, BORSUK_6:79; A,A are_homotopic by A1, BORSUK_2:12; then A + (((- B) + B) + C),A + C are_homotopic by A1, A2, A6, BORSUK_6:75; hence ((A + (- B)) + B) + C,A + C are_homotopic by A4, BORSUK_6:79; ::_thesis: verum end; theorem :: TOPALG_1:38 for T being non empty pathwise_connected TopSpace for a1, b1, d1, c1 being Point of T for A being Path of a1,b1 for B being Path of d1,b1 for C being Path of b1,c1 holds ((A + (- B)) + B) + C,A + C are_homotopic proof let T be non empty pathwise_connected TopSpace; ::_thesis: for a1, b1, d1, c1 being Point of T for A being Path of a1,b1 for B being Path of d1,b1 for C being Path of b1,c1 holds ((A + (- B)) + B) + C,A + C are_homotopic let a1, b1, d1, c1 be Point of T; ::_thesis: for A being Path of a1,b1 for B being Path of d1,b1 for C being Path of b1,c1 holds ((A + (- B)) + B) + C,A + C are_homotopic A1: b1,d1 are_connected by BORSUK_2:def_3; ( a1,b1 are_connected & b1,c1 are_connected ) by BORSUK_2:def_3; hence for A being Path of a1,b1 for B being Path of d1,b1 for C being Path of b1,c1 holds ((A + (- B)) + B) + C,A + C are_homotopic by A1, Th37; ::_thesis: verum end; theorem Th39: :: TOPALG_1:39 for X being non empty TopSpace for a, b, c, d being Point of X st a,b are_connected & a,c are_connected & c,d are_connected holds for A being Path of a,b for B being Path of c,d for C being Path of a,c holds (((A + (- A)) + C) + B) + (- B),C are_homotopic proof let X be non empty TopSpace; ::_thesis: for a, b, c, d being Point of X st a,b are_connected & a,c are_connected & c,d are_connected holds for A being Path of a,b for B being Path of c,d for C being Path of a,c holds (((A + (- A)) + C) + B) + (- B),C are_homotopic let a, b, c, d be Point of X; ::_thesis: ( a,b are_connected & a,c are_connected & c,d are_connected implies for A being Path of a,b for B being Path of c,d for C being Path of a,c holds (((A + (- A)) + C) + B) + (- B),C are_homotopic ) assume that A1: a,b are_connected and A2: a,c are_connected and A3: c,d are_connected ; ::_thesis: for A being Path of a,b for B being Path of c,d for C being Path of a,c holds (((A + (- A)) + C) + B) + (- B),C are_homotopic let A be Path of a,b; ::_thesis: for B being Path of c,d for C being Path of a,c holds (((A + (- A)) + C) + B) + (- B),C are_homotopic let B be Path of c,d; ::_thesis: for C being Path of a,c holds (((A + (- A)) + C) + B) + (- B),C are_homotopic let C be Path of a,c; ::_thesis: (((A + (- A)) + C) + B) + (- B),C are_homotopic ( B + (- B),B + (- B) are_homotopic & (A + (- A)) + C,C are_homotopic ) by A1, A2, Th25, BORSUK_2:12; then A4: ((A + (- A)) + C) + (B + (- B)),C + (B + (- B)) are_homotopic by A2, BORSUK_6:75; ( C,(C + B) + (- B) are_homotopic & (C + B) + (- B),C + (B + (- B)) are_homotopic ) by A2, A3, Th19, BORSUK_2:12, BORSUK_6:73; then A5: C,C + (B + (- B)) are_homotopic by BORSUK_6:79; (((A + (- A)) + C) + B) + (- B),((A + (- A)) + C) + (B + (- B)) are_homotopic by A2, A3, BORSUK_6:73; then (((A + (- A)) + C) + B) + (- B),C + (B + (- B)) are_homotopic by A4, BORSUK_6:79; hence (((A + (- A)) + C) + B) + (- B),C are_homotopic by A5, BORSUK_6:79; ::_thesis: verum end; theorem :: TOPALG_1:40 for T being non empty pathwise_connected TopSpace for a1, b1, c1, d1 being Point of T for A being Path of a1,b1 for B being Path of c1,d1 for C being Path of a1,c1 holds (((A + (- A)) + C) + B) + (- B),C are_homotopic proof let T be non empty pathwise_connected TopSpace; ::_thesis: for a1, b1, c1, d1 being Point of T for A being Path of a1,b1 for B being Path of c1,d1 for C being Path of a1,c1 holds (((A + (- A)) + C) + B) + (- B),C are_homotopic let a1, b1, c1, d1 be Point of T; ::_thesis: for A being Path of a1,b1 for B being Path of c1,d1 for C being Path of a1,c1 holds (((A + (- A)) + C) + B) + (- B),C are_homotopic A1: c1,d1 are_connected by BORSUK_2:def_3; ( a1,b1 are_connected & a1,c1 are_connected ) by BORSUK_2:def_3; hence for A being Path of a1,b1 for B being Path of c1,d1 for C being Path of a1,c1 holds (((A + (- A)) + C) + B) + (- B),C are_homotopic by A1, Th39; ::_thesis: verum end; theorem Th41: :: TOPALG_1:41 for X being non empty TopSpace for a, b, c, d being Point of X st a,b are_connected & a,c are_connected & d,c are_connected holds for A being Path of a,b for B being Path of c,d for C being Path of a,c holds (A + (((- A) + C) + B)) + (- B),C are_homotopic proof let X be non empty TopSpace; ::_thesis: for a, b, c, d being Point of X st a,b are_connected & a,c are_connected & d,c are_connected holds for A being Path of a,b for B being Path of c,d for C being Path of a,c holds (A + (((- A) + C) + B)) + (- B),C are_homotopic let a, b, c, d be Point of X; ::_thesis: ( a,b are_connected & a,c are_connected & d,c are_connected implies for A being Path of a,b for B being Path of c,d for C being Path of a,c holds (A + (((- A) + C) + B)) + (- B),C are_homotopic ) assume that A1: ( a,b are_connected & a,c are_connected ) and A2: d,c are_connected ; ::_thesis: for A being Path of a,b for B being Path of c,d for C being Path of a,c holds (A + (((- A) + C) + B)) + (- B),C are_homotopic let A be Path of a,b; ::_thesis: for B being Path of c,d for C being Path of a,c holds (A + (((- A) + C) + B)) + (- B),C are_homotopic let B be Path of c,d; ::_thesis: for C being Path of a,c holds (A + (((- A) + C) + B)) + (- B),C are_homotopic let C be Path of a,c; ::_thesis: (A + (((- A) + C) + B)) + (- B),C are_homotopic A3: (((A + (- A)) + C) + B) + (- B),C are_homotopic by A1, A2, Th39; A4: - B, - B are_homotopic by A2, BORSUK_2:12; ( A + (((- A) + C) + B),((A + (- A)) + C) + B are_homotopic & a,d are_connected ) by A1, A2, Th33, BORSUK_6:42; then (A + (((- A) + C) + B)) + (- B),(((A + (- A)) + C) + B) + (- B) are_homotopic by A2, A4, BORSUK_6:75; hence (A + (((- A) + C) + B)) + (- B),C are_homotopic by A3, BORSUK_6:79; ::_thesis: verum end; theorem :: TOPALG_1:42 for T being non empty pathwise_connected TopSpace for a1, b1, c1, d1 being Point of T for A being Path of a1,b1 for B being Path of c1,d1 for C being Path of a1,c1 holds (A + (((- A) + C) + B)) + (- B),C are_homotopic proof let T be non empty pathwise_connected TopSpace; ::_thesis: for a1, b1, c1, d1 being Point of T for A being Path of a1,b1 for B being Path of c1,d1 for C being Path of a1,c1 holds (A + (((- A) + C) + B)) + (- B),C are_homotopic let a1, b1, c1, d1 be Point of T; ::_thesis: for A being Path of a1,b1 for B being Path of c1,d1 for C being Path of a1,c1 holds (A + (((- A) + C) + B)) + (- B),C are_homotopic A1: a1,c1 are_connected by BORSUK_2:def_3; ( a1,b1 are_connected & d1,c1 are_connected ) by BORSUK_2:def_3; hence for A being Path of a1,b1 for B being Path of c1,d1 for C being Path of a1,c1 holds (A + (((- A) + C) + B)) + (- B),C are_homotopic by A1, Th41; ::_thesis: verum end; theorem Th43: :: TOPALG_1:43 for X being non empty TopSpace for a, b, c, d, e, f being Point of X st a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected & a,f are_connected holds for A being Path of a,b for B being Path of b,c for C being Path of c,d for D being Path of d,e for E being Path of f,c holds (A + (B + C)) + D,((A + B) + (- E)) + ((E + C) + D) are_homotopic proof let X be non empty TopSpace; ::_thesis: for a, b, c, d, e, f being Point of X st a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected & a,f are_connected holds for A being Path of a,b for B being Path of b,c for C being Path of c,d for D being Path of d,e for E being Path of f,c holds (A + (B + C)) + D,((A + B) + (- E)) + ((E + C) + D) are_homotopic let a, b, c, d, e, f be Point of X; ::_thesis: ( a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected & a,f are_connected implies for A being Path of a,b for B being Path of b,c for C being Path of c,d for D being Path of d,e for E being Path of f,c holds (A + (B + C)) + D,((A + B) + (- E)) + ((E + C) + D) are_homotopic ) assume that A1: ( a,b are_connected & b,c are_connected ) and A2: ( c,d are_connected & d,e are_connected ) and A3: a,f are_connected ; ::_thesis: for A being Path of a,b for B being Path of b,c for C being Path of c,d for D being Path of d,e for E being Path of f,c holds (A + (B + C)) + D,((A + B) + (- E)) + ((E + C) + D) are_homotopic let A be Path of a,b; ::_thesis: for B being Path of b,c for C being Path of c,d for D being Path of d,e for E being Path of f,c holds (A + (B + C)) + D,((A + B) + (- E)) + ((E + C) + D) are_homotopic let B be Path of b,c; ::_thesis: for C being Path of c,d for D being Path of d,e for E being Path of f,c holds (A + (B + C)) + D,((A + B) + (- E)) + ((E + C) + D) are_homotopic let C be Path of c,d; ::_thesis: for D being Path of d,e for E being Path of f,c holds (A + (B + C)) + D,((A + B) + (- E)) + ((E + C) + D) are_homotopic let D be Path of d,e; ::_thesis: for E being Path of f,c holds (A + (B + C)) + D,((A + B) + (- E)) + ((E + C) + D) are_homotopic let E be Path of f,c; ::_thesis: (A + (B + C)) + D,((A + B) + (- E)) + ((E + C) + D) are_homotopic A4: (A + B) + (- E),(A + B) + (- E) are_homotopic by A3, BORSUK_2:12; A5: a,c are_connected by A1, BORSUK_6:42; then A6: f,c are_connected by A3, BORSUK_6:42; then A7: E + (C + D),(E + C) + D are_homotopic by A2, BORSUK_6:73; A8: c,e are_connected by A2, BORSUK_6:42; then A9: ((A + B) + (- E)) + (E + (C + D)),(((A + B) + (- E)) + E) + (C + D) are_homotopic by A3, A6, BORSUK_6:73; A10: (A + B) + (C + D),(A + (B + C)) + D are_homotopic by A1, A2, Th35; f,e are_connected by A8, A6, BORSUK_6:42; then ((A + B) + (- E)) + (E + (C + D)),((A + B) + (- E)) + ((E + C) + D) are_homotopic by A3, A7, A4, BORSUK_6:75; then A11: (((A + B) + (- E)) + E) + (C + D),((A + B) + (- E)) + ((E + C) + D) are_homotopic by A9, BORSUK_6:79; (((A + B) + (- E)) + E) + (C + D),(A + B) + (C + D) are_homotopic by A5, A8, A6, Th37; then (A + (B + C)) + D,(((A + B) + (- E)) + E) + (C + D) are_homotopic by A10, BORSUK_6:79; hence (A + (B + C)) + D,((A + B) + (- E)) + ((E + C) + D) are_homotopic by A11, BORSUK_6:79; ::_thesis: verum end; theorem :: TOPALG_1:44 for T being non empty pathwise_connected TopSpace for a1, b1, c1, d1, e1, f1 being Point of T for A being Path of a1,b1 for B being Path of b1,c1 for C being Path of c1,d1 for D being Path of d1,e1 for E being Path of f1,c1 holds (A + (B + C)) + D,((A + B) + (- E)) + ((E + C) + D) are_homotopic proof let T be non empty pathwise_connected TopSpace; ::_thesis: for a1, b1, c1, d1, e1, f1 being Point of T for A being Path of a1,b1 for B being Path of b1,c1 for C being Path of c1,d1 for D being Path of d1,e1 for E being Path of f1,c1 holds (A + (B + C)) + D,((A + B) + (- E)) + ((E + C) + D) are_homotopic let a1, b1, c1, d1, e1, f1 be Point of T; ::_thesis: for A being Path of a1,b1 for B being Path of b1,c1 for C being Path of c1,d1 for D being Path of d1,e1 for E being Path of f1,c1 holds (A + (B + C)) + D,((A + B) + (- E)) + ((E + C) + D) are_homotopic A1: ( c1,d1 are_connected & d1,e1 are_connected ) by BORSUK_2:def_3; A2: a1,f1 are_connected by BORSUK_2:def_3; ( a1,b1 are_connected & b1,c1 are_connected ) by BORSUK_2:def_3; hence for A being Path of a1,b1 for B being Path of b1,c1 for C being Path of c1,d1 for D being Path of d1,e1 for E being Path of f1,c1 holds (A + (B + C)) + D,((A + B) + (- E)) + ((E + C) + D) are_homotopic by A1, A2, Th43; ::_thesis: verum end; begin definition let T be TopStruct ; let t be Point of T; mode Loop of t is Path of t,t; end; definition let T be non empty TopStruct ; let t1, t2 be Point of T; defpred S1[ set ] means \$1 is Path of t1,t2; func Paths (t1,t2) -> set means :Def1: :: TOPALG_1:def 1 for x being set holds ( x in it iff x is Path of t1,t2 ); existence ex b1 being set st for x being set holds ( x in b1 iff x is Path of t1,t2 ) proof consider X being set such that A1: for x being set holds ( x in X iff ( x in Funcs ( the carrier of I[01], the carrier of T) & S1[x] ) ) from XBOOLE_0:sch_1(); take X ; ::_thesis: for x being set holds ( x in X iff x is Path of t1,t2 ) let x be set ; ::_thesis: ( x in X iff x is Path of t1,t2 ) thus ( x in X implies x is Path of t1,t2 ) by A1; ::_thesis: ( x is Path of t1,t2 implies x in X ) assume A2: x is Path of t1,t2 ; ::_thesis: x in X then x in Funcs ( the carrier of I[01], the carrier of T) by FUNCT_2:8; hence x in X by A1, A2; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff x is Path of t1,t2 ) ) & ( for x being set holds ( x in b2 iff x is Path of t1,t2 ) ) holds b1 = b2 proof thus for X1, X2 being set st ( for x being set holds ( x in X1 iff S1[x] ) ) & ( for x being set holds ( x in X2 iff S1[x] ) ) holds X1 = X2 from XBOOLE_0:sch_3(); ::_thesis: verum end; end; :: deftheorem Def1 defines Paths TOPALG_1:def_1_:_ for T being non empty TopStruct for t1, t2 being Point of T for b4 being set holds ( b4 = Paths (t1,t2) iff for x being set holds ( x in b4 iff x is Path of t1,t2 ) ); registration let T be non empty TopStruct ; let t1, t2 be Point of T; cluster Paths (t1,t2) -> non empty ; coherence not Paths (t1,t2) is empty proof the Path of t1,t2 in Paths (t1,t2) by Def1; hence not Paths (t1,t2) is empty ; ::_thesis: verum end; end; definition let T be non empty TopStruct ; let t be Point of T; func Loops t -> set equals :: TOPALG_1:def 2 Paths (t,t); coherence Paths (t,t) is set ; end; :: deftheorem defines Loops TOPALG_1:def_2_:_ for T being non empty TopStruct for t being Point of T holds Loops t = Paths (t,t); registration let T be non empty TopStruct ; let t be Point of T; cluster Loops t -> non empty ; coherence not Loops t is empty ; end; Lm2: for X being non empty TopSpace for a, b being Point of X st a,b are_connected holds ex E being Equivalence_Relation of (Paths (a,b)) st for x, y being set holds ( [x,y] in E iff ( x in Paths (a,b) & y in Paths (a,b) & ex P, Q being Path of a,b st ( P = x & Q = y & P,Q are_homotopic ) ) ) proof let X be non empty TopSpace; ::_thesis: for a, b being Point of X st a,b are_connected holds ex E being Equivalence_Relation of (Paths (a,b)) st for x, y being set holds ( [x,y] in E iff ( x in Paths (a,b) & y in Paths (a,b) & ex P, Q being Path of a,b st ( P = x & Q = y & P,Q are_homotopic ) ) ) let a, b be Point of X; ::_thesis: ( a,b are_connected implies ex E being Equivalence_Relation of (Paths (a,b)) st for x, y being set holds ( [x,y] in E iff ( x in Paths (a,b) & y in Paths (a,b) & ex P, Q being Path of a,b st ( P = x & Q = y & P,Q are_homotopic ) ) ) ) assume A1: a,b are_connected ; ::_thesis: ex E being Equivalence_Relation of (Paths (a,b)) st for x, y being set holds ( [x,y] in E iff ( x in Paths (a,b) & y in Paths (a,b) & ex P, Q being Path of a,b st ( P = x & Q = y & P,Q are_homotopic ) ) ) defpred S1[ set , set ] means ex P, Q being Path of a,b st ( P = \$1 & Q = \$2 & P,Q are_homotopic ); A2: for x being set st x in Paths (a,b) holds S1[x,x] proof let x be set ; ::_thesis: ( x in Paths (a,b) implies S1[x,x] ) assume x in Paths (a,b) ; ::_thesis: S1[x,x] then reconsider x = x as Path of a,b by Def1; x,x are_homotopic by A1, BORSUK_2:12; hence S1[x,x] ; ::_thesis: verum end; A3: for x, y, z being set st S1[x,y] & S1[y,z] holds S1[x,z] by BORSUK_6:79; A4: for x, y being set st S1[x,y] holds S1[y,x] ; thus ex EqR being Equivalence_Relation of (Paths (a,b)) st for x, y being set holds ( [x,y] in EqR iff ( x in Paths (a,b) & y in Paths (a,b) & S1[x,y] ) ) from EQREL_1:sch_1(A2, A4, A3); ::_thesis: verum end; definition let X be non empty TopSpace; let a, b be Point of X; assume B1: a,b are_connected ; func EqRel (X,a,b) -> Relation of (Paths (a,b)) means :Def3: :: TOPALG_1:def 3 for P, Q being Path of a,b holds ( [P,Q] in it iff P,Q are_homotopic ); existence ex b1 being Relation of (Paths (a,b)) st for P, Q being Path of a,b holds ( [P,Q] in b1 iff P,Q are_homotopic ) proof consider E being Equivalence_Relation of (Paths (a,b)) such that A1: for x, y being set holds ( [x,y] in E iff ( x in Paths (a,b) & y in Paths (a,b) & ex P, Q being Path of a,b st ( P = x & Q = y & P,Q are_homotopic ) ) ) by B1, Lm2; take E ; ::_thesis: for P, Q being Path of a,b holds ( [P,Q] in E iff P,Q are_homotopic ) let P, Q be Path of a,b; ::_thesis: ( [P,Q] in E iff P,Q are_homotopic ) thus ( [P,Q] in E implies P,Q are_homotopic ) ::_thesis: ( P,Q are_homotopic implies [P,Q] in E ) proof assume [P,Q] in E ; ::_thesis: P,Q are_homotopic then ex P1, Q1 being Path of a,b st ( P1 = P & Q1 = Q & P1,Q1 are_homotopic ) by A1; hence P,Q are_homotopic ; ::_thesis: verum end; ( P in Paths (a,b) & Q in Paths (a,b) ) by Def1; hence ( P,Q are_homotopic implies [P,Q] in E ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Relation of (Paths (a,b)) st ( for P, Q being Path of a,b holds ( [P,Q] in b1 iff P,Q are_homotopic ) ) & ( for P, Q being Path of a,b holds ( [P,Q] in b2 iff P,Q are_homotopic ) ) holds b1 = b2 proof let E, F be Relation of (Paths (a,b)); ::_thesis: ( ( for P, Q being Path of a,b holds ( [P,Q] in E iff P,Q are_homotopic ) ) & ( for P, Q being Path of a,b holds ( [P,Q] in F iff P,Q are_homotopic ) ) implies E = F ) assume that A2: for P, Q being Path of a,b holds ( [P,Q] in E iff P,Q are_homotopic ) and A3: for P, Q being Path of a,b holds ( [P,Q] in F iff P,Q are_homotopic ) ; ::_thesis: E = F let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x,y] in E or [x,y] in F ) & ( not [x,y] in F or [x,y] in E ) ) thus ( [x,y] in E implies [x,y] in F ) ::_thesis: ( not [x,y] in F or [x,y] in E ) proof assume A4: [x,y] in E ; ::_thesis: [x,y] in F then ( x in Paths (a,b) & y in Paths (a,b) ) by ZFMISC_1:87; then reconsider x = x, y = y as Path of a,b by Def1; x,y are_homotopic by A2, A4; hence [x,y] in F by A3; ::_thesis: verum end; assume A5: [x,y] in F ; ::_thesis: [x,y] in E then ( x in Paths (a,b) & y in Paths (a,b) ) by ZFMISC_1:87; then reconsider x = x, y = y as Path of a,b by Def1; x,y are_homotopic by A3, A5; hence [x,y] in E by A2; ::_thesis: verum end; end; :: deftheorem Def3 defines EqRel TOPALG_1:def_3_:_ for X being non empty TopSpace for a, b being Point of X st a,b are_connected holds for b4 being Relation of (Paths (a,b)) holds ( b4 = EqRel (X,a,b) iff for P, Q being Path of a,b holds ( [P,Q] in b4 iff P,Q are_homotopic ) ); Lm3: for X being non empty TopSpace for a, b being Point of X st a,b are_connected holds ( not EqRel (X,a,b) is empty & EqRel (X,a,b) is total & EqRel (X,a,b) is symmetric & EqRel (X,a,b) is transitive ) proof let X be non empty TopSpace; ::_thesis: for a, b being Point of X st a,b are_connected holds ( not EqRel (X,a,b) is empty & EqRel (X,a,b) is total & EqRel (X,a,b) is symmetric & EqRel (X,a,b) is transitive ) let a, b be Point of X; ::_thesis: ( a,b are_connected implies ( not EqRel (X,a,b) is empty & EqRel (X,a,b) is total & EqRel (X,a,b) is symmetric & EqRel (X,a,b) is transitive ) ) set E = EqRel (X,a,b); set W = Paths (a,b); assume A1: a,b are_connected ; ::_thesis: ( not EqRel (X,a,b) is empty & EqRel (X,a,b) is total & EqRel (X,a,b) is symmetric & EqRel (X,a,b) is transitive ) then consider EqR being Equivalence_Relation of (Paths (a,b)) such that A2: for x, y being set holds ( [x,y] in EqR iff ( x in Paths (a,b) & y in Paths (a,b) & ex P, Q being Path of a,b st ( P = x & Q = y & P,Q are_homotopic ) ) ) by Lm2; EqRel (X,a,b) = EqR proof let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x,y] in EqRel (X,a,b) or [x,y] in EqR ) & ( not [x,y] in EqR or [x,y] in EqRel (X,a,b) ) ) thus ( [x,y] in EqRel (X,a,b) implies [x,y] in EqR ) ::_thesis: ( not [x,y] in EqR or [x,y] in EqRel (X,a,b) ) proof assume A3: [x,y] in EqRel (X,a,b) ; ::_thesis: [x,y] in EqR then A4: ( x in Paths (a,b) & y in Paths (a,b) ) by ZFMISC_1:87; then reconsider x = x, y = y as Path of a,b by Def1; x,y are_homotopic by A1, A3, Def3; hence [x,y] in EqR by A2, A4; ::_thesis: verum end; assume A5: [x,y] in EqR ; ::_thesis: [x,y] in EqRel (X,a,b) then ( x in Paths (a,b) & y in Paths (a,b) ) by ZFMISC_1:87; then reconsider x = x, y = y as Path of a,b by Def1; ex P, Q being Path of a,b st ( P = x & Q = y & P,Q are_homotopic ) by A2, A5; hence [x,y] in EqRel (X,a,b) by A1, Def3; ::_thesis: verum end; hence ( not EqRel (X,a,b) is empty & EqRel (X,a,b) is total & EqRel (X,a,b) is symmetric & EqRel (X,a,b) is transitive ) by EQREL_1:9, RELAT_1:40; ::_thesis: verum end; theorem Th45: :: TOPALG_1:45 for X being non empty TopSpace for a, b being Point of X st a,b are_connected holds for P, Q being Path of a,b holds ( Q in Class ((EqRel (X,a,b)),P) iff P,Q are_homotopic ) proof let X be non empty TopSpace; ::_thesis: for a, b being Point of X st a,b are_connected holds for P, Q being Path of a,b holds ( Q in Class ((EqRel (X,a,b)),P) iff P,Q are_homotopic ) let a, b be Point of X; ::_thesis: ( a,b are_connected implies for P, Q being Path of a,b holds ( Q in Class ((EqRel (X,a,b)),P) iff P,Q are_homotopic ) ) set E = EqRel (X,a,b); assume A1: a,b are_connected ; ::_thesis: for P, Q being Path of a,b holds ( Q in Class ((EqRel (X,a,b)),P) iff P,Q are_homotopic ) let P, Q be Path of a,b; ::_thesis: ( Q in Class ((EqRel (X,a,b)),P) iff P,Q are_homotopic ) A2: ( not EqRel (X,a,b) is empty & EqRel (X,a,b) is total & EqRel (X,a,b) is symmetric & EqRel (X,a,b) is transitive ) by A1, Lm3; hereby ::_thesis: ( P,Q are_homotopic implies Q in Class ((EqRel (X,a,b)),P) ) assume Q in Class ((EqRel (X,a,b)),P) ; ::_thesis: P,Q are_homotopic then [Q,P] in EqRel (X,a,b) by A2, EQREL_1:19; hence P,Q are_homotopic by A1, Def3; ::_thesis: verum end; assume P,Q are_homotopic ; ::_thesis: Q in Class ((EqRel (X,a,b)),P) then [Q,P] in EqRel (X,a,b) by A1, Def3; hence Q in Class ((EqRel (X,a,b)),P) by A2, EQREL_1:19; ::_thesis: verum end; theorem Th46: :: TOPALG_1:46 for X being non empty TopSpace for a, b being Point of X st a,b are_connected holds for P, Q being Path of a,b holds ( Class ((EqRel (X,a,b)),P) = Class ((EqRel (X,a,b)),Q) iff P,Q are_homotopic ) proof let X be non empty TopSpace; ::_thesis: for a, b being Point of X st a,b are_connected holds for P, Q being Path of a,b holds ( Class ((EqRel (X,a,b)),P) = Class ((EqRel (X,a,b)),Q) iff P,Q are_homotopic ) let a, b be Point of X; ::_thesis: ( a,b are_connected implies for P, Q being Path of a,b holds ( Class ((EqRel (X,a,b)),P) = Class ((EqRel (X,a,b)),Q) iff P,Q are_homotopic ) ) set E = EqRel (X,a,b); assume A1: a,b are_connected ; ::_thesis: for P, Q being Path of a,b holds ( Class ((EqRel (X,a,b)),P) = Class ((EqRel (X,a,b)),Q) iff P,Q are_homotopic ) let P, Q be Path of a,b; ::_thesis: ( Class ((EqRel (X,a,b)),P) = Class ((EqRel (X,a,b)),Q) iff P,Q are_homotopic ) A2: Q in Paths (a,b) by Def1; A3: ( not EqRel (X,a,b) is empty & EqRel (X,a,b) is total & EqRel (X,a,b) is symmetric & EqRel (X,a,b) is transitive ) by A1, Lm3; hereby ::_thesis: ( P,Q are_homotopic implies Class ((EqRel (X,a,b)),P) = Class ((EqRel (X,a,b)),Q) ) assume Class ((EqRel (X,a,b)),P) = Class ((EqRel (X,a,b)),Q) ; ::_thesis: P,Q are_homotopic then P in Class ((EqRel (X,a,b)),Q) by A3, A2, EQREL_1:23; hence P,Q are_homotopic by A1, Th45; ::_thesis: verum end; assume P,Q are_homotopic ; ::_thesis: Class ((EqRel (X,a,b)),P) = Class ((EqRel (X,a,b)),Q) then P in Class ((EqRel (X,a,b)),Q) by A1, Th45; hence Class ((EqRel (X,a,b)),P) = Class ((EqRel (X,a,b)),Q) by A3, A2, EQREL_1:23; ::_thesis: verum end; definition let X be non empty TopSpace; let a be Point of X; func EqRel (X,a) -> Relation of (Loops a) equals :: TOPALG_1:def 4 EqRel (X,a,a); coherence EqRel (X,a,a) is Relation of (Loops a) ; end; :: deftheorem defines EqRel TOPALG_1:def_4_:_ for X being non empty TopSpace for a being Point of X holds EqRel (X,a) = EqRel (X,a,a); registration let X be non empty TopSpace; let a be Point of X; cluster EqRel (X,a) -> non empty total symmetric transitive ; coherence ( not EqRel (X,a) is empty & EqRel (X,a) is total & EqRel (X,a) is symmetric & EqRel (X,a) is transitive ) by Lm3; end; definition let X be non empty TopSpace; let a be Point of X; set E = EqRel (X,a); set A = Class (EqRel (X,a)); set W = Loops a; func FundamentalGroup (X,a) -> strict multMagma means :Def5: :: TOPALG_1:def 5 ( the carrier of it = Class (EqRel (X,a)) & ( for x, y being Element of it ex P, Q being Loop of a st ( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),Q) & the multF of it . (x,y) = Class ((EqRel (X,a)),(P + Q)) ) ) ); existence ex b1 being strict multMagma st ( the carrier of b1 = Class (EqRel (X,a)) & ( for x, y being Element of b1 ex P, Q being Loop of a st ( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),Q) & the multF of b1 . (x,y) = Class ((EqRel (X,a)),(P + Q)) ) ) ) proof defpred S1[ set , set , set ] means ex P, Q being Loop of a st ( \$1 = Class ((EqRel (X,a)),P) & \$2 = Class ((EqRel (X,a)),Q) & \$3 = Class ((EqRel (X,a)),(P + Q)) ); A1: for x, y being Element of Class (EqRel (X,a)) ex z being Element of Class (EqRel (X,a)) st S1[x,y,z] proof let x, y be Element of Class (EqRel (X,a)); ::_thesis: ex z being Element of Class (EqRel (X,a)) st S1[x,y,z] x in Class (EqRel (X,a)) ; then consider P being set such that A2: P in Loops a and A3: x = Class ((EqRel (X,a)),P) by EQREL_1:def_3; y in Class (EqRel (X,a)) ; then consider Q being set such that A4: Q in Loops a and A5: y = Class ((EqRel (X,a)),Q) by EQREL_1:def_3; reconsider P = P, Q = Q as Loop of a by A2, A4, Def1; P + Q in Loops a by Def1; then reconsider z = Class ((EqRel (X,a)),(P + Q)) as Element of Class (EqRel (X,a)) by EQREL_1:def_3; take z ; ::_thesis: S1[x,y,z] thus S1[x,y,z] by A3, A5; ::_thesis: verum end; consider g being BinOp of (Class (EqRel (X,a))) such that A6: for a, b being Element of Class (EqRel (X,a)) holds S1[a,b,g . (a,b)] from BINOP_1:sch_3(A1); take multMagma(# (Class (EqRel (X,a))),g #) ; ::_thesis: ( the carrier of multMagma(# (Class (EqRel (X,a))),g #) = Class (EqRel (X,a)) & ( for x, y being Element of multMagma(# (Class (EqRel (X,a))),g #) ex P, Q being Loop of a st ( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),Q) & the multF of multMagma(# (Class (EqRel (X,a))),g #) . (x,y) = Class ((EqRel (X,a)),(P + Q)) ) ) ) thus ( the carrier of multMagma(# (Class (EqRel (X,a))),g #) = Class (EqRel (X,a)) & ( for x, y being Element of multMagma(# (Class (EqRel (X,a))),g #) ex P, Q being Loop of a st ( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),Q) & the multF of multMagma(# (Class (EqRel (X,a))),g #) . (x,y) = Class ((EqRel (X,a)),(P + Q)) ) ) ) by A6; ::_thesis: verum end; uniqueness for b1, b2 being strict multMagma st the carrier of b1 = Class (EqRel (X,a)) & ( for x, y being Element of b1 ex P, Q being Loop of a st ( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),Q) & the multF of b1 . (x,y) = Class ((EqRel (X,a)),(P + Q)) ) ) & the carrier of b2 = Class (EqRel (X,a)) & ( for x, y being Element of b2 ex P, Q being Loop of a st ( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),Q) & the multF of b2 . (x,y) = Class ((EqRel (X,a)),(P + Q)) ) ) holds b1 = b2 proof let F, G be strict multMagma ; ::_thesis: ( the carrier of F = Class (EqRel (X,a)) & ( for x, y being Element of F ex P, Q being Loop of a st ( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),Q) & the multF of F . (x,y) = Class ((EqRel (X,a)),(P + Q)) ) ) & the carrier of G = Class (EqRel (X,a)) & ( for x, y being Element of G ex P, Q being Loop of a st ( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),Q) & the multF of G . (x,y) = Class ((EqRel (X,a)),(P + Q)) ) ) implies F = G ) assume that A7: the carrier of F = Class (EqRel (X,a)) and A8: for x, y being Element of F ex P, Q being Loop of a st ( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),Q) & the multF of F . (x,y) = Class ((EqRel (X,a)),(P + Q)) ) and A9: the carrier of G = Class (EqRel (X,a)) and A10: for x, y being Element of G ex P, Q being Loop of a st ( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),Q) & the multF of G . (x,y) = Class ((EqRel (X,a)),(P + Q)) ) ; ::_thesis: F = G set g = the multF of G; set f = the multF of F; for c, d being Element of F holds the multF of F . (c,d) = the multF of G . (c,d) proof let c, d be Element of F; ::_thesis: the multF of F . (c,d) = the multF of G . (c,d) consider P1, Q1 being Loop of a such that A11: ( c = Class ((EqRel (X,a)),P1) & d = Class ((EqRel (X,a)),Q1) ) and A12: the multF of F . (c,d) = Class ((EqRel (X,a)),(P1 + Q1)) by A8; consider P2, Q2 being Loop of a such that A13: ( c = Class ((EqRel (X,a)),P2) & d = Class ((EqRel (X,a)),Q2) ) and A14: the multF of G . (c,d) = Class ((EqRel (X,a)),(P2 + Q2)) by A7, A9, A10; ( P1,P2 are_homotopic & Q1,Q2 are_homotopic ) by A11, A13, Th46; then P1 + Q1,P2 + Q2 are_homotopic by BORSUK_6:75; hence the multF of F . (c,d) = the multF of G . (c,d) by A12, A14, Th46; ::_thesis: verum end; hence F = G by A7, A9, BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def5 defines FundamentalGroup TOPALG_1:def_5_:_ for X being non empty TopSpace for a being Point of X for b3 being strict multMagma holds ( b3 = FundamentalGroup (X,a) iff ( the carrier of b3 = Class (EqRel (X,a)) & ( for x, y being Element of b3 ex P, Q being Loop of a st ( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),Q) & the multF of b3 . (x,y) = Class ((EqRel (X,a)),(P + Q)) ) ) ) ); notation let X be non empty TopSpace; let a be Point of X; synonym pi_1 (X,a) for FundamentalGroup (X,a); end; registration let X be non empty TopSpace; let a be Point of X; cluster FundamentalGroup (X,a) -> non empty strict ; coherence not pi_1 (X,a) is empty proof the carrier of (pi_1 (X,a)) = Class (EqRel (X,a)) by Def5; hence not the carrier of (pi_1 (X,a)) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum end; end; theorem Th47: :: TOPALG_1:47 for X being non empty TopSpace for a being Point of X for x being set holds ( x in the carrier of (pi_1 (X,a)) iff ex P being Loop of a st x = Class ((EqRel (X,a)),P) ) proof let X be non empty TopSpace; ::_thesis: for a being Point of X for x being set holds ( x in the carrier of (pi_1 (X,a)) iff ex P being Loop of a st x = Class ((EqRel (X,a)),P) ) let a be Point of X; ::_thesis: for x being set holds ( x in the carrier of (pi_1 (X,a)) iff ex P being Loop of a st x = Class ((EqRel (X,a)),P) ) let x be set ; ::_thesis: ( x in the carrier of (pi_1 (X,a)) iff ex P being Loop of a st x = Class ((EqRel (X,a)),P) ) A1: the carrier of (pi_1 (X,a)) = Class (EqRel (X,a)) by Def5; hereby ::_thesis: ( ex P being Loop of a st x = Class ((EqRel (X,a)),P) implies x in the carrier of (pi_1 (X,a)) ) assume x in the carrier of (pi_1 (X,a)) ; ::_thesis: ex P being Loop of a st x = Class ((EqRel (X,a)),P) then consider P being Element of Loops a such that A2: x = Class ((EqRel (X,a)),P) by A1, EQREL_1:36; reconsider P = P as Loop of a by Def1; take P = P; ::_thesis: x = Class ((EqRel (X,a)),P) thus x = Class ((EqRel (X,a)),P) by A2; ::_thesis: verum end; given P being Loop of a such that A3: x = Class ((EqRel (X,a)),P) ; ::_thesis: x in the carrier of (pi_1 (X,a)) P in Loops a by Def1; hence x in the carrier of (pi_1 (X,a)) by A1, A3, EQREL_1:def_3; ::_thesis: verum end; Lm4: for S being non empty TopSpace for s being Point of S for x, y being Element of (pi_1 (S,s)) for P, Q being Loop of s st x = Class ((EqRel (S,s)),P) & y = Class ((EqRel (S,s)),Q) holds x * y = Class ((EqRel (S,s)),(P + Q)) proof let S be non empty TopSpace; ::_thesis: for s being Point of S for x, y being Element of (pi_1 (S,s)) for P, Q being Loop of s st x = Class ((EqRel (S,s)),P) & y = Class ((EqRel (S,s)),Q) holds x * y = Class ((EqRel (S,s)),(P + Q)) let s be Point of S; ::_thesis: for x, y being Element of (pi_1 (S,s)) for P, Q being Loop of s st x = Class ((EqRel (S,s)),P) & y = Class ((EqRel (S,s)),Q) holds x * y = Class ((EqRel (S,s)),(P + Q)) set X = pi_1 (S,s); let x, y be Element of (pi_1 (S,s)); ::_thesis: for P, Q being Loop of s st x = Class ((EqRel (S,s)),P) & y = Class ((EqRel (S,s)),Q) holds x * y = Class ((EqRel (S,s)),(P + Q)) let P, Q be Loop of s; ::_thesis: ( x = Class ((EqRel (S,s)),P) & y = Class ((EqRel (S,s)),Q) implies x * y = Class ((EqRel (S,s)),(P + Q)) ) consider P1, Q1 being Loop of s such that A1: ( x = Class ((EqRel (S,s)),P1) & y = Class ((EqRel (S,s)),Q1) ) and A2: the multF of (pi_1 (S,s)) . (x,y) = Class ((EqRel (S,s)),(P1 + Q1)) by Def5; assume ( x = Class ((EqRel (S,s)),P) & y = Class ((EqRel (S,s)),Q) ) ; ::_thesis: x * y = Class ((EqRel (S,s)),(P + Q)) then ( P,P1 are_homotopic & Q,Q1 are_homotopic ) by A1, Th46; then P + Q,P1 + Q1 are_homotopic by BORSUK_6:75; hence x * y = Class ((EqRel (S,s)),(P + Q)) by A2, Th46; ::_thesis: verum end; registration let X be non empty TopSpace; let a be Point of X; cluster FundamentalGroup (X,a) -> strict Group-like associative ; coherence ( pi_1 (X,a) is associative & pi_1 (X,a) is Group-like ) proof set C = the constant Loop of a; set E = EqRel (X,a); set G = pi_1 (X,a); set e = Class ((EqRel (X,a)), the constant Loop of a); the constant Loop of a in Loops a by Def1; then A1: Class ((EqRel (X,a)), the constant Loop of a) in Class (EqRel (X,a)) by EQREL_1:def_3; thus pi_1 (X,a) is associative ::_thesis: pi_1 (X,a) is Group-like proof let x, y, z be Element of (pi_1 (X,a)); :: according to GROUP_1:def_3 ::_thesis: (x * y) * z = x * (y * z) consider A being Loop of a such that A2: x = Class ((EqRel (X,a)),A) by Th47; consider B being Loop of a such that A3: y = Class ((EqRel (X,a)),B) by Th47; consider BC being Loop of a such that A4: y * z = Class ((EqRel (X,a)),BC) by Th47; consider C being Loop of a such that A5: z = Class ((EqRel (X,a)),C) by Th47; y * z = Class ((EqRel (X,a)),(B + C)) by A3, A5, Lm4; then ( A,A are_homotopic & BC,B + C are_homotopic ) by A4, Th46, BORSUK_2:12; then A6: A + BC,A + (B + C) are_homotopic by BORSUK_6:75; consider AB being Loop of a such that A7: x * y = Class ((EqRel (X,a)),AB) by Th47; x * y = Class ((EqRel (X,a)),(A + B)) by A2, A3, Lm4; then ( C,C are_homotopic & AB,A + B are_homotopic ) by A7, Th46, BORSUK_2:12; then A8: AB + C,(A + B) + C are_homotopic by BORSUK_6:75; A9: (A + B) + C,A + (B + C) are_homotopic by BORSUK_6:73; thus (x * y) * z = Class ((EqRel (X,a)),(AB + C)) by A5, A7, Lm4 .= Class ((EqRel (X,a)),((A + B) + C)) by A8, Th46 .= Class ((EqRel (X,a)),(A + (B + C))) by A9, Th46 .= Class ((EqRel (X,a)),(A + BC)) by A6, Th46 .= x * (y * z) by A2, A4, Lm4 ; ::_thesis: verum end; reconsider e = Class ((EqRel (X,a)), the constant Loop of a) as Element of (pi_1 (X,a)) by A1, Def5; take e ; :: according to GROUP_1:def_2 ::_thesis: for b1 being Element of the carrier of (pi_1 (X,a)) holds ( b1 * e = b1 & e * b1 = b1 & ex b2 being Element of the carrier of (pi_1 (X,a)) st ( b1 * b2 = e & b2 * b1 = e ) ) let h be Element of (pi_1 (X,a)); ::_thesis: ( h * e = h & e * h = h & ex b1 being Element of the carrier of (pi_1 (X,a)) st ( h * b1 = e & b1 * h = e ) ) consider A being Loop of a such that A10: h = Class ((EqRel (X,a)),A) by Th47; A11: A + the constant Loop of a,A are_homotopic by BORSUK_6:80; thus h * e = Class ((EqRel (X,a)),(A + the constant Loop of a)) by A10, Lm4 .= h by A10, A11, Th46 ; ::_thesis: ( e * h = h & ex b1 being Element of the carrier of (pi_1 (X,a)) st ( h * b1 = e & b1 * h = e ) ) A12: the constant Loop of a + A,A are_homotopic by BORSUK_6:82; thus e * h = Class ((EqRel (X,a)),( the constant Loop of a + A)) by A10, Lm4 .= h by A10, A12, Th46 ; ::_thesis: ex b1 being Element of the carrier of (pi_1 (X,a)) st ( h * b1 = e & b1 * h = e ) set x = Class ((EqRel (X,a)),(- A)); - A in Loops a by Def1; then Class ((EqRel (X,a)),(- A)) in Class (EqRel (X,a)) by EQREL_1:def_3; then reconsider x = Class ((EqRel (X,a)),(- A)) as Element of (pi_1 (X,a)) by Def5; take x ; ::_thesis: ( h * x = e & x * h = e ) A13: A + (- A), the constant Loop of a are_homotopic by BORSUK_6:84; thus h * x = Class ((EqRel (X,a)),(A + (- A))) by A10, Lm4 .= e by A13, Th46 ; ::_thesis: x * h = e A14: (- A) + A, the constant Loop of a are_homotopic by BORSUK_6:86; thus x * h = Class ((EqRel (X,a)),((- A) + A)) by A10, Lm4 .= e by A14, Th46 ; ::_thesis: verum end; end; definition let T be non empty TopSpace; let x0, x1 be Point of T; let P be Path of x0,x1; assume A1: x0,x1 are_connected ; func pi_1-iso P -> Function of (pi_1 (T,x1)),(pi_1 (T,x0)) means :Def6: :: TOPALG_1:def 6 for Q being Loop of x1 holds it . (Class ((EqRel (T,x1)),Q)) = Class ((EqRel (T,x0)),((P + Q) + (- P))); existence ex b1 being Function of (pi_1 (T,x1)),(pi_1 (T,x0)) st for Q being Loop of x1 holds b1 . (Class ((EqRel (T,x1)),Q)) = Class ((EqRel (T,x0)),((P + Q) + (- P))) proof defpred S1[ set , set ] means ex L being Loop of x1 st ( \$1 = Class ((EqRel (T,x1)),L) & \$2 = Class ((EqRel (T,x0)),((P + L) + (- P))) ); A2: P,P are_homotopic by A1, BORSUK_2:12; A3: for x being Element of (pi_1 (T,x1)) ex y being Element of (pi_1 (T,x0)) st S1[x,y] proof let x be Element of (pi_1 (T,x1)); ::_thesis: ex y being Element of (pi_1 (T,x0)) st S1[x,y] consider Q being Loop of x1 such that A4: x = Class ((EqRel (T,x1)),Q) by Th47; reconsider y = Class ((EqRel (T,x0)),((P + Q) + (- P))) as Element of (pi_1 (T,x0)) by Th47; take y ; ::_thesis: S1[x,y] thus S1[x,y] by A4; ::_thesis: verum end; consider f being Function of the carrier of (pi_1 (T,x1)), the carrier of (pi_1 (T,x0)) such that A5: for x being Element of (pi_1 (T,x1)) holds S1[x,f . x] from FUNCT_2:sch_3(A3); reconsider f = f as Function of (pi_1 (T,x1)),(pi_1 (T,x0)) ; take f ; ::_thesis: for Q being Loop of x1 holds f . (Class ((EqRel (T,x1)),Q)) = Class ((EqRel (T,x0)),((P + Q) + (- P))) let Q be Loop of x1; ::_thesis: f . (Class ((EqRel (T,x1)),Q)) = Class ((EqRel (T,x0)),((P + Q) + (- P))) ( the carrier of (pi_1 (T,x1)) = Class (EqRel (T,x1)) & Q in Loops x1 ) by Def1, Def5; then Class ((EqRel (T,x1)),Q) is Element of (pi_1 (T,x1)) by EQREL_1:def_3; then consider L being Loop of x1 such that A6: Class ((EqRel (T,x1)),Q) = Class ((EqRel (T,x1)),L) and A7: f . (Class ((EqRel (T,x1)),Q)) = Class ((EqRel (T,x0)),((P + L) + (- P))) by A5; A8: - P, - P are_homotopic by A1, BORSUK_2:12; L,Q are_homotopic by A6, Th46; then P + L,P + Q are_homotopic by A1, A2, BORSUK_6:75; then (P + L) + (- P),(P + Q) + (- P) are_homotopic by A1, A8, BORSUK_6:75; hence f . (Class ((EqRel (T,x1)),Q)) = Class ((EqRel (T,x0)),((P + Q) + (- P))) by A7, Th46; ::_thesis: verum end; uniqueness for b1, b2 being Function of (pi_1 (T,x1)),(pi_1 (T,x0)) st ( for Q being Loop of x1 holds b1 . (Class ((EqRel (T,x1)),Q)) = Class ((EqRel (T,x0)),((P + Q) + (- P))) ) & ( for Q being Loop of x1 holds b2 . (Class ((EqRel (T,x1)),Q)) = Class ((EqRel (T,x0)),((P + Q) + (- P))) ) holds b1 = b2 proof let f1, f2 be Function of (pi_1 (T,x1)),(pi_1 (T,x0)); ::_thesis: ( ( for Q being Loop of x1 holds f1 . (Class ((EqRel (T,x1)),Q)) = Class ((EqRel (T,x0)),((P + Q) + (- P))) ) & ( for Q being Loop of x1 holds f2 . (Class ((EqRel (T,x1)),Q)) = Class ((EqRel (T,x0)),((P + Q) + (- P))) ) implies f1 = f2 ) assume that A9: for Q being Loop of x1 holds f1 . (Class ((EqRel (T,x1)),Q)) = Class ((EqRel (T,x0)),((P + Q) + (- P))) and A10: for Q being Loop of x1 holds f2 . (Class ((EqRel (T,x1)),Q)) = Class ((EqRel (T,x0)),((P + Q) + (- P))) ; ::_thesis: f1 = f2 for x being Element of (pi_1 (T,x1)) holds f1 . x = f2 . x proof let x be Element of (pi_1 (T,x1)); ::_thesis: f1 . x = f2 . x consider L being Loop of x1 such that A11: x = Class ((EqRel (T,x1)),L) by Th47; thus f1 . x = Class ((EqRel (T,x0)),((P + L) + (- P))) by A9, A11 .= f2 . x by A10, A11 ; ::_thesis: verum end; hence f1 = f2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def6 defines pi_1-iso TOPALG_1:def_6_:_ for T being non empty TopSpace for x0, x1 being Point of T for P being Path of x0,x1 st x0,x1 are_connected holds for b5 being Function of (pi_1 (T,x1)),(pi_1 (T,x0)) holds ( b5 = pi_1-iso P iff for Q being Loop of x1 holds b5 . (Class ((EqRel (T,x1)),Q)) = Class ((EqRel (T,x0)),((P + Q) + (- P))) ); theorem Th48: :: TOPALG_1:48 for X being non empty TopSpace for x0, x1 being Point of X for P, Q being Path of x0,x1 st x0,x1 are_connected & P,Q are_homotopic holds pi_1-iso P = pi_1-iso Q proof let X be non empty TopSpace; ::_thesis: for x0, x1 being Point of X for P, Q being Path of x0,x1 st x0,x1 are_connected & P,Q are_homotopic holds pi_1-iso P = pi_1-iso Q let x0, x1 be Point of X; ::_thesis: for P, Q being Path of x0,x1 st x0,x1 are_connected & P,Q are_homotopic holds pi_1-iso P = pi_1-iso Q let P, Q be Path of x0,x1; ::_thesis: ( x0,x1 are_connected & P,Q are_homotopic implies pi_1-iso P = pi_1-iso Q ) assume that A1: x0,x1 are_connected and A2: P,Q are_homotopic ; ::_thesis: pi_1-iso P = pi_1-iso Q for x being Element of (pi_1 (X,x1)) holds (pi_1-iso P) . x = (pi_1-iso Q) . x proof A3: - P, - Q are_homotopic by A1, A2, BORSUK_6:77; let x be Element of (pi_1 (X,x1)); ::_thesis: (pi_1-iso P) . x = (pi_1-iso Q) . x consider L being Loop of x1 such that A4: x = Class ((EqRel (X,x1)),L) by Th47; L,L are_homotopic by BORSUK_2:12; then P + L,Q + L are_homotopic by A1, A2, BORSUK_6:75; then A5: (P + L) + (- P),(Q + L) + (- Q) are_homotopic by A1, A3, BORSUK_6:75; thus (pi_1-iso P) . x = Class ((EqRel (X,x0)),((P + L) + (- P))) by A1, A4, Def6 .= Class ((EqRel (X,x0)),((Q + L) + (- Q))) by A5, Th46 .= (pi_1-iso Q) . x by A1, A4, Def6 ; ::_thesis: verum end; hence pi_1-iso P = pi_1-iso Q by FUNCT_2:63; ::_thesis: verum end; theorem :: TOPALG_1:49 for T being non empty pathwise_connected TopSpace for y0, y1 being Point of T for R, V being Path of y0,y1 st R,V are_homotopic holds pi_1-iso R = pi_1-iso V proof let T be non empty pathwise_connected TopSpace; ::_thesis: for y0, y1 being Point of T for R, V being Path of y0,y1 st R,V are_homotopic holds pi_1-iso R = pi_1-iso V let y0, y1 be Point of T; ::_thesis: for R, V being Path of y0,y1 st R,V are_homotopic holds pi_1-iso R = pi_1-iso V let R, V be Path of y0,y1; ::_thesis: ( R,V are_homotopic implies pi_1-iso R = pi_1-iso V ) y0,y1 are_connected by BORSUK_2:def_3; hence ( R,V are_homotopic implies pi_1-iso R = pi_1-iso V ) by Th48; ::_thesis: verum end; theorem Th50: :: TOPALG_1:50 for X being non empty TopSpace for x0, x1 being Point of X for P being Path of x0,x1 st x0,x1 are_connected holds pi_1-iso P is Homomorphism of (pi_1 (X,x1)),(pi_1 (X,x0)) proof let X be non empty TopSpace; ::_thesis: for x0, x1 being Point of X for P being Path of x0,x1 st x0,x1 are_connected holds pi_1-iso P is Homomorphism of (pi_1 (X,x1)),(pi_1 (X,x0)) let x0, x1 be Point of X; ::_thesis: for P being Path of x0,x1 st x0,x1 are_connected holds pi_1-iso P is Homomorphism of (pi_1 (X,x1)),(pi_1 (X,x0)) let P be Path of x0,x1; ::_thesis: ( x0,x1 are_connected implies pi_1-iso P is Homomorphism of (pi_1 (X,x1)),(pi_1 (X,x0)) ) set f = pi_1-iso P; assume A1: x0,x1 are_connected ; ::_thesis: pi_1-iso P is Homomorphism of (pi_1 (X,x1)),(pi_1 (X,x0)) now__::_thesis:_for_x,_y_being_Element_of_(pi_1_(X,x1))_holds_(pi_1-iso_P)_._(x_*_y)_=_((pi_1-iso_P)_._x)_*_((pi_1-iso_P)_._y) let x, y be Element of (pi_1 (X,x1)); ::_thesis: (pi_1-iso P) . (x * y) = ((pi_1-iso P) . x) * ((pi_1-iso P) . y) consider A being Loop of x1 such that A2: x = Class ((EqRel (X,x1)),A) by Th47; consider B being Loop of x1 such that A3: y = Class ((EqRel (X,x1)),B) by Th47; consider D being Loop of x0 such that A4: (pi_1-iso P) . y = Class ((EqRel (X,x0)),D) by Th47; (pi_1-iso P) . y = Class ((EqRel (X,x0)),((P + B) + (- P))) by A1, A3, Def6; then A5: D,(P + B) + (- P) are_homotopic by A4, Th46; A6: (P + (A + B)) + (- P),((P + A) + (- P)) + ((P + B) + (- P)) are_homotopic by A1, Th43; consider C being Loop of x0 such that A7: (pi_1-iso P) . x = Class ((EqRel (X,x0)),C) by Th47; (pi_1-iso P) . x = Class ((EqRel (X,x0)),((P + A) + (- P))) by A1, A2, Def6; then C,(P + A) + (- P) are_homotopic by A7, Th46; then C + D,((P + A) + (- P)) + ((P + B) + (- P)) are_homotopic by A5, BORSUK_6:75; then A8: (P + (A + B)) + (- P),C + D are_homotopic by A6, BORSUK_6:79; thus (pi_1-iso P) . (x * y) = (pi_1-iso P) . (Class ((EqRel (X,x1)),(A + B))) by A2, A3, Lm4 .= Class ((EqRel (X,x0)),((P + (A + B)) + (- P))) by A1, Def6 .= Class ((EqRel (X,x0)),(C + D)) by A8, Th46 .= ((pi_1-iso P) . x) * ((pi_1-iso P) . y) by A7, A4, Lm4 ; ::_thesis: verum end; hence pi_1-iso P is Homomorphism of (pi_1 (X,x1)),(pi_1 (X,x0)) by GROUP_6:def_6; ::_thesis: verum end; registration let T be non empty pathwise_connected TopSpace; let x0, x1 be Point of T; let P be Path of x0,x1; cluster pi_1-iso P -> multiplicative ; coherence pi_1-iso P is multiplicative proof x0,x1 are_connected by BORSUK_2:def_3; hence pi_1-iso P is multiplicative by Th50; ::_thesis: verum end; end; theorem Th51: :: TOPALG_1:51 for X being non empty TopSpace for x0, x1 being Point of X for P being Path of x0,x1 st x0,x1 are_connected holds pi_1-iso P is one-to-one proof let X be non empty TopSpace; ::_thesis: for x0, x1 being Point of X for P being Path of x0,x1 st x0,x1 are_connected holds pi_1-iso P is one-to-one let x0, x1 be Point of X; ::_thesis: for P being Path of x0,x1 st x0,x1 are_connected holds pi_1-iso P is one-to-one let P be Path of x0,x1; ::_thesis: ( x0,x1 are_connected implies pi_1-iso P is one-to-one ) assume A1: x0,x1 are_connected ; ::_thesis: pi_1-iso P is one-to-one set f = pi_1-iso P; let a, b be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not a in K48((pi_1-iso P)) or not b in K48((pi_1-iso P)) or not (pi_1-iso P) . a = (pi_1-iso P) . b or a = b ) assume that A2: a in dom (pi_1-iso P) and A3: b in dom (pi_1-iso P) and A4: (pi_1-iso P) . a = (pi_1-iso P) . b ; ::_thesis: a = b consider B being Loop of x1 such that A5: b = Class ((EqRel (X,x1)),B) by A3, Th47; A6: (pi_1-iso P) . b = Class ((EqRel (X,x0)),((P + B) + (- P))) by A1, A5, Def6; consider A being Loop of x1 such that A7: a = Class ((EqRel (X,x1)),A) by A2, Th47; (pi_1-iso P) . a = Class ((EqRel (X,x0)),((P + A) + (- P))) by A1, A7, Def6; then (P + A) + (- P),(P + B) + (- P) are_homotopic by A4, A6, Th46; then P + A,P + B are_homotopic by A1, Th27; then A,B are_homotopic by A1, Th29; hence a = b by A7, A5, Th46; ::_thesis: verum end; theorem Th52: :: TOPALG_1:52 for X being non empty TopSpace for x0, x1 being Point of X for P being Path of x0,x1 st x0,x1 are_connected holds pi_1-iso P is onto proof let X be non empty TopSpace; ::_thesis: for x0, x1 being Point of X for P being Path of x0,x1 st x0,x1 are_connected holds pi_1-iso P is onto let x0, x1 be Point of X; ::_thesis: for P being Path of x0,x1 st x0,x1 are_connected holds pi_1-iso P is onto let P be Path of x0,x1; ::_thesis: ( x0,x1 are_connected implies pi_1-iso P is onto ) assume A1: x0,x1 are_connected ; ::_thesis: pi_1-iso P is onto set f = pi_1-iso P; thus rng (pi_1-iso P) c= the carrier of (pi_1 (X,x0)) ; :: according to XBOOLE_0:def_10,FUNCT_2:def_3 ::_thesis: the carrier of (pi_1 (X,x0)) c= rng (pi_1-iso P) let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in the carrier of (pi_1 (X,x0)) or y in rng (pi_1-iso P) ) assume y in the carrier of (pi_1 (X,x0)) ; ::_thesis: y in rng (pi_1-iso P) then consider Y being Loop of x0 such that A2: y = Class ((EqRel (X,x0)),Y) by Th47; A3: (P + (((- P) + Y) + P)) + (- P),Y are_homotopic by A1, Th41; set Z = Class ((EqRel (X,x1)),(((- P) + Y) + P)); dom (pi_1-iso P) = the carrier of (pi_1 (X,x1)) by FUNCT_2:def_1; then A4: Class ((EqRel (X,x1)),(((- P) + Y) + P)) in dom (pi_1-iso P) by Th47; (pi_1-iso P) . (Class ((EqRel (X,x1)),(((- P) + Y) + P))) = Class ((EqRel (X,x0)),((P + (((- P) + Y) + P)) + (- P))) by A1, Def6 .= y by A2, A3, Th46 ; hence y in rng (pi_1-iso P) by A4, FUNCT_1:def_3; ::_thesis: verum end; registration let T be non empty pathwise_connected TopSpace; let x0, x1 be Point of T; let P be Path of x0,x1; cluster pi_1-iso P -> one-to-one onto ; coherence ( pi_1-iso P is one-to-one & pi_1-iso P is onto ) proof x0,x1 are_connected by BORSUK_2:def_3; hence ( pi_1-iso P is one-to-one & pi_1-iso P is onto ) by Th51, Th52; ::_thesis: verum end; end; theorem Th53: :: TOPALG_1:53 for X being non empty TopSpace for x0, x1 being Point of X for P being Path of x0,x1 st x0,x1 are_connected holds (pi_1-iso P) " = pi_1-iso (- P) proof let X be non empty TopSpace; ::_thesis: for x0, x1 being Point of X for P being Path of x0,x1 st x0,x1 are_connected holds (pi_1-iso P) " = pi_1-iso (- P) let x0, x1 be Point of X; ::_thesis: for P being Path of x0,x1 st x0,x1 are_connected holds (pi_1-iso P) " = pi_1-iso (- P) let P be Path of x0,x1; ::_thesis: ( x0,x1 are_connected implies (pi_1-iso P) " = pi_1-iso (- P) ) set f = pi_1-iso P; set g = pi_1-iso (- P); assume A1: x0,x1 are_connected ; ::_thesis: (pi_1-iso P) " = pi_1-iso (- P) then ( pi_1-iso P is one-to-one & pi_1-iso P is onto ) by Th51, Th52; then A2: (pi_1-iso P) " = (pi_1-iso P) " by TOPS_2:def_4; A3: pi_1-iso P is one-to-one by A1, Th51; for x being Element of (pi_1 (X,x0)) holds ((pi_1-iso P) ") . x = (pi_1-iso (- P)) . x proof let x be Element of (pi_1 (X,x0)); ::_thesis: ((pi_1-iso P) ") . x = (pi_1-iso (- P)) . x consider Q being Loop of x0 such that A4: x = Class ((EqRel (X,x0)),Q) by Th47; - (- P) = P by A1, BORSUK_6:43; then A5: (P + (((- P) + Q) + (- (- P)))) + (- P),Q are_homotopic by A1, Th41; dom (pi_1-iso P) = the carrier of (pi_1 (X,x1)) by FUNCT_2:def_1; then A6: Class ((EqRel (X,x1)),(((- P) + Q) + (- (- P)))) in dom (pi_1-iso P) by Th47; (pi_1-iso P) . (Class ((EqRel (X,x1)),(((- P) + Q) + (- (- P))))) = Class ((EqRel (X,x0)),((P + (((- P) + Q) + (- (- P)))) + (- P))) by A1, Def6 .= x by A4, A5, Th46 ; hence ((pi_1-iso P) ") . x = Class ((EqRel (X,x1)),(((- P) + Q) + (- (- P)))) by A3, A2, A6, FUNCT_1:32 .= (pi_1-iso (- P)) . x by A1, A4, Def6 ; ::_thesis: verum end; hence (pi_1-iso P) " = pi_1-iso (- P) by FUNCT_2:63; ::_thesis: verum end; theorem :: TOPALG_1:54 for T being non empty pathwise_connected TopSpace for y0, y1 being Point of T for R being Path of y0,y1 holds (pi_1-iso R) " = pi_1-iso (- R) proof let T be non empty pathwise_connected TopSpace; ::_thesis: for y0, y1 being Point of T for R being Path of y0,y1 holds (pi_1-iso R) " = pi_1-iso (- R) let y0, y1 be Point of T; ::_thesis: for R being Path of y0,y1 holds (pi_1-iso R) " = pi_1-iso (- R) let R be Path of y0,y1; ::_thesis: (pi_1-iso R) " = pi_1-iso (- R) y0,y1 are_connected by BORSUK_2:def_3; hence (pi_1-iso R) " = pi_1-iso (- R) by Th53; ::_thesis: verum end; theorem Th55: :: TOPALG_1:55 for X being non empty TopSpace for x0, x1 being Point of X for P being Path of x0,x1 st x0,x1 are_connected holds for h being Homomorphism of (pi_1 (X,x1)),(pi_1 (X,x0)) st h = pi_1-iso P holds h is bijective proof let X be non empty TopSpace; ::_thesis: for x0, x1 being Point of X for P being Path of x0,x1 st x0,x1 are_connected holds for h being Homomorphism of (pi_1 (X,x1)),(pi_1 (X,x0)) st h = pi_1-iso P holds h is bijective let x0, x1 be Point of X; ::_thesis: for P being Path of x0,x1 st x0,x1 are_connected holds for h being Homomorphism of (pi_1 (X,x1)),(pi_1 (X,x0)) st h = pi_1-iso P holds h is bijective let P be Path of x0,x1; ::_thesis: ( x0,x1 are_connected implies for h being Homomorphism of (pi_1 (X,x1)),(pi_1 (X,x0)) st h = pi_1-iso P holds h is bijective ) assume A1: x0,x1 are_connected ; ::_thesis: for h being Homomorphism of (pi_1 (X,x1)),(pi_1 (X,x0)) st h = pi_1-iso P holds h is bijective let h be Homomorphism of (pi_1 (X,x1)),(pi_1 (X,x0)); ::_thesis: ( h = pi_1-iso P implies h is bijective ) assume h = pi_1-iso P ; ::_thesis: h is bijective then ( h is one-to-one & h is onto ) by A1, Th51, Th52; hence h is bijective ; ::_thesis: verum end; theorem :: TOPALG_1:56 for T being non empty pathwise_connected TopSpace for y0, y1 being Point of T for R being Path of y0,y1 holds pi_1-iso R is bijective ; theorem :: TOPALG_1:57 for X being non empty TopSpace for x0, x1 being Point of X st x0,x1 are_connected holds pi_1 (X,x0), pi_1 (X,x1) are_isomorphic proof let X be non empty TopSpace; ::_thesis: for x0, x1 being Point of X st x0,x1 are_connected holds pi_1 (X,x0), pi_1 (X,x1) are_isomorphic let x0, x1 be Point of X; ::_thesis: ( x0,x1 are_connected implies pi_1 (X,x0), pi_1 (X,x1) are_isomorphic ) set P = the Path of x1,x0; assume A1: x0,x1 are_connected ; ::_thesis: pi_1 (X,x0), pi_1 (X,x1) are_isomorphic then reconsider h = pi_1-iso the Path of x1,x0 as Homomorphism of (pi_1 (X,x0)),(pi_1 (X,x1)) by Th50; take h ; :: according to GROUP_6:def_11 ::_thesis: h is bijective thus h is bijective by A1, Th55; ::_thesis: verum end; theorem :: TOPALG_1:58 for T being non empty pathwise_connected TopSpace for y0, y1 being Point of T holds pi_1 (T,y0), pi_1 (T,y1) are_isomorphic proof let T be non empty pathwise_connected TopSpace; ::_thesis: for y0, y1 being Point of T holds pi_1 (T,y0), pi_1 (T,y1) are_isomorphic let y0, y1 be Point of T; ::_thesis: pi_1 (T,y0), pi_1 (T,y1) are_isomorphic set R = the Path of y1,y0; take pi_1-iso the Path of y1,y0 ; :: according to GROUP_6:def_11 ::_thesis: pi_1-iso the Path of y1,y0 is bijective thus pi_1-iso the Path of y1,y0 is bijective ; ::_thesis: verum end; begin definition let n be Nat; let P, Q be Function of I[01],(TOP-REAL n); func RealHomotopy (P,Q) -> Function of [:I[01],I[01]:],(TOP-REAL n) means :Def7: :: TOPALG_1:def 7 for s, t being Element of I[01] holds it . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)); existence ex b1 being Function of [:I[01],I[01]:],(TOP-REAL n) st for s, t being Element of I[01] holds b1 . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) proof set I = the carrier of I[01]; deffunc H1( Element of the carrier of I[01], Element of the carrier of I[01]) -> Element of the carrier of (TOP-REAL n) = ((1 - \$2) * (P . \$1)) + (\$2 * (Q . \$1)); consider F being Function of [: the carrier of I[01], the carrier of I[01]:], the carrier of (TOP-REAL n) such that A1: for x, y being Element of the carrier of I[01] holds F . (x,y) = H1(x,y) from BINOP_1:sch_4(); 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 [:I[01],I[01]:],(TOP-REAL n) ; take F ; ::_thesis: for s, t being Element of I[01] holds F . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) let x, y be Element of the carrier of I[01]; ::_thesis: F . (x,y) = ((1 - y) * (P . x)) + (y * (Q . x)) thus F . (x,y) = ((1 - y) * (P . x)) + (y * (Q . x)) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Function of [:I[01],I[01]:],(TOP-REAL n) st ( for s, t being Element of I[01] holds b1 . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) ) & ( for s, t being Element of I[01] holds b2 . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) ) holds b1 = b2 proof set I = the carrier of I[01]; let f, g be Function of [:I[01],I[01]:],(TOP-REAL n); ::_thesis: ( ( for s, t being Element of I[01] holds f . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) ) & ( for s, t being Element of I[01] holds g . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) ) implies f = g ) assume that A2: for s, t being Element of I[01] holds f . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) and A3: for s, t being Element of I[01] holds g . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) ; ::_thesis: f = g A4: for s, t being Element of the carrier of I[01] holds f . (s,t) = g . (s,t) proof let s, t be Element of the carrier of I[01]; ::_thesis: f . (s,t) = g . (s,t) thus f . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) by A2 .= g . (s,t) by A3 ; ::_thesis: verum end; the carrier of [:I[01],I[01]:] = [: the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def_2; hence f = g by A4, BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def7 defines RealHomotopy TOPALG_1:def_7_:_ for n being Nat for P, Q being Function of I[01],(TOP-REAL n) for b4 being Function of [:I[01],I[01]:],(TOP-REAL n) holds ( b4 = RealHomotopy (P,Q) iff for s, t being Element of I[01] holds b4 . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) ); Lm5: for n being Nat for P, Q being continuous Function of I[01],(TOP-REAL n) holds RealHomotopy (P,Q) is continuous proof let n be Nat; ::_thesis: for P, Q being continuous Function of I[01],(TOP-REAL n) holds RealHomotopy (P,Q) is continuous set I = the carrier of I[01]; let P, Q be continuous Function of I[01],(TOP-REAL n); ::_thesis: RealHomotopy (P,Q) is continuous set F = RealHomotopy (P,Q); set T = the carrier of (TOP-REAL n); set PI = [:P,(id I[01]):]; set QI = [:Q,(id I[01]):]; deffunc H1( Element of (TOP-REAL n), Element of the carrier of I[01]) -> Element of the carrier of (TOP-REAL n) = \$2 * \$1; deffunc H2( Element of (TOP-REAL n), Element of the carrier of I[01]) -> Element of the carrier of (TOP-REAL n) = (1 - \$2) * \$1; consider Pa being Function of [: the carrier of (TOP-REAL n), the carrier of I[01]:], the carrier of (TOP-REAL n) such that A1: for x being Element of the carrier of (TOP-REAL n) for i being Element of the carrier of I[01] holds Pa . (x,i) = H2(x,i) from BINOP_1:sch_4(); consider Pb being Function of [: the carrier of (TOP-REAL n), the carrier of I[01]:], the carrier of (TOP-REAL n) such that A2: for x being Element of the carrier of (TOP-REAL n) for i being Element of the carrier of I[01] holds Pb . (x,i) = H1(x,i) from BINOP_1:sch_4(); the carrier of [:(TOP-REAL n),I[01]:] = [: the carrier of (TOP-REAL n), the carrier of I[01]:] by BORSUK_1:def_2; then reconsider Pa = Pa, Pb = Pb as Function of [:(TOP-REAL n),I[01]:],(TOP-REAL n) ; A3: Pb is continuous by A2, Th18; A4: for p being Point of [:I[01],I[01]:] holds (RealHomotopy (P,Q)) . p = ((Pa * [:P,(id I[01]):]) . p) + ((Pb * [:Q,(id I[01]):]) . p) proof A5: dom Q = the carrier of I[01] by FUNCT_2:def_1; A6: dom P = the carrier of I[01] by FUNCT_2:def_1; let p be Point of [:I[01],I[01]:]; ::_thesis: (RealHomotopy (P,Q)) . p = ((Pa * [:P,(id I[01]):]) . p) + ((Pb * [:Q,(id I[01]):]) . p) consider s, t being Point of I[01] such that A7: p = [s,t] by BORSUK_1:10; A8: ( dom (id I[01]) = the carrier of I[01] & (id I[01]) . t = t ) by FUNCT_1:18, FUNCT_2:def_1; A9: (Pb * [:Q,(id I[01]):]) . p = Pb . ([:Q,(id I[01]):] . (s,t)) by A7, FUNCT_2:15 .= Pb . ((Q . s),t) by A5, A8, FUNCT_3:def_8 .= t * (Q . s) by A2 ; A10: (Pa * [:P,(id I[01]):]) . p = Pa . ([:P,(id I[01]):] . (s,t)) by A7, FUNCT_2:15 .= Pa . ((P . s),t) by A6, A8, FUNCT_3:def_8 .= (1 - t) * (P . s) by A1 ; thus (RealHomotopy (P,Q)) . p = (RealHomotopy (P,Q)) . (s,t) by A7 .= ((Pa * [:P,(id I[01]):]) . p) + ((Pb * [:Q,(id I[01]):]) . p) by A10, A9, Def7 ; ::_thesis: verum end; Pa is continuous by A1, Th17; hence RealHomotopy (P,Q) is continuous by A3, A4, Lm1; ::_thesis: verum end; Lm6: for n being Nat for a, b being Point of (TOP-REAL n) for P, Q being Path of a,b for s being Point of I[01] holds ( (RealHomotopy (P,Q)) . (s,0) = P . s & (RealHomotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds ( (RealHomotopy (P,Q)) . (0,t) = a & (RealHomotopy (P,Q)) . (1,t) = b ) ) ) proof let n be Nat; ::_thesis: for a, b being Point of (TOP-REAL n) for P, Q being Path of a,b for s being Point of I[01] holds ( (RealHomotopy (P,Q)) . (s,0) = P . s & (RealHomotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds ( (RealHomotopy (P,Q)) . (0,t) = a & (RealHomotopy (P,Q)) . (1,t) = b ) ) ) let a, b be Point of (TOP-REAL n); ::_thesis: for P, Q being Path of a,b for s being Point of I[01] holds ( (RealHomotopy (P,Q)) . (s,0) = P . s & (RealHomotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds ( (RealHomotopy (P,Q)) . (0,t) = a & (RealHomotopy (P,Q)) . (1,t) = b ) ) ) let P, Q be Path of a,b; ::_thesis: for s being Point of I[01] holds ( (RealHomotopy (P,Q)) . (s,0) = P . s & (RealHomotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds ( (RealHomotopy (P,Q)) . (0,t) = a & (RealHomotopy (P,Q)) . (1,t) = b ) ) ) set F = RealHomotopy (P,Q); let s be Point of I[01]; ::_thesis: ( (RealHomotopy (P,Q)) . (s,0) = P . s & (RealHomotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds ( (RealHomotopy (P,Q)) . (0,t) = a & (RealHomotopy (P,Q)) . (1,t) = b ) ) ) thus (RealHomotopy (P,Q)) . (s,0) = ((1 - 0) * (P . s)) + (0 * (Q . s)) by Def7, BORSUK_1:def_14 .= (P . s) + (0 * (Q . s)) by EUCLID:29 .= (P . s) + (0. (TOP-REAL n)) by EUCLID:29 .= P . s by EUCLID:27 ; ::_thesis: ( (RealHomotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds ( (RealHomotopy (P,Q)) . (0,t) = a & (RealHomotopy (P,Q)) . (1,t) = b ) ) ) thus (RealHomotopy (P,Q)) . (s,1) = ((1 - 1) * (P . s)) + (1 * (Q . s)) by Def7, BORSUK_1:def_15 .= (0. (TOP-REAL n)) + (1 * (Q . s)) by EUCLID:29 .= (0. (TOP-REAL n)) + (Q . s) by EUCLID:29 .= Q . s by EUCLID:27 ; ::_thesis: for t being Point of I[01] holds ( (RealHomotopy (P,Q)) . (0,t) = a & (RealHomotopy (P,Q)) . (1,t) = b ) let t be Point of I[01]; ::_thesis: ( (RealHomotopy (P,Q)) . (0,t) = a & (RealHomotopy (P,Q)) . (1,t) = b ) A1: n in NAT by ORDINAL1:def_12; then A2: ( P . 0[01] = a & Q . 0[01] = a ) by BORSUK_2:def_4; thus (RealHomotopy (P,Q)) . (0,t) = ((1 - t) * (P . 0[01])) + (t * (Q . 0[01])) by Def7 .= ((1 * a) - (t * a)) + (t * a) by A2, EUCLID:50 .= 1 * a by EUCLID:48 .= a by EUCLID:29 ; ::_thesis: (RealHomotopy (P,Q)) . (1,t) = b A3: ( P . 1[01] = b & Q . 1[01] = b ) by A1, BORSUK_2:def_4; thus (RealHomotopy (P,Q)) . (1,t) = ((1 - t) * (P . 1[01])) + (t * (Q . 1[01])) by Def7 .= ((1 * b) - (t * b)) + (t * b) by A3, EUCLID:50 .= 1 * b by EUCLID:48 .= b by EUCLID:29 ; ::_thesis: verum end; theorem Th59: :: TOPALG_1:59 for n being Nat for a, b being Point of (TOP-REAL n) for P, Q being Path of a,b holds P,Q are_homotopic proof let n be Nat; ::_thesis: for a, b being Point of (TOP-REAL n) for P, Q being Path of a,b holds P,Q are_homotopic let a, b be Point of (TOP-REAL n); ::_thesis: for P, Q being Path of a,b holds P,Q are_homotopic let P, Q be Path of a,b; ::_thesis: P,Q are_homotopic take F = RealHomotopy (P,Q); :: according to BORSUK_2:def_7 ::_thesis: ( F is continuous & ( for b1 being Element of the carrier of K543() holds ( F . (b1,0) = P . b1 & F . (b1,1) = Q . b1 & F . (0,b1) = a & F . (1,b1) = b ) ) ) A1: n in NAT by ORDINAL1:def_12; then P is continuous ; hence F is continuous by A1, Lm5; ::_thesis: for b1 being Element of the carrier of K543() holds ( F . (b1,0) = P . b1 & F . (b1,1) = Q . b1 & F . (0,b1) = a & F . (1,b1) = b ) thus for b1 being Element of the carrier of K543() holds ( F . (b1,0) = P . b1 & F . (b1,1) = Q . b1 & F . (0,b1) = a & F . (1,b1) = b ) by Lm6; ::_thesis: verum end; registration let n be Nat; let a, b be Point of (TOP-REAL n); let P, Q be Path of a,b; cluster -> continuous for Homotopy of P,Q; coherence for b1 being Homotopy of P,Q holds b1 is continuous proof let F be Homotopy of P,Q; ::_thesis: F is continuous P,Q are_homotopic by Th59; hence F is continuous by BORSUK_6:def_11; ::_thesis: verum end; end; theorem Th60: :: TOPALG_1:60 for n being Nat for a being Point of (TOP-REAL n) for C being Loop of a holds the carrier of (pi_1 ((TOP-REAL n),a)) = {(Class ((EqRel ((TOP-REAL n),a)),C))} proof let n be Nat; ::_thesis: for a being Point of (TOP-REAL n) for C being Loop of a holds the carrier of (pi_1 ((TOP-REAL n),a)) = {(Class ((EqRel ((TOP-REAL n),a)),C))} let a be Point of (TOP-REAL n); ::_thesis: for C being Loop of a holds the carrier of (pi_1 ((TOP-REAL n),a)) = {(Class ((EqRel ((TOP-REAL n),a)),C))} let C be Loop of a; ::_thesis: the carrier of (pi_1 ((TOP-REAL n),a)) = {(Class ((EqRel ((TOP-REAL n),a)),C))} set X = TOP-REAL n; set E = EqRel ((TOP-REAL n),a); hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {(Class ((EqRel ((TOP-REAL n),a)),C))} c= the carrier of (pi_1 ((TOP-REAL n),a)) let x be set ; ::_thesis: ( x in the carrier of (pi_1 ((TOP-REAL n),a)) implies x in {(Class ((EqRel ((TOP-REAL n),a)),C))} ) assume x in the carrier of (pi_1 ((TOP-REAL n),a)) ; ::_thesis: x in {(Class ((EqRel ((TOP-REAL n),a)),C))} then consider P being Loop of a such that A1: x = Class ((EqRel ((TOP-REAL n),a)),P) by Th47; P,C are_homotopic by Th59; then x = Class ((EqRel ((TOP-REAL n),a)),C) by A1, Th46; hence x in {(Class ((EqRel ((TOP-REAL n),a)),C))} by TARSKI:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(Class ((EqRel ((TOP-REAL n),a)),C))} or x in the carrier of (pi_1 ((TOP-REAL n),a)) ) assume x in {(Class ((EqRel ((TOP-REAL n),a)),C))} ; ::_thesis: x in the carrier of (pi_1 ((TOP-REAL n),a)) then A2: x = Class ((EqRel ((TOP-REAL n),a)),C) by TARSKI:def_1; C in Loops a by Def1; then x in Class (EqRel ((TOP-REAL n),a)) by A2, EQREL_1:def_3; hence x in the carrier of (pi_1 ((TOP-REAL n),a)) by Def5; ::_thesis: verum end; registration let n be Nat; let a be Point of (TOP-REAL n); cluster FundamentalGroup ((TOP-REAL n),a) -> trivial strict ; coherence pi_1 ((TOP-REAL n),a) is trivial proof set C = the constant Loop of a; set X = TOP-REAL n; set E = EqRel ((TOP-REAL n),a); the carrier of (pi_1 ((TOP-REAL n),a)) = Class (EqRel ((TOP-REAL n),a)) by Def5; then {(Class ((EqRel ((TOP-REAL n),a)), the constant Loop of a))} = Class (EqRel ((TOP-REAL n),a)) by Th60; hence pi_1 ((TOP-REAL n),a) is trivial by Def5; ::_thesis: verum end; end; theorem :: TOPALG_1:61 for S being non empty TopSpace for s being Point of S for x, y being Element of (pi_1 (S,s)) for P, Q being Loop of s st x = Class ((EqRel (S,s)),P) & y = Class ((EqRel (S,s)),Q) holds x * y = Class ((EqRel (S,s)),(P + Q)) by Lm4; theorem Th62: :: TOPALG_1:62 for X being non empty TopSpace for a being Point of X for C being constant Loop of a holds 1_ (pi_1 (X,a)) = Class ((EqRel (X,a)),C) proof let X be non empty TopSpace; ::_thesis: for a being Point of X for C being constant Loop of a holds 1_ (pi_1 (X,a)) = Class ((EqRel (X,a)),C) let a be Point of X; ::_thesis: for C being constant Loop of a holds 1_ (pi_1 (X,a)) = Class ((EqRel (X,a)),C) let C be constant Loop of a; ::_thesis: 1_ (pi_1 (X,a)) = Class ((EqRel (X,a)),C) set G = pi_1 (X,a); reconsider g = Class ((EqRel (X,a)),C) as Element of (pi_1 (X,a)) by Th47; set E = EqRel (X,a); now__::_thesis:_for_h_being_Element_of_(pi_1_(X,a))_holds_ (_h_*_g_=_h_&_g_*_h_=_h_) let h be Element of (pi_1 (X,a)); ::_thesis: ( h * g = h & g * h = h ) consider P being Loop of a such that A1: h = Class ((EqRel (X,a)),P) by Th47; A2: P,P + C are_homotopic by BORSUK_6:80; thus h * g = Class ((EqRel (X,a)),(P + C)) by A1, Lm4 .= h by A1, A2, Th46 ; ::_thesis: g * h = h A3: P,C + P are_homotopic by BORSUK_6:82; thus g * h = Class ((EqRel (X,a)),(C + P)) by A1, Lm4 .= h by A1, A3, Th46 ; ::_thesis: verum end; hence 1_ (pi_1 (X,a)) = Class ((EqRel (X,a)),C) by GROUP_1:4; ::_thesis: verum end; theorem :: TOPALG_1:63 for X being non empty TopSpace for a being Point of X for x, y being Element of (pi_1 (X,a)) for P being Loop of a st x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),(- P)) holds x " = y proof let X be non empty TopSpace; ::_thesis: for a being Point of X for x, y being Element of (pi_1 (X,a)) for P being Loop of a st x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),(- P)) holds x " = y let a be Point of X; ::_thesis: for x, y being Element of (pi_1 (X,a)) for P being Loop of a st x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),(- P)) holds x " = y set E = EqRel (X,a); set G = pi_1 (X,a); let x, y be Element of (pi_1 (X,a)); ::_thesis: for P being Loop of a st x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),(- P)) holds x " = y let P be Loop of a; ::_thesis: ( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),(- P)) implies x " = y ) assume A1: ( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),(- P)) ) ; ::_thesis: x " = y set C = the constant Loop of a; A2: (- P) + P, the constant Loop of a are_homotopic by BORSUK_6:86; A3: y * x = Class ((EqRel (X,a)),((- P) + P)) by A1, Lm4 .= Class ((EqRel (X,a)), the constant Loop of a) by A2, Th46 .= 1_ (pi_1 (X,a)) by Th62 ; A4: P + (- P), the constant Loop of a are_homotopic by BORSUK_6:84; x * y = Class ((EqRel (X,a)),(P + (- P))) by A1, Lm4 .= Class ((EqRel (X,a)), the constant Loop of a) by A4, Th46 .= 1_ (pi_1 (X,a)) by Th62 ; hence x " = y by A3, GROUP_1:def_5; ::_thesis: verum end; registration let n be Nat; let P, Q be continuous Function of I[01],(TOP-REAL n); cluster RealHomotopy (P,Q) -> continuous ; coherence RealHomotopy (P,Q) is continuous by Lm5; end; theorem :: TOPALG_1:64 for n being Nat for a, b being Point of (TOP-REAL n) for P, Q being Path of a,b holds RealHomotopy (P,Q) is Homotopy of P,Q proof let n be Nat; ::_thesis: for a, b being Point of (TOP-REAL n) for P, Q being Path of a,b holds RealHomotopy (P,Q) is Homotopy of P,Q let a, b be Point of (TOP-REAL n); ::_thesis: for P, Q being Path of a,b holds RealHomotopy (P,Q) is Homotopy of P,Q let P, Q be Path of a,b; ::_thesis: RealHomotopy (P,Q) is Homotopy of P,Q thus P,Q are_homotopic by Th59; :: according to BORSUK_6:def_11 ::_thesis: ( RealHomotopy (P,Q) is continuous & ( for b1 being Element of the carrier of K543() holds ( (RealHomotopy (P,Q)) . (b1,0) = P . b1 & (RealHomotopy (P,Q)) . (b1,1) = Q . b1 & (RealHomotopy (P,Q)) . (0,b1) = a & (RealHomotopy (P,Q)) . (1,b1) = b ) ) ) A1: n in NAT by ORDINAL1:def_12; then P is continuous ; hence RealHomotopy (P,Q) is continuous by A1; ::_thesis: for b1 being Element of the carrier of K543() holds ( (RealHomotopy (P,Q)) . (b1,0) = P . b1 & (RealHomotopy (P,Q)) . (b1,1) = Q . b1 & (RealHomotopy (P,Q)) . (0,b1) = a & (RealHomotopy (P,Q)) . (1,b1) = b ) thus for b1 being Element of the carrier of K543() holds ( (RealHomotopy (P,Q)) . (b1,0) = P . b1 & (RealHomotopy (P,Q)) . (b1,1) = Q . b1 & (RealHomotopy (P,Q)) . (0,b1) = a & (RealHomotopy (P,Q)) . (1,b1) = b ) by Lm6; ::_thesis: verum end; theorem :: TOPALG_1:65 for X being non empty TopSpace for a, b being Point of X st a,b are_connected holds ( not EqRel (X,a,b) is empty & EqRel (X,a,b) is total & EqRel (X,a,b) is symmetric & EqRel (X,a,b) is transitive ) by Lm3;