let x0, y0 be Point of (); :: thesis: for P, Q being Path of x0,y0
for F being Homotopy of P,Q
for xt being Point of R^1 st P,Q are_homotopic & xt in CircleMap " {x0} holds
ex yt being Point of R^1 ex Pt, Qt being Path of xt,yt ex Ft being Homotopy of Pt,Qt st
( Pt,Qt are_homotopic & F = CircleMap * Ft & yt in CircleMap " {y0} & ( for F1 being Homotopy of Pt,Qt st F = CircleMap * F1 holds
Ft = F1 ) )

let P, Q be Path of x0,y0; :: thesis: for F being Homotopy of P,Q
for xt being Point of R^1 st P,Q are_homotopic & xt in CircleMap " {x0} holds
ex yt being Point of R^1 ex Pt, Qt being Path of xt,yt ex Ft being Homotopy of Pt,Qt st
( Pt,Qt are_homotopic & F = CircleMap * Ft & yt in CircleMap " {y0} & ( for F1 being Homotopy of Pt,Qt st F = CircleMap * F1 holds
Ft = F1 ) )

let F be Homotopy of P,Q; :: thesis: for xt being Point of R^1 st P,Q are_homotopic & xt in CircleMap " {x0} holds
ex yt being Point of R^1 ex Pt, Qt being Path of xt,yt ex Ft being Homotopy of Pt,Qt st
( Pt,Qt are_homotopic & F = CircleMap * Ft & yt in CircleMap " {y0} & ( for F1 being Homotopy of Pt,Qt st F = CircleMap * F1 holds
Ft = F1 ) )

let xt be Point of R^1; :: thesis: ( P,Q are_homotopic & xt in CircleMap " {x0} implies ex yt being Point of R^1 ex Pt, Qt being Path of xt,yt ex Ft being Homotopy of Pt,Qt st
( Pt,Qt are_homotopic & F = CircleMap * Ft & yt in CircleMap " {y0} & ( for F1 being Homotopy of Pt,Qt st F = CircleMap * F1 holds
Ft = F1 ) ) )

set cP1 = the constant Loop of x0;
set g1 = I[01] --> xt;
set cP2 = the constant Loop of y0;
assume A1: P,Q are_homotopic ; :: thesis: ( not xt in CircleMap " {x0} or ex yt being Point of R^1 ex Pt, Qt being Path of xt,yt ex Ft being Homotopy of Pt,Qt st
( Pt,Qt are_homotopic & F = CircleMap * Ft & yt in CircleMap " {y0} & ( for F1 being Homotopy of Pt,Qt st F = CircleMap * F1 holds
Ft = F1 ) ) )

then A2: F is continuous by BORSUK_6:def 11;
assume A3: xt in CircleMap " {x0} ; :: thesis: ex yt being Point of R^1 ex Pt, Qt being Path of xt,yt ex Ft being Homotopy of Pt,Qt st
( Pt,Qt are_homotopic & F = CircleMap * Ft & yt in CircleMap " {y0} & ( for F1 being Homotopy of Pt,Qt st F = CircleMap * F1 holds
Ft = F1 ) )

then consider ft being Function of I[01],R^1 such that
A4: ft . 0 = xt and
A5: P = CircleMap * ft and
A6: ft is continuous and
for f1 being Function of I[01],R^1 st f1 is continuous & P = CircleMap * f1 & f1 . 0 = xt holds
ft = f1 by Th23;
defpred S1[ set , set , set ] means \$3 = ft . \$1;
A7: for x being Element of the carrier of I[01]
for y being Element of ex z being Element of REAL st S1[x,y,z]
proof
let x be Element of the carrier of I[01]; :: thesis: for y being Element of ex z being Element of REAL st S1[x,y,z]
ft . x in REAL by XREAL_0:def 1;
hence for y being Element of ex z being Element of REAL st S1[x,y,z] ; :: thesis: verum
end;
consider Ft being Function of [: the carrier of I[01],:],REAL such that
A8: for y being Element of the carrier of I[01]
for i being Element of holds S1[y,i,Ft . (y,i)] from CircleMap . xt in {x0} by ;
then A9: CircleMap . xt = x0 by TARSKI:def 1;
A10: for x being Point of I[01] holds the constant Loop of x0 . x = (CircleMap * (I[01] --> xt)) . x
proof
let x be Point of I[01]; :: thesis: the constant Loop of x0 . x = (CircleMap * (I[01] --> xt)) . x
thus the constant Loop of x0 . x = x0 by TOPALG_3:21
.= CircleMap . ((I[01] --> xt) . x) by
.= (CircleMap * (I[01] --> xt)) . x by FUNCT_2:15 ; :: thesis: verum
end;
consider ft1 being Function of I[01],R^1 such that
ft1 . 0 = xt and
the constant Loop of x0 = CircleMap * ft1 and
ft1 is continuous and
A11: for f1 being Function of I[01],R^1 st f1 is continuous & the constant Loop of x0 = CircleMap * f1 & f1 . 0 = xt holds
ft1 = f1 by ;
(I[01] --> xt) . j0 = xt by TOPALG_3:4;
then A12: ft1 = I[01] --> xt by ;
A13: rng Ft c= REAL ;
A14: dom Ft = [: the carrier of I[01],:] by FUNCT_2:def 1;
A15: the carrier of = [: the carrier of I[01], the carrier of ():] by BORSUK_1:def 2;
then reconsider Ft = Ft as Function of ,R^1 by ;
A16: for x being object st x in dom () holds
(F | [: the carrier of I[01],:]) . x = () . x
proof
let x be object ; :: thesis: ( x in dom () implies (F | [: the carrier of I[01],:]) . x = () . x )
assume A17: x in dom () ; :: thesis: (F | [: the carrier of I[01],:]) . x = () . x
consider x1, x2 being object such that
A18: x1 in the carrier of I[01] and
A19: x2 in and
A20: x = [x1,x2] by ;
x2 = 0 by ;
hence (F | [: the carrier of I[01],:]) . x = F . (x1,0) by
.= () . x1 by
.= CircleMap . (ft . x1) by
.= CircleMap . (Ft . (x1,x2)) by A8, A18, A19
.= () . x by ;
:: thesis: verum
end;
for p being Point of
for V being Subset of R^1 st Ft . p in V & V is open holds
ex W being Subset of st
( p in W & W is open & Ft .: W c= V )
proof
let p be Point of ; :: thesis: for V being Subset of R^1 st Ft . p in V & V is open holds
ex W being Subset of st
( p in W & W is open & Ft .: W c= V )

let V be Subset of R^1; :: thesis: ( Ft . p in V & V is open implies ex W being Subset of st
( p in W & W is open & Ft .: W c= V ) )

assume A21: ( Ft . p in V & V is open ) ; :: thesis: ex W being Subset of st
( p in W & W is open & Ft .: W c= V )

consider p1 being Point of I[01], p2 being Point of () such that
A22: p = [p1,p2] by ;
S1[p1,p2,Ft . (p1,p2)] by ;
then consider W1 being Subset of I[01] such that
A23: p1 in W1 and
A24: W1 is open and
A25: ft .: W1 c= V by ;
reconsider W1 = W1 as non empty Subset of I[01] by A23;
take W = [:W1,():]; :: thesis: ( p in W & W is open & Ft .: W c= V )
thus p in W by ; :: thesis: ( W is open & Ft .: W c= V )
thus W is open by ; :: thesis: Ft .: W c= V
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Ft .: W or y in V )
assume y in Ft .: W ; :: thesis: y in V
then consider x being Element of such that
A26: x in W and
A27: y = Ft . x by FUNCT_2:65;
consider x1 being Element of W1, x2 being Point of () such that
A28: x = [x1,x2] by ;
( S1[x1,x2,Ft . (x1,x2)] & ft . x1 in ft .: W1 ) by ;
hence y in V by ; :: thesis: verum
end;
then A29: Ft is continuous by JGRAPH_2:10;
take yt = ft . j1; :: thesis: ex Pt, Qt being Path of xt,yt ex Ft being Homotopy of Pt,Qt st
( Pt,Qt are_homotopic & F = CircleMap * Ft & yt in CircleMap " {y0} & ( for F1 being Homotopy of Pt,Qt st F = CircleMap * F1 holds
Ft = F1 ) )

A30: [j1,j0] in [: the carrier of I[01],:] by ;
reconsider ft = ft as Path of xt,yt by ;
A31: [j0,j0] in [: the carrier of I[01],:] by ;
A32: dom F = the carrier of by FUNCT_2:def 1;
then A33: [: the carrier of I[01],:] c= dom F by ;
then dom (F | [: the carrier of I[01],:]) = [: the carrier of I[01],:] by RELAT_1:62;
then F | [: the carrier of I[01],:] = CircleMap * Ft by ;
then consider G being Function of ,R^1 such that
A34: G is continuous and
A35: F = CircleMap * G and
A36: G | [: the carrier of I[01],:] = Ft and
A37: for H being Function of ,R^1 st H is continuous & F = CircleMap * H & H | [: the carrier of I[01],:] = Ft holds
G = H by ;
set sM0 = Prj2 (j0,G);
A38: for x being Point of I[01] holds the constant Loop of x0 . x = (CircleMap * (Prj2 (j0,G))) . x
proof
let x be Point of I[01]; :: thesis: the constant Loop of x0 . x = (CircleMap * (Prj2 (j0,G))) . x
thus (CircleMap * (Prj2 (j0,G))) . x = CircleMap . ((Prj2 (j0,G)) . x) by FUNCT_2:15
.= CircleMap . (G . (j0,x)) by Def3
.= () . (j0,x) by
.= x0 by
.= the constant Loop of x0 . x by TOPALG_3:21 ; :: thesis: verum
end;
set g2 = I[01] --> yt;
A39: CircleMap . yt = P . j1 by
.= y0 by BORSUK_2:def 4 ;
A40: for x being Point of I[01] holds the constant Loop of y0 . x = (CircleMap * (I[01] --> yt)) . x
proof
let x be Point of I[01]; :: thesis: the constant Loop of y0 . x = (CircleMap * (I[01] --> yt)) . x
thus the constant Loop of y0 . x = y0 by TOPALG_3:21
.= CircleMap . ((I[01] --> yt) . x) by
.= (CircleMap * (I[01] --> yt)) . x by FUNCT_2:15 ; :: thesis: verum
end;
A41: CircleMap . yt in {y0} by ;
then yt in CircleMap " {y0} by FUNCT_2:38;
then consider ft2 being Function of I[01],R^1 such that
ft2 . 0 = yt and
the constant Loop of y0 = CircleMap * ft2 and
ft2 is continuous and
A42: for f1 being Function of I[01],R^1 st f1 is continuous & the constant Loop of y0 = CircleMap * f1 & f1 . 0 = yt holds
ft2 = f1 by Th23;
(I[01] --> yt) . j0 = yt by TOPALG_3:4;
then A43: ft2 = I[01] --> yt by ;
set sM1 = Prj2 (j1,G);
A44: for x being Point of I[01] holds the constant Loop of y0 . x = (CircleMap * (Prj2 (j1,G))) . x
proof
let x be Point of I[01]; :: thesis: the constant Loop of y0 . x = (CircleMap * (Prj2 (j1,G))) . x
thus (CircleMap * (Prj2 (j1,G))) . x = CircleMap . ((Prj2 (j1,G)) . x) by FUNCT_2:15
.= CircleMap . (G . (j1,x)) by Def3
.= () . (j1,x) by
.= y0 by
.= the constant Loop of y0 . x by TOPALG_3:21 ; :: thesis: verum
end;
(Prj2 (j1,G)) . 0 = G . (j1,j0) by Def3
.= Ft . (j1,j0) by
.= yt by ;
then A45: ft2 = Prj2 (j1,G) by ;
(Prj2 (j0,G)) . 0 = G . (j0,j0) by Def3
.= Ft . (j0,j0) by
.= xt by A4, A8, Lm4 ;
then A46: ft1 = Prj2 (j0,G) by ;
set Qt = Prj1 (j1,G);
A47: (Prj1 (j1,G)) . 0 = G . (j0,j1) by Def2
.= (Prj2 (j0,G)) . j1 by Def3
.= xt by ;
(Prj1 (j1,G)) . 1 = G . (j1,j1) by Def2
.= (Prj2 (j1,G)) . j1 by Def3
.= yt by ;
then reconsider Qt = Prj1 (j1,G) as Path of xt,yt by ;
A48: now :: thesis: for s being Point of I[01] holds
( G . (s,0) = ft . s & G . (s,1) = Qt . s & ( for t being Point of I[01] holds
( G . (0,t) = xt & G . (1,t) = yt ) ) )
let s be Point of I[01]; :: thesis: ( G . (s,0) = ft . s & G . (s,1) = Qt . s & ( for t being Point of I[01] holds
( G . (0,t) = xt & G . (1,t) = yt ) ) )

[s,0] in [: the carrier of I[01],:] by ;
hence G . (s,0) = Ft . (s,j0) by
.= ft . s by ;
:: thesis: ( G . (s,1) = Qt . s & ( for t being Point of I[01] holds
( G . (0,t) = xt & G . (1,t) = yt ) ) )

thus G . (s,1) = Qt . s by Def2; :: thesis: for t being Point of I[01] holds
( G . (0,t) = xt & G . (1,t) = yt )

let t be Point of I[01]; :: thesis: ( G . (0,t) = xt & G . (1,t) = yt )
thus G . (0,t) = (Prj2 (j0,G)) . t by Def3
.= xt by ; :: thesis: G . (1,t) = yt
thus G . (1,t) = (Prj2 (j1,G)) . t by Def3
.= yt by ; :: thesis: verum
end;
then ft,Qt are_homotopic by A34;
then reconsider G = G as Homotopy of ft,Qt by ;
take ft ; :: thesis: ex Qt being Path of xt,yt ex Ft being Homotopy of ft,Qt st
( ft,Qt are_homotopic & F = CircleMap * Ft & yt in CircleMap " {y0} & ( for F1 being Homotopy of ft,Qt st F = CircleMap * F1 holds
Ft = F1 ) )

take Qt ; :: thesis: ex Ft being Homotopy of ft,Qt st
( ft,Qt are_homotopic & F = CircleMap * Ft & yt in CircleMap " {y0} & ( for F1 being Homotopy of ft,Qt st F = CircleMap * F1 holds
Ft = F1 ) )

take G ; :: thesis: ( ft,Qt are_homotopic & F = CircleMap * G & yt in CircleMap " {y0} & ( for F1 being Homotopy of ft,Qt st F = CircleMap * F1 holds
G = F1 ) )

thus A49: ft,Qt are_homotopic by ; :: thesis: ( F = CircleMap * G & yt in CircleMap " {y0} & ( for F1 being Homotopy of ft,Qt st F = CircleMap * F1 holds
G = F1 ) )

thus F = CircleMap * G by A35; :: thesis: ( yt in CircleMap " {y0} & ( for F1 being Homotopy of ft,Qt st F = CircleMap * F1 holds
G = F1 ) )

thus yt in CircleMap " {y0} by ; :: thesis: for F1 being Homotopy of ft,Qt st F = CircleMap * F1 holds
G = F1

let F1 be Homotopy of ft,Qt; :: thesis: ( F = CircleMap * F1 implies G = F1 )
assume A50: F = CircleMap * F1 ; :: thesis: G = F1
A51: dom F1 = the carrier of by FUNCT_2:def 1;
then A52: dom (F1 | [: the carrier of I[01],:]) = [: the carrier of I[01],:] by ;
for x being object st x in dom (F1 | [: the carrier of I[01],:]) holds
(F1 | [: the carrier of I[01],:]) . x = Ft . x
proof
let x be object ; :: thesis: ( x in dom (F1 | [: the carrier of I[01],:]) implies (F1 | [: the carrier of I[01],:]) . x = Ft . x )
assume A53: x in dom (F1 | [: the carrier of I[01],:]) ; :: thesis: (F1 | [: the carrier of I[01],:]) . x = Ft . x
then consider x1, x2 being object such that
A54: x1 in the carrier of I[01] and
A55: x2 in and
A56: x = [x1,x2] by ;
A57: x2 = 0 by ;
thus (F1 | [: the carrier of I[01],:]) . x = F1 . (x1,x2) by
.= ft . x1 by
.= Ft . (x1,x2) by A8, A54, A55
.= Ft . x by A56 ; :: thesis: verum
end;
then F1 | [: the carrier of I[01],:] = Ft by ;
hence G = F1 by ; :: thesis: verum