let x0, y0 be Point of (Tunit_circle 2); :: 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 S_{1}[ 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_{1}[x,y,z]

A8: for y being Element of the carrier of I[01]

for i being Element of {0} holds S_{1}[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

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

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 )

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],{0}:] by Lm4, ZFMISC_1:87;

reconsider ft = ft as Path of xt,yt by A4, A6, BORSUK_2:def 4;

A31: [j0,j0] in [: the carrier of I[01],{0}:] by Lm4, ZFMISC_1:87;

A32: dom F = the carrier of [:I[01],I[01]:] by FUNCT_2:def 1;

then A33: [: the carrier of I[01],{0}:] c= dom F by Lm3, Lm5, ZFMISC_1:95;

then dom (F | [: the carrier of I[01],{0}:]) = [: the carrier of I[01],{0}:] by RELAT_1:62;

then F | [: the carrier of I[01],{0}:] = CircleMap * Ft by A14, A13, A16, Lm12, FUNCT_1:2, RELAT_1:27;

then consider G being Function of [:I[01],I[01]:],R^1 such that

A34: G is continuous and

A35: F = CircleMap * G and

A36: G | [: the carrier of I[01],{0}:] = Ft and

A37: for H being Function of [:I[01],I[01]:],R^1 st H is continuous & F = CircleMap * H & H | [: the carrier of I[01],{0}:] = Ft holds

G = H by A2, A29, Th22;

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

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

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

.= 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;

then reconsider G = G as Homotopy of ft,Qt by A34, A48, BORSUK_6:def 11;

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 A34, A48; :: 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 A41, FUNCT_2:38; :: 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 [: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

hence G = F1 by A37, A50; :: thesis: verum

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 S

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

proof

consider Ft being Function of [: the carrier of I[01],{0}:],REAL such that
let x be Element of the carrier of I[01]; :: thesis: for y being Element of {0} ex z being Element of REAL st S_{1}[x,y,z]

ft . x in REAL by XREAL_0:def 1;

hence for y being Element of {0} ex z being Element of REAL st S_{1}[x,y,z]
; :: thesis: verum

end;ft . x in REAL by XREAL_0:def 1;

hence for y being Element of {0} ex z being Element of REAL st S

A8: for y being Element of the carrier of I[01]

for i being Element of {0} holds S

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

consider ft1 being Function of I[01],R^1 such that
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 A9, TOPALG_3:4

.= (CircleMap * (I[01] --> xt)) . x by FUNCT_2:15 ; :: thesis: verum

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

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

for p being Point of [:I[01],(Sspace 0[01]):]
let x be object ; :: thesis: ( x in dom (CircleMap * Ft) implies (F | [: the carrier of I[01],{0}:]) . x = (CircleMap * Ft) . x )

assume A17: x in dom (CircleMap * Ft) ; :: thesis: (F | [: the carrier of I[01],{0}:]) . x = (CircleMap * Ft) . x

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

end;assume A17: x in dom (CircleMap * Ft) ; :: thesis: (F | [: the carrier of I[01],{0}:]) . x = (CircleMap * Ft) . x

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

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

then A29:
Ft is continuous
by JGRAPH_2:10;
let p be Point of [:I[01],(Sspace 0[01]):]; :: thesis: 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 V be Subset of R^1; :: thesis: ( Ft . p in V & V is open implies ex W being Subset of [:I[01],(Sspace 0[01]):] 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 [:I[01],(Sspace 0[01]):] st

( p in W & W is open & Ft .: W c= V )

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_{1}[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: ( p in W & W is open & Ft .: W c= V )

thus p in W by A22, A23, ZFMISC_1:def 2; :: thesis: ( W is open & Ft .: W c= V )

thus W is open by A24, BORSUK_1:6; :: 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 [: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_{1}[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: verum

end;ex W being Subset of [:I[01],(Sspace 0[01]):] 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 [:I[01],(Sspace 0[01]):] 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 [:I[01],(Sspace 0[01]):] st

( p in W & W is open & Ft .: W c= V )

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

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: ( p in W & W is open & Ft .: W c= V )

thus p in W by A22, A23, ZFMISC_1:def 2; :: thesis: ( W is open & Ft .: W c= V )

thus W is open by A24, BORSUK_1:6; :: 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 [: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

hence y in V by A25, A27, A28; :: thesis: verum

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],{0}:] by Lm4, ZFMISC_1:87;

reconsider ft = ft as Path of xt,yt by A4, A6, BORSUK_2:def 4;

A31: [j0,j0] in [: the carrier of I[01],{0}:] by Lm4, ZFMISC_1:87;

A32: dom F = the carrier of [:I[01],I[01]:] by FUNCT_2:def 1;

then A33: [: the carrier of I[01],{0}:] c= dom F by Lm3, Lm5, ZFMISC_1:95;

then dom (F | [: the carrier of I[01],{0}:]) = [: the carrier of I[01],{0}:] by RELAT_1:62;

then F | [: the carrier of I[01],{0}:] = CircleMap * Ft by A14, A13, A16, Lm12, FUNCT_1:2, RELAT_1:27;

then consider G being Function of [:I[01],I[01]:],R^1 such that

A34: G is continuous and

A35: F = CircleMap * G and

A36: G | [: the carrier of I[01],{0}:] = Ft and

A37: for H being Function of [:I[01],I[01]:],R^1 st H is continuous & F = CircleMap * H & H | [: the carrier of I[01],{0}:] = Ft holds

G = H by A2, A29, Th22;

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

set g2 = I[01] --> yt;
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

.= (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: verum

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

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

A41:
CircleMap . yt in {y0}
by A39, TARSKI:def 1;
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 A39, TOPALG_3:4

.= (CircleMap * (I[01] --> yt)) . x by FUNCT_2:15 ; :: thesis: verum

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

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

(Prj2 (j1,G)) . 0 =
G . (j1,j0)
by Def3
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

.= (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: verum

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

.= 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: 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 ) ) )

then
ft,Qt are_homotopic
by A34;( 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],{0}:] by Lm4, ZFMISC_1:87;

hence G . (s,0) = Ft . (s,j0) by A36, FUNCT_1:49

.= ft . s by A8, Lm4 ;

:: 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 A46, A12, TOPALG_3:4 ; :: thesis: G . (1,t) = yt

thus G . (1,t) = (Prj2 (j1,G)) . t by Def3

.= yt by A45, A43, TOPALG_3:4 ; :: thesis: verum

end;( G . (0,t) = xt & G . (1,t) = yt ) ) )

[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: ( 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 A46, A12, TOPALG_3:4 ; :: thesis: G . (1,t) = yt

thus G . (1,t) = (Prj2 (j1,G)) . t by Def3

.= yt by A45, A43, TOPALG_3:4 ; :: thesis: verum

then reconsider G = G as Homotopy of ft,Qt by A34, A48, BORSUK_6:def 11;

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 A34, A48; :: 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 A41, FUNCT_2:38; :: 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 [: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

then
F1 | [: the carrier of I[01],{0}:] = Ft
by A32, A33, A14, A51, RELAT_1:62;
let x be object ; :: thesis: ( x in dom (F1 | [: the carrier of I[01],{0}:]) implies (F1 | [: the carrier of I[01],{0}:]) . x = Ft . x )

assume A53: x in dom (F1 | [: the carrier of I[01],{0}:]) ; :: thesis: (F1 | [: the carrier of I[01],{0}:]) . x = Ft . x

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

end;assume A53: x in dom (F1 | [: the carrier of I[01],{0}:]) ; :: thesis: (F1 | [: the carrier of I[01],{0}:]) . x = Ft . x

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

hence G = F1 by A37, A50; :: thesis: verum