let i be Integer; 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; 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;
BORSUK_2:def 7 ( F is continuous & ( for b1 being Element of the carrier of I[01] holds
( F . (b1,0) = (cLoop i) . b1 & F . (b1,1) = P . b1 & F . (0,b1) = c[10] & F . (1,b1) = c[10] ) ) )
thus
F is
continuous
;
for b1 being Element of the carrier of I[01] holds
( F . (b1,0) = (cLoop i) . b1 & F . (b1,1) = P . b1 & F . (0,b1) = c[10] & F . (1,b1) = c[10] )
let s be
Point of
I[01];
( 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
;
( 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
;
( 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
;
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
;
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
; verum