let x0, y0 be Point of (Tunit_circle 2); :: thesis:
let P, Q be Path of x0,y0; :: thesis:
let F be Homotopy of P,Q; :: thesis:
let xt be Point of R^1; :: thesis:
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:
then A2: F is continuous by BORSUK_6:def 11;
assume A3: xt in CircleMap " {x0} ; :: thesis:
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 S₁[ set , set , set ] means $3 = ft . $1;
A7: for x being Element of the carrier of I[01]
for y being Element of {0} ex z being Element of REAL st S₁[x,y,z]

proof

let x be Element of the carrier of I[01]; :: thesis:
ft . x in REAL by XREAL_0:def 1;
hence for y being Element of {0} ex z being Element of REAL st S₁[x,y,z] ; :: thesis:

end;

consider Ft being Function of [: the carrier of I[01],{0}:],REAL such that
A8: for y being Element of the carrier of I[01]
for i being Element of {0} holds S₁[y,i,Ft . (y,i)] from BINOP_1:sch 3(A7);
CircleMap . xt in {x0} by A3, FUNCT_2:38;
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:
thus the constant Loop of x0 . x = x0 by TOPALG_3:21
.= CircleMap . ((I[01] --> xt) . x) by A9, TOPALG_3:4
.= (CircleMap * (I[01] --> xt)) . x by FUNCT_2:15 ; :: thesis:

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 A3, Th23;
(I[01] --> xt) . j0 = xt by TOPALG_3:4;
then A12: ft1 = I[01] --> xt by A11, A10, FUNCT_2:63;
A13: rng Ft c= REAL ;
A14: dom Ft = [: the carrier of I[01],{0}:] by FUNCT_2:def 1;
A15: the carrier of [:I[01],(Sspace 0[01]):] = [: the carrier of I[01], the carrier of (Sspace 0[01]):] by BORSUK_1:def 2;
then reconsider Ft = Ft as Function of [:I[01],(Sspace 0[01]):],R^1 by Lm14, TOPMETR:17;
A16: for x being object st x in dom (CircleMap * Ft) holds
(F | [: the carrier of I[01],{0}:]) . x = (CircleMap * Ft) . x

proof

let x be object ; :: thesis:
assume A17: x in dom (CircleMap * Ft) ; :: thesis:
consider x1, x2 being object such that
A18: x1 in the carrier of I[01] and
A19: x2 in {0} and
A20: x = [x1,x2] by A15, A17, Lm14, ZFMISC_1:def 2;
x2 = 0 by A19, TARSKI:def 1;
hence (F | [: the carrier of I[01],{0}:]) . x = F . (x1,0) by A15, A17, A20, Lm14, FUNCT_1:49
.= (CircleMap * ft) . x1 by A1, A5, A18, BORSUK_6:def 11
.= CircleMap . (ft . x1) by A18, FUNCT_2:15
.= CircleMap . (Ft . (x1,x2)) by A8, A18, A19
.= (CircleMap * Ft) . x by A17, A20, FUNCT_1:12 ;
:: thesis:

end;

for p being Point of [:I[01],(Sspace 0[01]):]
for V being Subset of R^1 st Ft . p in V & V is open holds
ex W being Subset of [:I[01],(Sspace 0[01]):] st
( p in W & W is open & Ft .: W c= V )

proof

let p be Point of [:I[01],(Sspace 0[01]):]; :: thesis:
let V be Subset of R^1; :: thesis:
assume A21: ( Ft . p in V & V is open ) ; :: thesis:
consider p1 being Point of I[01], p2 being Point of (Sspace 0[01]) such that
A22: p = [p1,p2] by A15, DOMAIN_1:1;
S₁[p1,p2,Ft . (p1,p2)] by A8, Lm14;
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 A6, A21, A22, JGRAPH_2:10;
reconsider W1 = W1 as non empty Subset of I[01] by A23;
take W = [:W1,([#] (Sspace 0[01])):]; :: thesis:
thus p in W by A22, A23, ZFMISC_1:def 2; :: thesis:
thus W is open by A24, BORSUK_1:6; :: thesis:
let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in Ft .: W ; :: thesis:
then consider x being Element of [:I[01],(Sspace 0[01]):] 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 (Sspace 0[01]) such that
A28: x = [x1,x2] by A26, DOMAIN_1:1;
( S₁[x1,x2,Ft . (x1,x2)] & ft . x1 in ft .: W1 ) by A8, Lm14, FUNCT_2:35;
hence y in V by A25, A27, A28; :: thesis:

end;

proof

let x be Point of I[01]; :: thesis:
thus (CircleMap * (Prj2 (j0,G))) . x = CircleMap . ((Prj2 (j0,G)) . x) by FUNCT_2:15
.= CircleMap . (G . (j0,x)) by Def3
.= (CircleMap * G) . (j0,x) by Lm5, BINOP_1:18
.= x0 by A1, A35, BORSUK_6:def 11
.= the constant Loop of x0 . x by TOPALG_3:21 ; :: thesis:

end;

set g2 = I[01] --> yt;
A39: CircleMap . yt = P . j1 by A5, FUNCT_2:15
.= 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:
thus the constant Loop of y0 . x = y0 by TOPALG_3:21
.= CircleMap . ((I[01] --> yt) . x) by A39, TOPALG_3:4
.= (CircleMap * (I[01] --> yt)) . x by FUNCT_2:15 ; :: thesis:

end;

A41: CircleMap . yt in {y0} by A39, TARSKI:def 1;
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 A42, A40, FUNCT_2:63;
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:
thus (CircleMap * (Prj2 (j1,G))) . x = CircleMap . ((Prj2 (j1,G)) . x) by FUNCT_2:15
.= CircleMap . (G . (j1,x)) by Def3
.= (CircleMap * G) . (j1,x) by Lm5, BINOP_1:18
.= y0 by A1, A35, BORSUK_6:def 11
.= the constant Loop of y0 . x by TOPALG_3:21 ; :: thesis:

end;

(Prj2 (j1,G)) . 0 = G . (j1,j0) by Def3
.= Ft . (j1,j0) by A36, A30, FUNCT_1:49
.= yt by A8, Lm4 ;
then A45: ft2 = Prj2 (j1,G) by A34, A42, A44, FUNCT_2:63;
(Prj2 (j0,G)) . 0 = G . (j0,j0) by Def3
.= Ft . (j0,j0) by A36, A31, FUNCT_1:49
.= xt by A4, A8, Lm4 ;
then A46: ft1 = Prj2 (j0,G) by A34, A11, A38, FUNCT_2:63;
set Qt = Prj1 (j1,G);
A47: (Prj1 (j1,G)) . 0 = G . (j0,j1) by Def2
.= (Prj2 (j0,G)) . j1 by Def3
.= xt by A46, A12, TOPALG_3:4 ;
(Prj1 (j1,G)) . 1 = G . (j1,j1) by Def2
.= (Prj2 (j1,G)) . j1 by Def3
.= yt by A45, A43, TOPALG_3:4 ;
then reconsider Qt = Prj1 (j1,G) as Path of xt,yt by A34, A47, BORSUK_2:def 4;

A48: now :: thesis:

let s be Point of I[01]; :: thesis:
[s,0] in [: the carrier of I[01],{0}:] by Lm4, ZFMISC_1:87;
hence G . (s,0) = Ft . (s,j0) by A36, FUNCT_1:49
.= ft . s by A8, Lm4 ;
:: thesis:
thus G . (s,1) = Qt . s by Def2; :: thesis:
let t be Point of I[01]; :: thesis:
thus G . (0,t) = (Prj2 (j0,G)) . t by Def3
.= xt by A46, A12, TOPALG_3:4 ; :: thesis:
thus G . (1,t) = (Prj2 (j1,G)) . t by Def3
.= yt by A45, A43, TOPALG_3:4 ; :: thesis:

end;

then ft,Qt are_homotopic by A34;
then reconsider G = G as Homotopy of ft,Qt by A34, A48, BORSUK_6:def 11;
take ft ; :: thesis:
take Qt ; :: thesis:
take G ; :: thesis:
thus A49: ft,Qt are_homotopic by A34, A48; :: thesis:
thus F = CircleMap * G by A35; :: thesis:
thus yt in CircleMap " {y0} by A41, FUNCT_2:38; :: thesis:
let F1 be Homotopy of ft,Qt; :: thesis:
assume A50: F = CircleMap * F1 ; :: thesis:
A51: dom F1 = the carrier of [:I[01],I[01]:] by FUNCT_2:def 1;
then A52: dom (F1 | [: the carrier of I[01],{0}:]) = [: the carrier of I[01],{0}:] by A32, A33, RELAT_1:62;
for x being object st x in dom (F1 | [: the carrier of I[01],{0}:]) holds
(F1 | [: the carrier of I[01],{0}:]) . x = Ft . x

proof

let x be object ; :: thesis:
assume A53: x in dom (F1 | [: the carrier of I[01],{0}:]) ; :: thesis:
then consider x1, x2 being object such that
A54: x1 in the carrier of I[01] and
A55: x2 in {0} and
A56: x = [x1,x2] by A52, ZFMISC_1:def 2;
A57: x2 = 0 by A55, TARSKI:def 1;
thus (F1 | [: the carrier of I[01],{0}:]) . x = F1 . (x1,x2) by A53, A56, FUNCT_1:47
.= ft . x1 by A49, A54, A57, BORSUK_6:def 11
.= Ft . (x1,x2) by A8, A54, A55
.= Ft . x by A56 ; :: thesis:

end;

then F1 | [: the carrier of I[01],{0}:] = Ft by A32, A33, A14, A51, RELAT_1:62;
hence G = F1 by A37, A50; :: thesis: