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;
A1: (CircleMap * f) . 0 = CircleMap . (f . j0) by FUNCT_2:15
.= 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:31, TOPREALB:def 8 ;
(CircleMap * f) . 1 = CircleMap . (f . j1) by FUNCT_2:15
.= 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:9
.= c[10] by COMPLEX2:8, SIN_COS:31, TOPREALB:def 8 ;
then reconsider P = CircleMap * f as Loop of c[10] by A1, BORSUK_2:def 4;
A2: cLoop i = CircleMap * (ExtendInt i) by Th20;
A3: cLoop i,P are_homotopic

proof

reconsider J = R^1 as non empty interval 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:18
.= CircleMap . (((1 - j0) * ((ExtendInt i) . s)) + (j0 * (f . s))) by TOPALG_2:def 4
.= (cLoop i) . s by A2, FUNCT_2:15 ; :: 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:18
.= CircleMap . (((1 - j1) * ((ExtendInt i) . s)) + (j1 * (f . s))) by TOPALG_2:def 4
.= P . s by FUNCT_2:15 ; :: thesis: ( F . (0,s) = c[10] & F . (1,s) = c[10] )
thus F . (0,s) = CircleMap . (G . (j0,s)) by Lm5, BINOP_1:18
.= CircleMap . (((1 - s) * ((ExtendInt i) . j0)) + (s * (f . j0))) by TOPALG_2:def 4
.= 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:32 ; :: thesis: F . (1,s) = c[10]
thus F . (1,s) = CircleMap . (G . (j1,s)) by Lm5, BINOP_1:18
.= CircleMap . (((1 - s) * ((ExtendInt i) . j1)) + (s * (f . j1))) by TOPALG_2:def 4
.= 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:32 ; :: 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 A3, TOPALG_1:46 ; :: thesis: verum