:: TOPALG_2 semantic presentation

begin


registration
let n be Element of NAT ;
cluster non empty convex for Element of bool the carrier of (TOP-REAL n);
existence
 ex b1 being Subset of (TOP-REAL n) st
( not b1 is empty & b1 is convex )
proof
set a = the Point of (TOP-REAL n);
take  LSeg ( the Point of (TOP-REAL n), the Point of (TOP-REAL n)) ; ::_thesis: ( not LSeg ( the Point of (TOP-REAL n), the Point of (TOP-REAL n)) is empty & LSeg ( the Point of (TOP-REAL n), the Point of (TOP-REAL n)) is convex )
thus  ( not LSeg ( the Point of (TOP-REAL n), the Point of (TOP-REAL n)) is empty & LSeg ( the Point of (TOP-REAL n), the Point of (TOP-REAL n)) is convex ) ; ::_thesis: verum
end;
end;

definition
let n be Element of NAT ;
let T be SubSpace of TOP-REAL n;
attrT is convex  means :Def1: :: TOPALG_2:def 1
 [#] T is convex Subset of (TOP-REAL n);
end;

:: deftheorem Def1 defines convex TOPALG_2:def_1_:_
 for n being Element of NAT
for T being SubSpace of TOP-REAL n holds
( T is convex iff [#] T is convex Subset of (TOP-REAL n) );

registration
let n be Element of NAT ;
cluster non empty convex  ->  non empty pathwise_connected for SubSpace of TOP-REAL n;
coherence
 for b1 being non empty SubSpace of TOP-REAL n st b1 is convex holds
b1 is pathwise_connected
proof
let T be non empty SubSpace of TOP-REAL n; ::_thesis: ( T is convex implies T is pathwise_connected )
assume A1: [#] T is convex Subset of (TOP-REAL n) ; :: according to TOPALG_2:def_1 ::_thesis: T is pathwise_connected
let a, b be Point of T; :: according to BORSUK_2:def_3 ::_thesis: a,b are_connected
A2: the carrier of T is Subset of (TOP-REAL n) by TSEP_1:1;
 ( a in the carrier of T & b in the carrier of T ) ;
then reconsider a1 = a, b1 = b as Point of (TOP-REAL n) by A2;
percases ( a1 <> b1 or a1 = b1 ) ;
supposeA3: a1 <> b1 ; ::_thesis: a,b are_connected
 [#] ((TOP-REAL n) | (LSeg (a1,b1))) = LSeg (a1,b1) by PRE_TOPC:def_5;
then A4: the carrier of ((TOP-REAL n) | (LSeg (a1,b1))) c= the carrier of T by A1, JORDAN1:def_1;
then A5: (TOP-REAL n) | (LSeg (a1,b1)) is SubSpace of T by TSEP_1:4;
 LSeg (a1,b1) is_an_arc_of a1,b1 by A3, TOPREAL1:9;
then consider h being Function of I[01],((TOP-REAL n) | (LSeg (a1,b1))) such that
A6: h is being_homeomorphism and
A7: ( h . 0 = a1 & h . 1 = b1 ) by TOPREAL1:def_1;
reconsider f = h as Function of I[01],T by A4, FUNCT_2:7;
take  f ; :: according to BORSUK_2:def_1 ::_thesis: ( f is continuous & f . 0 = a & f . 1 = b )
 h is continuous by A6, TOPS_2:def_5;
hence  f is continuous by A5, PRE_TOPC:26; ::_thesis: ( f . 0 = a & f . 1 = b )
thus  ( f . 0 = a & f . 1 = b ) by A7; ::_thesis: verum
end;
suppose a1 = b1 ; ::_thesis: a,b are_connected
hence  a,b are_connected ; ::_thesis: verum
end;
end;
end;
end;

registration
let n be Element of NAT ;
cluster non empty strict TopSpace-like convex for SubSpace of TOP-REAL n;
existence
 ex b1 being SubSpace of TOP-REAL n st
( b1 is strict & not b1 is empty & b1 is convex )
proof
 TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is SubSpace of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) by TSEP_1:2;
then reconsider T = TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) as SubSpace of TOP-REAL n by PRE_TOPC:35;
take  T ; ::_thesis: ( T is strict & not T is empty & T is convex )
thus  ( T is strict & not T is empty ) ; ::_thesis: T is convex
 [#] (TOP-REAL n) = [#] TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) ;
hence  [#] T is convex Subset of (TOP-REAL n) ; :: according to TOPALG_2:def_1 ::_thesis: verum
end;
end;

theorem :: TOPALG_2:1
for X being non empty TopSpace
for Y being non empty SubSpace of X
for x1, x2 being Point of X
for y1, y2 being Point of Y
for f being Path of y1,y2 st x1 = y1 & x2 = y2 & y1,y2 are_connected holds
f is Path of x1,x2
proof
let X be non empty TopSpace; ::_thesis: for Y being non empty SubSpace of X
for x1, x2 being Point of X
for y1, y2 being Point of Y
for f being Path of y1,y2 st x1 = y1 & x2 = y2 & y1,y2 are_connected holds
f is Path of x1,x2
let Y be non empty SubSpace of X; ::_thesis: for x1, x2 being Point of X
for y1, y2 being Point of Y
for f being Path of y1,y2 st x1 = y1 & x2 = y2 & y1,y2 are_connected holds
f is Path of x1,x2
let x1, x2 be Point of X; ::_thesis: for y1, y2 being Point of Y
for f being Path of y1,y2 st x1 = y1 & x2 = y2 & y1,y2 are_connected holds
f is Path of x1,x2
let y1, y2 be Point of Y; ::_thesis: for f being Path of y1,y2 st x1 = y1 & x2 = y2 & y1,y2 are_connected holds
f is Path of x1,x2
let f be Path of y1,y2; ::_thesis: ( x1 = y1 & x2 = y2 & y1,y2 are_connected implies f is Path of x1,x2 )
assume that
A1: ( x1 = y1 & x2 = y2 ) and
A2: y1,y2 are_connected ; ::_thesis: f is Path of x1,x2
 the carrier of Y is Subset of X by TSEP_1:1;
then reconsider g = f as Function of I[01],X by FUNCT_2:7;
 f is continuous by A2, BORSUK_2:def_2;
then A3: g is continuous by PRE_TOPC:26;
A4: ( g . 0 = x1 & g . 1 = x2 ) by A1, A2, BORSUK_2:def_2;
then  x1,x2 are_connected by A3, BORSUK_2:def_1;
hence  f is Path of x1,x2 by A4, A3, BORSUK_2:def_2; ::_thesis: verum
end;

set I = the carrier of I[01];

Lm1:  the carrier of [:I[01],I[01]:] = [: the carrier of I[01], the carrier of I[01]:]
by BORSUK_1:def_2;

Lm2:  the carrier of [:(TOP-REAL 1),I[01]:] = [: the carrier of (TOP-REAL 1), the carrier of I[01]:]
by BORSUK_1:def_2;

Lm3:  the carrier of [:R^1,I[01]:] = [: the carrier of R^1, the carrier of I[01]:]
by BORSUK_1:def_2;

Lm4:  dom (id I[01]) = the carrier of I[01]
by FUNCT_2:def_1;

definition
let n be Element of NAT ;
let T be non empty convex SubSpace of TOP-REAL n;
let P, Q be Function of I[01],T;
func ConvexHomotopy (P,Q) ->  Function of [:I[01],I[01]:],T means :Def2: :: TOPALG_2:def 2
 for s, t being Element of I[01]
for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds
it . (s,t) = ((1 - t) * a1) + (t * b1);
existence
 ex b1 being Function of [:I[01],I[01]:],T st
for s, t being Element of I[01]
for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds
b1 . (s,t) = ((1 - t) * a1) + (t * b1)
proof
defpred S1[ Element of the carrier of I[01], Element of the carrier of I[01], set ] means  ex a1, b1 being Point of (TOP-REAL n) st
( a1 = P . $1 & b1 = Q . $1 & $3 = ((1 - $2) * a1) + ($2 * b1) );
A1: for x, y being Element of the carrier of I[01] ex z being Element of T st S1[x,y,z]
proof
let x, y be Element of the carrier of I[01]; ::_thesis: ex z being Element of T st S1[x,y,z]
A2: the carrier of T is Subset of (TOP-REAL n) by TSEP_1:1;
 ( P . x in the carrier of T & Q . x in the carrier of T ) ;
then reconsider a1 = P . x, b1 = Q . x as Point of (TOP-REAL n) by A2;
set z = ((1 - y) * a1) + (y * b1);
A3: y <= 1 by BORSUK_1:43;
 [#] T is convex Subset of (TOP-REAL n) by Def1;
then A4: LSeg (a1,b1) c= [#] T by JORDAN1:def_1;
 ( y is Real & 0 <= y ) by BORSUK_1:43, XREAL_0:def_1;
then  ((1 - y) * a1) + (y * b1) in LSeg (a1,b1) by A3;
hence  ex z being Element of T st S1[x,y,z] by A4; ::_thesis: verum
end;
consider F being Function of [: the carrier of I[01], the carrier of I[01]:], the carrier of T such that
A5: for x, y being Element of the carrier of I[01] holds S1[x,y,F . (x,y)] from BINOP_1:sch_3(A1);
reconsider F = F as Function of [:I[01],I[01]:],T by Lm1;
take  F ; ::_thesis: for s, t being Element of I[01]
for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds
F . (s,t) = ((1 - t) * a1) + (t * b1)
let x, y be Element of the carrier of I[01]; ::_thesis: for a1, b1 being Point of (TOP-REAL n) st a1 = P . x & b1 = Q . x holds
F . (x,y) = ((1 - y) * a1) + (y * b1)
 ex a1, b1 being Point of (TOP-REAL n) st
( a1 = P . x & b1 = Q . x & F . (x,y) = ((1 - y) * a1) + (y * b1) ) by A5;
hence  for a1, b1 being Point of (TOP-REAL n) st a1 = P . x & b1 = Q . x holds
F . (x,y) = ((1 - y) * a1) + (y * b1) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of [:I[01],I[01]:],T st ( for s, t being Element of I[01]
for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds
b1 . (s,t) = ((1 - t) * a1) + (t * b1) ) & ( for s, t being Element of I[01]
for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds
b2 . (s,t) = ((1 - t) * a1) + (t * b1) ) holds
b1 = b2
proof
let f, g be Function of [:I[01],I[01]:],T; ::_thesis: ( ( for s, t being Element of I[01]
for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds
f . (s,t) = ((1 - t) * a1) + (t * b1) ) & ( for s, t being Element of I[01]
for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds
g . (s,t) = ((1 - t) * a1) + (t * b1) ) implies f = g )
assume that
A6: for s, t being Element of I[01]
for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds
f . (s,t) = ((1 - t) * a1) + (t * b1) and
A7: for s, t being Element of I[01]
for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds
g . (s,t) = ((1 - t) * a1) + (t * b1) ; ::_thesis: f = g
 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)
reconsider a1 = P . s, b1 = Q . s as Point of (TOP-REAL n) by PRE_TOPC:25;
 f . (s,t) = ((1 - t) * a1) + (t * b1) by A6;
hence  f . (s,t) = g . (s,t) by A7; ::_thesis: verum
end;
hence  f = g by Lm1, BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines ConvexHomotopy TOPALG_2:def_2_:_
 for n being Element of NAT
for T being non empty convex SubSpace of TOP-REAL n
for P, Q being Function of I[01],T
for b5 being Function of [:I[01],I[01]:],T holds
( b5 = ConvexHomotopy (P,Q) iff for s, t being Element of I[01]
for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds
b5 . (s,t) = ((1 - t) * a1) + (t * b1) );

Lm5:  for n being Element of NAT
for T being non empty convex SubSpace of TOP-REAL n
for P, Q being continuous Function of I[01],T holds ConvexHomotopy (P,Q) is continuous
proof
let n be Element of NAT ; ::_thesis: for T being non empty convex SubSpace of TOP-REAL n
for P, Q being continuous Function of I[01],T holds ConvexHomotopy (P,Q) is continuous
let T be non empty convex SubSpace of TOP-REAL n; ::_thesis: for P, Q being continuous Function of I[01],T holds ConvexHomotopy (P,Q) is continuous
let P, Q be continuous Function of I[01],T; ::_thesis: ConvexHomotopy (P,Q) is continuous
set F = ConvexHomotopy (P,Q);
A1: the carrier of T is Subset of (TOP-REAL n) by TSEP_1:1;
then reconsider G = ConvexHomotopy (P,Q) as Function of [:I[01],I[01]:],(TOP-REAL n) by FUNCT_2:7;
reconsider P1 = P, Q1 = Q as Function of I[01],(TOP-REAL n) by A1, FUNCT_2:7;
set E = the carrier of (TOP-REAL n);
set PI = [:P,(id I[01]):];
set QI = [:Q,(id I[01]):];
reconsider P1 = P1, Q1 = Q1 as continuous Function of I[01],(TOP-REAL n) by PRE_TOPC:26;
set P1I = [:P1,(id I[01]):];
set Q1I = [:Q1,(id I[01]):];
deffunc H1( Element of the carrier 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 the carrier 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
A2: 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
A3: 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) ;
A4: Pb is continuous by A3, TOPALG_1:18;
 Pa is continuous by A2, TOPALG_1:17;
then consider g being Function of [:I[01],I[01]:],(TOP-REAL n) such that
A5: for r being Point of [:I[01],I[01]:] holds g . r = ((Pa * [:P1,(id I[01]):]) . r) + ((Pb * [:Q1,(id I[01]):]) . r) and
A6: g is continuous by A4, JGRAPH_6:12;
A7: for p being Point of [:I[01],I[01]:] holds G . p = ((Pa * [:P1,(id I[01]):]) . p) + ((Pb * [:Q1,(id I[01]):]) . p)
proof
A8: dom Q = the carrier of I[01] by FUNCT_2:def_1;
A9: dom P = the carrier of I[01] by FUNCT_2:def_1;
let p be Point of [:I[01],I[01]:]; ::_thesis: G . p = ((Pa * [:P1,(id I[01]):]) . p) + ((Pb * [:Q1,(id I[01]):]) . p)
consider s, t being Point of I[01] such that
A10: p = [s,t] by BORSUK_1:10;
reconsider a1 = P . s, b1 = Q . s as Point of (TOP-REAL n) by PRE_TOPC:25;
A11: (ConvexHomotopy (P,Q)) . (s,t) = ((1 - t) * a1) + (t * b1) by Def2;
A12: (id I[01]) . t = t by FUNCT_1:18;
A13: (Pb * [:Q,(id I[01]):]) . p = Pb . ([:Q,(id I[01]):] . (s,t)) by A10, FUNCT_2:15
.= Pb . ((Q . s),t) by A8, A12, Lm4, FUNCT_3:def_8
.= t * (Q1 . s) by A3 ;
(Pa * [:P,(id I[01]):]) . p = Pa . ([:P,(id I[01]):] . (s,t)) by A10, FUNCT_2:15
.= Pa . ((P . s),t) by A9, A12, Lm4, FUNCT_3:def_8
.= (1 - t) * (P1 . s) by A2 ;
hence  G . p = ((Pa * [:P1,(id I[01]):]) . p) + ((Pb * [:Q1,(id I[01]):]) . p) by A10, A13, A11; ::_thesis: verum
end;
 for p being Point of [:I[01],I[01]:] holds G . p = g . p
proof
let p be Point of [:I[01],I[01]:]; ::_thesis: G . p = g . p
thus G . p = ((Pa * [:P1,(id I[01]):]) . p) + ((Pb * [:Q1,(id I[01]):]) . p) by A7
.= g . p by A5 ; ::_thesis: verum
end;
hence  ConvexHomotopy (P,Q) is continuous by A6, FUNCT_2:63, PRE_TOPC:27; ::_thesis: verum
end;

Lm6:  for n being Element of NAT
for T being non empty convex SubSpace of TOP-REAL n
for a, b being Point of T
for P, Q being Path of a,b
for s being Point of I[01] holds
( (ConvexHomotopy (P,Q)) . (s,0) = P . s & (ConvexHomotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds
( (ConvexHomotopy (P,Q)) . (0,t) = a & (ConvexHomotopy (P,Q)) . (1,t) = b ) ) )
proof
let n be Element of NAT ; ::_thesis: for T being non empty convex SubSpace of TOP-REAL n
for a, b being Point of T
for P, Q being Path of a,b
for s being Point of I[01] holds
( (ConvexHomotopy (P,Q)) . (s,0) = P . s & (ConvexHomotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds
( (ConvexHomotopy (P,Q)) . (0,t) = a & (ConvexHomotopy (P,Q)) . (1,t) = b ) ) )
reconsider x0 = 0 , x1 = 1 as Point of I[01] by BORSUK_1:def_14, BORSUK_1:def_15;
let T be non empty convex SubSpace of TOP-REAL n; ::_thesis: for a, b being Point of T
for P, Q being Path of a,b
for s being Point of I[01] holds
( (ConvexHomotopy (P,Q)) . (s,0) = P . s & (ConvexHomotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds
( (ConvexHomotopy (P,Q)) . (0,t) = a & (ConvexHomotopy (P,Q)) . (1,t) = b ) ) )
let a, b be Point of T; ::_thesis: for P, Q being Path of a,b
for s being Point of I[01] holds
( (ConvexHomotopy (P,Q)) . (s,0) = P . s & (ConvexHomotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds
( (ConvexHomotopy (P,Q)) . (0,t) = a & (ConvexHomotopy (P,Q)) . (1,t) = b ) ) )
let P, Q be Path of a,b; ::_thesis: for s being Point of I[01] holds
( (ConvexHomotopy (P,Q)) . (s,0) = P . s & (ConvexHomotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds
( (ConvexHomotopy (P,Q)) . (0,t) = a & (ConvexHomotopy (P,Q)) . (1,t) = b ) ) )
set F = ConvexHomotopy (P,Q);
let s be Point of I[01]; ::_thesis: ( (ConvexHomotopy (P,Q)) . (s,0) = P . s & (ConvexHomotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds
( (ConvexHomotopy (P,Q)) . (0,t) = a & (ConvexHomotopy (P,Q)) . (1,t) = b ) ) )
reconsider a1 = P . s, b1 = Q . s as Point of (TOP-REAL n) by PRE_TOPC:25;
A1: P . x0 = a by BORSUK_2:def_4;
 (ConvexHomotopy (P,Q)) . (s,x0) = ((1 - x0) * a1) + (x0 * b1) by Def2;
hence (ConvexHomotopy (P,Q)) . (s,0) = a1 + (0 * b1) by EUCLID:29
.= a1 + (0. (TOP-REAL n)) by EUCLID:29
.= P . s by EUCLID:27 ;
::_thesis: ( (ConvexHomotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds
( (ConvexHomotopy (P,Q)) . (0,t) = a & (ConvexHomotopy (P,Q)) . (1,t) = b ) ) )
 (ConvexHomotopy (P,Q)) . (s,x1) = ((1 - x1) * a1) + (x1 * b1) by Def2;
hence (ConvexHomotopy (P,Q)) . (s,1) = (0. (TOP-REAL n)) + (1 * b1) by EUCLID:29
.= (0. (TOP-REAL n)) + b1 by EUCLID:29
.= Q . s by EUCLID:27 ;
::_thesis: for t being Point of I[01] holds
( (ConvexHomotopy (P,Q)) . (0,t) = a & (ConvexHomotopy (P,Q)) . (1,t) = b )
reconsider a1 = P . x0, b1 = Q . x0 as Point of (TOP-REAL n) by PRE_TOPC:25;
let t be Point of I[01]; ::_thesis: ( (ConvexHomotopy (P,Q)) . (0,t) = a & (ConvexHomotopy (P,Q)) . (1,t) = b )
 ( (ConvexHomotopy (P,Q)) . (0,t) = ((1 - t) * a1) + (t * b1) & Q . x0 = a ) by Def2, BORSUK_2:def_4;
hence (ConvexHomotopy (P,Q)) . (0,t) = ((1 * a1) - (t * a1)) + (t * a1) by A1, EUCLID:50
.= 1 * a1 by EUCLID:48
.= a by A1, EUCLID:29 ;
::_thesis: (ConvexHomotopy (P,Q)) . (1,t) = b
A2: Q . x1 = b by BORSUK_2:def_4;
reconsider a1 = P . x1, b1 = Q . x1 as Point of (TOP-REAL n) by PRE_TOPC:25;
A3: P . x1 = b by BORSUK_2:def_4;
 (ConvexHomotopy (P,Q)) . (1,t) = ((1 - t) * a1) + (t * b1) by Def2;
hence (ConvexHomotopy (P,Q)) . (1,t) = ((1 * a1) - (t * b1)) + (t * a1) by A3, A2, EUCLID:50
.= 1 * b1 by A3, A2, EUCLID:48
.= b by A2, EUCLID:29 ;
::_thesis: verum
end;

theorem Th2: :: TOPALG_2:2
for n being Element of NAT
for T being non empty convex SubSpace of TOP-REAL n
for a, b being Point of T
for P, Q being Path of a,b holds P,Q are_homotopic
proof
let n be Element of NAT ; ::_thesis: for T being non empty convex SubSpace of TOP-REAL n
for a, b being Point of T
for P, Q being Path of a,b holds P,Q are_homotopic
let T be non empty convex SubSpace of TOP-REAL n; ::_thesis: for a, b being Point of T
for P, Q being Path of a,b holds P,Q are_homotopic
let a, b be Point of T; ::_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 = ConvexHomotopy (P,Q); :: according to BORSUK_2:def_7 ::_thesis: ( F is continuous & ( for b1 being Element of the carrier of I[01] holds
( F . (b1,0) = P . b1 & F . (b1,1) = Q . b1 & F . (0,b1) = a & F . (1,b1) = b ) ) )
thus  F is continuous by Lm5; ::_thesis: for b1 being Element of the carrier of I[01] 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 I[01] 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 Element of NAT ;
let T be non empty convex SubSpace of TOP-REAL n;
let a, b be Point of T;
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 Th2;
hence  F is continuous by BORSUK_6:def_11; ::_thesis: verum
end;
end;

theorem Th3: :: TOPALG_2:3
for n being Element of NAT
for T being non empty convex SubSpace of TOP-REAL n
for a being Point of T
for C being Loop of a holds the carrier of (pi_1 (T,a)) = {(Class ((EqRel (T,a)),C))}
proof
let n be Element of NAT ; ::_thesis: for T being non empty convex SubSpace of TOP-REAL n
for a being Point of T
for C being Loop of a holds the carrier of (pi_1 (T,a)) = {(Class ((EqRel (T,a)),C))}
let T be non empty convex SubSpace of TOP-REAL n; ::_thesis: for a being Point of T
for C being Loop of a holds the carrier of (pi_1 (T,a)) = {(Class ((EqRel (T,a)),C))}
let a be Point of T; ::_thesis: for C being Loop of a holds the carrier of (pi_1 (T,a)) = {(Class ((EqRel (T,a)),C))}
let C be Loop of a; ::_thesis: the carrier of (pi_1 (T,a)) = {(Class ((EqRel (T,a)),C))}
set E = EqRel (T,a);
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {(Class ((EqRel (T,a)),C))} c= the carrier of (pi_1 (T,a))
let x be set ; ::_thesis: ( x in the carrier of (pi_1 (T,a)) implies x in {(Class ((EqRel (T,a)),C))} )
assume  x in the carrier of (pi_1 (T,a)) ; ::_thesis: x in {(Class ((EqRel (T,a)),C))}
then consider P being Loop of a such that
A1: x = Class ((EqRel (T,a)),P) by TOPALG_1:47;
 P,C are_homotopic by Th2;
then  x = Class ((EqRel (T,a)),C) by A1, TOPALG_1:46;
hence  x in {(Class ((EqRel (T,a)),C))} by TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(Class ((EqRel (T,a)),C))} or x in the carrier of (pi_1 (T,a)) )
assume  x in {(Class ((EqRel (T,a)),C))} ; ::_thesis: x in the carrier of (pi_1 (T,a))
then A2: x = Class ((EqRel (T,a)),C) by TARSKI:def_1;
 C in Loops a by TOPALG_1:def_1;
then  x in Class (EqRel (T,a)) by A2, EQREL_1:def_3;
hence  x in the carrier of (pi_1 (T,a)) by TOPALG_1:def_5; ::_thesis: verum
end;

registration
let n be Element of NAT ;
let T be non empty convex SubSpace of TOP-REAL n;
let a be Point of T;
cluster FundamentalGroup (T,a) ->  trivial ;
coherence
 pi_1 (T,a) is trivial
proof
set C = the constant Loop of a;
set E = EqRel (T,a);
 the carrier of (pi_1 (T,a)) = Class (EqRel (T,a)) by TOPALG_1:def_5;
then  {(Class ((EqRel (T,a)), the constant Loop of a))} = Class (EqRel (T,a)) by Th3;
hence  pi_1 (T,a) is trivial by TOPALG_1:def_5; ::_thesis: verum
end;
end;

begin

theorem Th4: :: TOPALG_2:4
for a being real number holds |[a]| /. 1 = a
proof
let a be real number ; ::_thesis: |[a]| /. 1 = a
reconsider y = a as Real by XREAL_0:def_1;
thus |[a]| /. 1 = <*y*> /. 1
.= a by FINSEQ_4:16 ; ::_thesis: verum
end;

theorem :: TOPALG_2:5
for a, b being real number st a <= b holds
[.a,b.] =  {  (((1 - l) * a) + (l * b)) where l is Real : ( 0 <= l & l <= 1 )  }
proof
let a, b be real number ; ::_thesis: ( a <= b implies [.a,b.] =  {  (((1 - l) * a) + (l * b)) where l is Real : ( 0 <= l & l <= 1 )  }  )
set X =  {  (((1 - l) * a) + (l * b)) where l is Real : ( 0 <= l & l <= 1 )  }  ;
assume A1: a <= b ; ::_thesis: [.a,b.] =  {  (((1 - l) * a) + (l * b)) where l is Real : ( 0 <= l & l <= 1 )  }
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis:  {  (((1 - l) * a) + (l * b)) where l is Real : ( 0 <= l & l <= 1 )  }  c= [.a,b.]
let x be set ; ::_thesis: ( x in [.a,b.] implies b1 in  {  (((1 - b2) * a) + (b2 * b)) where l is Real : ( 0 <= b2 & b2 <= 1 )  }  )
assume A2: x in [.a,b.] ; ::_thesis: b1 in  {  (((1 - b2) * a) + (b2 * b)) where l is Real : ( 0 <= b2 & b2 <= 1 )  }
then reconsider y = x as Real ;
A3: ( a <= y & y <= b ) by A2, XXREAL_1:1;
percases ( a < b or a = b ) by A1, XXREAL_0:1;
suppose a < b ; ::_thesis: b1 in  {  (((1 - b2) * a) + (b2 * b)) where l is Real : ( 0 <= b2 & b2 <= 1 )  }
then A4: b - a > b - b by XREAL_1:15;
reconsider l = (y - a) / (b - a) as Real ;
 l in the carrier of (Closed-Interval-TSpace (0,1)) by A3, BORSUK_6:2;
then  l in [.0,1.] by TOPMETR:18;
then A5: ( 0 <= l & l <= 1 ) by XXREAL_1:1;
((1 - l) * a) + (l * b) = a + (l * (b - a))
.= a + (y - a) by A4, XCMPLX_1:87
.= y ;
hence  x in  {  (((1 - l) * a) + (l * b)) where l is Real : ( 0 <= l & l <= 1 )  }  by A5; ::_thesis: verum
end;
suppose a = b ; ::_thesis: b1 in  {  (((1 - b2) * a) + (b2 * b)) where l is Real : ( 0 <= b2 & b2 <= 1 )  }
then  ((1 - 1) * a) + (1 * b) = y by A3, XXREAL_0:1;
hence  x in  {  (((1 - l) * a) + (l * b)) where l is Real : ( 0 <= l & l <= 1 )  }  ; ::_thesis: verum
end;
end;
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (((1 - l) * a) + (l * b)) where l is Real : ( 0 <= l & l <= 1 )  }  or x in [.a,b.] )
assume  x in  {  (((1 - l) * a) + (l * b)) where l is Real : ( 0 <= l & l <= 1 )  }  ; ::_thesis: x in [.a,b.]
then consider l being Real such that
A6: x = ((1 - l) * a) + (l * b) and
A7: ( 0 <= l & l <= 1 ) ;
 ( a <= ((1 - l) * a) + (l * b) & ((1 - l) * a) + (l * b) <= b ) by A1, A7, XREAL_1:172, XREAL_1:173;
hence  x in [.a,b.] by A6, XXREAL_1:1; ::_thesis: verum
end;

theorem Th6: :: TOPALG_2:6
for F being Function of [:R^1,I[01]:],R^1 st ( for x being Point of R^1
for i being Point of I[01] holds F . (x,i) = (1 - i) * x ) holds
F is continuous
proof
deffunc H1( Element of (TOP-REAL 1), Element of the carrier of I[01]) ->  Element of the carrier of (TOP-REAL 1) = (1 - $2) * $1;
consider G being Function of [: the carrier of (TOP-REAL 1), the carrier of I[01]:], the carrier of (TOP-REAL 1) such that
A1: for x being Point of (TOP-REAL 1)
for i being Point of I[01] holds G . (x,i) = H1(x,i) from BINOP_1:sch_4();
reconsider G = G as Function of [:(TOP-REAL 1),I[01]:],(TOP-REAL 1) by Lm2;
consider f being Function of (TOP-REAL 1),R^1 such that
A2: for p being Element of (TOP-REAL 1) holds f . p = p /. 1 by JORDAN2B:1;
A3: f is being_homeomorphism by A2, JORDAN2B:28;
then A4: f is continuous by TOPS_2:def_5;
let F be Function of [:R^1,I[01]:],R^1; ::_thesis: ( ( for x being Point of R^1
for i being Point of I[01] holds F . (x,i) = (1 - i) * x ) implies F is continuous )
assume A5: for x being Point of R^1
for i being Point of I[01] holds F . (x,i) = (1 - i) * x ; ::_thesis: F is continuous
A6: for x being Point of [:R^1,I[01]:] holds F . x = (f * (G * [:(f "),(id I[01]):])) . x
proof
reconsider ff = f as Function ;
let x be Point of [:R^1,I[01]:]; ::_thesis: F . x = (f * (G * [:(f "),(id I[01]):])) . x
consider a being Point of R^1, b being Point of I[01] such that
A7: x = [a,b] by BORSUK_1:10;
A8: dom (f ") = the carrier of R^1 by FUNCT_2:def_1;
 rng f = [#] R^1 by A3, TOPS_2:def_5;
then A9: f is onto by FUNCT_2:def_3;
A10: dom f = the carrier of (TOP-REAL 1) by FUNCT_2:def_1;
set g = ff " ;
consider z being Real such that
A11: (1 - b) * ((f ") . a) = <*z*> by JORDAN2B:20;
A12: <*a*> = |[a]| ;
then reconsider w = <*a*> as Element of REAL 1 by EUCLID:22;
A13: ff is one-to-one by A3, TOPS_2:def_5;
f . <*a*> = |[a]| /. 1 by A2
.= a by Th4 ;
then  <*a*> = (ff ") . a by A10, A13, A12, FUNCT_1:32;
then A14: w = (f /") . a by A9, A13, TOPS_2:def_4;
A15: <*z*> = (1 - b) * ((f /") . a) by A11
.= (1 - b) * w by A14
.= <*((1 - b) * a)*> by RVSUM_1:47 ;
thus (f * (G * [:(f "),(id I[01]):])) . x = f . ((G * [:(f "),(id I[01]):]) . x) by FUNCT_2:15
.= f . (G . ([:(f "),(id I[01]):] . (a,b))) by A7, FUNCT_2:15
.= f . (G . (((f ") . a),((id I[01]) . b))) by A8, Lm4, FUNCT_3:def_8
.= f . (G . (((f ") . a),b)) by FUNCT_1:18
.= f . ((1 - b) * ((f ") . a)) by A1
.= ((1 - b) * ((f ") . a)) /. 1 by A2
.= <*z*> /. 1 by A11
.= (1 - b) * a by A15, FINSEQ_4:16
.= F . (a,b) by A5
.= F . x by A7 ; ::_thesis: verum
end;
 f " is continuous by A3, TOPS_2:def_5;
then A16: [:(f "),(id I[01]):] is continuous ;
 G is continuous by A1, TOPALG_1:17;
hence  F is continuous by A4, A16, A6, FUNCT_2:63; ::_thesis: verum
end;

theorem Th7: :: TOPALG_2:7
for F being Function of [:R^1,I[01]:],R^1 st ( for x being Point of R^1
for i being Point of I[01] holds F . (x,i) = i * x ) holds
F is continuous
proof
deffunc H1( Element of (TOP-REAL 1), Element of the carrier of I[01]) ->  Element of the carrier of (TOP-REAL 1) = $2 * $1;
consider G being Function of [: the carrier of (TOP-REAL 1), the carrier of I[01]:], the carrier of (TOP-REAL 1) such that
A1: for x being Point of (TOP-REAL 1)
for i being Point of I[01] holds G . (x,i) = H1(x,i) from BINOP_1:sch_4();
reconsider G = G as Function of [:(TOP-REAL 1),I[01]:],(TOP-REAL 1) by Lm2;
consider f being Function of (TOP-REAL 1),R^1 such that
A2: for p being Element of (TOP-REAL 1) holds f . p = p /. 1 by JORDAN2B:1;
A3: f is being_homeomorphism by A2, JORDAN2B:28;
then A4: f is continuous by TOPS_2:def_5;
let F be Function of [:R^1,I[01]:],R^1; ::_thesis: ( ( for x being Point of R^1
for i being Point of I[01] holds F . (x,i) = i * x ) implies F is continuous )
assume A5: for x being Point of R^1
for i being Point of I[01] holds F . (x,i) = i * x ; ::_thesis: F is continuous
A6: for x being Point of [:R^1,I[01]:] holds F . x = (f * (G * [:(f "),(id I[01]):])) . x
proof
reconsider ff = f as Function ;
let x be Point of [:R^1,I[01]:]; ::_thesis: F . x = (f * (G * [:(f "),(id I[01]):])) . x
consider a being Point of R^1, b being Point of I[01] such that
A7: x = [a,b] by BORSUK_1:10;
A8: dom (f ") = the carrier of R^1 by FUNCT_2:def_1;
 rng f = [#] R^1 by A3, TOPS_2:def_5;
then A9: f is onto by FUNCT_2:def_3;
A10: dom f = the carrier of (TOP-REAL 1) by FUNCT_2:def_1;
set g = ff " ;
consider z being Real such that
A11: b * ((f ") . a) = <*z*> by JORDAN2B:20;
A12: <*a*> = |[a]| ;
then reconsider w = <*a*> as Element of REAL 1 by EUCLID:22;
A13: ff is one-to-one by A3, TOPS_2:def_5;
f . <*a*> = |[a]| /. 1 by A2
.= a by Th4 ;
then  <*a*> = (ff ") . a by A10, A13, A12, FUNCT_1:32;
then A14: w = (f /") . a by A9, A13, TOPS_2:def_4;
A15: <*z*> = b * ((f /") . a) by A11
.= b * w by A14
.= <*(b * a)*> by RVSUM_1:47 ;
thus (f * (G * [:(f "),(id I[01]):])) . x = f . ((G * [:(f "),(id I[01]):]) . x) by FUNCT_2:15
.= f . (G . ([:(f "),(id I[01]):] . (a,b))) by A7, FUNCT_2:15
.= f . (G . (((f ") . a),((id I[01]) . b))) by A8, Lm4, FUNCT_3:def_8
.= f . (G . (((f ") . a),b)) by FUNCT_1:18
.= f . (b * ((f ") . a)) by A1
.= (b * ((f ") . a)) /. 1 by A2
.= <*z*> /. 1 by A11
.= z by FINSEQ_4:16
.= b * a by A15, FINSEQ_1:76
.= F . (a,b) by A5
.= F . x by A7 ; ::_thesis: verum
end;
 f " is continuous by A3, TOPS_2:def_5;
then A16: [:(f "),(id I[01]):] is continuous ;
 G is continuous by A1, TOPALG_1:18;
hence  F is continuous by A4, A16, A6, FUNCT_2:63; ::_thesis: verum
end;

registration
cluster non empty V166() V167() V168() interval for Element of bool the carrier of R^1;
existence
 ex b1 being Subset of R^1 st
( not b1 is empty & b1 is interval )
proof
 REAL c= the carrier of R^1 by TOPMETR:17;
then reconsider P = REAL as non empty Subset of R^1 ;
take  P ; ::_thesis: ( not P is empty & P is interval )
thus  not P is empty ; ::_thesis: P is interval
let a, b be ext-real number ; :: according to XXREAL_2:def_12 ::_thesis: ( not a in P or not b in P or K58(a,b) c= P )
assume  ( a in P & b in P ) ; ::_thesis: K58(a,b) c= P
then reconsider a = a, b = b as Real ;
 [.a,b.] c= P ;
hence  K58(a,b) c= P ; ::_thesis: verum
end;
end;

registration
let T be real-membered TopStruct ;
clusterV166() V167() V168() interval for Element of bool the carrier of T;
existence
 ex b1 being Subset of T st b1 is interval
proof
take  {} T ; ::_thesis: {} T is interval
thus  {} T is interval ; ::_thesis: verum
end;
end;

definition
let T be real-membered TopStruct ;
attrT is interval  means :Def3: :: TOPALG_2:def 3
 [#] T is interval ;
end;

:: deftheorem Def3 defines interval TOPALG_2:def_3_:_
 for T being real-membered TopStruct holds
( T is interval iff [#] T is interval );

Lm7:  for T being SubSpace of R^1 st T = R^1 holds
T is interval
proof
let T be SubSpace of R^1 ; ::_thesis: ( T = R^1 implies T is interval )
assume A1: T = R^1 ; ::_thesis: T is interval
A2: [#] T = REAL by A1, TOPMETR:17;
then reconsider P = [#] T as Subset of REAL ;
 P is interval by A2;
hence  [#] T is interval ; :: according to TOPALG_2:def_3 ::_thesis: verum
end;

registration
cluster non empty strict TopSpace-like real-membered interval for SubSpace of R^1 ;
existence
 ex b1 being SubSpace of R^1 st
( b1 is strict & not b1 is empty & b1 is interval )
proof
reconsider T = R^1 as non empty strict SubSpace of R^1 by TSEP_1:2;
take  T ; ::_thesis: ( T is strict & not T is empty & T is interval )
thus  ( T is strict & not T is empty & T is interval ) by Lm7; ::_thesis: verum
end;
end;

definition
:: original: R^1
redefine func R^1  ->  interval SubSpace of R^1 ;
coherence
 R^1 is interval SubSpace of R^1 by Lm7, TSEP_1:2;
end;

theorem Th8: :: TOPALG_2:8
for T being non empty interval SubSpace of R^1
for a, b being Point of T holds [.a,b.] c= the carrier of T
proof
let T be non empty interval SubSpace of R^1 ; ::_thesis: for a, b being Point of T holds [.a,b.] c= the carrier of T
let a, b be Point of T; ::_thesis: [.a,b.] c= the carrier of T
reconsider a1 = a, b1 = b as Point of R^1 by PRE_TOPC:25;
 [#] T is interval Subset of T by Def3;
then  [.a1,b1.] c= the carrier of T by XXREAL_2:def_12;
hence  [.a,b.] c= the carrier of T ; ::_thesis: verum
end;

registration
cluster non empty interval  ->  non empty pathwise_connected for SubSpace of R^1 ;
coherence
 for b1 being non empty SubSpace of R^1 st b1 is interval holds
b1 is pathwise_connected
proof
let T be non empty SubSpace of R^1 ; ::_thesis: ( T is interval implies T is pathwise_connected )
assume A1: T is interval ; ::_thesis: T is pathwise_connected
let a, b be Point of T; :: according to BORSUK_2:def_3 ::_thesis: a,b are_connected
percases ( a <= b or b <= a ) ;
supposeA2: a <= b ; ::_thesis: a,b are_connected
set f = L[01] (((#) (a,b)),((a,b) (#)));
set X = Closed-Interval-TSpace (a,b);
A3: the carrier of (Closed-Interval-TSpace (a,b)) = [.a,b.] by A2, TOPMETR:18;
 [.a,b.] c= the carrier of T by A1, Th8;
then reconsider f = L[01] (((#) (a,b)),((a,b) (#))) as Function of I[01],T by A3, FUNCT_2:7, TOPMETR:20;
take  f ; :: according to BORSUK_2:def_1 ::_thesis: ( f is continuous & f . 0 = a & f . 1 = b )
 the carrier of (Closed-Interval-TSpace (a,b)) is Subset of R^1 by TSEP_1:1;
then reconsider g = f as Function of I[01],R^1 by FUNCT_2:7, TOPMETR:20;
 L[01] (((#) (a,b)),((a,b) (#))) is continuous by A2, TREAL_1:8;
then  g is continuous by PRE_TOPC:26, TOPMETR:20;
hence  f is continuous by PRE_TOPC:27; ::_thesis: ( f . 0 = a & f . 1 = b )
thus f . 0 = f . ((#) (0,1)) by TREAL_1:def_1
.= (#) (a,b) by A2, TREAL_1:9
.= a by A2, TREAL_1:def_1 ; ::_thesis: f . 1 = b
thus f . 1 = f . ((0,1) (#)) by TREAL_1:def_2
.= (a,b) (#) by A2, TREAL_1:9
.= b by A2, TREAL_1:def_2 ; ::_thesis: verum
end;
supposeA4: b <= a ; ::_thesis: a,b are_connected
set f = L[01] (((b,a) (#)),((#) (b,a)));
set X = Closed-Interval-TSpace (b,a);
A5: the carrier of (Closed-Interval-TSpace (b,a)) = [.b,a.] by A4, TOPMETR:18;
 [.b,a.] c= the carrier of T by A1, Th8;
then reconsider f = L[01] (((b,a) (#)),((#) (b,a))) as Function of I[01],T by A5, FUNCT_2:7, TOPMETR:20;
take  f ; :: according to BORSUK_2:def_1 ::_thesis: ( f is continuous & f . 0 = a & f . 1 = b )
 the carrier of (Closed-Interval-TSpace (b,a)) is Subset of R^1 by TSEP_1:1;
then reconsider g = f as Function of I[01],R^1 by FUNCT_2:7, TOPMETR:20;
 L[01] (((b,a) (#)),((#) (b,a))) is continuous by A4, TREAL_1:8;
then  g is continuous by PRE_TOPC:26, TOPMETR:20;
hence  f is continuous by PRE_TOPC:27; ::_thesis: ( f . 0 = a & f . 1 = b )
thus f . 0 = f . ((#) (0,1)) by TREAL_1:def_1
.= (b,a) (#) by A4, TREAL_1:9
.= a by A4, TREAL_1:def_2 ; ::_thesis: f . 1 = b
thus f . 1 = f . ((0,1) (#)) by TREAL_1:def_2
.= (#) (b,a) by A4, TREAL_1:9
.= b by A4, TREAL_1:def_1 ; ::_thesis: verum
end;
end;
end;
end;

theorem Th9: :: TOPALG_2:9
for a, b being real number st a <= b holds
Closed-Interval-TSpace (a,b) is interval
proof
let a, b be real number ; ::_thesis: ( a <= b implies Closed-Interval-TSpace (a,b) is interval )
set X = Closed-Interval-TSpace (a,b);
assume  a <= b ; ::_thesis: Closed-Interval-TSpace (a,b) is interval
then  [.a,b.] = [#] (Closed-Interval-TSpace (a,b)) by TOPMETR:18;
hence  [#] (Closed-Interval-TSpace (a,b)) is interval ; :: according to TOPALG_2:def_3 ::_thesis: verum
end;

theorem Th10: :: TOPALG_2:10
I[01] is interval by Th9, TOPMETR:20;

theorem :: TOPALG_2:11
for a, b being real number st a <= b holds
Closed-Interval-TSpace (a,b) is pathwise_connected
proof
let a, b be real number ; ::_thesis: ( a <= b implies Closed-Interval-TSpace (a,b) is pathwise_connected )
assume  a <= b ; ::_thesis: Closed-Interval-TSpace (a,b) is pathwise_connected
then reconsider X = Closed-Interval-TSpace (a,b) as non empty interval SubSpace of R^1 by Th9;
 X is pathwise_connected ;
hence  Closed-Interval-TSpace (a,b) is pathwise_connected ; ::_thesis: verum
end;

definition
let T be non empty interval SubSpace of R^1 ;
let P, Q be Function of I[01],T;
func R1Homotopy (P,Q) ->  Function of [:I[01],I[01]:],T means :Def4: :: TOPALG_2:def 4
 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]:],T st
for s, t being Element of I[01] holds b1 . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s))
proof
defpred S1[ Element of the carrier of I[01], Element of the carrier of I[01], set ] means $3 = ((1 - $2) * (P . $1)) + ($2 * (Q . $1));
A1: for m, n being Element of the carrier of I[01] ex z being Element of T st S1[m,n,z]
proof
let m, n be Element of the carrier of I[01]; ::_thesis: ex z being Element of T st S1[m,n,z]
A2: 0 <= n by BORSUK_1:43;
set z = ((1 - n) * (P . m)) + (n * (Q . m));
A3: n <= 1 by BORSUK_1:43;
percases ( P . m <= Q . m or P . m > Q . m ) ;
suppose P . m <= Q . m ; ::_thesis: ex z being Element of T st S1[m,n,z]
then  ( P . m <= ((1 - n) * (P . m)) + (n * (Q . m)) & ((1 - n) * (P . m)) + (n * (Q . m)) <= Q . m ) by A2, A3, XREAL_1:172, XREAL_1:173;
then A4: ((1 - n) * (P . m)) + (n * (Q . m)) in [.(P . m),(Q . m).] by XXREAL_1:1;
 [.(P . m),(Q . m).] c= the carrier of T by Th8;
hence  ex z being Element of T st S1[m,n,z] by A4; ::_thesis: verum
end;
supposeA5: P . m > Q . m ; ::_thesis: ex z being Element of T st S1[m,n,z]
 1 - 1 <= 1 - n by A3, XREAL_1:13;
then  (1 - n) * (Q . m) <= (1 - n) * (P . m) by A5, XREAL_1:64;
then A6: ((1 - n) * (Q . m)) + (n * (Q . m)) <= ((1 - n) * (P . m)) + (n * (Q . m)) by XREAL_1:6;
A7: [.(Q . m),(P . m).] c= the carrier of T by Th8;
 (Q . m) - (P . m) < (Q . m) - (Q . m) by A5, XREAL_1:15;
then  n * ((Q . m) - (P . m)) <= n * 0 by A2, XREAL_1:131;
then  (P . m) + (n * ((Q . m) - (P . m))) <= (P . m) + 0 by XREAL_1:6;
then  ((1 - n) * (P . m)) + (n * (Q . m)) in [.(Q . m),(P . m).] by A6, XXREAL_1:1;
hence  ex z being Element of T st S1[m,n,z] by A7; ::_thesis: verum
end;
end;
end;
consider F being Function of [: the carrier of I[01], the carrier of I[01]:], the carrier of T such that
A8: for m, n being Element of the carrier of I[01] holds S1[m,n,F . (m,n)] from BINOP_1:sch_3(A1);
reconsider F = F as Function of [:I[01],I[01]:],T by Lm1;
take  F ; ::_thesis: for s, t being Element of I[01] holds F . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s))
let s, t be Element of the carrier of I[01]; ::_thesis: F . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s))
thus  F . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) by A8; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of [:I[01],I[01]:],T 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
let f, g be Function of [:I[01],I[01]:],T; ::_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
A9: for s, t being Element of I[01] holds f . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) and
A10: for s, t being Element of I[01] holds g . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) ; ::_thesis: f = g
 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 A9
.= g . (s,t) by A10 ; ::_thesis: verum
end;
hence  f = g by Lm1, BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines R1Homotopy TOPALG_2:def_4_:_
 for T being non empty interval SubSpace of R^1
for P, Q being Function of I[01],T
for b4 being Function of [:I[01],I[01]:],T holds
( b4 = R1Homotopy (P,Q) iff for s, t being Element of I[01] holds b4 . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) );

Lm8:  for T being non empty interval SubSpace of R^1
for P, Q being continuous Function of I[01],T holds R1Homotopy (P,Q) is continuous
proof
set E = the carrier of R^1;
let T be non empty interval SubSpace of R^1 ; ::_thesis: for P, Q being continuous Function of I[01],T holds R1Homotopy (P,Q) is continuous
let P, Q be continuous Function of I[01],T; ::_thesis: R1Homotopy (P,Q) is continuous
set F = R1Homotopy (P,Q);
set PI = [:P,(id I[01]):];
set QI = [:Q,(id I[01]):];
defpred S1[ Element of the carrier of R^1, Element of the carrier of I[01], set ] means $3 = (1 - $2) * $1;
defpred S2[ Element of the carrier of R^1, Element of the carrier of I[01], set ] means $3 = $2 * $1;
A1: the carrier of T is Subset of R^1 by TSEP_1:1;
then reconsider G = R1Homotopy (P,Q) as Function of [:I[01],I[01]:],R^1 by FUNCT_2:7;
reconsider P1 = P, Q1 = Q as Function of I[01],R^1 by A1, FUNCT_2:7;
reconsider P1 = P1, Q1 = Q1 as continuous Function of I[01],R^1 by PRE_TOPC:26;
set P1I = [:P1,(id I[01]):];
set Q1I = [:Q1,(id I[01]):];
A2: for x being Element of the carrier of R^1
for y being Element of the carrier of I[01] ex z being Element of the carrier of R^1 st S1[x,y,z] by TOPMETR:17;
consider Pa being Function of [: the carrier of R^1, the carrier of I[01]:], the carrier of R^1 such that
A3: for x being Element of the carrier of R^1
for i being Element of the carrier of I[01] holds S1[x,i,Pa . (x,i)] from BINOP_1:sch_3(A2);
A4: for x being Element of the carrier of R^1
for y being Element of the carrier of I[01] ex z being Element of the carrier of R^1 st S2[x,y,z]
proof
let x be Element of the carrier of R^1; ::_thesis: for y being Element of the carrier of I[01] ex z being Element of the carrier of R^1 st S2[x,y,z]
let y be Element of the carrier of I[01]; ::_thesis: ex z being Element of the carrier of R^1 st S2[x,y,z]
 y * x in REAL by XREAL_0:def_1;
hence  ex z being Element of the carrier of R^1 st S2[x,y,z] by TOPMETR:17; ::_thesis: verum
end;
consider Pb being Function of [: the carrier of R^1, the carrier of I[01]:], the carrier of R^1 such that
A5: for x being Element of the carrier of R^1
for i being Element of the carrier of I[01] holds S2[x,i,Pb . (x,i)] from BINOP_1:sch_3(A4);
reconsider Pa = Pa, Pb = Pb as Function of [:R^1,I[01]:],R^1 by Lm3;
A6: Pb is continuous by A5, Th7;
 Pa is continuous by A3, Th6;
then consider g being Function of [:I[01],I[01]:],R^1 such that
A7: for p being Point of [:I[01],I[01]:]
for r1, r2 being real number st (Pa * [:P1,(id I[01]):]) . p = r1 & (Pb * [:Q1,(id I[01]):]) . p = r2 holds
g . p = r1 + r2 and
A8: g is continuous by A6, JGRAPH_2:19;
A9: for p being Point of [:I[01],I[01]:] holds G . p = ((Pa * [:P1,(id I[01]):]) . p) + ((Pb * [:Q1,(id I[01]):]) . p)
proof
A10: dom Q = the carrier of I[01] by FUNCT_2:def_1;
A11: dom P = the carrier of I[01] by FUNCT_2:def_1;
let p be Point of [:I[01],I[01]:]; ::_thesis: G . p = ((Pa * [:P1,(id I[01]):]) . p) + ((Pb * [:Q1,(id I[01]):]) . p)
consider s, t being Point of I[01] such that
A12: p = [s,t] by BORSUK_1:10;
reconsider a1 = P . s, b1 = Q . s as Point of R^1 by PRE_TOPC:25;
A13: P . s in the carrier of T ;
A14: (R1Homotopy (P,Q)) . (s,t) = ((1 - t) * a1) + (t * b1) by Def4;
A15: Q . s in the carrier of T ;
A16: (id I[01]) . t = t by FUNCT_1:18;
A17: (Pb * [:Q,(id I[01]):]) . p = Pb . ([:Q,(id I[01]):] . (s,t)) by A12, FUNCT_2:15
.= Pb . ((Q . s),t) by A10, A16, Lm4, FUNCT_3:def_8
.= t * (Q . s) by A1, A5, A15 ;
(Pa * [:P,(id I[01]):]) . p = Pa . ([:P,(id I[01]):] . (s,t)) by A12, FUNCT_2:15
.= Pa . ((P . s),t) by A11, A16, Lm4, FUNCT_3:def_8
.= (1 - t) * (P . s) by A1, A3, A13 ;
hence  G . p = ((Pa * [:P1,(id I[01]):]) . p) + ((Pb * [:Q1,(id I[01]):]) . p) by A12, A17, A14; ::_thesis: verum
end;
 for p being Point of [:I[01],I[01]:] holds G . p = g . p
proof
let p be Point of [:I[01],I[01]:]; ::_thesis: G . p = g . p
thus G . p = ((Pa * [:P1,(id I[01]):]) . p) + ((Pb * [:Q1,(id I[01]):]) . p) by A9
.= g . p by A7 ; ::_thesis: verum
end;
hence  R1Homotopy (P,Q) is continuous by A8, FUNCT_2:63, PRE_TOPC:27; ::_thesis: verum
end;

Lm9:  for T being non empty interval SubSpace of R^1
for a, b being Point of T
for P, Q being Path of a,b
for s being Point of I[01] holds
( (R1Homotopy (P,Q)) . (s,0) = P . s & (R1Homotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds
( (R1Homotopy (P,Q)) . (0,t) = a & (R1Homotopy (P,Q)) . (1,t) = b ) ) )
proof
let T be non empty interval SubSpace of R^1 ; ::_thesis: for a, b being Point of T
for P, Q being Path of a,b
for s being Point of I[01] holds
( (R1Homotopy (P,Q)) . (s,0) = P . s & (R1Homotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds
( (R1Homotopy (P,Q)) . (0,t) = a & (R1Homotopy (P,Q)) . (1,t) = b ) ) )
let a, b be Point of T; ::_thesis: for P, Q being Path of a,b
for s being Point of I[01] holds
( (R1Homotopy (P,Q)) . (s,0) = P . s & (R1Homotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds
( (R1Homotopy (P,Q)) . (0,t) = a & (R1Homotopy (P,Q)) . (1,t) = b ) ) )
let P, Q be Path of a,b; ::_thesis: for s being Point of I[01] holds
( (R1Homotopy (P,Q)) . (s,0) = P . s & (R1Homotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds
( (R1Homotopy (P,Q)) . (0,t) = a & (R1Homotopy (P,Q)) . (1,t) = b ) ) )
set F = R1Homotopy (P,Q);
let s be Point of I[01]; ::_thesis: ( (R1Homotopy (P,Q)) . (s,0) = P . s & (R1Homotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds
( (R1Homotopy (P,Q)) . (0,t) = a & (R1Homotopy (P,Q)) . (1,t) = b ) ) )
A1: ( P . 0[01] = a & Q . 0[01] = a ) by BORSUK_2:def_4;
thus (R1Homotopy (P,Q)) . (s,0) = ((1 - 0) * (P . s)) + (0 * (Q . s)) by Def4, BORSUK_1:def_14
.= P . s ; ::_thesis: ( (R1Homotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds
( (R1Homotopy (P,Q)) . (0,t) = a & (R1Homotopy (P,Q)) . (1,t) = b ) ) )
thus (R1Homotopy (P,Q)) . (s,1) = ((1 - 1) * (P . s)) + (1 * (Q . s)) by Def4, BORSUK_1:def_15
.= Q . s ; ::_thesis: for t being Point of I[01] holds
( (R1Homotopy (P,Q)) . (0,t) = a & (R1Homotopy (P,Q)) . (1,t) = b )
let t be Point of I[01]; ::_thesis: ( (R1Homotopy (P,Q)) . (0,t) = a & (R1Homotopy (P,Q)) . (1,t) = b )
thus (R1Homotopy (P,Q)) . (0,t) = ((1 - t) * (P . 0[01])) + (t * (Q . 0[01])) by Def4
.= a by A1 ; ::_thesis: (R1Homotopy (P,Q)) . (1,t) = b
A2: ( P . 1[01] = b & Q . 1[01] = b ) by BORSUK_2:def_4;
thus (R1Homotopy (P,Q)) . (1,t) = ((1 - t) * (P . 1[01])) + (t * (Q . 1[01])) by Def4
.= b by A2 ; ::_thesis: verum
end;

theorem Th12: :: TOPALG_2:12
for T being non empty interval SubSpace of R^1
for a, b being Point of T
for P, Q being Path of a,b holds P,Q are_homotopic
proof
let T be non empty interval SubSpace of R^1 ; ::_thesis: for a, b being Point of T
for P, Q being Path of a,b holds P,Q are_homotopic
let a, b be Point of T; ::_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 = R1Homotopy (P,Q); :: according to BORSUK_2:def_7 ::_thesis: ( F is continuous & ( for b1 being Element of the carrier of I[01] holds
( F . (b1,0) = P . b1 & F . (b1,1) = Q . b1 & F . (0,b1) = a & F . (1,b1) = b ) ) )
thus  F is continuous by Lm8; ::_thesis: for b1 being Element of the carrier of I[01] 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 I[01] holds
( F . (b1,0) = P . b1 & F . (b1,1) = Q . b1 & F . (0,b1) = a & F . (1,b1) = b ) by Lm9; ::_thesis: verum
end;

registration
let T be non empty interval SubSpace of R^1 ;
let a, b be Point of T;
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 Th12;
hence  F is continuous by BORSUK_6:def_11; ::_thesis: verum
end;
end;

theorem Th13: :: TOPALG_2:13
for T being non empty interval SubSpace of R^1
for a being Point of T
for C being Loop of a holds the carrier of (pi_1 (T,a)) = {(Class ((EqRel (T,a)),C))}
proof
let T be non empty interval SubSpace of R^1 ; ::_thesis: for a being Point of T
for C being Loop of a holds the carrier of (pi_1 (T,a)) = {(Class ((EqRel (T,a)),C))}
let a be Point of T; ::_thesis: for C being Loop of a holds the carrier of (pi_1 (T,a)) = {(Class ((EqRel (T,a)),C))}
let C be Loop of a; ::_thesis: the carrier of (pi_1 (T,a)) = {(Class ((EqRel (T,a)),C))}
set E = EqRel (T,a);
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {(Class ((EqRel (T,a)),C))} c= the carrier of (pi_1 (T,a))
let x be set ; ::_thesis: ( x in the carrier of (pi_1 (T,a)) implies x in {(Class ((EqRel (T,a)),C))} )
assume  x in the carrier of (pi_1 (T,a)) ; ::_thesis: x in {(Class ((EqRel (T,a)),C))}
then consider P being Loop of a such that
A1: x = Class ((EqRel (T,a)),P) by TOPALG_1:47;
 P,C are_homotopic by Th12;
then  x = Class ((EqRel (T,a)),C) by A1, TOPALG_1:46;
hence  x in {(Class ((EqRel (T,a)),C))} by TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(Class ((EqRel (T,a)),C))} or x in the carrier of (pi_1 (T,a)) )
assume  x in {(Class ((EqRel (T,a)),C))} ; ::_thesis: x in the carrier of (pi_1 (T,a))
then A2: x = Class ((EqRel (T,a)),C) by TARSKI:def_1;
 C in Loops a by TOPALG_1:def_1;
then  x in Class (EqRel (T,a)) by A2, EQREL_1:def_3;
hence  x in the carrier of (pi_1 (T,a)) by TOPALG_1:def_5; ::_thesis: verum
end;

registration
let T be non empty interval SubSpace of R^1 ;
let a be Point of T;
cluster FundamentalGroup (T,a) ->  trivial ;
coherence
 pi_1 (T,a) is trivial
proof
set C = the constant Loop of a;
set E = EqRel (T,a);
 the carrier of (pi_1 (T,a)) = Class (EqRel (T,a)) by TOPALG_1:def_5;
then  {(Class ((EqRel (T,a)), the constant Loop of a))} = Class (EqRel (T,a)) by Th13;
hence  pi_1 (T,a) is trivial by TOPALG_1:def_5; ::_thesis: verum
end;
end;

theorem :: TOPALG_2:14
for a, b being real number st a <= b holds
for x, y being Point of (Closed-Interval-TSpace (a,b))
for P, Q being Path of x,y holds P,Q are_homotopic
proof
let a, b be real number ; ::_thesis: ( a <= b implies for x, y being Point of (Closed-Interval-TSpace (a,b))
for P, Q being Path of x,y holds P,Q are_homotopic )
assume A1: a <= b ; ::_thesis: for x, y being Point of (Closed-Interval-TSpace (a,b))
for P, Q being Path of x,y holds P,Q are_homotopic
let x, y be Point of (Closed-Interval-TSpace (a,b)); ::_thesis: for P, Q being Path of x,y holds P,Q are_homotopic
let P, Q be Path of x,y; ::_thesis: P,Q are_homotopic
 Closed-Interval-TSpace (a,b) is interval by A1, Th9;
hence  P,Q are_homotopic by Th12; ::_thesis: verum
end;

theorem :: TOPALG_2:15
for a, b being real number st a <= b holds
for x being Point of (Closed-Interval-TSpace (a,b))
for C being Loop of x holds the carrier of (pi_1 ((Closed-Interval-TSpace (a,b)),x)) = {(Class ((EqRel ((Closed-Interval-TSpace (a,b)),x)),C))}
proof
let a, b be real number ; ::_thesis: ( a <= b implies for x being Point of (Closed-Interval-TSpace (a,b))
for C being Loop of x holds the carrier of (pi_1 ((Closed-Interval-TSpace (a,b)),x)) = {(Class ((EqRel ((Closed-Interval-TSpace (a,b)),x)),C))} )
assume A1: a <= b ; ::_thesis: for x being Point of (Closed-Interval-TSpace (a,b))
for C being Loop of x holds the carrier of (pi_1 ((Closed-Interval-TSpace (a,b)),x)) = {(Class ((EqRel ((Closed-Interval-TSpace (a,b)),x)),C))}
let x be Point of (Closed-Interval-TSpace (a,b)); ::_thesis: for C being Loop of x holds the carrier of (pi_1 ((Closed-Interval-TSpace (a,b)),x)) = {(Class ((EqRel ((Closed-Interval-TSpace (a,b)),x)),C))}
let C be Loop of x; ::_thesis: the carrier of (pi_1 ((Closed-Interval-TSpace (a,b)),x)) = {(Class ((EqRel ((Closed-Interval-TSpace (a,b)),x)),C))}
 Closed-Interval-TSpace (a,b) is interval by A1, Th9;
hence  the carrier of (pi_1 ((Closed-Interval-TSpace (a,b)),x)) = {(Class ((EqRel ((Closed-Interval-TSpace (a,b)),x)),C))} by Th13; ::_thesis: verum
end;

theorem :: TOPALG_2:16
for x, y being Point of I[01]
for P, Q being Path of x,y holds P,Q are_homotopic by Th10, Th12;

theorem :: TOPALG_2:17
for x being Point of I[01]
for C being Loop of x holds the carrier of (pi_1 (I[01],x)) = {(Class ((EqRel (I[01],x)),C))} by Th10, Th13;

registration
let x be Point of I[01];
cluster FundamentalGroup (I[01],x) ->  trivial ;
coherence
 pi_1 (I[01],x) is trivial by Th10;
end;

registration
let n be Element of NAT ;
let T be non empty convex SubSpace of TOP-REAL n;
let P, Q be continuous Function of I[01],T;
cluster ConvexHomotopy (P,Q) ->  continuous ;
coherence
 ConvexHomotopy (P,Q) is continuous by Lm5;
end;

theorem :: TOPALG_2:18
for n being Element of NAT
for T being non empty convex SubSpace of TOP-REAL n
for a, b being Point of T
for P, Q being Path of a,b holds ConvexHomotopy (P,Q) is Homotopy of P,Q
proof
let n be Element of NAT ; ::_thesis: for T being non empty convex SubSpace of TOP-REAL n
for a, b being Point of T
for P, Q being Path of a,b holds ConvexHomotopy (P,Q) is Homotopy of P,Q
let T be non empty convex SubSpace of TOP-REAL n; ::_thesis: for a, b being Point of T
for P, Q being Path of a,b holds ConvexHomotopy (P,Q) is Homotopy of P,Q
let a, b be Point of T; ::_thesis: for P, Q being Path of a,b holds ConvexHomotopy (P,Q) is Homotopy of P,Q
let P, Q be Path of a,b; ::_thesis: ConvexHomotopy (P,Q) is Homotopy of P,Q
thus  P,Q are_homotopic by Th2; :: according to BORSUK_6:def_11 ::_thesis: ( ConvexHomotopy (P,Q) is continuous & ( for b1 being Element of the carrier of I[01] holds
( (ConvexHomotopy (P,Q)) . (b1,0) = P . b1 & (ConvexHomotopy (P,Q)) . (b1,1) = Q . b1 & (ConvexHomotopy (P,Q)) . (0,b1) = a & (ConvexHomotopy (P,Q)) . (1,b1) = b ) ) )
thus  ConvexHomotopy (P,Q) is continuous ; ::_thesis: for b1 being Element of the carrier of I[01] holds
( (ConvexHomotopy (P,Q)) . (b1,0) = P . b1 & (ConvexHomotopy (P,Q)) . (b1,1) = Q . b1 & (ConvexHomotopy (P,Q)) . (0,b1) = a & (ConvexHomotopy (P,Q)) . (1,b1) = b )
thus  for b1 being Element of the carrier of I[01] holds
( (ConvexHomotopy (P,Q)) . (b1,0) = P . b1 & (ConvexHomotopy (P,Q)) . (b1,1) = Q . b1 & (ConvexHomotopy (P,Q)) . (0,b1) = a & (ConvexHomotopy (P,Q)) . (1,b1) = b ) by Lm6; ::_thesis: verum
end;

registration
let T be non empty interval SubSpace of R^1 ;
let P, Q be continuous Function of I[01],T;
cluster R1Homotopy (P,Q) ->  continuous ;
coherence
 R1Homotopy (P,Q) is continuous by Lm8;
end;

theorem :: TOPALG_2:19
for T being non empty interval SubSpace of R^1
for a, b being Point of T
for P, Q being Path of a,b holds R1Homotopy (P,Q) is Homotopy of P,Q
proof
let T be non empty interval SubSpace of R^1 ; ::_thesis: for a, b being Point of T
for P, Q being Path of a,b holds R1Homotopy (P,Q) is Homotopy of P,Q
let a, b be Point of T; ::_thesis: for P, Q being Path of a,b holds R1Homotopy (P,Q) is Homotopy of P,Q
let P, Q be Path of a,b; ::_thesis: R1Homotopy (P,Q) is Homotopy of P,Q
thus  P,Q are_homotopic by Th12; :: according to BORSUK_6:def_11 ::_thesis: ( R1Homotopy (P,Q) is continuous & ( for b1 being Element of the carrier of I[01] holds
( (R1Homotopy (P,Q)) . (b1,0) = P . b1 & (R1Homotopy (P,Q)) . (b1,1) = Q . b1 & (R1Homotopy (P,Q)) . (0,b1) = a & (R1Homotopy (P,Q)) . (1,b1) = b ) ) )
thus  R1Homotopy (P,Q) is continuous ; ::_thesis: for b1 being Element of the carrier of I[01] holds
( (R1Homotopy (P,Q)) . (b1,0) = P . b1 & (R1Homotopy (P,Q)) . (b1,1) = Q . b1 & (R1Homotopy (P,Q)) . (0,b1) = a & (R1Homotopy (P,Q)) . (1,b1) = b )
thus  for b1 being Element of the carrier of I[01] holds
( (R1Homotopy (P,Q)) . (b1,0) = P . b1 & (R1Homotopy (P,Q)) . (b1,1) = Q . b1 & (R1Homotopy (P,Q)) . (0,b1) = a & (R1Homotopy (P,Q)) . (1,b1) = b ) by Lm9; ::_thesis: verum
end;