let i be Integer; :: thesis: for f being Path of R^1 0, R^1 i holds Ciso . i = Class ((EqRel ((),c[10])),())
let f be Path of R^1 0, R^1 i; :: thesis: Ciso . i = Class ((EqRel ((),c[10])),())
set P = CircleMap * f;
A1: () . 0 = CircleMap . (f . j0) by FUNCT_2:15
.= CircleMap . () 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 ;
() . 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
.= |[(),(sin (((2 * PI) * i) + 0))]| by COMPLEX2:9
.= c[10] by ;
then reconsider P = CircleMap * f as Loop of c[10] by ;
A2: cLoop i = CircleMap * () 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 ,R^1 ;
take F = CircleMap * G; :: according to BORSUK_2:def 7 :: thesis: ( F is continuous & ( for b1 being Element of the carrier of I[01] holds
( F . (b1,0) = () . b1 & F . (b1,1) = P . b1 & F . (0,b1) = c[10] & F . (1,b1) = c[10] ) ) )

thus F is continuous ; :: thesis: for b1 being Element of the carrier of I[01] holds
( F . (b1,0) = () . b1 & F . (b1,1) = P . b1 & F . (0,b1) = c[10] & F . (1,b1) = c[10] )

let s be Point of I[01]; :: thesis: ( F . (s,0) = () . 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
.= CircleMap . (((1 - j0) * (() . s)) + (j0 * (f . s))) by TOPALG_2:def 4
.= () . s by ; :: 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
.= CircleMap . (((1 - j1) * (() . 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
.= CircleMap . (((1 - s) * (() . j0)) + (s * (f . j0))) by TOPALG_2:def 4
.= CircleMap . (((1 - s) * ()) + (s * (f . j0))) by BORSUK_2:def 4
.= CircleMap . (((1 - s) * ()) + (s * ())) 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
.= CircleMap . (((1 - s) * (() . 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 ((),c[10])),()) by Def5
.= Class ((EqRel ((),c[10])),()) by ; :: thesis: verum