borsuk_7.miz

begin

 reserve a,b,c,x,y,z for object,

X,Y,Z for set,

n for Nat,

i,j for Integer,

r,r1,r2,r3,s for Real,

c1,c2 for Complex,

p for Point of ( TOP-REAL n);

 reconsider Q = 0 as Nat;

 set T2 = ( TOP-REAL 2);

 set o2 = |[ 0 , 0 ]|;

 set o = |[ 0 , 0 , 0 ]|;

 set I = the carrier of I[01] ;

 set II = the carrier of [: I[01] , I[01] :];

 set R = the carrier of R^1 ;

 set X01 = [. 0 , 1.[;

 set K = ( R^1 X01);

 set R01 = ( R^1 | ( R^1 ]. 0 , 1.[));

 reconsider j0 = 0 , j1 = 1 as Point of I[01] by BORSUK_1:def 14, BORSUK_1:def 15;



 Lm1: II = [:I, I:] by BORSUK_1:def 2;



 Lm2: 0 in { 0 } by TARSKI:def 1;

 Lm3:

 now

 let s;

 assume s <= (1 / 2);

 then s <= 1 by XXREAL_0: 2;

 hence 0 <= s implies s in I by BORSUK_1: 43;

 end;

 Lm4:

 now

 let s;

 set t = (s + (1 / 2));

 assume 0 <= s & s <= (1 / 2);

 then (Q + (1 / 2)) <= t & t <= ((1 / 2) + (1 / 2)) by XREAL_1: 6;

 hence t in I by BORSUK_1: 43;

 end;

 registration

 cluster -> irrational for Element of IRRAT ;

 coherence by BORSUK_5: 17;

 end

 theorem :: BORSUK_7:1



 Th1: 0 <= r & 0 <= s & (r ^2 ) = (s ^2 ) implies r = s

 proof

 assume that

 A1: 0 <= r and

 A2: 0 <= s and

 A3: (r ^2 ) = (s ^2 ) and

 A4: r <> s;

 ( - Q) >= ( - ( - s)) by A1, A3, A4, SQUARE_1: 40;

 hence contradiction by A4, A2, A3, SQUARE_1: 40;

 end;

 theorem :: BORSUK_7:2



 Th2: ( frac r) >= ( frac s) implies ( frac (r - s)) = (( frac r) - ( frac s))

 proof

 assume

 A1: ( frac r) >= ( frac s);

 set a = (((r - s) - ( frac r)) + ( frac s));



 A2: a = ((r - ( frac r)) - (s - ( frac s)));



 A3: a = ((r - s) + (( - ( frac r)) + ( frac s)));

 ( - ( frac r)) <= ( - ( frac s)) by A1, XREAL_1: 24;

 then (( - ( frac r)) + ( frac s)) <= (( - ( frac s)) + ( frac s)) by XREAL_1: 6;

 then

 A4: a <= ((r - s) + Q) by A3, XREAL_1: 6;



 A5: a = ((r - s) - (( frac r) - ( frac s)));



 A6: 0 <= ( frac s) by INT_1: 43;

 ( frac r) < 1 by INT_1: 43;

 then (1 + ( frac s)) > (( frac r) + Q) by A6, XREAL_1: 8;

 then 1 > (( frac r) - ( frac s)) by XREAL_1: 19;

 then ((r - s) - 1) < a by A5, XREAL_1: 10;

 then a = [\(r - s)/] by A4, A2, INT_1:def 6;

 hence thesis;

 end;

 theorem :: BORSUK_7:3



 Th3: ( frac r) < ( frac s) implies ( frac (r - s)) = ((( frac r) - ( frac s)) + 1)

 proof

 assume

 A1: ( frac r) < ( frac s);

 set a = ((((r - s) - ( frac r)) + ( frac s)) - 1);



 A2: a = (((r - ( frac r)) - (s - ( frac s))) - 1);



 A3: a = ((r - s) + ((( - ( frac r)) + ( frac s)) - 1));

 ( frac s) < 1 by INT_1: 43;

 then

 A4: (( frac s) - 1) < (1 - 1) by XREAL_1: 9;

 0 <= ( frac r) by INT_1: 43;

 then ((( frac s) - 1) - ( frac r)) <= (( frac r) - ( frac r)) by A4;

 then

 A5: ((((r - s) - ( frac r)) + ( frac s)) - 1) <= ((r - s) + Q) by A3, XREAL_1: 6;



 A6: a = (((r - s) - 1) - (( frac r) - ( frac s)));

 (( frac r) - ( frac r)) > (( frac r) - ( frac s)) by A1, XREAL_1: 10;

 then (((r - s) - 1) - Q) < a by A6, XREAL_1: 10;

 then a = [\(r - s)/] by A5, A2, INT_1:def 6;

 hence thesis;

 end;

 theorem :: BORSUK_7:4



 Th4: ex i st ( frac (r - s)) = ((( frac r) - ( frac s)) + i) & (i = 0 or i = 1)

 proof

 ( frac (r - s)) = ((( frac r) - ( frac s)) + Q) or ( frac (r - s)) = ((( frac r) - ( frac s)) + 1) by Th2, Th3;

 hence thesis;

 end;

 theorem :: BORSUK_7:5



 Th5: ( sin r) = 0 implies r = ((2 * PI ) * [\(r / (2 * PI ))/]) or r = ( PI + ((2 * PI ) * [\(r / (2 * PI ))/]))

 proof

 set i = [\(r / (2 * PI ))/];

 assume

 A1: ( sin r) = 0 ;

 consider w be Real such that

 A2: w = (((2 * PI ) * ( - i)) + r) and

 A3: 0 <= w and

 A4: w < (2 * PI ) by COMPLEX2: 1;

 ( sin w) = ( sin r) by A2, COMPLEX2: 8;

 then w = 0 or w = PI by A1, A3, A4, COMPTRIG: 17;

 hence thesis by A2;

 end;

 theorem :: BORSUK_7:6



 Th6: ( cos r) = 0 implies r = (( PI / 2) + ((2 * PI ) * [\(r / (2 * PI ))/])) or r = (((3 * PI ) / 2) + ((2 * PI ) * [\(r / (2 * PI ))/]))

 proof

 set i = [\(r / (2 * PI ))/];

 assume

 A1: ( cos r) = 0 ;

 consider w be Real such that

 A2: w = (((2 * PI ) * ( - i)) + r) and

 A3: 0 <= w and

 A4: w < (2 * PI ) by COMPLEX2: 1;

 ( cos w) = ( cos r) by A2, COMPLEX2: 9;

 then w = ( PI / 2) or w = ((3 * PI ) / 2) by A1, A3, A4, COMPTRIG: 18;

 hence thesis by A2;

 end;

 theorem :: BORSUK_7:7



 Th7: ( sin r) = 0 implies ex i st r = ( PI * i)

 proof

 assume ( sin r) = 0 ;

 then r = ((2 * PI ) * [\(r / (2 * PI ))/]) or r = ( PI + ((2 * PI ) * [\(r / (2 * PI ))/])) by Th5;

 then r = ( PI * (2 * [\(r / (2 * PI ))/])) or r = ( PI * (1 + (2 * [\(r / (2 * PI ))/])));

 hence thesis;

 end;

 theorem :: BORSUK_7:8



 Th8: ( cos r) = 0 implies ex i st r = (( PI / 2) + ( PI * i))

 proof

 assume ( cos r) = 0 ;

 then r = (( PI / 2) + ((2 * PI ) * [\(r / (2 * PI ))/])) or r = (((3 * PI ) / 2) + ((2 * PI ) * [\(r / (2 * PI ))/])) by Th6;

 then r = (( PI / 2) + ( PI * (2 * [\(r / (2 * PI ))/]))) or r = (( PI / 2) + ( PI * (1 + (2 * [\(r / (2 * PI ))/]))));

 hence thesis;

 end;

 Lm5:

 now

 let r, s;

 assume ( sin ((r - s) / 2)) = 0 ;

 then

 consider i such that

 A1: ((r - s) / 2) = ( PI * i) by Th7;

 r = (s + ((2 * PI ) * i)) by A1;

 hence ex i st r = (s + ((2 * PI ) * i));

 end;

 theorem :: BORSUK_7:9



 Th9: ( sin r) = ( sin s) implies ex i st r = (s + ((2 * PI ) * i)) or r = (( PI - s) + ((2 * PI ) * i))

 proof

 assume

 A1: ( sin r) = ( sin s);



 A2: (( sin r) - ( sin s)) = (2 * (( cos ((r + s) / 2)) * ( sin ((r - s) / 2)))) by SIN_COS4: 16;

 per cases by A1, A2;

 suppose ( sin ((r - s) / 2)) = 0 ;

 hence thesis by Lm5;

 end;

 suppose ( cos ((r + s) / 2)) = 0 ;

 then

 consider i such that

 A3: ((r + s) / 2) = (( PI / 2) + ( PI * i)) by Th8;

 r = (( PI - s) + ((2 * PI ) * i)) by A3;

 hence thesis;

 end;

 end;

 theorem :: BORSUK_7:10



 Th10: ( cos r) = ( cos s) implies ex i st r = (s + ((2 * PI ) * i)) or r = (( - s) + ((2 * PI ) * i))

 proof

 assume

 A1: ( cos r) = ( cos s);



 A2: (( cos r) - ( cos s)) = ( - (2 * (( sin ((r + s) / 2)) * ( sin ((r - s) / 2))))) by SIN_COS4: 18;

 per cases by A1, A2;

 suppose ( sin ((r - s) / 2)) = 0 ;

 hence thesis by Lm5;

 end;

 suppose ( sin ((r + s) / 2)) = 0 ;

 then

 consider i such that

 A3: ((r + s) / 2) = ( PI * i) by Th7;

 ((r + s) - s) = (((2 * PI ) * i) - s) by A3;

 hence thesis;

 end;

 end;

 theorem :: BORSUK_7:11



 Th11: ( sin r) = ( sin s) & ( cos r) = ( cos s) implies ex i st r = (s + ((2 * PI ) * i))

 proof

 assume that

 A1: ( sin r) = ( sin s) and

 A2: ( cos r) = ( cos s);

 consider i such that

 A3: r = (s + ((2 * PI ) * i)) or r = (( PI - s) + ((2 * PI ) * i)) by A1, Th9;

 consider j such that

 A4: r = (s + ((2 * PI ) * j)) or r = (( - s) + ((2 * PI ) * j)) by A2, Th10;

 per cases by A3, A4;

 suppose r = (s + ((2 * PI ) * i)) or r = (s + ((2 * PI ) * j));

 hence thesis;

 end;

 suppose r = (( PI - s) + ((2 * PI ) * i)) & r = (( - s) + ((2 * PI ) * j));

 then ( PI / PI ) = (( PI * (2 * (j - i))) / PI );

 then ( PI / PI ) = (2 * (j - i)) by XCMPLX_1: 89;

 then 1 = (2 * (j - i)) by XCMPLX_1: 60;

 then (j - i) = (1 / 2);

 hence thesis by NAT_D: 33;

 end;

 end;

 theorem :: BORSUK_7:12



 Th12: |.c1.| = |.c2.| & ( Arg c1) = (( Arg c2) + ((2 * PI ) * i)) implies c1 = c2

 proof

 assume

 A1: |.c1.| = |.c2.| & ( Arg c1) = (( Arg c2) + ((2 * PI ) * i));



 A2: ( cos ( Arg c2)) = ( cos (( Arg c2) + ((2 * PI ) * i))) & ( sin ( Arg c2)) = ( sin (( Arg c2) + ((2 * PI ) * i))) by COMPLEX2: 8, COMPLEX2: 9;

 c1 = (( |.c1.| * ( cos ( Arg c1))) + (( |.c1.| * ( sin ( Arg c1))) * )) & c2 = (( |.c2.| * ( cos ( Arg c2))) + (( |.c2.| * ( sin ( Arg c2))) * )) by COMPTRIG: 62;

 hence c1 = c2 by A1, A2;

 end;

 registration

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

 let c be Complex;

 cluster (f + c) -> one-to-one;

 coherence

 proof

 let x,y be object;

 assume that

 A1: x in ( dom (f + c)) & y in ( dom (f + c)) and

 A2: ((f + c) . x) = ((f + c) . y);



 A3: ( dom (f + c)) = ( dom f) by VALUED_1:def 2;

 ((f + c) . x) = ((f . x) + c) & ((f + c) . y) = ((f . y) + c) by A1, VALUED_1:def 2;

 hence thesis by A1, A3, A2, FUNCT_1:def 4;

 end;

 end

 registration

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

 let c be Complex;

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

 coherence ;

 end

 ::$Canceled

 theorem :: BORSUK_7:14



 Th13: ( - ( 0* n)) = ( 0* n)

 proof

 set f = ( 0* n), g = ( - f);

 thus ( len f) = ( len g) by COMPLSP2: 5;

 let k be Nat such that 1 <= k & k <= ( len g);



 A1: (f . k) = 0 ;



 thus (f . k) = ( - Q)

 .= (g . k) by A1, VALUED_1: 8;

 end;

 theorem :: BORSUK_7:15



 Th14: for f be complex-valued Function holds f <> ( 0* n) implies ( - f) <> ( 0* n)

 proof

 let f be complex-valued Function;

 assume

 A1: f <> ( 0* n);

 assume ( - f) = ( 0* n);

 then ( - ( - f)) = ( - ( 0* n));

 hence thesis by A1, Th13;

 end;

 theorem :: BORSUK_7:16



 Th15: ( sqr <*r1, r2, r3*>) = <*(r1 ^2 ), (r2 ^2 ), (r3 ^2 )*>

 proof

 <*r1, r2*> is FinSequence of REAL & <*r3*> is FinSequence of REAL by TOPREALC: 19;



 hence ( sqr <*r1, r2, r3*>) = (( sqr <*r1, r2*>) ^ ( sqr <*r3*>)) by TOPREAL7: 10

 .= ( <*(r1 ^2 ), (r2 ^2 )*> ^ ( sqr <*r3*>)) by TOPREAL6: 11

 .= <*(r1 ^2 ), (r2 ^2 ), (r3 ^2 )*> by RVSUM_1: 55;

 end;

 theorem :: BORSUK_7:17



 Th16: ( Sum ( sqr <*r1, r2, r3*>)) = (((r1 ^2 ) + (r2 ^2 )) + (r3 ^2 ))

 proof



 thus ( Sum ( sqr <*r1, r2, r3*>)) = ( Sum <*(r1 ^2 ), (r2 ^2 ), (r3 ^2 )*>) by Th15

 .= (((r1 ^2 ) + (r2 ^2 )) + (r3 ^2 )) by RVSUM_1: 78;

 end;

 theorem :: BORSUK_7:18



 Th17: for c be Complex holds for f be complex-valued FinSequence holds ((c (#) f) ^2 ) = ((c ^2 ) (#) (f ^2 ))

 proof

 let c be Complex;

 let f be complex-valued FinSequence;



 A1: ( dom ((c (#) f) ^2 )) = ( dom (c (#) f)) by VALUED_1: 11

 .= ( dom f) by VALUED_1:def 5;



 A2: ( dom ((c ^2 ) (#) (f ^2 ))) = ( dom (f ^2 )) by VALUED_1:def 5

 .= ( dom f) by VALUED_1: 11;

 now

 let x be object;

 assume x in ( dom ((c (#) f) ^2 ));



 thus (((c (#) f) ^2 ) . x) = (((c (#) f) . x) ^2 ) by VALUED_1: 11

 .= ((c * (f . x)) ^2 ) by VALUED_1: 6

 .= ((c ^2 ) * ((f . x) ^2 ))

 .= ((c ^2 ) * ((f ^2 ) . x)) by VALUED_1: 11

 .= (((c ^2 ) (#) (f ^2 )) . x) by VALUED_1: 6;

 end;

 hence thesis by A1, A2;

 end;

 theorem :: BORSUK_7:19



 Th18: for c be Complex holds for f be complex-valued FinSequence holds ((f (/) c) ^2 ) = ((f ^2 ) (/) (c ^2 ))

 proof

 let c be Complex;

 let f be complex-valued FinSequence;



 thus ((f (/) c) ^2 ) = (((1 / c) ^2 ) (#) (f ^2 )) by Th17

 .= (((1 * 1) / (c * c)) (#) (f ^2 )) by XCMPLX_1: 76

 .= ((f ^2 ) (/) (c ^2 ));

 end;

 theorem :: BORSUK_7:20



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

 proof

 let f be real-valued FinSequence;

 ( Sum (f (/) ( Sum f))) = (( Sum f) / ( Sum f)) by RVSUM_1: 87;

 hence thesis by XCMPLX_1: 60;

 end;



 Lm6: (1,2,3) are_mutually_distinct ;

 ::$Canceled

 ::$Canceled

 theorem :: BORSUK_7:30



 Th20: <*a, b, c*> = ((1,2,3) --> (a,b,c))

 proof

 set f = ((1,2,3) --> (a,b,c));

 set g = <*a, b, c*>;



 A1: ( dom g) = ( Seg ( len g)) by FINSEQ_1:def 3

 .= {1, 2, 3} by FINSEQ_1: 45, FINSEQ_3: 1;



 A2: ( dom f) = {1, 2, 3} by FUNCT_4: 128;

 now

 let x be object;

 assume

 A3: x in ( dom f);

 per cases by A2, A3, ENUMSET1:def 1;

 suppose

 A4: x = 1;



 hence (f . x) = a by FUNCT_4: 134

 .= (g . x) by A4, FINSEQ_1: 45;

 end;

 suppose

 A5: x = 2;



 hence (f . x) = b by FUNCT_4: 135

 .= (g . x) by A5, FINSEQ_1: 45;

 end;

 suppose

 A6: x = 3;



 hence (f . x) = c by FUNCT_4: 135

 .= (g . x) by A6, FINSEQ_1: 45;

 end;

 end;

 hence thesis by A1, FUNCT_4: 128, FUNCT_1: 2;

 end;

 theorem :: BORSUK_7:31



 Th21: (a,b,c) are_mutually_distinct implies ( product ((a,b,c) --> ( {x}, {y}, {z}))) = {((a,b,c) --> (x,y,z))}

 proof

 assume

 A1: (a,b,c) are_mutually_distinct ;

 set X = {((a,b,c) --> (x,y,z))}, f = ((a,b,c) --> ( {x}, {y}, {z}));



 A2: ( dom f) = {a, b, c} by FUNCT_4: 128;

 now

 let m be object;

 thus m in X implies ex g be Function st m = g & ( dom g) = ( dom f) & for x be object st x in ( dom f) holds (g . x) in (f . x)

 proof

 assume

 A3: m in X;

 take g = ((a,b,c) --> (x,y,z));

 thus m = g by A3, TARSKI:def 1;

 thus ( dom g) = ( dom f) by A2, FUNCT_4: 128;

 let k be object;

 assume k in ( dom f);

 then

 A4: k = a or k = b or k = c by A2, ENUMSET1:def 1;

 (g . a) = x & (f . a) = {x} & (g . b) = y & (f . b) = {y} & (g . c) = z & (f . c) = {z} by A1, FUNCT_4: 135, FUNCT_4: 134;

 hence (g . k) in (f . k) by A4, TARSKI:def 1;

 end;

 given g be Function such that

 A5: m = g and

 A6: ( dom g) = ( dom f) and

 A7: for x be object st x in ( dom f) holds (g . x) in (f . x);

 a in ( dom f) & b in ( dom f) & c in ( dom f) by A2, ENUMSET1:def 1;

 then (g . a) in (f . a) & (g . b) in (f . b) & (g . c) in (f . c) & (f . a) = {x} & (f . b) = {y} & (f . c) = {z} by A1, A7, FUNCT_4: 135, FUNCT_4: 134;

 then (g . a) = x & (g . b) = y & (g . c) = z by TARSKI:def 1;

 then g = ((a,b,c) --> (x,y,z)) by A2, A6, FUNCT_4: 136;

 hence m in X by A5, TARSKI:def 1;

 end;

 hence thesis by CARD_3:def 5;

 end;

 theorem :: BORSUK_7:32



 Th22: for A,B,C,D,E,F be 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

 let A,B,C,D,E,F be set such that

 A1: A c= B & C c= D & E c= F;

 set f = ((a,b,c) --> (A,C,E)), g = ((a,b,c) --> (B,D,F));



 A2: ( dom f) = {a, b, c} & ( dom g) = {a, b, c} by FUNCT_4: 128;

 per cases ;

 suppose a = c & a <> b;

 then f = ((a,b) --> (E,C)) & g = ((a,b) --> (F,D)) by FUNCT_4: 132;

 hence ( product f) c= ( product g) by A1, TOPREAL6: 21;

 end;

 suppose b = c & a <> b;

 then f = ((a,b) --> (A,E)) & g = ((a,b) --> (B,F)) by FUNCT_4: 133;

 hence ( product f) c= ( product g) by A1, TOPREAL6: 21;

 end;

 suppose a = b;

 then f = ((a,c) --> (C,E)) & g = ((a,c) --> (D,F)) by FUNCT_4: 81;

 hence ( product f) c= ( product g) by A1, TOPREAL6: 21;

 end;

 suppose

 A3: a <> b & a <> c & b <> c;

 for x be object st x in ( dom f) holds (f . x) c= (g . x)

 proof

 let x be object;

 assume x in ( dom f);

 then

 A4: x = a or x = b or x = c by A2, ENUMSET1:def 1;

 (a,b,c) are_mutually_distinct by A3;

 then (f . a) = A & (f . b) = C & (f . c) = E & (g . a) = B & (g . b) = D & (g . c) = F by FUNCT_4: 135, FUNCT_4: 134;

 hence thesis by A1, A4;

 end;

 hence thesis by A2, CARD_3: 27;

 end;

 end;

 theorem :: BORSUK_7:33



 Th23: (a,b,c) are_mutually_distinct & x in X & y in Y & z in Z implies ((a,b,c) --> (x,y,z)) in ( product ((a,b,c) --> (X,Y,Z)))

 proof

 assume

 A1: (a,b,c) are_mutually_distinct ;

 assume x in X & y in Y & z in Z;

 then {x} c= X & {y} c= Y & {z} c= Z by ZFMISC_1: 31;

 then ( product ((a,b,c) --> ( {x}, {y}, {z}))) c= ( product ((a,b,c) --> (X,Y,Z))) by Th22;

 then {((a,b,c) --> (x,y,z))} c= ( product ((a,b,c) --> (X,Y,Z))) by A1, Th21;

 hence thesis by ZFMISC_1: 31;

 end;

 definition

 let f be Function;

 :: BORSUK_7:def1

 attr f is odd means for x,y be complex-valued Function st x in ( dom f) & ( - x) in ( dom f) & y = (f . x) holds (f . ( - x)) = ( - y);

 end

 registration

 cluster {} -> odd;

 coherence ;

 end

 registration

 cluster odd for complex-functions-valued Function;

 existence

 proof

 take {} ;

 thus thesis;

 end;

 end

 set TC2 = ( Tunit_circle 2);

 set TC3 = ( Tunit_circle 3);



 Lm7: the carrier of TC3 = ( Sphere (o,1)) by EUCLID_5: 4, TOPREALB: 9;

 theorem :: BORSUK_7:34

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

 proof

 let p be Point of ( TOP-REAL 3);

 p = |[(p `1 ), (p `2 ), (p `3 )]| by EUCLID_5: 3;

 hence thesis by Th15;

 end;

 theorem :: BORSUK_7:35



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

 proof

 let p be Point of ( TOP-REAL 3);

 p = |[(p `1 ), (p `2 ), (p `3 )]| by EUCLID_5: 3;

 hence thesis by Th16;

 end;

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

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



 Lm8: the carrier of RR = QQ by PRE_TOPC: 8;

 theorem :: BORSUK_7:36



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

 proof

 let S be Subset of R^1 such that

 A1: S = RAT ;

 set X = ]. -infty , r.[;

 reconsider R = ( RAT /\ X) as Subset of RR by Lm8, XBOOLE_1: 17;



 A2: ( R^1 X) is open by BORSUK_5: 40;

 R = (( R^1 X) /\ the carrier of RR) by PRE_TOPC: 8;

 hence thesis by A1, A2, TSP_1:def 1;

 end;

 theorem :: BORSUK_7:37



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

 proof

 let S be Subset of R^1 such that

 A1: S = RAT ;

 set X = ].r, +infty .[;

 reconsider R = ( RAT /\ X) as Subset of RR by Lm8, XBOOLE_1: 17;



 A2: ( R^1 X) is open by BORSUK_5: 40;

 R = (( R^1 X) /\ the carrier of RR) by PRE_TOPC: 8;

 hence thesis by A1, A2, TSP_1:def 1;

 end;

 Lm9:

 now

 let T be connected non empty TopSpace;

 let f be Function of T, RR;

 let x,y be set such that

 A1: x in ( dom f) & y in ( dom f);

 assume (f . x) < (f . y);

 then

 consider r be 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: ( [#] GX) = ( rng f) by WAYBEL18: 9;

 thus ex Q1,Q2 be Subset of GX st Q1 misses Q2 & Q1 <> ( {} GX) & Q2 <> ( {} GX) & Q1 is open & Q2 is open & ( [#] GX) = (Q1 \/ Q2)

 proof

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

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

 Q1 c= ( rng f)

 proof

 let x be object;

 assume x in Q1;

 then ex q be Element of RAT st x = q & q in ( rng f) & q < r;

 hence thesis;

 end;

 then

 reconsider Q1 as Subset of GX by WAYBEL18: 9;

 Q2 c= ( rng f)

 proof

 let x be object;

 assume x in Q2;

 then ex q be Element of RAT st x = q & q in ( rng f) & q > r;

 hence thesis;

 end;

 then

 reconsider Q2 as Subset of GX by WAYBEL18: 9;

 take Q1, Q2;

 thus Q1 misses Q2

 proof

 assume not thesis;

 then

 consider x be object such that

 A5: x in Q1 & x in Q2 by XBOOLE_0: 3;

 (ex q be Element of RAT st x = q & q in ( rng f) & q > r) & ex q be Element of RAT st x = q & q in ( rng f) & q < r by A5;

 hence thesis;

 end;

 (f . x) in Q1 & (f . y) in Q2 by A2, A3, Lm8;

 hence Q1 <> ( {} GX) & Q2 <> ( {} GX);

 reconsider G1 = ( RAT /\ ]. -infty , r.[) as open Subset of RR by Th26;

 reconsider G2 = ( RAT /\ ].r, +infty .[) as open Subset of RR by Th27;

 Q1 = (G1 /\ the carrier of GX)

 proof

 thus Q1 c= (G1 /\ the carrier of GX)

 proof

 let x be object;

 assume x in Q1;

 then

 consider q be 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 thesis by A4, A6, A7, XBOOLE_0:def 4;

 end;

 let x be object;

 assume

 A9: x in (G1 /\ the carrier of GX);

 then

 A10: x in the carrier of GX by XBOOLE_0:def 4;



 A11: x in G1 by A9, XBOOLE_0:def 4;

 then

 reconsider 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 thesis by A4, A10;

 end;

 hence Q1 is open by TSP_1:def 1;

 Q2 = (G2 /\ the carrier of GX)

 proof

 thus Q2 c= (G2 /\ the carrier of GX)

 proof

 let x be object;

 assume x in Q2;

 then

 consider q be 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 thesis by A4, A12, A13, XBOOLE_0:def 4;

 end;

 let x be object;

 assume

 A15: x in (G2 /\ the carrier of GX);

 then

 A16: x in the carrier of GX by XBOOLE_0:def 4;



 A17: x in G2 by A15, XBOOLE_0:def 4;

 then

 reconsider 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 thesis by A4, A16;

 end;

 hence Q2 is open by TSP_1:def 1;

 thus (Q1 \/ Q2) = ( [#] GX)

 proof

 thus (Q1 \/ Q2) c= ( [#] GX);

 let x be Element of GX;

 assume

 A18: x in ( [#] GX);

 x < r or x > r by Lm8, A4, XXREAL_0: 1;

 then x in Q1 or x in Q2 by A18, Lm8, A4;

 hence thesis by XBOOLE_0:def 3;

 end;

 end;

 end;

 registration

 let X be connected non empty TopSpace, Y be non empty TopSpace;

 let f be continuous Function of X, Y;

 cluster ( Image f) -> connected;

 coherence

 proof

 set g = ( corestr f);



 A1: ( dom g) = ( [#] X) by FUNCT_2:def 1;

 ( rng g) = ( [#] ( Image f)) by FUNCT_2:def 3;

 then (g .: ( [#] X)) = ( [#] ( Image f)) by A1, RELAT_1: 113;

 hence thesis by CONNSP_1: 14, WAYBEL18: 10;

 end;

 end

 theorem :: BORSUK_7:38



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

 proof

 let S be Subset of R^1 such that

 A1: S = RAT ;

 let T be connected TopSpace;

 let f be Function of T, ( R^1 | S) such that

 A2: f is continuous;

 per cases ;

 suppose

 A3: T is non empty;

 set GX = ( Image f);

 let x,y be object such that

 A4: x in ( dom f) & y in ( dom f) and

 A5: (f . x) <> (f . y);

 per cases by A5, XXREAL_0: 1;

 suppose (f . x) < (f . y);

 then ex Q1,Q2 be Subset of GX st Q1 misses Q2 & Q1 <> ( {} GX) & Q2 <> ( {} GX) & Q1 is open & Q2 is open & ( [#] GX) = (Q1 \/ Q2) by A1, A3, A4, Lm9;

 hence thesis by A1, A2, A3, CONNSP_1: 11;

 end;

 suppose (f . y) < (f . x);

 then ex Q1,Q2 be Subset of GX st Q1 misses Q2 & Q1 <> ( {} GX) & Q2 <> ( {} GX) & Q1 is open & Q2 is open & ( [#] GX) = (Q1 \/ Q2) by A1, A3, A4, Lm9;

 hence thesis by A1, A2, A3, CONNSP_1: 11;

 end;

 end;

 suppose T is empty;

 hence thesis;

 end;

 end;

 theorem :: BORSUK_7:39



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

 proof

 set X = R^1 ;

 let a,b be Real;

 set S = ( Closed-Interval-TSpace (a,b));

 let f be continuous Function of S, X;

 let g be PartFunc of REAL , REAL ;

 assume that

 A1: a <= b and

 A2: f = g;

 set A = ( left_closed_halfline a);

 set B = [.a, b.];

 set C = ( right_closed_halfline b);

 the carrier of S = B by A1, TOPMETR: 18;

 then

 reconsider a1 = a, b1 = b as Point of S by A1, XXREAL_1: 1;

 set f1 = ((X | ( R^1 A)) --> (f . a1));

 set f2 = ((X | ( R^1 C)) --> (f . b1));



 A3: the carrier of (X | ( R^1 A)) = A by PRE_TOPC: 8;

 S = (X | ( R^1 B)) by A1, TOPMETR: 19;

 then

 reconsider f as continuous Function of (X | ( R^1 B)), X;



 A4: ( dom f1) = the carrier of (X | ( R^1 A))

 .= A by PRE_TOPC: 8;



 A5: ( dom f) = the carrier of (X | ( R^1 B)) by FUNCT_2:def 1

 .= B by PRE_TOPC: 8;



 A6: ( dom f2) = the carrier of (X | ( R^1 C))

 .= C by PRE_TOPC: 8;

 b in REAL by XREAL_0:def 1;

 then

 A7: b < +infty by XXREAL_0: 9;

 f1 tolerates f

 proof

 let x be object such that

 A8: x in (( dom f1) /\ ( dom f));

 a in REAL by XREAL_0:def 1;

 then (A /\ B) = {a} by A1, XXREAL_0: 12, XXREAL_1: 417;

 then

 A9: x = a by A4, A5, A8, TARSKI:def 1;

 then a in A by A4, A8, XBOOLE_0:def 4;

 hence (f1 . x) = (f . x) by A3, A9, FUNCOP_1: 7;

 end;

 then

 reconsider ff = (f1 +* f) as continuous Function of (X | (( R^1 A) \/ ( R^1 B))), X by TOPGEN_5: 10;

 set G = (ff +* f2);

 ff tolerates f2

 proof

 let x be object;

 assume

 A10: x in (( dom ff) /\ ( dom f2));

 then

 A11: x in ( dom ff) by XBOOLE_0:def 4;



 A12: x in ( dom f2) by A10;

 then

 reconsider y = x as Real;



 A13: b <= y by A6, A12, XXREAL_1: 3;



 A14: ( dom ff) = (( dom f1) \/ ( dom f)) by FUNCT_4:def 1;

 per cases by A11, A14, XBOOLE_0:def 3;

 suppose that

 A15: x in ( dom f1) and

 A16: not x in ( dom f);

 y <= a by A4, A15, XXREAL_1: 2;

 then b <= a by A13, XXREAL_0: 2;

 then a = b by A1, XXREAL_0: 1;



 hence (f2 . x) = (f . a1) by A10, FUNCOP_1: 7

 .= (f1 . x) by A15, FUNCOP_1: 7

 .= (ff . x) by A16, FUNCT_4: 11;

 end;

 suppose

 A17: x in ( dom f);

 then y <= b by A5, XXREAL_1: 1;

 then b = y by A13, XXREAL_0: 1;



 hence (f2 . x) = (f . x) by A10, FUNCOP_1: 7

 .= (ff . x) by A17, FUNCT_4: 13;

 end;

 end;

 then

 A18: G is continuous Function of (X | (( R^1 (A \/ B)) \/ ( R^1 C))), X by TOPGEN_5: 10;



 A19: ((A \/ B) \/ C) c= REAL ;



 A20: ( dom G) = (( dom ff) \/ ( dom f2)) by FUNCT_4:def 1

 .= ((( dom f1) \/ ( dom f)) \/ ( dom f2)) by FUNCT_4:def 1;



 A21: ( dom G) = REAL

 proof

 thus ( dom G) c= REAL by A4, A5, A6, A19, A20;

 let x be object;

 assume x in REAL ;

 then

 reconsider y = x as Element of REAL ;



 A22: y < +infty by XXREAL_0: 9;



 A23: -infty < y by XXREAL_0: 12;

 per cases ;

 suppose

 A24: y < b;

 per cases ;

 suppose y < a;

 then y in A by A23, XXREAL_1: 2;

 then y in (( dom f1) \/ ( dom f)) by A4, XBOOLE_0:def 3;

 hence thesis by A20, XBOOLE_0:def 3;

 end;

 suppose y >= a;

 then y in B by A24, XXREAL_1: 1;

 then y in (( dom f1) \/ ( dom f)) by A5, XBOOLE_0:def 3;

 hence thesis by A20, XBOOLE_0:def 3;

 end;

 end;

 suppose y >= b;

 then y in C by A22, XXREAL_1: 3;

 hence thesis by A6, A20, XBOOLE_0:def 3;

 end;

 end;

 then ((A \/ B) \/ C) = ( [#] X) by A4, A5, A6, A20, TOPMETR: 17;

 then

 A25: (X | (( R^1 (A \/ B)) \/ ( R^1 C))) = X by TSEP_1: 3;

 ( rng G) c= REAL by TOPMETR: 17;

 then

 reconsider G as PartFunc of REAL , REAL by A21, RELSET_1: 4;



 A26: G is continuous by A18, A25, JORDAN5A: 7;



 A27: ( dom f) = (( dom G) /\ B) by A5, A21, XBOOLE_1: 28;

 now

 let x be object;

 assume

 A28: x in ( dom f);

 then

 reconsider y = x as Real;



 A29: y <= b by A5, A28, XXREAL_1: 1;

 per cases by A29, XXREAL_0: 1;

 suppose y < b;

 then not y in ( dom f2) by A6, XXREAL_1: 3;



 hence (G . x) = (ff . x) by FUNCT_4: 11

 .= (f . x) by A28, FUNCT_4: 13;

 end;

 suppose

 A30: y = b;

 then

 A31: x in ( dom f2) by A6, A7, XXREAL_1: 3;



 hence (G . x) = (f2 . x) by FUNCT_4: 13

 .= (f . x) by A30, A31, FUNCOP_1: 7;

 end;

 end;

 then g = (G | B) by A2, A27, FUNCT_1: 46;

 hence g is continuous by A26;

 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;

 :: original: +

 redefine

 func f + r -> Function of X, R^1 ;

 coherence

 proof

 (r + f) is Function of X, REAL ;

 hence thesis by TOPMETR: 17;

 end;

 end

 definition

 let X be set;

 let f be Function of X, R^1 ;

 let r;

 :: original: -

 redefine

 func f - r -> Function of X, R^1 ;

 coherence

 proof

 (f - r) is Function of X, REAL ;

 hence thesis by TOPMETR: 17;

 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

 now

 thus (f + r) is continuous;



 thus ((f + r) . 0 ) = ((f . j0) + r) by VALUED_1: 2

 .= (s + r) by BORSUK_2:def 4;



 thus ((f + r) . 1) = ((f . j1) + r) by VALUED_1: 2

 .= (t + r) by BORSUK_2:def 4;

 end;

 hence thesis by BORSUK_2:def 4;

 end;

 :: original: -

 redefine

 func f - r -> Path of (s - r), (t - r) ;

 coherence

 proof

 now

 thus (f - r) is continuous;



 thus ((f - r) . 0 ) = ((f . j0) - r) by VALUED_1: 2

 .= (s - r) by BORSUK_2:def 4;



 thus ((f - r) . 1) = ((f . j1) - r) by VALUED_1: 2

 .= (t - r) by BORSUK_2:def 4;

 end;

 hence thesis by BORSUK_2:def 4;

 end;

 end

 definition

 :: BORSUK_7:def2

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

 coherence

 proof

 set p = |[1, 0 , 0 ]|;

 |.(p - ( 0. ( TOP-REAL 3))).| = |.p.| by RLVECT_1: 13

 .= ( sqrt ((((p `1 ) ^2 ) + ((p `2 ) ^2 )) + ((p `3 ) ^2 ))) by Th25

 .= ( sqrt (((1 ^2 ) + ((p `2 ) ^2 )) + ((p `3 ) ^2 ))) by EUCLID_5: 2

 .= ( sqrt (((1 ^2 ) + (Q ^2 )) + ((p `3 ) ^2 ))) by EUCLID_5: 2

 .= 1 by EUCLID_5: 2, SQUARE_1: 18;

 then p in ( Sphere (( 0. ( TOP-REAL 3)),1)) by TOPREAL9: 9;

 hence thesis by TOPREALB: 9;

 end;

 end

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

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

 definition

 :: BORSUK_7:def3

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

 coherence

 proof

 |[( - 1), ( - Q), ( - Q)]| = ( - c100) by EUCLID_5: 11

 .= ( - c[100] );

 hence thesis by TOPREALC: 60;

 end;

 end

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

 theorem :: BORSUK_7:40



 Th30: ( - c[100] ) = c[-100]

 proof

 ( - c100) = |[( - 1), ( - Q), ( - Q)]| by EUCLID_5: 11

 .= c[-100] ;

 hence thesis;

 end;

 theorem :: BORSUK_7:41

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

 theorem :: BORSUK_7:42

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

 proof

 (c100 - mc100) = |[(1 - ( - 1)), (Q - Q), (Q - Q)]| by EUCLID_5: 13

 .= |[2, 0 , 0 ]|;

 hence thesis;

 end;

 theorem :: BORSUK_7:43

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

 proof

 let p be Point of T2;

 set c = ( euc2cpx p);



 A1: c = (( |.c.| * ( cos ( Arg c))) + (( |.c.| * ( sin ( Arg c))) * )) by COMPTRIG: 62;



 A2: |.c.| = |.p.| by EUCLID_3: 25;

 ( Re c) = (p `1 ) & ( Im c) = (p `2 ) by COMPLEX1: 12;

 hence thesis by A1, A2, COMPLEX1: 12;

 end;

 theorem :: BORSUK_7:44

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

 proof

 let p be Point of T2;

 set c = ( euc2cpx p);



 A1: c = (( |.c.| * ( cos ( Arg c))) + (( |.c.| * ( sin ( Arg c))) * )) by COMPTRIG: 62;

 |.c.| = |.p.| by EUCLID_3: 25;

 hence thesis by A1, EUCLID_3: 2;

 end;

 theorem :: BORSUK_7:45



 Th35: for p1,p2 be Point of ( TOP-REAL 2) holds |.p1.| = |.p2.| & ( Arg p1) = (( Arg p2) + ((2 * PI ) * i)) implies p1 = p2

 proof

 let p1,p2 be Point of T2;

 |.( euc2cpx p1).| = |.p1.| & |.( euc2cpx p2).| = |.p2.| by EUCLID_3: 25;

 hence thesis by Th12, EUCLID_3: 4;

 end;

 set CM = CircleMap ;

 theorem :: BORSUK_7:46



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

 proof

 let p be Point of T2;

 set z = ( euc2cpx p);

 set A = ((2 * PI ) * ( frac r));

 assume

 A1: p = (CM . r);

 reconsider q = (CM . ( R^1 r)) as Point of T2 by PRE_TOPC: 25;



 A2: |.z.| = |.p.| by EUCLID_3: 25;



 A3: |.q.| = 1 by TOPREALB: 12;

 ( frac r) < 1 & 0 <= ( frac r) by INT_1: 43;

 then

 A4: ((2 * PI ) * Q) <= A & A < ((2 * PI ) * 1) by XREAL_1: 68;



 A5: ( |[( cos ((2 * PI ) * r)), ( sin ((2 * PI ) * r))]| `1 ) = ( cos ((2 * PI ) * r)) & ( |[( cos ((2 * PI ) * r)), ( sin ((2 * PI ) * r))]| `2 ) = ( sin ((2 * PI ) * r)) by EUCLID: 52;



 A6: (CM . r) = |[( cos ((2 * PI ) * r)), ( sin ((2 * PI ) * r))]| by TOPREALB:def 11;

 A = (((2 * PI ) * r) + ((2 * PI ) * ( - [\r/])));

 then ( cos ((2 * PI ) * r)) = ( cos A) & ( sin ((2 * PI ) * r)) = ( sin A) by COMPLEX2: 8, COMPLEX2: 9;

 then z = (( |.z.| * ( cos A)) + (( |.z.| * ( sin A)) * )) by A1, A2, A3, A5, A6;

 hence thesis by A4, A2, A1, A3, COMPLEX1: 44, COMPTRIG:def 1;

 end;

 theorem :: BORSUK_7:47



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

 proof

 let p1,p2 be Point of ( TOP-REAL 3), u1,u2 be Point of ( Euclid 3);

 assume

 A1: u1 = p1 & u2 = p2;



 A2: p1 = |[(p1 `1 ), (p1 `2 ), (p1 `3 )]| by EUCLID_5: 3;

 reconsider p21 = (p2 `1 ), p22 = (p2 `2 ), p23 = (p2 `3 ) as Element of REAL by XREAL_0:def 1;

 reconsider p11 = (p1 `1 ), p12 = (p1 `2 ), p13 = (p1 `3 ) as Element of REAL by XREAL_0:def 1;



 A3: u2 = <*p21, p22, p23*> by A1, EUCLID_5: 3;

 reconsider v1 = u1, v2 = u2 as Element of ( REAL 3);

 reconsider d1 = ( diffreal . (p11,p21)), d2 = ( diffreal . (p12,p22)), d3 = ( diffreal . (p13,p23)) as Element of REAL ;

 (v1 - v2) = <*d1, d2, d3*> by A1, A2, A3, FINSEQ_2: 76

 .= <*((p1 `1 ) - (p2 `1 )), ( diffreal . ((p1 `2 ),(p2 `2 ))), ( diffreal . ((p1 `3 ),(p2 `3 )))*> by BINOP_2:def 10

 .= <*((p1 `1 ) - (p2 `1 )), ((p1 `2 ) - (p2 `2 )), ( diffreal . ((p1 `3 ),(p2 `3 )))*> by BINOP_2:def 10

 .= <*((p1 `1 ) - (p2 `1 )), ((p1 `2 ) - (p2 `2 )), ((p1 `3 ) - (p2 `3 ))*> by BINOP_2:def 10;



 then ( abs (v1 - v2)) = <*( absreal . ((p1 `1 ) - (p2 `1 ))), ( absreal . ((p1 `2 ) - (p2 `2 ))), ( absreal . ((p1 `3 ) - (p2 `3 )))*> by FINSEQ_2: 37

 .= <* |.((p1 `1 ) - (p2 `1 )).|, ( absreal . ((p1 `2 ) - (p2 `2 ))), ( absreal . ((p1 `3 ) - (p2 `3 )))*> by EUCLID:def 2

 .= <* |.((p1 `1 ) - (p2 `1 )).|, |.((p1 `2 ) - (p2 `2 )).|, ( absreal . ((p1 `3 ) - (p2 `3 )))*> by EUCLID:def 2

 .= <* |.((p1 `1 ) - (p2 `1 )).|, |.((p1 `2 ) - (p2 `2 )).|, |.((p1 `3 ) - (p2 `3 )).|*> by EUCLID:def 2;



 then

 A4: ( sqr ( abs (v1 - v2))) = <*( sqrreal . |.((p1 `1 ) - (p2 `1 )).|), ( sqrreal . |.((p1 `2 ) - (p2 `2 )).|), ( sqrreal . |.((p1 `3 ) - (p2 `3 )).|)*> by FINSEQ_2: 37

 .= <*( |.((p1 `1 ) - (p2 `1 )).| ^2 ), ( sqrreal . |.((p1 `2 ) - (p2 `2 )).|), ( sqrreal . |.((p1 `3 ) - (p2 `3 )).|)*> by RVSUM_1:def 2

 .= <*( |.((p1 `1 ) - (p2 `1 )).| ^2 ), ( |.((p1 `2 ) - (p2 `2 )).| ^2 ), ( sqrreal . |.((p1 `3 ) - (p2 `3 )).|)*> by RVSUM_1:def 2

 .= <*( |.((p1 `1 ) - (p2 `1 )).| ^2 ), ( |.((p1 `2 ) - (p2 `2 )).| ^2 ), ( |.((p1 `3 ) - (p2 `3 )).| ^2 )*> by RVSUM_1:def 2

 .= <*(((p1 `1 ) - (p2 `1 )) ^2 ), ( |.((p1 `2 ) - (p2 `2 )).| ^2 ), ( |.((p1 `3 ) - (p2 `3 )).| ^2 )*> by COMPLEX1: 75

 .= <*(((p1 `1 ) - (p2 `1 )) ^2 ), (((p1 `2 ) - (p2 `2 )) ^2 ), ( |.((p1 `3 ) - (p2 `3 )).| ^2 )*> by COMPLEX1: 75

 .= <*(((p1 `1 ) - (p2 `1 )) ^2 ), (((p1 `2 ) - (p2 `2 )) ^2 ), (((p1 `3 ) - (p2 `3 )) ^2 )*> by COMPLEX1: 75;

 (( Pitag_dist 3) . (u1,u2)) = |.(v1 - v2).| by EUCLID:def 6

 .= ( sqrt ( Sum ( sqr ( abs (v1 - v2))))) by EUCLID: 25;

 hence thesis by A4, RVSUM_1: 78;

 end;

 theorem :: BORSUK_7:48



 Th38: for p be Point of ( TOP-REAL 3), e be Point of ( Euclid 3) holds p = e & (p `3 ) = 0 implies ( 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

 let p be Point of ( TOP-REAL 3), e be Point of ( Euclid 3);

 set A = ].((p `1 ) - (r / ( sqrt 2))), ((p `1 ) + (r / ( sqrt 2))).[, B = ].((p `2 ) - (r / ( sqrt 2))), ((p `2 ) + (r / ( sqrt 2))).[, C = { 0 }, f = ((1,2,3) --> (A,B,C));

 assume that

 A1: p = e and

 A2: (p `3 ) = 0 ;

 let a be object;

 assume a in ( product f);

 then

 consider g be Function such that

 A3: a = g and

 A4: ( dom g) = ( dom f) and

 A5: for x be object st x in ( dom f) holds (g . x) in (f . x) by CARD_3:def 5;



 A6: A = { m where m be Real : ((p `1 ) - (r / ( sqrt 2))) < m & m < ((p `1 ) + (r / ( sqrt 2))) } by RCOMP_1:def 2;



 A7: B = { n where n be Real : ((p `2 ) - (r / ( sqrt 2))) < n & n < ((p `2 ) + (r / ( sqrt 2))) } by RCOMP_1:def 2;



 A8: ( dom f) = {1, 2, 3} by FUNCT_4: 128;

 then

 A9: 1 in ( dom f) & 2 in ( dom f) & 3 in ( dom f) by ENUMSET1:def 1;



 A10: (f . 1) = A & (f . 2) = B & (f . 3) = C by FUNCT_4: 135, FUNCT_4: 134;

 then

 A11: (g . 1) in A & (g . 2) in B & (g . 3) in C by A5, A9;

 then

 consider m be Real such that

 A12: m = (g . 1) and ((p `1 ) - (r / ( sqrt 2))) < m & m < ((p `1 ) + (r / ( sqrt 2))) by A6;

 consider n be Real such that

 A13: n = (g . 2) and ((p `2 ) - (r / ( sqrt 2))) < n & n < ((p `2 ) + (r / ( sqrt 2))) by A7, A11;

 (g . 3) in (f . 3) by A5, A9;

 then

 A14: (g . 3) = 0 by A10, TARSKI:def 1;

 ((p `1 ) + (r / ( sqrt 2))) > ((p `1 ) - (r / ( sqrt 2))) by A11, XXREAL_1: 28;

 then ((p `1 ) - ((p `1 ) + (r / ( sqrt 2)))) < ((p `1 ) - ((p `1 ) - (r / ( sqrt 2)))) by XREAL_1: 10;

 then (( - (r / ( sqrt 2))) + (r / ( sqrt 2))) < ((r / ( sqrt 2)) + (r / ( sqrt 2))) by XREAL_1: 6;

 then

 A15: 0 < r;



 A16: ( dom <*(g . 1), (g . 2), (g . 3)*>) = ( Seg ( len <*(g . 1), (g . 2), (g . 3)*>)) by FINSEQ_1:def 3

 .= {1, 2, 3} by FINSEQ_1: 45, FINSEQ_3: 1;

 now

 let k be object;

 assume k in ( dom g);

 then k = 1 or k = 2 or k = 3 by A4, A8, ENUMSET1:def 1;

 hence (g . k) = ( <*(g . 1), (g . 2), (g . 3)*> . k) by FINSEQ_1: 45;

 end;

 then

 A17: a = |[m, n, 0 ]| by A3, A4, A12, A13, A16, A14, FUNCT_4: 128, FUNCT_1: 2;

 then

 reconsider c = a as Point of ( TOP-REAL 3);

 reconsider b = c as Point of ( Euclid 3) by TOPREAL3: 8;

 |.(m - (p `1 )).| < (r / ( sqrt 2)) & |.(n - (p `2 )).| < (r / ( sqrt 2)) by A11, A12, A13, RCOMP_1: 1;

 then ( |.(m - (p `1 )).| ^2 ) < ((r / ( sqrt 2)) ^2 ) & ( |.(n - (p `2 )).| ^2 ) < ((r / ( sqrt 2)) ^2 ) by SQUARE_1: 16;

 then ( |.(m - (p `1 )).| ^2 ) < ((r ^2 ) / (( sqrt 2) ^2 )) & ( |.(n - (p `2 )).| ^2 ) < ((r ^2 ) / (( sqrt 2) ^2 )) by XCMPLX_1: 76;

 then ( |.(m - (p `1 )).| ^2 ) < ((r ^2 ) / 2) & ( |.(n - (p `2 )).| ^2 ) < ((r ^2 ) / 2) by SQUARE_1:def 2;

 then ((m - (p `1 )) ^2 ) < ((r ^2 ) / 2) & ((n - (p `2 )) ^2 ) < ((r ^2 ) / 2) by COMPLEX1: 75;

 then (((m - (p `1 )) ^2 ) + ((n - (p `2 )) ^2 )) < (((r ^2 ) / 2) + ((r ^2 ) / 2)) by XREAL_1: 8;

 then ( sqrt (((m - (p `1 )) ^2 ) + ((n - (p `2 )) ^2 ))) < ( sqrt (r ^2 )) by SQUARE_1: 27;

 then

 A18: ( sqrt (((m - (p `1 )) ^2 ) + ((n - (p `2 )) ^2 ))) < r by A15, SQUARE_1: 22;



 A19: m = (c `1 ) & n = (c `2 ) by A17, EUCLID_5: 2;

 ( dist (b,e)) = (( Pitag_dist 3) . (b,e)) by METRIC_1:def 1

 .= ( sqrt (((((c `1 ) - (p `1 )) ^2 ) + (((c `2 ) - (p `2 )) ^2 )) + (((c `3 ) - (p `3 )) ^2 ))) by A1, Th37

 .= ( sqrt (((((c `1 ) - (p `1 )) ^2 ) + (((c `2 ) - (p `2 )) ^2 )) + ((Q - Q) ^2 ))) by A2, A17, EUCLID_5: 2

 .= ( sqrt (((((c `1 ) - (p `1 )) ^2 ) + (((c `2 ) - (p `2 )) ^2 )) + Q));

 hence a in ( Ball (e,r)) by A18, A19, METRIC_1: 11;

 end;

 theorem :: BORSUK_7:49



 Th39: for c be Complex holds for s be Real holds ( Rotate (c,s)) = ( Rotate (c,(s + ((2 * PI ) * i))))

 proof

 let c be Complex;

 let s be Real;

 ( cos (s + ( Arg c))) = ( cos ((s + ( Arg c)) + ((2 * PI ) * i))) & ( sin (s + ( Arg c))) = ( sin ((s + ( Arg c)) + ((2 * PI ) * i))) by COMPLEX2: 8, COMPLEX2: 9;

 hence thesis;

 end;

 theorem :: BORSUK_7:50

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

 proof

 let s be Real;

 let p be Point of T2;

 set q = ((p `1 ) + ((p `2 ) * ));



 A1: ( Rotate (q,s)) = ( Rotate (q,(s + ((2 * PI ) * i)))) by Th39;



 thus (( Rotate s) . p) = |[( Re ( Rotate (q,s))), ( Im ( Rotate (q,s)))]| by JORDAN24:def 3

 .= (( Rotate (s + ((2 * PI ) * i))) . p) by A1, JORDAN24:def 3;

 end;

 theorem :: BORSUK_7:51



 Th41: for s be Real, p be Point of ( TOP-REAL 2) holds |.(( Rotate s) . p).| = |.p.|

 proof

 let s be Real;

 let p be Point of T2;

 set c = ( euc2cpx p);

 set q = (( Rotate s) . p);



 A1: ( Re ( Rotate (c,s))) = ( |.c.| * ( cos (s + ( Arg c)))) & ( Im ( Rotate (c,s))) = ( |.c.| * ( sin (s + ( Arg c)))) by COMPLEX1: 12;

 q = ( cpx2euc ( Rotate (c,s))) by JORDAN24:def 3;

 then

 A2: (q `1 ) = ( Re ( Rotate (c,s))) & (q `2 ) = ( Im ( Rotate (c,s))) by EUCLID: 52;

 ( |.p.| ^2 ) = (( |.c.| ^2 ) * 1) by EUCLID_3: 25

 .= (( |.c.| ^2 ) * ((( cos (s + ( Arg c))) ^2 ) + (( sin (s + ( Arg c))) ^2 ))) by SIN_COS: 29

 .= ((( |.c.| * ( cos (s + ( Arg c)))) ^2 ) + (( |.c.| * ( sin (s + ( Arg c)))) ^2 ))

 .= ( |.q.| ^2 ) by A1, A2, JGRAPH_1: 29;

 hence |.p.| = |.q.| by Th1;

 end;

 theorem :: BORSUK_7:52



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

 proof

 let s be Real;

 let p be Point of T2;

 (( Rotate s) . p) = ( cpx2euc ( Rotate (( euc2cpx p),s))) by JORDAN24:def 3;

 hence thesis by EUCLID_3: 1;

 end;

 theorem :: BORSUK_7:53



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

 proof

 let s be Real;

 let p be Point of T2;

 set c = ( euc2cpx p);

 assume p <> ( 0. T2);

 then ex i st ( Arg ( Rotate (c,s))) = (((2 * PI ) * i) + (s + ( Arg c))) by COMPLEX2: 54, EUCLID_3: 18;

 hence thesis by Th42;

 end;

 theorem :: BORSUK_7:54



 Th44: for s be Real holds (( Rotate s) . ( 0. ( TOP-REAL 2))) = ( 0. ( TOP-REAL 2))

 proof

 let s be Real;



 thus (( Rotate s) . ( 0. T2)) = ( cpx2euc ( Rotate (( euc2cpx ( 0. T2)),s))) by JORDAN24:def 3

 .= ( 0. T2) by COMPLEX2: 52, EUCLID_3: 16, EUCLID_3: 17;

 end;

 theorem :: BORSUK_7:55



 Th45: for s be Real, p be Point of ( TOP-REAL 2) holds (( Rotate s) . p) = ( 0. ( TOP-REAL 2)) implies p = ( 0. ( TOP-REAL 2))

 proof

 let s be Real;

 let p be Point of T2;

 |.p.| = |.(( Rotate s) . p).| by Th41;

 hence thesis by TOPRNS_1: 23, TOPRNS_1: 24;

 end;

 theorem :: BORSUK_7:56



 Th46: for s be Real, p be Point of ( TOP-REAL 2) holds (( Rotate s) . (( Rotate ( - s)) . p)) = p

 proof

 let s be Real;

 let p be Point of T2;

 set f = ( Rotate s);

 set g = ( Rotate ( - s));

 per cases ;

 suppose

 A1: p <> ( 0. T2);

 then

 consider i such that

 A2: ( Arg (g . p)) = ((( - s) + ( Arg p)) + ((2 * PI ) * i)) by Th43;

 consider j such that

 A3: ( Arg (f . (g . p))) = ((s + ( Arg (g . p))) + ((2 * PI ) * j)) by A1, Th45, Th43;



 A4: |.(f . (g . p)).| = |.(g . p).| by Th41

 .= |.p.| by Th41;

 ( Arg (f . (g . p))) = (( Arg p) + ((2 * PI ) * (i + j))) by A2, A3;

 hence (f . (g . p)) = p by A4, Th35;

 end;

 suppose

 A5: p = ( 0. T2);

 (( Rotate s) . (( Rotate ( - s)) . ( 0. T2))) = (( Rotate s) . ( 0. T2)) by Th44

 .= ( 0. T2) by Th44;

 hence thesis by A5;

 end;

 end;

 theorem :: BORSUK_7:57

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

 proof

 let s be Real;

 let p be Point of T2;

 set f = ( Rotate s);

 set g = ( Rotate ( - s));



 thus ((f * g) . p) = (f . (g . p)) by FUNCT_2: 15

 .= p by Th46

 .= (( id T2) . p);

 end;

 theorem :: BORSUK_7:58



 Th48: for s be Real, p be 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

 let s be Real;

 let p be Point of T2;



 A1: |.p.| = |.(( Rotate s) . p).| by Th41;



 A2: ((( Rotate s) . p) - ( 0. T2)) = (( Rotate s) . p) by RLVECT_1: 13;

 hereby

 assume p in ( Sphere (( 0. T2),r));

 then |.p.| = r by TOPREAL9: 12;

 hence (( Rotate s) . p) in ( Sphere (( 0. T2),r)) by A1, A2, TOPREAL9: 9;

 end;

 assume (( Rotate s) . p) in ( Sphere (( 0. T2),r));

 then

 A3: |.(( Rotate s) . p).| = r by TOPREAL9: 12;



 A4: (( Rotate ( - s)) . (( Rotate ( - ( - s))) . p)) = p by Th46;

 ((( Rotate ( - s)) . (( Rotate s) . p)) - ( 0. T2)) = (( Rotate ( - s)) . (( Rotate s) . p)) by RLVECT_1: 13;

 hence p in ( Sphere (( 0. T2),r)) by A4, A3, A1, TOPREAL9: 9;

 end;

 theorem :: BORSUK_7:59



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

 proof

 let r be non negative Real;

 let s be Real;

 set f = ( Rotate s);

 set C = ( Sphere (( 0. T2),r));

 thus (f .: C) c= C

 proof

 let y be Point of T2;

 assume y in (f .: C);

 then ex c be Element of T2 st c in C & y = (f . c) by FUNCT_2: 65;

 hence y in C by Th48;

 end;

 let y be Point of T2;

 set x = (( Rotate ( - s)) . y);

 assume y in C;

 then x in C by Th48;

 then (f . x) in (f .: C) by FUNCT_2: 35;

 hence y in (f .: C) by Th46;

 end;

 definition

 let r be non negative Real;

 let s be Real;

 :: BORSUK_7:def4

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

 coherence

 proof

 set T = ( Tcircle (( 0. T2),r));

 set f = (( Rotate s) | T);

 set C = the carrier of T;



 A1: ( dom f) = C by FUNCT_2:def 1;

 for x st x in C holds (f . x) in C

 proof

 let x;

 assume

 A2: x in C;

 then

 A3: (f . x) = (( Rotate s) . x) by FUNCT_1: 49;

 the carrier of T = ( Sphere (( 0. T2),r)) by TOPREALB: 9;

 hence thesis by A3, A2, Th48;

 end;

 hence thesis by A1, FUNCT_2: 3;

 end;

 end

 registration

 let r be non negative Real, s be Real;

 cluster ( RotateCircle (r,s)) -> being_homeomorphism;

 coherence

 proof

 set T = ( Tcircle (( 0. T2),r));

 set C = ( [#] T);

 C c= ( [#] T2) by PRE_TOPC:def 4;

 then

 reconsider C as Subset of T2;



 A1: the TopStruct of T2 = ( TopSpaceMetr ( Euclid 2)) by EUCLID:def 8;

 then

 reconsider f = ( Rotate s) as Function of ( TopSpaceMetr ( Euclid 2)), ( TopSpaceMetr ( Euclid 2));



 A2: f is onto isometric by JORDAN24: 2;

 reconsider A = C as Subset of ( TopSpaceMetr ( Euclid 2)) by A1;

 (T2 | C) = T by PRE_TOPC:def 5;

 then

 A3: (( TopSpaceMetr ( Euclid 2)) | A) = T by A1, PRE_TOPC: 36;

 the carrier of T = ( Sphere (( 0. T2),r)) by TOPREALB: 9;

 then (( Rotate s) .: C) = C by Th49;

 hence thesis by A2, A3, JORDAN24: 14;

 end;

 end

 theorem :: BORSUK_7:60



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

 proof

 let p be Point of T2;

 assume

 A1: p = (CM . r2);

 set s = ( - ( Arg p));

 reconsider q = (CM . ( R^1 r1)), w = (CM . ( R^1 (r1 - r2))) as Point of T2 by PRE_TOPC: 25;

 |.q.| = 1 by TOPREALB: 12;

 then q <> ( 0. T2) by TOPRNS_1: 23;

 then

 consider i such that

 A2: ( Arg (( Rotate s) . q)) = ((s + ( Arg q)) + ((2 * PI ) * i)) by Th43;



 A3: ( Arg p) = ((2 * PI ) * ( frac r2)) by A1, Th36;



 A4: |.(( Rotate s) . q).| = |.q.| by Th41

 .= 1 by TOPREALB: 12

 .= |.w.| by TOPREALB: 12;

 consider j such that

 A5: ( frac (r1 - r2)) = ((( frac r1) - ( frac r2)) + j) and j = 0 or j = 1 by Th4;



 A6: ( Arg (( Rotate s) . q)) = ((( - ((2 * PI ) * ( frac r2))) + ((2 * PI ) * ( frac r1))) + ((2 * PI ) * i)) by A2, A3, Th36

 .= (((2 * PI ) * ( frac (r1 - r2))) + ((2 * PI ) * (i - j))) by A5

 .= (( Arg w) + ((2 * PI ) * (i - j))) by Th36;



 thus (( RotateCircle (1,s)) . (CM . r1)) = (( Rotate s) . q) by FUNCT_1: 49

 .= (CM . (r1 - r2)) by A4, A6, Th35;

 end;

 begin

 definition

 let n be non zero Nat;

 let p be Point of ( TOP-REAL n);

 let r be non negative Real;

 :: BORSUK_7:def5

 func CircleIso (p,r) -> Function of ( Tunit_circle n), ( Tcircle (p,r)) means

 : Def5: for a be Point of ( Tunit_circle n), b be Point of ( TOP-REAL n) st a = b holds (it . a) = ((r * b) + p);

 existence

 proof

 set U = ( Tunit_circle n), C = ( Tcircle (p,r));

 defpred P[ Point of U, set] means ex w be Point of ( TOP-REAL n) st w = $1 & $2 = ((r * w) + p);



 A1: n in NAT by ORDINAL1:def 12;

 then

 A2: the carrier of C = ( Sphere (p,r)) by TOPREALB: 9;



 A3: for u be Point of U holds ex y be Point of C st P[u, y]

 proof

 let u be Point of U;

 reconsider v = u as Point of ( TOP-REAL n) by PRE_TOPC: 25;

 set y = ((r * v) + p);

 |.(y - p).| = |.(r * v).| by RLVECT_4: 1

 .= ( |.r.| * |.v.|) by TOPRNS_1: 7

 .= (r * |.v.|) by ABSVALUE:def 1

 .= (r * 1) by A1, TOPREALB: 12;

 then

 reconsider y as Point of C by A2, TOPREAL9: 9;

 take y;

 thus P[u, y];

 end;

 consider f be Function of U, C such that

 A4: for x be Point of U holds P[x, (f . x)] from FUNCT_2:sch 3( A3);

 take f;

 let a be Point of U, b be Point of ( TOP-REAL n);

 P[a, (f . a)] by A4;

 hence thesis;

 end;

 uniqueness

 proof

 let f,g be Function of ( Tunit_circle n), ( Tcircle (p,r)) such that

 A5: for a be Point of ( Tunit_circle n), b be Point of ( TOP-REAL n) st a = b holds (f . a) = ((r * b) + p) and

 A6: for a be Point of ( Tunit_circle n), b be Point of ( TOP-REAL n) st a = b holds (g . a) = ((r * b) + p);

 let x be Point of ( Tunit_circle n);

 reconsider y = x as Point of ( TOP-REAL n) by PRE_TOPC: 25;



 thus (f . x) = ((r * y) + p) by A5

 .= (g . x) by A6;

 end;

 end

 registration

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

 cluster ( CircleIso (p,r)) -> being_homeomorphism;

 coherence

 proof



 A1: n in NAT by ORDINAL1:def 12;

 for a be Point of ( Tunit_circle n), b be Point of ( TOP-REAL n) st a = b holds (( CircleIso (p,r)) . a) = ((r * b) + p) by Def5;

 hence thesis by A1, TOPREALB: 19;

 end;

 end

 definition

 :: BORSUK_7:def6

 func SphereMap -> Function of R^1 , ( Tunit_circle 3) means

 : Def6: for x be Real holds (it . x) = |[( cos ((2 * PI ) * x)), ( sin ((2 * PI ) * x)), 0 ]|;

 existence

 proof

 defpred P[ Real, set] means $2 = |[( cos ((2 * PI ) * $1)), ( sin ((2 * PI ) * $1)), 0 ]|;



 A1: for x be Element of R^1 holds ex y be Element of TC3 st P[x, y]

 proof

 let x be Element of R^1 ;

 set y = |[( cos ((2 * PI ) * x)), ( sin ((2 * PI ) * x)), 0 ]|;

 |.(y - o).| = |.y.| by EUCLID_5: 4, RLVECT_1: 13

 .= ( sqrt ((((y `1 ) ^2 ) + ((y `2 ) ^2 )) + ((y `3 ) ^2 ))) by Th25

 .= ( sqrt (((( cos ((2 * PI ) * x)) ^2 ) + ((y `2 ) ^2 )) + ((y `3 ) ^2 ))) by EUCLID_5: 2

 .= ( sqrt (((( cos ((2 * PI ) * x)) ^2 ) + (( sin ((2 * PI ) * x)) ^2 )) + ((y `3 ) ^2 ))) by EUCLID_5: 2

 .= ( sqrt (((( cos ((2 * PI ) * x)) ^2 ) + (( sin ((2 * PI ) * x)) ^2 )) + (Q ^2 ))) by EUCLID_5: 2

 .= 1 by SIN_COS: 29, SQUARE_1: 18;

 then y is Element of TC3 by Lm7, TOPREAL9: 9;

 hence thesis;

 end;

 consider f be Function of R, TC3 such that

 A2: for x be Element of R^1 holds P[x, (f . x)] from FUNCT_2:sch 3( A1);

 take f;

 let x be Real;

 x is Point of R^1 by TOPMETR: 17, XREAL_0:def 1;

 hence thesis by A2;

 end;

 uniqueness

 proof

 let f,g be Function of R^1 , TC3 such that

 A3: for x be Real holds (f . x) = |[( cos ((2 * PI ) * x)), ( sin ((2 * PI ) * x)), 0 ]| and

 A4: for x be Real holds (g . x) = |[( cos ((2 * PI ) * x)), ( sin ((2 * PI ) * x)), 0 ]|;

 let x be Point of R^1 ;



 thus (f . x) = |[( cos ((2 * PI ) * x)), ( sin ((2 * PI ) * x)), 0 ]| by A3

 .= (g . x) by A4;

 end;

 end

 set SM = SphereMap ;

 theorem :: BORSUK_7:61

 ( SphereMap . i) = c[100]

 proof



 thus (SM . i) = |[( cos (((2 * PI ) * i) + Q)), (( sin ((2 * PI ) * i)) + Q), 0 ]| by Def6

 .= |[( cos 0 ), ( sin (((2 * PI ) * i) + Q)), 0 ]| by COMPLEX2: 9

 .= c[100] by COMPLEX2: 8, SIN_COS: 31;

 end;



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

 proof



 A1: sin = ( R^1 sin );

 ( R^1 | ( R^1 ( dom sin ))) = R^1 by SIN_COS: 24, TOPREALB: 6;

 hence thesis by A1;

 end;



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

 proof



 A1: cos = ( R^1 cos );

 ( R^1 | ( R^1 ( dom cos ))) = R^1 by SIN_COS: 24, TOPREALB: 6;

 hence thesis by A1;

 end;



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

 proof

 ( SphereMap . r) = |[( cos (((2 * PI ) * r) + Q)), ( sin ((2 * PI ) * r)), 0 ]| by Def6

 .= |[(( cos * ( AffineMap ((2 * PI ), 0 ))) . r), ( sin (((2 * PI ) * r) + Q)), 0 ]| by TOPREALB: 2

 .= |[(( cos * ( AffineMap ((2 * PI ), 0 ))) . r), (( sin * ( AffineMap ((2 * PI ), 0 ))) . r), 0 ]| by TOPREALB: 1;

 hence thesis;

 end;

 registration

 cluster SphereMap -> continuous;

 coherence

 proof



 A1: ( AffineMap ((2 * PI ), 0 )) = ( R^1 ( AffineMap ((2 * PI ), 0 )));



 A2: ( R^1 | ( R^1 ( dom sin ))) = R^1 by SIN_COS: 24, TOPREALB: 6;



 A3: ( R^1 | ( R^1 ( dom cos ))) = R^1 by SIN_COS: 24, TOPREALB: 6;

 set sR = ( R^1 sin ), cR = ( R^1 cos );

 reconsider sR, cR as Function of R^1 , R^1 by Lm10, Lm11;

 reconsider l = ( AffineMap ((2 * PI ), 0 )) as Function of R^1 , R^1 by TOPREALB: 8;



 A4: ( dom ( AffineMap ((2 * PI ), 0 ))) = REAL by FUNCT_2:def 1;



 A5: ( rng ( AffineMap ((2 * PI ), 0 ))) = ( [#] REAL ) by FCONT_1: 55;

 set s = (sR * l);

 set c = (cR * l);

 reconsider g = SM as Function of R^1 , ( TOP-REAL 3) by TOPREALA: 7;

 for p be Point of R^1 , V be Subset of ( TOP-REAL 3) st (g . p) in V & V is open holds ex W be Subset of R^1 st p in W & W is open & (g .: W) c= V

 proof

 let p be Point of R^1 , V be Subset of ( TOP-REAL 3) such that

 A6: (g . p) in V and

 A7: V is open;



 A8: V = ( Int V) by A7, TOPS_1: 23;

 reconsider e = (g . p) as Point of ( Euclid 3) by TOPREAL3: 8;

 consider r be Real such that

 A9: r > 0 and

 A10: ( Ball (e,r)) c= V by A6, A8, GOBOARD6: 5;

 set A = ].(((g . p) `1 ) - (r / ( sqrt 2))), (((g . p) `1 ) + (r / ( sqrt 2))).[;

 set B = ].(((g . p) `2 ) - (r / ( sqrt 2))), (((g . p) `2 ) + (r / ( sqrt 2))).[;

 set F = ((1,2,3) --> (A,B, { 0 }));



 A11: (g . p) = |[(c . p), (s . p), 0 ]| by Lm12;

 then

 A12: ((g . p) `2 ) = (s . p) by EUCLID_5: 2;

 ((g . p) `3 ) = 0 by A11, EUCLID_5: 2;

 then

 A13: ( product F) c= ( Ball (e,r)) by Th38;

 reconsider A, B as Subset of R^1 by TOPMETR: 17;



 A14: A is open by JORDAN6: 35;



 A15: B is open by JORDAN6: 35;



 A16: sR is continuous by A2, PRE_TOPC: 26;

 (s . p) in B by A9, A12, TOPREAL6: 15;

 then

 consider Ws be Subset of R^1 such that

 A17: p in Ws and

 A18: Ws is open and

 A19: (s .: Ws) c= B by A15, A16, A1, A4, A5, JGRAPH_2: 10, TOPREALB: 5;



 A20: ((g . p) `1 ) = (c . p) by A11, EUCLID_5: 2;



 A21: cR is continuous by A3, PRE_TOPC: 26;

 (c . p) in A by A9, A20, TOPREAL6: 15;

 then

 consider Wc be Subset of R^1 such that

 A22: p in Wc and

 A23: Wc is open and

 A24: (c .: Wc) c= A by A14, A21, A1, A4, A5, JGRAPH_2: 10, TOPREALB: 5;

 set W = (Ws /\ Wc);

 take W;

 thus p in W by A17, A22, XBOOLE_0:def 4;

 thus W is open by A18, A23;

 let y be Point of ( TOP-REAL 3);

 assume y in (g .: W);

 then

 consider x be Element of R^1 such that

 A25: x in W and

 A26: y = (g . x) by FUNCT_2: 65;



 A27: (g . x) = |[(c . x), (s . x), 0 ]| by Lm12;

 x in Ws by A25, XBOOLE_0:def 4;

 then

 A28: (s . x) in (s .: Ws) by FUNCT_2: 35;

 x in Wc by A25, XBOOLE_0:def 4;

 then

 A29: (c . x) in (c .: Wc) by FUNCT_2: 35;

 |[(c . x), (s . x), 0 ]| = ((1,2,3) --> ((c . x),(s . x), 0 )) by Th20;

 then |[(c . x), (s . x), 0 ]| in ( product F) by A19, A24, A28, A29, Lm2, Lm6, Th23;

 then |[(c . x), (s . x), 0 ]| in ( Ball (e,r)) by A13;

 hence y in V by A10, A26, A27;

 end;

 then g is continuous by JGRAPH_2: 10;

 hence thesis by PRE_TOPC: 27;

 end;

 end

 definition

 let r be Real;

 :: BORSUK_7:def7

 func eLoop (r) -> Function of I[01] , ( Tunit_circle 3) means

 : Def7: for x be Point of I[01] holds (it . x) = |[( cos (((2 * PI ) * r) * x)), ( sin (((2 * PI ) * r) * x)), 0 ]|;

 existence

 proof

 defpred P[ Real, set] means $2 = |[( cos (((2 * PI ) * r) * $1)), ( sin (((2 * PI ) * r) * $1)), 0 ]|;



 A1: for x be Element of I[01] holds ex y be Element of TC3 st P[x, y]

 proof

 let x be Element of I[01] ;

 set y = |[( cos (((2 * PI ) * r) * x)), ( sin (((2 * PI ) * r) * x)), 0 ]|;

 |.(y - o).| = |.y.| by EUCLID_5: 4, RLVECT_1: 13

 .= ( sqrt ((((y `1 ) ^2 ) + ((y `2 ) ^2 )) + ((y `3 ) ^2 ))) by Th25

 .= ( sqrt (((( cos (((2 * PI ) * r) * x)) ^2 ) + ((y `2 ) ^2 )) + ((y `3 ) ^2 ))) by EUCLID_5: 2

 .= ( sqrt (((( cos (((2 * PI ) * r) * x)) ^2 ) + (( sin (((2 * PI ) * r) * x)) ^2 )) + ((y `3 ) ^2 ))) by EUCLID_5: 2

 .= ( sqrt (((( cos (((2 * PI ) * r) * x)) ^2 ) + (( sin (((2 * PI ) * r) * x)) ^2 )) + (Q ^2 ))) by EUCLID_5: 2

 .= 1 by SIN_COS: 29, SQUARE_1: 18;

 then

 reconsider y as Element of TC3 by Lm7, TOPREAL9: 9;

 take y;

 thus P[x, y];

 end;

 ex f be Function of I, TC3 st for x be Element of I[01] holds P[x, (f . x)] from FUNCT_2:sch 3( A1);

 hence thesis;

 end;

 uniqueness

 proof

 let f,g be Function of I[01] , TC3 such that

 A2: for x be Point of I[01] holds (f . x) = |[( cos (((2 * PI ) * r) * x)), ( sin (((2 * PI ) * r) * x)), 0 ]| and

 A3: for x be Point of I[01] holds (g . x) = |[( cos (((2 * PI ) * r) * x)), ( sin (((2 * PI ) * r) * x)), 0 ]|;

 let x be Point of I[01] ;



 thus (f . x) = |[( cos (((2 * PI ) * r) * x)), ( sin (((2 * PI ) * r) * x)), 0 ]| by A2

 .= (g . x) by A3;

 end;

 end

 theorem :: BORSUK_7:62



 Th52: ( eLoop r) = ( SphereMap * ( ExtendInt r))

 proof

 let x be Point of I[01] ;



 A1: (( ExtendInt r) . x) = (r * x) by TOPALG_5:def 1;



 thus (( eLoop r) . x) = |[( cos (((2 * PI ) * r) * x)), ( sin (((2 * PI ) * r) * x)), 0 ]| by Def7

 .= |[( cos ((2 * PI ) * (( ExtendInt r) . x))), ( sin ((2 * PI ) * (( ExtendInt r) . x))), 0 ]| by A1

 .= (SM . (( ExtendInt r) . x)) by Def6

 .= ((SM * ( ExtendInt r)) . x) by FUNCT_2: 15;

 end;

 definition

 let i;

 :: original: eLoop

 redefine

 func eLoop (i) -> Loop of c[100] ;

 coherence

 proof

 set f = ( eLoop i);

 thus ( c[100] , c[100] ) are_connected ;

 f = (SM * ( ExtendInt i)) by Th52;

 hence f is continuous;



 thus (f . 0 ) = |[( cos (((2 * PI ) * i) * j0)), ( sin (((2 * PI ) * i) * j0)), 0 ]| by Def7

 .= c[100] by SIN_COS: 31;



 thus (f . 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;

 end;

 end

 registration

 let i;

 cluster ( eLoop i) -> nullhomotopic;

 coherence

 proof

 ( Tunit_circle 3) is having_trivial_Fundamental_Group by TOPALG_6: 47;

 hence thesis;

 end;

 end

 theorem :: BORSUK_7:63



 Th53: p <> ( 0. ( TOP-REAL n)) implies |.(p (/) |.p.|).| = 1

 proof



 A1: ( |.p.| ^2 ) = ( Sum ( sqr p)) by TOPREAL9: 5;

 assume p <> ( 0. ( TOP-REAL n));

 then |.p.| <> 0 by EUCLID_2: 42;

 then ( Sum (( sqr p) (/) ( Sum ( sqr p)))) = 1 by A1, Th19;

 hence thesis by A1, Th18, SQUARE_1: 18;

 end;

 definition

 let n be Nat;

 let p be Point of ( TOP-REAL n);

 assume

 A1: p <> ( 0. ( TOP-REAL n));

 :: BORSUK_7:def8

 func Rn->S1 (p) -> Point of ( Tcircle (( 0. ( TOP-REAL n)),1)) equals

 : Def8: (p (/) |.p.|);

 coherence

 proof



 A2: n in NAT by ORDINAL1:def 12;

 |.((p (/) |.p.|) - ( 0. ( TOP-REAL n))).| = |.(p (/) |.p.|).| by RLVECT_1: 13

 .= 1 by A1, Th53;

 then (p (/) |.p.|) in ( Sphere (( 0. ( TOP-REAL n)),1)) by TOPREAL9: 9;

 hence thesis by A2, TOPREALB: 9;

 end;

 end

 reserve n for non zero Nat;

 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);

 :: BORSUK_7:def9

 func Sn1->Sn (f) -> Function of ( Tunit_circle (n + 1)), ( Tunit_circle n) means

 : Def9: for x,y be Point of ( Tcircle (( 0. ( TOP-REAL (n + 1))),1)) st y = ( - x) holds (it . x) = ( Rn->S1 ((f . x) - (f . y)));

 existence

 proof

 defpred P[ Point of TC4, set] means for y be Point of TC4 st y = ( - $1) holds $2 = ( Rn->S1 ((f . $1) - (f . y)));



 A1: for x be Element of TC4 holds ex z be Element of TC2 st P[x, z]

 proof

 let x be Element of TC4;

 reconsider y = ( - x) as Element of TC4 by TOPREALC: 60;

 reconsider z = ( Rn->S1 ((f . x) - (f . y))) as Point of TC2;

 take z;

 thus thesis;

 end;

 ex g be Function of TC4, TC2 st for x be Element of TC4 holds P[x, (g . x)] from FUNCT_2:sch 3( A1);

 hence thesis;

 end;

 uniqueness

 proof

 let F,G be Function of TC3, TC2 such that

 A2: for x,y be Point of TC4 st y = ( - x) holds (F . x) = ( Rn->S1 ((f . x) - (f . y))) and

 A3: for x,y be Point of TC4 st y = ( - x) holds (G . x) = ( Rn->S1 ((f . x) - (f . y)));

 let p be Point of TC3;

 reconsider p2 = p as Point of TC4;

 reconsider p1 = ( - p) as Point of TC4 by TOPREALC: 60;



 thus (F . p) = ( Rn->S1 ((f . p2) - (f . p1))) by A2

 .= (G . p) by A3;

 end;

 end

 definition

 let x0,y0 be Point of ( Tunit_circle 2), xt be set, f be Path of x0, y0;

 :: BORSUK_7:def10

 func liftPath (f,xt) -> Function of I[01] , R^1 means

 : Def10: (it . 0 ) = xt & f = ( CircleMap * it ) & it is continuous & for f1 be 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

 definition

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

 :: BORSUK_7:def11

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

 end

 definition

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

 :: BORSUK_7:def12

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

 end

 definition

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

 :: BORSUK_7:def13

 attr f is with_antipodals means ex x,y be Point of ( TOP-REAL m) st (x,y) are_antipodals_of (p,r,f);

 end

 notation

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

 antonym f is without_antipodals for f is with_antipodals;

 end

 theorem :: BORSUK_7:64



 Th54: for n be non zero Nat, r be non negative Real, x be 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

 let n be non zero Nat, r be non negative Real, x be Point of ( TOP-REAL n) such that

 A1: x is Point of ( Tcircle (( 0. ( TOP-REAL n)),r));

 reconsider y = x as Point of ( Tcircle (( 0. ( TOP-REAL n)),r)) by A1;

 ( - x) = ( - y);

 hence x is Point of ( Tcircle (( 0. ( TOP-REAL n)),r)) & ( - x) is Point of ( Tcircle (( 0. ( TOP-REAL n)),r)) by TOPREALC: 60;

 (((1 - (1 / 2)) * x) + ((1 / 2) * ( - x))) = (((1 / 2) * x) + ( - ((1 / 2) * x))) by RLVECT_1: 25

 .= ( 0. ( TOP-REAL n)) by RLVECT_1: 5;

 hence thesis;

 end;

 theorem :: BORSUK_7:65



 Th55: for n be non zero Nat, p,x,y,x1,y1 be Point of ( TOP-REAL n), r be 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

 let n be non zero Nat, p,x,y,x1,y1 be Point of ( TOP-REAL n), r be positive Real;

 set h = ( CircleIso (p,r));

 assume that

 A1: (x,y) are_antipodals_of (( 0. ( TOP-REAL n)),1) and

 A2: x1 = (h . x) and

 A3: y1 = (h . y);



 A4: x is Point of ( Tcircle (( 0. ( TOP-REAL n)),1)) by A1;

 hence x1 is Point of ( Tcircle (p,r)) by A2, FUNCT_2: 5;



 A5: y is Point of ( Tcircle (( 0. ( TOP-REAL n)),1)) by A1;

 hence y1 is Point of ( Tcircle (p,r)) by A3, FUNCT_2: 5;

 ( 0. ( TOP-REAL n)) in ( LSeg (x,y)) by A1;

 then

 consider a be Real such that

 A6: ( 0. ( TOP-REAL n)) = (((1 - a) * x) + (a * y)) and

 A7: 0 <= a & a <= 1;



 A8: ((1 - a) * x1) = ((1 - a) * ((r * x) + p)) by A2, A4, Def5

 .= (((1 - a) * (r * x)) + ((1 - a) * p)) by RLVECT_1:def 5

 .= (((r * (1 - a)) * x) + ((1 - a) * p)) by RLVECT_1:def 7

 .= ((r * ((1 - a) * x)) + ((1 - a) * p)) by RLVECT_1:def 7;

 (a * y1) = (a * ((r * y) + p)) by A3, A5, Def5

 .= ((a * (r * y)) + (a * p)) by RLVECT_1:def 5

 .= (((r * a) * y) + (a * p)) by RLVECT_1:def 7

 .= ((r * (a * y)) + (a * p)) by RLVECT_1:def 7;



 then (((1 - a) * x1) + (a * y1)) = ((((r * ((1 - a) * x)) + ((1 - a) * p)) + (r * (a * y))) + (a * p)) by A8, RLVECT_1:def 3

 .= ((((r * ((1 - a) * x)) + (r * (a * y))) + ((1 - a) * p)) + (a * p)) by RLVECT_1:def 3

 .= (((r * (((1 - a) * x) + (a * y))) + ((1 - a) * p)) + (a * p)) by RLVECT_1:def 5

 .= ((( 0. ( TOP-REAL n)) + ((1 - a) * p)) + (a * p)) by A6, RLVECT_1: 10

 .= (((1 - a) * p) + (a * p)) by RLVECT_1: 4

 .= (((1 * p) - (a * p)) + (a * p)) by RLVECT_1: 35

 .= (1 * p) by RLVECT_4: 1

 .= p by RLVECT_1:def 8;

 hence thesis by A7;

 end;

 theorem :: BORSUK_7:66



 Th56: for f be Function of ( Tcircle (( 0. ( TOP-REAL (n + 1))),1)), ( TOP-REAL n) holds for x be Point of ( Tcircle (( 0. ( TOP-REAL (n + 1))),1)) st f is without_antipodals holds ((f . x) - (f . ( - x))) <> ( 0. ( TOP-REAL n))

 proof

 set TC4 = ( Tcircle (( 0. ( TOP-REAL (n + 1))),1));

 let f be Function of TC4, ( TOP-REAL n);

 let x be Point of TC4;

 assume

 A1: f is without_antipodals;



 A2: ( dom f) = the carrier of TC4 by FUNCT_2:def 1;

 reconsider y = ( - x) as Point of TC4 by TOPREALC: 60;

 reconsider a = x, b = y as Point of TC4;

 reconsider x1 = x as Point of ( TOP-REAL (n + 1)) by PRE_TOPC: 25;

 assume

 A3: ((f . x) - (f . ( - x))) = ( 0. ( TOP-REAL n));

 (x1,( - x1)) are_antipodals_of (( 0. ( TOP-REAL (n + 1))),1,f)

 proof

 thus (x1,( - x1)) are_antipodals_of (( 0. ( TOP-REAL (n + 1))),1) by Th54;

 (f . x) = (f . a) & (f . y) = (f . b);

 hence x1 in ( dom f) & ( - x1) in ( dom f) by A2;

 ((f . a) - (f . y)) = ( 0. ( TOP-REAL n)) by A3;

 hence (f . x1) = (f . ( - x1)) by RLVECT_1: 21;

 end;

 hence contradiction by A1;

 end;

 theorem :: BORSUK_7:67



 Th57: for f be Function of ( Tcircle (( 0. ( TOP-REAL (n + 1))),1)), ( TOP-REAL n) holds f is without_antipodals implies ( Sn1->Sn f) is odd

 proof

 set TC4 = ( Tcircle (( 0. ( TOP-REAL (n + 1))),1));

 let f be Function of TC4, ( TOP-REAL n);

 assume

 A1: f is without_antipodals;

 set g = ( Sn1->Sn f);

 let x,y be complex-valued Function such that

 A2: x in ( dom g) and

 A3: ( - x) in ( dom g) and

 A4: y = (g . x);

 reconsider b = ( - x) as Point of TC4 by A3;

 reconsider a = ( - b) as Point of TC4 by A2;

 set p = ((f . b) - (f . a));

 set q = ((f . a) - (f . b));



 A5: p = ( - q) by RLVECT_1: 33;

 ( 0. ( TOP-REAL n)) = ( 0* n) by EUCLID: 70;

 then

 A6: ( - p qua real-valued Function) <> ( 0. ( TOP-REAL n)) by A1, Th56, Th14;



 thus (g . ( - x)) = ( Rn->S1 p) by Def9

 .= (p (/) |.p.|) by A1, Th56, Def8

 .= (p (/) |.( - q).|) by RLVECT_1: 33

 .= (( - q) (/) |.( - q).|) by RLVECT_1: 33

 .= ( - (q qua real-valued Function (/) |.( - q).|)) by VALUED_2: 30

 .= ( - (q (/) |.q.|)) by TOPRNS_1: 26

 .= ( - ( Rn->S1 q)) by A5, A6, Def8

 .= ( - y) by A4, Def9;

 end;

 theorem :: BORSUK_7:68



 Th58: for f be Function of ( Tcircle (( 0. ( TOP-REAL (n + 1))),1)), ( TOP-REAL n) holds for g,B1 be 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

 let f be Function of ( Tcircle (( 0. ( TOP-REAL (n + 1))),1)), ( TOP-REAL n);

 let g,B1 be Function of ( Tcircle (( 0. ( TOP-REAL (n + 1))),1)), ( TOP-REAL n) such that

 A1: g = (f (-) ) and

 A2: B1 = (f <--> g) and

 A3: f is without_antipodals;

 set T = ( Tcircle (( 0. ( TOP-REAL (n + 1))),1));

 set B = ( Sn1->Sn f);

 set B2 = ((n NormF ) * B1);

 set BB = (B1 </> B2);

 set TC3 = ( Tunit_circle (n + 1));



 A4: ( dom B1) = the carrier of TC3 by FUNCT_2:def 1;

 ( dom (n NormF )) = the carrier of ( TOP-REAL n) by FUNCT_2:def 1;

 then ( rng B1) c= ( dom (n NormF ));

 then

 A5: ( dom B2) = ( dom B1) by RELAT_1: 27;



 A6: ( dom BB) = (( dom B1) /\ ( dom B2)) by VALUED_2: 71

 .= the carrier of TC3 by A5, FUNCT_2:def 1;

 hence ( dom B) = ( dom BB) by FUNCT_2:def 1;

 let x be object;

 assume x in ( dom B);

 then

 reconsider x1 = x as Point of T;

 reconsider y1 = ( - x1) as Point of T by TOPREALC: 60;

 set p = ((f . x1) - (f . y1));



 A7: ( dom g) = the carrier of T by FUNCT_2:def 1;



 A8: (B1 . x1) = ((f . x1) qua real-valued Function - (g . x1)) by A4, A2, VALUED_2:def 46

 .= p by A7, A1, VALUED_2:def 34;



 A9: (B2 . x1) = ((n NormF ) . (B1 . x1)) by FUNCT_2: 15

 .= |.p.| by A8, JGRAPH_4:def 1;

 (B . x1) = ( Rn->S1 p) by Def9

 .= ((B1 . x1) (/) (B2 . x1)) by A8, A9, A3, Th56, Def8

 .= ((B1 . x1) (#) ((B2 qua complex-valued Function " ) . x1)) by VALUED_1: 10

 .= (BB . x1) by A6, VALUED_2:def 43;

 hence thesis;

 end;



 Lm13: for f be Function of ( Tcircle (( 0. ( TOP-REAL (n + 1))),1)), ( TOP-REAL n) holds f is without_antipodals continuous implies ( Sn1->Sn f) is continuous

 proof

 set T = ( Tcircle (( 0. ( TOP-REAL (n + 1))),1));

 let f be Function of T, ( TOP-REAL n);

 assume that

 A1: f is without_antipodals and

 A2: f is continuous;

 set B = ( Sn1->Sn f);

 reconsider g = (f (-) ) as Function of T, ( TOP-REAL n) by TOPREALC: 61;

 reconsider B1 = (f <--> g) as Function of T, ( TOP-REAL n) by TOPREALC: 40;

 set B2 = ((n NormF ) * B1);



 A3: ( dom g) = the carrier of T by FUNCT_2:def 1;



 A4: ( dom B1) = the carrier of T by FUNCT_2:def 1;

 A5:

 now

 let t be Point of T;



 thus (B2 . t) = ((n NormF ) . (B1 . t)) by FUNCT_2: 15

 .= |.(B1 . t).| by JGRAPH_4:def 1;

 end;

 A6:

 now

 let t be Point of T;



 A7: (B1 . t) = ((f . t) qua real-valued Function - (g . t)) by A4, VALUED_2:def 46

 .= ((f . t) qua real-valued Function - (f . ( - t))) by A3, VALUED_2:def 34;

 ((f . t) - (f . ( - t))) <> ( 0. ( TOP-REAL n)) by A1, Th56;

 hence |.(B1 . t).| <> 0 by A7, TOPRNS_1: 24;

 end;



 A8: B2 is non-empty

 proof

 let x be object;

 assume x in ( dom B2);

 then

 reconsider x as Point of T;

 (B2 . x) = |.(B1 . x).| by A5;

 hence thesis by A6;

 end;



 A9: g is continuous Function of T, ( TOP-REAL n) by A2, TOPREALC: 62;

 (B1 </> B2) is Function of T, ( TOP-REAL n) by TOPREALC: 46;

 hence thesis by A1, Th58, A8, A2, A9, TOPMETR: 6;

 end;

 deffunc BU( Function of ( Tcircle (( 0. ( TOP-REAL (2 + 1))),1)), ( TOP-REAL 2)) = (( Sn1->Sn $1) * ( eLoop 1));



 Lm14: for f be Function of ( Tcircle (( 0. ( TOP-REAL (2 + 1))),1)), ( TOP-REAL 2) holds f is without_antipodals & 0 <= s & s <= (1 / 2) implies ( BU(f) . (s + (1 / 2))) = ( - ( BU(f) . s))

 proof

 let f be Function of ( Tcircle (( 0. ( TOP-REAL (2 + 1))),1)), T2;

 set l = ( eLoop 1);

 set g = ( Sn1->Sn f);

 set t = (s + (1 / 2));

 assume f is without_antipodals;

 then

 A1: g is odd by Th57;

 assume

 A2: 0 <= s & s <= (1 / 2);

 then

 A3: t in I by Lm4;

 reconsider s1 = s as Point of I[01] by A2, Lm3;



 A4: ( dom g) = the carrier of ( Tunit_circle (2 + 1)) by FUNCT_2:def 1;



 A5: ( - (l . s1)) is Point of ( Tcircle (( 0. ( TOP-REAL 3)),1)) by TOPREALC: 60;



 A6: (l . t) = |[( cos (((2 * PI ) * 1) * t)), ( sin (((2 * PI ) * 1) * t)), 0 ]| by A3, Def7

 .= |[( - ( cos ((2 * PI ) * s))), ( sin (((2 * PI ) * s) + PI )), 0 ]| by SIN_COS: 79

 .= |[( - ( cos ((2 * PI ) * s))), ( - ( sin ((2 * PI ) * s))), ( - Q)]| by SIN_COS: 79

 .= ( - |[( cos (((2 * PI ) * 1) * s)), ( sin (((2 * PI ) * 1) * s)), 0 ]|) by EUCLID_5: 11

 .= ( - (l . s1)) by Def7;



 thus ( BU(f) . t) = (g . (l . t)) by A2, Lm4, FUNCT_2: 15

 .= ( - (g . (l . s1))) by A1, A4, A5, A6

 .= ( - ( BU(f) . s1)) by FUNCT_2: 15

 .= ( - ( BU(f) . s));

 end;

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

 Lm15:

 now

 let a,b be Point of R^1 such that

 A1: ( CircleMap . a) = ( - ( CircleMap . b));

 thus ex I be odd Integer st qqI[a, b, I]

 proof



 A2: (CM . a) = |[( cos ((2 * PI ) * a)), ( sin ((2 * PI ) * a))]| & (CM . 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 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);

 thus qqI[a, b, I] by A6;

 end;

 end;



 Lm16: for f be Function of ( Tcircle (( 0. ( TOP-REAL (2 + 1))),1)), ( TOP-REAL 2) holds f is without_antipodals continuous implies BU(f) is nullhomotopic Loop of (( Sn1->Sn f) . c100a)

 proof

 let f be Function of ( Tcircle (( 0. ( TOP-REAL (2 + 1))),1)), ( TOP-REAL 2);

 assume f is without_antipodals continuous;

 then

 reconsider g = ( Sn1->Sn f) as continuous Function of TC3, TC2 by Lm13;

 BU(f) = (g * ( eLoop 1));

 hence thesis;

 end;

 Lm17:

 now

 let f be Function of ( Tcircle (( 0. ( TOP-REAL (2 + 1))),1)), ( TOP-REAL 2);

 let s;

 let xt be set such that

 A1: f is without_antipodals continuous and

 A2: xt in ( CircleMap " {(( Sn1->Sn f) . c[100] )}) and

 A3: 0 <= s & s <= (1 / 2);

 thus ex IT be odd Integer st for L be Loop of (( Sn1->Sn f) . c100a) st L = BU(f) holds (( liftPath (L,xt)) . (s + (1 / 2))) = ((( liftPath (L,xt)) . s) + (IT / 2))

 proof

 reconsider s as Point of I[01] by A3, Lm3;

 reconsider L = BU(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 = t as Point of I[01] by A3, Lm4;



 A4: BU(f) = (CM * l) by A2, Def10;

 ((CM * l) . t1) = (CM . (l . t1)) & ((CM * l) . s) = (CM . (l . s)) by FUNCT_2: 15;

 then (CM . (l . t)) = ( - (CM . (l . s))) by A4, A3, A1, Lm14;

 then

 consider I be odd Integer such that

 A5: qqI[(l . t1), (l . s), I] by Lm15;

 take I;

 thus thesis by A5;

 end;

 end;

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

 Lm18:

 now

 let f be Function of ( Tcircle (( 0. ( TOP-REAL (2 + 1))),1)), ( TOP-REAL 2);

 let xt be set such that

 A1: f is without_antipodals continuous and

 A2: xt in ( CircleMap " {(( Sn1->Sn f) . c[100] )});

 reconsider L1 = BU(f) as Loop of (( Sn1->Sn f) . c100a) by A1, Lm16;

 thus ex I be odd Integer st qqP[f, xt, I]

 proof

 set l1 = ( liftPath (L1,xt));

 set S = [. 0 , (1 / 2).];

 set AF = ( AffineMap (1,(1 / 2)));

 set W = (2 (#) ((l1 * (AF | S)) - l1));

 ( dom AF) = REAL by FUNCT_2:def 1;

 then

 A3: ( dom (AF | S)) = S by RELAT_1: 62;



 A4: ( dom l1) = I by FUNCT_2:def 1;



 A5: ( rng (AF | S)) c= I

 proof

 let y be object;

 assume y in ( rng (AF | S));

 then

 consider x be object such that

 A6: x in ( dom (AF | S)) and

 A7: ((AF | S) . x) = y by FUNCT_1:def 3;

 reconsider x as Real by A6;



 A8: ((AF | S) . x) = (AF . 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 thesis by A7, A8, BORSUK_1: 43;

 end;



 A9: ( dom ((l1 * (AF | S)) - l1)) = (( dom (l1 * (AF | S))) /\ ( dom l1)) by VALUED_1: 12

 .= (( dom (AF | S)) /\ ( dom l1)) by A4, A5, RELAT_1: 27

 .= S by A3, A4, BORSUK_1: 40, XBOOLE_1: 28, XXREAL_1: 34;



 A10: ( dom W) = ( dom ((l1 * (AF | S)) - l1)) by VALUED_1:def 5;

 ( rng W) c= REAL by VALUED_0:def 3;

 then

 reconsider W as PartFunc of REAL , REAL by A9, A10, RELSET_1: 4;

 consider ITj0 be odd Integer such that

 A11: for L be Loop of (( Sn1->Sn f) . c100a) st L = BU(f) holds (( liftPath (L,xt)) . (j0 + (1 / 2))) = ((( liftPath (L,xt)) . j0) + (ITj0 / 2)) by A1, A2, Lm17;

 take ITj0;

 let L be Loop of (( Sn1->Sn f) . c100a) such that

 A12: L = BU(f);

 let s be Real such that

 A13: 0 <= s & s <= (1 / 2);

 set l = ( liftPath (L,xt));



 A14: s in S by A13, XXREAL_1: 1;



 A15: 0 in S by XXREAL_1: 1;



 then

 A16: ((AF | S) . 0 ) = (AF . 0 ) by FUNCT_1: 49

 .= ((1 * Q) + (1 / 2)) by FCONT_1:def 4;



 A17: ((AF | S) . s) = (AF . s) by A14, FUNCT_1: 49

 .= ((1 * s) + (1 / 2)) by FCONT_1:def 4;

 consider ITs be odd Integer such that

 A18: for L be Loop of (( Sn1->Sn f) . c100a) st L = BU(f) holds (( liftPath (L,xt)) . (s + (1 / 2))) = ((( liftPath (L,xt)) . s) + (ITs / 2)) by A1, A2, A13, Lm17;



 A19: (l1 . (j0 + (1 / 2))) = ((l1 . j0) + (ITj0 / 2)) by A11;



 A20: (l1 . (s + (1 / 2))) = ((l1 . s) + (ITs / 2)) by A18;



 A21: (W . 0 ) = (2 * (((l1 * (AF | S)) - l1) . 0 )) by VALUED_1: 6

 .= (2 * (((l1 * (AF | S)) . 0 ) - (l1 . 0 ))) by A9, A15, VALUED_1: 13

 .= (2 * ((l1 . (1 / 2)) - (l1 . 0 ))) by A16, A3, A15, FUNCT_1: 13

 .= (2 * (ITj0 / 2)) by A19;



 A22: (W . s) = (2 * (((l1 * (AF | S)) - l1) . s)) by VALUED_1: 6

 .= (2 * (((l1 * (AF | S)) . s) - (l1 . s))) by A9, A14, VALUED_1: 13

 .= (2 * ((l1 . (s + (1 / 2))) - (l1 . s))) by A17, A3, A14, FUNCT_1: 13

 .= (2 * (ITs / 2)) by A20;



 A23: ( rng W) c= INT

 proof

 let y be object;

 assume y in ( rng W);

 then

 consider s be object such that

 A24: s in ( dom W) and

 A25: (W . s) = y by FUNCT_1:def 3;

 reconsider s as Real by A24;



 A26: ((AF | S) . s) = (AF . s) by A9, A10, A24, FUNCT_1: 49

 .= ((1 * s) + (1 / 2)) by FCONT_1:def 4;

 0 <= s & s <= (1 / 2) by A9, A10, A24, XXREAL_1: 1;

 then

 consider ITs be odd Integer such that

 A27: for L be Loop of (( Sn1->Sn f) . c100a) st L = BU(f) holds (( liftPath (L,xt)) . (s + (1 / 2))) = ((( liftPath (L,xt)) . s) + (ITs / 2)) by A1, A2, Lm17;



 A28: (l1 . (s + (1 / 2))) = ((l1 . s) + (ITs / 2)) by A27;

 (W . s) = (2 * (((l1 * (AF | S)) - l1) . s)) by VALUED_1: 6

 .= (2 * (((l1 * (AF | S)) . s) - (l1 . s))) by A10, A24, VALUED_1: 13

 .= (2 * ((l1 . (s + (1 / 2))) - (l1 . s))) by A26, A3, A9, A10, A24, FUNCT_1: 13

 .= (2 * (ITs / 2)) by A28;

 hence thesis by A25, INT_1:def 2;

 end;

 set T = ( Closed-Interval-TSpace ( 0 ,(1 / 2)));



 A29: the carrier of T = S by TOPMETR: 18;



 A30: ( rng W) c= RAT by A23, NUMBERS: 14;

 reconsider SR = RAT as Subset of R^1 by NUMBERS: 12, TOPMETR: 17;

 reconsider W1 = W as Function of T, ( R^1 | SR) by A10, A9, Lm8, A29, A23, FUNCT_2: 2, NUMBERS: 14, XBOOLE_1: 1;



 A31: T is connected by TREAL_1: 20;



 A32: ( R^1 | ( R^1 ( dom W))) = T by A10, A9, A29, PRE_TOPC: 8, TSEP_1: 5;

 reconsider f1 = ( R^1 (AF | S)) as Function of T, I[01] by A5, A3, A29, FUNCT_2: 2;

 ( rng l1) c= REAL by TOPMETR: 17;

 then

 reconsider ll1 = l1 as PartFunc of REAL , REAL by A4, BORSUK_1: 40, RELSET_1: 4;

 l1 is continuous by A2, Def10;

 then

 A33: ll1 is continuous by Th29, TOPMETR: 20;

 ((ll1 * (AF | S)) - ll1) is continuous by A33;

 then

 reconsider W as continuous PartFunc of REAL , REAL ;

 the carrier of ( R^1 | ( R^1 ( rng W))) = ( rng W) by PRE_TOPC: 8;

 then

 A34: ( R^1 | ( R^1 ( rng W))) is SubSpace of RR by A30, Lm8, TSEP_1: 4;

 ( R^1 W) is continuous;

 then W1 is continuous by A32, A34, PRE_TOPC: 26;

 then W1 is constant by A31, Th28;

 hence thesis by A20, A12, A21, A22, A9, A10, A15, A14;

 end;

 end;



 Lm19: for f be Function of ( Tcircle (( 0. ( TOP-REAL (2 + 1))),1)), ( TOP-REAL 2) holds for xt be Point of R^1 holds for L be Loop of (( Sn1->Sn f) . c100a) st L = BU(f) holds for I be Integer st qqP[f, xt, I] holds (( liftPath (L,xt)) . 1) = ((( liftPath (L,xt)) . 0 ) + I)

 proof

 let f be Function of ( Tcircle (( 0. ( TOP-REAL (2 + 1))),1)), ( TOP-REAL 2);

 let xt be Point of R^1 ;

 let L be Loop of (( Sn1->Sn f) . c100a) such that

 A1: L = BU(f);

 let I be Integer such that

 A2: qqP[f, xt, I];

 set l = ( liftPath (L,xt));

 ((1 / 2) + (1 / 2)) = 1;



 hence (l . 1) = ((l . (Q + (1 / 2))) + (I / 2)) by A1, A2

 .= (((l . 0 ) + (I / 2)) + (I / 2)) by A1, A2

 .= ((l . 0 ) + I);

 end;



 Lm20: for f be Function of ( Tcircle (( 0. ( TOP-REAL (2 + 1))),1)), ( TOP-REAL 2) holds f is without_antipodals continuous implies not BU(f) is nullhomotopic Loop of (( Sn1->Sn f) . c100a)

 proof

 let f be Function of ( Tcircle (( 0. ( TOP-REAL (2 + 1))),1)), ( TOP-REAL 2);

 assume

 A1: f is without_antipodals continuous;

 then

 reconsider L = BU(f) as Loop of (( Sn1->Sn f) . c100a) by Lm16;

 set g = ( Sn1->Sn f);

 set s = (g . c100a);

 not L is nullhomotopic

 proof

 let c be constant Loop of s;

 ( rng CM) = the carrier of TC2 by FUNCT_2:def 3;

 then

 consider xt be object such that

 A2: xt in R and

 A3: (CM . xt) = s by FUNCT_2: 11;

 reconsider xt as Point of R^1 by A2;

 s in {s} by TARSKI:def 1;

 then

 A4: xt in (CM " {s}) by A3, FUNCT_2: 38;

 then

 consider q be odd Integer such that

 A5: qqP[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: (CM . q) = c[10] by TOPREALB: 32;



 A8: (CM . 0 ) = c[10] by TOPREALB: 32;

 set hh = (l - xt);

 hh is Path of ( R^1 0 ), ( R^1 q)

 proof

 thus hh is continuous;



 thus (hh . 0 ) = ((l . j0) - xt) by VALUED_1: 4

 .= (xt - xt) by A4, Def10

 .= ( R^1 0 );



 thus (hh . 1) = ((l . j1) - xt) by VALUED_1: 4

 .= ((xt + q) - xt) by A6, A4, Def10

 .= ( R^1 q);

 end;

 then

 reconsider hh as Path of ( R^1 0 ), ( R^1 q);

 reconsider Ch = (CM * 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 = (CM * xx) 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 (TC2, c[10] )),(CM * hh))) by TOPALG_5: 25;



 A11: ( Ciso . 0 ) = ( Class (( EqRel (TC2, c[10] )),(CM * xx))) 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 ;

 then

 consider F be Function of [: I[01] , I[01] :], TC2 such that

 A13: F is continuous and

 A14: for t be Point of I[01] holds (F . (t, 0 )) = ( BU(f) . t) & (F . (t,1)) = (c . t) & (F . ( 0 ,t)) = s & (F . (1,t)) = s;

 reconsider S = s as Point of T2 by PRE_TOPC: 25;

 set A = ( - ( Arg S));

 set H = ( RotateCircle (1,A));

 set G = (H * F);



 A15: |.( euc2cpx S).| = |.S.| by EUCLID_3: 25

 .= 1 by TOPREALB: 12;



 A16: ( Rotate (( euc2cpx S),A)) = |.( euc2cpx S).| by COMPLEX2: 55;



 A17: (H . s) = (( Rotate A) . S) by FUNCT_1: 49

 .= c[10] by A16, A15, COMPLEX1: 6, JORDAN24:def 3;

 now

 let t be Point of I[01] ;

 reconsider E = ( eLoop 1) as Function of I[01] , ( Tunit_circle (2 + 1));

 reconsider BU = BU(f) as Function of I[01] , ( Tunit_circle 2);

 reconsider T = (BU . t) as Point of T2 by PRE_TOPC: 25;

 BU(f) = (CM * l) by A4, Def10;

 then

 A18: ( BU(f) . t) = (CM . (l . t)) by FUNCT_2: 15;



 thus (G . (t, 0 )) = (H . (F . (t,j0))) by Lm1, BINOP_1: 18

 .= (H . T) by A14

 .= (CM . ((l . t) - xt)) by A3, A18, Th50

 .= (CM . (hh . t)) by VALUED_1: 4

 .= (Ch . t) by FUNCT_2: 15;



 thus (G . (t,1)) = (H . (F . (t,j1))) by Lm1, BINOP_1: 18

 .= (H . (c . t)) by A14

 .= (H . s) by TOPALG_3: 21

 .= (CM . (xt - xt)) by A17, TOPREALB: 32

 .= (CM . ((X . t) - xt))

 .= (CM . (xx . t)) by VALUED_1: 4

 .= (Cx . t) by FUNCT_2: 15;



 thus (G . ( 0 ,t)) = (H . (F . (j0,t))) by Lm1, BINOP_1: 18

 .= c[10] by A14, A17;



 thus (G . (1,t)) = (H . (F . (j1,t))) by Lm1, BINOP_1: 18

 .= c[10] by A14, A17;

 end;

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

 end;

 hence thesis;

 end;



 Lm21: for f be continuous Function of ( Tcircle (( 0. ( TOP-REAL (2 + 1))),1)), ( TOP-REAL 2) holds f is with_antipodals

 proof

 let f be continuous Function of ( Tcircle (( 0. ( TOP-REAL (2 + 1))),1)), T2;

 assume

 A1: not thesis;

 then not BU(f) is nullhomotopic Loop of (( Sn1->Sn f) . c100a) by Lm20;

 hence contradiction by A1, Lm16;

 end;

 registration

 let n;

 let r be negative Real, p be Point of ( TOP-REAL (n + 1));

 cluster -> without_antipodals for Function of ( Tcircle (p,r)), ( TOP-REAL n);

 coherence

 proof

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

 let x,y be Point of ( TOP-REAL (n + 1));

 thus not (x,y) are_antipodals_of (p,r,f);

 end;

 end

 ::$Notion-Name

 registration

 let r be non negative Real, p be Point of ( TOP-REAL 3);

 cluster continuous -> with_antipodals for Function of ( Tcircle (p,r)), ( TOP-REAL 2);

 coherence

 proof

 let f be Function of ( Tcircle (p,r)), T2;

 assume

 A1: f is continuous;



 A2: ( dom f) = the carrier of ( Tcircle (p,r)) by FUNCT_2:def 1;

 per cases ;

 suppose r is positive;

 then

 reconsider r1 = r as positive Real;

 reconsider f1 = f as continuous Function of ( Tcircle (p,r1)), T2 by A1;

 reconsider h = ( CircleIso (p,r1)) as Function of ( Tcircle (( 0. ( TOP-REAL 3)),1)), ( Tcircle (p,r1));

 (f1 * h) is with_antipodals by Lm21;

 then

 consider x,y be Point of ( TOP-REAL 3) such that

 A3: (x,y) are_antipodals_of (( 0. ( TOP-REAL 3)),1,(f1 * h));



 A4: x in ( dom (f * h)) by A3;



 A5: y in ( dom (f * h)) by A3;



 A6: ((f * h) . x) = ((f * h) . y) by A3;

 (h . x) is Point of ( Tcircle (p,r1)) & (h . y) is Point of ( Tcircle (p,r1)) by A4, A5, FUNCT_2: 5;

 then

 reconsider hx = (h . x), hy = (h . y) as Point of ( TOP-REAL 3) by PRE_TOPC: 25;

 take hx, hy;

 (x,y) are_antipodals_of (( 0. ( TOP-REAL 3)),1) by A3;

 hence (hx,hy) are_antipodals_of (p,r) by Th55;

 thus hx in ( dom f) by A2, A4, FUNCT_2: 5;

 thus hy in ( dom f) by A2, A5, FUNCT_2: 5;



 thus (f . hx) = ((f * h) . x) by A4, FUNCT_2: 15

 .= (f . hy) by A5, A6, FUNCT_2: 15;

 end;

 suppose

 A7: r is zero;

 take p, p;

 reconsider e = p as Point of ( Euclid 3) by TOPREAL3: 8;



 A8: the carrier of ( Tcircle (p,r)) = ( Sphere (p,r)) by TOPREALB: 9

 .= ( Sphere (e,r)) by TOPREAL9: 15

 .= {e} by A7, TOPREAL6: 54;

 thus (p,p) are_antipodals_of (p,r) by A8, TARSKI:def 1, RLTOPSP1: 68;

 thus p in ( dom f) & p in ( dom f) by A2, A8, TARSKI:def 1;

 thus (f . p) = (f . p);

 end;

 end;

 end