let f be Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2); :: thesis: ( f is without_antipodals & f is continuous implies not H₁(f) is nullhomotopic Loop of (Sn1->Sn f) . c100a )
assume A1: ( f is without_antipodals & f is continuous ) ; :: thesis: H₁(f) is not nullhomotopic Loop of (Sn1->Sn f) . c100a
then reconsider L = H₁(f) as Loop of (Sn1->Sn f) . c100a by Lm16;
set g = Sn1->Sn f;
set s = (Sn1->Sn f) . c100a;
not L is nullhomotopic

proof

let c be constant Loop of (Sn1->Sn f) . c100a; :: according to TOPALG_6:def 3 :: thesis: not L,c are_homotopic
rng CircleMap = the carrier of (Tunit_circle 2) by FUNCT_2:def 3;
then consider xt being object such that
A2: xt in the carrier of R^1 and
A3: CircleMap . xt = (Sn1->Sn f) . c100a by FUNCT_2:11;
reconsider xt = xt as Point of R^1 by A2;
(Sn1->Sn f) . c100a in {((Sn1->Sn f) . c100a)} by TARSKI:def 1;
then A4: xt in CircleMap " {((Sn1->Sn f) . c100a)} by A3, FUNCT_2:38;
then consider q being odd Integer such that
A5: S₂[f,xt,q] by A1, Lm18;
reconsider l = liftPath (L,xt) as continuous Function of I[01],R^1 by A4, Def10;
A6: l . 1 = (l . 0) + q by A5, Lm19;
A7: CircleMap . q = c[10] by TOPREALB:32;
A8: CircleMap . 0 = c[10] by TOPREALB:32;
set hh = l - xt;
l - xt is Path of R^1 0, R^1 q

proof

thus l - xt is continuous ; :: according to BORSUK_2:def 4 :: thesis: ( (l - xt) . 0 = R^1 0 & (l - xt) . 1 = R^1 q )
thus (l - xt) . 0 = (l . j0) - xt by VALUED_1:4
.= xt - xt by A4, Def10
.= R^1 0 ; :: thesis: (l - xt) . 1 = R^1 q
thus (l - xt) . 1 = (l . j1) - xt by VALUED_1:4
.= (xt + q) - xt by A6, A4, Def10
.= R^1 q ; :: thesis: verum

end;

then reconsider hh = l - xt as Path of R^1 0, R^1 q ;
reconsider Ch = CircleMap * hh as Loop of c[10] by A7, TOPREALB:32;
reconsider X = I[01] --> xt as Loop of xt by JORDAN:41;
set xx = X - xt;
reconsider Cx = CircleMap * (X - xt) as Loop of c[10] by A8;
A9: dom Ciso = the carrier of INT.Group by FUNCT_2:def 1;
A10: Ciso . q = Class ((EqRel ((Tunit_circle 2),c[10])),(CircleMap * hh)) by TOPALG_5:25;
A11: Ciso . 0 = Class ((EqRel ((Tunit_circle 2),c[10])),(CircleMap * (X - xt))) by TOPALG_5:25;
Ciso . (@' 0) <> Ciso . (@' q) by A9, FUNCT_1:def 4;
then A12: not Cx,Ch are_homotopic by A10, A11, TOPALG_1:46;
assume L,c are_homotopic ; :: thesis: contradiction
then consider F being Function of [:I[01],I[01]:],(Tunit_circle 2) such that
A13: F is continuous and
A14: for t being Point of I[01] holds
( F . (t,0) = H₁(f) . t & F . (t,1) = c . t & F . (0,t) = (Sn1->Sn f) . c100a & F . (1,t) = (Sn1->Sn f) . c100a ) ;
reconsider S = (Sn1->Sn f) . c100a as Point of (TOP-REAL 2) by PRE_TOPC:25;
set A = - (Arg S);
set H = RotateCircle (1,(- (Arg S)));
set G = (RotateCircle (1,(- (Arg S)))) * F;
A15: |.(euc2cpx S).| = |.S.| by EUCLID_3:25
.= 1 by TOPREALB:12 ;
A16: Rotate ((euc2cpx S),(- (Arg S))) = |.(euc2cpx S).| by COMPLEX2:55;
A17: (RotateCircle (1,(- (Arg S)))) . ((Sn1->Sn f) . c100a) = (Rotate (- (Arg S))) . S by FUNCT_1:49
.= c[10] by A16, A15, COMPLEX1:6, JORDAN24:def 3 ;

now :: thesis: for t being Point of I[01] holds
( ((RotateCircle (1,(- (Arg S)))) * F) . (t,0) = Ch . t & ((RotateCircle (1,(- (Arg S)))) * F) . (t,1) = Cx . t & ((RotateCircle (1,(- (Arg S)))) * F) . (0,t) = c[10] & ((RotateCircle (1,(- (Arg S)))) * F) . (1,t) = c[10] )

let t be Point of I[01]; :: thesis: ( ((RotateCircle (1,(- (Arg S)))) * F) . (t,0) = Ch . t & ((RotateCircle (1,(- (Arg S)))) * F) . (t,1) = Cx . t & ((RotateCircle (1,(- (Arg S)))) * F) . (0,t) = c[10] & ((RotateCircle (1,(- (Arg S)))) * F) . (1,t) = c[10] )
reconsider E = eLoop 1 as Function of I[01],(Tunit_circle (2 + 1)) ;
reconsider BU = H₁(f) as Function of I[01],(Tunit_circle 2) ;
reconsider T = BU . t as Point of (TOP-REAL 2) by PRE_TOPC:25;
H₁(f) = CircleMap * l by A4, Def10;
then A18: H₁(f) . t = CircleMap . (l . t) by FUNCT_2:15;
thus ((RotateCircle (1,(- (Arg S)))) * F) . (t,0) = (RotateCircle (1,(- (Arg S)))) . (F . (t,j0)) by Lm1, BINOP_1:18
.= (RotateCircle (1,(- (Arg S)))) . T by A14
.= CircleMap . ((l . t) - xt) by A3, A18, Th50
.= CircleMap . (hh . t) by VALUED_1:4
.= Ch . t by FUNCT_2:15 ; :: thesis: ( ((RotateCircle (1,(- (Arg S)))) * F) . (t,1) = Cx . t & ((RotateCircle (1,(- (Arg S)))) * F) . (0,t) = c[10] & ((RotateCircle (1,(- (Arg S)))) * F) . (1,t) = c[10] )
thus ((RotateCircle (1,(- (Arg S)))) * F) . (t,1) = (RotateCircle (1,(- (Arg S)))) . (F . (t,j1)) by Lm1, BINOP_1:18
.= (RotateCircle (1,(- (Arg S)))) . (c . t) by A14
.= (RotateCircle (1,(- (Arg S)))) . ((Sn1->Sn f) . c100a) by TOPALG_3:21
.= CircleMap . (xt - xt) by A17, TOPREALB:32
.= CircleMap . ((X . t) - xt)
.= CircleMap . ((X - xt) . t) by VALUED_1:4
.= Cx . t by FUNCT_2:15 ; :: thesis: ( ((RotateCircle (1,(- (Arg S)))) * F) . (0,t) = c[10] & ((RotateCircle (1,(- (Arg S)))) * F) . (1,t) = c[10] )
thus ((RotateCircle (1,(- (Arg S)))) * F) . (0,t) = (RotateCircle (1,(- (Arg S)))) . (F . (j0,t)) by Lm1, BINOP_1:18
.= c[10] by A14, A17 ; :: thesis: ((RotateCircle (1,(- (Arg S)))) * F) . (1,t) = c[10]
thus ((RotateCircle (1,(- (Arg S)))) * F) . (1,t) = (RotateCircle (1,(- (Arg S)))) . (F . (j1,t)) by Lm1, BINOP_1:18
.= c[10] by A14, A17 ; :: thesis: verum

end;

hence contradiction by A12, A13, BORSUK_2:def 7; :: thesis: verum

end;

hence H₁(f) is not nullhomotopic Loop of (Sn1->Sn f) . c100a ; :: thesis: verum