set f = eLoop i;
thus c[100] , c[100] are_connected ; :: according to BORSUK_2:def 2 :: thesis: ( eLoop i is continuous & (eLoop i) . 0 = c[100] & (eLoop i) . 1 = c[100] )
eLoop i = SphereMap * (ExtendInt i) by Th52;
hence eLoop i is continuous ; :: thesis: ( (eLoop i) . 0 = c[100] & (eLoop i) . 1 = c[100] )
thus (eLoop i) . 0 = |[(cos (((2 * PI) * i) * j0)),(sin (((2 * PI) * i) * j0)),0]| by Def7
.= c[100] by SIN_COS:31 ; :: thesis: (eLoop i) . 1 = c[100]
thus (eLoop i) . 1 = |[(cos (((2 * PI) * i) * j1)),(sin (((2 * PI) * i) * j1)),0]| by Def7
.= |[(cos 0),(sin (((2 * PI) * i) + Q)),0]| by COMPLEX2:9
.= c[100] by COMPLEX2:8, SIN_COS:31 ; :: thesis: verum