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