let i be Integer; :: thesis: for f being Path of R^1 0 , R^1 i holds Ciso . i = Class (EqRel (Tunit_circle 2),c[10] ),(CircleMap * f)
let f be Path of R^1 0 , R^1 i; :: thesis: Ciso . i = Class (EqRel (Tunit_circle 2),c[10] ),(CircleMap * f)
set P = CircleMap * f;
CircleMap * f is Loop of c[10]

proof

thus CircleMap * f is continuous ; :: according to BORSUK_2:def 4 :: thesis: ( (CircleMap * f) . 0 = c[10] & (CircleMap * f) . 1 = c[10] )
thus (CircleMap * f) . 0 = CircleMap . (f . j0) by FUNCT_2:21
.= CircleMap . (R^1 0 ) by BORSUK_2:def 4
.= CircleMap . 0 by TOPREALB:def 2
.= |[(cos ((2 * PI ) * 0 )),(sin ((2 * PI ) * 0 ))]| by TOPREALB:def 11
.= c[10] by SIN_COS:34, TOPREALB:def 8 ; :: thesis: (CircleMap * f) . 1 = c[10]
thus (CircleMap * f) . 1 = CircleMap . (f . j1) by FUNCT_2:21
.= CircleMap . (R^1 i) by BORSUK_2:def 4
.= CircleMap . i by TOPREALB:def 2
.= |[(cos (((2 * PI ) * i) + 0 )),(sin (((2 * PI ) * i) + 0 ))]| by TOPREALB:def 11
.= |[(cos 0 ),(sin (((2 * PI ) * i) + 0 ))]| by COMPLEX2:10
.= c[10] by COMPLEX2:9, SIN_COS:34, TOPREALB:def 8 ; :: thesis: verum

end;

then reconsider P = CircleMap * f as Loop of c[10] ;
A1: cLoop i = CircleMap * (ExtendInt i) by Th20;
A2: cLoop i,P are_homotopic

proof

reconsider J = R^1 as non empty convex SubSpace of R^1 ;
reconsider r0 = R^1 0 , ri = R^1 i as Point of J ;
reconsider O = ExtendInt i, ff = f as Path of r0,ri ;
reconsider G = R1Homotopy O,ff as Function of [:I[01] ,I[01] :],R^1 ;
take F = CircleMap * G; :: according to BORSUK_2:def 7 :: thesis: ( F is continuous & ( for b₁ being Element of the carrier of I[01] holds
( F . b₁,0 = (cLoop i) . b₁ & F . b₁,1 = P . b₁ & F . 0 ,b₁ = c[10] & F . 1,b₁ = c[10] ) ) )
thus F is continuous ; :: thesis: for b₁ being Element of the carrier of I[01] holds
( F . b₁,0 = (cLoop i) . b₁ & F . b₁,1 = P . b₁ & F . 0 ,b₁ = c[10] & F . 1,b₁ = c[10] )
let s be Point of I[01] ; :: thesis: ( F . s,0 = (cLoop i) . s & F . s,1 = P . s & F . 0 ,s = c[10] & F . 1,s = c[10] )
thus F . s,0 = CircleMap . (G . s,j0) by Lm5, BINOP_1:30
.= CircleMap . (((1 - j0) * ((ExtendInt i) . s)) + (j0 * (f . s))) by TOPALG_2:def 5
.= (cLoop i) . s by A1, FUNCT_2:21 ; :: thesis: ( F . s,1 = P . s & F . 0 ,s = c[10] & F . 1,s = c[10] )
thus F . s,1 = CircleMap . (G . s,j1) by Lm5, BINOP_1:30
.= CircleMap . (((1 - j1) * ((ExtendInt i) . s)) + (j1 * (f . s))) by TOPALG_2:def 5
.= P . s by FUNCT_2:21 ; :: thesis: ( F . 0 ,s = c[10] & F . 1,s = c[10] )
thus F . 0 ,s = CircleMap . (G . j0,s) by Lm5, BINOP_1:30
.= CircleMap . (((1 - s) * ((ExtendInt i) . j0)) + (s * (f . j0))) by TOPALG_2:def 5
.= CircleMap . (((1 - s) * (R^1 0 )) + (s * (f . j0))) by BORSUK_2:def 4
.= CircleMap . (((1 - s) * (R^1 0 )) + (s * (R^1 0 ))) by BORSUK_2:def 4
.= CircleMap . (((1 - s) * 0 ) + (s * 0 )) by TOPREALB:def 2
.= c[10] by TOPREALB:33 ; :: thesis: F . 1,s = c[10]
thus F . 1,s = CircleMap . (G . j1,s) by Lm5, BINOP_1:30
.= CircleMap . (((1 - s) * ((ExtendInt i) . j1)) + (s * (f . j1))) by TOPALG_2:def 5
.= CircleMap . (((1 - s) * (R^1 i)) + (s * (f . j1))) by BORSUK_2:def 4
.= CircleMap . (((1 - s) * (R^1 i)) + (s * (R^1 i))) by BORSUK_2:def 4
.= CircleMap . i by TOPREALB:def 2
.= c[10] by TOPREALB:33 ; :: thesis: verum

end;

thus Ciso . i = Class (EqRel (Tunit_circle 2),c[10] ),(cLoop i) by Def5
.= Class (EqRel (Tunit_circle 2),c[10] ),(CircleMap * f) by A2, TOPALG_1:47 ; :: thesis: verum