set f = cLoop n;

cLoop n = CircleMap * (ExtendInt n) by Th20;

hence cLoop n is continuous ; :: according to BORSUK_2:def 4 :: thesis: ( (cLoop n) . 0 = c[10] & (cLoop n) . 1 = c[10] )

thus (cLoop n) . 0 = |[(cos (((2 * PI) * n) * j0)),(sin (((2 * PI) * n) * j0))]| by Def4

.= c[10] by SIN_COS:31, TOPREALB:def 8 ; :: thesis: (cLoop n) . 1 = c[10]

thus (cLoop n) . 1 = |[(cos (((2 * PI) * n) * j1)),(sin (((2 * PI) * n) * j1))]| by Def4

.= |[(cos 0),(sin (((2 * PI) * n) + 0))]| by COMPLEX2:9

.= c[10] by COMPLEX2:8, SIN_COS:31, TOPREALB:def 8 ; :: thesis: verum

cLoop n = CircleMap * (ExtendInt n) by Th20;

hence cLoop n is continuous ; :: according to BORSUK_2:def 4 :: thesis: ( (cLoop n) . 0 = c[10] & (cLoop n) . 1 = c[10] )

thus (cLoop n) . 0 = |[(cos (((2 * PI) * n) * j0)),(sin (((2 * PI) * n) * j0))]| by Def4

.= c[10] by SIN_COS:31, TOPREALB:def 8 ; :: thesis: (cLoop n) . 1 = c[10]

thus (cLoop n) . 1 = |[(cos (((2 * PI) * n) * j1)),(sin (((2 * PI) * n) * j1))]| by Def4

.= |[(cos 0),(sin (((2 * PI) * n) + 0))]| by COMPLEX2:9

.= c[10] by COMPLEX2:8, SIN_COS:31, TOPREALB:def 8 ; :: thesis: verum