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:
consider cP1 being constant Loop of x0;
set g1 = I[01] --> xt;
consider cP2 being constant Loop of y0;
assume A1: P,Q are_homotopic ; :: thesis:
then A2: F is continuous by BORSUK_6:def 13;
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] ;
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:46;
then A9: CircleMap . xt = x0 by TARSKI:def 1;
A10: for x being Point of I[01] holds cP1 . x = (CircleMap * (I[01] --> xt)) . x

end;

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 )

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:9;
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:20;
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:46; :: thesis:
let y be set ; :: 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:116;
consider x1 being Element of W1, x2 being Point of (Sspace 0[01] ) such that
A28: x = [x1,x2] by A26, DOMAIN_1:9;
( S₁[x1,x2,Ft . x1,x2] & ft . x1 in ft .: W1 ) by A8, Lm14, FUNCT_2:43;
hence y in V by A25, A27, A28; :: thesis:

end;

let x be Point of I[01] ; :: thesis:
thus (CircleMap * (Prj2 j0,G)) . x = CircleMap . ((Prj2 j0,G) . x) by FUNCT_2:21
.= CircleMap . (G . j0,x) by Def3
.= (CircleMap * G) . j0,x by Lm5, BINOP_1:30
.= x0 by A1, A35, BORSUK_6:def 13
.= cP1 . x by TOPALG_3:22 ; :: thesis:

end;

set g2 = I[01] --> yt;
A39: CircleMap . yt = P . j1 by A5, FUNCT_2:21
.= y0 by BORSUK_2:def 4 ;
A40: for x being Point of I[01] holds cP2 . x = (CircleMap * (I[01] --> yt)) . x

end;

let x be Point of I[01] ; :: thesis:
thus (CircleMap * (Prj2 j1,G)) . x = CircleMap . ((Prj2 j1,G) . x) by FUNCT_2:21
.= CircleMap . (G . j1,x) by Def3
.= (CircleMap * G) . j1,x by Lm5, BINOP_1:30
.= y0 by A1, A35, BORSUK_6:def 13
.= cP2 . x by TOPALG_3:22 ; :: thesis:

end;

(Prj2 j1,G) . 0 = G . j1,j0 by Def3
.= Ft . j1,j0 by A36, A30, FUNCT_1:72
.= yt by A8, Lm4 ;
then A45: ft2 = Prj2 j1,G by A34, A42, A44, FUNCT_2:113;
(Prj2 j0,G) . 0 = G . j0,j0 by Def3
.= Ft . j0,j0 by A36, A31, FUNCT_1:72
.= xt by A4, A8, Lm4 ;
then A46: ft1 = Prj2 j0,G by A34, A11, A38, FUNCT_2:113;
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:5 ;
(Prj1 j1,G) . 1 = G . j1,j1 by Def2
.= (Prj2 j1,G) . j1 by Def3
.= yt by A45, A43, TOPALG_3:5 ;
then reconsider Qt = Prj1 j1,G as Path of xt,yt by A34, A47, BORSUK_2:def 4;

A48: now

let s be Point of I[01] ; :: thesis:
[s,0 ] in [:the carrier of I[01] ,{0 }:] by Lm4, ZFMISC_1:106;
hence G . s,0 = Ft . s,j0 by A36, FUNCT_1:72
.= 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:5 ; :: thesis:
thus G . 1,t = (Prj2 j1,G) . t by Def3
.= yt by A45, A43, TOPALG_3:5 ; :: thesis:

end;

let x be set ; :: thesis:
assume A53: x in dom (F1 | [:the carrier of I[01] ,{0 }:]) ; :: thesis:
then consider x1, x2 being set 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:70
.= ft . x1 by A49, A54, A57, BORSUK_6:def 13
.= Ft . x1,x2 by A8, A54, A55
.= Ft . x by A56 ; :: thesis:

end;