BORSUK_7: The {B}orsuk-Ulam Theorem

proof end;

end;

registration

let f be one-to-one complex-valued Function;
let c be Complex;

cluster f - c -> one-to-one ;

coherence ;

end;

theorem :: BORSUK_7:13

canceled;

::$CT

theorem Th13: :: BORSUK_7:14

for n being Nat holds - (0* n) = 0* n

proof end;

theorem Th14: :: BORSUK_7:15

for n being Nat
for f being complex-valued Function st f <> 0* n holds
- f <> 0* n

proof end;

theorem Th15: :: BORSUK_7:16

for r1, r2, r3 being Real holds sqr <*r1,r2,r3*> = <*(r1 ^2),(r2 ^2),(r3 ^2)*>

proof end;

theorem Th16: :: BORSUK_7:17

for r1, r2, r3 being Real holds Sum (sqr <*r1,r2,r3*>) = ((r1 ^2) + (r2 ^2)) + (r3 ^2)

proof end;

theorem Th17: :: BORSUK_7:18

for c being Complex
for f being complex-valued FinSequence holds (c (#) f) ^2 = (c ^2) (#) (f ^2)

proof end;

theorem Th18: :: BORSUK_7:19

for c being Complex
for f being complex-valued FinSequence holds (f (/) c) ^2 = (f ^2) (/) (c ^2)

proof end;

theorem Th19: :: BORSUK_7:20

for f being real-valued FinSequence st Sum f <> 0 holds
Sum (f (/) (Sum f)) = 1

proof end;

Lm6: 1,2,3 are_mutually_distinct
;

canceled;

theorem :: BORSUK_7:21

canceled;

theorem :: BORSUK_7:22

canceled;

theorem :: BORSUK_7:23

canceled;

theorem :: BORSUK_7:24

canceled;

theorem :: BORSUK_7:25

canceled;

theorem :: BORSUK_7:26

canceled;

theorem :: BORSUK_7:27

canceled;

theorem :: BORSUK_7:28

canceled;

theorem :: BORSUK_7:29

canceled;

::$CD
::$CT 9

theorem Th20: :: BORSUK_7:30

for a, b, c being object holds <*a,b,c*> = (1,2,3) --> (a,b,c)

proof end;

theorem Th21: :: BORSUK_7:31

for a, b, c, x, y, z being object st a,b,c are_mutually_distinct holds
product ((a,b,c) --> ({x},{y},{z})) = {((a,b,c) --> (x,y,z))}

proof end;

theorem Th22: :: BORSUK_7:32

for a, b, c being object
for A, B, C, D, E, F being set st A c= B & C c= D & E c= F holds
product ((a,b,c) --> (A,C,E)) c= product ((a,b,c) --> (B,D,F))

proof end;

theorem Th23: :: BORSUK_7:33

for a, b, c, x, y, z being object
for X, Y, Z being set st a,b,c are_mutually_distinct & x in X & y in Y & z in Z holds
(a,b,c) --> (x,y,z) in product ((a,b,c) --> (X,Y,Z))

proof end;

definition

let f be Function;

attr f is odd means :: BORSUK_7:def 1
for x, y being complex-valued Function st x in dom f & - x in dom f & y = f . x holds
f . (- x) = - y;

end;

:: deftheorem defines odd BORSUK_7:def 1 :

registration

cluster {} -> odd ;

coherence ;

end;

registration

cluster Relation-like Function-like Function-yielding V168() complex-functions-valued odd for set ;

proof end;

end;

set TC2 = Tunit_circle 2;

set TC3 = Tunit_circle 3;

Lm7: the carrier of (Tunit_circle 3) = Sphere (|[0,0,0]|,1)
by EUCLID_5:4, TOPREALB:9;

theorem :: BORSUK_7:34

for p being Point of (TOP-REAL 3) holds sqr p = <*((p `1) ^2),((p `2) ^2),((p `3) ^2)*>

proof end;

theorem Th25: :: BORSUK_7:35

for p being Point of (TOP-REAL 3) holds Sum (sqr p) = (((p `1) ^2) + ((p `2) ^2)) + ((p `3) ^2)

proof end;

reconsider QQ = RAT as Subset of REAL by NUMBERS:12;

set RR = R^1 | (R^1 QQ);

Lm8: the carrier of (R^1 | (R^1 QQ)) = QQ
by PRE_TOPC:8;

theorem Th26: :: BORSUK_7:36

for r being Real
for S being Subset of R^1 st S = RAT holds
RAT /\ ].-infty,r.[ is open Subset of (R^1 | S)

proof end;

theorem Th27: :: BORSUK_7:37

for r being Real
for S being Subset of R^1 st S = RAT holds
RAT /\ ].r,+infty.[ is open Subset of (R^1 | S)

proof end;

Lm9: now :: thesis:

let T be non empty connected TopSpace; :: thesis:
let f be Function of T,(R^1 | (R^1 QQ)); :: thesis:
let x, y be set ; :: thesis:
assume A1: ( x in dom f & y in dom f ) ; :: thesis:
assume f . x < f . y ; :: thesis:
then consider r being irrational Real such that
A2: ( f . x < r & r < f . y ) by BORSUK_5:27;
set GX = Image f;
A3: ( f . x in rng f & f . y in rng f ) by A1, FUNCT_1:def 3;
A4: [#] (Image f) = rng f by WAYBEL18:9;
thus ex Q1, Q2 being Subset of (Image f) st
( Q1 misses Q2 & Q1 <> {} (Image f) & Q2 <> {} (Image f) & Q1 is open & Q2 is open & [#] (Image f) = Q1 \/ Q2 ) :: thesis:

set Q1 = { q where q is Element of RAT : ( q in rng f & q < r ) } ;
set Q2 = { q where q is Element of RAT : ( q in rng f & q > r ) } ;
{ q where q is Element of RAT : ( q in rng f & q < r ) } c= rng f

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { q where q is Element of RAT : ( q in rng f & q < r ) } ; :: thesis:
then ex q being Element of RAT st
( x = q & q in rng f & q < r ) ;
hence x in rng f ; :: thesis:

end;

then reconsider Q1 = { q where q is Element of RAT : ( q in rng f & q < r ) } as Subset of (Image f) by WAYBEL18:9;
{ q where q is Element of RAT : ( q in rng f & q > r ) } c= rng f

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { q where q is Element of RAT : ( q in rng f & q > r ) } ; :: thesis:
then ex q being Element of RAT st
( x = q & q in rng f & q > r ) ;
hence x in rng f ; :: thesis:

end;

then reconsider Q2 = { q where q is Element of RAT : ( q in rng f & q > r ) } as Subset of (Image f) by WAYBEL18:9;
take Q1 ; :: thesis:
take Q2 ; :: thesis:
thus Q1 misses Q2 :: thesis:

assume not Q1 misses Q2 ; :: thesis:
then consider x being object such that
A5: ( x in Q1 & x in Q2 ) by XBOOLE_0:3;
( ex q being Element of RAT st
( x = q & q in rng f & q > r ) & ex q being Element of RAT st
( x = q & q in rng f & q < r ) ) by A5;
hence contradiction ; :: thesis:

end;

( f . x in Q1 & f . y in Q2 ) by A2, A3, Lm8;
hence ( Q1 <> {} (Image f) & Q2 <> {} (Image f) ) ; :: thesis:
reconsider G1 = RAT /\ ].-infty,r.[ as open Subset of (R^1 | (R^1 QQ)) by Th26;
reconsider G2 = RAT /\ ].r,+infty.[ as open Subset of (R^1 | (R^1 QQ)) by Th27;
Q1 = G1 /\ the carrier of (Image f)

thus Q1 c= G1 /\ the carrier of (Image f) :: according to XBOOLE_0:def 10 :: thesis:

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in Q1 ; :: thesis:
then consider q being Element of RAT such that
A6: x = q and
A7: q in rng f and
A8: q < r ;
q in ].-infty,r.[ by A8, XXREAL_1:233;
then q in G1 by XBOOLE_0:def 4;
hence x in G1 /\ the carrier of (Image f) by A4, A6, A7, XBOOLE_0:def 4; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A9: x in G1 /\ the carrier of (Image f) ; :: thesis:
then A10: x in the carrier of (Image f) by XBOOLE_0:def 4;
A11: x in G1 by A9, XBOOLE_0:def 4;
then reconsider x = x as Element of RAT by XBOOLE_0:def 4;
x in ].-infty,r.[ by A11, XBOOLE_0:def 4;
then x < r by XXREAL_1:233;
hence x in Q1 by A4, A10; :: thesis:

end;

hence Q1 is open by TSP_1:def 1; :: thesis:
Q2 = G2 /\ the carrier of (Image f)

thus Q2 c= G2 /\ the carrier of (Image f) :: according to XBOOLE_0:def 10 :: thesis:

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in Q2 ; :: thesis:
then consider q being Element of RAT such that
A12: x = q and
A13: q in rng f and
A14: q > r ;
q in ].r,+infty.[ by A14, XXREAL_1:235;
then q in G2 by XBOOLE_0:def 4;
hence x in G2 /\ the carrier of (Image f) by A4, A12, A13, XBOOLE_0:def 4; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A15: x in G2 /\ the carrier of (Image f) ; :: thesis:
then A16: x in the carrier of (Image f) by XBOOLE_0:def 4;
A17: x in G2 by A15, XBOOLE_0:def 4;
then reconsider x = x as Element of RAT by XBOOLE_0:def 4;
x in ].r,+infty.[ by A17, XBOOLE_0:def 4;
then x > r by XXREAL_1:235;
hence x in Q2 by A4, A16; :: thesis:

end;

hence Q2 is open by TSP_1:def 1; :: thesis:
thus Q1 \/ Q2 = [#] (Image f) :: thesis:

thus Q1 \/ Q2 c= [#] (Image f) ; :: according to XBOOLE_0:def 10 :: thesis:
let x be Element of (Image f); :: according to LATTICE7:def 1 :: thesis:
assume A18: x in [#] (Image f) ; :: thesis:
( x < r or x > r ) by Lm8, A4, XXREAL_0:1;
then ( x in Q1 or x in Q2 ) by A18, Lm8, A4;
hence x in Q1 \/ Q2 by XBOOLE_0:def 3; :: thesis:

end;

registration

let X be non empty connected TopSpace;
let Y be non empty TopSpace;
let f be continuous Function of X,Y;

cluster Image f -> connected ;

proof end;

end;

theorem Th28: :: BORSUK_7:38

for S being Subset of R^1 st S = RAT holds
for T being connected TopSpace
for f being Function of T,(R^1 | S) st f is continuous holds
f is constant

proof end;

theorem Th29: :: BORSUK_7:39

for a, b being Real
for f being continuous Function of (Closed-Interval-TSpace (a,b)),R^1
for g being PartFunc of REAL,REAL st a <= b & f = g holds
g is continuous

proof end;

definition

let s be Point of R^1;
let r be Real;
:: original: +
redefine func s + r -> Point of R^1;
coherence by TOPMETR:17, XREAL_0:def 1;

end;

definition

let s be Point of R^1;
let r be Real;
:: original: -
redefine func s - r -> Point of R^1;
coherence by TOPMETR:17, XREAL_0:def 1;

end;

definition

let X be set ;
let f be Function of X,R^1;
let r be Real;
:: original: +
redefine func f + r -> Function of X,R^1;
coherence

proof end;

end;

definition

let X be set ;
let f be Function of X,R^1;
let r be Real;
:: original: -
redefine func f - r -> Function of X,R^1;
coherence

proof end;

end;

definition

let s, t be Point of R^1;
let f be Path of s,t;
let r be Real;
:: original: +
redefine func f + r -> Path of s + r,t + r;
coherence

proof end;

:: original: -
redefine func f - r -> Path of s - r,t - r;
coherence

proof end;

end;

definition

func c[100] -> Point of (Tunit_circle 3) equals :: BORSUK_7:def 2
|[1,0,0]|;

proof end;

end;

:: deftheorem defines c[100] BORSUK_7:def 2 :

reconsider c100 = c[100] as Point of (TOP-REAL 3) ;

reconsider c100a = c[100] as Point of (Tunit_circle (2 + 1)) ;

definition

func c[-100] -> Point of (Tunit_circle 3) equals :: BORSUK_7:def 3
|[(- 1),0,0]|;

proof end;

end;

:: deftheorem defines c[-100] BORSUK_7:def 3 :

reconsider mc100 = c[-100] as Point of (TOP-REAL 3) ;

theorem Th30: :: BORSUK_7:40

- c[100] = c[-100]

proof end;

theorem :: BORSUK_7:41

- c[-100] = c[100] by Th30;

theorem :: BORSUK_7:42

c[100] - c[-100] = |[2,0,0]|

proof end;

theorem :: BORSUK_7:43

for p being Point of (TOP-REAL 2) holds
( p `1 = |.p.| * (cos (Arg p)) & p `2 = |.p.| * (sin (Arg p)) )

proof end;

theorem :: BORSUK_7:44

for p being Point of (TOP-REAL 2) holds p = cpx2euc ((|.p.| * (cos (Arg p))) + ((|.p.| * (sin (Arg p))) * <i>))

proof end;

theorem Th35: :: BORSUK_7:45

for i being Integer
for p1, p2 being Point of (TOP-REAL 2) st |.p1.| = |.p2.| & Arg p1 = (Arg p2) + ((2 * PI) * i) holds
p1 = p2

proof end;

set CM = CircleMap ;

theorem Th36: :: BORSUK_7:46

for r being Real
for p being Point of (TOP-REAL 2) st p = CircleMap . r holds
Arg p = (2 * PI) * (frac r)

proof end;

theorem Th37: :: BORSUK_7:47

for p1, p2 being Point of (TOP-REAL 3)
for u1, u2 being Point of (Euclid 3) st u1 = p1 & u2 = p2 holds
(Pitag_dist 3) . (u1,u2) = sqrt (((((p1 `1) - (p2 `1)) ^2) + (((p1 `2) - (p2 `2)) ^2)) + (((p1 `3) - (p2 `3)) ^2))

proof end;

theorem Th38: :: BORSUK_7:48

for r being Real
for p being Point of (TOP-REAL 3)
for e being Point of (Euclid 3) st p = e & p `3 = 0 holds
product ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) c= Ball (e,r)

proof end;

theorem Th39: :: BORSUK_7:49

for i being Integer
for c being Complex
for s being Real holds Rotate (c,s) = Rotate (c,(s + ((2 * PI) * i)))

proof end;

theorem :: BORSUK_7:50

for i being Integer
for s being Real holds Rotate s = Rotate (s + ((2 * PI) * i))

proof end;

theorem Th41: :: BORSUK_7:51

for s being Real
for p being Point of (TOP-REAL 2) holds |.((Rotate s) . p).| = |.p.|

proof end;

theorem Th42: :: BORSUK_7:52

for s being Real
for p being Point of (TOP-REAL 2) holds Arg ((Rotate s) . p) = Arg (Rotate ((euc2cpx p),s))

proof end;

theorem Th43: :: BORSUK_7:53

for s being Real
for p being Point of (TOP-REAL 2) st p <> 0. (TOP-REAL 2) holds
ex i being Integer st Arg ((Rotate s) . p) = (s + (Arg p)) + ((2 * PI) * i)

proof end;

theorem Th44: :: BORSUK_7:54

for s being Real holds (Rotate s) . (0. (TOP-REAL 2)) = 0. (TOP-REAL 2)

proof end;

theorem Th45: :: BORSUK_7:55

for s being Real
for p being Point of (TOP-REAL 2) st (Rotate s) . p = 0. (TOP-REAL 2) holds
p = 0. (TOP-REAL 2)

proof end;

theorem Th46: :: BORSUK_7:56

for s being Real
for p being Point of (TOP-REAL 2) holds (Rotate s) . ((Rotate (- s)) . p) = p

proof end;

theorem :: BORSUK_7:57

for s being Real holds (Rotate s) * (Rotate (- s)) = id (TOP-REAL 2)

proof end;

theorem Th48: :: BORSUK_7:58

for r, s being Real
for p being Point of (TOP-REAL 2) holds
( p in Sphere ((0. (TOP-REAL 2)),r) iff (Rotate s) . p in Sphere ((0. (TOP-REAL 2)),r) )

proof end;

theorem Th49: :: BORSUK_7:59

for r being non negative Real
for s being Real holds (Rotate s) .: (Sphere ((0. (TOP-REAL 2)),r)) = Sphere ((0. (TOP-REAL 2)),r)

proof end;

definition

let r be non negative Real;
let s be Real;

func RotateCircle (r,s) -> Function of (Tcircle ((0. (TOP-REAL 2)),r)),(Tcircle ((0. (TOP-REAL 2)),r)) equals :: BORSUK_7:def 4
(Rotate s) | (Tcircle ((0. (TOP-REAL 2)),r));

proof end;

end;

:: deftheorem defines RotateCircle BORSUK_7:def 4 :

registration

let r be non negative Real;
let s be Real;

cluster RotateCircle (r,s) -> being_homeomorphism ;

proof end;

end;

theorem Th50: :: BORSUK_7:60

for r1, r2 being Real
for p being Point of (TOP-REAL 2) st p = CircleMap . r2 holds
(RotateCircle (1,(- (Arg p)))) . (CircleMap . r1) = CircleMap . (r1 - r2)

proof end;

definition

let n be non zero Nat;
let p be Point of (TOP-REAL n);
let r be non negative Real;

func CircleIso (p,r) -> Function of (Tunit_circle n),(Tcircle (p,r)) means :Def5: :: BORSUK_7:def 5
for a being Point of (Tunit_circle n)
for b being Point of (TOP-REAL n) st a = b holds
it . a = (r * b) + p;

proof end;

proof end;

end;

:: deftheorem Def5 defines CircleIso BORSUK_7:def 5 :

registration

let n be non zero Nat;
let p be Point of (TOP-REAL n);
let r be positive Real;

cluster CircleIso (p,r) -> being_homeomorphism ;

proof end;

end;

definition

func SphereMap -> Function of R^1,(Tunit_circle 3) means :Def6: :: BORSUK_7:def 6
for x being Real holds it . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]|;

proof end;

proof end;

end;

:: deftheorem Def6 defines SphereMap BORSUK_7:def 6 :

set SM = SphereMap ;

theorem :: BORSUK_7:61

for i being Integer holds SphereMap . i = c[100]

proof end;

Lm10: sin is Function of R^1,R^1

proof end;

Lm11: cos is Function of R^1,R^1

proof end;

Lm12: for r being Real holds SphereMap . r = |[((cos * (AffineMap ((2 * PI),Q))) . r),((sin * (AffineMap ((2 * PI),0))) . r),0]|

proof end;

registration

cluster SphereMap -> continuous ;

proof end;

end;

definition

let r be Real;

func eLoop r -> Function of I[01],(Tunit_circle 3) means :Def7: :: BORSUK_7:def 7
for x being Point of I[01] holds it . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]|;

proof end;

proof end;

end;

:: deftheorem Def7 defines eLoop BORSUK_7:def 7 :

theorem Th52: :: BORSUK_7:62

for r being Real holds eLoop r = SphereMap * (ExtendInt r)

proof end;

definition

let i be Integer;
:: original: eLoop
redefine func eLoop i -> Loop of c[100] ;
coherence

proof end;

end;

registration

let i be Integer;

cluster eLoop i -> nullhomotopic for Loop of c[100] ;

proof end;

end;

theorem Th53: :: BORSUK_7:63

for n being Nat
for p being Point of (TOP-REAL n) st p <> 0. (TOP-REAL n) holds
|.(p (/) |.p.|).| = 1

proof end;

definition

let n be Nat;
let p be Point of (TOP-REAL n);
assume A1: p <> 0. (TOP-REAL n) ;

func Rn->S1 p -> Point of (Tcircle ((0. (TOP-REAL n)),1)) equals :Def8: :: BORSUK_7:def 8
p (/) |.p.|;

proof end;

end;

:: deftheorem Def8 defines Rn->S1 BORSUK_7:def 8 :

definition

let n be non zero Nat;
let f be Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n);
set TC4 = Tcircle ((0. (TOP-REAL (n + 1))),1);
set TC3 = Tunit_circle (n + 1);
set TC2 = Tunit_circle n;

func Sn1->Sn f -> Function of (Tunit_circle (n + 1)),(Tunit_circle n) means :Def9: :: BORSUK_7:def 9
for x, y being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st y = - x holds
it . x = Rn->S1 ((f . x) - (f . y));

proof end;

proof end;

end;

:: deftheorem Def9 defines Sn1->Sn BORSUK_7:def 9 :

definition

let x0, y0 be Point of (Tunit_circle 2);
let xt be set ;
let f be Path of x0,y0;
assume A1: xt in CircleMap " {x0} ;

func liftPath (f,xt) -> Function of I[01],R^1 means :Def10: :: BORSUK_7:def 10
( it . 0 = xt & f = CircleMap * it & it is continuous & ( for f1 being Function of I[01],R^1 st f1 is continuous & f = CircleMap * f1 & f1 . 0 = xt holds
it = f1 ) );

existence by A1, TOPALG_5:23;
uniqueness ;

end;

:: deftheorem Def10 defines liftPath BORSUK_7:def 10 :

definition

let n be Nat;
let p, x, y be Point of (TOP-REAL n);
let r be Real;

pred x,y are_antipodals_of p,r means :: BORSUK_7:def 11
( x is Point of (Tcircle (p,r)) & y is Point of (Tcircle (p,r)) & p in LSeg (x,y) );

end;

:: deftheorem defines are_antipodals_of BORSUK_7:def 11 :

definition

let n be Nat;
let p, x, y be Point of (TOP-REAL n);
let r be Real;
let f be Function;

pred x,y are_antipodals_of p,r,f means :: BORSUK_7:def 12
( x,y are_antipodals_of p,r & x in dom f & y in dom f & f . x = f . y );

end;

:: deftheorem defines are_antipodals_of BORSUK_7:def 12 :

definition

let m, n be Nat;
let p be Point of (TOP-REAL m);
let r be Real;
let f be Function of (Tcircle (p,r)),(TOP-REAL n);

attr f is with_antipodals means :: BORSUK_7:def 13
ex x, y being Point of (TOP-REAL m) st x,y are_antipodals_of p,r,f;

end;

:: deftheorem defines with_antipodals BORSUK_7:def 13 :

notation

let m, n be Nat;
let p be Point of (TOP-REAL m);
let r be Real;
let f be Function of (Tcircle (p,r)),(TOP-REAL n);
antonym without_antipodals f for with_antipodals ;

end;

theorem Th54: :: BORSUK_7:64

for n being non zero Nat
for r being non negative Real
for x being Point of (TOP-REAL n) st x is Point of (Tcircle ((0. (TOP-REAL n)),r)) holds
x, - x are_antipodals_of 0. (TOP-REAL n),r

proof end;

theorem Th55: :: BORSUK_7:65

for n being non zero Nat
for p, x, y, x1, y1 being Point of (TOP-REAL n)
for r being positive Real st x,y are_antipodals_of 0. (TOP-REAL n),1 & x1 = (CircleIso (p,r)) . x & y1 = (CircleIso (p,r)) . y holds
x1,y1 are_antipodals_of p,r

proof end;

theorem Th56: :: BORSUK_7:66

for n being non zero Nat
for f being Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n)
for x being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st f is without_antipodals holds
(f . x) - (f . (- x)) <> 0. (TOP-REAL n)

proof end;

theorem Th57: :: BORSUK_7:67

for n being non zero Nat
for f being Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n) st f is without_antipodals holds
Sn1->Sn f is odd

proof end;

theorem Th58: :: BORSUK_7:68

for n being non zero Nat
for f, g, B1 being Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n) st g = f (-) & B1 = f <--> g & f is without_antipodals holds
Sn1->Sn f = B1 </> ((n NormF) * B1)

proof end;

Lm13: for n being non zero Nat
for f being Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n) st f is without_antipodals & f is continuous holds
Sn1->Sn f is continuous

proof end;

deffunc H₁( Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2)) -> Element of bool [: the carrier of I[01], the carrier of (Tunit_circle 2):] = (Sn1->Sn $1) * (eLoop 1);

Lm14: for s being Real
for f being Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2) st f is without_antipodals & 0 <= s & s <= 1 / 2 holds
H₁(f) . (s + (1 / 2)) = - (H₁(f) . s)

proof end;

defpred S₁[ Point of R^1, Point of R^1, Integer] means $1 = $2 + ($3 / 2);

Lm15: now :: thesis:

let a, b be Point of R^1; :: thesis:
assume A1: CircleMap . a = - (CircleMap . b) ; :: thesis:
thus ex I being odd Integer st S₁[a,b,I] :: thesis:

A2: ( CircleMap . a = |[(cos ((2 * PI) * a)),(sin ((2 * PI) * a))]| & CircleMap . b = |[(cos ((2 * PI) * b)),(sin ((2 * PI) * b))]| ) by TOPREALB:def 11;
A3: - |[(cos ((2 * PI) * b)),(sin ((2 * PI) * b))]| = |[(- (cos ((2 * PI) * b))),(- (sin ((2 * PI) * b)))]| by EUCLID:60;
then A4: cos ((2 * PI) * a) = - (cos ((2 * PI) * b)) by A1, A2, FINSEQ_1:77
.= cos (PI + ((2 * PI) * b)) by SIN_COS:79 ;
sin ((2 * PI) * a) = - (sin ((2 * PI) * b)) by A1, A2, A3, FINSEQ_1:77
.= sin (PI + ((2 * PI) * b)) by SIN_COS:79 ;
then consider i being Integer such that
A5: (2 * PI) * a = (PI + ((2 * PI) * b)) + ((2 * PI) * i) by A4, Th11;
A6: 2 * a = (PI * (2 * a)) / PI by XCMPLX_1:89
.= (PI * ((1 + (2 * b)) + (2 * i))) / PI by A5
.= (1 + (2 * b)) + (2 * i) by XCMPLX_1:89 ;
take I = (2 * i) + 1; :: thesis:
thus S₁[a,b,I] by A6; :: thesis:

end;

Lm16: for f being Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2) st f is without_antipodals & f is continuous holds
H₁(f) is nullhomotopic Loop of (Sn1->Sn f) . c100a

proof end;

Lm17: now :: thesis:

let f be Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2); :: thesis:
let s be Real; :: thesis:
let xt be set ; :: thesis:
assume that
A1: ( f is without_antipodals & f is continuous ) and
A2: xt in CircleMap " {((Sn1->Sn f) . c[100])} and
A3: ( 0 <= s & s <= 1 / 2 ) ; :: thesis:
thus ex IT being odd Integer st
for L being Loop of (Sn1->Sn f) . c100a st L = H₁(f) holds
(liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (IT / 2) :: thesis:

reconsider s = s as Point of I[01] by A3, Lm3;
reconsider L = H₁(f) as Loop of (Sn1->Sn f) . c100a by A1, Lm16;
set l = liftPath (L,xt);
set t = R^1 (s + (1 / 2));
reconsider t1 = R^1 (s + (1 / 2)) as Point of I[01] by A3, Lm4;
A4: H₁(f) = CircleMap * (liftPath (L,xt)) by A2, Def10;
( (CircleMap * (liftPath (L,xt))) . t1 = CircleMap . ((liftPath (L,xt)) . t1) & (CircleMap * (liftPath (L,xt))) . s = CircleMap . ((liftPath (L,xt)) . s) ) by FUNCT_2:15;
then CircleMap . ((liftPath (L,xt)) . (R^1 (s + (1 / 2)))) = - (CircleMap . ((liftPath (L,xt)) . s)) by A4, A3, A1, Lm14;
then consider I being odd Integer such that
A5: S₁[(liftPath (L,xt)) . t1,(liftPath (L,xt)) . s,I] by Lm15;
take I ; :: thesis:
thus for L being Loop of (Sn1->Sn f) . c100a st L = H₁(f) holds
(liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (I / 2) by A5; :: thesis:

end;

defpred S₂[ Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2), set , Integer] means for L being Loop of (Sn1->Sn $1) . c100a st L = H₁($1) holds
for s being Real st 0 <= s & s <= 1 / 2 holds
(liftPath (L,$2)) . (s + (1 / 2)) = ((liftPath (L,$2)) . s) + ($3 / 2);

Lm18: now :: thesis:

let f be Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2); :: thesis:
let xt be set ; :: thesis:
assume that
A1: ( f is without_antipodals & f is continuous ) and
A2: xt in CircleMap " {((Sn1->Sn f) . c[100])} ; :: thesis:
reconsider L1 = H₁(f) as Loop of (Sn1->Sn f) . c100a by A1, Lm16;
thus ex I being odd Integer st S₂[f,xt,I] :: thesis:

set l1 = liftPath (L1,xt);
set S = [.0,(1 / 2).];
set AF = AffineMap (1,(1 / 2));
set W = 2 (#) (((liftPath (L1,xt)) * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) - (liftPath (L1,xt)));
dom (AffineMap (1,(1 / 2))) = REAL by FUNCT_2:def 1;
then A3: dom ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]) = [.0,(1 / 2).] by RELAT_1:62;
A4: dom (liftPath (L1,xt)) = the carrier of I[01] by FUNCT_2:def 1;
A5: rng ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]) c= the carrier of I[01]

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]) ; :: thesis:
then consider x being object such that
A6: x in dom ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]) and
A7: ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]) . x = y by FUNCT_1:def 3;
reconsider x = x as Real by A6;
A8: ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]) . x = (AffineMap (1,(1 / 2))) . x by A6, FUNCT_1:47
.= (1 * x) + (1 / 2) by FCONT_1:def 4 ;
( 0 <= x & x <= 1 / 2 ) by A6, A3, XXREAL_1:1;
then ( Q + (1 / 2) <= x + (1 / 2) & x + (1 / 2) <= (1 / 2) + (1 / 2) ) by XREAL_1:6;
hence y in the carrier of I[01] by A7, A8, BORSUK_1:43; :: thesis:

end;

A9: dom (((liftPath (L1,xt)) * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) - (liftPath (L1,xt))) = (dom ((liftPath (L1,xt)) * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]))) /\ (dom (liftPath (L1,xt))) by VALUED_1:12
.= (dom ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) /\ (dom (liftPath (L1,xt))) by A4, A5, RELAT_1:27
.= [.0,(1 / 2).] by A3, A4, BORSUK_1:40, XBOOLE_1:28, XXREAL_1:34 ;
A10: dom (2 (#) (((liftPath (L1,xt)) * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) - (liftPath (L1,xt)))) = dom (((liftPath (L1,xt)) * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) - (liftPath (L1,xt))) by VALUED_1:def 5;
rng (2 (#) (((liftPath (L1,xt)) * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) - (liftPath (L1,xt)))) c= REAL by VALUED_0:def 3;
then reconsider W = 2 (#) (((liftPath (L1,xt)) * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) - (liftPath (L1,xt))) as PartFunc of REAL,REAL by A9, A10, RELSET_1:4;
consider ITj0 being odd Integer such that
A11: for L being Loop of (Sn1->Sn f) . c100a st L = H₁(f) holds
(liftPath (L,xt)) . (j0 + (1 / 2)) = ((liftPath (L,xt)) . j0) + (ITj0 / 2) by A1, A2, Lm17;
take ITj0 ; :: thesis:
let L be Loop of (Sn1->Sn f) . c100a; :: thesis:
assume A12: L = H₁(f) ; :: thesis:
let s be Real; :: thesis:
assume A13: ( 0 <= s & s <= 1 / 2 ) ; :: thesis:
set l = liftPath (L,xt);
A14: s in [.0,(1 / 2).] by A13, XXREAL_1:1;
A15: 0 in [.0,(1 / 2).] by XXREAL_1:1;
then A16: ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]) . 0 = (AffineMap (1,(1 / 2))) . 0 by FUNCT_1:49
.= (1 * Q) + (1 / 2) by FCONT_1:def 4 ;
A17: ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]) . s = (AffineMap (1,(1 / 2))) . s by A14, FUNCT_1:49
.= (1 * s) + (1 / 2) by FCONT_1:def 4 ;
consider ITs being odd Integer such that
A18: for L being Loop of (Sn1->Sn f) . c100a st L = H₁(f) holds
(liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (ITs / 2) by A1, A2, A13, Lm17;
A19: (liftPath (L1,xt)) . (j0 + (1 / 2)) = ((liftPath (L1,xt)) . j0) + (ITj0 / 2) by A11;
A20: (liftPath (L1,xt)) . (s + (1 / 2)) = ((liftPath (L1,xt)) . s) + (ITs / 2) by A18;
A21: W . 0 = 2 * ((((liftPath (L1,xt)) * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) - (liftPath (L1,xt))) . 0) by VALUED_1:6
.= 2 * ((((liftPath (L1,xt)) * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) . 0) - ((liftPath (L1,xt)) . 0)) by A9, A15, VALUED_1:13
.= 2 * (((liftPath (L1,xt)) . (1 / 2)) - ((liftPath (L1,xt)) . 0)) by A16, A3, A15, FUNCT_1:13
.= 2 * (ITj0 / 2) by A19 ;
A22: W . s = 2 * ((((liftPath (L1,xt)) * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) - (liftPath (L1,xt))) . s) by VALUED_1:6
.= 2 * ((((liftPath (L1,xt)) * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) . s) - ((liftPath (L1,xt)) . s)) by A9, A14, VALUED_1:13
.= 2 * (((liftPath (L1,xt)) . (s + (1 / 2))) - ((liftPath (L1,xt)) . s)) by A17, A3, A14, FUNCT_1:13
.= 2 * (ITs / 2) by A20 ;
A23: rng W c= INT