:: 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;