:: BORSUK_7 semantic presentation begin 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 [.0,1.[; 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: the carrier of [:I[01],I[01]:] = [: the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def_2; Lm2: 0 in {0} by TARSKI:def_1; Lm3: now__::_thesis:_for_s_being_real_number_st_s_<=_1_/_2_&_0_<=_s_holds_ s_in_the_carrier_of_I[01] let s be real number ; ::_thesis: ( s <= 1 / 2 & 0 <= s implies s in the carrier of I[01] ) assume s <= 1 / 2 ; ::_thesis: ( 0 <= s implies s in the carrier of I[01] ) then s <= 1 by XXREAL_0:2; hence ( 0 <= s implies s in the carrier of I[01] ) by BORSUK_1:43; ::_thesis: verum end; Lm4: now__::_thesis:_for_s_being_real_number_st_0_<=_s_&_s_<=_1_/_2_holds_ s_+_(1_/_2)_in_the_carrier_of_I[01] let s be real number ; ::_thesis: ( 0 <= s & s <= 1 / 2 implies s + (1 / 2) in the carrier of I[01] ) set t = s + (1 / 2); assume ( 0 <= s & s <= 1 / 2 ) ; ::_thesis: s + (1 / 2) in the carrier of I[01] then ( Q + (1 / 2) <= s + (1 / 2) & s + (1 / 2) <= (1 / 2) + (1 / 2) ) by XREAL_1:6; hence s + (1 / 2) in the carrier of I[01] by BORSUK_1:43; ::_thesis: verum end; registration cluster -> irrational for Element of IRRAT ; coherence for b1 being Element of IRRAT holds b1 is irrational by BORSUK_5:17; end; theorem Th1: :: BORSUK_7:1 for r, s being real number st 0 <= r & 0 <= s & r ^2 = s ^2 holds r = s proof let r, s be real number ; ::_thesis: ( 0 <= r & 0 <= s & r ^2 = s ^2 implies r = s ) assume that A1: 0 <= r and A2: 0 <= s and A3: r ^2 = s ^2 and A4: r <> s ; ::_thesis: contradiction - Q >= - (- s) by A1, A3, A4, SQUARE_1:40; hence contradiction by A4, A2, A3, SQUARE_1:40; ::_thesis: verum end; theorem Th2: :: BORSUK_7:2 for r, s being real number st frac r >= frac s holds frac (r - s) = (frac r) - (frac s) proof let r, s be real number ; ::_thesis: ( frac r >= frac s implies frac (r - s) = (frac r) - (frac s) ) assume A1: frac r >= frac s ; ::_thesis: frac (r - s) = (frac r) - (frac s) set a = ((r - s) - (frac r)) + (frac s); A2: ((r - s) - (frac r)) + (frac s) = (r - (frac r)) - (s - (frac s)) ; A3: ((r - s) - (frac r)) + (frac s) = (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: ((r - s) - (frac r)) + (frac s) <= (r - s) + Q by A3, XREAL_1:6; A5: ((r - s) - (frac r)) + (frac s) = (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 < ((r - s) - (frac r)) + (frac s) by A5, XREAL_1:10; then ((r - s) - (frac r)) + (frac s) = [\(r - s)/] by A4, A2, INT_1:def_6; hence frac (r - s) = (frac r) - (frac s) ; ::_thesis: verum end; theorem Th3: :: BORSUK_7:3 for r, s being real number st frac r < frac s holds frac (r - s) = ((frac r) - (frac s)) + 1 proof let r, s be real number ; ::_thesis: ( frac r < frac s implies frac (r - s) = ((frac r) - (frac s)) + 1 ) assume A1: frac r < frac s ; ::_thesis: frac (r - s) = ((frac r) - (frac s)) + 1 set a = (((r - s) - (frac r)) + (frac s)) - 1; A2: (((r - s) - (frac r)) + (frac s)) - 1 = ((r - (frac r)) - (s - (frac s))) - 1 ; A3: (((r - s) - (frac r)) + (frac s)) - 1 = (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: (((r - s) - (frac r)) + (frac s)) - 1 = ((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 < (((r - s) - (frac r)) + (frac s)) - 1 by A6, XREAL_1:10; then (((r - s) - (frac r)) + (frac s)) - 1 = [\(r - s)/] by A5, A2, INT_1:def_6; hence frac (r - s) = ((frac r) - (frac s)) + 1 ; ::_thesis: verum end; theorem Th4: :: BORSUK_7:4 for r, s being real number ex i being Integer st ( frac (r - s) = ((frac r) - (frac s)) + i & ( i = 0 or i = 1 ) ) proof let r, s be real number ; ::_thesis: ex i being Integer st ( frac (r - s) = ((frac r) - (frac s)) + i & ( i = 0 or i = 1 ) ) ( frac (r - s) = ((frac r) - (frac s)) + Q or frac (r - s) = ((frac r) - (frac s)) + 1 ) by Th2, Th3; hence ex i being Integer st ( frac (r - s) = ((frac r) - (frac s)) + i & ( i = 0 or i = 1 ) ) ; ::_thesis: verum end; theorem Th5: :: BORSUK_7:5 for r being real number holds ( not sin r = 0 or r = (2 * PI) * [\(r / (2 * PI))/] or r = PI + ((2 * PI) * [\(r / (2 * PI))/]) ) proof let r be real number ; ::_thesis: ( not sin r = 0 or r = (2 * PI) * [\(r / (2 * PI))/] or r = PI + ((2 * PI) * [\(r / (2 * PI))/]) ) set i = [\(r / (2 * PI))/]; assume A1: sin r = 0 ; ::_thesis: ( r = (2 * PI) * [\(r / (2 * PI))/] or r = PI + ((2 * PI) * [\(r / (2 * PI))/]) ) consider w being real number such that A2: w = ((2 * PI) * (- [\(r / (2 * PI))/])) + 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 ( r = (2 * PI) * [\(r / (2 * PI))/] or r = PI + ((2 * PI) * [\(r / (2 * PI))/]) ) by A2; ::_thesis: verum end; theorem Th6: :: BORSUK_7:6 for r being real number holds ( not cos r = 0 or r = (PI / 2) + ((2 * PI) * [\(r / (2 * PI))/]) or r = ((3 * PI) / 2) + ((2 * PI) * [\(r / (2 * PI))/]) ) proof let r be real number ; ::_thesis: ( not cos r = 0 or r = (PI / 2) + ((2 * PI) * [\(r / (2 * PI))/]) or r = ((3 * PI) / 2) + ((2 * PI) * [\(r / (2 * PI))/]) ) set i = [\(r / (2 * PI))/]; assume A1: cos r = 0 ; ::_thesis: ( r = (PI / 2) + ((2 * PI) * [\(r / (2 * PI))/]) or r = ((3 * PI) / 2) + ((2 * PI) * [\(r / (2 * PI))/]) ) consider w being real number such that A2: w = ((2 * PI) * (- [\(r / (2 * PI))/])) + 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 ( r = (PI / 2) + ((2 * PI) * [\(r / (2 * PI))/]) or r = ((3 * PI) / 2) + ((2 * PI) * [\(r / (2 * PI))/]) ) by A2; ::_thesis: verum end; theorem Th7: :: BORSUK_7:7 for r being real number st sin r = 0 holds ex i being Integer st r = PI * i proof let r be real number ; ::_thesis: ( sin r = 0 implies ex i being Integer st r = PI * i ) assume sin r = 0 ; ::_thesis: ex i being Integer st r = PI * i 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 ex i being Integer st r = PI * i ; ::_thesis: verum end; theorem Th8: :: BORSUK_7:8 for r being real number st cos r = 0 holds ex i being Integer st r = (PI / 2) + (PI * i) proof let r be real number ; ::_thesis: ( cos r = 0 implies ex i being Integer st r = (PI / 2) + (PI * i) ) assume cos r = 0 ; ::_thesis: ex i being Integer st r = (PI / 2) + (PI * i) 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 ex i being Integer st r = (PI / 2) + (PI * i) ; ::_thesis: verum end; Lm5: now__::_thesis:_for_r,_s_being_real_number_st_sin_((r_-_s)_/_2)_=_0_holds_ ex_i_being_Integer_st_r_=_s_+_((2_*_PI)_*_i) let r, s be real number ; ::_thesis: ( sin ((r - s) / 2) = 0 implies ex i being Integer st r = s + ((2 * PI) * i) ) assume sin ((r - s) / 2) = 0 ; ::_thesis: ex i being Integer st r = s + ((2 * PI) * i) then consider i being Integer such that A1: (r - s) / 2 = PI * i by Th7; r = s + ((2 * PI) * i) by A1; hence ex i being Integer st r = s + ((2 * PI) * i) ; ::_thesis: verum end; theorem Th9: :: BORSUK_7:9 for r, s being real number st sin r = sin s holds ex i being Integer st ( r = s + ((2 * PI) * i) or r = (PI - s) + ((2 * PI) * i) ) proof let r, s be real number ; ::_thesis: ( sin r = sin s implies ex i being Integer st ( r = s + ((2 * PI) * i) or r = (PI - s) + ((2 * PI) * i) ) ) assume A1: sin r = sin s ; ::_thesis: ex i being Integer st ( r = s + ((2 * PI) * i) or r = (PI - s) + ((2 * PI) * i) ) A2: (sin r) - (sin s) = 2 * ((cos ((r + s) / 2)) * (sin ((r - s) / 2))) by SIN_COS4:16; percases ( sin ((r - s) / 2) = 0 or cos ((r + s) / 2) = 0 ) by A1, A2; suppose sin ((r - s) / 2) = 0 ; ::_thesis: ex i being Integer st ( r = s + ((2 * PI) * i) or r = (PI - s) + ((2 * PI) * i) ) hence ex i being Integer st ( r = s + ((2 * PI) * i) or r = (PI - s) + ((2 * PI) * i) ) by Lm5; ::_thesis: verum end; suppose cos ((r + s) / 2) = 0 ; ::_thesis: ex i being Integer st ( r = s + ((2 * PI) * i) or r = (PI - s) + ((2 * PI) * i) ) then consider i being Integer such that A3: (r + s) / 2 = (PI / 2) + (PI * i) by Th8; r = (PI - s) + ((2 * PI) * i) by A3; hence ex i being Integer st ( r = s + ((2 * PI) * i) or r = (PI - s) + ((2 * PI) * i) ) ; ::_thesis: verum end; end; end; theorem Th10: :: BORSUK_7:10 for r, s being real number st cos r = cos s holds ex i being Integer st ( r = s + ((2 * PI) * i) or r = (- s) + ((2 * PI) * i) ) proof let r, s be real number ; ::_thesis: ( cos r = cos s implies ex i being Integer st ( r = s + ((2 * PI) * i) or r = (- s) + ((2 * PI) * i) ) ) assume A1: cos r = cos s ; ::_thesis: ex i being Integer st ( r = s + ((2 * PI) * i) or r = (- s) + ((2 * PI) * i) ) A2: (cos r) - (cos s) = - (2 * ((sin ((r + s) / 2)) * (sin ((r - s) / 2)))) by SIN_COS4:18; percases ( sin ((r - s) / 2) = 0 or sin ((r + s) / 2) = 0 ) by A1, A2; suppose sin ((r - s) / 2) = 0 ; ::_thesis: ex i being Integer st ( r = s + ((2 * PI) * i) or r = (- s) + ((2 * PI) * i) ) hence ex i being Integer st ( r = s + ((2 * PI) * i) or r = (- s) + ((2 * PI) * i) ) by Lm5; ::_thesis: verum end; suppose sin ((r + s) / 2) = 0 ; ::_thesis: ex i being Integer st ( r = s + ((2 * PI) * i) or r = (- s) + ((2 * PI) * i) ) then consider i being Integer such that A3: (r + s) / 2 = PI * i by Th7; (r + s) - s = ((2 * PI) * i) - s by A3; hence ex i being Integer st ( r = s + ((2 * PI) * i) or r = (- s) + ((2 * PI) * i) ) ; ::_thesis: verum end; end; end; theorem Th11: :: BORSUK_7:11 for r, s being real number st sin r = sin s & cos r = cos s holds ex i being Integer st r = s + ((2 * PI) * i) proof let r, s be real number ; ::_thesis: ( sin r = sin s & cos r = cos s implies ex i being Integer st r = s + ((2 * PI) * i) ) assume that A1: sin r = sin s and A2: cos r = cos s ; ::_thesis: ex i being Integer st r = s + ((2 * PI) * i) consider i being Integer such that A3: ( r = s + ((2 * PI) * i) or r = (PI - s) + ((2 * PI) * i) ) by A1, Th9; consider j being Integer such that A4: ( r = s + ((2 * PI) * j) or r = (- s) + ((2 * PI) * j) ) by A2, Th10; percases ( r = s + ((2 * PI) * i) or r = s + ((2 * PI) * j) or ( r = (PI - s) + ((2 * PI) * i) & r = (- s) + ((2 * PI) * j) ) ) by A3, A4; suppose ( r = s + ((2 * PI) * i) or r = s + ((2 * PI) * j) ) ; ::_thesis: ex i being Integer st r = s + ((2 * PI) * i) hence ex i being Integer st r = s + ((2 * PI) * i) ; ::_thesis: verum end; suppose ( r = (PI - s) + ((2 * PI) * i) & r = (- s) + ((2 * PI) * j) ) ; ::_thesis: ex i being Integer st r = s + ((2 * PI) * i) 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 ex i being Integer st r = s + ((2 * PI) * i) by NAT_D:33; ::_thesis: verum end; end; end; theorem Th12: :: BORSUK_7:12 for i being Integer for c1, c2 being complex number st |.c1.| = |.c2.| & Arg c1 = (Arg c2) + ((2 * PI) * i) holds c1 = c2 proof let i be Integer; ::_thesis: for c1, c2 being complex number st |.c1.| = |.c2.| & Arg c1 = (Arg c2) + ((2 * PI) * i) holds c1 = c2 let c1, c2 be complex number ; ::_thesis: ( |.c1.| = |.c2.| & Arg c1 = (Arg c2) + ((2 * PI) * i) implies c1 = c2 ) assume A1: ( |.c1.| = |.c2.| & Arg c1 = (Arg c2) + ((2 * PI) * i) ) ; ::_thesis: c1 = c2 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; ::_thesis: verum end; registration let f be one-to-one complex-valued Function; let c be complex number ; clusterc + f -> one-to-one ; coherence f + c is one-to-one proof let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x in dom (f + c) or not b1 in dom (f + c) or not (f + c) . x = (f + c) . b1 or x = b1 ) let y be set ; ::_thesis: ( not x in dom (f + c) or not y in dom (f + c) or not (f + c) . x = (f + c) . y or x = y ) assume that A1: ( x in dom (f + c) & y in dom (f + c) ) and A2: (f + c) . x = (f + c) . y ; ::_thesis: x = 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 x = y by A1, A3, A2, FUNCT_1:def_4; ::_thesis: verum end; end; registration let f be one-to-one complex-valued Function; let c be complex number ; clusterf - c -> one-to-one ; coherence f - c is one-to-one ; end; theorem Th13: :: BORSUK_7:13 for f being complex-valued FinSequence holds len (- f) = len f proof let f be complex-valued FinSequence; ::_thesis: len (- f) = len f Seg (len (- f)) = dom (- f) by FINSEQ_1:def_3 .= dom f by VALUED_1:def_5 .= Seg (len f) by FINSEQ_1:def_3 ; hence len (- f) = len f by FINSEQ_1:6; ::_thesis: verum end; theorem Th14: :: BORSUK_7:14 for n being Nat holds - (0* n) = 0* n proof let n be Nat; ::_thesis: - (0* n) = 0* n set f = 0* n; set g = - (0* n); thus len (0* n) = len (- (0* n)) by Th13; :: according to FINSEQ_1:def_17 ::_thesis: for b1 being set holds ( not 1 <= b1 or not b1 <= len (- (0* n)) or (- (0* n)) . b1 = (0* n) . b1 ) let k be Nat; ::_thesis: ( not 1 <= k or not k <= len (- (0* n)) or (- (0* n)) . k = (0* n) . k ) assume ( 1 <= k & k <= len (- (0* n)) ) ; ::_thesis: (- (0* n)) . k = (0* n) . k A1: (0* n) . k = 0 ; thus (0* n) . k = - Q .= (- (0* n)) . k by A1, VALUED_1:8 ; ::_thesis: verum end; theorem Th15: :: BORSUK_7:15 for n being Nat for f being complex-valued Function st f <> 0* n holds - f <> 0* n proof let n be Nat; ::_thesis: for f being complex-valued Function st f <> 0* n holds - f <> 0* n let f be complex-valued Function; ::_thesis: ( f <> 0* n implies - f <> 0* n ) assume A1: f <> 0* n ; ::_thesis: - f <> 0* n assume - f = 0* n ; ::_thesis: contradiction then - (- f) = - (0* n) ; hence contradiction by A1, Th14; ::_thesis: verum end; theorem Th16: :: BORSUK_7:16 for r1, r2, r3 being real number holds sqr <*r1,r2,r3*> = <*(r1 ^2),(r2 ^2),(r3 ^2)*> proof let r1, r2, r3 be real number ; ::_thesis: sqr <*r1,r2,r3*> = <*(r1 ^2),(r2 ^2),(r3 ^2)*> A1: ( r1 in REAL & r2 in REAL & r3 in REAL ) by XREAL_0:def_1; ( <*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 A1, TOPREAL6:11 .= <*(r1 ^2),(r2 ^2),(r3 ^2)*> by RVSUM_1:55 ; ::_thesis: verum end; theorem Th17: :: BORSUK_7:17 for r1, r2, r3 being real number holds Sum (sqr <*r1,r2,r3*>) = ((r1 ^2) + (r2 ^2)) + (r3 ^2) proof let r1, r2, r3 be real number ; ::_thesis: Sum (sqr <*r1,r2,r3*>) = ((r1 ^2) + (r2 ^2)) + (r3 ^2) thus Sum (sqr <*r1,r2,r3*>) = Sum <*(r1 ^2),(r2 ^2),(r3 ^2)*> by Th16 .= ((r1 ^2) + (r2 ^2)) + (r3 ^2) by RVSUM_1:78 ; ::_thesis: verum end; theorem Th18: :: BORSUK_7:18 for c being complex number for f being complex-valued FinSequence holds (c (#) f) ^2 = (c ^2) (#) (f ^2) proof let c be complex number ; ::_thesis: for f being complex-valued FinSequence holds (c (#) f) ^2 = (c ^2) (#) (f ^2) let f be complex-valued FinSequence; ::_thesis: (c (#) f) ^2 = (c ^2) (#) (f ^2) 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__::_thesis:_for_x_being_set_st_x_in_dom_((c_(#)_f)_^2)_holds_ ((c_(#)_f)_^2)_._x_=_((c_^2)_(#)_(f_^2))_._x let x be set ; ::_thesis: ( x in dom ((c (#) f) ^2) implies ((c (#) f) ^2) . x = ((c ^2) (#) (f ^2)) . x ) assume x in dom ((c (#) f) ^2) ; ::_thesis: ((c (#) f) ^2) . x = ((c ^2) (#) (f ^2)) . x 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 ; ::_thesis: verum end; hence (c (#) f) ^2 = (c ^2) (#) (f ^2) by A1, A2, FUNCT_1:2; ::_thesis: verum end; theorem Th19: :: BORSUK_7:19 for c being complex number for f being complex-valued FinSequence holds (f (/) c) ^2 = (f ^2) (/) (c ^2) proof let c be complex number ; ::_thesis: for f being complex-valued FinSequence holds (f (/) c) ^2 = (f ^2) (/) (c ^2) let f be complex-valued FinSequence; ::_thesis: (f (/) c) ^2 = (f ^2) (/) (c ^2) thus (f (/) c) ^2 = ((1 / c) ^2) (#) (f ^2) by Th18 .= ((1 * 1) / (c * c)) (#) (f ^2) by XCMPLX_1:76 .= (f ^2) (/) (c ^2) ; ::_thesis: verum end; theorem Th20: :: BORSUK_7:20 for f being real-valued FinSequence st Sum f <> 0 holds Sum (f (/) (Sum f)) = 1 proof let f be real-valued FinSequence; ::_thesis: ( Sum f <> 0 implies Sum (f (/) (Sum f)) = 1 ) Sum (f (/) (Sum f)) = (Sum f) / (Sum f) by RVSUM_1:87; hence ( Sum f <> 0 implies Sum (f (/) (Sum f)) = 1 ) by XCMPLX_1:60; ::_thesis: verum end; Lm6: 1,2,3 are_mutually_different proof thus ( 1 <> 2 & 1 <> 3 & 2 <> 3 ) ; :: according to ZFMISC_1:def_5 ::_thesis: verum end; definition let a, b, c, x, y, z be set ; func(a,b,c) --> (x,y,z) -> set equals :: BORSUK_7:def 1 ((a,b) --> (x,y)) +* (c .--> z); coherence ((a,b) --> (x,y)) +* (c .--> z) is set ; end; :: deftheorem defines --> BORSUK_7:def_1_:_ for a, b, c, x, y, z being set holds (a,b,c) --> (x,y,z) = ((a,b) --> (x,y)) +* (c .--> z); registration let a, b, c, x, y, z be set ; cluster(a,b,c) --> (x,y,z) -> Relation-like Function-like ; coherence ( (a,b,c) --> (x,y,z) is Function-like & (a,b,c) --> (x,y,z) is Relation-like ) ; end; theorem :: BORSUK_7:21 for a, b, x, y, z being set for c being complex number holds dom ((a,b,c) --> (x,y,z)) = {a,b,c} by BVFUNC14:11; theorem :: BORSUK_7:22 for a, b, x, y, z being set for c being complex number holds rng ((a,b,c) --> (x,y,z)) c= {x,y,z} proof let a, b, x, y, z be set ; ::_thesis: for c being complex number holds rng ((a,b,c) --> (x,y,z)) c= {x,y,z} let c be complex number ; ::_thesis: rng ((a,b,c) --> (x,y,z)) c= {x,y,z} A1: {x,y} \/ {z} = {x,y,z} by ENUMSET1:3; A2: rng ((a,b,c) --> (x,y,z)) c= (rng ((a,b) --> (x,y))) \/ (rng (c .--> z)) by FUNCT_4:17; A3: rng (c .--> z) = {z} by FUNCOP_1:8; rng ((a,b) --> (x,y)) c= {x,y} by FUNCT_4:62; then (rng ((a,b) --> (x,y))) \/ (rng (c .--> z)) c= {x,y} \/ {z} by A3, XBOOLE_1:13; hence rng ((a,b,c) --> (x,y,z)) c= {x,y,z} by A2, A1, XBOOLE_1:1; ::_thesis: verum end; theorem :: BORSUK_7:23 for a, x, y, z being set holds (a,a,a) --> (x,y,z) = a .--> z proof let a, x, y, z be set ; ::_thesis: (a,a,a) --> (x,y,z) = a .--> z thus (a,a,a) --> (x,y,z) = (a,a) --> (y,z) by FUNCT_4:81 .= a .--> z by FUNCT_4:81 ; ::_thesis: verum end; theorem :: BORSUK_7:24 for a, b, x, y, z being set holds (a,a,b) --> (x,y,z) = (a,b) --> (y,z) by FUNCT_4:81; theorem Th25: :: BORSUK_7:25 for a, b, x, y, z being set st a <> b holds (a,b,a) --> (x,y,z) = (a,b) --> (z,y) proof let a, b, x, y, z be set ; ::_thesis: ( a <> b implies (a,b,a) --> (x,y,z) = (a,b) --> (z,y) ) assume A1: a <> b ; ::_thesis: (a,b,a) --> (x,y,z) = (a,b) --> (z,y) A2: dom ((a,b,a) --> (x,y,z)) = {a,b,a} by BVFUNC14:11 .= {a,a,b} by ENUMSET1:57 .= {a,b} by ENUMSET1:30 ; hence dom ((a,b,a) --> (x,y,z)) = dom ((a,b) --> (z,y)) by FUNCT_4:62; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds ( not b1 in dom ((a,b,a) --> (x,y,z)) or ((a,b,a) --> (x,y,z)) . b1 = ((a,b) --> (z,y)) . b1 ) let k be set ; ::_thesis: ( not k in dom ((a,b,a) --> (x,y,z)) or ((a,b,a) --> (x,y,z)) . k = ((a,b) --> (z,y)) . k ) assume A3: k in dom ((a,b,a) --> (x,y,z)) ; ::_thesis: ((a,b,a) --> (x,y,z)) . k = ((a,b) --> (z,y)) . k percases ( k = a or k = b ) by A2, A3, TARSKI:def_2; supposeA4: k = a ; ::_thesis: ((a,b,a) --> (x,y,z)) . k = ((a,b) --> (z,y)) . k hence ((a,b,a) --> (x,y,z)) . k = z by FUNCT_4:89 .= ((a,b) --> (z,y)) . k by A1, A4, FUNCT_4:63 ; ::_thesis: verum end; supposeA5: k = b ; ::_thesis: ((a,b,a) --> (x,y,z)) . k = ((a,b) --> (z,y)) . k thus ((a,b,a) --> (x,y,z)) . k = ((a .--> x) +* ((b,a) --> (y,z))) . k by FUNCT_4:14 .= y by A1, A5, FUNCT_4:84 .= ((a,b) --> (z,y)) . k by A5, FUNCT_4:63 ; ::_thesis: verum end; end; end; theorem Th26: :: BORSUK_7:26 for a, b, x, y, z being set holds (a,b,b) --> (x,y,z) = (a,b) --> (x,z) proof let a, b, x, y, z be set ; ::_thesis: (a,b,b) --> (x,y,z) = (a,b) --> (x,z) thus (a,b,b) --> (x,y,z) = (a .--> x) +* ((b,b) --> (y,z)) by FUNCT_4:14 .= (a,b) --> (x,z) by FUNCT_4:81 ; ::_thesis: verum end; theorem :: BORSUK_7:27 for a, b, x, y, z being set for c being complex number st a <> b & a <> c holds ((a,b,c) --> (x,y,z)) . a = x by BVFUNC14:13; theorem Th28: :: BORSUK_7:28 for a, b, x, y, z being set for c being complex number st a,b,c are_mutually_different holds ( ((a,b,c) --> (x,y,z)) . a = x & ((a,b,c) --> (x,y,z)) . b = y & ((a,b,c) --> (x,y,z)) . c = z ) proof let a, b, x, y, z be set ; ::_thesis: for c being complex number st a,b,c are_mutually_different holds ( ((a,b,c) --> (x,y,z)) . a = x & ((a,b,c) --> (x,y,z)) . b = y & ((a,b,c) --> (x,y,z)) . c = z ) let c be complex number ; ::_thesis: ( a,b,c are_mutually_different implies ( ((a,b,c) --> (x,y,z)) . a = x & ((a,b,c) --> (x,y,z)) . b = y & ((a,b,c) --> (x,y,z)) . c = z ) ) assume A1: a,b,c are_mutually_different ; ::_thesis: ( ((a,b,c) --> (x,y,z)) . a = x & ((a,b,c) --> (x,y,z)) . b = y & ((a,b,c) --> (x,y,z)) . c = z ) set f = (a,b) --> (x,y); set g = c .--> z; set h = (a,b,c) --> (x,y,z); A2: a <> b by A1, ZFMISC_1:def_5; a <> c by A1, ZFMISC_1:def_5; then A3: not a in {c} by TARSKI:def_1; b <> c by A1, ZFMISC_1:def_5; then A4: not b in {c} by TARSKI:def_1; A5: c in {c} by TARSKI:def_1; A6: dom (c .--> z) = {c} by FUNCOP_1:13; hence ((a,b,c) --> (x,y,z)) . a = ((a,b) --> (x,y)) . a by A3, FUNCT_4:11 .= x by A2, FUNCT_4:63 ; ::_thesis: ( ((a,b,c) --> (x,y,z)) . b = y & ((a,b,c) --> (x,y,z)) . c = z ) thus ((a,b,c) --> (x,y,z)) . b = ((a,b) --> (x,y)) . b by A4, A6, FUNCT_4:11 .= y by FUNCT_4:63 ; ::_thesis: ((a,b,c) --> (x,y,z)) . c = z thus ((a,b,c) --> (x,y,z)) . c = (c .--> z) . c by A5, A6, FUNCT_4:13 .= z by FUNCOP_1:72 ; ::_thesis: verum end; theorem Th29: :: BORSUK_7:29 for a, b, x, y, z being set for c being complex number for f being Function st dom f = {a,b,c} & f . a = x & f . b = y & f . c = z holds f = (a,b,c) --> (x,y,z) proof let a, b, x, y, z be set ; ::_thesis: for c being complex number for f being Function st dom f = {a,b,c} & f . a = x & f . b = y & f . c = z holds f = (a,b,c) --> (x,y,z) let c be complex number ; ::_thesis: for f being Function st dom f = {a,b,c} & f . a = x & f . b = y & f . c = z holds f = (a,b,c) --> (x,y,z) let f be Function; ::_thesis: ( dom f = {a,b,c} & f . a = x & f . b = y & f . c = z implies f = (a,b,c) --> (x,y,z) ) assume that A1: dom f = {a,b,c} and A2: ( f . a = x & f . b = y & f . c = z ) ; ::_thesis: f = (a,b,c) --> (x,y,z) set g = (a,b,c) --> (x,y,z); thus dom f = dom ((a,b,c) --> (x,y,z)) by A1, BVFUNC14:11; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds ( not b1 in dom f or f . b1 = ((a,b,c) --> (x,y,z)) . b1 ) let k be set ; ::_thesis: ( not k in dom f or f . k = ((a,b,c) --> (x,y,z)) . k ) assume k in dom f ; ::_thesis: f . k = ((a,b,c) --> (x,y,z)) . k then A3: ( k = a or k = b or k = c ) by A1, ENUMSET1:def_1; percases ( a,b,c are_mutually_different or not a,b,c are_mutually_different ) ; suppose a,b,c are_mutually_different ; ::_thesis: f . k = ((a,b,c) --> (x,y,z)) . k hence f . k = ((a,b,c) --> (x,y,z)) . k by A2, A3, Th28; ::_thesis: verum end; supposeA4: not a,b,c are_mutually_different ; ::_thesis: f . k = ((a,b,c) --> (x,y,z)) . k percases ( ( a = b & a <> c ) or a = c or ( b = c & a <> c ) ) by A4, ZFMISC_1:def_5; supposeA5: ( a = b & a <> c ) ; ::_thesis: f . k = ((a,b,c) --> (x,y,z)) . k then (a,b,c) --> (x,y,z) = (a,c) --> (y,z) by FUNCT_4:81; hence f . k = ((a,b,c) --> (x,y,z)) . k by A5, A2, A3, FUNCT_4:63; ::_thesis: verum end; supposeA6: a = c ; ::_thesis: f . k = ((a,b,c) --> (x,y,z)) . k percases ( a <> b or a = b ) ; supposeA7: a <> b ; ::_thesis: f . k = ((a,b,c) --> (x,y,z)) . k then (a,b,c) --> (x,y,z) = (a,b) --> (z,y) by A6, Th25; hence f . k = ((a,b,c) --> (x,y,z)) . k by A6, A2, A3, A7, FUNCT_4:63; ::_thesis: verum end; suppose a = b ; ::_thesis: f . k = ((a,b,c) --> (x,y,z)) . k hence f . k = ((a,b,c) --> (x,y,z)) . k by A6, A2, A3, FUNCOP_1:72; ::_thesis: verum end; end; end; supposeA8: ( b = c & a <> c ) ; ::_thesis: f . k = ((a,b,c) --> (x,y,z)) . k then (a,b,c) --> (x,y,z) = (a,b) --> (x,z) by Th26; hence f . k = ((a,b,c) --> (x,y,z)) . k by A8, A2, A3, FUNCT_4:63; ::_thesis: verum end; end; end; end; end; theorem Th30: :: BORSUK_7:30 for a, b being set for c being complex number holds <*a,b,c*> = (1,2,3) --> (a,b,c) proof let a, b be set ; ::_thesis: for c being complex number holds <*a,b,c*> = (1,2,3) --> (a,b,c) let c be complex number ; ::_thesis: <*a,b,c*> = (1,2,3) --> (a,b,c) set f = (1,2,3) --> (a,b,c); set g = <*a,b,c*>; A1: dom <*a,b,c*> = Seg (len <*a,b,c*>) by FINSEQ_1:def_3 .= {1,2,3} by FINSEQ_3:1, FINSEQ_1:45 ; A2: dom ((1,2,3) --> (a,b,c)) = {1,2,3} by BVFUNC14:11; now__::_thesis:_for_x_being_set_st_x_in_dom_((1,2,3)_-->_(a,b,c))_holds_ ((1,2,3)_-->_(a,b,c))_._x_=_<*a,b,c*>_._x let x be set ; ::_thesis: ( x in dom ((1,2,3) --> (a,b,c)) implies ((1,2,3) --> (a,b,c)) . b1 = <*a,b,c*> . b1 ) assume A3: x in dom ((1,2,3) --> (a,b,c)) ; ::_thesis: ((1,2,3) --> (a,b,c)) . b1 = <*a,b,c*> . b1 percases ( x = 1 or x = 2 or x = 3 ) by A2, A3, ENUMSET1:def_1; supposeA4: x = 1 ; ::_thesis: ((1,2,3) --> (a,b,c)) . b1 = <*a,b,c*> . b1 hence ((1,2,3) --> (a,b,c)) . x = a by Lm6, Th28 .= <*a,b,c*> . x by A4, FINSEQ_1:45 ; ::_thesis: verum end; supposeA5: x = 2 ; ::_thesis: ((1,2,3) --> (a,b,c)) . b1 = <*a,b,c*> . b1 hence ((1,2,3) --> (a,b,c)) . x = b by Lm6, Th28 .= <*a,b,c*> . x by A5, FINSEQ_1:45 ; ::_thesis: verum end; supposeA6: x = 3 ; ::_thesis: ((1,2,3) --> (a,b,c)) . b1 = <*a,b,c*> . b1 hence ((1,2,3) --> (a,b,c)) . x = c by Lm6, Th28 .= <*a,b,c*> . x by A6, FINSEQ_1:45 ; ::_thesis: verum end; end; end; hence <*a,b,c*> = (1,2,3) --> (a,b,c) by A1, BVFUNC14:11, FUNCT_1:2; ::_thesis: verum end; theorem Th31: :: BORSUK_7:31 for a, b, x, y, z being set for c being complex number st a,b,c are_mutually_different holds product ((a,b,c) --> ({x},{y},{z})) = {((a,b,c) --> (x,y,z))} proof let a, b, x, y, z be set ; ::_thesis: for c being complex number st a,b,c are_mutually_different holds product ((a,b,c) --> ({x},{y},{z})) = {((a,b,c) --> (x,y,z))} let c be complex number ; ::_thesis: ( a,b,c are_mutually_different implies product ((a,b,c) --> ({x},{y},{z})) = {((a,b,c) --> (x,y,z))} ) assume A1: a,b,c are_mutually_different ; ::_thesis: product ((a,b,c) --> ({x},{y},{z})) = {((a,b,c) --> (x,y,z))} set X = {((a,b,c) --> (x,y,z))}; set f = (a,b,c) --> ({x},{y},{z}); A2: dom ((a,b,c) --> ({x},{y},{z})) = {a,b,c} by BVFUNC14:11; now__::_thesis:_for_m_being_set_holds_ (_(_m_in_{((a,b,c)_-->_(x,y,z))}_implies_ex_g_being_Function_st_ (_m_=_g_&_dom_g_=_dom_((a,b,c)_-->_({x},{y},{z}))_&_(_for_x_being_set_st_x_in_dom_((a,b,c)_-->_({x},{y},{z}))_holds_ g_._x_in_((a,b,c)_-->_({x},{y},{z}))_._x_)_)_)_&_(_ex_g_being_Function_st_ (_m_=_g_&_dom_g_=_dom_((a,b,c)_-->_({x},{y},{z}))_&_(_for_x_being_set_st_x_in_dom_((a,b,c)_-->_({x},{y},{z}))_holds_ g_._x_in_((a,b,c)_-->_({x},{y},{z}))_._x_)_)_implies_m_in_{((a,b,c)_-->_(x,y,z))}_)_) let m be set ; ::_thesis: ( ( m in {((a,b,c) --> (x,y,z))} implies ex g being Function st ( m = g & dom g = dom ((a,b,c) --> ({x},{y},{z})) & ( for x being set st x in dom ((a,b,c) --> ({x},{y},{z})) holds g . x in ((a,b,c) --> ({x},{y},{z})) . x ) ) ) & ( ex g being Function st ( m = g & dom g = dom ((a,b,c) --> ({x},{y},{z})) & ( for x being set st x in dom ((a,b,c) --> ({x},{y},{z})) holds g . x in ((a,b,c) --> ({x},{y},{z})) . x ) ) implies m in {((a,b,c) --> (x,y,z))} ) ) thus ( m in {((a,b,c) --> (x,y,z))} implies ex g being Function st ( m = g & dom g = dom ((a,b,c) --> ({x},{y},{z})) & ( for x being set st x in dom ((a,b,c) --> ({x},{y},{z})) holds g . x in ((a,b,c) --> ({x},{y},{z})) . x ) ) ) ::_thesis: ( ex g being Function st ( m = g & dom g = dom ((a,b,c) --> ({x},{y},{z})) & ( for x being set st x in dom ((a,b,c) --> ({x},{y},{z})) holds g . x in ((a,b,c) --> ({x},{y},{z})) . x ) ) implies m in {((a,b,c) --> (x,y,z))} ) proof assume A3: m in {((a,b,c) --> (x,y,z))} ; ::_thesis: ex g being Function st ( m = g & dom g = dom ((a,b,c) --> ({x},{y},{z})) & ( for x being set st x in dom ((a,b,c) --> ({x},{y},{z})) holds g . x in ((a,b,c) --> ({x},{y},{z})) . x ) ) take g = (a,b,c) --> (x,y,z); ::_thesis: ( m = g & dom g = dom ((a,b,c) --> ({x},{y},{z})) & ( for x being set st x in dom ((a,b,c) --> ({x},{y},{z})) holds g . x in ((a,b,c) --> ({x},{y},{z})) . x ) ) thus m = g by A3, TARSKI:def_1; ::_thesis: ( dom g = dom ((a,b,c) --> ({x},{y},{z})) & ( for x being set st x in dom ((a,b,c) --> ({x},{y},{z})) holds g . x in ((a,b,c) --> ({x},{y},{z})) . x ) ) thus dom g = dom ((a,b,c) --> ({x},{y},{z})) by A2, BVFUNC14:11; ::_thesis: for x being set st x in dom ((a,b,c) --> ({x},{y},{z})) holds g . x in ((a,b,c) --> ({x},{y},{z})) . x let k be set ; ::_thesis: ( k in dom ((a,b,c) --> ({x},{y},{z})) implies g . k in ((a,b,c) --> ({x},{y},{z})) . k ) assume k in dom ((a,b,c) --> ({x},{y},{z})) ; ::_thesis: g . k in ((a,b,c) --> ({x},{y},{z})) . k then A4: ( k = a or k = b or k = c ) by A2, ENUMSET1:def_1; ( g . a = x & ((a,b,c) --> ({x},{y},{z})) . a = {x} & g . b = y & ((a,b,c) --> ({x},{y},{z})) . b = {y} & g . c = z & ((a,b,c) --> ({x},{y},{z})) . c = {z} ) by A1, Th28; hence g . k in ((a,b,c) --> ({x},{y},{z})) . k by A4, TARSKI:def_1; ::_thesis: verum end; given g being Function such that A5: m = g and A6: dom g = dom ((a,b,c) --> ({x},{y},{z})) and A7: for x being set st x in dom ((a,b,c) --> ({x},{y},{z})) holds g . x in ((a,b,c) --> ({x},{y},{z})) . x ; ::_thesis: m in {((a,b,c) --> (x,y,z))} ( a in dom ((a,b,c) --> ({x},{y},{z})) & b in dom ((a,b,c) --> ({x},{y},{z})) & c in dom ((a,b,c) --> ({x},{y},{z})) ) by A2, ENUMSET1:def_1; then ( g . a in ((a,b,c) --> ({x},{y},{z})) . a & g . b in ((a,b,c) --> ({x},{y},{z})) . b & g . c in ((a,b,c) --> ({x},{y},{z})) . c & ((a,b,c) --> ({x},{y},{z})) . a = {x} & ((a,b,c) --> ({x},{y},{z})) . b = {y} & ((a,b,c) --> ({x},{y},{z})) . c = {z} ) by A1, A7, Th28; 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, Th29; hence m in {((a,b,c) --> (x,y,z))} by A5, TARSKI:def_1; ::_thesis: verum end; hence product ((a,b,c) --> ({x},{y},{z})) = {((a,b,c) --> (x,y,z))} by CARD_3:def_5; ::_thesis: verum end; theorem Th32: :: BORSUK_7:32 for a, b being set for c being complex number 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 let a, b be set ; ::_thesis: for c being complex number 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)) let c be complex number ; ::_thesis: 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)) let A, B, C, D, E, F be set ; ::_thesis: ( A c= B & C c= D & E c= F implies product ((a,b,c) --> (A,C,E)) c= product ((a,b,c) --> (B,D,F)) ) assume A1: ( A c= B & C c= D & E c= F ) ; ::_thesis: product ((a,b,c) --> (A,C,E)) c= product ((a,b,c) --> (B,D,F)) set f = (a,b,c) --> (A,C,E); set g = (a,b,c) --> (B,D,F); A2: ( dom ((a,b,c) --> (A,C,E)) = {a,b,c} & dom ((a,b,c) --> (B,D,F)) = {a,b,c} ) by BVFUNC14:11; percases ( ( a = c & a <> b ) or ( b = c & a <> b ) or a = b or ( a <> b & a <> c & b <> c ) ) ; suppose ( a = c & a <> b ) ; ::_thesis: product ((a,b,c) --> (A,C,E)) c= product ((a,b,c) --> (B,D,F)) then ( (a,b,c) --> (A,C,E) = (a,b) --> (E,C) & (a,b,c) --> (B,D,F) = (a,b) --> (F,D) ) by Th25; hence product ((a,b,c) --> (A,C,E)) c= product ((a,b,c) --> (B,D,F)) by A1, TOPREAL6:21; ::_thesis: verum end; suppose ( b = c & a <> b ) ; ::_thesis: product ((a,b,c) --> (A,C,E)) c= product ((a,b,c) --> (B,D,F)) then ( (a,b,c) --> (A,C,E) = (a,b) --> (A,E) & (a,b,c) --> (B,D,F) = (a,b) --> (B,F) ) by Th26; hence product ((a,b,c) --> (A,C,E)) c= product ((a,b,c) --> (B,D,F)) by A1, TOPREAL6:21; ::_thesis: verum end; suppose a = b ; ::_thesis: product ((a,b,c) --> (A,C,E)) c= product ((a,b,c) --> (B,D,F)) then ( (a,b,c) --> (A,C,E) = (a,c) --> (C,E) & (a,b,c) --> (B,D,F) = (a,c) --> (D,F) ) by FUNCT_4:81; hence product ((a,b,c) --> (A,C,E)) c= product ((a,b,c) --> (B,D,F)) by A1, TOPREAL6:21; ::_thesis: verum end; supposeA3: ( a <> b & a <> c & b <> c ) ; ::_thesis: product ((a,b,c) --> (A,C,E)) c= product ((a,b,c) --> (B,D,F)) for x being set st x in dom ((a,b,c) --> (A,C,E)) holds ((a,b,c) --> (A,C,E)) . x c= ((a,b,c) --> (B,D,F)) . x proof let x be set ; ::_thesis: ( x in dom ((a,b,c) --> (A,C,E)) implies ((a,b,c) --> (A,C,E)) . x c= ((a,b,c) --> (B,D,F)) . x ) assume x in dom ((a,b,c) --> (A,C,E)) ; ::_thesis: ((a,b,c) --> (A,C,E)) . x c= ((a,b,c) --> (B,D,F)) . x then A4: ( x = a or x = b or x = c ) by A2, ENUMSET1:def_1; a,b,c are_mutually_different by A3, ZFMISC_1:def_5; then ( ((a,b,c) --> (A,C,E)) . a = A & ((a,b,c) --> (A,C,E)) . b = C & ((a,b,c) --> (A,C,E)) . c = E & ((a,b,c) --> (B,D,F)) . a = B & ((a,b,c) --> (B,D,F)) . b = D & ((a,b,c) --> (B,D,F)) . c = F ) by Th28; hence ((a,b,c) --> (A,C,E)) . x c= ((a,b,c) --> (B,D,F)) . x by A1, A4; ::_thesis: verum end; hence product ((a,b,c) --> (A,C,E)) c= product ((a,b,c) --> (B,D,F)) by A2, CARD_3:27; ::_thesis: verum end; end; end; theorem Th33: :: BORSUK_7:33 for a, b, x, X, y, Y, z, Z being set for c being complex number st a,b,c are_mutually_different & 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 let a, b, x, X, y, Y, z, Z be set ; ::_thesis: for c being complex number st a,b,c are_mutually_different & x in X & y in Y & z in Z holds (a,b,c) --> (x,y,z) in product ((a,b,c) --> (X,Y,Z)) let c be complex number ; ::_thesis: ( a,b,c are_mutually_different & x in X & y in Y & z in Z implies (a,b,c) --> (x,y,z) in product ((a,b,c) --> (X,Y,Z)) ) assume A1: a,b,c are_mutually_different ; ::_thesis: ( not x in X or not y in Y or not z in Z or (a,b,c) --> (x,y,z) in product ((a,b,c) --> (X,Y,Z)) ) assume ( x in X & y in Y & z in Z ) ; ::_thesis: (a,b,c) --> (x,y,z) in product ((a,b,c) --> (X,Y,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 Th32; then {((a,b,c) --> (x,y,z))} c= product ((a,b,c) --> (X,Y,Z)) by A1, Th31; hence (a,b,c) --> (x,y,z) in product ((a,b,c) --> (X,Y,Z)) by ZFMISC_1:31; ::_thesis: verum end; definition let f be Function; attrf is odd means :Def2: :: BORSUK_7:def 2 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 Def2 defines odd BORSUK_7:def_2_:_ for f being Function holds ( f is odd iff for x, y being complex-valued Function st x in dom f & - x in dom f & y = f . x holds f . (- x) = - y ); registration cluster {} -> odd ; coherence {} is odd proof thus for x, y being complex-valued Function st x in dom {} & - x in dom {} & y = {} . x holds {} . (- x) = - y ; :: according to BORSUK_7:def_2 ::_thesis: verum end; end; registration cluster Relation-like Function-like complex-functions-valued odd for set ; existence ex b1 being complex-functions-valued Function st b1 is odd proof take {} ; ::_thesis: {} is odd thus {} is odd ; ::_thesis: verum 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 let p be Point of (TOP-REAL 3); ::_thesis: sqr p = <*((p `1) ^2),((p `2) ^2),((p `3) ^2)*> p = |[(p `1),(p `2),(p `3)]| by EUCLID_5:3; hence sqr p = <*((p `1) ^2),((p `2) ^2),((p `3) ^2)*> by Th16; ::_thesis: verum end; theorem Th35: :: 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 let p be Point of (TOP-REAL 3); ::_thesis: Sum (sqr p) = (((p `1) ^2) + ((p `2) ^2)) + ((p `3) ^2) p = |[(p `1),(p `2),(p `3)]| by EUCLID_5:3; hence Sum (sqr p) = (((p `1) ^2) + ((p `2) ^2)) + ((p `3) ^2) by Th17; ::_thesis: verum 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 Th36: :: BORSUK_7:36 for r being real number for S being Subset of R^1 st S = RAT holds RAT /\ ].-infty,r.[ is open Subset of (R^1 | S) proof let r be real number ; ::_thesis: for S being Subset of R^1 st S = RAT holds RAT /\ ].-infty,r.[ is open Subset of (R^1 | S) let S be Subset of R^1; ::_thesis: ( S = RAT implies RAT /\ ].-infty,r.[ is open Subset of (R^1 | S) ) assume A1: S = RAT ; ::_thesis: RAT /\ ].-infty,r.[ is open Subset of (R^1 | S) set X = ].-infty,r.[; reconsider R = RAT /\ ].-infty,r.[ as Subset of (R^1 | (R^1 QQ)) by Lm8, XBOOLE_1:17; A2: R^1 ].-infty,r.[ is open by BORSUK_5:40; R = (R^1 ].-infty,r.[) /\ the carrier of (R^1 | (R^1 QQ)) by PRE_TOPC:8; hence RAT /\ ].-infty,r.[ is open Subset of (R^1 | S) by A1, A2, TSP_1:def_1; ::_thesis: verum end; theorem Th37: :: BORSUK_7:37 for r being real number for S being Subset of R^1 st S = RAT holds RAT /\ ].r,+infty.[ is open Subset of (R^1 | S) proof let r be real number ; ::_thesis: for S being Subset of R^1 st S = RAT holds RAT /\ ].r,+infty.[ is open Subset of (R^1 | S) let S be Subset of R^1; ::_thesis: ( S = RAT implies RAT /\ ].r,+infty.[ is open Subset of (R^1 | S) ) assume A1: S = RAT ; ::_thesis: RAT /\ ].r,+infty.[ is open Subset of (R^1 | S) set X = ].r,+infty.[; reconsider R = RAT /\ ].r,+infty.[ as Subset of (R^1 | (R^1 QQ)) by Lm8, XBOOLE_1:17; A2: R^1 ].r,+infty.[ is open by BORSUK_5:40; R = (R^1 ].r,+infty.[) /\ the carrier of (R^1 | (R^1 QQ)) by PRE_TOPC:8; hence RAT /\ ].r,+infty.[ is open Subset of (R^1 | S) by A1, A2, TSP_1:def_1; ::_thesis: verum end; Lm9: now__::_thesis:_for_T_being_non_empty_connected_TopSpace for_f_being_Function_of_T,(R^1_|_(R^1_QQ)) for_x,_y_being_set_st_x_in_dom_f_&_y_in_dom_f_&_f_._x_<_f_._y_holds_ 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_) let T be non empty connected TopSpace; ::_thesis: for f being Function of T,(R^1 | (R^1 QQ)) for x, y being set st x in dom f & y in dom f & f . x < f . y holds 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 ) let f be Function of T,(R^1 | (R^1 QQ)); ::_thesis: for x, y being set st x in dom f & y in dom f & f . x < f . y holds 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 ) let x, y be set ; ::_thesis: ( x in dom f & y in dom f & f . x < f . y implies 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 ) ) assume A1: ( x in dom f & y in dom f ) ; ::_thesis: ( f . x < f . y implies 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 ) ) assume f . x < f . y ; ::_thesis: 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 ) then consider r being real irrational number 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: verum proof 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 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { q where q is Element of RAT : ( q in rng f & q < r ) } or x in rng f ) assume x in { q where q is Element of RAT : ( q in rng f & q < r ) } ; ::_thesis: x in rng f then ex q being Element of RAT st ( x = q & q in rng f & q < r ) ; hence x in rng f ; ::_thesis: verum 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 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { q where q is Element of RAT : ( q in rng f & q > r ) } or x in rng f ) assume x in { q where q is Element of RAT : ( q in rng f & q > r ) } ; ::_thesis: x in rng f then ex q being Element of RAT st ( x = q & q in rng f & q > r ) ; hence x in rng f ; ::_thesis: verum 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: ex 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 ) take Q2 ; ::_thesis: ( Q1 misses Q2 & Q1 <> {} (Image f) & Q2 <> {} (Image f) & Q1 is open & Q2 is open & [#] (Image f) = Q1 \/ Q2 ) thus Q1 misses Q2 ::_thesis: ( Q1 <> {} (Image f) & Q2 <> {} (Image f) & Q1 is open & Q2 is open & [#] (Image f) = Q1 \/ Q2 ) proof assume not Q1 misses Q2 ; ::_thesis: contradiction then consider x being set 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: verum end; ( f . x in Q1 & f . y in Q2 ) by A2, A3, Lm8; hence ( Q1 <> {} (Image f) & Q2 <> {} (Image f) ) ; ::_thesis: ( Q1 is open & Q2 is open & [#] (Image f) = Q1 \/ Q2 ) reconsider G1 = RAT /\ ].-infty,r.[ as open Subset of (R^1 | (R^1 QQ)) by Th36; reconsider G2 = RAT /\ ].r,+infty.[ as open Subset of (R^1 | (R^1 QQ)) by Th37; Q1 = G1 /\ the carrier of (Image f) proof thus Q1 c= G1 /\ the carrier of (Image f) :: according to XBOOLE_0:def_10 ::_thesis: G1 /\ the carrier of (Image f) c= Q1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Q1 or x in G1 /\ the carrier of (Image f) ) assume x in Q1 ; ::_thesis: x in G1 /\ the carrier of (Image f) 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: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in G1 /\ the carrier of (Image f) or x in Q1 ) assume A9: x in G1 /\ the carrier of (Image f) ; ::_thesis: x in Q1 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: verum end; hence Q1 is open by TSP_1:def_1; ::_thesis: ( Q2 is open & [#] (Image f) = Q1 \/ Q2 ) Q2 = G2 /\ the carrier of (Image f) proof thus Q2 c= G2 /\ the carrier of (Image f) :: according to XBOOLE_0:def_10 ::_thesis: G2 /\ the carrier of (Image f) c= Q2 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Q2 or x in G2 /\ the carrier of (Image f) ) assume x in Q2 ; ::_thesis: x in G2 /\ the carrier of (Image f) 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: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in G2 /\ the carrier of (Image f) or x in Q2 ) assume A15: x in G2 /\ the carrier of (Image f) ; ::_thesis: x in Q2 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: verum end; hence Q2 is open by TSP_1:def_1; ::_thesis: [#] (Image f) = Q1 \/ Q2 thus Q1 \/ Q2 = [#] (Image f) ::_thesis: verum proof thus Q1 \/ Q2 c= [#] (Image f) ; :: according to XBOOLE_0:def_10 ::_thesis: [#] (Image f) c= Q1 \/ Q2 let x be Element of (Image f); :: according to LATTICE7:def_1 ::_thesis: ( not x in [#] (Image f) or x in Q1 \/ Q2 ) assume A18: x in [#] (Image f) ; ::_thesis: x in Q1 \/ Q2 ( 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: verum end; end; 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 ; coherence Image f is connected proof set g = corestr f; A1: dom (corestr f) = [#] X by FUNCT_2:def_1; rng (corestr f) = [#] (Image f) by FUNCT_2:def_3; then (corestr f) .: ([#] X) = [#] (Image f) by A1, RELAT_1:113; hence Image f is connected by CONNSP_1:14, WAYBEL18:10; ::_thesis: verum end; end; theorem Th38: :: 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 let S be Subset of R^1; ::_thesis: ( S = RAT implies for T being connected TopSpace for f being Function of T,(R^1 | S) st f is continuous holds f is constant ) assume A1: S = RAT ; ::_thesis: for T being connected TopSpace for f being Function of T,(R^1 | S) st f is continuous holds f is constant let T be connected TopSpace; ::_thesis: for f being Function of T,(R^1 | S) st f is continuous holds f is constant let f be Function of T,(R^1 | S); ::_thesis: ( f is continuous implies f is constant ) assume A2: f is continuous ; ::_thesis: f is constant percases ( not T is empty or T is empty ) ; supposeA3: not T is empty ; ::_thesis: f is constant set GX = Image f; let x, y be set ; :: according to FUNCT_1:def_10 ::_thesis: ( not x in dom f or not y in dom f or f . x = f . y ) assume that A4: ( x in dom f & y in dom f ) and A5: f . x <> f . y ; ::_thesis: contradiction percases ( f . x < f . y or f . y < f . x ) by A5, XXREAL_0:1; suppose f . x < f . y ; ::_thesis: contradiction then 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 ) by A1, A3, A4, Lm9; hence contradiction by A1, A2, A3, CONNSP_1:11; ::_thesis: verum end; suppose f . y < f . x ; ::_thesis: contradiction then 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 ) by A1, A3, A4, Lm9; hence contradiction by A1, A2, A3, CONNSP_1:11; ::_thesis: verum end; end; end; suppose T is empty ; ::_thesis: f is constant hence f is constant ; ::_thesis: verum end; end; end; theorem Th39: :: BORSUK_7:39 for a, b being real number 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 set X = R^1 ; let a, b be real number ; ::_thesis: 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 set S = Closed-Interval-TSpace (a,b); let f be continuous Function of (Closed-Interval-TSpace (a,b)),R^1; ::_thesis: for g being PartFunc of REAL,REAL st a <= b & f = g holds g is continuous let g be PartFunc of REAL,REAL; ::_thesis: ( a <= b & f = g implies g is continuous ) assume that A1: a <= b and A2: f = g ; ::_thesis: g is continuous set A = left_closed_halfline a; set B = [.a,b.]; set C = right_closed_halfline b; the carrier of (Closed-Interval-TSpace (a,b)) = [.a,b.] by A1, TOPMETR:18; then reconsider a1 = a, b1 = b as Point of (Closed-Interval-TSpace (a,b)) by A1, XXREAL_1:1; set f1 = (R^1 | (R^1 (left_closed_halfline a))) --> (f . a1); set f2 = (R^1 | (R^1 (right_closed_halfline b))) --> (f . b1); A3: the carrier of (R^1 | (R^1 (left_closed_halfline a))) = left_closed_halfline a by PRE_TOPC:8; Closed-Interval-TSpace (a,b) = R^1 | (R^1 [.a,b.]) by A1, TOPMETR:19; then reconsider f = f as continuous Function of (R^1 | (R^1 [.a,b.])),R^1 ; A4: dom ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1)) = the carrier of (R^1 | (R^1 (left_closed_halfline a))) by FUNCT_2:def_1 .= left_closed_halfline a by PRE_TOPC:8 ; A5: dom f = the carrier of (R^1 | (R^1 [.a,b.])) by FUNCT_2:def_1 .= [.a,b.] by PRE_TOPC:8 ; A6: dom ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)) = the carrier of (R^1 | (R^1 (right_closed_halfline b))) by FUNCT_2:def_1 .= right_closed_halfline b by PRE_TOPC:8 ; b in REAL by XREAL_0:def_1; then A7: b < +infty by XXREAL_0:9; (R^1 | (R^1 (left_closed_halfline a))) --> (f . a1) tolerates f proof let x be set ; :: according to PARTFUN1:def_4 ::_thesis: ( not x in (dom ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1))) /\ (dom f) or ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1)) . x = f . x ) assume A8: x in (dom ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1))) /\ (dom f) ; ::_thesis: ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1)) . x = f . x a in REAL by XREAL_0:def_1; then (left_closed_halfline a) /\ [.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 left_closed_halfline a by A4, A8, XBOOLE_0:def_4; hence ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1)) . x = f . x by A3, A9, FUNCOP_1:7; ::_thesis: verum end; then reconsider ff = ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1)) +* f as continuous Function of (R^1 | ((R^1 (left_closed_halfline a)) \/ (R^1 [.a,b.]))),R^1 by TOPGEN_5:10; set G = ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)); ff tolerates (R^1 | (R^1 (right_closed_halfline b))) --> (f . b1) proof let x be set ; :: according to PARTFUN1:def_4 ::_thesis: ( not x in (dom ff) /\ (dom ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1))) or ff . x = ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)) . x ) assume A10: x in (dom ff) /\ (dom ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1))) ; ::_thesis: ff . x = ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)) . x then A11: x in dom ff by XBOOLE_0:def_4; A12: x in dom ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)) by A10, XBOOLE_0:def_4; then reconsider y = x as Real by A6; A13: b <= y by A6, A12, XXREAL_1:3; A14: dom ff = (dom ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1))) \/ (dom f) by FUNCT_4:def_1; percases ( ( x in dom ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1)) & not x in dom f ) or x in dom f ) by A11, A14, XBOOLE_0:def_3; supposethat A15: x in dom ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1)) and A16: not x in dom f ; ::_thesis: ff . x = ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)) . x 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 ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)) . x = f . a1 by A10, FUNCOP_1:7 .= ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1)) . x by A15, FUNCOP_1:7 .= ff . x by A16, FUNCT_4:11 ; ::_thesis: verum end; supposeA17: x in dom f ; ::_thesis: ff . x = ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)) . x then y <= b by A5, XXREAL_1:1; then b = y by A13, XXREAL_0:1; hence ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)) . x = f . x by A10, FUNCOP_1:7 .= ff . x by A17, FUNCT_4:13 ; ::_thesis: verum end; end; end; then A18: ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)) is continuous Function of (R^1 | ((R^1 ((left_closed_halfline a) \/ [.a,b.])) \/ (R^1 (right_closed_halfline b)))),R^1 by TOPGEN_5:10; A19: ((left_closed_halfline a) \/ [.a,b.]) \/ (right_closed_halfline b) c= REAL ; A20: dom (ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1))) = (dom ff) \/ (dom ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1))) by FUNCT_4:def_1 .= ((dom ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1))) \/ (dom f)) \/ (dom ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1))) by FUNCT_4:def_1 ; A21: dom (ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1))) = REAL proof thus dom (ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1))) c= REAL by A4, A5, A6, A19, A20; :: according to XBOOLE_0:def_10 ::_thesis: REAL c= dom (ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1))) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in REAL or x in dom (ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1))) ) assume x in REAL ; ::_thesis: x in dom (ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1))) then reconsider y = x as Real ; A22: y < +infty by XXREAL_0:9; A23: -infty < y by XXREAL_0:12; percases ( y < b or y >= b ) ; supposeA24: y < b ; ::_thesis: x in dom (ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1))) percases ( y < a or y >= a ) ; suppose y < a ; ::_thesis: x in dom (ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1))) then y in left_closed_halfline a by A23, XXREAL_1:2; then y in (dom ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1))) \/ (dom f) by A4, XBOOLE_0:def_3; hence x in dom (ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1))) by A20, XBOOLE_0:def_3; ::_thesis: verum end; suppose y >= a ; ::_thesis: x in dom (ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1))) then y in [.a,b.] by A24, XXREAL_1:1; then y in (dom ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1))) \/ (dom f) by A5, XBOOLE_0:def_3; hence x in dom (ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1))) by A20, XBOOLE_0:def_3; ::_thesis: verum end; end; end; suppose y >= b ; ::_thesis: x in dom (ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1))) then y in right_closed_halfline b by A22, XXREAL_1:3; hence x in dom (ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1))) by A6, A20, XBOOLE_0:def_3; ::_thesis: verum end; end; end; then ((left_closed_halfline a) \/ [.a,b.]) \/ (right_closed_halfline b) = [#] R^1 by A4, A5, A6, A20, TOPMETR:17; then A25: R^1 | ((R^1 ((left_closed_halfline a) \/ [.a,b.])) \/ (R^1 (right_closed_halfline b))) = R^1 by TSEP_1:3; rng (ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1))) c= REAL by TOPMETR:17; then reconsider G = ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)) as PartFunc of REAL,REAL by A21, RELSET_1:4; A26: G is continuous by A18, A25, JORDAN5A:7; A27: dom f = (dom G) /\ [.a,b.] by A5, A21, XBOOLE_1:28; now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_ G_._x_=_f_._x let x be set ; ::_thesis: ( x in dom f implies G . b1 = f . b1 ) assume A28: x in dom f ; ::_thesis: G . b1 = f . b1 then reconsider y = x as Real by A5; A29: y <= b by A5, A28, XXREAL_1:1; percases ( y < b or y = b ) by A29, XXREAL_0:1; suppose y < b ; ::_thesis: G . b1 = f . b1 then not y in dom ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)) by A6, XXREAL_1:3; hence G . x = ff . x by FUNCT_4:11 .= f . x by A28, FUNCT_4:13 ; ::_thesis: verum end; supposeA30: y = b ; ::_thesis: G . b1 = f . b1 then A31: x in dom ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)) by A6, A7, XXREAL_1:3; hence G . x = ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)) . x by FUNCT_4:13 .= f . x by A30, A31, FUNCOP_1:7 ; ::_thesis: verum end; end; end; then g = G | [.a,b.] by A2, A27, FUNCT_1:46; hence g is continuous by A26; ::_thesis: verum end; definition let s be Point of R^1; let r be real number ; :: original: + redefine funcs + r -> Point of R^1; coherence s + r is Point of R^1 by TOPMETR:17, XREAL_0:def_1; end; definition let s be Point of R^1; let r be real number ; :: original: - redefine funcs - r -> Point of R^1; coherence s - r is Point of R^1 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 number ; :: original: + redefine funcf + r -> Function of X,R^1; coherence r + f is Function of X,R^1 proof r + f is Function of X,REAL ; hence r + f is Function of X,R^1 by TOPMETR:17; ::_thesis: verum end; end; definition let X be set ; let f be Function of X,R^1; let r be real number ; :: original: - redefine funcf - r -> Function of X,R^1; coherence f - r is Function of X,R^1 proof f - r is Function of X,REAL ; hence f - r is Function of X,R^1 by TOPMETR:17; ::_thesis: verum end; end; definition let s, t be Point of R^1; let f be Path of s,t; let r be real number ; :: original: + redefine funcf + r -> Path of s + r,t + r; coherence r + f is Path of s + r,t + r proof now__::_thesis:_(_f_+_r_is_continuous_&_(f_+_r)_._0_=_s_+_r_&_(f_+_r)_._1_=_t_+_r_) thus f + r is continuous ; ::_thesis: ( (f + r) . 0 = s + r & (f + r) . 1 = t + r ) thus (f + r) . 0 = (f . j0) + r by VALUED_1:2 .= s + r by BORSUK_2:def_4 ; ::_thesis: (f + r) . 1 = t + r thus (f + r) . 1 = (f . j1) + r by VALUED_1:2 .= t + r by BORSUK_2:def_4 ; ::_thesis: verum end; hence r + f is Path of s + r,t + r by BORSUK_2:def_4; ::_thesis: verum end; :: original: - redefine funcf - r -> Path of s - r,t - r; coherence f - r is Path of s - r,t - r proof now__::_thesis:_(_f_-_r_is_continuous_&_(f_-_r)_._0_=_s_-_r_&_(f_-_r)_._1_=_t_-_r_) thus f - r is continuous ; ::_thesis: ( (f - r) . 0 = s - r & (f - r) . 1 = t - r ) thus (f - r) . 0 = (f . j0) - r by VALUED_1:2 .= s - r by BORSUK_2:def_4 ; ::_thesis: (f - r) . 1 = t - r thus (f - r) . 1 = (f . j1) - r by VALUED_1:2 .= t - r by BORSUK_2:def_4 ; ::_thesis: verum end; hence f - r is Path of s - r,t - r by BORSUK_2:def_4; ::_thesis: verum end; end; definition func c[100] -> Point of (Tunit_circle 3) equals :: BORSUK_7:def 3 |[1,0,0]|; coherence |[1,0,0]| is Point of (Tunit_circle 3) proof set p = |[1,0,0]|; |.(|[1,0,0]| - (0. (TOP-REAL 3))).| = |.|[1,0,0]|.| by RLVECT_1:13 .= sqrt ((((|[1,0,0]| `1) ^2) + ((|[1,0,0]| `2) ^2)) + ((|[1,0,0]| `3) ^2)) by Th35 .= sqrt (((1 ^2) + ((|[1,0,0]| `2) ^2)) + ((|[1,0,0]| `3) ^2)) by EUCLID_5:2 .= sqrt (((1 ^2) + (Q ^2)) + ((|[1,0,0]| `3) ^2)) by EUCLID_5:2 .= 1 by EUCLID_5:2, SQUARE_1:18 ; then |[1,0,0]| in Sphere ((0. (TOP-REAL 3)),1) by TOPREAL9:9; hence |[1,0,0]| is Point of (Tunit_circle 3) by TOPREALB:9; ::_thesis: verum end; end; :: deftheorem defines c[100] BORSUK_7:def_3_:_ c[100] = |[1,0,0]|; 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 4 |[(- 1),0,0]|; coherence |[(- 1),0,0]| is Point of (Tunit_circle 3) proof |[(- 1),(- Q),(- Q)]| = - c100 by EUCLID_5:11 .= - c[100] ; hence |[(- 1),0,0]| is Point of (Tunit_circle 3) by TOPREALC:60; ::_thesis: verum end; end; :: deftheorem defines c[-100] BORSUK_7:def_4_:_ c[-100] = |[(- 1),0,0]|; reconsider mc100 = c[-100] as Point of (TOP-REAL 3) ; theorem Th40: :: BORSUK_7:40 - c[100] = c[-100] proof - c100 = |[(- 1),(- Q),(- Q)]| by EUCLID_5:11 .= c[-100] ; hence - c[100] = c[-100] ; ::_thesis: verum end; theorem :: BORSUK_7:41 - c[-100] = c[100] by Th40; 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 c[100] - c[-100] = |[2,0,0]| ; ::_thesis: verum 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 let p be Point of (TOP-REAL 2); ::_thesis: ( p `1 = |.p.| * (cos (Arg p)) & p `2 = |.p.| * (sin (Arg p)) ) set c = euc2cpx p; A1: euc2cpx p = (|.(euc2cpx p).| * (cos (Arg (euc2cpx p)))) + ((|.(euc2cpx p).| * (sin (Arg (euc2cpx p)))) * ) by COMPTRIG:62; A2: |.(euc2cpx p).| = |.p.| by EUCLID_3:25; ( Re (euc2cpx p) = p `1 & Im (euc2cpx p) = p `2 ) by COMPLEX1:12; hence ( p `1 = |.p.| * (cos (Arg p)) & p `2 = |.p.| * (sin (Arg p)) ) by A1, A2, COMPLEX1:12; ::_thesis: verum end; theorem :: BORSUK_7:44 for p being Point of (TOP-REAL 2) holds p = cpx2euc ((|.p.| * (cos (Arg p))) + ((|.p.| * (sin (Arg p))) * )) proof let p be Point of (TOP-REAL 2); ::_thesis: p = cpx2euc ((|.p.| * (cos (Arg p))) + ((|.p.| * (sin (Arg p))) * )) set c = euc2cpx p; A1: euc2cpx p = (|.(euc2cpx p).| * (cos (Arg (euc2cpx p)))) + ((|.(euc2cpx p).| * (sin (Arg (euc2cpx p)))) * ) by COMPTRIG:62; |.(euc2cpx p).| = |.p.| by EUCLID_3:25; hence p = cpx2euc ((|.p.| * (cos (Arg p))) + ((|.p.| * (sin (Arg p))) * )) by A1, EUCLID_3:2; ::_thesis: verum end; theorem Th45: :: 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 let i be Integer; ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st |.p1.| = |.p2.| & Arg p1 = (Arg p2) + ((2 * PI) * i) holds p1 = p2 let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( |.p1.| = |.p2.| & Arg p1 = (Arg p2) + ((2 * PI) * i) implies p1 = p2 ) ( |.(euc2cpx p1).| = |.p1.| & |.(euc2cpx p2).| = |.p2.| ) by EUCLID_3:25; hence ( |.p1.| = |.p2.| & Arg p1 = (Arg p2) + ((2 * PI) * i) implies p1 = p2 ) by Th12, EUCLID_3:4; ::_thesis: verum end; set CM = CircleMap ; theorem Th46: :: BORSUK_7:46 for r being real number for p being Point of (TOP-REAL 2) st p = CircleMap . r holds Arg p = (2 * PI) * (frac r) proof let r be real number ; ::_thesis: for p being Point of (TOP-REAL 2) st p = CircleMap . r holds Arg p = (2 * PI) * (frac r) let p be Point of (TOP-REAL 2); ::_thesis: ( p = CircleMap . r implies Arg p = (2 * PI) * (frac r) ) set z = euc2cpx p; set A = (2 * PI) * (frac r); assume A1: p = CircleMap . r ; ::_thesis: Arg p = (2 * PI) * (frac r) reconsider q = CircleMap . (R^1 r) as Point of (TOP-REAL 2) by PRE_TOPC:25; A2: |.(euc2cpx p).| = |.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 <= (2 * PI) * (frac r) & (2 * PI) * (frac r) < (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: CircleMap . r = |[(cos ((2 * PI) * r)),(sin ((2 * PI) * r))]| by TOPREALB:def_11; (2 * PI) * (frac r) = ((2 * PI) * r) + ((2 * PI) * (- [\r/])) ; then ( cos ((2 * PI) * r) = cos ((2 * PI) * (frac r)) & sin ((2 * PI) * r) = sin ((2 * PI) * (frac r)) ) by COMPLEX2:8, COMPLEX2:9; then euc2cpx p = (|.(euc2cpx p).| * (cos ((2 * PI) * (frac r)))) + ((|.(euc2cpx p).| * (sin ((2 * PI) * (frac r)))) * ) by A1, A2, A3, A5, A6; hence Arg p = (2 * PI) * (frac r) by A4, A2, A1, A3, COMPLEX1:44, COMPTRIG:def_1; ::_thesis: verum end; theorem Th47: :: 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 let p1, p2 be Point of (TOP-REAL 3); ::_thesis: 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)) let u1, u2 be Point of (Euclid 3); ::_thesis: ( 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)) ) assume A1: ( u1 = p1 & u2 = p2 ) ; ::_thesis: (Pitag_dist 3) . (u1,u2) = sqrt (((((p1 `1) - (p2 `1)) ^2) + (((p1 `2) - (p2 `2)) ^2)) + (((p1 `3) - (p2 `3)) ^2)) A2: p1 = |[(p1 `1),(p1 `2),(p1 `3)]| by EUCLID_5:3; A3: u2 = <*(p2 `1),(p2 `2),(p2 `3)*> by A1, EUCLID_5:3; reconsider v1 = u1, v2 = u2 as Element of REAL 3 ; v1 - v2 = <*(diffreal . ((p1 `1),(p2 `1))),(diffreal . ((p1 `2),(p2 `2))),(diffreal . ((p1 `3),(p2 `3)))*> 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 .= <*(abs ((p1 `1) - (p2 `1))),(absreal . ((p1 `2) - (p2 `2))),(absreal . ((p1 `3) - (p2 `3)))*> by EUCLID:def_2 .= <*(abs ((p1 `1) - (p2 `1))),(abs ((p1 `2) - (p2 `2))),(absreal . ((p1 `3) - (p2 `3)))*> by EUCLID:def_2 .= <*(abs ((p1 `1) - (p2 `1))),(abs ((p1 `2) - (p2 `2))),(abs ((p1 `3) - (p2 `3)))*> by EUCLID:def_2 ; then A4: sqr (abs (v1 - v2)) = <*(sqrreal . (abs ((p1 `1) - (p2 `1)))),(sqrreal . (abs ((p1 `2) - (p2 `2)))),(sqrreal . (abs ((p1 `3) - (p2 `3))))*> by FINSEQ_2:37 .= <*((abs ((p1 `1) - (p2 `1))) ^2),(sqrreal . (abs ((p1 `2) - (p2 `2)))),(sqrreal . (abs ((p1 `3) - (p2 `3))))*> by RVSUM_1:def_2 .= <*((abs ((p1 `1) - (p2 `1))) ^2),((abs ((p1 `2) - (p2 `2))) ^2),(sqrreal . (abs ((p1 `3) - (p2 `3))))*> by RVSUM_1:def_2 .= <*((abs ((p1 `1) - (p2 `1))) ^2),((abs ((p1 `2) - (p2 `2))) ^2),((abs ((p1 `3) - (p2 `3))) ^2)*> by RVSUM_1:def_2 .= <*(((p1 `1) - (p2 `1)) ^2),((abs ((p1 `2) - (p2 `2))) ^2),((abs ((p1 `3) - (p2 `3))) ^2)*> by COMPLEX1:75 .= <*(((p1 `1) - (p2 `1)) ^2),(((p1 `2) - (p2 `2)) ^2),((abs ((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 (Pitag_dist 3) . (u1,u2) = sqrt (((((p1 `1) - (p2 `1)) ^2) + (((p1 `2) - (p2 `2)) ^2)) + (((p1 `3) - (p2 `3)) ^2)) by A4, RVSUM_1:78; ::_thesis: verum end; theorem Th48: :: BORSUK_7:48 for r being real number 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 let r be real number ; ::_thesis: 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) let p be Point of (TOP-REAL 3); ::_thesis: 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) let e be Point of (Euclid 3); ::_thesis: ( 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) ) set A = ].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[; set B = ].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[; set C = {0}; set f = (1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0}); assume that A1: p = e and A2: p `3 = 0 ; ::_thesis: 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) let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in 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})) or a in Ball (e,r) ) assume a in 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})) ; ::_thesis: a in Ball (e,r) then consider g being Function such that A3: a = g and A4: dom g = dom ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) and A5: for x being set st x in dom ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) holds g . x in ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) . x by CARD_3:def_5; A6: ].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[ = { m where m is Real : ( (p `1) - (r / (sqrt 2)) < m & m < (p `1) + (r / (sqrt 2)) ) } by RCOMP_1:def_2; A7: ].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[ = { n where n is Real : ( (p `2) - (r / (sqrt 2)) < n & n < (p `2) + (r / (sqrt 2)) ) } by RCOMP_1:def_2; A8: dom ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) = {1,2,3} by BVFUNC14:11; then A9: ( 1 in dom ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) & 2 in dom ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) & 3 in dom ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) ) by ENUMSET1:def_1; A10: ( ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) . 1 = ].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[ & ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) . 2 = ].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[ & ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) . 3 = {0} ) by Lm6, Th28; then A11: ( g . 1 in ].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[ & g . 2 in ].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[ & g . 3 in {0} ) by A5, A9; then consider m being Real such that A12: m = g . 1 and ( (p `1) - (r / (sqrt 2)) < m & m < (p `1) + (r / (sqrt 2)) ) by A6; consider n being 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 ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) . 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_3:1, FINSEQ_1:45 ; now__::_thesis:_for_k_being_set_st_k_in_dom_g_holds_ g_._k_=_<*(g_._1),(g_._2),(g_._3)*>_._k let k be set ; ::_thesis: ( k in dom g implies g . k = <*(g . 1),(g . 2),(g . 3)*> . k ) assume k in dom g ; ::_thesis: g . k = <*(g . 1),(g . 2),(g . 3)*> . k 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; ::_thesis: verum end; then A17: a = |[m,n,0]| by A3, A4, A12, A13, A16, A14, BVFUNC14:11, FUNCT_1:2; then reconsider c = a as Point of (TOP-REAL 3) ; reconsider b = c as Point of (Euclid 3) by TOPREAL3:8; ( abs (m - (p `1)) < r / (sqrt 2) & abs (n - (p `2)) < r / (sqrt 2) ) by A11, A12, A13, RCOMP_1:1; then ( (abs (m - (p `1))) ^2 < (r / (sqrt 2)) ^2 & (abs (n - (p `2))) ^2 < (r / (sqrt 2)) ^2 ) by SQUARE_1:16; then ( (abs (m - (p `1))) ^2 < (r ^2) / ((sqrt 2) ^2) & (abs (n - (p `2))) ^2 < (r ^2) / ((sqrt 2) ^2) ) by XCMPLX_1:76; then ( (abs (m - (p `1))) ^2 < (r ^2) / 2 & (abs (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, Th47 .= 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; ::_thesis: verum end; theorem Th49: :: BORSUK_7:49 for i being Integer for c being complex number for s being Real holds Rotate (c,s) = Rotate (c,(s + ((2 * PI) * i))) proof let i be Integer; ::_thesis: for c being complex number for s being Real holds Rotate (c,s) = Rotate (c,(s + ((2 * PI) * i))) let c be complex number ; ::_thesis: for s being Real holds Rotate (c,s) = Rotate (c,(s + ((2 * PI) * i))) let s be Real; ::_thesis: Rotate (c,s) = Rotate (c,(s + ((2 * PI) * i))) ( 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 Rotate (c,s) = Rotate (c,(s + ((2 * PI) * i))) ; ::_thesis: verum end; theorem :: BORSUK_7:50 for i being Integer for s being Real holds Rotate s = Rotate (s + ((2 * PI) * i)) proof let i be Integer; ::_thesis: for s being Real holds Rotate s = Rotate (s + ((2 * PI) * i)) let s be Real; ::_thesis: Rotate s = Rotate (s + ((2 * PI) * i)) let p be Point of (TOP-REAL 2); :: according to FUNCT_2:def_8 ::_thesis: (Rotate s) . p = (Rotate (s + ((2 * PI) * i))) . p set q = (p `1) + ((p `2) * ); A1: Rotate (((p `1) + ((p `2) * )),s) = Rotate (((p `1) + ((p `2) * )),(s + ((2 * PI) * i))) by Th49; thus (Rotate s) . p = |[(Re (Rotate (((p `1) + ((p `2) * )),s))),(Im (Rotate (((p `1) + ((p `2) * )),s)))]| by JORDAN24:def_3 .= (Rotate (s + ((2 * PI) * i))) . p by A1, JORDAN24:def_3 ; ::_thesis: verum end; theorem Th51: :: BORSUK_7:51 for s being Real for p being Point of (TOP-REAL 2) holds |.((Rotate s) . p).| = |.p.| proof let s be Real; ::_thesis: for p being Point of (TOP-REAL 2) holds |.((Rotate s) . p).| = |.p.| let p be Point of (TOP-REAL 2); ::_thesis: |.((Rotate s) . p).| = |.p.| set c = euc2cpx p; set q = (Rotate s) . p; A1: ( Re (Rotate ((euc2cpx p),s)) = |.(euc2cpx p).| * (cos (s + (Arg (euc2cpx p)))) & Im (Rotate ((euc2cpx p),s)) = |.(euc2cpx p).| * (sin (s + (Arg (euc2cpx p)))) ) by COMPLEX1:12; (Rotate s) . p = cpx2euc (Rotate ((euc2cpx p),s)) by JORDAN24:def_3; then A2: ( ((Rotate s) . p) `1 = Re (Rotate ((euc2cpx p),s)) & ((Rotate s) . p) `2 = Im (Rotate ((euc2cpx p),s)) ) by EUCLID:52; |.p.| ^2 = (|.(euc2cpx p).| ^2) * 1 by EUCLID_3:25 .= (|.(euc2cpx p).| ^2) * (((cos (s + (Arg (euc2cpx p)))) ^2) + ((sin (s + (Arg (euc2cpx p)))) ^2)) by SIN_COS:29 .= ((|.(euc2cpx p).| * (cos (s + (Arg (euc2cpx p))))) ^2) + ((|.(euc2cpx p).| * (sin (s + (Arg (euc2cpx p))))) ^2) .= |.((Rotate s) . p).| ^2 by A1, A2, JGRAPH_1:29 ; hence |.p.| = |.((Rotate s) . p).| by Th1; ::_thesis: verum end; theorem Th52: :: 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 let s be Real; ::_thesis: for p being Point of (TOP-REAL 2) holds Arg ((Rotate s) . p) = Arg (Rotate ((euc2cpx p),s)) let p be Point of (TOP-REAL 2); ::_thesis: Arg ((Rotate s) . p) = Arg (Rotate ((euc2cpx p),s)) (Rotate s) . p = cpx2euc (Rotate ((euc2cpx p),s)) by JORDAN24:def_3; hence Arg ((Rotate s) . p) = Arg (Rotate ((euc2cpx p),s)) by EUCLID_3:1; ::_thesis: verum end; theorem Th53: :: 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 let s be Real; ::_thesis: 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) let p be Point of (TOP-REAL 2); ::_thesis: ( p <> 0. (TOP-REAL 2) implies ex i being Integer st Arg ((Rotate s) . p) = (s + (Arg p)) + ((2 * PI) * i) ) set c = euc2cpx p; assume p <> 0. (TOP-REAL 2) ; ::_thesis: ex i being Integer st Arg ((Rotate s) . p) = (s + (Arg p)) + ((2 * PI) * i) then ex i being Integer st Arg (Rotate ((euc2cpx p),s)) = ((2 * PI) * i) + (s + (Arg (euc2cpx p))) by COMPLEX2:54, EUCLID_3:18; hence ex i being Integer st Arg ((Rotate s) . p) = (s + (Arg p)) + ((2 * PI) * i) by Th52; ::_thesis: verum end; theorem Th54: :: BORSUK_7:54 for s being Real holds (Rotate s) . (0. (TOP-REAL 2)) = 0. (TOP-REAL 2) proof let s be Real; ::_thesis: (Rotate s) . (0. (TOP-REAL 2)) = 0. (TOP-REAL 2) thus (Rotate s) . (0. (TOP-REAL 2)) = cpx2euc (Rotate ((euc2cpx (0. (TOP-REAL 2))),s)) by JORDAN24:def_3 .= 0. (TOP-REAL 2) by COMPLEX2:52, EUCLID_3:16, EUCLID_3:17 ; ::_thesis: verum end; theorem Th55: :: 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 let s be Real; ::_thesis: for p being Point of (TOP-REAL 2) st (Rotate s) . p = 0. (TOP-REAL 2) holds p = 0. (TOP-REAL 2) let p be Point of (TOP-REAL 2); ::_thesis: ( (Rotate s) . p = 0. (TOP-REAL 2) implies p = 0. (TOP-REAL 2) ) |.p.| = |.((Rotate s) . p).| by Th51; hence ( (Rotate s) . p = 0. (TOP-REAL 2) implies p = 0. (TOP-REAL 2) ) by TOPRNS_1:23, TOPRNS_1:24; ::_thesis: verum end; theorem Th56: :: BORSUK_7:56 for s being Real for p being Point of (TOP-REAL 2) holds (Rotate s) . ((Rotate (- s)) . p) = p proof let s be Real; ::_thesis: for p being Point of (TOP-REAL 2) holds (Rotate s) . ((Rotate (- s)) . p) = p let p be Point of (TOP-REAL 2); ::_thesis: (Rotate s) . ((Rotate (- s)) . p) = p set f = Rotate s; set g = Rotate (- s); percases ( p <> 0. (TOP-REAL 2) or p = 0. (TOP-REAL 2) ) ; supposeA1: p <> 0. (TOP-REAL 2) ; ::_thesis: (Rotate s) . ((Rotate (- s)) . p) = p then consider i being Integer such that A2: Arg ((Rotate (- s)) . p) = ((- s) + (Arg p)) + ((2 * PI) * i) by Th53; consider j being Integer such that A3: Arg ((Rotate s) . ((Rotate (- s)) . p)) = (s + (Arg ((Rotate (- s)) . p))) + ((2 * PI) * j) by A1, Th55, Th53; A4: |.((Rotate s) . ((Rotate (- s)) . p)).| = |.((Rotate (- s)) . p).| by Th51 .= |.p.| by Th51 ; Arg ((Rotate s) . ((Rotate (- s)) . p)) = (Arg p) + ((2 * PI) * (i + j)) by A2, A3; hence (Rotate s) . ((Rotate (- s)) . p) = p by A4, Th45; ::_thesis: verum end; supposeA5: p = 0. (TOP-REAL 2) ; ::_thesis: (Rotate s) . ((Rotate (- s)) . p) = p (Rotate s) . ((Rotate (- s)) . (0. (TOP-REAL 2))) = (Rotate s) . (0. (TOP-REAL 2)) by Th54 .= 0. (TOP-REAL 2) by Th54 ; hence (Rotate s) . ((Rotate (- s)) . p) = p by A5; ::_thesis: verum end; end; end; theorem :: BORSUK_7:57 for s being Real holds (Rotate s) * (Rotate (- s)) = id (TOP-REAL 2) proof let s be Real; ::_thesis: (Rotate s) * (Rotate (- s)) = id (TOP-REAL 2) let p be Point of (TOP-REAL 2); :: according to FUNCT_2:def_8 ::_thesis: ((Rotate s) * (Rotate (- s))) . p = (id (TOP-REAL 2)) . p set f = Rotate s; set g = Rotate (- s); thus ((Rotate s) * (Rotate (- s))) . p = (Rotate s) . ((Rotate (- s)) . p) by FUNCT_2:15 .= p by Th56 .= (id (TOP-REAL 2)) . p by FUNCT_1:18 ; ::_thesis: verum end; theorem Th58: :: BORSUK_7:58 for r being real number for 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 let r be real number ; ::_thesis: for 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) ) let s be Real; ::_thesis: 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) ) let p be Point of (TOP-REAL 2); ::_thesis: ( p in Sphere ((0. (TOP-REAL 2)),r) iff (Rotate s) . p in Sphere ((0. (TOP-REAL 2)),r) ) A1: |.p.| = |.((Rotate s) . p).| by Th51; A2: ((Rotate s) . p) - (0. (TOP-REAL 2)) = (Rotate s) . p by RLVECT_1:13; hereby ::_thesis: ( (Rotate s) . p in Sphere ((0. (TOP-REAL 2)),r) implies p in Sphere ((0. (TOP-REAL 2)),r) ) assume p in Sphere ((0. (TOP-REAL 2)),r) ; ::_thesis: (Rotate s) . p in Sphere ((0. (TOP-REAL 2)),r) then |.p.| = r by TOPREAL9:12; hence (Rotate s) . p in Sphere ((0. (TOP-REAL 2)),r) by A1, A2, TOPREAL9:9; ::_thesis: verum end; assume (Rotate s) . p in Sphere ((0. (TOP-REAL 2)),r) ; ::_thesis: p in Sphere ((0. (TOP-REAL 2)),r) then A3: |.((Rotate s) . p).| = r by TOPREAL9:12; A4: (Rotate (- s)) . ((Rotate (- (- s))) . p) = p by Th56; ((Rotate (- s)) . ((Rotate s) . p)) - (0. (TOP-REAL 2)) = (Rotate (- s)) . ((Rotate s) . p) by RLVECT_1:13; hence p in Sphere ((0. (TOP-REAL 2)),r) by A4, A3, A1, TOPREAL9:9; ::_thesis: verum end; theorem Th59: :: BORSUK_7:59 for r being real non negative number for s being Real holds (Rotate s) .: (Sphere ((0. (TOP-REAL 2)),r)) = Sphere ((0. (TOP-REAL 2)),r) proof let r be real non negative number ; ::_thesis: for s being Real holds (Rotate s) .: (Sphere ((0. (TOP-REAL 2)),r)) = Sphere ((0. (TOP-REAL 2)),r) let s be Real; ::_thesis: (Rotate s) .: (Sphere ((0. (TOP-REAL 2)),r)) = Sphere ((0. (TOP-REAL 2)),r) set f = Rotate s; set C = Sphere ((0. (TOP-REAL 2)),r); thus (Rotate s) .: (Sphere ((0. (TOP-REAL 2)),r)) c= Sphere ((0. (TOP-REAL 2)),r) :: according to XBOOLE_0:def_10 ::_thesis: Sphere ((0. (TOP-REAL 2)),r) c= (Rotate s) .: (Sphere ((0. (TOP-REAL 2)),r)) proof let y be Point of (TOP-REAL 2); :: according to LATTICE7:def_1 ::_thesis: ( not y in (Rotate s) .: (Sphere ((0. (TOP-REAL 2)),r)) or y in Sphere ((0. (TOP-REAL 2)),r) ) assume y in (Rotate s) .: (Sphere ((0. (TOP-REAL 2)),r)) ; ::_thesis: y in Sphere ((0. (TOP-REAL 2)),r) then ex c being Element of (TOP-REAL 2) st ( c in Sphere ((0. (TOP-REAL 2)),r) & y = (Rotate s) . c ) by FUNCT_2:65; hence y in Sphere ((0. (TOP-REAL 2)),r) by Th58; ::_thesis: verum end; let y be Point of (TOP-REAL 2); :: according to LATTICE7:def_1 ::_thesis: ( not y in Sphere ((0. (TOP-REAL 2)),r) or y in (Rotate s) .: (Sphere ((0. (TOP-REAL 2)),r)) ) set x = (Rotate (- s)) . y; assume y in Sphere ((0. (TOP-REAL 2)),r) ; ::_thesis: y in (Rotate s) .: (Sphere ((0. (TOP-REAL 2)),r)) then (Rotate (- s)) . y in Sphere ((0. (TOP-REAL 2)),r) by Th58; then (Rotate s) . ((Rotate (- s)) . y) in (Rotate s) .: (Sphere ((0. (TOP-REAL 2)),r)) by FUNCT_2:35; hence y in (Rotate s) .: (Sphere ((0. (TOP-REAL 2)),r)) by Th56; ::_thesis: verum end; definition let r be real non negative number ; 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 5 (Rotate s) | (Tcircle ((0. (TOP-REAL 2)),r)); coherence (Rotate s) | (Tcircle ((0. (TOP-REAL 2)),r)) is Function of (Tcircle ((0. (TOP-REAL 2)),r)),(Tcircle ((0. (TOP-REAL 2)),r)) proof set T = Tcircle ((0. (TOP-REAL 2)),r); set f = (Rotate s) | (Tcircle ((0. (TOP-REAL 2)),r)); set C = the carrier of (Tcircle ((0. (TOP-REAL 2)),r)); A1: dom ((Rotate s) | (Tcircle ((0. (TOP-REAL 2)),r))) = the carrier of (Tcircle ((0. (TOP-REAL 2)),r)) by FUNCT_2:def_1; for x being set st x in the carrier of (Tcircle ((0. (TOP-REAL 2)),r)) holds ((Rotate s) | (Tcircle ((0. (TOP-REAL 2)),r))) . x in the carrier of (Tcircle ((0. (TOP-REAL 2)),r)) proof let x be set ; ::_thesis: ( x in the carrier of (Tcircle ((0. (TOP-REAL 2)),r)) implies ((Rotate s) | (Tcircle ((0. (TOP-REAL 2)),r))) . x in the carrier of (Tcircle ((0. (TOP-REAL 2)),r)) ) assume A2: x in the carrier of (Tcircle ((0. (TOP-REAL 2)),r)) ; ::_thesis: ((Rotate s) | (Tcircle ((0. (TOP-REAL 2)),r))) . x in the carrier of (Tcircle ((0. (TOP-REAL 2)),r)) then A3: ((Rotate s) | (Tcircle ((0. (TOP-REAL 2)),r))) . x = (Rotate s) . x by FUNCT_1:49; the carrier of (Tcircle ((0. (TOP-REAL 2)),r)) = Sphere ((0. (TOP-REAL 2)),r) by TOPREALB:9; hence ((Rotate s) | (Tcircle ((0. (TOP-REAL 2)),r))) . x in the carrier of (Tcircle ((0. (TOP-REAL 2)),r)) by A3, A2, Th58; ::_thesis: verum end; hence (Rotate s) | (Tcircle ((0. (TOP-REAL 2)),r)) is Function of (Tcircle ((0. (TOP-REAL 2)),r)),(Tcircle ((0. (TOP-REAL 2)),r)) by A1, FUNCT_2:3; ::_thesis: verum end; end; :: deftheorem defines RotateCircle BORSUK_7:def_5_:_ for r being real non negative number for s being Real holds RotateCircle (r,s) = (Rotate s) | (Tcircle ((0. (TOP-REAL 2)),r)); registration let r be real non negative number ; let s be Real; cluster RotateCircle (r,s) -> being_homeomorphism ; coherence RotateCircle (r,s) is being_homeomorphism proof set T = Tcircle ((0. (TOP-REAL 2)),r); set C = [#] (Tcircle ((0. (TOP-REAL 2)),r)); [#] (Tcircle ((0. (TOP-REAL 2)),r)) c= [#] (TOP-REAL 2) by PRE_TOPC:def_4; then reconsider C = [#] (Tcircle ((0. (TOP-REAL 2)),r)) as Subset of (TOP-REAL 2) ; A1: TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = 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 & f is isometric ) by JORDAN24:2; reconsider A = C as Subset of (TopSpaceMetr (Euclid 2)) by A1; (TOP-REAL 2) | C = Tcircle ((0. (TOP-REAL 2)),r) by PRE_TOPC:def_5; then A3: (TopSpaceMetr (Euclid 2)) | A = Tcircle ((0. (TOP-REAL 2)),r) by A1, PRE_TOPC:36; the carrier of (Tcircle ((0. (TOP-REAL 2)),r)) = Sphere ((0. (TOP-REAL 2)),r) by TOPREALB:9; then (Rotate s) .: C = C by Th59; hence RotateCircle (r,s) is being_homeomorphism by A2, A3, JORDAN24:14; ::_thesis: verum end; end; theorem Th60: :: BORSUK_7:60 for r2, r1 being real number for p being Point of (TOP-REAL 2) st p = CircleMap . r2 holds (RotateCircle (1,(- (Arg p)))) . (CircleMap . r1) = CircleMap . (r1 - r2) proof let r2, r1 be real number ; ::_thesis: for p being Point of (TOP-REAL 2) st p = CircleMap . r2 holds (RotateCircle (1,(- (Arg p)))) . (CircleMap . r1) = CircleMap . (r1 - r2) let p be Point of (TOP-REAL 2); ::_thesis: ( p = CircleMap . r2 implies (RotateCircle (1,(- (Arg p)))) . (CircleMap . r1) = CircleMap . (r1 - r2) ) assume A1: p = CircleMap . r2 ; ::_thesis: (RotateCircle (1,(- (Arg p)))) . (CircleMap . r1) = CircleMap . (r1 - r2) set s = - (Arg p); reconsider q = CircleMap . (R^1 r1), w = CircleMap . (R^1 (r1 - r2)) as Point of (TOP-REAL 2) by PRE_TOPC:25; |.q.| = 1 by TOPREALB:12; then q <> 0. (TOP-REAL 2) by TOPRNS_1:23; then consider i being Integer such that A2: Arg ((Rotate (- (Arg p))) . q) = ((- (Arg p)) + (Arg q)) + ((2 * PI) * i) by Th53; A3: Arg p = (2 * PI) * (frac r2) by A1, Th46; A4: |.((Rotate (- (Arg p))) . q).| = |.q.| by Th51 .= 1 by TOPREALB:12 .= |.w.| by TOPREALB:12 ; consider j being Integer such that A5: frac (r1 - r2) = ((frac r1) - (frac r2)) + j and ( j = 0 or j = 1 ) by Th4; A6: Arg ((Rotate (- (Arg p))) . q) = ((- ((2 * PI) * (frac r2))) + ((2 * PI) * (frac r1))) + ((2 * PI) * i) by A2, A3, Th46 .= ((2 * PI) * (frac (r1 - r2))) + ((2 * PI) * (i - j)) by A5 .= (Arg w) + ((2 * PI) * (i - j)) by Th46 ; thus (RotateCircle (1,(- (Arg p)))) . (CircleMap . r1) = (Rotate (- (Arg p))) . q by FUNCT_1:49 .= CircleMap . (r1 - r2) by A4, A6, Th45 ; ::_thesis: verum end; begin definition let n be non empty Nat; let p be Point of (TOP-REAL n); let r be real non negative number ; func CircleIso (p,r) -> Function of (Tunit_circle n),(Tcircle (p,r)) means :Def6: :: BORSUK_7:def 6 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; existence ex b1 being Function of (Tunit_circle n),(Tcircle (p,r)) st for a being Point of (Tunit_circle n) for b being Point of (TOP-REAL n) st a = b holds b1 . a = (r * b) + p proof set U = Tunit_circle n; set C = Tcircle (p,r); defpred S1[ Point of (Tunit_circle n), set ] means ex w being Point of (TOP-REAL n) st ( w = $1 & $2 = (r * w) + p ); A1: r is Real by XREAL_0:def_1; A2: n in NAT by ORDINAL1:def_12; then A3: the carrier of (Tcircle (p,r)) = Sphere (p,r) by TOPREALB:9; A4: for u being Point of (Tunit_circle n) ex y being Point of (Tcircle (p,r)) st S1[u,y] proof let u be Point of (Tunit_circle n); ::_thesis: ex y being Point of (Tcircle (p,r)) st S1[u,y] reconsider v = u as Point of (TOP-REAL n) by PRE_TOPC:25; set y = (r * v) + p; |.(((r * v) + p) - p).| = |.(r * v).| by EUCLID:48 .= (abs r) * |.v.| by A2, A1, TOPRNS_1:7 .= r * |.v.| by ABSVALUE:def_1 .= r * 1 by A2, TOPREALB:12 ; then reconsider y = (r * v) + p as Point of (Tcircle (p,r)) by A2, A3, TOPREAL9:9; take y ; ::_thesis: S1[u,y] thus S1[u,y] ; ::_thesis: verum end; consider f being Function of (Tunit_circle n),(Tcircle (p,r)) such that A5: for x being Point of (Tunit_circle n) holds S1[x,f . x] from FUNCT_2:sch_3(A4); take f ; ::_thesis: for a being Point of (Tunit_circle n) for b being Point of (TOP-REAL n) st a = b holds f . a = (r * b) + p let a be Point of (Tunit_circle n); ::_thesis: for b being Point of (TOP-REAL n) st a = b holds f . a = (r * b) + p let b be Point of (TOP-REAL n); ::_thesis: ( a = b implies f . a = (r * b) + p ) S1[a,f . a] by A5; hence ( a = b implies f . a = (r * b) + p ) ; ::_thesis: verum end; uniqueness for b1, b2 being Function of (Tunit_circle n),(Tcircle (p,r)) st ( for a being Point of (Tunit_circle n) for b being Point of (TOP-REAL n) st a = b holds b1 . a = (r * b) + p ) & ( for a being Point of (Tunit_circle n) for b being Point of (TOP-REAL n) st a = b holds b2 . a = (r * b) + p ) holds b1 = b2 proof let f, g be Function of (Tunit_circle n),(Tcircle (p,r)); ::_thesis: ( ( for a being Point of (Tunit_circle n) for b being Point of (TOP-REAL n) st a = b holds f . a = (r * b) + p ) & ( for a being Point of (Tunit_circle n) for b being Point of (TOP-REAL n) st a = b holds g . a = (r * b) + p ) implies f = g ) assume that A6: for a being Point of (Tunit_circle n) for b being Point of (TOP-REAL n) st a = b holds f . a = (r * b) + p and A7: for a being Point of (Tunit_circle n) for b being Point of (TOP-REAL n) st a = b holds g . a = (r * b) + p ; ::_thesis: f = g let x be Point of (Tunit_circle n); :: according to FUNCT_2:def_8 ::_thesis: f . x = g . x reconsider y = x as Point of (TOP-REAL n) by PRE_TOPC:25; thus f . x = (r * y) + p by A6 .= g . x by A7 ; ::_thesis: verum end; end; :: deftheorem Def6 defines CircleIso BORSUK_7:def_6_:_ for n being non empty Nat for p being Point of (TOP-REAL n) for r being real non negative number for b4 being Function of (Tunit_circle n),(Tcircle (p,r)) holds ( b4 = CircleIso (p,r) iff for a being Point of (Tunit_circle n) for b being Point of (TOP-REAL n) st a = b holds b4 . a = (r * b) + p ); registration let n be non empty Nat; let p be Point of (TOP-REAL n); let r be real positive number ; cluster CircleIso (p,r) -> being_homeomorphism ; coherence CircleIso (p,r) is being_homeomorphism proof A1: n in NAT by ORDINAL1:def_12; for a being Point of (Tunit_circle n) for b being Point of (TOP-REAL n) st a = b holds (CircleIso (p,r)) . a = (r * b) + p by Def6; hence CircleIso (p,r) is being_homeomorphism by A1, TOPREALB:19; ::_thesis: verum end; end; definition func SphereMap -> Function of R^1,(Tunit_circle 3) means :Def7: :: BORSUK_7:def 7 for x being real number holds it . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]|; existence ex b1 being Function of R^1,(Tunit_circle 3) st for x being real number holds b1 . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| proof defpred S1[ real number , set ] means $2 = |[(cos ((2 * PI) * $1)),(sin ((2 * PI) * $1)),0]|; A1: for x being Element of R^1 ex y being Element of (Tunit_circle 3) st S1[x,y] proof let x be Element of R^1; ::_thesis: ex y being Element of (Tunit_circle 3) st S1[x,y] set y = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]|; |.(|[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| - |[0,0,0]|).| = |.|[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]|.| by EUCLID_5:4, RLVECT_1:13 .= sqrt ((((|[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| `1) ^2) + ((|[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| `2) ^2)) + ((|[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| `3) ^2)) by Th35 .= sqrt ((((cos ((2 * PI) * x)) ^2) + ((|[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| `2) ^2)) + ((|[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| `3) ^2)) by EUCLID_5:2 .= sqrt ((((cos ((2 * PI) * x)) ^2) + ((sin ((2 * PI) * x)) ^2)) + ((|[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| `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 |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| is Element of (Tunit_circle 3) by Lm7, TOPREAL9:9; hence ex y being Element of (Tunit_circle 3) st S1[x,y] ; ::_thesis: verum end; consider f being Function of the carrier of R^1,(Tunit_circle 3) such that A2: for x being Element of R^1 holds S1[x,f . x] from FUNCT_2:sch_3(A1); take f ; ::_thesis: for x being real number holds f . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| let x be real number ; ::_thesis: f . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| x is Point of R^1 by TOPMETR:17, XREAL_0:def_1; hence f . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| by A2; ::_thesis: verum end; uniqueness for b1, b2 being Function of R^1,(Tunit_circle 3) st ( for x being real number holds b1 . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| ) & ( for x being real number holds b2 . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| ) holds b1 = b2 proof let f, g be Function of R^1,(Tunit_circle 3); ::_thesis: ( ( for x being real number holds f . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| ) & ( for x being real number holds g . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| ) implies f = g ) assume that A3: for x being real number holds f . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| and A4: for x being real number holds g . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| ; ::_thesis: f = g let x be Point of R^1; :: according to FUNCT_2:def_8 ::_thesis: f . x = g . x thus f . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| by A3 .= g . x by A4 ; ::_thesis: verum end; end; :: deftheorem Def7 defines SphereMap BORSUK_7:def_7_:_ for b1 being Function of R^1,(Tunit_circle 3) holds ( b1 = SphereMap iff for x being real number holds b1 . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| ); set SM = SphereMap ; theorem :: BORSUK_7:61 for i being Integer holds SphereMap . i = c[100] proof let i be Integer; ::_thesis: SphereMap . i = c[100] thus SphereMap . i = |[(cos (((2 * PI) * i) + Q)),((sin ((2 * PI) * i)) + Q),0]| by Def7 .= |[(cos 0),(sin (((2 * PI) * i) + Q)),0]| by COMPLEX2:9 .= c[100] by COMPLEX2:8, SIN_COS:31 ; ::_thesis: verum 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 sin is Function of R^1,R^1 by A1, TOPREALA:7; ::_thesis: verum 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 cos is Function of R^1,R^1 by A1, TOPREALA:7; ::_thesis: verum end; Lm12: for r being real number holds SphereMap . r = |[((cos * (AffineMap ((2 * PI),Q))) . r),((sin * (AffineMap ((2 * PI),0))) . r),0]| proof let r be real number ; ::_thesis: SphereMap . r = |[((cos * (AffineMap ((2 * PI),Q))) . r),((sin * (AffineMap ((2 * PI),0))) . r),0]| SphereMap . r = |[(cos (((2 * PI) * r) + Q)),(sin ((2 * PI) * r)),0]| by Def7 .= |[((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 SphereMap . r = |[((cos * (AffineMap ((2 * PI),Q))) . r),((sin * (AffineMap ((2 * PI),0))) . r),0]| ; ::_thesis: verum end; registration cluster SphereMap -> continuous ; coherence SphereMap is continuous 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; set cR = R^1 cos; reconsider sR = R^1 sin, cR = R^1 cos 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 = SphereMap as Function of R^1,(TOP-REAL 3) by TOPREALA:7; for p being Point of R^1 for V being Subset of (TOP-REAL 3) st g . p in V & V is open holds ex W being Subset of R^1 st ( p in W & W is open & g .: W c= V ) proof let p be Point of R^1; ::_thesis: for V being Subset of (TOP-REAL 3) st g . p in V & V is open holds ex W being Subset of R^1 st ( p in W & W is open & g .: W c= V ) let V be Subset of (TOP-REAL 3); ::_thesis: ( g . p in V & V is open implies ex W being Subset of R^1 st ( p in W & W is open & g .: W c= V ) ) assume that A6: g . p in V and A7: V is open ; ::_thesis: ex W being Subset of R^1 st ( p in W & W is open & g .: W c= V ) A8: V = Int V by A7, TOPS_1:23; A9: ( (cR * l) . p is Real & (sR * l) . p is Real ) by XREAL_0:def_1; reconsider e = g . p as Point of (Euclid 3) by TOPREAL3:8; consider r being real number such that A10: r > 0 and A11: 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) --> (].(((g . p) `1) - (r / (sqrt 2))),(((g . p) `1) + (r / (sqrt 2))).[,].(((g . p) `2) - (r / (sqrt 2))),(((g . p) `2) + (r / (sqrt 2))).[,{0}); A12: g . p = |[((cR * l) . p),((sR * l) . p),0]| by Lm12; then A13: (g . p) `2 = (sR * l) . p by A9, EUCLID_5:2; (g . p) `3 = 0 by A9, A12, EUCLID_5:2; then A14: product ((1,2,3) --> (].(((g . p) `1) - (r / (sqrt 2))),(((g . p) `1) + (r / (sqrt 2))).[,].(((g . p) `2) - (r / (sqrt 2))),(((g . p) `2) + (r / (sqrt 2))).[,{0})) c= Ball (e,r) by Th48; reconsider A = ].(((g . p) `1) - (r / (sqrt 2))),(((g . p) `1) + (r / (sqrt 2))).[, B = ].(((g . p) `2) - (r / (sqrt 2))),(((g . p) `2) + (r / (sqrt 2))).[ as Subset of R^1 by TOPMETR:17; A15: A is open by JORDAN6:35; A16: B is open by JORDAN6:35; A17: sR is continuous by A2, PRE_TOPC:26; (sR * l) . p in B by A10, A13, TOPREAL6:15; then consider Ws being Subset of R^1 such that A18: p in Ws and A19: Ws is open and A20: (sR * l) .: Ws c= B by A16, A17, A1, A4, A5, JGRAPH_2:10, TOPREALB:5; A21: (g . p) `1 = (cR * l) . p by A12, A9, EUCLID_5:2; A22: cR is continuous by A3, PRE_TOPC:26; (cR * l) . p in A by A10, A21, TOPREAL6:15; then consider Wc being Subset of R^1 such that A23: p in Wc and A24: Wc is open and A25: (cR * l) .: Wc c= A by A15, A22, A1, A4, A5, JGRAPH_2:10, TOPREALB:5; set W = Ws /\ Wc; take Ws /\ Wc ; ::_thesis: ( p in Ws /\ Wc & Ws /\ Wc is open & g .: (Ws /\ Wc) c= V ) thus p in Ws /\ Wc by A18, A23, XBOOLE_0:def_4; ::_thesis: ( Ws /\ Wc is open & g .: (Ws /\ Wc) c= V ) thus Ws /\ Wc is open by A19, A24; ::_thesis: g .: (Ws /\ Wc) c= V let y be Point of (TOP-REAL 3); :: according to LATTICE7:def_1 ::_thesis: ( not y in g .: (Ws /\ Wc) or y in V ) assume y in g .: (Ws /\ Wc) ; ::_thesis: y in V then consider x being Element of R^1 such that A26: x in Ws /\ Wc and A27: y = g . x by FUNCT_2:65; A28: g . x = |[((cR * l) . x),((sR * l) . x),0]| by Lm12; x in Ws by A26, XBOOLE_0:def_4; then A29: (sR * l) . x in (sR * l) .: Ws by FUNCT_2:35; x in Wc by A26, XBOOLE_0:def_4; then A30: (cR * l) . x in (cR * l) .: Wc by FUNCT_2:35; |[((cR * l) . x),((sR * l) . x),0]| = (1,2,3) --> (((cR * l) . x),((sR * l) . x),0) by Th30; then |[((cR * l) . x),((sR * l) . x),0]| in product ((1,2,3) --> (].(((g . p) `1) - (r / (sqrt 2))),(((g . p) `1) + (r / (sqrt 2))).[,].(((g . p) `2) - (r / (sqrt 2))),(((g . p) `2) + (r / (sqrt 2))).[,{0})) by A20, A25, A29, A30, Lm2, Lm6, Th33; then |[((cR * l) . x),((sR * l) . x),0]| in Ball (e,r) by A14; hence y in V by A11, A27, A28; ::_thesis: verum end; then g is continuous by JGRAPH_2:10; hence SphereMap is continuous by PRE_TOPC:27; ::_thesis: verum end; end; definition let r be real number ; func eLoop r -> Function of I[01],(Tunit_circle 3) means :Def8: :: BORSUK_7:def 8 for x being Point of I[01] holds it . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]|; existence ex b1 being Function of I[01],(Tunit_circle 3) st for x being Point of I[01] holds b1 . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| proof defpred S1[ real number , set ] means $2 = |[(cos (((2 * PI) * r) * $1)),(sin (((2 * PI) * r) * $1)),0]|; A1: for x being Element of I[01] ex y being Element of (Tunit_circle 3) st S1[x,y] proof let x be Element of I[01]; ::_thesis: ex y being Element of (Tunit_circle 3) st S1[x,y] set y = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]|; |.(|[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| - |[0,0,0]|).| = |.|[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]|.| by EUCLID_5:4, RLVECT_1:13 .= sqrt ((((|[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| `1) ^2) + ((|[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| `2) ^2)) + ((|[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| `3) ^2)) by Th35 .= sqrt ((((cos (((2 * PI) * r) * x)) ^2) + ((|[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| `2) ^2)) + ((|[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| `3) ^2)) by EUCLID_5:2 .= sqrt ((((cos (((2 * PI) * r) * x)) ^2) + ((sin (((2 * PI) * r) * x)) ^2)) + ((|[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| `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 = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| as Element of (Tunit_circle 3) by Lm7, TOPREAL9:9; take y ; ::_thesis: S1[x,y] thus S1[x,y] ; ::_thesis: verum end; ex f being Function of the carrier of I[01],(Tunit_circle 3) st for x being Element of I[01] holds S1[x,f . x] from FUNCT_2:sch_3(A1); hence ex b1 being Function of I[01],(Tunit_circle 3) st for x being Point of I[01] holds b1 . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| ; ::_thesis: verum end; uniqueness for b1, b2 being Function of I[01],(Tunit_circle 3) st ( for x being Point of I[01] holds b1 . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| ) & ( for x being Point of I[01] holds b2 . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| ) holds b1 = b2 proof let f, g be Function of I[01],(Tunit_circle 3); ::_thesis: ( ( for x being Point of I[01] holds f . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| ) & ( for x being Point of I[01] holds g . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| ) implies f = g ) assume that A2: for x being Point of I[01] holds f . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| and A3: for x being Point of I[01] holds g . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| ; ::_thesis: f = g let x be Point of I[01]; :: according to FUNCT_2:def_8 ::_thesis: f . x = g . x thus f . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| by A2 .= g . x by A3 ; ::_thesis: verum end; end; :: deftheorem Def8 defines eLoop BORSUK_7:def_8_:_ for r being real number for b2 being Function of I[01],(Tunit_circle 3) holds ( b2 = eLoop r iff for x being Point of I[01] holds b2 . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| ); theorem Th62: :: BORSUK_7:62 for r being real number holds eLoop r = SphereMap * (ExtendInt r) proof let r be real number ; ::_thesis: eLoop r = SphereMap * (ExtendInt r) let x be Point of I[01]; :: according to FUNCT_2:def_8 ::_thesis: (eLoop r) . x = (SphereMap * (ExtendInt r)) . x 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 Def8 .= |[(cos ((2 * PI) * ((ExtendInt r) . x))),(sin ((2 * PI) * ((ExtendInt r) . x))),0]| by A1 .= SphereMap . ((ExtendInt r) . x) by Def7 .= (SphereMap * (ExtendInt r)) . x by FUNCT_2:15 ; ::_thesis: verum end; definition let i be Integer; :: original: eLoop redefine func eLoop i -> Loop of c[100] ; coherence eLoop i is Loop of c[100] proof set f = eLoop i; thus c[100] , c[100] are_connected ; :: according to BORSUK_2:def_2 ::_thesis: ( eLoop i is continuous & (eLoop i) . 0 = c[100] & (eLoop i) . 1 = c[100] ) eLoop i = SphereMap * (ExtendInt i) by Th62; hence eLoop i is continuous ; ::_thesis: ( (eLoop i) . 0 = c[100] & (eLoop i) . 1 = c[100] ) thus (eLoop i) . 0 = |[(cos (((2 * PI) * i) * j0)),(sin (((2 * PI) * i) * j0)),0]| by Def8 .= c[100] by SIN_COS:31 ; ::_thesis: (eLoop i) . 1 = c[100] thus (eLoop i) . 1 = |[(cos (((2 * PI) * i) * j1)),(sin (((2 * PI) * i) * j1)),0]| by Def8 .= |[(cos 0),(sin (((2 * PI) * i) + Q)),0]| by COMPLEX2:9 .= c[100] by COMPLEX2:8, SIN_COS:31 ; ::_thesis: verum end; end; registration let i be Integer; cluster eLoop i -> nullhomotopic for Loop of c[100] ; coherence for b1 being Loop of c[100] st b1 = eLoop i holds b1 is nullhomotopic proof Tunit_circle 3 is having_trivial_Fundamental_Group by TOPALG_6:47; hence for b1 being Loop of c[100] st b1 = eLoop i holds b1 is nullhomotopic ; ::_thesis: verum end; end; theorem Th63: :: 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 let n be Nat; ::_thesis: for p being Point of (TOP-REAL n) st p <> 0. (TOP-REAL n) holds |.(p (/) |.p.|).| = 1 let p be Point of (TOP-REAL n); ::_thesis: ( p <> 0. (TOP-REAL n) implies |.(p (/) |.p.|).| = 1 ) A1: |.p.| ^2 = Sum (sqr p) by TOPREAL9:5; assume p <> 0. (TOP-REAL n) ; ::_thesis: |.(p (/) |.p.|).| = 1 then |.p.| <> 0 by EUCLID_2:42; then Sum ((sqr p) (/) (Sum (sqr p))) = 1 by A1, Th20; hence |.(p (/) |.p.|).| = 1 by A1, Th19, SQUARE_1:18; ::_thesis: verum 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 :Def9: :: BORSUK_7:def 9 p (/) |.p.|; coherence p (/) |.p.| is Point of (Tcircle ((0. (TOP-REAL n)),1)) proof A2: n in NAT by ORDINAL1:def_12; |.((p (/) |.p.|) - (0. (TOP-REAL n))).| = |.(p (/) |.p.|).| by RLVECT_1:13 .= 1 by A1, Th63 ; then p (/) |.p.| in Sphere ((0. (TOP-REAL n)),1) by A2, TOPREAL9:9; hence p (/) |.p.| is Point of (Tcircle ((0. (TOP-REAL n)),1)) by A2, TOPREALB:9; ::_thesis: verum end; end; :: deftheorem Def9 defines Rn->S1 BORSUK_7:def_9_:_ for n being Nat for p being Point of (TOP-REAL n) st p <> 0. (TOP-REAL n) holds Rn->S1 p = p (/) |.p.|; 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 :Def10: :: BORSUK_7:def 10 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)); existence ex b1 being Function of (Tunit_circle (n + 1)),(Tunit_circle n) st for x, y being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st y = - x holds b1 . x = Rn->S1 ((f . x) - (f . y)) proof defpred S1[ Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)), set ] means for y being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st y = - $1 holds $2 = Rn->S1 ((f . $1) - (f . y)); A1: for x being Element of (Tcircle ((0. (TOP-REAL (n + 1))),1)) ex z being Element of (Tunit_circle n) st S1[x,z] proof let x be Element of (Tcircle ((0. (TOP-REAL (n + 1))),1)); ::_thesis: ex z being Element of (Tunit_circle n) st S1[x,z] reconsider y = - x as Element of (Tcircle ((0. (TOP-REAL (n + 1))),1)) by TOPREALC:60; reconsider z = Rn->S1 ((f . x) - (f . y)) as Point of (Tunit_circle n) ; take z ; ::_thesis: S1[x,z] thus S1[x,z] ; ::_thesis: verum end; ex g being Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(Tunit_circle n) st for x being Element of (Tcircle ((0. (TOP-REAL (n + 1))),1)) holds S1[x,g . x] from FUNCT_2:sch_3(A1); hence ex b1 being Function of (Tunit_circle (n + 1)),(Tunit_circle n) st for x, y being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st y = - x holds b1 . x = Rn->S1 ((f . x) - (f . y)) ; ::_thesis: verum end; uniqueness for b1, b2 being Function of (Tunit_circle (n + 1)),(Tunit_circle n) st ( for x, y being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st y = - x holds b1 . x = Rn->S1 ((f . x) - (f . y)) ) & ( for x, y being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st y = - x holds b2 . x = Rn->S1 ((f . x) - (f . y)) ) holds b1 = b2 proof let F, G be Function of (Tunit_circle (n + 1)),(Tunit_circle n); ::_thesis: ( ( for x, y being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st y = - x holds F . x = Rn->S1 ((f . x) - (f . y)) ) & ( for x, y being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st y = - x holds G . x = Rn->S1 ((f . x) - (f . y)) ) implies F = G ) assume that A2: for x, y being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st y = - x holds F . x = Rn->S1 ((f . x) - (f . y)) and A3: for x, y being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st y = - x holds G . x = Rn->S1 ((f . x) - (f . y)) ; ::_thesis: F = G let p be Point of (Tunit_circle (n + 1)); :: according to FUNCT_2:def_8 ::_thesis: F . p = G . p reconsider p2 = p as Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) ; reconsider p1 = - p as Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) by TOPREALC:60; thus F . p = Rn->S1 ((f . p2) - (f . p1)) by A2 .= G . p by A3 ; ::_thesis: verum end; end; :: deftheorem Def10 defines Sn1->Sn BORSUK_7:def_10_:_ for n being non zero Nat for f being Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n) for b3 being Function of (Tunit_circle (n + 1)),(Tunit_circle n) holds ( b3 = Sn1->Sn f iff for x, y being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st y = - x holds b3 . x = Rn->S1 ((f . x) - (f . y)) ); 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 :Def11: :: BORSUK_7:def 11 ( 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 ex b1 being Function of I[01],R^1 st ( b1 . 0 = xt & f = CircleMap * b1 & b1 is continuous & ( for f1 being Function of I[01],R^1 st f1 is continuous & f = CircleMap * f1 & f1 . 0 = xt holds b1 = f1 ) ) by A1, TOPALG_5:23; uniqueness for b1, b2 being Function of I[01],R^1 st b1 . 0 = xt & f = CircleMap * b1 & b1 is continuous & ( for f1 being Function of I[01],R^1 st f1 is continuous & f = CircleMap * f1 & f1 . 0 = xt holds b1 = f1 ) & b2 . 0 = xt & f = CircleMap * b2 & b2 is continuous & ( for f1 being Function of I[01],R^1 st f1 is continuous & f = CircleMap * f1 & f1 . 0 = xt holds b2 = f1 ) holds b1 = b2 ; end; :: deftheorem Def11 defines liftPath BORSUK_7:def_11_:_ for x0, y0 being Point of (Tunit_circle 2) for xt being set for f being Path of x0,y0 st xt in CircleMap " {x0} holds for b5 being Function of I[01],R^1 holds ( b5 = liftPath (f,xt) iff ( b5 . 0 = xt & f = CircleMap * b5 & b5 is continuous & ( for f1 being Function of I[01],R^1 st f1 is continuous & f = CircleMap * f1 & f1 . 0 = xt holds b5 = f1 ) ) ); definition let n be Nat; let p, x, y be Point of (TOP-REAL n); let r be real number ; predx,y are_antipodals_of p,r means :Def12: :: BORSUK_7:def 12 ( x is Point of (Tcircle (p,r)) & y is Point of (Tcircle (p,r)) & p in LSeg (x,y) ); end; :: deftheorem Def12 defines are_antipodals_of BORSUK_7:def_12_:_ for n being Nat for p, x, y being Point of (TOP-REAL n) for r being real number holds ( x,y are_antipodals_of p,r iff ( x is Point of (Tcircle (p,r)) & y is Point of (Tcircle (p,r)) & p in LSeg (x,y) ) ); definition let n be Nat; let p, x, y be Point of (TOP-REAL n); let r be real number ; let f be Function; predx,y are_antipodals_of p,r,f means :Def13: :: BORSUK_7:def 13 ( x,y are_antipodals_of p,r & x in dom f & y in dom f & f . x = f . y ); end; :: deftheorem Def13 defines are_antipodals_of BORSUK_7:def_13_:_ for n being Nat for p, x, y being Point of (TOP-REAL n) for r being real number for f being Function holds ( x,y are_antipodals_of p,r,f iff ( x,y are_antipodals_of p,r & x in dom f & y in dom f & f . x = f . y ) ); definition let m, n be Nat; let p be Point of (TOP-REAL m); let r be real number ; let f be Function of (Tcircle (p,r)),(TOP-REAL n); attrf is with_antipodals means :Def14: :: BORSUK_7:def 14 ex x, y being Point of (TOP-REAL m) st x,y are_antipodals_of p,r,f; end; :: deftheorem Def14 defines with_antipodals BORSUK_7:def_14_:_ for m, n being Nat for p being Point of (TOP-REAL m) for r being real number for f being Function of (Tcircle (p,r)),(TOP-REAL n) holds ( f is with_antipodals iff ex x, y being Point of (TOP-REAL m) st x,y are_antipodals_of p,r,f ); notation let m, n be Nat; let p be Point of (TOP-REAL m); let r be real number ; let f be Function of (Tcircle (p,r)),(TOP-REAL n); antonym without_antipodals f for with_antipodals ; end; theorem Th64: :: BORSUK_7:64 for n being non empty Nat for r being real non negative number 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 let n be non empty Nat; ::_thesis: for r being real non negative number 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 let r be real non negative number ; ::_thesis: 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 let x be Point of (TOP-REAL n); ::_thesis: ( x is Point of (Tcircle ((0. (TOP-REAL n)),r)) implies x, - x are_antipodals_of 0. (TOP-REAL n),r ) assume A1: x is Point of (Tcircle ((0. (TOP-REAL n)),r)) ; ::_thesis: x, - x are_antipodals_of 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; :: according to BORSUK_7:def_12 ::_thesis: 0. (TOP-REAL n) in LSeg (x,(- x)) ((1 - (1 / 2)) * x) + ((1 / 2) * (- x)) = ((1 / 2) * x) + (- ((1 / 2) * x)) by EUCLID:40 .= 0. (TOP-REAL n) by EUCLID:36 ; hence 0. (TOP-REAL n) in LSeg (x,(- x)) ; ::_thesis: verum end; theorem Th65: :: BORSUK_7:65 for n being non empty Nat for p, x, y, x1, y1 being Point of (TOP-REAL n) for r being real positive number 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 empty Nat; ::_thesis: for p, x, y, x1, y1 being Point of (TOP-REAL n) for r being real positive number 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 let p, x, y, x1, y1 be Point of (TOP-REAL n); ::_thesis: for r being real positive number 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 let r be real positive number ; ::_thesis: ( x,y are_antipodals_of 0. (TOP-REAL n),1 & x1 = (CircleIso (p,r)) . x & y1 = (CircleIso (p,r)) . y implies x1,y1 are_antipodals_of p,r ) set h = CircleIso (p,r); assume that A1: x,y are_antipodals_of 0. (TOP-REAL n),1 and A2: x1 = (CircleIso (p,r)) . x and A3: y1 = (CircleIso (p,r)) . y ; ::_thesis: x1,y1 are_antipodals_of p,r A4: x is Point of (Tcircle ((0. (TOP-REAL n)),1)) by A1, Def12; hence x1 is Point of (Tcircle (p,r)) by A2, FUNCT_2:5; :: according to BORSUK_7:def_12 ::_thesis: ( y1 is Point of (Tcircle (p,r)) & p in LSeg (x1,y1) ) A5: y is Point of (Tcircle ((0. (TOP-REAL n)),1)) by A1, Def12; hence y1 is Point of (Tcircle (p,r)) by A3, FUNCT_2:5; ::_thesis: p in LSeg (x1,y1) 0. (TOP-REAL n) in LSeg (x,y) by A1, Def12; then consider a being 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, Def6 .= ((1 - a) * (r * x)) + ((1 - a) * p) by EUCLID:32 .= ((r * (1 - a)) * x) + ((1 - a) * p) by EUCLID:30 .= (r * ((1 - a) * x)) + ((1 - a) * p) by EUCLID:30 ; a * y1 = a * ((r * y) + p) by A3, A5, Def6 .= (a * (r * y)) + (a * p) by EUCLID:32 .= ((r * a) * y) + (a * p) by EUCLID:30 .= (r * (a * y)) + (a * p) by EUCLID:30 ; then ((1 - a) * x1) + (a * y1) = (((r * ((1 - a) * x)) + ((1 - a) * p)) + (r * (a * y))) + (a * p) by A8, EUCLID:26 .= (((r * ((1 - a) * x)) + (r * (a * y))) + ((1 - a) * p)) + (a * p) by EUCLID:26 .= ((r * (((1 - a) * x) + (a * y))) + ((1 - a) * p)) + (a * p) by EUCLID:32 .= ((0. (TOP-REAL n)) + ((1 - a) * p)) + (a * p) by A6, EUCLID:28 .= ((1 - a) * p) + (a * p) by EUCLID:27 .= ((1 * p) - (a * p)) + (a * p) by EUCLID:50 .= 1 * p by EUCLID:48 .= p by EUCLID:29 ; hence p in LSeg (x1,y1) by A7; ::_thesis: verum end; theorem Th66: :: 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 let n be non zero Nat; ::_thesis: 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) set TC4 = Tcircle ((0. (TOP-REAL (n + 1))),1); let f be Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n); ::_thesis: 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) let x be Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)); ::_thesis: ( f is without_antipodals implies (f . x) - (f . (- x)) <> 0. (TOP-REAL n) ) assume A1: f is without_antipodals ; ::_thesis: (f . x) - (f . (- x)) <> 0. (TOP-REAL n) A2: dom f = the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),1)) by FUNCT_2:def_1; reconsider y = - x as Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) by TOPREALC:60; reconsider a = x, b = y as Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) ; reconsider x1 = x as Point of (TOP-REAL (n + 1)) by PRE_TOPC:25; assume A3: (f . x) - (f . (- x)) = 0. (TOP-REAL n) ; ::_thesis: contradiction 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 Th64; :: according to BORSUK_7:def_13 ::_thesis: ( x1 in dom f & - x1 in dom f & f . x1 = f . (- x1) ) ( f . x = f . a & f . y = f . b ) ; hence ( x1 in dom f & - x1 in dom f ) by A2; ::_thesis: f . x1 = f . (- x1) (f . a) - (f . y) = 0. (TOP-REAL n) by A3; hence f . x1 = f . (- x1) by EUCLID:43; ::_thesis: verum end; hence contradiction by A1, Def14; ::_thesis: verum end; theorem Th67: :: 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 let n be non zero Nat; ::_thesis: 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 set TC4 = Tcircle ((0. (TOP-REAL (n + 1))),1); let f be Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n); ::_thesis: ( f is without_antipodals implies Sn1->Sn f is odd ) assume A1: f is without_antipodals ; ::_thesis: Sn1->Sn f is odd set g = Sn1->Sn f; let x, y be complex-valued Function; :: according to BORSUK_7:def_2 ::_thesis: ( x in dom (Sn1->Sn f) & - x in dom (Sn1->Sn f) & y = (Sn1->Sn f) . x implies (Sn1->Sn f) . (- x) = - y ) assume that A2: x in dom (Sn1->Sn f) and A3: - x in dom (Sn1->Sn f) and A4: y = (Sn1->Sn f) . x ; ::_thesis: (Sn1->Sn f) . (- x) = - y reconsider b = - x as Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) by A3; reconsider a = - b as Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) by A2; set p = (f . b) - (f . a); set q = (f . a) - (f . b); A5: (f . b) - (f . a) = - ((f . a) - (f . b)) by EUCLID:44; A6: n in NAT by ORDINAL1:def_12; 0. (TOP-REAL n) = 0* n by EUCLID:70; then A7: - ((f . b) - (f . a)) <> 0. (TOP-REAL n) by A1, Th66, Th15; thus (Sn1->Sn f) . (- x) = Rn->S1 ((f . b) - (f . a)) by Def10 .= ((f . b) - (f . a)) (/) |.((f . b) - (f . a)).| by A1, Th66, Def9 .= ((f . b) - (f . a)) (/) |.(- ((f . a) - (f . b))).| by EUCLID:44 .= (- ((f . a) - (f . b))) (/) |.(- ((f . a) - (f . b))).| by EUCLID:44 .= - (((f . a) - (f . b)) (/) |.(- ((f . a) - (f . b))).|) by VALUED_2:30 .= - (((f . a) - (f . b)) (/) |.((f . a) - (f . b)).|) by A6, TOPRNS_1:26 .= - (Rn->S1 ((f . a) - (f . b))) by A5, A7, Def9 .= - y by A4, Def10 ; ::_thesis: verum end; theorem Th68: :: 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 let n be non zero Nat; ::_thesis: 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) let f be Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n); ::_thesis: for 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) let g, B1 be Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n); ::_thesis: ( g = f (-) & B1 = f <--> g & f is without_antipodals implies Sn1->Sn f = B1 ((n NormF) * B1) ) assume that A1: g = f (-) and A2: B1 = f <--> g and A3: f is without_antipodals ; ::_thesis: Sn1->Sn f = B1 ((n NormF) * B1) set T = Tcircle ((0. (TOP-REAL (n + 1))),1); set B = Sn1->Sn f; set B2 = (n NormF) * B1; set BB = B1 ((n NormF) * B1); set TC3 = Tunit_circle (n + 1); A4: dom B1 = the carrier of (Tunit_circle (n + 1)) 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 ((n NormF) * B1) = dom B1 by RELAT_1:27; A6: dom (B1 ((n NormF) * B1)) = (dom B1) /\ (dom ((n NormF) * B1)) by VALUED_2:71 .= the carrier of (Tunit_circle (n + 1)) by A5, FUNCT_2:def_1 ; hence dom (Sn1->Sn f) = dom (B1 ((n NormF) * B1)) by FUNCT_2:def_1; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds ( not b1 in dom (Sn1->Sn f) or (Sn1->Sn f) . b1 = (B1 ((n NormF) * B1)) . b1 ) let x be set ; ::_thesis: ( not x in dom (Sn1->Sn f) or (Sn1->Sn f) . x = (B1 ((n NormF) * B1)) . x ) assume x in dom (Sn1->Sn f) ; ::_thesis: (Sn1->Sn f) . x = (B1 ((n NormF) * B1)) . x then reconsider x1 = x as Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) ; reconsider y1 = - x1 as Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) by TOPREALC:60; set p = (f . x1) - (f . y1); A7: dom g = the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),1)) by FUNCT_2:def_1; A8: B1 . x1 = (f . x1) - (g . x1) by A4, A2, VALUED_2:def_46 .= (f . x1) - (f . y1) by A7, A1, VALUED_2:def_34 ; A9: ((n NormF) * B1) . x1 = (n NormF) . (B1 . x1) by FUNCT_2:15 .= |.((f . x1) - (f . y1)).| by A8, JGRAPH_4:def_1 ; (Sn1->Sn f) . x1 = Rn->S1 ((f . x1) - (f . y1)) by Def10 .= (B1 . x1) (/) (((n NormF) * B1) . x1) by A8, A9, A3, Th66, Def9 .= (B1 . x1) (#) ((((n NormF) * B1) ") . x1) by VALUED_1:10 .= (B1 ((n NormF) * B1)) . x1 by A6, VALUED_2:def_43 ; hence (Sn1->Sn f) . x = (B1 ((n NormF) * B1)) . x ; ::_thesis: verum 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 let n be non zero Nat; ::_thesis: 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 set T = Tcircle ((0. (TOP-REAL (n + 1))),1); let f be Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n); ::_thesis: ( f is without_antipodals & f is continuous implies Sn1->Sn f is continuous ) assume that A1: f is without_antipodals and A2: f is continuous ; ::_thesis: Sn1->Sn f is continuous set B = Sn1->Sn f; reconsider g = f (-) as Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n) by TOPREALC:61; reconsider B1 = f <--> g as Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n) by TOPREALC:40; set B2 = (n NormF) * B1; A3: dom g = the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),1)) by FUNCT_2:def_1; A4: dom B1 = the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),1)) by FUNCT_2:def_1; A5: now__::_thesis:_for_t_being_Point_of_(Tcircle_((0._(TOP-REAL_(n_+_1))),1))_holds_((n_NormF)_*_B1)_._t_=_|.(B1_._t).| let t be Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)); ::_thesis: ((n NormF) * B1) . t = |.(B1 . t).| thus ((n NormF) * B1) . t = (n NormF) . (B1 . t) by FUNCT_2:15 .= |.(B1 . t).| by JGRAPH_4:def_1 ; ::_thesis: verum end; A6: now__::_thesis:_for_t_being_Point_of_(Tcircle_((0._(TOP-REAL_(n_+_1))),1))_holds_|.(B1_._t).|_<>_0 let t be Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)); ::_thesis: |.(B1 . t).| <> 0 A7: n in NAT by ORDINAL1:def_12; A8: B1 . t = (f . t) - (g . t) by A4, VALUED_2:def_46 .= (f . t) - (f . (- t)) by A3, VALUED_2:def_34 ; (f . t) - (f . (- t)) <> 0. (TOP-REAL n) by A1, Th66; hence |.(B1 . t).| <> 0 by A8, A7, TOPRNS_1:24; ::_thesis: verum end; A9: (n NormF) * B1 is non-empty proof let x be set ; :: according to FUNCT_1:def_9 ::_thesis: ( not x in dom ((n NormF) * B1) or not ((n NormF) * B1) . x is empty ) assume x in dom ((n NormF) * B1) ; ::_thesis: not ((n NormF) * B1) . x is empty then reconsider x = x as Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) ; ((n NormF) * B1) . x = |.(B1 . x).| by A5; hence not ((n NormF) * B1) . x is empty by A6; ::_thesis: verum end; A10: g is continuous Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n) by A2, TOPREALC:62; B1 ((n NormF) * B1) is Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n) by TOPREALC:46; hence Sn1->Sn f is continuous by A1, Th68, TOPMETR:6, A9, A2, A10; ::_thesis: verum end; deffunc H1( 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 number 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 H1(f) . (s + (1 / 2)) = - (H1(f) . s) proof let s be real number ; ::_thesis: 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 H1(f) . (s + (1 / 2)) = - (H1(f) . s) let f be Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2); ::_thesis: ( f is without_antipodals & 0 <= s & s <= 1 / 2 implies H1(f) . (s + (1 / 2)) = - (H1(f) . s) ) set l = eLoop 1; set g = Sn1->Sn f; set t = s + (1 / 2); assume f is without_antipodals ; ::_thesis: ( not 0 <= s or not s <= 1 / 2 or H1(f) . (s + (1 / 2)) = - (H1(f) . s) ) then A1: Sn1->Sn f is odd by Th67; assume A2: ( 0 <= s & s <= 1 / 2 ) ; ::_thesis: H1(f) . (s + (1 / 2)) = - (H1(f) . s) then A3: s + (1 / 2) in the carrier of I[01] by Lm4; reconsider s1 = s as Point of I[01] by A2, Lm3; A4: dom (Sn1->Sn f) = the carrier of (Tunit_circle (2 + 1)) by FUNCT_2:def_1; A5: - ((eLoop 1) . s1) is Point of (Tcircle ((0. (TOP-REAL 3)),1)) by TOPREALC:60; A6: (eLoop 1) . (s + (1 / 2)) = |[(cos (((2 * PI) * 1) * (s + (1 / 2)))),(sin (((2 * PI) * 1) * (s + (1 / 2)))),0]| by A3, Def8 .= |[(- (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 .= - ((eLoop 1) . s1) by Def8 ; thus H1(f) . (s + (1 / 2)) = (Sn1->Sn f) . ((eLoop 1) . (s + (1 / 2))) by A2, Lm4, FUNCT_2:15 .= - ((Sn1->Sn f) . ((eLoop 1) . s1)) by A1, A4, A5, A6, Def2 .= - (H1(f) . s1) by FUNCT_2:15 .= - (H1(f) . s) ; ::_thesis: verum end; defpred S1[ Point of R^1, Point of R^1, Integer] means $1 = $2 + ($3 / 2); Lm15: now__::_thesis:_for_a,_b_being_Point_of_R^1_st_CircleMap_._a_=_-_(CircleMap_._b)_holds_ ex_I_being_odd_Integer_st_S1[a,b,I] let a, b be Point of R^1; ::_thesis: ( CircleMap . a = - (CircleMap . b) implies ex I being odd Integer st S1[a,b,I] ) assume A1: CircleMap . a = - (CircleMap . b) ; ::_thesis: ex I being odd Integer st S1[a,b,I] thus ex I being odd Integer st S1[a,b,I] ::_thesis: verum proof 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: S1[a,b,I] thus S1[a,b,I] by A6; ::_thesis: verum end; 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 H1(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); ::_thesis: ( f is without_antipodals & f is continuous implies H1(f) is nullhomotopic Loop of (Sn1->Sn f) . c100a ) assume ( f is without_antipodals & f is continuous ) ; ::_thesis: H1(f) is nullhomotopic Loop of (Sn1->Sn f) . c100a then reconsider g = Sn1->Sn f as continuous Function of (Tunit_circle 3),(Tunit_circle 2) by Lm13; H1(f) = g * (eLoop 1) ; hence H1(f) is nullhomotopic Loop of (Sn1->Sn f) . c100a ; ::_thesis: verum end; Lm17: now__::_thesis:_for_f_being_Function_of_(Tcircle_((0._(TOP-REAL_(2_+_1))),1)),(TOP-REAL_2) for_s_being_real_number_ for_xt_being_set_st_f_is_without_antipodals_&_f_is_continuous_&_xt_in_CircleMap_"_{((Sn1->Sn_f)_._c[100])}_&_0_<=_s_&_s_<=_1_/_2_holds_ ex_IT_being_odd_Integer_st_ for_L_being_Loop_of_(Sn1->Sn_f)_._c100a_st_L_=_H1(f)_holds_ (liftPath_(L,xt))_._(s_+_(1_/_2))_=_((liftPath_(L,xt))_._s)_+_(IT_/_2) let f be Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2); ::_thesis: for s being real number for xt being set st f is without_antipodals & f is continuous & xt in CircleMap " {((Sn1->Sn f) . c[100])} & 0 <= s & s <= 1 / 2 holds ex IT being odd Integer st for L being Loop of (Sn1->Sn f) . c100a st L = H1(f) holds (liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (IT / 2) let s be real number ; ::_thesis: for xt being set st f is without_antipodals & f is continuous & xt in CircleMap " {((Sn1->Sn f) . c[100])} & 0 <= s & s <= 1 / 2 holds ex IT being odd Integer st for L being Loop of (Sn1->Sn f) . c100a st L = H1(f) holds (liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (IT / 2) let xt be set ; ::_thesis: ( f is without_antipodals & f is continuous & xt in CircleMap " {((Sn1->Sn f) . c[100])} & 0 <= s & s <= 1 / 2 implies ex IT being odd Integer st for L being Loop of (Sn1->Sn f) . c100a st L = H1(f) holds (liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (IT / 2) ) 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: ex IT being odd Integer st for L being Loop of (Sn1->Sn f) . c100a st L = H1(f) holds (liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (IT / 2) thus ex IT being odd Integer st for L being Loop of (Sn1->Sn f) . c100a st L = H1(f) holds (liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (IT / 2) ::_thesis: verum proof reconsider s = s as Point of I[01] by A3, Lm3; reconsider L = H1(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: H1(f) = CircleMap * (liftPath (L,xt)) by A2, Def11; ( (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: S1[(liftPath (L,xt)) . t1,(liftPath (L,xt)) . s,I] by Lm15; take I ; ::_thesis: for L being Loop of (Sn1->Sn f) . c100a st L = H1(f) holds (liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (I / 2) thus for L being Loop of (Sn1->Sn f) . c100a st L = H1(f) holds (liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (I / 2) by A5; ::_thesis: verum end; end; defpred S2[ 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 = H1($1) holds for s being real number st 0 <= s & s <= 1 / 2 holds (liftPath (L,$2)) . (s + (1 / 2)) = ((liftPath (L,$2)) . s) + ($3 / 2); Lm18: now__::_thesis:_for_f_being_Function_of_(Tcircle_((0._(TOP-REAL_(2_+_1))),1)),(TOP-REAL_2) for_xt_being_set_st_f_is_without_antipodals_&_f_is_continuous_&_xt_in_CircleMap_"_{((Sn1->Sn_f)_._c[100])}_holds_ ex_I_being_odd_Integer_st_S2[f,xt,I] let f be Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2); ::_thesis: for xt being set st f is without_antipodals & f is continuous & xt in CircleMap " {((Sn1->Sn f) . c[100])} holds ex I being odd Integer st S2[f,xt,I] let xt be set ; ::_thesis: ( f is without_antipodals & f is continuous & xt in CircleMap " {((Sn1->Sn f) . c[100])} implies ex I being odd Integer st S2[f,xt,I] ) assume that A1: ( f is without_antipodals & f is continuous ) and A2: xt in CircleMap " {((Sn1->Sn f) . c[100])} ; ::_thesis: ex I being odd Integer st S2[f,xt,I] reconsider L1 = H1(f) as Loop of (Sn1->Sn f) . c100a by A1, Lm16; thus ex I being odd Integer st S2[f,xt,I] ::_thesis: verum proof 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] proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]) or y in the carrier of I[01] ) assume y in rng ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]) ; ::_thesis: y in the carrier of I[01] then consider x being set 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 number 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: verum 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 = H1(f) holds (liftPath (L,xt)) . (j0 + (1 / 2)) = ((liftPath (L,xt)) . j0) + (ITj0 / 2) by A1, A2, Lm17; take ITj0 ; ::_thesis: S2[f,xt,ITj0] let L be Loop of (Sn1->Sn f) . c100a; ::_thesis: ( L = H1(f) implies for s being real number st 0 <= s & s <= 1 / 2 holds (liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (ITj0 / 2) ) assume A12: L = H1(f) ; ::_thesis: for s being real number st 0 <= s & s <= 1 / 2 holds (liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (ITj0 / 2) let s be real number ; ::_thesis: ( 0 <= s & s <= 1 / 2 implies (liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (ITj0 / 2) ) assume A13: ( 0 <= s & s <= 1 / 2 ) ; ::_thesis: (liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (ITj0 / 2) 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 = H1(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 proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng W or y in INT ) assume y in rng W ; ::_thesis: y in INT then consider s being set such that A24: s in dom W and A25: W . s = y by FUNCT_1:def_3; reconsider s = s as real number by A24; A26: ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]) . s = (AffineMap (1,(1 / 2))) . 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 being odd Integer such that A27: for L being Loop of (Sn1->Sn f) . c100a st L = H1(f) holds (liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (ITs / 2) by A1, A2, Lm17; A28: (liftPath (L1,xt)) . (s + (1 / 2)) = ((liftPath (L1,xt)) . s) + (ITs / 2) by A27; 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 A10, A24, VALUED_1:13 .= 2 * (((liftPath (L1,xt)) . (s + (1 / 2))) - ((liftPath (L1,xt)) . s)) by A26, A3, A9, A10, A24, FUNCT_1:13 .= 2 * (ITs / 2) by A28 ; hence y in INT by A25, INT_1:def_2; ::_thesis: verum end; set T = Closed-Interval-TSpace (0,(1 / 2)); A29: the carrier of (Closed-Interval-TSpace (0,(1 / 2))) = [.0,(1 / 2).] by TOPMETR:18; A30: rng W c= RAT by A23, NUMBERS:14, XBOOLE_1:1; reconsider SR = RAT as Subset of R^1 by NUMBERS:12, TOPMETR:17; reconsider W1 = W as Function of (Closed-Interval-TSpace (0,(1 / 2))),(R^1 | SR) by A10, A9, Lm8, A29, A23, FUNCT_2:2, NUMBERS:14, XBOOLE_1:1; A31: Closed-Interval-TSpace (0,(1 / 2)) is connected by TREAL_1:20; A32: R^1 | (R^1 (dom W)) = Closed-Interval-TSpace (0,(1 / 2)) by A10, A9, A29, PRE_TOPC:8, TSEP_1:5; reconsider f1 = R^1 ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]) as Function of (Closed-Interval-TSpace (0,(1 / 2))),I[01] by A5, A3, A29, FUNCT_2:2; rng (liftPath (L1,xt)) c= REAL by TOPMETR:17; then reconsider ll1 = liftPath (L1,xt) as PartFunc of REAL,REAL by A4, BORSUK_1:40, RELSET_1:4; liftPath (L1,xt) is continuous by A2, Def11; then A33: ll1 is continuous by Th39, TOPMETR:20; (ll1 * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) - ll1 is continuous by A33; then reconsider W = 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 R^1 | (R^1 QQ) 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, Th38; hence (liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (ITj0 / 2) by A20, A12, A21, A22, A9, A10, A15, A14, FUNCT_1:def_10; ::_thesis: verum end; end; Lm19: for f being Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2) for xt being Point of R^1 for L being Loop of (Sn1->Sn f) . c100a st L = H1(f) holds for I being Integer st S2[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); ::_thesis: for xt being Point of R^1 for L being Loop of (Sn1->Sn f) . c100a st L = H1(f) holds for I being Integer st S2[f,xt,I] holds (liftPath (L,xt)) . 1 = ((liftPath (L,xt)) . 0) + I let xt be Point of R^1; ::_thesis: for L being Loop of (Sn1->Sn f) . c100a st L = H1(f) holds for I being Integer st S2[f,xt,I] holds (liftPath (L,xt)) . 1 = ((liftPath (L,xt)) . 0) + I let L be Loop of (Sn1->Sn f) . c100a; ::_thesis: ( L = H1(f) implies for I being Integer st S2[f,xt,I] holds (liftPath (L,xt)) . 1 = ((liftPath (L,xt)) . 0) + I ) assume A1: L = H1(f) ; ::_thesis: for I being Integer st S2[f,xt,I] holds (liftPath (L,xt)) . 1 = ((liftPath (L,xt)) . 0) + I let I be Integer; ::_thesis: ( S2[f,xt,I] implies (liftPath (L,xt)) . 1 = ((liftPath (L,xt)) . 0) + I ) assume A2: S2[f,xt,I] ; ::_thesis: (liftPath (L,xt)) . 1 = ((liftPath (L,xt)) . 0) + I set l = liftPath (L,xt); (1 / 2) + (1 / 2) = 1 ; hence (liftPath (L,xt)) . 1 = ((liftPath (L,xt)) . (Q + (1 / 2))) + (I / 2) by A1, A2 .= (((liftPath (L,xt)) . 0) + (I / 2)) + (I / 2) by A1, A2 .= ((liftPath (L,xt)) . 0) + I ; ::_thesis: verum end; Lm20: for f being Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2) st f is without_antipodals & f is continuous holds not H1(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); ::_thesis: ( f is without_antipodals & f is continuous implies not H1(f) is nullhomotopic Loop of (Sn1->Sn f) . c100a ) assume A1: ( f is without_antipodals & f is continuous ) ; ::_thesis: H1(f) is not nullhomotopic Loop of (Sn1->Sn f) . c100a then reconsider L = H1(f) as Loop of (Sn1->Sn f) . c100a by Lm16; set g = Sn1->Sn f; set s = (Sn1->Sn f) . c100a; not L is nullhomotopic proof let c be constant Loop of (Sn1->Sn f) . c100a; :: according to TOPALG_6:def_3 ::_thesis: not L,c are_homotopic rng CircleMap = the carrier of (Tunit_circle 2) by FUNCT_2:def_3; then consider xt being set such that A2: xt in the carrier of R^1 and A3: CircleMap . xt = (Sn1->Sn f) . c100a by FUNCT_2:11; reconsider xt = xt as Point of R^1 by A2; (Sn1->Sn f) . c100a in {((Sn1->Sn f) . c100a)} by TARSKI:def_1; then A4: xt in CircleMap " {((Sn1->Sn f) . c100a)} by A3, FUNCT_2:38; then consider q being odd Integer such that A5: S2[f,xt,q] by A1, Lm18; reconsider l = liftPath (L,xt) as continuous Function of I[01],R^1 by A4, Def11; A6: l . 1 = (l . 0) + q by A5, Lm19; A7: CircleMap . q = c[10] by TOPREALB:32; A8: CircleMap . 0 = c[10] by TOPREALB:32; set hh = l - xt; l - xt is Path of R^1 0, R^1 q proof thus l - xt is continuous ; :: according to BORSUK_2:def_4 ::_thesis: ( (l - xt) . 0 = R^1 0 & (l - xt) . 1 = R^1 q ) thus (l - xt) . 0 = (l . j0) - xt by VALUED_1:4 .= xt - xt by A4, Def11 .= R^1 0 ; ::_thesis: (l - xt) . 1 = R^1 q thus (l - xt) . 1 = (l . j1) - xt by VALUED_1:4 .= (xt + q) - xt by A6, A4, Def11 .= R^1 q ; ::_thesis: verum end; then reconsider hh = l - xt as Path of R^1 0, R^1 q ; reconsider Ch = CircleMap * hh as Loop of c[10] by A7, TOPREALB:32; reconsider X = I[01] --> xt as Loop of xt by JORDAN:41; set xx = X - xt; reconsider Cx = CircleMap * (X - xt) as Loop of c[10] by A8; A9: dom Ciso = the carrier of INT.Group by FUNCT_2:def_1; A10: Ciso . q = Class ((EqRel ((Tunit_circle 2),c[10])),(CircleMap * hh)) by TOPALG_5:25; A11: Ciso . 0 = Class ((EqRel ((Tunit_circle 2),c[10])),(CircleMap * (X - xt))) by TOPALG_5:25; Ciso . (@' 0) <> Ciso . (@' q) by A9, FUNCT_1:def_4; then A12: not Cx,Ch are_homotopic by A10, A11, TOPALG_1:46; assume L,c are_homotopic ; ::_thesis: contradiction then consider F being Function of [:I[01],I[01]:],(Tunit_circle 2) such that A13: F is continuous and A14: for t being Point of I[01] holds ( F . (t,0) = H1(f) . t & F . (t,1) = c . t & F . (0,t) = (Sn1->Sn f) . c100a & F . (1,t) = (Sn1->Sn f) . c100a ) by BORSUK_2:def_7; reconsider S = (Sn1->Sn f) . c100a as Point of (TOP-REAL 2) by PRE_TOPC:25; set A = - (Arg S); set H = RotateCircle (1,(- (Arg S))); set G = (RotateCircle (1,(- (Arg S)))) * F; A15: |.(euc2cpx S).| = |.S.| by EUCLID_3:25 .= 1 by TOPREALB:12 ; A16: Rotate ((euc2cpx S),(- (Arg S))) = |.(euc2cpx S).| by COMPLEX2:55; A17: (RotateCircle (1,(- (Arg S)))) . ((Sn1->Sn f) . c100a) = (Rotate (- (Arg S))) . S by FUNCT_1:49 .= c[10] by A16, A15, COMPLEX1:6, JORDAN24:def_3 ; now__::_thesis:_for_t_being_Point_of_I[01]_holds_ (_((RotateCircle_(1,(-_(Arg_S))))_*_F)_._(t,0)_=_Ch_._t_&_((RotateCircle_(1,(-_(Arg_S))))_*_F)_._(t,1)_=_Cx_._t_&_((RotateCircle_(1,(-_(Arg_S))))_*_F)_._(0,t)_=_c[10]_&_((RotateCircle_(1,(-_(Arg_S))))_*_F)_._(1,t)_=_c[10]_) let t be Point of I[01]; ::_thesis: ( ((RotateCircle (1,(- (Arg S)))) * F) . (t,0) = Ch . t & ((RotateCircle (1,(- (Arg S)))) * F) . (t,1) = Cx . t & ((RotateCircle (1,(- (Arg S)))) * F) . (0,t) = c[10] & ((RotateCircle (1,(- (Arg S)))) * F) . (1,t) = c[10] ) reconsider E = eLoop 1 as Function of I[01],(Tunit_circle (2 + 1)) ; reconsider BU = H1(f) as Function of I[01],(Tunit_circle 2) ; reconsider T = BU . t as Point of (TOP-REAL 2) by PRE_TOPC:25; H1(f) = CircleMap * l by A4, Def11; then A18: H1(f) . t = CircleMap . (l . t) by FUNCT_2:15; thus ((RotateCircle (1,(- (Arg S)))) * F) . (t,0) = (RotateCircle (1,(- (Arg S)))) . (F . (t,j0)) by Lm1, BINOP_1:18 .= (RotateCircle (1,(- (Arg S)))) . T by A14 .= CircleMap . ((l . t) - xt) by A3, A18, Th60 .= CircleMap . (hh . t) by VALUED_1:4 .= Ch . t by FUNCT_2:15 ; ::_thesis: ( ((RotateCircle (1,(- (Arg S)))) * F) . (t,1) = Cx . t & ((RotateCircle (1,(- (Arg S)))) * F) . (0,t) = c[10] & ((RotateCircle (1,(- (Arg S)))) * F) . (1,t) = c[10] ) thus ((RotateCircle (1,(- (Arg S)))) * F) . (t,1) = (RotateCircle (1,(- (Arg S)))) . (F . (t,j1)) by Lm1, BINOP_1:18 .= (RotateCircle (1,(- (Arg S)))) . (c . t) by A14 .= (RotateCircle (1,(- (Arg S)))) . ((Sn1->Sn f) . c100a) by TOPALG_3:21 .= CircleMap . (xt - xt) by A17, TOPREALB:32 .= CircleMap . ((X . t) - xt) by TOPALG_3:21 .= CircleMap . ((X - xt) . t) by VALUED_1:4 .= Cx . t by FUNCT_2:15 ; ::_thesis: ( ((RotateCircle (1,(- (Arg S)))) * F) . (0,t) = c[10] & ((RotateCircle (1,(- (Arg S)))) * F) . (1,t) = c[10] ) thus ((RotateCircle (1,(- (Arg S)))) * F) . (0,t) = (RotateCircle (1,(- (Arg S)))) . (F . (j0,t)) by Lm1, BINOP_1:18 .= c[10] by A14, A17 ; ::_thesis: ((RotateCircle (1,(- (Arg S)))) * F) . (1,t) = c[10] thus ((RotateCircle (1,(- (Arg S)))) * F) . (1,t) = (RotateCircle (1,(- (Arg S)))) . (F . (j1,t)) by Lm1, BINOP_1:18 .= c[10] by A14, A17 ; ::_thesis: verum end; hence contradiction by A12, A13, BORSUK_2:def_7; ::_thesis: verum end; hence H1(f) is not nullhomotopic Loop of (Sn1->Sn f) . c100a ; ::_thesis: verum end; Lm21: for f being 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)),(TOP-REAL 2); ::_thesis: f is with_antipodals assume A1: not f is with_antipodals ; ::_thesis: contradiction then H1(f) is not nullhomotopic Loop of (Sn1->Sn f) . c100a by Lm20; hence contradiction by A1, Lm16; ::_thesis: verum end; registration let n be non zero Nat; let r be real negative number ; let p be Point of (TOP-REAL (n + 1)); cluster Function-like quasi_total -> without_antipodals for Element of bool [: the carrier of (Tcircle (p,r)), the carrier of (TOP-REAL n):]; coherence for b1 being Function of (Tcircle (p,r)),(TOP-REAL n) holds b1 is without_antipodals proof let f be Function of (Tcircle (p,r)),(TOP-REAL n); ::_thesis: f is without_antipodals let x, y be Point of (TOP-REAL (n + 1)); :: according to BORSUK_7:def_14 ::_thesis: not x,y are_antipodals_of p,r,f not x in dom f ; hence not x,y are_antipodals_of p,r,f by Def13; ::_thesis: verum end; end; registration let r be real non negative number ; let p be Point of (TOP-REAL 3); cluster Function-like quasi_total continuous -> with_antipodals for Element of bool [: the carrier of (Tcircle (p,r)), the carrier of (TOP-REAL 2):]; coherence for b1 being Function of (Tcircle (p,r)),(TOP-REAL 2) st b1 is continuous holds b1 is with_antipodals proof let f be Function of (Tcircle (p,r)),(TOP-REAL 2); ::_thesis: ( f is continuous implies f is with_antipodals ) assume A1: f is continuous ; ::_thesis: f is with_antipodals A2: dom f = the carrier of (Tcircle (p,r)) by FUNCT_2:def_1; percases ( r is positive or r is zero ) ; suppose r is positive ; ::_thesis: f is with_antipodals then reconsider r1 = r as real positive number ; reconsider f1 = f as continuous Function of (Tcircle (p,r1)),(TOP-REAL 2) 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 being Point of (TOP-REAL 3) such that A3: x,y are_antipodals_of 0. (TOP-REAL 3),1,f1 * h by Def14; A4: x in dom (f * h) by A3, Def13; A5: y in dom (f * h) by A3, Def13; A6: (f * h) . x = (f * h) . y by A3, Def13; ( 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 ; :: according to BORSUK_7:def_14 ::_thesis: ex y being Point of (TOP-REAL 3) st hx,y are_antipodals_of p,r,f take hy ; ::_thesis: hx,hy are_antipodals_of p,r,f x,y are_antipodals_of 0. (TOP-REAL 3),1 by A3, Def13; hence hx,hy are_antipodals_of p,r by Th65; :: according to BORSUK_7:def_13 ::_thesis: ( hx in dom f & hy in dom f & f . hx = f . hy ) thus hx in dom f by A2, A4, FUNCT_2:5; ::_thesis: ( hy in dom f & f . hx = f . hy ) thus hy in dom f by A2, A5, FUNCT_2:5; ::_thesis: f . hx = f . hy thus f . hx = (f * h) . x by A4, FUNCT_2:15 .= f . hy by A5, A6, FUNCT_2:15 ; ::_thesis: verum end; supposeA7: r is zero ; ::_thesis: f is with_antipodals take p ; :: according to BORSUK_7:def_14 ::_thesis: ex y being Point of (TOP-REAL 3) st p,y are_antipodals_of p,r,f take p ; ::_thesis: p,p are_antipodals_of p,r,f 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 :: according to BORSUK_7:def_13 ::_thesis: ( p in dom f & p in dom f & f . p = f . p ) proof thus ( p is Point of (Tcircle (p,r)) & p is Point of (Tcircle (p,r)) ) by A8, TARSKI:def_1; :: according to BORSUK_7:def_12 ::_thesis: p in LSeg (p,p) thus p in LSeg (p,p) by RLTOPSP1:68; ::_thesis: verum end; thus ( p in dom f & p in dom f ) by A2, A8, TARSKI:def_1; ::_thesis: f . p = f . p thus f . p = f . p ; ::_thesis: verum end; end; end; end;