:: BROUWER2 semantic presentation begin Lm1: for n being Nat for p, q being Point of (TOP-REAL n) for r being real number holds (((1 - r) * p) + (r * q)) - p = r * (q - p) proof let n be Nat; ::_thesis: for p, q being Point of (TOP-REAL n) for r being real number holds (((1 - r) * p) + (r * q)) - p = r * (q - p) let p, q be Point of (TOP-REAL n); ::_thesis: for r being real number holds (((1 - r) * p) + (r * q)) - p = r * (q - p) let r be real number ; ::_thesis: (((1 - r) * p) + (r * q)) - p = r * (q - p) thus (((1 - r) * p) + (r * q)) - p = (r * q) + (((1 - r) * p) - p) by EUCLID:45 .= (r * q) + (((1 * p) - (r * p)) - p) by EUCLID:50 .= (r * q) + ((p - (r * p)) - p) by RLVECT_1:def_8 .= (r * q) + ((p + (- (r * p))) + (- p)) .= (r * q) + ((p + (- p)) + (- (r * p))) by EUCLID:26 .= (r * q) + ((p - p) - (r * p)) .= (r * q) + ((0. (TOP-REAL n)) - (r * p)) by RLVECT_1:15 .= (r * q) - (r * p) by RLVECT_1:14 .= r * (q - p) by EUCLID:49 ; ::_thesis: verum end; Lm2: for n being Nat for p being Point of (TOP-REAL n) for r being real number st r >= 0 holds r * p in halfline ((0. (TOP-REAL n)),p) proof let n be Nat; ::_thesis: for p being Point of (TOP-REAL n) for r being real number st r >= 0 holds r * p in halfline ((0. (TOP-REAL n)),p) let p be Point of (TOP-REAL n); ::_thesis: for r being real number st r >= 0 holds r * p in halfline ((0. (TOP-REAL n)),p) let r be real number ; ::_thesis: ( r >= 0 implies r * p in halfline ((0. (TOP-REAL n)),p) ) A1: n in NAT by ORDINAL1:def_12; assume A2: r >= 0 ; ::_thesis: r * p in halfline ((0. (TOP-REAL n)),p) ( (1 - r) * (0. (TOP-REAL n)) = 0. (TOP-REAL n) & (0. (TOP-REAL n)) + (r * p) = r * p ) by RLVECT_1:4, RLVECT_1:10; hence r * p in halfline ((0. (TOP-REAL n)),p) by A1, A2, TOPREAL9:26; ::_thesis: verum end; theorem Th1: :: BROUWER2:1 for n being Nat for p, q being Point of (TOP-REAL n) for r being real number holds ((1 - r) * p) + (r * q) = p + (r * (q - p)) proof let n be Nat; ::_thesis: for p, q being Point of (TOP-REAL n) for r being real number holds ((1 - r) * p) + (r * q) = p + (r * (q - p)) let p, q be Point of (TOP-REAL n); ::_thesis: for r being real number holds ((1 - r) * p) + (r * q) = p + (r * (q - p)) let r be real number ; ::_thesis: ((1 - r) * p) + (r * q) = p + (r * (q - p)) thus p + (r * (q - p)) = ((((1 - r) * p) + (r * q)) - p) + p by Lm1 .= (((1 - r) * p) + (r * q)) - (p - p) by EUCLID:47 .= (((1 - r) * p) + (r * q)) - (0. (TOP-REAL n)) by RLVECT_1:15 .= ((1 - r) * p) + (r * q) by RLVECT_1:13 ; ::_thesis: verum end; theorem Th2: :: BROUWER2:2 for n being Nat for u, p, q, w being Point of (TOP-REAL n) st u in halfline (p,q) & w in halfline (p,q) & |.(u - p).| = |.(w - p).| holds u = w proof let n be Nat; ::_thesis: for u, p, q, w being Point of (TOP-REAL n) st u in halfline (p,q) & w in halfline (p,q) & |.(u - p).| = |.(w - p).| holds u = w let u, p, q, w be Point of (TOP-REAL n); ::_thesis: ( u in halfline (p,q) & w in halfline (p,q) & |.(u - p).| = |.(w - p).| implies u = w ) set r1 = u; set r2 = w; assume that A1: u in halfline (p,q) and A2: w in halfline (p,q) and A3: |.(u - p).| = |.(w - p).| ; ::_thesis: u = w A4: n in NAT by ORDINAL1:def_12; percases ( p <> q or p = q ) ; suppose p <> q ; ::_thesis: u = w then A5: |.(q - p).| <> 0 by A4, TOPRNS_1:28; consider a1 being real number such that A6: u = ((1 - a1) * p) + (a1 * q) and A7: a1 >= 0 by A1, A4, TOPREAL9:26; A8: abs a1 = a1 by A7, ABSVALUE:def_1; ( a1 in REAL & u - p = a1 * (q - p) ) by A6, Lm1, XREAL_0:def_1; then A9: |.(u - p).| = (abs a1) * |.(q - p).| by A4, TOPRNS_1:7; consider a2 being real number such that A10: w = ((1 - a2) * p) + (a2 * q) and A11: a2 >= 0 by A2, A4, TOPREAL9:26; ( a2 in REAL & w - p = a2 * (q - p) ) by A10, Lm1, XREAL_0:def_1; then A12: |.(w - p).| = (abs a2) * |.(q - p).| by A4, TOPRNS_1:7; abs a2 = a2 by A11, ABSVALUE:def_1; then a1 = a2 by A3, A5, A9, A12, A8, XCMPLX_1:5; hence u = w by A6, A10; ::_thesis: verum end; supposeA13: p = q ; ::_thesis: u = w then u in {p} by A1, A4, TOPREAL9:29; then A14: u = p by TARSKI:def_1; w in {p} by A2, A4, A13, TOPREAL9:29; hence u = w by A14, TARSKI:def_1; ::_thesis: verum end; end; end; Lm3: for n being Nat for p, q being Point of (TOP-REAL n) for A being Subset of (TOP-REAL n) st p in A & p <> q & A /\ (halfline (p,q)) is bounded holds ex w being Point of (Euclid n) st ( w in (Fr A) /\ (halfline (p,q)) & ( for u, P being Point of (Euclid n) st P = p & u in A /\ (halfline (p,q)) holds dist (P,u) <= dist (P,w) ) & ( for r being real number st r > 0 holds ex u being Point of (Euclid n) st ( u in A /\ (halfline (p,q)) & dist (w,u) < r ) ) ) proof let n be Nat; ::_thesis: for p, q being Point of (TOP-REAL n) for A being Subset of (TOP-REAL n) st p in A & p <> q & A /\ (halfline (p,q)) is bounded holds ex w being Point of (Euclid n) st ( w in (Fr A) /\ (halfline (p,q)) & ( for u, P being Point of (Euclid n) st P = p & u in A /\ (halfline (p,q)) holds dist (P,u) <= dist (P,w) ) & ( for r being real number st r > 0 holds ex u being Point of (Euclid n) st ( u in A /\ (halfline (p,q)) & dist (w,u) < r ) ) ) let p, q be Point of (TOP-REAL n); ::_thesis: for A being Subset of (TOP-REAL n) st p in A & p <> q & A /\ (halfline (p,q)) is bounded holds ex w being Point of (Euclid n) st ( w in (Fr A) /\ (halfline (p,q)) & ( for u, P being Point of (Euclid n) st P = p & u in A /\ (halfline (p,q)) holds dist (P,u) <= dist (P,w) ) & ( for r being real number st r > 0 holds ex u being Point of (Euclid n) st ( u in A /\ (halfline (p,q)) & dist (w,u) < r ) ) ) set TRn = TOP-REAL n; let A be Subset of (TOP-REAL n); ::_thesis: ( p in A & p <> q & A /\ (halfline (p,q)) is bounded implies ex w being Point of (Euclid n) st ( w in (Fr A) /\ (halfline (p,q)) & ( for u, P being Point of (Euclid n) st P = p & u in A /\ (halfline (p,q)) holds dist (P,u) <= dist (P,w) ) & ( for r being real number st r > 0 holds ex u being Point of (Euclid n) st ( u in A /\ (halfline (p,q)) & dist (w,u) < r ) ) ) ) assume that A1: p in A and A2: p <> q and A3: A /\ (halfline (p,q)) is bounded ; ::_thesis: ex w being Point of (Euclid n) st ( w in (Fr A) /\ (halfline (p,q)) & ( for u, P being Point of (Euclid n) st P = p & u in A /\ (halfline (p,q)) holds dist (P,u) <= dist (P,w) ) & ( for r being real number st r > 0 holds ex u being Point of (Euclid n) st ( u in A /\ (halfline (p,q)) & dist (w,u) < r ) ) ) reconsider P = p, Q = q as Element of (Euclid n) by EUCLID:67; A4: dist (P,Q) > 0 by A2, METRIC_1:7; set H = halfline (p,q); reconsider AH = A /\ (halfline (p,q)) as bounded Subset of (Euclid n) by A3, JORDAN2C:11; A5: n in NAT by ORDINAL1:def_12; then A6: dist (Q,P) = |.(q - p).| by SPPOL_1:39; p in halfline (p,q) by A5, TOPREAL9:27; then A7: p in AH by A1, XBOOLE_0:def_4; set DAH = diameter AH; set X = { r where r is Real : ( ((1 - r) * p) + (r * q) in AH & 0 <= r ) } ; set dAH = (diameter AH) + 1; A8: now__::_thesis:_for_x_being_set_st_x_in__{__r_where_r_is_Real_:_(_((1_-_r)_*_p)_+_(r_*_q)_in_AH_&_0_<=_r_)__}__holds_ x_is_real let x be set ; ::_thesis: ( x in { r where r is Real : ( ((1 - r) * p) + (r * q) in AH & 0 <= r ) } implies x is real ) assume x in { r where r is Real : ( ((1 - r) * p) + (r * q) in AH & 0 <= r ) } ; ::_thesis: x is real then ex r being Real st ( x = r & ((1 - r) * p) + (r * q) in AH & 0 <= r ) ; hence x is real ; ::_thesis: verum end; ( 1 * p = p & 0 * q = 0. (TOP-REAL n) ) by RLVECT_1:10, RLVECT_1:def_8; then p = ((1 - 0) * p) + (0 * q) by RLVECT_1:def_4; then A9: 0 in { r where r is Real : ( ((1 - r) * p) + (r * q) in AH & 0 <= r ) } by A7; then reconsider X = { r where r is Real : ( ((1 - r) * p) + (r * q) in AH & 0 <= r ) } as non empty real-membered set by A8, MEMBERED:def_3; A10: (diameter AH) + 0 < (diameter AH) + 1 by XREAL_1:8; now__::_thesis:_for_x_being_ext-real_number_st_x_in_X_holds_ x_<=_((diameter_AH)_+_1)_/_(dist_(Q,P)) let x be ext-real number ; ::_thesis: ( x in X implies x <= ((diameter AH) + 1) / (dist (Q,P)) ) assume x in X ; ::_thesis: x <= ((diameter AH) + 1) / (dist (Q,P)) then consider r being Real such that A11: x = r and A12: ((1 - r) * p) + (r * q) in AH and A13: 0 <= r ; reconsider PQ = ((1 - r) * p) + (r * q) as Element of (Euclid n) by A12; (((1 - r) * p) + (r * q)) - p = r * (q - p) by Lm1; then dist (PQ,P) = |.(r * (q - p)).| by A5, SPPOL_1:39 .= (abs r) * |.(q - p).| by A5, TOPRNS_1:7 .= r * (dist (Q,P)) by A6, A13, ABSVALUE:def_1 ; then r * (dist (Q,P)) <= diameter AH by A7, A12, TBSP_1:def_8; then A14: r * (dist (Q,P)) <= (diameter AH) + 1 by A10, XXREAL_0:2; (r * (dist (Q,P))) / (dist (Q,P)) = r * ((dist (Q,P)) / (dist (Q,P))) .= r * 1 by A4, XCMPLX_1:60 ; hence x <= ((diameter AH) + 1) / (dist (Q,P)) by A11, A14, XREAL_1:72; ::_thesis: verum end; then ((diameter AH) + 1) / (dist (P,Q)) is UpperBound of X by XXREAL_2:def_1; then X is bounded_above by XXREAL_2:def_10; then reconsider S = sup X as Real by XXREAL_2:16; A15: 0 <= S by A9, XXREAL_2:4; set Spq = ((1 - S) * p) + (S * q); reconsider spq = ((1 - S) * p) + (S * q) as Element of (Euclid n) by EUCLID:67; A16: for r being real number st r > 0 holds ex w being Point of (Euclid n) st ( w in AH & dist (spq,w) < r ) proof let r be real number ; ::_thesis: ( r > 0 implies ex w being Point of (Euclid n) st ( w in AH & dist (spq,w) < r ) ) assume A17: r > 0 ; ::_thesis: ex w being Point of (Euclid n) st ( w in AH & dist (spq,w) < r ) set r2 = r / |.(q - p).|; assume A18: for w being Point of (Euclid n) st w in AH holds dist (spq,w) >= r ; ::_thesis: contradiction now__::_thesis:_for_x_being_ext-real_number_st_x_in_X_holds_ S_-_(r_/_|.(q_-_p).|)_>=_x let x be ext-real number ; ::_thesis: ( x in X implies S - (r / |.(q - p).|) >= x ) assume A19: x in X ; ::_thesis: S - (r / |.(q - p).|) >= x then consider w being Real such that A20: x = w and A21: ((1 - w) * p) + (w * q) in AH and 0 <= w ; S - w >= 0 by A19, A20, XREAL_1:48, XXREAL_2:4; then A22: abs (S - w) = S - w by ABSVALUE:def_1; reconsider PQ = ((1 - w) * p) + (w * q) as Element of (Euclid n) by A21; A23: PQ = p + (w * (q - p)) by Th1; (((1 - S) * p) + (S * q)) - (p + (w * (q - p))) = ((((1 - S) * p) + (S * q)) - p) - (w * (q - p)) by RLVECT_1:27 .= (S * (q - p)) - (w * (q - p)) by Lm1 .= (S - w) * (q - p) by RLVECT_1:35 ; then dist (spq,PQ) = |.((S - w) * (q - p)).| by A5, A23, SPPOL_1:39 .= (S - w) * |.(q - p).| by A5, A22, TOPRNS_1:7 ; then (S - w) * |.(q - p).| >= r by A18, A21; then S - w >= r / |.(q - p).| by A2, A6, METRIC_1:7, XREAL_1:79; hence S - (r / |.(q - p).|) >= x by A20, XREAL_1:11; ::_thesis: verum end; then S - (r / |.(q - p).|) is UpperBound of X by XXREAL_2:def_1; then S - 0 <= S - (r / |.(q - p).|) by XXREAL_2:def_3; hence contradiction by A4, A6, A17, XREAL_1:8; ::_thesis: verum end; A24: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8; now__::_thesis:_for_U_being_Subset_of_(TOP-REAL_n)_st_U_is_open_&_((1_-_S)_*_p)_+_(S_*_q)_in_U_holds_ (_A_meets_U_&_U_\_A_<>_{}_) let U be Subset of (TOP-REAL n); ::_thesis: ( U is open & ((1 - S) * p) + (S * q) in U implies ( A meets U & U \ A <> {} ) ) reconsider UE = U as Subset of (TopSpaceMetr (Euclid n)) by A24; assume that A25: U is open and A26: ((1 - S) * p) + (S * q) in U ; ::_thesis: ( A meets U & U \ A <> {} ) UE in the topology of (TopSpaceMetr (Euclid n)) by A24, A25, PRE_TOPC:def_2; then UE is open by PRE_TOPC:def_2; then consider r being real number such that A27: r > 0 and A28: Ball (spq,r) c= UE by A26, TOPMETR:15; set r2 = r / |.(q - p).|; set Sr = S + ((r / |.(q - p).|) / 2); consider w being Element of (Euclid n) such that A29: ( w in AH & dist (spq,w) < r ) by A16, A27; ( w in Ball (spq,r) & w in A ) by A29, METRIC_1:11, XBOOLE_0:def_4; hence A meets U by A28, XBOOLE_0:3; ::_thesis: U \ A <> {} A30: (r / |.(q - p).|) * |.(q - p).| = r * (|.(q - p).| / |.(q - p).|) .= r * 1 by A4, A6, XCMPLX_1:60 ; S + ((r / |.(q - p).|) / 2) > S + 0 by A4, A6, A27, XREAL_1:6; then S - (S + ((r / |.(q - p).|) / 2)) < 0 by XREAL_1:49; then A31: abs (S - (S + ((r / |.(q - p).|) / 2))) = - (S - (S + ((r / |.(q - p).|) / 2))) by ABSVALUE:def_1 .= (r / |.(q - p).|) / 2 ; set Srpq = ((1 - (S + ((r / |.(q - p).|) / 2))) * p) + ((S + ((r / |.(q - p).|) / 2)) * q); reconsider srpq = ((1 - (S + ((r / |.(q - p).|) / 2))) * p) + ((S + ((r / |.(q - p).|) / 2)) * q) as Element of (Euclid n) by EUCLID:67; A32: srpq in halfline (p,q) by A15, A27; A33: not srpq in A proof assume srpq in A ; ::_thesis: contradiction then srpq in AH by A32, XBOOLE_0:def_4; then S + ((r / |.(q - p).|) / 2) in X by A15, A27; then S + ((r / |.(q - p).|) / 2) <= S + 0 by XXREAL_2:4; hence contradiction by A4, A6, A27, XREAL_1:8; ::_thesis: verum end; (((1 - S) * p) + (S * q)) - (((1 - (S + ((r / |.(q - p).|) / 2))) * p) + ((S + ((r / |.(q - p).|) / 2)) * q)) = (((1 - S) * p) + (S * q)) - (p + ((S + ((r / |.(q - p).|) / 2)) * (q - p))) by Th1 .= ((((1 - S) * p) + (S * q)) - p) - ((S + ((r / |.(q - p).|) / 2)) * (q - p)) by RLVECT_1:27 .= (S * (q - p)) - ((S + ((r / |.(q - p).|) / 2)) * (q - p)) by Lm1 .= (S - (S + ((r / |.(q - p).|) / 2))) * (q - p) by RLVECT_1:35 ; then dist (spq,srpq) = |.((S - (S + ((r / |.(q - p).|) / 2))) * (q - p)).| by A5, SPPOL_1:39 .= ((r / |.(q - p).|) / 2) * |.(q - p).| by A5, A31, TOPRNS_1:7 .= r / 2 by A30 ; then dist (spq,srpq) < r by A27, XREAL_1:216; then srpq in Ball (spq,r) by METRIC_1:11; hence U \ A <> {} by A28, A33, XBOOLE_0:def_5; ::_thesis: verum end; then A34: ((1 - S) * p) + (S * q) in Fr A by TOPGEN_1:9; take spq ; ::_thesis: ( spq in (Fr A) /\ (halfline (p,q)) & ( for u, P being Point of (Euclid n) st P = p & u in A /\ (halfline (p,q)) holds dist (P,u) <= dist (P,spq) ) & ( for r being real number st r > 0 holds ex u being Point of (Euclid n) st ( u in A /\ (halfline (p,q)) & dist (spq,u) < r ) ) ) A35: (((1 - S) * p) + (S * q)) - p = S * (q - p) by Lm1; ((1 - S) * p) + (S * q) in halfline (p,q) by A15; hence spq in (Fr A) /\ (halfline (p,q)) by A34, XBOOLE_0:def_4; ::_thesis: ( ( for u, P being Point of (Euclid n) st P = p & u in A /\ (halfline (p,q)) holds dist (P,u) <= dist (P,spq) ) & ( for r being real number st r > 0 holds ex u being Point of (Euclid n) st ( u in A /\ (halfline (p,q)) & dist (spq,u) < r ) ) ) A36: abs S = S by A15, ABSVALUE:def_1; hereby ::_thesis: for r being real number st r > 0 holds ex u being Point of (Euclid n) st ( u in A /\ (halfline (p,q)) & dist (spq,u) < r ) let u, P be Point of (Euclid n); ::_thesis: ( P = p & u in A /\ (halfline (p,q)) implies dist (P,u) <= dist (P,spq) ) assume that A37: P = p and A38: u in A /\ (halfline (p,q)) ; ::_thesis: dist (P,u) <= dist (P,spq) A39: dist (P,spq) = |.(S * (q - p)).| by A5, A35, A37, SPPOL_1:39 .= S * |.(q - p).| by A5, A36, TOPRNS_1:7 ; u in halfline (p,q) by A38, XBOOLE_0:def_4; then consider Ur being real number such that A40: u = ((1 - Ur) * p) + (Ur * q) and A41: 0 <= Ur by A5, TOPREAL9:26; A42: abs Ur = Ur by A41, ABSVALUE:def_1; Ur in REAL by XREAL_0:def_1; then Ur in X by A38, A40, A41; then A43: Ur <= S by XXREAL_2:4; set du = dist (P,u); set ds = dist (P,spq); A44: (((1 - Ur) * p) + (Ur * q)) - p = Ur * (q - p) by Lm1; dist (P,u) = |.(Ur * (q - p)).| by A5, A37, A40, A44, SPPOL_1:39 .= Ur * |.(q - p).| by A5, A42, TOPRNS_1:7 ; hence dist (P,u) <= dist (P,spq) by A39, A43, XREAL_1:64; ::_thesis: verum end; thus for r being real number st r > 0 holds ex u being Point of (Euclid n) st ( u in A /\ (halfline (p,q)) & dist (spq,u) < r ) by A16; ::_thesis: verum end; theorem :: BROUWER2:3 for n being Nat for p, q being Point of (TOP-REAL n) for S being Subset of (TOP-REAL n) st p in S & p <> q & S /\ (halfline (p,q)) is bounded holds ex w being Point of (TOP-REAL n) st ( w in (Fr S) /\ (halfline (p,q)) & ( for u being Point of (TOP-REAL n) st u in S /\ (halfline (p,q)) holds |.(p - u).| <= |.(p - w).| ) & ( for r being real number st r > 0 holds ex u being Point of (TOP-REAL n) st ( u in S /\ (halfline (p,q)) & |.(w - u).| < r ) ) ) proof let n be Nat; ::_thesis: for p, q being Point of (TOP-REAL n) for S being Subset of (TOP-REAL n) st p in S & p <> q & S /\ (halfline (p,q)) is bounded holds ex w being Point of (TOP-REAL n) st ( w in (Fr S) /\ (halfline (p,q)) & ( for u being Point of (TOP-REAL n) st u in S /\ (halfline (p,q)) holds |.(p - u).| <= |.(p - w).| ) & ( for r being real number st r > 0 holds ex u being Point of (TOP-REAL n) st ( u in S /\ (halfline (p,q)) & |.(w - u).| < r ) ) ) let p, q be Point of (TOP-REAL n); ::_thesis: for S being Subset of (TOP-REAL n) st p in S & p <> q & S /\ (halfline (p,q)) is bounded holds ex w being Point of (TOP-REAL n) st ( w in (Fr S) /\ (halfline (p,q)) & ( for u being Point of (TOP-REAL n) st u in S /\ (halfline (p,q)) holds |.(p - u).| <= |.(p - w).| ) & ( for r being real number st r > 0 holds ex u being Point of (TOP-REAL n) st ( u in S /\ (halfline (p,q)) & |.(w - u).| < r ) ) ) set T = TOP-REAL n; set E = Euclid n; let A be Subset of (TOP-REAL n); ::_thesis: ( p in A & p <> q & A /\ (halfline (p,q)) is bounded implies ex w being Point of (TOP-REAL n) st ( w in (Fr A) /\ (halfline (p,q)) & ( for u being Point of (TOP-REAL n) st u in A /\ (halfline (p,q)) holds |.(p - u).| <= |.(p - w).| ) & ( for r being real number st r > 0 holds ex u being Point of (TOP-REAL n) st ( u in A /\ (halfline (p,q)) & |.(w - u).| < r ) ) ) ) assume A1: ( p in A & p <> q & A /\ (halfline (p,q)) is bounded ) ; ::_thesis: ex w being Point of (TOP-REAL n) st ( w in (Fr A) /\ (halfline (p,q)) & ( for u being Point of (TOP-REAL n) st u in A /\ (halfline (p,q)) holds |.(p - u).| <= |.(p - w).| ) & ( for r being real number st r > 0 holds ex u being Point of (TOP-REAL n) st ( u in A /\ (halfline (p,q)) & |.(w - u).| < r ) ) ) consider W being Point of (Euclid n) such that A2: W in (Fr A) /\ (halfline (p,q)) and A3: for u, P being Point of (Euclid n) st P = p & u in A /\ (halfline (p,q)) holds dist (P,u) <= dist (P,W) and A4: for r being real number st r > 0 holds ex u being Point of (Euclid n) st ( u in A /\ (halfline (p,q)) & dist (W,u) < r ) by A1, Lm3; reconsider w = W as Point of (TOP-REAL n) by EUCLID:67; take w ; ::_thesis: ( w in (Fr A) /\ (halfline (p,q)) & ( for u being Point of (TOP-REAL n) st u in A /\ (halfline (p,q)) holds |.(p - u).| <= |.(p - w).| ) & ( for r being real number st r > 0 holds ex u being Point of (TOP-REAL n) st ( u in A /\ (halfline (p,q)) & |.(w - u).| < r ) ) ) thus w in (Fr A) /\ (halfline (p,q)) by A2; ::_thesis: ( ( for u being Point of (TOP-REAL n) st u in A /\ (halfline (p,q)) holds |.(p - u).| <= |.(p - w).| ) & ( for r being real number st r > 0 holds ex u being Point of (TOP-REAL n) st ( u in A /\ (halfline (p,q)) & |.(w - u).| < r ) ) ) reconsider P = p as Point of (Euclid n) by EUCLID:67; A5: n in NAT by ORDINAL1:def_12; hereby ::_thesis: for r being real number st r > 0 holds ex u being Point of (TOP-REAL n) st ( u in A /\ (halfline (p,q)) & |.(w - u).| < r ) let u be Point of (TOP-REAL n); ::_thesis: ( u in A /\ (halfline (p,q)) implies |.(p - u).| <= |.(p - w).| ) assume A6: u in A /\ (halfline (p,q)) ; ::_thesis: |.(p - u).| <= |.(p - w).| reconsider U = u as Point of (Euclid n) by EUCLID:67; A7: dist (P,U) = |.(p - u).| by A5, SPPOL_1:39; dist (P,U) <= dist (P,W) by A3, A6; hence |.(p - u).| <= |.(p - w).| by A5, A7, SPPOL_1:39; ::_thesis: verum end; let r be real number ; ::_thesis: ( r > 0 implies ex u being Point of (TOP-REAL n) st ( u in A /\ (halfline (p,q)) & |.(w - u).| < r ) ) assume r > 0 ; ::_thesis: ex u being Point of (TOP-REAL n) st ( u in A /\ (halfline (p,q)) & |.(w - u).| < r ) then consider U being Point of (Euclid n) such that A8: ( U in A /\ (halfline (p,q)) & dist (W,U) < r ) by A4; reconsider u = U as Point of (TOP-REAL n) by EUCLID:67; n in NAT by ORDINAL1:def_12; then dist (W,U) = |.(w - u).| by SPPOL_1:39; hence ex u being Point of (TOP-REAL n) st ( u in A /\ (halfline (p,q)) & |.(w - u).| < r ) by A8; ::_thesis: verum end; theorem Th4: :: BROUWER2:4 for n being Nat for p, q being Point of (TOP-REAL n) for A being convex Subset of (TOP-REAL n) st A is closed & p in Int A & p <> q & A /\ (halfline (p,q)) is bounded holds ex u being Point of (TOP-REAL n) st (Fr A) /\ (halfline (p,q)) = {u} proof let n be Nat; ::_thesis: for p, q being Point of (TOP-REAL n) for A being convex Subset of (TOP-REAL n) st A is closed & p in Int A & p <> q & A /\ (halfline (p,q)) is bounded holds ex u being Point of (TOP-REAL n) st (Fr A) /\ (halfline (p,q)) = {u} let p, q be Point of (TOP-REAL n); ::_thesis: for A being convex Subset of (TOP-REAL n) st A is closed & p in Int A & p <> q & A /\ (halfline (p,q)) is bounded holds ex u being Point of (TOP-REAL n) st (Fr A) /\ (halfline (p,q)) = {u} set TRn = TOP-REAL n; set En = Euclid n; let A be convex Subset of (TOP-REAL n); ::_thesis: ( A is closed & p in Int A & p <> q & A /\ (halfline (p,q)) is bounded implies ex u being Point of (TOP-REAL n) st (Fr A) /\ (halfline (p,q)) = {u} ) assume that A1: A is closed and A2: p in Int A and A3: p <> q and A4: A /\ (halfline (p,q)) is bounded ; ::_thesis: ex u being Point of (TOP-REAL n) st (Fr A) /\ (halfline (p,q)) = {u} A5: n in NAT by ORDINAL1:def_12; reconsider P = p, Q = q as Point of (Euclid n) by EUCLID:67; A6: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8; then reconsider I = Int A as Subset of (TopSpaceMetr (Euclid n)) ; Int A in the topology of (TopSpaceMetr (Euclid n)) by A6, PRE_TOPC:def_2; then I is open by PRE_TOPC:def_2; then consider r being real number such that A7: r > 0 and A8: Ball (P,r) c= I by A2, TOPMETR:15; dist (P,P) < r by A7, METRIC_1:1; then A9: P in Ball (P,r) by METRIC_1:11; set H = halfline (p,q); reconsider AH = A /\ (halfline (p,q)) as bounded Subset of (Euclid n) by A4, JORDAN2C:11; A10: Int A c= A by TOPS_1:16; then consider W being Point of (Euclid n) such that A11: W in (Fr A) /\ (halfline (p,q)) and A12: for u, P being Point of (Euclid n) st P = p & u in AH holds dist (P,u) <= dist (P,W) and for r being real number st r > 0 holds ex u being Point of (Euclid n) st ( u in AH & dist (W,u) < r ) by A2, A3, A4, Lm3; reconsider w = W as Point of (TOP-REAL n) by EUCLID:67; A13: W in Fr A by A11, XBOOLE_0:def_4; W in halfline (p,q) by A11, XBOOLE_0:def_4; then consider Wr being real number such that A14: W = ((1 - Wr) * p) + (Wr * q) and A15: Wr >= 0 by A5, TOPREAL9:26; A16: Fr A c= A by A1, TOPS_1:35; A17: Fr A misses Ball (P,r) by A8, TOPS_1:39, XBOOLE_1:63; (Fr A) /\ (halfline (p,q)) = {W} proof assume (Fr A) /\ (halfline (p,q)) <> {W} ; ::_thesis: contradiction then consider u being set such that A18: u in (Fr A) /\ (halfline (p,q)) and A19: u <> W by A11, ZFMISC_1:35; reconsider u = u as Point of (TOP-REAL n) by A18; A20: u in halfline (p,q) by A18, XBOOLE_0:def_4; then consider Ur being real number such that A21: u = ((1 - Ur) * p) + (Ur * q) and A22: Ur >= 0 by A5, TOPREAL9:26; A23: abs Ur = Ur by A22, ABSVALUE:def_1; reconsider U = u as Element of (Euclid n) by EUCLID:67; A24: Wr - Ur in REAL by XREAL_0:def_1; (((1 - Ur) * p) + (Ur * q)) - p = Ur * (q - p) by Lm1; then A25: dist (U,P) = |.(Ur * (q - p)).| by A5, A21, SPPOL_1:39 .= Ur * |.(q - p).| by A5, A23, TOPRNS_1:7 ; set R = (r * (Wr - Ur)) / Wr; reconsider b = Ball (U,((r * (Wr - Ur)) / Wr)) as Subset of (TopSpaceMetr (Euclid n)) by A6, EUCLID:67; set x = (Wr - Ur) / Wr; b is open by TOPMETR:14; then b in the topology of (TOP-REAL n) by A6, PRE_TOPC:def_2; then reconsider B = b as open Subset of (TOP-REAL n) by PRE_TOPC:def_2; A26: abs Wr = Wr by A15, ABSVALUE:def_1; (((1 - Wr) * p) + (Wr * q)) - p = Wr * (q - p) by Lm1; then A27: dist (W,P) = |.(Wr * (q - p)).| by A5, A14, SPPOL_1:39 .= Wr * |.(q - p).| by A5, A26, TOPRNS_1:7 ; A28: u in Fr A by A18, XBOOLE_0:def_4; then A29: u in AH by A16, A20, XBOOLE_0:def_4; P <> W by A17, A9, A13, XBOOLE_0:3; then A30: Wr > 0 by A27, METRIC_1:7; then A31: 1 - ((Wr - Ur) / Wr) = (Wr / Wr) - ((Wr - Ur) / Wr) by XCMPLX_1:60 .= Ur / Wr ; P <> u by A17, A9, A28, XBOOLE_0:3; then Ur > 0 by A25, METRIC_1:7; then 1 - ((Wr - Ur) / Wr) >= ((Wr - Ur) / Wr) - ((Wr - Ur) / Wr) by A30, A31; then A32: ( (Wr - Ur) / Wr in REAL & (Wr - Ur) / Wr <= 1 ) by XREAL_0:def_1, XREAL_1:6; A33: ((1 - Wr) * p) + (Wr * q) = (Wr * (q - p)) + p by Th1; A34: ((1 - Ur) * p) + (Ur * q) = p + (Ur * (q - p)) by Th1; then (((1 - Wr) * p) + (Wr * q)) - (((1 - Ur) * p) + (Ur * q)) = ((p + (Wr * (q - p))) - p) - (Ur * (q - p)) by A33, RLVECT_1:27 .= ((Wr * (q - p)) + (p - p)) - (Ur * (q - p)) by EUCLID:45 .= ((Wr * (q - p)) + (0. (TOP-REAL n))) - (Ur * (q - p)) by EUCLID:42 .= (Wr * (q - p)) - (Ur * (q - p)) by RLVECT_1:def_4 .= (Wr - Ur) * (q - p) by EUCLID:50 ; then A35: dist (U,W) = |.((Wr - Ur) * (q - p)).| by A5, A14, A21, SPPOL_1:39 .= (abs (Wr - Ur)) * |.(q - p).| by A5, A24, TOPRNS_1:7 ; dist (U,W) > 0 by A19, METRIC_1:7; then |.(q - p).| > 0 by A35, XREAL_1:134; then Ur <= Wr by A12, A25, A27, A29, XREAL_1:68; then Wr - Ur >= 0 by XREAL_1:48; then A36: abs (Wr - Ur) = Wr - Ur by ABSVALUE:def_1; then A37: Wr - Ur > 0 by A19, A35, METRIC_1:7; dist (U,U) = 0 by METRIC_1:1; then U in B by A7, A30, A37, METRIC_1:11; then B \ A <> {} by A28, TOPGEN_1:9; then consider t being set such that A38: t in B \ A by XBOOLE_0:def_1; A39: t in B by A38, XBOOLE_0:def_5; reconsider t = t as Point of (TOP-REAL n) by A38; set z = p + ((Wr / (Wr - Ur)) * (t - u)); reconsider Z = p + ((Wr / (Wr - Ur)) * (t - u)) as Point of (Euclid n) by EUCLID:67; reconsider T = t as Point of (Euclid n) by EUCLID:67; A40: dist (U,T) = |.(u - t).| by A5, SPPOL_1:39; A41: (Wr / (Wr - Ur)) * ((r * (Wr - Ur)) / Wr) = (((Wr / Wr) * (Wr - Ur)) / (Wr - Ur)) * r .= ((Wr - Ur) / (Wr - Ur)) * r by A30, XCMPLX_1:88 .= r by A37, XCMPLX_1:88 ; abs (- Wr) = - (- Wr) by A30, ABSVALUE:def_1; then A42: ( (- Wr) / (Wr - Ur) in REAL & abs ((- Wr) / (Wr - Ur)) = Wr / (Wr - Ur) ) by A36, COMPLEX1:67, XREAL_0:def_1; A43: (Ur / Wr) * (Wr * (q - p)) = ((Ur / Wr) * Wr) * (q - p) by RLVECT_1:def_7 .= ((Wr / Wr) * Ur) * (q - p) .= Ur * (q - p) by A30, XCMPLX_1:88 ; p - (p + ((Wr / (Wr - Ur)) * (t - u))) = (p - p) - ((Wr / (Wr - Ur)) * (t - u)) by RLVECT_1:27 .= (0. (TOP-REAL n)) - ((Wr / (Wr - Ur)) * (t - u)) by RLVECT_1:15 .= - ((Wr / (Wr - Ur)) * (t - u)) by RLVECT_1:14 .= (- 1) * ((Wr / (Wr - Ur)) * (t - u)) by RLVECT_1:16 .= ((- 1) * (Wr / (Wr - Ur))) * (t - u) by RLVECT_1:def_7 .= ((- Wr) / (Wr - Ur)) * (t - u) ; then A44: dist (P,Z) = |.(((- Wr) / (Wr - Ur)) * (t - u)).| by A5, SPPOL_1:39 .= (Wr / (Wr - Ur)) * |.(t - u).| by A5, A42, TOPRNS_1:7 ; dist (U,T) < (r * (Wr - Ur)) / Wr by A39, METRIC_1:11; then (Wr / (Wr - Ur)) * |.(u - t).| < r by A30, A37, A40, A41, XREAL_1:68; then dist (P,Z) < r by A5, A40, A44, SPPOL_1:39; then Z in Ball (P,r) by METRIC_1:11; then A45: Z in I by A8; ((Wr - Ur) / Wr) * ((Wr / (Wr - Ur)) * (t - u)) = (((Wr - Ur) / Wr) * (Wr / (Wr - Ur))) * (t - u) by RLVECT_1:def_7 .= ((((Wr - Ur) / (Wr - Ur)) * Wr) / Wr) * (t - u) .= (Wr / Wr) * (t - u) by A37, XCMPLX_1:88 .= 1 * (t - u) by A30, XCMPLX_1:60 .= t - u by RLVECT_1:def_8 ; then ((Wr - Ur) / Wr) * (p + ((Wr / (Wr - Ur)) * (t - u))) = (((Wr - Ur) / Wr) * p) + (t - u) by RLVECT_1:def_5; then (((Wr - Ur) / Wr) * (p + ((Wr / (Wr - Ur)) * (t - u)))) + ((1 - ((Wr - Ur) / Wr)) * w) = ((t - u) + (((Wr - Ur) / Wr) * p)) + (((1 - ((Wr - Ur) / Wr)) * p) + (Ur * (q - p))) by A14, A31, A33, A43, RLVECT_1:def_5 .= (((t - u) + (((Wr - Ur) / Wr) * p)) + ((1 - ((Wr - Ur) / Wr)) * p)) + (Ur * (q - p)) by RLVECT_1:def_3 .= ((t - u) + ((((Wr - Ur) / Wr) * p) + ((1 - ((Wr - Ur) / Wr)) * p))) + (Ur * (q - p)) by RLVECT_1:def_3 .= ((t - u) + ((((Wr - Ur) / Wr) + (1 - ((Wr - Ur) / Wr))) * p)) + (Ur * (q - p)) by RLVECT_1:def_6 .= ((t - u) + p) + (Ur * (q - p)) by RLVECT_1:def_8 .= (t - u) + u by A21, A34, RLVECT_1:def_3 .= t - (u - u) by RLVECT_1:29 .= t - (0. (TOP-REAL n)) by RLVECT_1:15 .= t by RLVECT_1:13 ; then t in A by A16, A10, A13, A30, A32, A37, A45, RLTOPSP1:def_1; hence contradiction by A38, XBOOLE_0:def_5; ::_thesis: verum end; hence ex u being Point of (TOP-REAL n) st (Fr A) /\ (halfline (p,q)) = {u} by A11; ::_thesis: verum end; Lm4: for n being Element of NAT st n > 0 holds for A being convex Subset of (TOP-REAL n) st A is compact & 0* n in Int A holds ex h being Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) st ( h is being_homeomorphism & h .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) ) proof let n be Element of NAT ; ::_thesis: ( n > 0 implies for A being convex Subset of (TOP-REAL n) st A is compact & 0* n in Int A holds ex h being Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) st ( h is being_homeomorphism & h .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) ) ) set TRn = TOP-REAL n; set En = Euclid n; set cTRn = the carrier of (TOP-REAL n); assume A1: n > 0 ; ::_thesis: for A being convex Subset of (TOP-REAL n) st A is compact & 0* n in Int A holds ex h being Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) st ( h is being_homeomorphism & h .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) ) the carrier of (TOP-REAL n) \ {(0. (TOP-REAL n))} = {(0. (TOP-REAL n))} ` by SUBSET_1:def_4; then reconsider cTR0 = the carrier of (TOP-REAL n) \ {(0. (TOP-REAL n))} as non empty open Subset of (TOP-REAL n) by A1; set CL = cl_Ball ((0. (TOP-REAL n)),1); set S = Sphere ((0. (TOP-REAL n)),1); set TRn0 = (TOP-REAL n) | cTR0; set nN = n NormF ; set En = Euclid n; set I0 = (0. (TOP-REAL n)) .--> (0. (TOP-REAL n)); let A be convex Subset of (TOP-REAL n); ::_thesis: ( A is compact & 0* n in Int A implies ex h being Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) st ( h is being_homeomorphism & h .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) ) ) assume that A2: A is compact and A3: 0* n in Int A ; ::_thesis: ex h being Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) st ( h is being_homeomorphism & h .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) ) A4: not A is empty by A3; reconsider 0TRn = 0. (TOP-REAL n) as Point of (Euclid n) by EUCLID:67; A5: 0* n = 0. (TOP-REAL n) by EUCLID:70; then consider e being real number such that A6: e > 0 and A7: Ball (0TRn,e) c= A by A3, GOBOARD6:5; Fr A misses Int A by TOPS_1:39; then A8: not 0* n in Fr A by A3, XBOOLE_0:3; then A9: (Fr A) \ {(0. (TOP-REAL n))} = Fr A by A5, ZFMISC_1:57; set TM = TopSpaceMetr (Euclid n); A10: [#] ((TOP-REAL n) | cTR0) = cTR0 by PRE_TOPC:def_5; A11: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8; then reconsider a = A as Subset of (TopSpaceMetr (Euclid n)) ; reconsider aa = a as Subset of (Euclid n) by EUCLID:67; (TOP-REAL n) | A is compact by A2; then (TopSpaceMetr (Euclid n)) | a is compact by A11, PRE_TOPC:36; then A12: a is compact by A4, COMPTS_1:3; A13: for p being Point of (TOP-REAL n) st p <> 0. (TOP-REAL n) holds ex x being Point of (TOP-REAL n) st (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {x} proof let p be Point of (TOP-REAL n); ::_thesis: ( p <> 0. (TOP-REAL n) implies ex x being Point of (TOP-REAL n) st (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {x} ) assume A14: p <> 0. (TOP-REAL n) ; ::_thesis: ex x being Point of (TOP-REAL n) st (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {x} A15: A /\ (halfline ((0. (TOP-REAL n)),p)) c= aa by XBOOLE_1:17; then reconsider F = A /\ (halfline ((0. (TOP-REAL n)),p)) as Subset of (Euclid n) by XBOOLE_1:1; A16: 0. (TOP-REAL n) in Int A by A3, EUCLID:70; F is bounded by A12, A15, HAUSDORF:18, TBSP_1:14; then A /\ (halfline ((0. (TOP-REAL n)),p)) is bounded by JORDAN2C:11; hence ex x being Point of (TOP-REAL n) st (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {x} by A2, A14, A16, Th4; ::_thesis: verum end; not Fr A is empty proof set q = the Element of cTR0; the Element of cTR0 <> 0. (TOP-REAL n) by ZFMISC_1:56; then ex x being Point of (TOP-REAL n) st (Fr A) /\ (halfline ((0. (TOP-REAL n)), the Element of cTR0)) = {x} by A13; hence not Fr A is empty ; ::_thesis: verum end; then reconsider FrA = Fr A as non empty Subset of ((TOP-REAL n) | cTR0) by A10, A9, XBOOLE_1:33; A17: Fr A c= A by A2, TOPS_1:35; set TS = (TOP-REAL n) | (Sphere ((0. (TOP-REAL n)),1)); reconsider I = incl ((TOP-REAL n) | cTR0) as continuous Function of ((TOP-REAL n) | cTR0),(TOP-REAL n) by TMAP_1:87; A18: [#] ((TOP-REAL n) | (Sphere ((0. (TOP-REAL n)),1))) = Sphere ((0. (TOP-REAL n)),1) by PRE_TOPC:def_5; A19: (n NormF) | ((TOP-REAL n) | cTR0) = (n NormF) | the carrier of ((TOP-REAL n) | cTR0) by TMAP_1:def_4; A20: not 0 in rng ((n NormF) | ((TOP-REAL n) | cTR0)) proof assume 0 in rng ((n NormF) | ((TOP-REAL n) | cTR0)) ; ::_thesis: contradiction then consider x being set such that A21: x in dom ((n NormF) | ((TOP-REAL n) | cTR0)) and A22: ((n NormF) | ((TOP-REAL n) | cTR0)) . x = 0 by FUNCT_1:def_3; x in dom (n NormF) by A19, A21, RELAT_1:57; then reconsider x = x as Element of (TOP-REAL n) ; reconsider X = x as Element of REAL n by EUCLID:22; 0 = (n NormF) . x by A19, A21, A22, FUNCT_1:47 .= |.X.| by JGRAPH_4:def_1 ; then x = 0. (TOP-REAL n) by A5, EUCLID:8; then x in {(0. (TOP-REAL n))} by TARSKI:def_1; hence contradiction by A10, A21, XBOOLE_0:def_5; ::_thesis: verum end; then reconsider nN0 = (n NormF) | ((TOP-REAL n) | cTR0) as non-empty continuous Function of ((TOP-REAL n) | cTR0),R^1 by RELAT_1:def_9; reconsider b = I nN0 as Function of ((TOP-REAL n) | cTR0),(TOP-REAL n) by TOPREALC:46; A23: dom b = cTR0 by A10, FUNCT_2:def_1; A24: for p being Point of (TOP-REAL n) st p in cTR0 holds ( b . p = (1 / |.p.|) * p & |.((1 / |.p.|) * p).| = 1 ) proof let p be Point of (TOP-REAL n); ::_thesis: ( p in cTR0 implies ( b . p = (1 / |.p.|) * p & |.((1 / |.p.|) * p).| = 1 ) ) assume A25: p in cTR0 ; ::_thesis: ( b . p = (1 / |.p.|) * p & |.((1 / |.p.|) * p).| = 1 ) then A26: ( nN0 . p = (n NormF) . p & I . p = p ) by A10, A19, FUNCT_1:49, TMAP_1:84; thus b . p = (I . p) (/) (nN0 . p) by A23, A25, VALUED_2:72 .= p (/) |.p.| by A26, JGRAPH_4:def_1 .= (1 / |.p.|) (#) p by VALUED_2:def_32 .= (1 / |.p.|) * p ; ::_thesis: |.((1 / |.p.|) * p).| = 1 A27: ( abs (1 / |.p.|) = 1 / |.p.| & p <> 0. (TOP-REAL n) ) by A25, ABSVALUE:def_1, ZFMISC_1:56; thus |.((1 / |.p.|) * p).| = (abs (1 / |.p.|)) * |.p.| by TOPRNS_1:7 .= 1 by A27, TOPRNS_1:24, XCMPLX_1:87 ; ::_thesis: verum end; A28: rng b c= Sphere ((0. (TOP-REAL n)),1) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng b or y in Sphere ((0. (TOP-REAL n)),1) ) assume y in rng b ; ::_thesis: y in Sphere ((0. (TOP-REAL n)),1) then consider x being set such that A29: x in dom b and A30: b . x = y by FUNCT_1:def_3; reconsider x = x as Point of (TOP-REAL n) by A23, A29; A31: ( ((1 / |.x.|) * x) - (0. (TOP-REAL n)) = (1 / |.x.|) * x & |.((1 / |.x.|) * x).| = 1 ) by A10, A24, A29, RLVECT_1:13; y = (1 / |.x.|) * x by A10, A24, A29, A30; hence y in Sphere ((0. (TOP-REAL n)),1) by A31; ::_thesis: verum end; then reconsider B = b as Function of ((TOP-REAL n) | cTR0),((TOP-REAL n) | (Sphere ((0. (TOP-REAL n)),1))) by A10, A18, A23, FUNCT_2:2; A32: (0. (TOP-REAL n)) .--> (0. (TOP-REAL n)) = {(0. (TOP-REAL n))} --> (0. (TOP-REAL n)) by FUNCOP_1:def_9; then A33: dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) = {(0. (TOP-REAL n))} by FUNCOP_1:13; set FRA = ((TOP-REAL n) | cTR0) | FrA; set H = b | (((TOP-REAL n) | cTR0) | FrA); A34: dom (b | (((TOP-REAL n) | cTR0) | FrA)) = the carrier of (((TOP-REAL n) | cTR0) | FrA) by FUNCT_2:def_1; A35: b | (((TOP-REAL n) | cTR0) | FrA) = b | the carrier of (((TOP-REAL n) | cTR0) | FrA) by TMAP_1:def_4; then A36: rng (b | (((TOP-REAL n) | cTR0) | FrA)) c= rng b by RELAT_1:70; then A37: rng (b | (((TOP-REAL n) | cTR0) | FrA)) c= Sphere ((0. (TOP-REAL n)),1) by A28, XBOOLE_1:1; reconsider H = b | (((TOP-REAL n) | cTR0) | FrA) as Function of (((TOP-REAL n) | cTR0) | FrA),((TOP-REAL n) | (Sphere ((0. (TOP-REAL n)),1))) by A18, A28, A34, A36, FUNCT_2:2, XBOOLE_1:1; A38: [#] (((TOP-REAL n) | cTR0) | FrA) = FrA by PRE_TOPC:def_5; A39: (Fr A) \ {(0. (TOP-REAL n))} c= cTR0 by XBOOLE_1:33; Sphere ((0. (TOP-REAL n)),1) c= rng H proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Sphere ((0. (TOP-REAL n)),1) or x in rng H ) assume x in Sphere ((0. (TOP-REAL n)),1) ; ::_thesis: x in rng H then consider p being Point of (TOP-REAL n) such that A40: x = p and A41: |.(p - (0. (TOP-REAL n))).| = 1 ; p <> 0. (TOP-REAL n) by A5, A41; then consider q being Point of (TOP-REAL n) such that A42: FrA /\ (halfline ((0. (TOP-REAL n)),p)) = {q} by A13; A43: q in {q} by TARSKI:def_1; then A44: q in FrA by A42, XBOOLE_0:def_4; then A45: ( b . q = (1 / |.q.|) * q & b . q = H . q ) by A9, A24, A35, A38, A39, FUNCT_1:49; q in halfline ((0. (TOP-REAL n)),p) by A42, A43, XBOOLE_0:def_4; then halfline ((0. (TOP-REAL n)),p) = halfline ((0. (TOP-REAL n)),q) by A5, A8, A44, TOPREAL9:31; then A46: (1 / |.q.|) * q in halfline ((0. (TOP-REAL n)),p) by Lm2; A47: ( ((1 / |.q.|) * q) - (0. (TOP-REAL n)) = (1 / |.q.|) * q & p in halfline ((0. (TOP-REAL n)),p) ) by RLVECT_1:13, TOPREAL9:28; ( H . q in rng H & |.((1 / |.q.|) * q).| = 1 ) by A9, A24, A34, A38, A39, A44, FUNCT_1:def_3; hence x in rng H by A40, A41, A46, A47, A45, Th2; ::_thesis: verum end; then A48: Sphere ((0. (TOP-REAL n)),1) = rng H by A37, XBOOLE_0:def_10; (Fr A) \ {(0. (TOP-REAL n))} c= cTR0 by XBOOLE_1:33; then A49: ( dom H = [#] (((TOP-REAL n) | cTR0) | FrA) & (TOP-REAL n) | (Fr A) = ((TOP-REAL n) | cTR0) | FrA ) by A9, FUNCT_2:def_1, PRE_TOPC:7; for x1, x2 being set st x1 in dom H & x2 in dom H & H . x1 = H . x2 holds x1 = x2 proof let x1, x2 be set ; ::_thesis: ( x1 in dom H & x2 in dom H & H . x1 = H . x2 implies x1 = x2 ) assume that A50: x1 in dom H and A51: x2 in dom H and A52: H . x1 = H . x2 ; ::_thesis: x1 = x2 A53: x2 in dom b by A35, A51, RELAT_1:57; A54: x1 in dom b by A35, A50, RELAT_1:57; then reconsider p1 = x1, p2 = x2 as Point of (TOP-REAL n) by A23, A53; A55: b . p1 = (1 / |.p1.|) * p1 by A10, A24, A54; x2 <> 0. (TOP-REAL n) by A10, A53, ZFMISC_1:56; then consider q being Point of (TOP-REAL n) such that A56: (Fr A) /\ (halfline ((0. (TOP-REAL n)),p2)) = {q} by A13; p2 in halfline ((0. (TOP-REAL n)),p2) by TOPREAL9:28; then p2 in {q} by A38, A51, A56, XBOOLE_0:def_4; then A57: p2 = q by TARSKI:def_1; |.((1 / |.p2.|) * p2).| = 1 by A10, A24, A53; then A58: (1 / |.p2.|) * p2 <> 0. (TOP-REAL n) by TOPRNS_1:23; A59: (0. (TOP-REAL n)) + ((1 / |.p2.|) * p2) = (1 / |.p2.|) * p2 by RLVECT_1:4; A60: b . p2 = (1 / |.p2.|) * p2 by A10, A24, A53; A61: ( H . x1 = b . x1 & H . x2 = b . x2 ) by A35, A50, A51, FUNCT_1:47; (1 - (1 / |.p1.|)) * (0. (TOP-REAL n)) = 0. (TOP-REAL n) by RLVECT_1:10; then A62: (1 / |.p1.|) * p1 in halfline ((0. (TOP-REAL n)),p1) by A52, A55, A59, A60, A61; (1 - (1 / |.p2.|)) * (0. (TOP-REAL n)) = 0. (TOP-REAL n) by RLVECT_1:10; then (1 / |.p2.|) * p2 in halfline ((0. (TOP-REAL n)),p2) by A59; then halfline ((0. (TOP-REAL n)),p2) = halfline ((0. (TOP-REAL n)),((1 / |.p1.|) * p1)) by A52, A55, A58, A60, A61, TOPREAL9:31 .= halfline ((0. (TOP-REAL n)),p1) by A52, A55, A58, A60, A61, A62, TOPREAL9:31 ; then p1 in halfline ((0. (TOP-REAL n)),p2) by TOPREAL9:28; then p1 in {q} by A38, A50, A56, XBOOLE_0:def_4; hence x1 = x2 by A57, TARSKI:def_1; ::_thesis: verum end; then A63: H is one-to-one by FUNCT_1:def_4; then H is being_homeomorphism by A2, A18, A48, A49, COMPTS_1:17, PRE_TOPC:27; then reconsider H1 = H " as continuous Function of ((TOP-REAL n) | (Sphere ((0. (TOP-REAL n)),1))),(((TOP-REAL n) | cTR0) | FrA) by TOPS_2:def_5; reconsider HH = H as Function ; set nN0F = nN0 | (((TOP-REAL n) | cTR0) | FrA); reconsider H1B = H1 * B as Function of ((TOP-REAL n) | cTR0),(((TOP-REAL n) | cTR0) | FrA) by A48; reconsider NH1B = (nN0 | (((TOP-REAL n) | cTR0) | FrA)) * H1B as Function of ((TOP-REAL n) | cTR0),R^1 ; A64: nN0 | (((TOP-REAL n) | cTR0) | FrA) = nN0 | the carrier of (((TOP-REAL n) | cTR0) | FrA) by TMAP_1:def_4; then ( rng NH1B c= rng (nN0 | (((TOP-REAL n) | cTR0) | FrA)) & rng (nN0 | (((TOP-REAL n) | cTR0) | FrA)) c= rng nN0 ) by RELAT_1:26, RELAT_1:70; then rng NH1B c= rng nN0 by XBOOLE_1:1; then A65: not 0 in rng NH1B by A20; ( B is continuous & not Sphere ((0. (TOP-REAL n)),1) is empty ) by A28, PRE_TOPC:27; then reconsider NH1B = NH1B as non-empty continuous Function of ((TOP-REAL n) | cTR0),R^1 by A65, RELAT_1:def_9; reconsider G = I NH1B as Function of ((TOP-REAL n) | cTR0),(TOP-REAL n) by TOPREALC:46; A66: dom G = cTR0 by A10, FUNCT_2:def_1; A67: dom (nN0 | (((TOP-REAL n) | cTR0) | FrA)) = FrA by A38, FUNCT_2:def_1; A68: for p being Point of (TOP-REAL n) st p in cTR0 holds ex Hp being Point of (TOP-REAL n) st ( Hp = H1B . p & Hp in FrA & G . p = (1 / |.Hp.|) * p & |.Hp.| > 0 ) proof let p be Point of (TOP-REAL n); ::_thesis: ( p in cTR0 implies ex Hp being Point of (TOP-REAL n) st ( Hp = H1B . p & Hp in FrA & G . p = (1 / |.Hp.|) * p & |.Hp.| > 0 ) ) assume A69: p in cTR0 ; ::_thesis: ex Hp being Point of (TOP-REAL n) st ( Hp = H1B . p & Hp in FrA & G . p = (1 / |.Hp.|) * p & |.Hp.| > 0 ) then A70: p in dom NH1B by A10, FUNCT_2:def_1; then A71: H1B . p in dom (nN0 | (((TOP-REAL n) | cTR0) | FrA)) by FUNCT_1:11; then reconsider Hp = H1B . p as Point of (TOP-REAL n) by A67; A72: (nN0 | (((TOP-REAL n) | cTR0) | FrA)) . Hp = nN0 . Hp by A64, A71, FUNCT_1:49; A73: ( (n NormF) . Hp = |.Hp.| & nN0 . Hp = (n NormF) . Hp ) by A19, A67, A71, FUNCT_1:49, JGRAPH_4:def_1; take Hp ; ::_thesis: ( Hp = H1B . p & Hp in FrA & G . p = (1 / |.Hp.|) * p & |.Hp.| > 0 ) A74: NH1B . p = (nN0 | (((TOP-REAL n) | cTR0) | FrA)) . (H1B . p) by A70, FUNCT_1:12; G . p = (I . p) (/) (NH1B . p) by A66, A69, VALUED_2:72 .= p (/) |.Hp.| by A10, A69, A74, A72, A73, TMAP_1:84 .= (1 / |.Hp.|) (#) p by VALUED_2:def_32 .= (1 / |.Hp.|) * p ; hence ( Hp = H1B . p & Hp in FrA & G . p = (1 / |.Hp.|) * p & |.Hp.| > 0 ) by A38, A64, A70, A71, A74, A73, FUNCT_1:49; ::_thesis: verum end; A75: not 0. (TOP-REAL n) in rng G proof assume 0. (TOP-REAL n) in rng G ; ::_thesis: contradiction then consider p being set such that A76: p in dom G and A77: G . p = 0. (TOP-REAL n) by FUNCT_1:def_3; reconsider p = p as Point of (TOP-REAL n) by A66, A76; consider Hp being Point of (TOP-REAL n) such that Hp = H1B . p and Hp in FrA and A78: ( G . p = (1 / |.Hp.|) * p & |.Hp.| > 0 ) by A10, A68, A76; p <> 0. (TOP-REAL n) by A10, A76, ZFMISC_1:56; hence contradiction by A77, A78, RLVECT_1:11; ::_thesis: verum end; A79: for x1, x2 being set st x1 in dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) & x2 in (dom G) \ (dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n)))) holds ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) . x1 <> G . x2 proof let x1, x2 be set ; ::_thesis: ( x1 in dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) & x2 in (dom G) \ (dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n)))) implies ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) . x1 <> G . x2 ) assume that A80: x1 in dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) and A81: x2 in (dom G) \ (dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n)))) ; ::_thesis: ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) . x1 <> G . x2 x1 = 0. (TOP-REAL n) by A80, TARSKI:def_1; then A82: ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) . x1 = 0. (TOP-REAL n) by FUNCOP_1:72; x2 in dom G by A81, XBOOLE_0:def_5; hence ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) . x1 <> G . x2 by A75, A82, FUNCT_1:def_3; ::_thesis: verum end; H is onto by A18, A48, FUNCT_2:def_3; then A83: H " = HH " by A63, TOPS_2:def_4; A84: for p being Point of (TOP-REAL n) st p in cTR0 holds (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {(H1B . p)} proof let p be Point of (TOP-REAL n); ::_thesis: ( p in cTR0 implies (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {(H1B . p)} ) assume A85: p in cTR0 ; ::_thesis: (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {(H1B . p)} then A86: p in dom H1B by A10, FUNCT_2:def_1; then A87: H1B . p = H1 . (B . p) by FUNCT_1:12; B . p in dom H1 by A86, FUNCT_1:11; then consider x being set such that A88: x in dom H and A89: H . x = B . p by A18, A48, FUNCT_1:def_3; reconsider x = x as Point of (TOP-REAL n) by A34, A38, A88; A90: H . x = b . x by A35, A88, FUNCT_1:47; set xp = |.x.| / |.p.|; A91: x in FrA by A38, A88; then A92: b . x = (1 / |.x.|) * x by A9, A24, A39; |.((1 / |.x.|) * x).| = 1 by A9, A24, A39, A91; then (1 / |.x.|) * x <> 0. (TOP-REAL n) by TOPRNS_1:23; then 1 / |.x.| <> 0 by RLVECT_1:10; then |.x.| > 0 ; then 1 = |.x.| / |.x.| by XCMPLX_1:60 .= |.x.| * (1 / |.x.|) ; then x = (|.x.| * (1 / |.x.|)) * x by RLVECT_1:def_8 .= |.x.| * ((1 / |.x.|) * x) by RLVECT_1:def_7 .= |.x.| * ((1 / |.p.|) * p) by A24, A85, A89, A90, A92 .= (|.x.| / |.p.|) * p by RLVECT_1:def_7 ; then x in halfline ((0. (TOP-REAL n)),p) by Lm2; then A93: x in (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) by A38, A88, XBOOLE_0:def_4; p <> 0. (TOP-REAL n) by A85, ZFMISC_1:56; then consider y being Point of (TOP-REAL n) such that A94: (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {y} by A13; H1 . (B . p) = x by A63, A83, A88, A89, FUNCT_1:34; hence (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {(H1B . p)} by A87, A93, A94, TARSKI:def_1; ::_thesis: verum end; for x1, x2 being set st x1 in dom G & x2 in dom G & G . x1 = G . x2 holds x1 = x2 proof let x1, x2 be set ; ::_thesis: ( x1 in dom G & x2 in dom G & G . x1 = G . x2 implies x1 = x2 ) assume that A95: x1 in dom G and A96: x2 in dom G and A97: G . x1 = G . x2 ; ::_thesis: x1 = x2 reconsider p1 = x1, p2 = x2 as Point of (TOP-REAL n) by A66, A95, A96; consider Hp1 being Point of (TOP-REAL n) such that A98: Hp1 = H1B . p1 and Hp1 in FrA and A99: G . p1 = (1 / |.Hp1.|) * p1 and A100: |.Hp1.| > 0 by A10, A68, A95; A101: FrA /\ (halfline ((0. (TOP-REAL n)),p1)) = {Hp1} by A10, A84, A95, A98; consider Hp2 being Point of (TOP-REAL n) such that A102: Hp2 = H1B . p2 and Hp2 in FrA and A103: G . p2 = (1 / |.Hp2.|) * p2 and |.Hp2.| > 0 by A10, A68, A96; p1 <> 0. (TOP-REAL n) by A10, A95, ZFMISC_1:56; then A104: (1 / |.Hp1.|) * p1 <> 0. (TOP-REAL n) by A100, RLVECT_1:11; then halfline ((0. (TOP-REAL n)),p1) = halfline ((0. (TOP-REAL n)),((1 / |.Hp1.|) * p1)) by Lm2, TOPREAL9:31 .= halfline ((0. (TOP-REAL n)),p2) by A97, A99, A103, A104, Lm2, TOPREAL9:31 ; then ( Hp1 in {Hp1} & {Hp1} = {Hp2} ) by A10, A84, A96, A101, A102, TARSKI:def_1; then 1 / |.Hp1.| = 1 / |.Hp2.| by TARSKI:def_1; hence x1 = x2 by A97, A99, A100, A103, RLVECT_1:36; ::_thesis: verum end; then A105: G is one-to-one by FUNCT_1:def_4; set G0 = G +* ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))); A106: dom (G +* ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n)))) = (dom G) \/ (dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n)))) by FUNCT_4:def_1 .= cTR0 \/ {(0. (TOP-REAL n))} by A32, A66, FUNCOP_1:13 .= the carrier of (TOP-REAL n) by ZFMISC_1:116 ; A107: for p, Hp being Point of (TOP-REAL n) st p in cTR0 & Hp = H1B . p holds ( p = G . (|.Hp.| * p) & |.Hp.| * p in dom G ) proof let p, Hp1 be Point of (TOP-REAL n); ::_thesis: ( p in cTR0 & Hp1 = H1B . p implies ( p = G . (|.Hp1.| * p) & |.Hp1.| * p in dom G ) ) assume that A108: p in cTR0 and A109: Hp1 = H1B . p ; ::_thesis: ( p = G . (|.Hp1.| * p) & |.Hp1.| * p in dom G ) reconsider p = p as Point of (TOP-REAL n) ; consider Hp being Point of (TOP-REAL n) such that A110: Hp = H1B . p and Hp in FrA and G . p = (1 / |.Hp.|) * p and A111: |.Hp.| > 0 by A68, A108; set Hpp = |.Hp.| * p; p <> 0. (TOP-REAL n) by A108, ZFMISC_1:56; then A112: |.Hp.| * p <> 0. (TOP-REAL n) by A111, RLVECT_1:11; then A113: |.Hp.| * p in cTR0 by ZFMISC_1:56; then consider HP being Point of (TOP-REAL n) such that A114: HP = H1B . (|.Hp.| * p) and HP in FrA and A115: G . (|.Hp.| * p) = (1 / |.HP.|) * (|.Hp.| * p) and |.HP.| > 0 by A68; A116: Hp in {Hp} by TARSKI:def_1; {HP} = (Fr A) /\ (halfline ((0. (TOP-REAL n)),(|.Hp.| * p))) by A84, A113, A114 .= (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) by A112, Lm2, TOPREAL9:31 .= {Hp} by A84, A108, A110 ; then G . (|.Hp.| * p) = (1 / |.Hp.|) * (|.Hp.| * p) by A115, A116, TARSKI:def_1 .= (|.Hp.| / |.Hp.|) * p by RLVECT_1:def_7 .= 1 * p by A111, XCMPLX_1:60 .= p by RLVECT_1:def_8 ; hence ( p = G . (|.Hp1.| * p) & |.Hp1.| * p in dom G ) by A66, A109, A110, A112, ZFMISC_1:56; ::_thesis: verum end; A117: Sphere ((0. (TOP-REAL n)),1) c= G .: FrA proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in Sphere ((0. (TOP-REAL n)),1) or p in G .: FrA ) assume A118: p in Sphere ((0. (TOP-REAL n)),1) ; ::_thesis: p in G .: FrA then reconsider p = p as Point of (TOP-REAL n) ; |.p.| = 1 by A118, TOPREAL9:12; then p <> 0. (TOP-REAL n) by TOPRNS_1:23; then A119: p in cTR0 by ZFMISC_1:56; then consider Hp being Point of (TOP-REAL n) such that A120: Hp = H1B . p and A121: Hp in FrA and G . p = (1 / |.Hp.|) * p and |.Hp.| > 0 by A68; set Hpp = |.Hp.| * p; A122: ( p = G . (|.Hp.| * p) & |.Hp.| * p in dom G ) by A107, A119, A120; ( Hp in {Hp} & (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {Hp} ) by A84, A119, A120, TARSKI:def_1; then A123: Hp in halfline ((0. (TOP-REAL n)),p) by XBOOLE_0:def_4; A124: Hp - (0. (TOP-REAL n)) = Hp by RLVECT_1:13; abs |.Hp.| = |.Hp.| by ABSVALUE:def_1; then A125: |.(|.Hp.| * p).| = |.Hp.| * |.p.| by TOPRNS_1:7 .= |.Hp.| * 1 by A118, TOPREAL9:12 ; ( (|.Hp.| * p) - (0. (TOP-REAL n)) = |.Hp.| * p & |.Hp.| * p in halfline ((0. (TOP-REAL n)),p) ) by Lm2, RLVECT_1:13; then Hp = |.Hp.| * p by A125, A123, A124, Th2; hence p in G .: FrA by A121, A122, FUNCT_1:def_6; ::_thesis: verum end; A126: 0. (TOP-REAL n) in {(0. (TOP-REAL n))} by TARSKI:def_1; then A127: ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) . (0. (TOP-REAL n)) = 0. (TOP-REAL n) by A32, FUNCOP_1:7; rng ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) = {(0. (TOP-REAL n))} by A32, FUNCOP_1:8; then rng (G +* ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n)))) = (rng G) \/ {(0. (TOP-REAL n))} by A33, A66, NECKLACE:6, XBOOLE_1:79; then reconsider G1 = G +* ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) as one-to-one Function of (TOP-REAL n),(TOP-REAL n) by A106, A79, A105, FUNCT_2:2, TOPMETR2:1; A128: G1 . (0. (TOP-REAL n)) = ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) . (0. (TOP-REAL n)) by A33, A126, FUNCT_4:13; A129: G .: FrA c= Sphere ((0. (TOP-REAL n)),1) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in G .: FrA or y in Sphere ((0. (TOP-REAL n)),1) ) assume y in G .: FrA ; ::_thesis: y in Sphere ((0. (TOP-REAL n)),1) then consider p being set such that A130: p in dom G and A131: p in FrA and A132: G . p = y by FUNCT_1:def_6; reconsider p = p as Point of (TOP-REAL n) by A131; consider Hp being Point of (TOP-REAL n) such that A133: Hp = H1B . p and Hp in FrA and A134: G . p = (1 / |.Hp.|) * p and A135: |.Hp.| > 0 by A10, A68, A130; p in halfline ((0. (TOP-REAL n)),p) by TOPREAL9:28; then A136: p in FrA /\ (halfline ((0. (TOP-REAL n)),p)) by A131, XBOOLE_0:def_4; FrA /\ (halfline ((0. (TOP-REAL n)),p)) = {Hp} by A10, A84, A130, A133; then A137: p = Hp by A136, TARSKI:def_1; abs (1 / |.Hp.|) = 1 / |.Hp.| by ABSVALUE:def_1; then |.((1 / |.Hp.|) * p).| = (1 / |.Hp.|) * |.Hp.| by A137, TOPRNS_1:7 .= 1 by A135, XCMPLX_1:106 ; then |.(((1 / |.Hp.|) * p) - (0. (TOP-REAL n))).| = 1 by RLVECT_1:13; hence y in Sphere ((0. (TOP-REAL n)),1) by A132, A134; ::_thesis: verum end; set TRnCL = (TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1)); set TRnA = (TOP-REAL n) | A; A138: Int A c= A by TOPS_1:16; set GA = G1 | ((TOP-REAL n) | A); A139: G1 | ((TOP-REAL n) | A) = G1 | the carrier of ((TOP-REAL n) | A) by TMAP_1:def_4; A140: [#] ((TOP-REAL n) | A) = A by PRE_TOPC:def_5; then A141: dom (G1 | ((TOP-REAL n) | A)) = A by FUNCT_2:def_1; A142: dom (G1 | ((TOP-REAL n) | A)) = the carrier of ((TOP-REAL n) | A) by FUNCT_2:def_1; A143: cl_Ball ((0. (TOP-REAL n)),1) c= rng (G1 | ((TOP-REAL n) | A)) proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in cl_Ball ((0. (TOP-REAL n)),1) or p in rng (G1 | ((TOP-REAL n) | A)) ) assume A144: p in cl_Ball ((0. (TOP-REAL n)),1) ; ::_thesis: p in rng (G1 | ((TOP-REAL n) | A)) then reconsider p = p as Point of (TOP-REAL n) ; percases ( p = 0. (TOP-REAL n) or p <> 0. (TOP-REAL n) ) ; suppose p = 0. (TOP-REAL n) ; ::_thesis: p in rng (G1 | ((TOP-REAL n) | A)) then p = (G1 | ((TOP-REAL n) | A)) . (0. (TOP-REAL n)) by A3, A138, A5, A127, A139, A140, A128, FUNCT_1:49; hence p in rng (G1 | ((TOP-REAL n) | A)) by A3, A138, A5, A140, A142, FUNCT_1:def_3; ::_thesis: verum end; supposeA145: p <> 0. (TOP-REAL n) ; ::_thesis: p in rng (G1 | ((TOP-REAL n) | A)) set h = halfline ((0. (TOP-REAL n)),p); A146: p in cTR0 by A145, ZFMISC_1:56; then consider Hp being Point of (TOP-REAL n) such that A147: Hp = H1B . p and A148: Hp in FrA and G . p = (1 / |.Hp.|) * p and A149: |.Hp.| > 0 by A68; A150: abs |.Hp.| = |.Hp.| by ABSVALUE:def_1; (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {Hp} by A84, A146, A147; then Hp in (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) by TARSKI:def_1; then A151: Hp in halfline ((0. (TOP-REAL n)),p) by XBOOLE_0:def_4; Hp <> 0. (TOP-REAL n) by A149, TOPRNS_1:23; then halfline ((0. (TOP-REAL n)),p) = halfline ((0. (TOP-REAL n)),Hp) by A151, TOPREAL9:31; then A152: |.p.| * Hp in halfline ((0. (TOP-REAL n)),p) by Lm2; |.p.| <= 1 by A144, TOPREAL9:11; then ( (1 - |.p.|) * (0. (TOP-REAL n)) = 0. (TOP-REAL n) & (|.p.| * Hp) + ((1 - |.p.|) * (0. (TOP-REAL n))) in A ) by A3, A138, A5, A17, A148, RLTOPSP1:def_1, RLVECT_1:10; then |.p.| * Hp in dom (G1 | ((TOP-REAL n) | A)) by A141, RLVECT_1:4; then A153: ( (G1 | ((TOP-REAL n) | A)) . (|.p.| * Hp) in rng (G1 | ((TOP-REAL n) | A)) & (G1 | ((TOP-REAL n) | A)) . (|.p.| * Hp) = G1 . (|.p.| * Hp) ) by A139, FUNCT_1:47, FUNCT_1:def_3; A154: |.Hp.| * p in halfline ((0. (TOP-REAL n)),p) by Lm2; |.Hp.| * p in dom G by A107, A146, A147; then |.Hp.| * p <> 0. (TOP-REAL n) by A10, ZFMISC_1:56; then not |.Hp.| * p in dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) by TARSKI:def_1; then A155: G . (|.Hp.| * p) = G1 . (|.Hp.| * p) by FUNCT_4:11; abs |.p.| = |.p.| by ABSVALUE:def_1; then |.(|.p.| * Hp).| = |.p.| * |.Hp.| by TOPRNS_1:7 .= |.(|.Hp.| * p).| by A150, TOPRNS_1:7 ; then A156: |.((|.p.| * Hp) - (0. (TOP-REAL n))).| = |.(|.Hp.| * p).| by RLVECT_1:13 .= |.((|.Hp.| * p) - (0. (TOP-REAL n))).| by RLVECT_1:13 ; p = G . (|.Hp.| * p) by A107, A146, A147; hence p in rng (G1 | ((TOP-REAL n) | A)) by A152, A155, A156, A153, A154, Th2; ::_thesis: verum end; end; end; rng (G1 | ((TOP-REAL n) | A)) c= cl_Ball ((0. (TOP-REAL n)),1) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (G1 | ((TOP-REAL n) | A)) or x in cl_Ball ((0. (TOP-REAL n)),1) ) assume x in rng (G1 | ((TOP-REAL n) | A)) ; ::_thesis: x in cl_Ball ((0. (TOP-REAL n)),1) then consider p being set such that A157: p in dom (G1 | ((TOP-REAL n) | A)) and A158: (G1 | ((TOP-REAL n) | A)) . p = x by FUNCT_1:def_3; reconsider p = p as Point of (TOP-REAL n) by A141, A157; A159: (G1 | ((TOP-REAL n) | A)) . p = G1 . p by A139, A157, FUNCT_1:47; A160: (G1 . p) - (0. (TOP-REAL n)) = G1 . p by RLVECT_1:13; percases ( p = 0. (TOP-REAL n) or p <> 0. (TOP-REAL n) ) ; suppose p = 0. (TOP-REAL n) ; ::_thesis: x in cl_Ball ((0. (TOP-REAL n)),1) then G1 . p = 0. (TOP-REAL n) by A32, A126, A128, FUNCOP_1:7; then |.((G1 . p) - (0. (TOP-REAL n))).| = 0 by A160, TOPRNS_1:23; hence x in cl_Ball ((0. (TOP-REAL n)),1) by A158, A159; ::_thesis: verum end; supposeA161: p <> 0. (TOP-REAL n) ; ::_thesis: x in cl_Ball ((0. (TOP-REAL n)),1) set h = halfline ((0. (TOP-REAL n)),p); A162: A /\ (halfline ((0. (TOP-REAL n)),p)) c= aa by XBOOLE_1:17; then reconsider F = A /\ (halfline ((0. (TOP-REAL n)),p)) as Subset of (Euclid n) by XBOOLE_1:1; F is bounded by A12, A162, HAUSDORF:18, TBSP_1:14; then A /\ (halfline ((0. (TOP-REAL n)),p)) is bounded by JORDAN2C:11; then consider w being Point of (Euclid n) such that A163: w in (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) and A164: for u, P being Point of (Euclid n) st P = 0. (TOP-REAL n) & u in A /\ (halfline ((0. (TOP-REAL n)),p)) holds dist (P,u) <= dist (P,w) and for r being real number st r > 0 holds ex u being Point of (Euclid n) st ( u in A /\ (halfline ((0. (TOP-REAL n)),p)) & dist (w,u) < r ) by A3, A138, A5, A161, Lm3; reconsider P = p as Point of (Euclid n) by EUCLID:67; p in halfline ((0. (TOP-REAL n)),p) by TOPREAL9:28; then A165: p in A /\ (halfline ((0. (TOP-REAL n)),p)) by A140, A157, XBOOLE_0:def_4; A166: not p in dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) by A161, TARSKI:def_1; A167: p in cTR0 by A161, ZFMISC_1:56; then consider Hp being Point of (TOP-REAL n) such that A168: Hp = H1B . p and Hp in FrA and A169: G . p = (1 / |.Hp.|) * p and |.Hp.| > 0 by A68; abs (1 / |.Hp.|) = 1 / |.Hp.| by ABSVALUE:def_1; then A170: |.((1 / |.Hp.|) * p).| = |.p.| / |.Hp.| by TOPRNS_1:7; (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {Hp} by A84, A167, A168; then w = Hp by A163, TARSKI:def_1; then A171: dist (0TRn,w) = |.((0. (TOP-REAL n)) - Hp).| by SPPOL_1:39 .= |.(- Hp).| by RLVECT_1:14 .= |.Hp.| by TOPRNS_1:26 ; dist (0TRn,P) = |.((0. (TOP-REAL n)) - p).| by SPPOL_1:39 .= |.(- p).| by RLVECT_1:14 .= |.p.| by TOPRNS_1:26 ; then |.((1 / |.Hp.|) * p).| <= 1 by A164, A165, A170, A171, XREAL_1:183; then |.(G1 . p).| <= 1 by A166, A169, FUNCT_4:11; hence x in cl_Ball ((0. (TOP-REAL n)),1) by A158, A159, A160; ::_thesis: verum end; end; end; then A172: rng (G1 | ((TOP-REAL n) | A)) = cl_Ball ((0. (TOP-REAL n)),1) by A143, XBOOLE_0:def_10; A173: [#] ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) = cl_Ball ((0. (TOP-REAL n)),1) by PRE_TOPC:def_5; then reconsider GA = G1 | ((TOP-REAL n) | A) as Function of ((TOP-REAL n) | A),((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) by A140, A141, A172, FUNCT_2:1; set e2 = e / 2; A174: GA is one-to-one by A139, FUNCT_1:52; A175: e / 2 < e by A6, XREAL_1:216; A176: G1 is continuous proof let x be Point of (TOP-REAL n); :: according to BORSUK_1:def_1 ::_thesis: for b1 being a_neighborhood of G1 . x ex b2 being a_neighborhood of x st G1 .: b2 c= b1 let U be a_neighborhood of G1 . x; ::_thesis: ex b1 being a_neighborhood of x st G1 .: b1 c= U percases ( x <> 0. (TOP-REAL n) or x = 0. (TOP-REAL n) ) ; supposeA177: x <> 0. (TOP-REAL n) ; ::_thesis: ex b1 being a_neighborhood of x st G1 .: b1 c= U then A178: x in dom G by A66, ZFMISC_1:56; then reconsider X = x as Point of ((TOP-REAL n) | cTR0) ; not x in dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) by A177, TARSKI:def_1; then A179: G . x = G1 . x by FUNCT_4:11; then A180: G1 . x <> 0. (TOP-REAL n) by A75, A178, FUNCT_1:def_3; then reconsider G1x = G1 . x as Point of ((TOP-REAL n) | cTR0) by A10, ZFMISC_1:56; G1 . x in cTR0 by A180, ZFMISC_1:56; then cTR0 is a_neighborhood of G1 . x by CONNSP_2:3; then cTR0 /\ U is a_neighborhood of G1 . x by CONNSP_2:2; then consider H being a_neighborhood of X such that A181: G .: H c= cTR0 /\ U by A179, BORSUK_1:def_1; reconsider h = H as Subset of (TOP-REAL n) by A10, XBOOLE_1:1; reconsider h = h as a_neighborhood of x by CONNSP_2:9; {(0. (TOP-REAL n))} misses H by A10, XBOOLE_1:63, XBOOLE_1:79; then ( cTR0 /\ U c= U & G .: H = G1 .: h ) by A32, BOOLMARK:3, XBOOLE_1:17; hence ex b1 being a_neighborhood of x st G1 .: b1 c= U by A181, XBOOLE_1:1; ::_thesis: verum reconsider U1 = cTR0 /\ U as Subset of ((TOP-REAL n) | cTR0) by A10, XBOOLE_1:17; end; supposeA182: x = 0. (TOP-REAL n) ; ::_thesis: ex b1 being a_neighborhood of x st G1 .: b1 c= U reconsider 0TRn = 0. (TOP-REAL n) as Point of (Euclid n) by EUCLID:67; A183: 0. (TOP-REAL n) in Int U by A127, A128, A182, CONNSP_2:def_1; then consider r being real number such that A184: r > 0 and A185: Ball (0TRn,r) c= U by GOBOARD6:5; reconsider B = Ball (0TRn,(r * (e / 2))) as Subset of (TOP-REAL n) by EUCLID:67; 0TRn in Int B by A6, A184, GOBOARD6:5; then reconsider Bx = B as a_neighborhood of x by A182, CONNSP_2:def_1; take Bx ; ::_thesis: G1 .: Bx c= U let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in G1 .: Bx or y in U ) assume A186: y in G1 .: Bx ; ::_thesis: y in U then reconsider p = y as Point of (TOP-REAL n) ; A187: Int U c= U by TOPS_1:16; percases ( y = 0. (TOP-REAL n) or p <> 0. (TOP-REAL n) ) ; suppose y = 0. (TOP-REAL n) ; ::_thesis: y in U hence y in U by A183, A187; ::_thesis: verum end; supposeA188: p <> 0. (TOP-REAL n) ; ::_thesis: y in U set PP = ((e / 2) / |.p.|) * p; abs ((e / 2) / |.p.|) = (e / 2) / |.p.| by A6, ABSVALUE:def_1; then A189: |.(((e / 2) / |.p.|) * p).| = ((e / 2) / |.p.|) * |.p.| by TOPRNS_1:7 .= (e / 2) * (|.p.| / |.p.|) .= (e / 2) * 1 by A188, TOPRNS_1:24, XCMPLX_1:60 .= e / 2 ; then |.((((e / 2) / |.p.|) * p) - (0. (TOP-REAL n))).| < e by A175, RLVECT_1:13; then A190: ((e / 2) / |.p.|) * p in Ball ((0. (TOP-REAL n)),e) ; set h = halfline ((0. (TOP-REAL n)),p); A191: A /\ (halfline ((0. (TOP-REAL n)),p)) c= aa by XBOOLE_1:17; then reconsider F = A /\ (halfline ((0. (TOP-REAL n)),p)) as Subset of (Euclid n) by XBOOLE_1:1; F is bounded by A12, A191, HAUSDORF:18, TBSP_1:14; then A /\ (halfline ((0. (TOP-REAL n)),p)) is bounded by JORDAN2C:11; then consider w being Point of (Euclid n) such that A192: w in (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) and A193: for u, P being Point of (Euclid n) st P = 0. (TOP-REAL n) & u in A /\ (halfline ((0. (TOP-REAL n)),p)) holds dist (P,u) <= dist (P,w) and for r being real number st r > 0 holds ex u being Point of (Euclid n) st ( u in A /\ (halfline ((0. (TOP-REAL n)),p)) & dist (w,u) < r ) by A3, A138, A5, A188, Lm3; A194: p in cTR0 by A188, ZFMISC_1:56; then consider Hp being Point of (TOP-REAL n) such that A195: Hp = H1B . p and Hp in FrA and G . p = (1 / |.Hp.|) * p and A196: |.Hp.| > 0 by A68; (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {Hp} by A84, A194, A195; then w = Hp by A192, TARSKI:def_1; then A197: dist (0TRn,w) = |.((0. (TOP-REAL n)) - Hp).| by SPPOL_1:39 .= |.(- Hp).| by RLVECT_1:14 .= |.Hp.| by TOPRNS_1:26 ; set Hpp = |.Hp.| * p; |.Hp.| * p in dom G by A107, A194, A195; then |.Hp.| * p <> 0. (TOP-REAL n) by A10, ZFMISC_1:56; then not |.Hp.| * p in dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) by TARSKI:def_1; then A198: G . (|.Hp.| * p) = G1 . (|.Hp.| * p) by FUNCT_4:11; |.Hp.| = abs |.Hp.| by ABSVALUE:def_1; then A199: ( Bx = Ball ((0. (TOP-REAL n)),(r * (e / 2))) & |.(|.Hp.| * p).| = |.Hp.| * |.p.| ) by TOPREAL9:13, TOPRNS_1:7; reconsider pp = ((e / 2) / |.p.|) * p as Point of (Euclid n) by EUCLID:67; consider x being set such that A200: x in dom G1 and A201: x in Bx and A202: G1 . x = p by A186, FUNCT_1:def_6; ( ((e / 2) / |.p.|) * p in halfline ((0. (TOP-REAL n)),p) & Ball ((0. (TOP-REAL n)),e) = Ball (0TRn,e) ) by A6, Lm2, TOPREAL9:13; then A203: pp in A /\ (halfline ((0. (TOP-REAL n)),p)) by A7, A190, XBOOLE_0:def_4; dist (0TRn,pp) = |.((0. (TOP-REAL n)) - (((e / 2) / |.p.|) * p)).| by SPPOL_1:39 .= |.(- (((e / 2) / |.p.|) * p)).| by RLVECT_1:14 .= e / 2 by A189, TOPRNS_1:26 ; then (e / 2) / |.Hp.| <= 1 by A193, A197, A203, XREAL_1:183; then A204: r * ((e / 2) / |.Hp.|) <= r * 1 by A184, XREAL_1:64; p = G . (|.Hp.| * p) by A107, A194, A195; then |.Hp.| * p = x by A106, A198, A200, A202, FUNCT_1:def_4; then |.p.| < (r * (e / 2)) / |.Hp.| by A196, A199, A201, TOPREAL9:10, XREAL_1:81; then |.p.| < r by A204, XXREAL_0:2; then |.(p - (0. (TOP-REAL n))).| < r by RLVECT_1:13; then p in Ball ((0. (TOP-REAL n)),r) ; then p in Ball (0TRn,r) by TOPREAL9:13; hence y in U by A185; ::_thesis: verum end; end; end; end; end; GA .: FrA = G1 .: FrA by A2, A139, A140, RELAT_1:129, TOPS_1:35; then GA .: FrA = G .: FrA by A5, A8, A32, BOOLMARK:3, ZFMISC_1:50; then A205: GA .: FrA = Sphere ((0. (TOP-REAL n)),1) by A117, A129, XBOOLE_0:def_10; ( dom GA = [#] ((TOP-REAL n) | A) & rng GA = [#] ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) ) by A143, A173, FUNCT_2:def_1, XBOOLE_0:def_10; then GA is being_homeomorphism by A2, A3, A138, A174, A176, COMPTS_1:17, PRE_TOPC:27; hence ex h being Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) st ( h is being_homeomorphism & h .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) ) by A205; ::_thesis: verum end; theorem Th5: :: BROUWER2:5 for n being Nat for p being Point of (TOP-REAL n) for r being real number st r > 0 holds Fr (cl_Ball (p,r)) = Sphere (p,r) proof let n be Nat; ::_thesis: for p being Point of (TOP-REAL n) for r being real number st r > 0 holds Fr (cl_Ball (p,r)) = Sphere (p,r) let p be Point of (TOP-REAL n); ::_thesis: for r being real number st r > 0 holds Fr (cl_Ball (p,r)) = Sphere (p,r) let r be real number ; ::_thesis: ( r > 0 implies Fr (cl_Ball (p,r)) = Sphere (p,r) ) set TR = TOP-REAL n; assume A1: r > 0 ; ::_thesis: Fr (cl_Ball (p,r)) = Sphere (p,r) set CB = cl_Ball (p,r); set B = Ball (p,r); set S = Sphere (p,r); reconsider tr = TOP-REAL n as TopSpace ; reconsider cb = cl_Ball (p,r) as Subset of tr ; A2: n in NAT by ORDINAL1:def_12; then A3: Ball (p,r) misses Sphere (p,r) by TOPREAL9:19; A4: (Ball (p,r)) \/ (Sphere (p,r)) = cl_Ball (p,r) by A2, TOPREAL9:18; A5: Int cb c= Ball (p,r) proof reconsider ONE = 1 as Real ; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Int cb or x in Ball (p,r) ) assume x in Int cb ; ::_thesis: x in Ball (p,r) then consider Q being Subset of (TOP-REAL n) such that A6: Q is open and A7: Q c= cl_Ball (p,r) and A8: x in Q by TOPS_1:22; reconsider q = x as Point of (TOP-REAL n) by A8; consider w being real positive number such that A9: Ball (q,w) c= Q by A6, A8, TOPS_4:2; assume not x in Ball (p,r) ; ::_thesis: contradiction then q in Sphere (p,r) by A4, A7, A8, XBOOLE_0:def_3; then A10: |.(q - p).| = r by A2, TOPREAL9:9; set w2 = w / 2; set wr = ((w / 2) / r) * (q - p); A11: abs ((w / 2) / r) = (w / 2) / r by A1, ABSVALUE:def_1; A12: ((((w / 2) / r) * (q - p)) + q) - p = (((w / 2) / r) * (q - p)) + (q - p) by RLVECT_1:28 .= (((w / 2) / r) * (q - p)) + (ONE * (q - p)) by RLVECT_1:def_8 .= (((w / 2) / r) + ONE) * (q - p) by RLVECT_1:def_6 ; |.(((((w / 2) / r) * (q - p)) + q) - q).| = |.((((w / 2) / r) * (q - p)) + (q - q)).| by EUCLID:45 .= |.((((w / 2) / r) * (q - p)) + (0. (TOP-REAL n))).| by RLVECT_1:15 .= |.(((w / 2) / r) * (q - p)).| by RLVECT_1:def_4 .= ((w / 2) / r) * r by A2, A10, A11, TOPRNS_1:7 .= w / 2 by A1, XCMPLX_1:87 ; then |.(((((w / 2) / r) * (q - p)) + q) - q).| < w by XREAL_1:216; then (((w / 2) / r) * (q - p)) + q in Ball (q,w) ; then A13: (((w / 2) / r) * (q - p)) + q in Q by A9; A14: ((w / 2) / r) + ONE = ((w / 2) / r) + (r / r) by A1, XCMPLX_1:60 .= ((w / 2) + r) / r ; A15: (w / 2) + r > 0 + r by XREAL_1:6; abs (((w / 2) + r) / r) = ((w / 2) + r) / r by A1, ABSVALUE:def_1; then |.(((((w / 2) / r) * (q - p)) + q) - p).| = (((w / 2) + r) / r) * r by A2, A10, A14, A12, TOPRNS_1:7 .= (w / 2) + r by A1, XCMPLX_1:87 ; hence contradiction by A2, A7, A13, A15, TOPREAL9:8; ::_thesis: verum end; Ball (p,r) c= Int cb by A2, TOPREAL9:16, TOPS_1:24; then Int cb = Ball (p,r) by A5, XBOOLE_0:def_10; then Fr (cl_Ball (p,r)) = (cl_Ball (p,r)) \ (Ball (p,r)) by TOPS_1:43; hence Fr (cl_Ball (p,r)) = Sphere (p,r) by A4, A3, XBOOLE_1:88; ::_thesis: verum end; registration let n be Element of NAT ; let A be bounded Subset of (TOP-REAL n); let p be Point of (TOP-REAL n); clusterp + A -> bounded ; coherence p + A is bounded proof set TR = TOP-REAL n; set En = Euclid n; reconsider a = A as bounded Subset of (Euclid n) by JORDAN2C:11; reconsider pA = p + A as Subset of (Euclid n) by EUCLID:67; consider r being Real such that A1: 0 < r and A2: for x, y being Point of (Euclid n) st x in a & y in a holds dist (x,y) <= r by TBSP_1:def_7; A3: pA = { (p + u) where u is Element of (TOP-REAL n) : u in A } by RUSUB_4:def_8; now__::_thesis:_for_x,_y_being_Point_of_(Euclid_n)_st_x_in_pA_&_y_in_pA_holds_ dist_(x,y)_<=_r let x, y be Point of (Euclid n); ::_thesis: ( x in pA & y in pA implies dist (x,y) <= r ) assume x in pA ; ::_thesis: ( y in pA implies dist (x,y) <= r ) then consider px being Element of (TOP-REAL n) such that A4: x = p + px and A5: px in A by A3; assume y in pA ; ::_thesis: dist (x,y) <= r then consider py being Element of (TOP-REAL n) such that A6: y = p + py and A7: py in A by A3; reconsider pX = px, pY = py as Point of (Euclid n) by EUCLID:67; (p + px) - (p + py) = ((p + px) - p) - py by EUCLID:46 .= px - py by EUCLID:48 ; then dist (x,y) = |.(px - py).| by A4, A6, SPPOL_1:39 .= dist (pX,pY) by SPPOL_1:39 ; hence dist (x,y) <= r by A2, A5, A7; ::_thesis: verum end; then pA is bounded by A1, TBSP_1:def_7; hence p + A is bounded by JORDAN2C:11; ::_thesis: verum end; end; begin theorem Th6: :: BROUWER2:6 for n being Element of NAT for A being convex Subset of (TOP-REAL n) st A is compact & not A is boundary holds ex h being Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) st ( h is being_homeomorphism & h .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) ) proof let n be Element of NAT ; ::_thesis: for A being convex Subset of (TOP-REAL n) st A is compact & not A is boundary holds ex h being Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) st ( h is being_homeomorphism & h .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) ) set TRn = TOP-REAL n; let A be convex Subset of (TOP-REAL n); ::_thesis: ( A is compact & not A is boundary implies ex h being Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) st ( h is being_homeomorphism & h .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) ) ) assume A1: ( A is compact & not A is boundary ) ; ::_thesis: ex h being Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) st ( h is being_homeomorphism & h .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) ) Int A <> {} by A1, TOPS_1:48; then consider p being set such that A2: p in Int A by XBOOLE_0:def_1; set TRnA = (TOP-REAL n) | A; reconsider p = p as Point of (TOP-REAL n) by A2; A3: Int A c= A by TOPS_1:16; A4: not A is empty by A2; percases ( n = 0 or n > 0 ) ; supposeA5: n = 0 ; ::_thesis: ex h being Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) st ( h is being_homeomorphism & h .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) ) set T = Tdisk ((0. (TOP-REAL n)),1); A6: {(0. (TOP-REAL n))} = the carrier of (TOP-REAL n) by A5, EUCLID:22, EUCLID:77; then A7: A = {(0. (TOP-REAL n))} by A4, ZFMISC_1:33; then reconsider I = id ((TOP-REAL n) | A) as Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) by A6, ZFMISC_1:33; take I ; ::_thesis: ( I is being_homeomorphism & I .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) ) A8: Fr A = A \ (Int A) by A5, TOPS_1:43; A9: Sphere ((0. (TOP-REAL n)),1) = {} proof assume Sphere ((0. (TOP-REAL n)),1) <> {} ; ::_thesis: contradiction then Sphere ((0. (TOP-REAL n)),1) = A by A6, A7, ZFMISC_1:33; then |.(0. (TOP-REAL n)).| = 1 by A6, A7, TOPREAL9:12; hence contradiction by TOPRNS_1:23; ::_thesis: verum end; Int A = A by A2, A3, A7, ZFMISC_1:33; then A10: Fr A = {} by A8, XBOOLE_1:37; Tdisk ((0. (TOP-REAL n)),1) = (TOP-REAL n) | A by A6, A7, ZFMISC_1:33; hence ( I is being_homeomorphism & I .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) ) by A10, A9; ::_thesis: verum end; supposeA11: n > 0 ; ::_thesis: ex h being Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) st ( h is being_homeomorphism & h .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) ) set T = transl ((- p),(TOP-REAL n)); set TA = (transl ((- p),(TOP-REAL n))) .: A; A12: (transl ((- p),(TOP-REAL n))) .: A = (- p) + A by RLTOPSP1:33; then A13: ( 0. (TOP-REAL n) = 0* n & (transl ((- p),(TOP-REAL n))) .: A is convex ) by CONVEX1:7, EUCLID:70; reconsider TT = (transl ((- p),(TOP-REAL n))) | A as Function of ((TOP-REAL n) | A),((TOP-REAL n) | ((transl ((- p),(TOP-REAL n))) .: A)) by JORDAN24:12; A14: TT .: (Int A) = (transl ((- p),(TOP-REAL n))) .: (Int A) by RELAT_1:129, TOPS_1:16; 0. (TOP-REAL n) = (- p) + p by RLVECT_1:5; then A15: 0. (TOP-REAL n) in { ((- p) + q) where q is Element of (TOP-REAL n) : q in Int A } by A2; Int ((transl ((- p),(TOP-REAL n))) .: A) = (- p) + (Int A) by A12, RLTOPSP1:37; then 0. (TOP-REAL n) in Int ((transl ((- p),(TOP-REAL n))) .: A) by A15, RUSUB_4:def_8; then consider h being Function of ((TOP-REAL n) | ((transl ((- p),(TOP-REAL n))) .: A)),(Tdisk ((0. (TOP-REAL n)),1)) such that A16: h is being_homeomorphism and A17: h .: (Fr ((transl ((- p),(TOP-REAL n))) .: A)) = Sphere ((0. (TOP-REAL n)),1) by A1, A11, A12, A13, Lm4; reconsider hTT = h * TT as Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) by A4; take hTT ; ::_thesis: ( hTT is being_homeomorphism & hTT .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) ) A18: Int ((transl ((- p),(TOP-REAL n))) .: A) = (- p) + (Int A) by A12, RLTOPSP1:37 .= (transl ((- p),(TOP-REAL n))) .: (Int A) by RLTOPSP1:33 ; A19: TT is being_homeomorphism by JORDAN24:14; then dom TT = [#] ((TOP-REAL n) | A) by TOPS_2:def_5; then A20: dom TT = A by PRE_TOPC:def_5; thus hTT is being_homeomorphism by A4, A16, A19, TOPS_2:57; ::_thesis: hTT .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) rng TT = [#] ((TOP-REAL n) | ((transl ((- p),(TOP-REAL n))) .: A)) by A19, TOPS_2:def_5; then A21: rng TT = (transl ((- p),(TOP-REAL n))) .: A by PRE_TOPC:def_5; Fr A = A \ (Int A) by A1, TOPS_1:43; then A22: TT .: (Fr A) = (TT .: A) \ (TT .: (Int A)) by A19, FUNCT_1:64; Fr ((transl ((- p),(TOP-REAL n))) .: A) = ((transl ((- p),(TOP-REAL n))) .: A) \ (Int ((transl ((- p),(TOP-REAL n))) .: A)) by A1, A12, TOPS_1:43 .= TT .: (Fr A) by A18, A22, A20, A21, A14, RELAT_1:113 ; hence hTT .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) by A17, RELAT_1:126; ::_thesis: verum end; end; end; theorem Th7: :: BROUWER2:7 for n being Nat for A, B being convex Subset of (TOP-REAL n) st A is compact & not A is boundary & B is compact & not B is boundary holds ex h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st ( h is being_homeomorphism & h .: (Fr A) = Fr B ) proof let n be Nat; ::_thesis: for A, B being convex Subset of (TOP-REAL n) st A is compact & not A is boundary & B is compact & not B is boundary holds ex h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st ( h is being_homeomorphism & h .: (Fr A) = Fr B ) set T = TOP-REAL n; let A, B be convex Subset of (TOP-REAL n); ::_thesis: ( A is compact & not A is boundary & B is compact & not B is boundary implies ex h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st ( h is being_homeomorphism & h .: (Fr A) = Fr B ) ) assume that A1: ( A is compact & not A is boundary ) and A2: ( B is compact & not B is boundary ) ; ::_thesis: ex h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st ( h is being_homeomorphism & h .: (Fr A) = Fr B ) A3: ( not A is empty & not B is empty ) by A1, A2; reconsider N = n as Element of NAT by ORDINAL1:def_12; set TN = TOP-REAL N; consider hA being Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL N)),1)) such that A4: hA is being_homeomorphism and A5: hA .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) by A1, Th6; consider hB being Function of ((TOP-REAL n) | B),(Tdisk ((0. (TOP-REAL N)),1)) such that A6: hB is being_homeomorphism and A7: hB .: (Fr B) = Sphere ((0. (TOP-REAL n)),1) by A2, Th6; reconsider h = (hB ") * hA as Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) ; take h ; ::_thesis: ( h is being_homeomorphism & h .: (Fr A) = Fr B ) hB " is being_homeomorphism by A6, TOPS_2:56; hence h is being_homeomorphism by A3, A4, TOPS_2:57; ::_thesis: h .: (Fr A) = Fr B A8: rng hB = [#] (Tdisk ((0. (TOP-REAL N)),1)) by A6, TOPS_2:def_5; dom hB = [#] ((TOP-REAL n) | B) by A6, TOPS_2:def_5; then A9: dom hB = B by PRE_TOPC:def_5; the carrier of (Tdisk ((0. (TOP-REAL N)),1)) = cl_Ball ((0. (TOP-REAL N)),1) by BROUWER:3; then A10: Sphere ((0. (TOP-REAL n)),1) is Subset of (Tdisk ((0. (TOP-REAL N)),1)) by TOPREAL9:17; thus h .: (Fr A) = (hB ") .: (Sphere ((0. (TOP-REAL n)),1)) by A5, RELAT_1:126 .= hB " (Sphere ((0. (TOP-REAL n)),1)) by A6, A8, A10, TOPS_2:55 .= Fr B by A2, A6, A7, A9, FUNCT_1:94, TOPS_1:35 ; ::_thesis: verum end; theorem Th8: :: BROUWER2:8 for n being Nat for A being convex Subset of (TOP-REAL n) st A is compact & not A is boundary holds for h being continuous Function of ((TOP-REAL n) | A),((TOP-REAL n) | A) holds h is with_fixpoint proof let n be Nat; ::_thesis: for A being convex Subset of (TOP-REAL n) st A is compact & not A is boundary holds for h being continuous Function of ((TOP-REAL n) | A),((TOP-REAL n) | A) holds h is with_fixpoint set T = TOP-REAL n; consider I being affinely-independent Subset of (TOP-REAL n) such that {} (TOP-REAL n) c= I and I c= [#] (TOP-REAL n) and A1: Affin I = Affin ([#] (TOP-REAL n)) by RLAFFIN1:60; reconsider TT = TOP-REAL n as non empty RLSStruct ; reconsider i = I as Subset of TT ; set II = Int i; A2: not I is empty by A1; then A3: not Int i is empty by RLAFFIN2:20; reconsider ii = Int i as Subset of (TOP-REAL n) ; A4: Int ii c= Int (conv I) by RLAFFIN2:5, TOPS_1:19; let A be convex Subset of (TOP-REAL n); ::_thesis: ( A is compact & not A is boundary implies for h being continuous Function of ((TOP-REAL n) | A),((TOP-REAL n) | A) holds h is with_fixpoint ) assume A5: ( A is compact & not A is boundary ) ; ::_thesis: for h being continuous Function of ((TOP-REAL n) | A),((TOP-REAL n) | A) holds h is with_fixpoint A6: not A is empty by A5; let h be continuous Function of ((TOP-REAL n) | A),((TOP-REAL n) | A); ::_thesis: h is with_fixpoint [#] (TOP-REAL n) is Affine by RUSUB_4:22; then ( dim (TOP-REAL n) = n & Affin ([#] (TOP-REAL n)) = [#] (TOP-REAL n) ) by RLAFFIN1:50, RLAFFIN3:4; then A7: card I = n + 1 by A1, RLAFFIN3:6; then ii is open by RLAFFIN3:33; then not conv I is boundary by A3, A4, TOPS_1:23; then consider f being Function of ((TOP-REAL n) | A),((TOP-REAL n) | (conv I)) such that A8: f is being_homeomorphism and f .: (Fr A) = Fr (conv I) by A5, Th7; reconsider fhf = f * (h * (f ")) as Function of ((TOP-REAL n) | (conv I)),((TOP-REAL n) | (conv I)) by A6; f " is continuous by A8, TOPS_2:def_5; then consider p being Point of (TOP-REAL n) such that A9: p in dom fhf and A10: fhf . p = p by A7, A2, A8, A6, SIMPLEX2:23; A11: p in dom (h * (f ")) by A9, FUNCT_1:11; reconsider F = f as Function ; A12: rng f = [#] ((TOP-REAL n) | (conv I)) by A8, TOPS_2:def_5; A13: f " = F " by A8, TOPS_2:def_4; consider x being set such that A14: x in dom F and A15: F . x = p by A12, A9, FUNCT_1:def_3; (F ") . p = x by A8, A14, A15, FUNCT_1:34; then (h * (f ")) . p = h . x by A11, A13, FUNCT_1:12; then A16: p = f . (h . x) by A9, A10, FUNCT_1:12; A17: dom f = [#] ((TOP-REAL n) | A) by A8, TOPS_2:def_5; then A18: x in dom h by A14, FUNCT_2:52; then h . x in rng h by FUNCT_1:def_3; then h . x = x by A8, A17, A14, A15, A16, FUNCT_1:def_4; then x is_a_fixpoint_of h by A18, ABIAN:def_3; hence h is with_fixpoint by ABIAN:def_5; ::_thesis: verum end; Lm5: for n being Nat holds not cl_Ball ((0. (TOP-REAL n)),1) is boundary proof let n be Nat; ::_thesis: not cl_Ball ((0. (TOP-REAL n)),1) is boundary set TR = TOP-REAL n; reconsider tr = TOP-REAL n as TopStruct ; reconsider cB = cl_Ball ((0. (TOP-REAL n)),1) as Subset of tr ; n in NAT by ORDINAL1:def_12; then Ball ((0. (TOP-REAL n)),1) c= Int cB by TOPREAL9:16, TOPS_1:24; hence not cl_Ball ((0. (TOP-REAL n)),1) is boundary ; ::_thesis: verum end; Lm6: for n being Element of NAT for X being non empty SubSpace of Tdisk ((0. (TOP-REAL n)),1) st X = Tcircle ((0. (TOP-REAL n)),1) holds not X is_a_retract_of Tdisk ((0. (TOP-REAL n)),1) proof let n be Element of NAT ; ::_thesis: for X being non empty SubSpace of Tdisk ((0. (TOP-REAL n)),1) st X = Tcircle ((0. (TOP-REAL n)),1) holds not X is_a_retract_of Tdisk ((0. (TOP-REAL n)),1) set TR = TOP-REAL n; set Td = Tdisk ((0. (TOP-REAL n)),1); A1: Sphere ((0. (TOP-REAL n)),1) c= cl_Ball ((0. (TOP-REAL n)),1) by TOPREAL9:17; set M = mlt ((- 1),(TOP-REAL n)); let X be non empty SubSpace of Tdisk ((0. (TOP-REAL n)),1); ::_thesis: ( X = Tcircle ((0. (TOP-REAL n)),1) implies not X is_a_retract_of Tdisk ((0. (TOP-REAL n)),1) ) assume A2: X = Tcircle ((0. (TOP-REAL n)),1) ; ::_thesis: not X is_a_retract_of Tdisk ((0. (TOP-REAL n)),1) A3: the carrier of X = Sphere ((0. (TOP-REAL n)),1) by A2, TOPREALB:9; assume X is_a_retract_of Tdisk ((0. (TOP-REAL n)),1) ; ::_thesis: contradiction then consider F being continuous Function of (Tdisk ((0. (TOP-REAL n)),1)),X such that A4: F is being_a_retraction by BORSUK_1:def_17; A5: the carrier of (Tdisk ((0. (TOP-REAL n)),1)) = cl_Ball ((0. (TOP-REAL n)),1) by BROUWER:3; then reconsider f = F as Function of (Tdisk ((0. (TOP-REAL n)),1)),(Tdisk ((0. (TOP-REAL n)),1)) by A3, A1, FUNCT_2:7; set Mf = ((mlt ((- 1),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) * f; A6: (mlt ((- 1),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1)) = (mlt ((- 1),(TOP-REAL n))) | the carrier of (Tdisk ((0. (TOP-REAL n)),1)) by TMAP_1:def_4; A7: rng (((mlt ((- 1),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) * f) c= Sphere ((0. (TOP-REAL n)),1) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (((mlt ((- 1),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) * f) or y in Sphere ((0. (TOP-REAL n)),1) ) assume y in rng (((mlt ((- 1),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) * f) ; ::_thesis: y in Sphere ((0. (TOP-REAL n)),1) then consider x being set such that A8: x in dom (((mlt ((- 1),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) * f) and A9: (((mlt ((- 1),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) * f) . x = y by FUNCT_1:def_3; A10: f . x in dom ((mlt ((- 1),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) by A8, FUNCT_1:11; then f . x in dom (mlt ((- 1),(TOP-REAL n))) by A6, RELAT_1:57; then reconsider fx = f . x as Point of (TOP-REAL n) ; x in dom f by A8, FUNCT_1:11; then f . x in rng F by FUNCT_1:def_3; then A11: 1 = |.fx.| by A3, TOPREAL9:12 .= |.(- fx).| by EUCLID:10 .= |.((- fx) - (0. (TOP-REAL n))).| by RLVECT_1:13 ; y = ((mlt ((- 1),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) . (f . x) by A8, A9, FUNCT_1:12; then y = (mlt ((- 1),(TOP-REAL n))) . (f . x) by A6, A10, FUNCT_1:47; then y = (- 1) * fx by RLTOPSP1:def_13 .= - fx by RLVECT_1:16 ; hence y in Sphere ((0. (TOP-REAL n)),1) by A11; ::_thesis: verum end; then rng (((mlt ((- 1),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) * f) c= cl_Ball ((0. (TOP-REAL n)),1) by A1, XBOOLE_1:1; then reconsider MF = ((mlt ((- 1),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) * f as Function of (Tdisk ((0. (TOP-REAL n)),1)),(Tdisk ((0. (TOP-REAL n)),1)) by A5, FUNCT_2:6; A12: not cl_Ball ((0. (TOP-REAL n)),1) is boundary by Lm5; f is continuous by PRE_TOPC:26; then MF is continuous by PRE_TOPC:27; then MF is with_fixpoint by A12, Th8; then consider p being set such that A13: p is_a_fixpoint_of MF by ABIAN:def_5; A14: p in dom MF by A13, ABIAN:def_3; A15: p = MF . p by A13, ABIAN:def_3; then A16: p in rng MF by A14, FUNCT_1:def_3; then reconsider p = p as Point of (TOP-REAL n) by A7; A17: f . p = p by A4, A3, A7, A16, BORSUK_1:def_16; then A18: p in dom ((mlt ((- 1),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) by A14, FUNCT_1:11; p = ((mlt ((- 1),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) . p by A14, A15, A17, FUNCT_1:12; then p = (mlt ((- 1),(TOP-REAL n))) . p by A6, A18, FUNCT_1:47; then p = (- 1) * p by RLTOPSP1:def_13 .= - p by RLVECT_1:16 ; then A19: p = 0. (TOP-REAL n) by RLVECT_1:19; |.p.| = 1 by A7, A16, TOPREAL9:12; hence contradiction by A19, TOPRNS_1:23; ::_thesis: verum end; theorem :: BROUWER2:9 for n being Nat for A being non empty convex Subset of (TOP-REAL n) st A is compact & not A is boundary holds for FR being non empty SubSpace of (TOP-REAL n) | A st [#] FR = Fr A holds not FR is_a_retract_of (TOP-REAL n) | A proof let n be Nat; ::_thesis: for A being non empty convex Subset of (TOP-REAL n) st A is compact & not A is boundary holds for FR being non empty SubSpace of (TOP-REAL n) | A st [#] FR = Fr A holds not FR is_a_retract_of (TOP-REAL n) | A set T = TOP-REAL n; A1: n in NAT by ORDINAL1:def_12; set cB = cl_Ball ((0. (TOP-REAL n)),1); set S = Sphere ((0. (TOP-REAL n)),1); A2: [#] ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) = cl_Ball ((0. (TOP-REAL n)),1) by PRE_TOPC:def_5; then reconsider s = Sphere ((0. (TOP-REAL n)),1) as Subset of ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) by A1, TOPREAL9:17; A3: (TOP-REAL n) | (Sphere ((0. (TOP-REAL n)),1)) = ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) | s by A1, PRE_TOPC:7, TOPREAL9:17; let A be non empty convex Subset of (TOP-REAL n); ::_thesis: ( A is compact & not A is boundary implies for FR being non empty SubSpace of (TOP-REAL n) | A st [#] FR = Fr A holds not FR is_a_retract_of (TOP-REAL n) | A ) assume A4: ( A is compact & not A is boundary ) ; ::_thesis: for FR being non empty SubSpace of (TOP-REAL n) | A st [#] FR = Fr A holds not FR is_a_retract_of (TOP-REAL n) | A A5: ( [#] ((TOP-REAL n) | A) = A & Fr A c= A ) by A4, PRE_TOPC:def_5, TOPS_1:35; let FR be non empty SubSpace of (TOP-REAL n) | A; ::_thesis: ( [#] FR = Fr A implies not FR is_a_retract_of (TOP-REAL n) | A ) assume A6: [#] FR = Fr A ; ::_thesis: not FR is_a_retract_of (TOP-REAL n) | A n > 0 proof assume n <= 0 ; ::_thesis: contradiction then n = 0 ; then {(0. (TOP-REAL n))} = the carrier of (TOP-REAL n) by EUCLID:22, EUCLID:77; then A7: A = [#] (TOP-REAL n) by ZFMISC_1:33; then Fr A = (Cl A) \ A by TOPS_1:42; hence contradiction by A6, A7, XBOOLE_1:37; ::_thesis: verum end; then reconsider Ts = ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) | s as non empty SubSpace of (TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1)) ; assume FR is_a_retract_of (TOP-REAL n) | A ; ::_thesis: contradiction then consider F being continuous Function of ((TOP-REAL n) | A),FR such that A8: F is being_a_retraction by BORSUK_1:def_17; reconsider f = F as Function of ((TOP-REAL n) | A),((TOP-REAL n) | A) by A6, A5, FUNCT_2:7; A9: f is continuous by PRE_TOPC:26; A10: rng F c= Fr A by A6; reconsider N = n as Element of NAT by ORDINAL1:def_12; set TN = TOP-REAL N; A11: [#] ((TOP-REAL n) | (Sphere ((0. (TOP-REAL n)),1))) = Sphere ((0. (TOP-REAL n)),1) by PRE_TOPC:def_5; ( (TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1)) = Tdisk ((0. (TOP-REAL N)),1) & (TOP-REAL n) | (Sphere ((0. (TOP-REAL n)),1)) = Tcircle ((0. (TOP-REAL N)),1) ) by TOPREALB:def_6; then A12: not Ts is_a_retract_of (TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1)) by A3, Lm6; not cl_Ball ((0. (TOP-REAL n)),1) is boundary by Lm5; then consider h being Function of ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))),((TOP-REAL n) | A) such that A13: h is being_homeomorphism and A14: h .: (Fr (cl_Ball ((0. (TOP-REAL n)),1))) = Fr A by A1, A4, Th7; A15: dom h = [#] ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) by A13, TOPS_2:def_5; rng ((h ") * f) = ((h ") * f) .: (dom ((h ") * f)) by RELAT_1:113; then A16: rng ((h ") * f) c= ((h ") * f) .: (dom f) by RELAT_1:25, RELAT_1:123; reconsider H = h as Function ; A17: Fr (cl_Ball ((0. (TOP-REAL n)),1)) = Sphere ((0. (TOP-REAL n)),1) by Th5; rng h = [#] ((TOP-REAL n) | A) by A13, TOPS_2:def_5; then A18: (h ") .: (Fr A) = h " (Fr A) by A13, A5, TOPS_2:55 .= Fr (cl_Ball ((0. (TOP-REAL n)),1)) by A13, A14, A2, A15, FUNCT_1:94, TOPS_1:35 ; ((h ") * f) .: (dom f) = (h ") .: (f .: (dom f)) by RELAT_1:126 .= (h ") .: (rng f) by RELAT_1:113 ; then ((h ") * f) .: (dom f) c= Fr (cl_Ball ((0. (TOP-REAL n)),1)) by A18, A10, RELAT_1:123; then ( rng (((h ") * f) * h) c= rng ((h ") * f) & rng ((h ") * f) c= Fr (cl_Ball ((0. (TOP-REAL n)),1)) ) by A16, RELAT_1:26, XBOOLE_1:1; then rng (((h ") * f) * h) c= Fr (cl_Ball ((0. (TOP-REAL n)),1)) by XBOOLE_1:1; then reconsider hfh = ((h ") * f) * h as Function of ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))),Ts by A3, A17, A11, FUNCT_2:6; h " is continuous by A13, TOPS_2:def_5; then hfh is continuous by A13, A9, PRE_TOPC:27; then not hfh is being_a_retraction by A12, BORSUK_1:def_17; then consider x being Point of ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) such that A19: x in Sphere ((0. (TOP-REAL n)),1) and A20: hfh . x <> x by A3, A11, BORSUK_1:def_16; set hx = h . x; A21: dom hfh = the carrier of ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) by FUNCT_2:def_1; then A22: hfh . x = ((h ") * f) . (h . x) by FUNCT_1:12; x in dom h by A21, FUNCT_1:11; then A23: h . x in the carrier of FR by A6, A14, A17, A19, FUNCT_1:def_6; h . x in dom ((h ") * f) by A21, FUNCT_1:11; then A24: ((h ") * f) . (h . x) = (h ") . (f . (h . x)) by FUNCT_1:12; A25: H " = h " by A13, TOPS_2:def_4; (H ") . (h . x) = x by A13, A15, FUNCT_1:34; hence contradiction by A8, A25, A20, A22, A24, A23, BORSUK_1:def_16; ::_thesis: verum end;