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:34, 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:10
.= c[10] by COMPLEX2:9, SIN_COS:34, TOPREALB:def 8 ; :: thesis: verum