brouwer2.miz



    begin

    reserve n for Nat,

p,q,u,w for Point of ( TOP-REAL n),

S for Subset of ( TOP-REAL n),

A,B for convex Subset of ( TOP-REAL n),

r for Real;

    

     Lm1: ((((1 - r) * p) + (r * q)) - p) = (r * (q - p))

    proof

      

      thus ((((1 - r) * p) + (r * q)) - p) = ((r * q) + (((1 - r) * p) - p)) by RLVECT_1:def 3

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

      .= ((r * q) + ((p - (r * p)) - p)) by RLVECT_1:def 8

      .= ((r * q) + ((p + ( - (r * p))) + ( - p)))

      .= ((r * q) + ((p + ( - p)) + ( - (r * p)))) by RLVECT_1:def 3

      .= ((r * q) + ((p - p) - (r * p)))

      .= ((r * q) + (( 0. ( TOP-REAL n)) - (r * p))) by RLVECT_1: 15

      .= ((r * q) - (r * p))

      .= (r * (q - p)) by RLVECT_1: 34;

    end;

    

     Lm2: r >= 0 implies (r * p) in ( halfline (( 0. ( TOP-REAL n)),p))

    proof

      assume

       A1: r >= 0 ;

      ((1 - r) * ( 0. ( TOP-REAL n))) = ( 0. ( TOP-REAL n)) & (( 0. ( TOP-REAL n)) + (r * p)) = (r * p);

      hence thesis by A1;

    end;

    theorem :: BROUWER2:1

    

     Th1: (((1 - r) * p) + (r * q)) = (p + (r * (q - p)))

    proof

      

      thus (p + (r * (q - p))) = (((((1 - r) * p) + (r * q)) - p) + p) by Lm1

      .= ((((1 - r) * p) + (r * q)) - (p - p)) by RLVECT_1: 29

      .= ((((1 - r) * p) + (r * q)) - ( 0. ( TOP-REAL n))) by RLVECT_1: 15

      .= (((1 - r) * p) + (r * q));

    end;

    theorem :: BROUWER2:2

    

     Th2: u in ( halfline (p,q)) & w in ( halfline (p,q)) & |.(u - p).| = |.(w - p).| implies u = w

    proof

      set r1 = u, r2 = w;

      assume that

       A1: r1 in ( halfline (p,q)) and

       A2: r2 in ( halfline (p,q)) and

       A3: |.(r1 - p).| = |.(r2 - p).|;

      per cases ;

        suppose p <> q;

        then

         A4: |.(q - p).| <> 0 by TOPRNS_1: 28;

        consider a1 be Real such that

         A5: r1 = (((1 - a1) * p) + (a1 * q)) and

         A6: a1 >= 0 by A1;

        

         A7: |.a1.| = a1 by A6, ABSVALUE:def 1;

        a1 in REAL & (r1 - p) = (a1 * (q - p)) by A5, Lm1, XREAL_0:def 1;

        then

         A8: |.(r1 - p).| = ( |.a1.| * |.(q - p).|) by TOPRNS_1: 7;

        consider a2 be Real such that

         A9: r2 = (((1 - a2) * p) + (a2 * q)) and

         A10: a2 >= 0 by A2;

        a2 in REAL & (r2 - p) = (a2 * (q - p)) by A9, Lm1, XREAL_0:def 1;

        then

         A11: |.(r2 - p).| = ( |.a2.| * |.(q - p).|) by TOPRNS_1: 7;

         |.a2.| = a2 by A10, ABSVALUE:def 1;

        then a1 = a2 by A3, A4, A8, A11, A7, XCMPLX_1: 5;

        hence thesis by A5, A9;

      end;

        suppose

         A12: p = q;

        then r1 in {p} by A1, TOPREAL9: 29;

        then

         A13: r1 = p by TARSKI:def 1;

        r2 in {p} by A2, A12, TOPREAL9: 29;

        hence thesis by A13, TARSKI:def 1;

      end;

    end;

    

     Lm3: for A be Subset of ( TOP-REAL n) st p in A & p <> q & (A /\ ( halfline (p,q))) is bounded holds ex w be Point of ( Euclid n) st w in (( Fr A) /\ ( halfline (p,q))) & (for u,P be Point of ( Euclid n) st P = p & u in (A /\ ( halfline (p,q))) holds ( dist (P,u)) <= ( dist (P,w))) & for r st r > 0 holds ex u be Point of ( Euclid n) st u in (A /\ ( halfline (p,q))) & ( dist (w,u)) < r

    proof

      set TRn = ( TOP-REAL n);

      let A be Subset of TRn such that

       A1: p in A and

       A2: p <> q and

       A3: (A /\ ( halfline (p,q))) is bounded;

      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 /\ H) as bounded Subset of ( Euclid n) by A3, JORDAN2C: 11;

      

       A5: ( dist (Q,P)) = |.(q - p).| by SPPOL_1: 39;

      p in H by TOPREAL9: 27;

      then

       A6: p in AH by A1, XBOOLE_0:def 4;

      set DAH = ( diameter AH);

      set X = { r where r be Real : (((1 - r) * p) + (r * q)) in AH & 0 <= r };

      set dAH = (DAH + 1);

       A7:

      now

        let x be object;

        assume x in X;

        then ex r be Real st x = r & (((1 - r) * p) + (r * q)) in AH & 0 <= r;

        hence x is real;

      end;

      (1 * p) = p & ( 0 * q) = ( 0. TRn) by RLVECT_1: 10, RLVECT_1:def 8;

      then p = (((1 - 0 ) * p) + ( 0 * q));

      then

       A8: 0 in X by A6;

      then

      reconsider X as non empty real-membered set by A7, MEMBERED:def 3;

      

       A9: (DAH + 0 ) < dAH by XREAL_1: 8;

      now

        let x be ExtReal;

        assume x in X;

        then

        consider r be Real such that

         A10: x = r and

         A11: (((1 - r) * p) + (r * q)) in AH and

         A12: 0 <= r;

        reconsider PQ = (((1 - r) * p) + (r * q)) as Element of ( Euclid n) by A11;

        ((((1 - r) * p) + (r * q)) - p) = (r * (q - p)) by Lm1;

        

        then ( dist (PQ,P)) = |.(r * (q - p)).| by SPPOL_1: 39

        .= ( |.r.| * |.(q - p).|) by TOPRNS_1: 7

        .= (r * ( dist (Q,P))) by A5, A12, ABSVALUE:def 1;

        then (r * ( dist (Q,P))) <= DAH by A6, A11, TBSP_1:def 8;

        then

         A13: (r * ( dist (Q,P))) <= dAH by A9, 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 <= (dAH / ( dist (Q,P))) by A10, A13, XREAL_1: 72;

      end;

      then (dAH / ( 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 Element of REAL by XXREAL_2: 16;

      

       A14: 0 <= S by A8, XXREAL_2: 4;

      set Spq = (((1 - S) * p) + (S * q));

      reconsider spq = Spq as Element of ( Euclid n) by EUCLID: 67;

      

       A15: for r be Real st r > 0 holds ex w be Point of ( Euclid n) st w in AH & ( dist (spq,w)) < r

      proof

        let r be Real such that

         A16: r > 0 ;

        set r2 = (r / |.(q - p).|);

        assume

         A17: for w be Point of ( Euclid n) st w in AH holds ( dist (spq,w)) >= r;

        now

          let x be ExtReal;

          assume

           A18: x in X;

          then

          consider w be Real such that

           A19: x = w and

           A20: (((1 - w) * p) + (w * q)) in AH and 0 <= w;

          (S - w) >= 0 by A18, A19, XREAL_1: 48, XXREAL_2: 4;

          then

           A21: |.(S - w).| = (S - w) by ABSVALUE:def 1;

          reconsider PQ = (((1 - w) * p) + (w * q)) as Element of ( Euclid n) by A20;

          

           A22: PQ = (p + (w * (q - p))) by Th1;

          (Spq - (p + (w * (q - p)))) = ((Spq - 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 A22, SPPOL_1: 39

          .= ((S - w) * |.(q - p).|) by A21, TOPRNS_1: 7;

          then ((S - w) * |.(q - p).|) >= r by A17, A20;

          then (S - w) >= r2 by A2, A5, METRIC_1: 7, XREAL_1: 79;

          hence (S - r2) >= x by A19, XREAL_1: 11;

        end;

        then (S - r2) is UpperBound of X by XXREAL_2:def 1;

        then (S - 0 ) <= (S - r2) by XXREAL_2:def 3;

        hence contradiction by A4, A5, A16, XREAL_1: 8;

      end;

      

       A23: the TopStruct of TRn = ( TopSpaceMetr ( Euclid n)) by EUCLID:def 8;

      now

        let U be Subset of TRn;

        reconsider UE = U as Subset of ( TopSpaceMetr ( Euclid n)) by A23;

        assume that

         A24: U is open and

         A25: Spq in U;

        UE in the topology of ( TopSpaceMetr ( Euclid n)) by A23, A24, PRE_TOPC:def 2;

        then UE is open by PRE_TOPC:def 2;

        then

        consider r be Real such that

         A26: r > 0 and

         A27: ( Ball (spq,r)) c= UE by A25, TOPMETR: 15;

        set r2 = (r / |.(q - p).|);

        set Sr = (S + (r2 / 2));

        consider w be Element of ( Euclid n) such that

         A28: w in AH & ( dist (spq,w)) < r by A15, A26;

        w in ( Ball (spq,r)) & w in A by A28, METRIC_1: 11, XBOOLE_0:def 4;

        hence A meets U by A27, XBOOLE_0: 3;

        

         A29: (r2 * |.(q - p).|) = (r * ( |.(q - p).| / |.(q - p).|))

        .= (r * 1) by A4, A5, XCMPLX_1: 60;

        Sr > (S + 0 ) by A4, A5, A26, XREAL_1: 6;

        then (S - Sr) < 0 by XREAL_1: 49;

        

        then

         A30: |.(S - Sr).| = ( - (S - Sr)) by ABSVALUE:def 1

        .= (r2 / 2);

        set Srpq = (((1 - Sr) * p) + (Sr * q));

        reconsider srpq = Srpq as Element of ( Euclid n) by EUCLID: 67;

        

         A31: srpq in H by A14, A26;

        

         A32: not srpq in A

        proof

          assume srpq in A;

          then srpq in AH by A31, XBOOLE_0:def 4;

          then Sr in X by A14, A26;

          then (S + (r2 / 2)) <= (S + 0 ) by XXREAL_2: 4;

          hence contradiction by A4, A5, A26, XREAL_1: 8;

        end;

        (Spq - Srpq) = (Spq - (p + (Sr * (q - p)))) by Th1

        .= ((Spq - p) - (Sr * (q - p))) by RLVECT_1: 27

        .= ((S * (q - p)) - (Sr * (q - p))) by Lm1

        .= ((S - Sr) * (q - p)) by RLVECT_1: 35;

        

        then ( dist (spq,srpq)) = |.((S - Sr) * (q - p)).| by SPPOL_1: 39

        .= ((r2 / 2) * |.(q - p).|) by A30, TOPRNS_1: 7

        .= (r / 2) by A29;

        then ( dist (spq,srpq)) < r by A26, XREAL_1: 216;

        then srpq in ( Ball (spq,r)) by METRIC_1: 11;

        hence (U \ A) <> {} by A27, A32, XBOOLE_0:def 5;

      end;

      then

       A33: Spq in ( Fr A) by TOPGEN_1: 9;

      take spq;

      

       A34: (Spq - p) = (S * (q - p)) by Lm1;

      Spq in H by A14;

      hence spq in (( Fr A) /\ H) by A33, XBOOLE_0:def 4;

      

       A35: |.S.| = S by A14, ABSVALUE:def 1;

      hereby

        let u,P be Point of ( Euclid n) such that

         A36: P = p and

         A37: u in (A /\ H);

        

         A38: ( dist (P,spq)) = |.(S * (q - p)).| by A34, A36, SPPOL_1: 39

        .= (S * |.(q - p).|) by A35, TOPRNS_1: 7;

        u in H by A37, XBOOLE_0:def 4;

        then

        consider Ur be Real such that

         A39: u = (((1 - Ur) * p) + (Ur * q)) and

         A40: 0 <= Ur;

        

         A41: |.Ur.| = Ur by A40, ABSVALUE:def 1;

        Ur in X by A37, A39, A40;

        then

         A42: Ur <= S by XXREAL_2: 4;

        set du = ( dist (P,u)), ds = ( dist (P,spq));

        

         A43: ((((1 - Ur) * p) + (Ur * q)) - p) = (Ur * (q - p)) by Lm1;

        ( dist (P,u)) = |.(Ur * (q - p)).| by A36, A39, A43, SPPOL_1: 39

        .= (Ur * |.(q - p).|) by A41, TOPRNS_1: 7;

        hence du <= ds by A38, A42, XREAL_1: 64;

      end;

      thus thesis by A15;

    end;

    theorem :: BROUWER2:3

    for S st p in S & p <> q & (S /\ ( halfline (p,q))) is bounded holds ex w st w in (( Fr S) /\ ( halfline (p,q))) & (for u st u in (S /\ ( halfline (p,q))) holds |.(p - u).| <= |.(p - w).|) & for r st r > 0 holds ex u st u in (S /\ ( halfline (p,q))) & |.(w - u).| < r

    proof

      set T = ( TOP-REAL n), E = ( Euclid n);

      let A be Subset of T such that

       A1: p in A & p <> q & (A /\ ( halfline (p,q))) is bounded;

      consider W be Point of E such that

       A2: W in (( Fr A) /\ ( halfline (p,q))) and

       A3: for u,P be Point of E st P = p & u in (A /\ ( halfline (p,q))) holds ( dist (P,u)) <= ( dist (P,W)) and

       A4: for r st r > 0 holds ex u be Point of E st u in (A /\ ( halfline (p,q))) & ( dist (W,u)) < r by A1, Lm3;

      reconsider w = W as Point of T by EUCLID: 67;

      take w;

      thus w in (( Fr A) /\ ( halfline (p,q))) by A2;

      reconsider P = p as Point of E by EUCLID: 67;

      hereby

        let u be Point of T such that

         A5: u in (A /\ ( halfline (p,q)));

        reconsider U = u as Point of E by EUCLID: 67;

        

         A6: ( dist (P,U)) = |.(p - u).| by SPPOL_1: 39;

        ( dist (P,U)) <= ( dist (P,W)) by A3, A5;

        hence |.(p - u).| <= |.(p - w).| by A6, SPPOL_1: 39;

      end;

      let r be Real;

      assume r > 0 ;

      then

      consider U be Point of E such that

       A7: U in (A /\ ( halfline (p,q))) & ( dist (W,U)) < r by A4;

      reconsider u = U as Point of T by EUCLID: 67;

      ( dist (W,U)) = |.(w - u).| by SPPOL_1: 39;

      hence thesis by A7;

    end;

    theorem :: BROUWER2:4

    

     Th4: for A st A is closed & p in ( Int A) & p <> q & (A /\ ( halfline (p,q))) is bounded holds ex u st (( Fr A) /\ ( halfline (p,q))) = {u}

    proof

      set TRn = ( TOP-REAL n);

      set En = ( Euclid n);

      let A be convex Subset of ( TOP-REAL n) such that

       A1: A is closed and

       A2: p in ( Int A) and

       A3: p <> q and

       A4: (A /\ ( halfline (p,q))) is bounded;

      reconsider P = p, Q = q as Point of En by EUCLID: 67;

      

       A5: the TopStruct of TRn = ( TopSpaceMetr ( Euclid n)) by EUCLID:def 8;

      then

      reconsider I = ( Int A) as Subset of ( TopSpaceMetr En);

      ( Int A) in the topology of ( TopSpaceMetr En) by A5, PRE_TOPC:def 2;

      then I is open by PRE_TOPC:def 2;

      then

      consider r be Real such that

       A6: r > 0 and

       A7: ( Ball (P,r)) c= I by A2, TOPMETR: 15;

      ( dist (P,P)) < r by A6, METRIC_1: 1;

      then

       A8: P in ( Ball (P,r)) by METRIC_1: 11;

      set H = ( halfline (p,q));

      reconsider AH = (A /\ H) as bounded Subset of En by A4, JORDAN2C: 11;

      

       A9: ( Int A) c= A by TOPS_1: 16;

      then

      consider W be Point of En such that

       A10: W in (( Fr A) /\ H) and

       A11: for u,P be Point of ( Euclid n) st P = p & u in AH holds ( dist (P,u)) <= ( dist (P,W)) and for r be Real st r > 0 holds ex u be Point of En st u in AH & ( dist (W,u)) < r by A2, A3, A4, Lm3;

      reconsider w = W as Point of TRn by EUCLID: 67;

      

       A12: W in ( Fr A) by A10, XBOOLE_0:def 4;

      W in H by A10, XBOOLE_0:def 4;

      then

      consider Wr be Real such that

       A13: W = (((1 - Wr) * p) + (Wr * q)) and

       A14: Wr >= 0 ;

      

       A15: ( Fr A) c= A by A1, TOPS_1: 35;

      

       A16: ( Fr A) misses ( Ball (P,r)) by A7, TOPS_1: 39, XBOOLE_1: 63;

      (( Fr A) /\ H) = {W}

      proof

        assume (( Fr A) /\ H) <> {W};

        then

        consider u be object such that

         A17: u in (( Fr A) /\ H) and

         A18: u <> W by A10, ZFMISC_1: 35;

        reconsider u as Point of TRn by A17;

        

         A19: u in H by A17, XBOOLE_0:def 4;

        then

        consider Ur be Real such that

         A20: u = (((1 - Ur) * p) + (Ur * q)) and

         A21: Ur >= 0 ;

        

         A22: |.Ur.| = Ur by A21, ABSVALUE:def 1;

        reconsider U = u as Element of En by EUCLID: 67;

        ((((1 - Ur) * p) + (Ur * q)) - p) = (Ur * (q - p)) by Lm1;

        

        then

         A23: ( dist (U,P)) = |.(Ur * (q - p)).| by A20, SPPOL_1: 39

        .= (Ur * |.(q - p).|) by A22, TOPRNS_1: 7;

        set R = ((r * (Wr - Ur)) / Wr);

        reconsider b = ( Ball (U,R)) as Subset of ( TopSpaceMetr En) by A5, EUCLID: 67;

        set x = ((Wr - Ur) / Wr);

        b is open by TOPMETR: 14;

        then b in the topology of TRn by A5, PRE_TOPC:def 2;

        then

        reconsider B = b as open Subset of TRn by PRE_TOPC:def 2;

        

         A24: |.Wr.| = Wr by A14, ABSVALUE:def 1;

        ((((1 - Wr) * p) + (Wr * q)) - p) = (Wr * (q - p)) by Lm1;

        

        then

         A25: ( dist (W,P)) = |.(Wr * (q - p)).| by A13, SPPOL_1: 39

        .= (Wr * |.(q - p).|) by A24, TOPRNS_1: 7;

        

         A26: u in ( Fr A) by A17, XBOOLE_0:def 4;

        then

         A27: u in AH by A15, A19, XBOOLE_0:def 4;

        P <> W by A16, A8, A12, XBOOLE_0: 3;

        then

         A28: Wr > 0 by A25, METRIC_1: 7;

        

        then

         A29: (1 - x) = ((Wr / Wr) - x) by XCMPLX_1: 60

        .= (Ur / Wr);

        P <> u by A16, A8, A26, XBOOLE_0: 3;

        then Ur > 0 by A23, METRIC_1: 7;

        then (1 - x) >= (x - x) by A28, A29;

        then

         A30: x in REAL & x <= 1 by XREAL_0:def 1, XREAL_1: 6;

        

         A31: (((1 - Wr) * p) + (Wr * q)) = ((Wr * (q - p)) + p) by Th1;

        

         A32: (((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 A31, RLVECT_1: 27

        .= (((Wr * (q - p)) + (p - p)) - (Ur * (q - p))) by RLVECT_1:def 3

        .= (((Wr * (q - p)) + ( 0. TRn)) - (Ur * (q - p))) by RLVECT_1: 5

        .= ((Wr * (q - p)) - (Ur * (q - p)))

        .= ((Wr - Ur) * (q - p)) by RLVECT_1: 35;

        

        then

         A33: ( dist (U,W)) = |.((Wr - Ur) * (q - p)).| by A13, A20, SPPOL_1: 39

        .= ( |.(Wr - Ur).| * |.(q - p).|) by TOPRNS_1: 7;

        ( dist (U,W)) > 0 by A18, METRIC_1: 7;

        then |.(q - p).| > 0 by A33, XREAL_1: 134;

        then Ur <= Wr by A11, A23, A25, A27, XREAL_1: 68;

        then (Wr - Ur) >= 0 by XREAL_1: 48;

        then

         A34: |.(Wr - Ur).| = (Wr - Ur) by ABSVALUE:def 1;

        then

         A35: (Wr - Ur) > 0 by A18, A33, METRIC_1: 7;

        ( dist (U,U)) = 0 by METRIC_1: 1;

        then U in B by A6, A28, A35, METRIC_1: 11;

        then (B \ A) <> {} by A26, TOPGEN_1: 9;

        then

        consider t be object such that

         A36: t in (B \ A) by XBOOLE_0:def 1;

        

         A37: t in B by A36, XBOOLE_0:def 5;

        reconsider t as Point of TRn by A36;

        set z = (p + ((Wr / (Wr - Ur)) * (t - u)));

        reconsider Z = z as Point of En by EUCLID: 67;

        reconsider T = t as Point of En by EUCLID: 67;

        

         A38: ( dist (U,T)) = |.(u - t).| by SPPOL_1: 39;

        

         A39: ((Wr / (Wr - Ur)) * R) = ((((Wr / Wr) * (Wr - Ur)) / (Wr - Ur)) * r)

        .= (((Wr - Ur) / (Wr - Ur)) * r) by A28, XCMPLX_1: 88

        .= r by A35, XCMPLX_1: 88;

         |.( - Wr).| = ( - ( - Wr)) by A28, ABSVALUE:def 1;

        then

         A40: (( - Wr) / (Wr - Ur)) in REAL & |.(( - Wr) / (Wr - Ur)).| = (Wr / (Wr - Ur)) by A34, COMPLEX1: 67, XREAL_0:def 1;

        

         A41: ((Ur / Wr) * (Wr * (q - p))) = (((Ur / Wr) * Wr) * (q - p)) by RLVECT_1:def 7

        .= (((Wr / Wr) * Ur) * (q - p))

        .= (Ur * (q - p)) by A28, XCMPLX_1: 88;

        (p - z) = ((p - p) - ((Wr / (Wr - Ur)) * (t - u))) by RLVECT_1: 27

        .= (( 0. TRn) - ((Wr / (Wr - Ur)) * (t - u))) by RLVECT_1: 15

        .= ( - ((Wr / (Wr - Ur)) * (t - u)))

        .= (( - 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

         A42: ( dist (P,Z)) = |.((( - Wr) / (Wr - Ur)) * (t - u)).| by SPPOL_1: 39

        .= ((Wr / (Wr - Ur)) * |.(t - u).|) by A40, TOPRNS_1: 7;

        ( dist (U,T)) < R by A37, METRIC_1: 11;

        then ((Wr / (Wr - Ur)) * |.(u - t).|) < r by A28, A35, A38, A39, XREAL_1: 68;

        then ( dist (P,Z)) < r by A38, A42, SPPOL_1: 39;

        then Z in ( Ball (P,r)) by METRIC_1: 11;

        then

         A43: Z in I by A7;

        (x * ((Wr / (Wr - Ur)) * (t - u))) = ((x * (Wr / (Wr - Ur))) * (t - u)) by RLVECT_1:def 7

        .= (((((Wr - Ur) / (Wr - Ur)) * Wr) / Wr) * (t - u))

        .= ((Wr / Wr) * (t - u)) by A35, XCMPLX_1: 88

        .= (1 * (t - u)) by A28, XCMPLX_1: 60

        .= (t - u) by RLVECT_1:def 8;

        then (x * z) = ((x * p) + (t - u)) by RLVECT_1:def 5;

        

        then ((x * z) + ((1 - x) * w)) = (((t - u) + (x * p)) + (((1 - x) * p) + (Ur * (q - p)))) by A13, A29, A31, A41, RLVECT_1:def 5

        .= ((((t - u) + (x * p)) + ((1 - x) * p)) + (Ur * (q - p))) by RLVECT_1:def 3

        .= (((t - u) + ((x * p) + ((1 - x) * p))) + (Ur * (q - p))) by RLVECT_1:def 3

        .= (((t - u) + ((x + (1 - x)) * p)) + (Ur * (q - p))) by RLVECT_1:def 6

        .= (((t - u) + p) + (Ur * (q - p))) by RLVECT_1:def 8

        .= ((t - u) + u) by A20, A32, RLVECT_1:def 3

        .= (t - (u - u)) by RLVECT_1: 29

        .= (t - ( 0. TRn)) by RLVECT_1: 15

        .= t;

        then t in A by A15, A9, A12, A28, A30, A35, A43, RLTOPSP1:def 1;

        hence contradiction by A36, XBOOLE_0:def 5;

      end;

      hence thesis by A10;

    end;

    

     Lm4: for n be Element of NAT st n > 0 holds for A be convex Subset of ( TOP-REAL n) st A is compact & ( 0* n) in ( Int A) holds ex h be 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 ;

      set TRn = ( TOP-REAL n), En = ( Euclid n), cTRn = the carrier of TRn;

      assume

       A1: n > 0 ;

      (cTRn \ {( 0. TRn)}) = ( {( 0. TRn)} ` ) by SUBSET_1:def 4;

      then

      reconsider cTR0 = (cTRn \ {( 0. TRn)}) as non empty open Subset of TRn by A1;

      set CL = ( cl_Ball (( 0. TRn),1)), S = ( Sphere (( 0. TRn),1));

      set TRn0 = (TRn | cTR0);

      set nN = (n NormF );

      set En = ( Euclid n);

      set I0 = (( 0. TRn) .--> ( 0. TRn));

      let A be convex Subset of TRn such that

       A2: A is compact and

       A3: ( 0* n) in ( Int A);

      

       A4: A is non empty by A3;

      reconsider 0TRn = ( 0. TRn) as Point of En by EUCLID: 67;

      

       A5: ( 0* n) = ( 0. TRn) by EUCLID: 70;

      then

      consider e be Real 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. TRn)}) = ( Fr A) by A5, ZFMISC_1: 57;

      set TM = ( TopSpaceMetr En);

      

       A10: ( [#] TRn0) = cTR0 by PRE_TOPC:def 5;

      

       A11: the TopStruct of TRn = TM by EUCLID:def 8;

      then

      reconsider a = A as Subset of TM;

      reconsider aa = a as Subset of En by EUCLID: 67;

      (TRn | A) is compact by A2;

      then (TM | a) is compact by A11, PRE_TOPC: 36;

      then

       A12: a is compact by A4, COMPTS_1: 3;

      

       A13: for p be Point of TRn st p <> ( 0. TRn) holds ex x be Point of TRn st (( Fr A) /\ ( halfline (( 0. TRn),p))) = {x}

      proof

        let p be Point of TRn such that

         A14: p <> ( 0. TRn);

        

         A15: (A /\ ( halfline (( 0. TRn),p))) c= aa by XBOOLE_1: 17;

        then

        reconsider F = (A /\ ( halfline (( 0. TRn),p))) as Subset of En by XBOOLE_1: 1;

        

         A16: ( 0. TRn) in ( Int A) by A3, EUCLID: 70;

        F is bounded by A12, A15, HAUSDORF: 18, TBSP_1: 14;

        then (A /\ ( halfline (( 0. TRn),p))) is bounded by JORDAN2C: 11;

        hence thesis by A2, A14, A16, Th4;

      end;

      ( Fr A) is non empty

      proof

        set q = the Element of cTR0;

        q <> ( 0. TRn) by ZFMISC_1: 56;

        then ex x be Point of TRn st (( Fr A) /\ ( halfline (( 0. TRn),q))) = {x} by A13;

        hence thesis;

      end;

      then

      reconsider FrA = ( Fr A) as non empty Subset of TRn0 by A10, A9, XBOOLE_1: 33;

      

       A17: ( Fr A) c= A by A2, TOPS_1: 35;

      set TS = (TRn | S);

      reconsider I = ( incl TRn0) as continuous Function of TRn0, TRn by TMAP_1: 87;

      

       A18: ( [#] TS) = S by PRE_TOPC:def 5;

      

       A19: (nN | TRn0) = (nN | the carrier of TRn0) by TMAP_1:def 4;

       not 0 in ( rng (nN | TRn0))

      proof

        assume 0 in ( rng (nN | TRn0));

        then

        consider x be object such that

         A20: x in ( dom (nN | TRn0)) and

         A21: ((nN | TRn0) . x) = 0 by FUNCT_1:def 3;

        x in ( dom nN) by A19, A20, RELAT_1: 57;

        then

        reconsider x as Element of TRn;

        reconsider X = x as Element of ( REAL n) by EUCLID: 22;

         0 = (nN . x) by A19, A20, A21, FUNCT_1: 47

        .= |.X.| by JGRAPH_4:def 1;

        then x = ( 0. TRn) by A5, EUCLID: 8;

        then x in {( 0. TRn)} by TARSKI:def 1;

        hence contradiction by A10, A20, XBOOLE_0:def 5;

      end;

      then

      reconsider nN0 = (nN | TRn0) as non-empty continuous Function of TRn0, R^1 by RELAT_1:def 9;

      reconsider b = (I </> nN0) as Function of TRn0, TRn by TOPREALC: 46;

      

       A22: ( dom b) = cTR0 by A10, FUNCT_2:def 1;

      

       A23: for p be Point of TRn st p in cTR0 holds (b . p) = ((1 / |.p.|) * p) & |.((1 / |.p.|) * p).| = 1

      proof

        let p be Point of TRn;

        assume

         A24: p in cTR0;

        then

         A25: (nN0 . p) = (nN . p) & (I . p) = p by A10, A19, FUNCT_1: 49, TMAP_1: 84;

        

        thus (b . p) = ((I . p) (/) (nN0 . p)) by A22, A24, VALUED_2: 72

        .= (p (/) |.p.|) by A25, JGRAPH_4:def 1

        .= ((1 / |.p.|) (#) p) by VALUED_2:def 32

        .= ((1 / |.p.|) * p);

        

         A26: |.(1 / |.p.|).| = (1 / |.p.|) & p <> ( 0. TRn) by A24, ABSVALUE:def 1, ZFMISC_1: 56;

        

        thus |.((1 / |.p.|) * p).| = ( |.(1 / |.p.|).| * |.p.|) by TOPRNS_1: 7

        .= 1 by A26, TOPRNS_1: 24, XCMPLX_1: 87;

      end;

      

       A27: ( rng b) c= S

      proof

        let y be object;

        assume y in ( rng b);

        then

        consider x be object such that

         A28: x in ( dom b) and

         A29: (b . x) = y by FUNCT_1:def 3;

        reconsider x as Point of TRn by A22, A28;

        

         A30: (((1 / |.x.|) * x) - ( 0. TRn)) = ((1 / |.x.|) * x) & |.((1 / |.x.|) * x).| = 1 by A10, A23, A28;

        y = ((1 / |.x.|) * x) by A10, A23, A28, A29;

        hence thesis by A30;

      end;

      then

      reconsider B = b as Function of TRn0, TS by A10, A18, A22, FUNCT_2: 2;

      

       A31: I0 = ( {( 0. TRn)} --> ( 0. TRn)) by FUNCOP_1:def 9;

      then

       A32: ( dom I0) = {( 0. TRn)};

      set FRA = (TRn0 | FrA), H = (b | FRA);

      

       A33: ( dom H) = the carrier of FRA by FUNCT_2:def 1;

      

       A34: H = (b | the carrier of FRA) by TMAP_1:def 4;

      then

       A35: ( rng H) c= ( rng b) by RELAT_1: 70;

      then

       A36: ( rng H) c= S by A27;

      reconsider H as Function of FRA, TS by A18, A27, A33, A35, FUNCT_2: 2, XBOOLE_1: 1;

      

       A37: ( [#] FRA) = FrA by PRE_TOPC:def 5;

      

       A38: (( Fr A) \ {( 0. TRn)}) c= cTR0 by XBOOLE_1: 33;

      S c= ( rng H)

      proof

        let x be object;

        assume x in S;

        then

        consider p be Point of TRn such that

         A39: x = p and

         A40: |.(p - ( 0. TRn)).| = 1;

        p <> ( 0. TRn) by A5, A40;

        then

        consider q be Point of TRn such that

         A41: (FrA /\ ( halfline (( 0. TRn),p))) = {q} by A13;

        

         A42: q in {q} by TARSKI:def 1;

        then

         A43: q in FrA by A41, XBOOLE_0:def 4;

        then

         A44: (b . q) = ((1 / |.q.|) * q) & (b . q) = (H . q) by A9, A23, A34, A37, A38, FUNCT_1: 49;

        q in ( halfline (( 0. TRn),p)) by A41, A42, XBOOLE_0:def 4;

        then ( halfline (( 0. TRn),p)) = ( halfline (( 0. TRn),q)) by A5, A8, A43, TOPREAL9: 31;

        then

         A45: ((1 / |.q.|) * q) in ( halfline (( 0. TRn),p)) by Lm2;

        

         A46: (((1 / |.q.|) * q) - ( 0. TRn)) = ((1 / |.q.|) * q) & p in ( halfline (( 0. TRn),p)) by TOPREAL9: 28;

        (H . q) in ( rng H) & |.((1 / |.q.|) * q).| = 1 by A9, A23, A33, A37, A38, A43, FUNCT_1:def 3;

        hence thesis by A39, A40, A45, A46, A44, Th2;

      end;

      then

       A47: S = ( rng H) by A36, XBOOLE_0:def 10;

      (( Fr A) \ {( 0. TRn)}) c= cTR0 by XBOOLE_1: 33;

      then

       A48: ( dom H) = ( [#] FRA) & (TRn | ( Fr A)) = FRA by A9, FUNCT_2:def 1, PRE_TOPC: 7;

      for x1,x2 be object st x1 in ( dom H) & x2 in ( dom H) & (H . x1) = (H . x2) holds x1 = x2

      proof

        let x1,x2 be object such that

         A49: x1 in ( dom H) and

         A50: x2 in ( dom H) and

         A51: (H . x1) = (H . x2);

        

         A52: x2 in ( dom b) by A34, A50, RELAT_1: 57;

        

         A53: x1 in ( dom b) by A34, A49, RELAT_1: 57;

        then

        reconsider p1 = x1, p2 = x2 as Point of TRn by A22, A52;

        

         A54: (b . p1) = ((1 / |.p1.|) * p1) by A10, A23, A53;

        x2 <> ( 0. TRn) by A10, A52, ZFMISC_1: 56;

        then

        consider q be Point of TRn such that

         A55: (( Fr A) /\ ( halfline (( 0. TRn),p2))) = {q} by A13;

        p2 in ( halfline (( 0. TRn),p2)) by TOPREAL9: 28;

        then p2 in {q} by A37, A50, A55, XBOOLE_0:def 4;

        then

         A56: p2 = q by TARSKI:def 1;

         |.((1 / |.p2.|) * p2).| = 1 by A10, A23, A52;

        then

         A57: ((1 / |.p2.|) * p2) <> ( 0. TRn) by TOPRNS_1: 23;

        

         A58: (( 0. TRn) + ((1 / |.p2.|) * p2)) = ((1 / |.p2.|) * p2);

        

         A59: (b . p2) = ((1 / |.p2.|) * p2) by A10, A23, A52;

        

         A60: (H . x1) = (b . x1) & (H . x2) = (b . x2) by A34, A49, A50, FUNCT_1: 47;

        ((1 - (1 / |.p1.|)) * ( 0. TRn)) = ( 0. TRn);

        then

         A61: ((1 / |.p1.|) * p1) in ( halfline (( 0. TRn),p1)) by A51, A54, A58, A59, A60;

        ((1 - (1 / |.p2.|)) * ( 0. TRn)) = ( 0. TRn);

        then ((1 / |.p2.|) * p2) in ( halfline (( 0. TRn),p2)) by A58;

        

        then ( halfline (( 0. TRn),p2)) = ( halfline (( 0. TRn),((1 / |.p1.|) * p1))) by A51, A54, A57, A59, A60, TOPREAL9: 31

        .= ( halfline (( 0. TRn),p1)) by A51, A54, A57, A59, A60, A61, TOPREAL9: 31;

        then p1 in ( halfline (( 0. TRn),p2)) by TOPREAL9: 28;

        then p1 in {q} by A37, A49, A55, XBOOLE_0:def 4;

        hence thesis by A56, TARSKI:def 1;

      end;

      then

       A62: H is one-to-one by FUNCT_1:def 4;

      then H is being_homeomorphism by A2, A18, A47, A48, COMPTS_1: 17, PRE_TOPC: 27;

      then

      reconsider H1 = (H " ) as continuous Function of TS, FRA by TOPS_2:def 5;

      reconsider HH = H as Function;

      set nN0F = (nN0 | FRA);

      reconsider H1B = (H1 * B) as Function of TRn0, FRA by A47;

      reconsider NH1B = (nN0F * H1B) as Function of TRn0, R^1 ;

      

       A63: nN0F = (nN0 | the carrier of FRA) by TMAP_1:def 4;

      then ( rng NH1B) c= ( rng nN0F) & ( rng nN0F) c= ( rng nN0) by RELAT_1: 26, RELAT_1: 70;

      then ( rng NH1B) c= ( rng nN0);

      then

       A64: not 0 in ( rng NH1B);

      (B is continuous) & S is non empty by A27, PRE_TOPC: 27;

      then

      reconsider NH1B as non-empty continuous Function of TRn0, R^1 by A64, RELAT_1:def 9;

      reconsider G = (I </> NH1B) as Function of TRn0, TRn by TOPREALC: 46;

      

       A65: ( dom G) = cTR0 by A10, FUNCT_2:def 1;

      

       A66: ( dom nN0F) = FrA by A37, FUNCT_2:def 1;

      

       A67: for p be Point of TRn st p in cTR0 holds ex Hp be Point of TRn st Hp = (H1B . p) & Hp in FrA & (G . p) = ((1 / |.Hp.|) * p) & |.Hp.| > 0

      proof

        let p be Point of TRn;

        assume

         A68: p in cTR0;

        then

         A69: p in ( dom NH1B) by A10, FUNCT_2:def 1;

        then

         A70: (H1B . p) in ( dom nN0F) by FUNCT_1: 11;

        then

        reconsider Hp = (H1B . p) as Point of TRn by A66;

        

         A71: (nN0F . Hp) = (nN0 . Hp) by A63, A70, FUNCT_1: 49;

        

         A72: (nN . Hp) = |.Hp.| & (nN0 . Hp) = (nN . Hp) by A19, A66, A70, FUNCT_1: 49, JGRAPH_4:def 1;

        take Hp;

        thus Hp = (H1B . p) & Hp in FrA by A37, A70;

        

         A73: (NH1B . p) = (nN0F . (H1B . p)) by A69, FUNCT_1: 12;

        

        thus (G . p) = ((I . p) (/) (NH1B . p)) by A65, A68, VALUED_2: 72

        .= (p (/) |.Hp.|) by A10, A68, A73, A71, A72, TMAP_1: 84

        .= ((1 / |.Hp.|) (#) p) by VALUED_2:def 32

        .= ((1 / |.Hp.|) * p);

         |.Hp.| <> 0 by A63, A69, A70, A73, A72, FUNCT_1: 49;

        hence thesis;

      end;

      

       A74: not ( 0. TRn) in ( rng G)

      proof

        assume ( 0. TRn) in ( rng G);

        then

        consider p be object such that

         A75: p in ( dom G) and

         A76: (G . p) = ( 0. TRn) by FUNCT_1:def 3;

        reconsider p as Point of TRn by A65, A75;

        consider Hp be Point of TRn such that Hp = (H1B . p) and Hp in FrA and

         A77: (G . p) = ((1 / |.Hp.|) * p) & |.Hp.| > 0 by A10, A67, A75;

        p <> ( 0. TRn) by A10, A75, ZFMISC_1: 56;

        hence contradiction by A76, A77, RLVECT_1: 11;

      end;

      

       A78: for x1,x2 be set st x1 in ( dom I0) & x2 in (( dom G) \ ( dom I0)) holds (I0 . x1) <> (G . x2)

      proof

        let x1,x2 be set such that

         A79: x1 in ( dom I0) and

         A80: x2 in (( dom G) \ ( dom I0));

        x1 = ( 0. TRn) by A79, TARSKI:def 1;

        then

         A81: (I0 . x1) = ( 0. TRn) by FUNCOP_1: 72;

        x2 in ( dom G) by A80, XBOOLE_0:def 5;

        hence thesis by A74, A81, FUNCT_1:def 3;

      end;

      H is onto by A18, A47, FUNCT_2:def 3;

      then

       A82: (H " ) = (HH " ) by A62, TOPS_2:def 4;

      

       A83: for p be Point of TRn st p in cTR0 holds (( Fr A) /\ ( halfline (( 0. TRn),p))) = {(H1B . p)}

      proof

        let p be Point of TRn;

        assume

         A84: p in cTR0;

        then

         A85: p in ( dom H1B) by A10, FUNCT_2:def 1;

        then

         A86: (H1B . p) = (H1 . (B . p)) by FUNCT_1: 12;

        (B . p) in ( dom H1) by A85, FUNCT_1: 11;

        then

        consider x be object such that

         A87: x in ( dom H) and

         A88: (H . x) = (B . p) by A18, A47, FUNCT_1:def 3;

        reconsider x as Point of TRn by A33, A37, A87;

        

         A89: (H . x) = (b . x) by A34, A87, FUNCT_1: 47;

        set xp = ( |.x.| / |.p.|);

        

         A90: x in FrA by A37, A87;

        then

         A91: (b . x) = ((1 / |.x.|) * x) by A9, A23, A38;

         |.((1 / |.x.|) * x).| = 1 by A9, A23, A38, A90;

        then ((1 / |.x.|) * x) <> ( 0. TRn) 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 A23, A84, A88, A89, A91

        .= (xp * p) by RLVECT_1:def 7;

        then x in ( halfline (( 0. TRn),p)) by Lm2;

        then

         A92: x in (( Fr A) /\ ( halfline (( 0. TRn),p))) by A37, A87, XBOOLE_0:def 4;

        p <> ( 0. TRn) by A84, ZFMISC_1: 56;

        then

        consider y be Point of TRn such that

         A93: (( Fr A) /\ ( halfline (( 0. TRn),p))) = {y} by A13;

        (H1 . (B . p)) = x by A62, A82, A87, A88, FUNCT_1: 34;

        hence thesis by A86, A92, A93, TARSKI:def 1;

      end;

      for x1,x2 be object st x1 in ( dom G) & x2 in ( dom G) & (G . x1) = (G . x2) holds x1 = x2

      proof

        let x1,x2 be object such that

         A94: x1 in ( dom G) and

         A95: x2 in ( dom G) and

         A96: (G . x1) = (G . x2);

        reconsider p1 = x1, p2 = x2 as Point of TRn by A65, A94, A95;

        consider Hp1 be Point of TRn such that

         A97: Hp1 = (H1B . p1) and Hp1 in FrA and

         A98: (G . p1) = ((1 / |.Hp1.|) * p1) and

         A99: |.Hp1.| > 0 by A10, A67, A94;

        

         A100: (FrA /\ ( halfline (( 0. TRn),p1))) = {Hp1} by A10, A83, A94, A97;

        consider Hp2 be Point of TRn such that

         A101: Hp2 = (H1B . p2) and Hp2 in FrA and

         A102: (G . p2) = ((1 / |.Hp2.|) * p2) and |.Hp2.| > 0 by A10, A67, A95;

        p1 <> ( 0. TRn) by A10, A94, ZFMISC_1: 56;

        then

         A103: ((1 / |.Hp1.|) * p1) <> ( 0. TRn) by A99, RLVECT_1: 11;

        

        then ( halfline (( 0. TRn),p1)) = ( halfline (( 0. TRn),((1 / |.Hp1.|) * p1))) by Lm2, TOPREAL9: 31

        .= ( halfline (( 0. TRn),p2)) by A96, A98, A102, A103, Lm2, TOPREAL9: 31;

        then Hp1 in {Hp1} & {Hp1} = {Hp2} by A10, A83, A95, A100, A101, TARSKI:def 1;

        then (1 / |.Hp1.|) = (1 / |.Hp2.|) by TARSKI:def 1;

        hence thesis by A96, A98, A99, A102, RLVECT_1: 36;

      end;

      then

       A104: G is one-to-one by FUNCT_1:def 4;

      set G0 = (G +* I0);

      

       A105: ( dom G0) = (( dom G) \/ ( dom I0)) by FUNCT_4:def 1

      .= (cTR0 \/ {( 0. TRn)}) by A31, A65

      .= cTRn by ZFMISC_1: 116;

      

       A106: for p,Hp be Point of TRn st p in cTR0 & Hp = (H1B . p) holds p = (G . ( |.Hp.| * p)) & ( |.Hp.| * p) in ( dom G)

      proof

        let p,Hp1 be Point of TRn such that

         A107: p in cTR0 and

         A108: Hp1 = (H1B . p);

        reconsider p as Point of TRn;

        consider Hp be Point of TRn such that

         A109: Hp = (H1B . p) and Hp in FrA and (G . p) = ((1 / |.Hp.|) * p) and

         A110: |.Hp.| > 0 by A67, A107;

        set Hpp = ( |.Hp.| * p);

        p <> ( 0. TRn) by A107, ZFMISC_1: 56;

        then

         A111: Hpp <> ( 0. TRn) by A110, RLVECT_1: 11;

        then

         A112: Hpp in cTR0 by ZFMISC_1: 56;

        then

        consider HP be Point of TRn such that

         A113: HP = (H1B . Hpp) and HP in FrA and

         A114: (G . Hpp) = ((1 / |.HP.|) * Hpp) and |.HP.| > 0 by A67;

        

         A115: Hp in {Hp} by TARSKI:def 1;

         {HP} = (( Fr A) /\ ( halfline (( 0. TRn),Hpp))) by A83, A112, A113

        .= (( Fr A) /\ ( halfline (( 0. TRn),p))) by A111, Lm2, TOPREAL9: 31

        .= {Hp} by A83, A107, A109;

        

        then (G . Hpp) = ((1 / |.Hp.|) * ( |.Hp.| * p)) by A114, A115, TARSKI:def 1

        .= (( |.Hp.| / |.Hp.|) * p) by RLVECT_1:def 7

        .= (1 * p) by A110, XCMPLX_1: 60

        .= p by RLVECT_1:def 8;

        hence thesis by A65, A108, A109, A111, ZFMISC_1: 56;

      end;

      

       A116: S c= (G .: FrA)

      proof

        let p be object;

        assume

         A117: p in S;

        then

        reconsider p as Point of TRn;

         |.p.| = 1 by A117, TOPREAL9: 12;

        then p <> ( 0. TRn) by TOPRNS_1: 23;

        then

         A118: p in cTR0 by ZFMISC_1: 56;

        then

        consider Hp be Point of TRn such that

         A119: Hp = (H1B . p) and

         A120: Hp in FrA and (G . p) = ((1 / |.Hp.|) * p) and |.Hp.| > 0 by A67;

        set Hpp = ( |.Hp.| * p);

        

         A121: p = (G . Hpp) & Hpp in ( dom G) by A106, A118, A119;

        Hp in {Hp} & (( Fr A) /\ ( halfline (( 0. TRn),p))) = {Hp} by A83, A118, A119, TARSKI:def 1;

        then

         A122: Hp in ( halfline (( 0. TRn),p)) by XBOOLE_0:def 4;

        

         A123: (Hp - ( 0. TRn)) = Hp;

         |. |.Hp.|.| = |.Hp.| by ABSVALUE:def 1;

        

        then

         A124: |.Hpp.| = ( |.Hp.| * |.p.|) by TOPRNS_1: 7

        .= ( |.Hp.| * 1) by A117, TOPREAL9: 12;

        (Hpp - ( 0. TRn)) = Hpp & Hpp in ( halfline (( 0. TRn),p)) by Lm2;

        then Hp = Hpp by A124, A122, A123, Th2;

        hence thesis by A120, A121, FUNCT_1:def 6;

      end;

      

       A125: ( 0. TRn) in {( 0. TRn)} by TARSKI:def 1;

      then

       A126: (I0 . ( 0. TRn)) = ( 0. TRn) by A31, FUNCOP_1: 7;

      ( rng I0) = {( 0. TRn)} by A31, FUNCOP_1: 8;

      then ( rng G0) = (( rng G) \/ {( 0. TRn)}) by A32, A65, NECKLACE: 6, XBOOLE_1: 79;

      then

      reconsider G1 = G0 as one-to-one Function of TRn, TRn by A105, A78, A104, FUNCT_2: 2, TOPMETR2: 1;

      

       A127: (G1 . ( 0. TRn)) = (I0 . ( 0. TRn)) by A32, A125, FUNCT_4: 13;

      

       A128: (G .: FrA) c= S

      proof

        let y be object;

        assume y in (G .: FrA);

        then

        consider p be object such that

         A129: p in ( dom G) and

         A130: p in FrA and

         A131: (G . p) = y by FUNCT_1:def 6;

        reconsider p as Point of TRn by A130;

        consider Hp be Point of TRn such that

         A132: Hp = (H1B . p) and Hp in FrA and

         A133: (G . p) = ((1 / |.Hp.|) * p) and

         A134: |.Hp.| > 0 by A10, A67, A129;

        p in ( halfline (( 0. TRn),p)) by TOPREAL9: 28;

        then

         A135: p in (FrA /\ ( halfline (( 0. TRn),p))) by A130, XBOOLE_0:def 4;

        (FrA /\ ( halfline (( 0. TRn),p))) = {Hp} by A10, A83, A129, A132;

        then

         A136: p = Hp by A135, TARSKI:def 1;

         |.(1 / |.Hp.|).| = (1 / |.Hp.|) by ABSVALUE:def 1;

        

        then |.((1 / |.Hp.|) * p).| = ((1 / |.Hp.|) * |.Hp.|) by A136, TOPRNS_1: 7

        .= 1 by A134, XCMPLX_1: 106;

        then |.(((1 / |.Hp.|) * p) - ( 0. TRn)).| = 1;

        hence thesis by A131, A133;

      end;

      set TRnCL = (TRn | CL);

      set TRnA = (TRn | A);

      

       A137: ( Int A) c= A by TOPS_1: 16;

      set GA = (G1 | TRnA);

      

       A138: (G1 | TRnA) = (G1 | the carrier of TRnA) by TMAP_1:def 4;

      

       A139: ( [#] TRnA) = A by PRE_TOPC:def 5;

      then

       A140: ( dom GA) = A by FUNCT_2:def 1;

      

       A141: ( dom GA) = the carrier of TRnA by FUNCT_2:def 1;

      

       A142: ( cl_Ball (( 0. TRn),1)) c= ( rng GA)

      proof

        let p be object;

        assume

         A143: p in ( cl_Ball (( 0. TRn),1));

        then

        reconsider p as Point of TRn;

        per cases ;

          suppose p = ( 0. TRn);

          then p = (GA . ( 0. TRn)) by A3, A137, A5, A126, A138, A139, A127, FUNCT_1: 49;

          hence thesis by A3, A137, A5, A139, A141, FUNCT_1:def 3;

        end;

          suppose

           A144: p <> ( 0. TRn);

          set h = ( halfline (( 0. TRn),p));

          

           A145: p in cTR0 by A144, ZFMISC_1: 56;

          then

          consider Hp be Point of TRn such that

           A146: Hp = (H1B . p) and

           A147: Hp in FrA and (G . p) = ((1 / |.Hp.|) * p) and

           A148: |.Hp.| > 0 by A67;

          

           A149: |. |.Hp.|.| = |.Hp.| by ABSVALUE:def 1;

          (( Fr A) /\ h) = {Hp} by A83, A145, A146;

          then Hp in (( Fr A) /\ h) by TARSKI:def 1;

          then

           A150: Hp in h by XBOOLE_0:def 4;

          Hp <> ( 0. TRn) by A148, TOPRNS_1: 23;

          then h = ( halfline (( 0. TRn),Hp)) by A150, TOPREAL9: 31;

          then

           A151: ( |.p.| * Hp) in h by Lm2;

           |.p.| <= 1 by A143, TOPREAL9: 11;

          then ((1 - |.p.|) * ( 0. TRn)) = ( 0. TRn) & (( |.p.| * Hp) + ((1 - |.p.|) * ( 0. TRn))) in A by A3, A137, A5, A17, A147, RLTOPSP1:def 1;

          then ( |.p.| * Hp) in ( dom GA) by A140;

          then

           A152: (GA . ( |.p.| * Hp)) in ( rng GA) & (GA . ( |.p.| * Hp)) = (G1 . ( |.p.| * Hp)) by A138, FUNCT_1: 47, FUNCT_1:def 3;

          

           A153: ( |.Hp.| * p) in h by Lm2;

          ( |.Hp.| * p) in ( dom G) by A106, A145, A146;

          then ( |.Hp.| * p) <> ( 0. TRn) by A10, ZFMISC_1: 56;

          then not ( |.Hp.| * p) in ( dom I0) by TARSKI:def 1;

          then

           A154: (G . ( |.Hp.| * p)) = (G1 . ( |.Hp.| * p)) by FUNCT_4: 11;

           |. |.p.|.| = |.p.| by ABSVALUE:def 1;

          

          then |.( |.p.| * Hp).| = ( |.p.| * |.Hp.|) by TOPRNS_1: 7

          .= |.( |.Hp.| * p).| by A149, TOPRNS_1: 7;

          

          then

           A155: |.(( |.p.| * Hp) - ( 0. TRn)).| = |.( |.Hp.| * p).|

          .= |.(( |.Hp.| * p) - ( 0. TRn)).|;

          p = (G . ( |.Hp.| * p)) by A106, A145, A146;

          hence thesis by A151, A154, A155, A152, A153, Th2;

        end;

      end;

      ( rng GA) c= ( cl_Ball (( 0. TRn),1))

      proof

        let x be object;

        assume x in ( rng GA);

        then

        consider p be object such that

         A156: p in ( dom GA) and

         A157: (GA . p) = x by FUNCT_1:def 3;

        reconsider p as Point of TRn by A140, A156;

        

         A158: (GA . p) = (G1 . p) by A138, A156, FUNCT_1: 47;

        

         A159: ((G1 . p) - ( 0. TRn)) = (G1 . p);

        per cases ;

          suppose p = ( 0. TRn);

          then (G1 . p) = ( 0. TRn) by A31, A125, A127, FUNCOP_1: 7;

          then |.((G1 . p) - ( 0. TRn)).| = 0 by TOPRNS_1: 23;

          hence thesis by A157, A158;

        end;

          suppose

           A160: p <> ( 0. TRn);

          set h = ( halfline (( 0. TRn),p));

          

           A161: (A /\ h) c= aa by XBOOLE_1: 17;

          then

          reconsider F = (A /\ h) as Subset of En by XBOOLE_1: 1;

          F is bounded by A12, A161, HAUSDORF: 18, TBSP_1: 14;

          then (A /\ h) is bounded by JORDAN2C: 11;

          then

          consider w be Point of En such that

           A162: w in (( Fr A) /\ h) and

           A163: for u,P be Point of En st P = ( 0. TRn) & u in (A /\ h) holds ( dist (P,u)) <= ( dist (P,w)) and for r st r > 0 holds ex u be Point of En st u in (A /\ h) & ( dist (w,u)) < r by A3, A137, A5, A160, Lm3;

          reconsider P = p as Point of En by EUCLID: 67;

          p in h by TOPREAL9: 28;

          then

           A164: p in (A /\ h) by A139, A156, XBOOLE_0:def 4;

          

           A165: not p in ( dom I0) by A160, TARSKI:def 1;

          

           A166: p in cTR0 by A160, ZFMISC_1: 56;

          then

          consider Hp be Point of TRn such that

           A167: Hp = (H1B . p) and Hp in FrA and

           A168: (G . p) = ((1 / |.Hp.|) * p) and |.Hp.| > 0 by A67;

           |.(1 / |.Hp.|).| = (1 / |.Hp.|) by ABSVALUE:def 1;

          then

           A169: |.((1 / |.Hp.|) * p).| = ( |.p.| / |.Hp.|) by TOPRNS_1: 7;

          (( Fr A) /\ h) = {Hp} by A83, A166, A167;

          then w = Hp by A162, TARSKI:def 1;

          

          then

           A170: ( dist (0TRn,w)) = |.(( 0. TRn) - Hp).| by SPPOL_1: 39

          .= |.( - Hp).|

          .= |.Hp.| by TOPRNS_1: 26;

          ( dist (0TRn,P)) = |.(( 0. TRn) - p).| by SPPOL_1: 39

          .= |.( - p).|

          .= |.p.| by TOPRNS_1: 26;

          then |.((1 / |.Hp.|) * p).| <= 1 by A163, A164, A169, A170, XREAL_1: 183;

          then |.(G1 . p).| <= 1 by A165, A168, FUNCT_4: 11;

          hence thesis by A157, A158, A159;

        end;

      end;

      then

       A171: ( rng GA) = CL by A142, XBOOLE_0:def 10;

      

       A172: ( [#] TRnCL) = CL by PRE_TOPC:def 5;

      then

      reconsider GA as Function of TRnA, TRnCL by A139, A140, A171, FUNCT_2: 1;

      set e2 = (e / 2);

      

       A173: GA is one-to-one by A138, FUNCT_1: 52;

      

       A174: e2 < e by A6, XREAL_1: 216;

      

       A175: G1 is continuous

      proof

        let x be Point of TRn, U be a_neighborhood of (G1 . x);

        per cases ;

          suppose

           A176: x <> ( 0. TRn);

          then

           A177: x in ( dom G) by A65, ZFMISC_1: 56;

          then

          reconsider X = x as Point of TRn0;

           not x in ( dom I0) by A176, TARSKI:def 1;

          then

           A178: (G . x) = (G1 . x) by FUNCT_4: 11;

          then

           A179: (G1 . x) <> ( 0. TRn) by A74, A177, FUNCT_1:def 3;

          then

          reconsider G1x = (G1 . x) as Point of TRn0 by A10, ZFMISC_1: 56;

          (G1 . x) in cTR0 by A179, 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 be a_neighborhood of X such that

           A180: (G .: H) c= (cTR0 /\ U) by A178, BORSUK_1:def 1;

          reconsider h = H as Subset of TRn by A10, XBOOLE_1: 1;

          reconsider h as a_neighborhood of x by CONNSP_2: 9;

           {( 0. TRn)} misses H by A10, XBOOLE_1: 63, XBOOLE_1: 79;

          then (cTR0 /\ U) c= U & (G .: H) = (G1 .: h) by A31, BOOLMARK: 3, XBOOLE_1: 17;

          hence thesis by A180, XBOOLE_1: 1;

          reconsider U1 = (cTR0 /\ U) as Subset of TRn0 by A10, XBOOLE_1: 17;

        end;

          suppose

           A181: x = ( 0. TRn);

          reconsider 0TRn = ( 0. TRn) as Point of ( Euclid n) by EUCLID: 67;

          

           A182: ( 0. TRn) in ( Int U) by A126, A127, A181, CONNSP_2:def 1;

          then

          consider r be Real such that

           A183: r > 0 and

           A184: ( Ball (0TRn,r)) c= U by GOBOARD6: 5;

          reconsider B = ( Ball (0TRn,(r * e2))) as Subset of TRn by EUCLID: 67;

          0TRn in ( Int B) by A6, A183, GOBOARD6: 5;

          then

          reconsider Bx = B as a_neighborhood of x by A181, CONNSP_2:def 1;

          take Bx;

          let y be object;

          assume

           A185: y in (G1 .: Bx);

          then

          reconsider p = y as Point of TRn;

          

           A186: ( Int U) c= U by TOPS_1: 16;

          per cases ;

            suppose y = ( 0. TRn);

            hence y in U by A182, A186;

          end;

            suppose

             A187: p <> ( 0. TRn);

            set PP = ((e2 / |.p.|) * p);

             |.(e2 / |.p.|).| = (e2 / |.p.|) by A6, ABSVALUE:def 1;

            

            then

             A188: |.PP.| = ((e2 / |.p.|) * |.p.|) by TOPRNS_1: 7

            .= (e2 * ( |.p.| / |.p.|))

            .= (e2 * 1) by A187, TOPRNS_1: 24, XCMPLX_1: 60

            .= e2;

            then |.(PP - ( 0. TRn)).| < e by A174;

            then

             A189: PP in ( Ball (( 0. TRn),e));

            set h = ( halfline (( 0. TRn),p));

            

             A190: (A /\ h) c= aa by XBOOLE_1: 17;

            then

            reconsider F = (A /\ h) as Subset of En by XBOOLE_1: 1;

            F is bounded by A12, A190, HAUSDORF: 18, TBSP_1: 14;

            then (A /\ h) is bounded by JORDAN2C: 11;

            then

            consider w be Point of En such that

             A191: w in (( Fr A) /\ h) and

             A192: for u,P be Point of En st P = ( 0. TRn) & u in (A /\ h) holds ( dist (P,u)) <= ( dist (P,w)) and for r st r > 0 holds ex u be Point of En st u in (A /\ h) & ( dist (w,u)) < r by A3, A137, A5, A187, Lm3;

            

             A193: p in cTR0 by A187, ZFMISC_1: 56;

            then

            consider Hp be Point of TRn such that

             A194: Hp = (H1B . p) and Hp in FrA and (G . p) = ((1 / |.Hp.|) * p) and

             A195: |.Hp.| > 0 by A67;

            (( Fr A) /\ h) = {Hp} by A83, A193, A194;

            then w = Hp by A191, TARSKI:def 1;

            

            then

             A196: ( dist (0TRn,w)) = |.(( 0. TRn) - Hp).| by SPPOL_1: 39

            .= |.( - Hp).|

            .= |.Hp.| by TOPRNS_1: 26;

            set Hpp = ( |.Hp.| * p);

            Hpp in ( dom G) by A106, A193, A194;

            then Hpp <> ( 0. TRn) by A10, ZFMISC_1: 56;

            then not Hpp in ( dom I0) by TARSKI:def 1;

            then

             A197: (G . Hpp) = (G1 . Hpp) by FUNCT_4: 11;

             |.Hp.| = |. |.Hp.|.| by ABSVALUE:def 1;

            then

             A198: Bx = ( Ball (( 0. TRn),(r * e2))) & |.Hpp.| = ( |.Hp.| * |.p.|) by TOPREAL9: 13, TOPRNS_1: 7;

            reconsider pp = PP as Point of En by EUCLID: 67;

            consider x be object such that

             A199: x in ( dom G1) and

             A200: x in Bx and

             A201: (G1 . x) = p by A185, FUNCT_1:def 6;

            PP in h & ( Ball (( 0. TRn),e)) = ( Ball (0TRn,e)) by A6, Lm2, TOPREAL9: 13;

            then

             A202: pp in (A /\ h) by A7, A189, XBOOLE_0:def 4;

            ( dist (0TRn,pp)) = |.(( 0. TRn) - PP).| by SPPOL_1: 39

            .= |.( - PP).|

            .= e2 by A188, TOPRNS_1: 26;

            then (e2 / |.Hp.|) <= 1 by A192, A196, A202, XREAL_1: 183;

            then

             A203: (r * (e2 / |.Hp.|)) <= (r * 1) by A183, XREAL_1: 64;

            p = (G . Hpp) by A106, A193, A194;

            then Hpp = x by A105, A197, A199, A201, FUNCT_1:def 4;

            then |.p.| < ((r * e2) / |.Hp.|) by A195, A198, A200, TOPREAL9: 10, XREAL_1: 81;

            then |.p.| < r by A203, XXREAL_0: 2;

            then |.(p - ( 0. TRn)).| < r;

            then p in ( Ball (( 0. TRn),r));

            then p in ( Ball (0TRn,r)) by TOPREAL9: 13;

            hence y in U by A184;

          end;

        end;

      end;

      (GA .: FrA) = (G1 .: FrA) by A2, A138, A139, RELAT_1: 129, TOPS_1: 35;

      then (GA .: FrA) = (G .: FrA) by A5, A8, A31, BOOLMARK: 3, ZFMISC_1: 50;

      then

       A204: (GA .: FrA) = S by A116, A128, XBOOLE_0:def 10;

      ( dom GA) = ( [#] TRnA) & ( rng GA) = ( [#] TRnCL) by A142, A172, FUNCT_2:def 1, XBOOLE_0:def 10;

      then GA is being_homeomorphism by A2, A3, A137, A173, A175, COMPTS_1: 17, PRE_TOPC: 27;

      hence thesis by A204;

    end;

    theorem :: BROUWER2:5

    

     Th5: r > 0 implies ( Fr ( cl_Ball (p,r))) = ( Sphere (p,r))

    proof

      set TR = ( TOP-REAL n);

      assume

       A1: r > 0 ;

      set CB = ( cl_Ball (p,r)), B = ( Ball (p,r)), S = ( Sphere (p,r));

      reconsider tr = TR as TopSpace;

      reconsider cb = CB as Subset of tr;

      

       A2: B misses S by TOPREAL9: 19;

      

       A3: (B \/ S) = CB by TOPREAL9: 18;

      

       A4: ( Int cb) c= B

      proof

        reconsider ONE = 1 as Real;

        let x be object;

        assume x in ( Int cb);

        then

        consider Q be Subset of TR such that

         A5: Q is open and

         A6: Q c= CB and

         A7: x in Q by TOPS_1: 22;

        reconsider q = x as Point of TR by A7;

        consider w be positive Real such that

         A8: ( Ball (q,w)) c= Q by A5, A7, TOPS_4: 2;

        assume not x in B;

        then q in ( Sphere (p,r)) by A3, A6, A7, XBOOLE_0:def 3;

        then

         A9: |.(q - p).| = r by TOPREAL9: 9;

        set w2 = (w / 2);

        set wr = ((w2 / r) * (q - p));

        

         A10: |.(w2 / r).| = (w2 / r) by A1, ABSVALUE:def 1;

        

         A11: ((wr + q) - p) = (wr + (q - p)) by RLVECT_1: 28

        .= (wr + (ONE * (q - p))) by RLVECT_1:def 8

        .= (((w2 / r) + ONE) * (q - p)) by RLVECT_1:def 6;

         |.((wr + q) - q).| = |.(wr + (q - q)).| by RLVECT_1:def 3

        .= |.(wr + ( 0. TR)).| by RLVECT_1: 15

        .= |.wr.|

        .= ((w2 / r) * r) by A9, A10, TOPRNS_1: 7

        .= w2 by A1, XCMPLX_1: 87;

        then |.((wr + q) - q).| < w by XREAL_1: 216;

        then (wr + q) in ( Ball (q,w));

        then

         A12: (wr + q) in Q by A8;

        

         A13: ((w2 / r) + ONE) = ((w2 / r) + (r / r)) by A1, XCMPLX_1: 60

        .= ((w2 + r) / r);

        

         A14: (w2 + r) > ( 0 + r) by XREAL_1: 6;

         |.((w2 + r) / r).| = ((w2 + r) / r) by A1, ABSVALUE:def 1;

        

        then |.((wr + q) - p).| = (((w2 + r) / r) * r) by A9, A13, A11, TOPRNS_1: 7

        .= (w2 + r) by A1, XCMPLX_1: 87;

        hence contradiction by A6, A12, A14, TOPREAL9: 8;

      end;

      B c= ( Int cb) by TOPREAL9: 16, TOPS_1: 24;

      then ( Int cb) = B by A4, XBOOLE_0:def 10;

      then ( Fr CB) = (CB \ B) by TOPS_1: 43;

      hence thesis by A3, A2, XBOOLE_1: 88;

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

      cluster (p + A) -> bounded;

      coherence

      proof

        set TR = ( TOP-REAL n);

        set En = ( Euclid n);

        reconsider a = A as bounded Subset of En by JORDAN2C: 11;

        reconsider pA = (p + A) as Subset of En by EUCLID: 67;

        consider r be Real such that

         A1: 0 < r and

         A2: for x,y be Point of En st x in a & y in a holds ( dist (x,y)) <= r by TBSP_1:def 7;

        

         A3: pA = { (p + u) where u be Element of TR : u in A } by RUSUB_4:def 8;

        now

          let x,y be Point of En;

          assume x in pA;

          then

          consider px be Element of TR such that

           A4: x = (p + px) and

           A5: px in A by A3;

          assume y in pA;

          then

          consider py be Element of TR such that

           A6: y = (p + py) and

           A7: py in A by A3;

          reconsider pX = px, pY = py as Point of En by EUCLID: 67;

          ((p + px) - (p + py)) = (((p + px) - p) - py) by RLVECT_1: 27

          .= (px - py) by RLVECT_4: 1;

          

          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;

        end;

        then pA is bounded by A1, TBSP_1:def 7;

        hence thesis by JORDAN2C: 11;

      end;

    end

    begin

    theorem :: BROUWER2:6

    

     Th6: for n be Element of NAT holds for A be convex Subset of ( TOP-REAL n) st A is compact non boundary holds ex h be 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 ;

      set TRn = ( TOP-REAL n);

      let A be convex Subset of TRn such that

       A1: A is compact non boundary;

      ( Int A) <> {} by A1, TOPS_1: 48;

      then

      consider p be object such that

       A2: p in ( Int A) by XBOOLE_0:def 1;

      set TRnA = (TRn | A);

      reconsider p as Point of TRn by A2;

      

       A3: ( Int A) c= A by TOPS_1: 16;

      

       A4: A is non empty by A2;

      per cases ;

        suppose

         A5: n = 0 ;

        set T = ( Tdisk (( 0. TRn),1));

        

         A6: {( 0. TRn)} = the carrier of TRn by A5, EUCLID: 22, EUCLID: 77;

        then

         A7: A = {( 0. TRn)} by A4, ZFMISC_1: 33;

        then

        reconsider I = ( id (TRn | A)) as Function of (TRn | A), T by A6, ZFMISC_1: 33;

        take I;

        

         A8: ( Fr A) = (A \ ( Int A)) by A5, TOPS_1: 43;

        

         A9: ( Sphere (( 0. TRn),1)) = {}

        proof

          assume ( Sphere (( 0. TRn),1)) <> {} ;

          then ( Sphere (( 0. TRn),1)) = A by A6, A7, ZFMISC_1: 33;

          then |.( 0. TRn).| = 1 by A6, A7, TOPREAL9: 12;

          hence contradiction by TOPRNS_1: 23;

        end;

        ( Int A) = A by A2, A3, A7, ZFMISC_1: 33;

        then

         A10: ( Fr A) = {} by A8, XBOOLE_1: 37;

        T = (TRn | A) by A6, A7, ZFMISC_1: 33;

        hence thesis by A10, A9;

      end;

        suppose

         A11: n > 0 ;

        set T = ( transl (( - p),TRn));

        set TA = (T .: A);

        

         A12: TA = (( - p) + A) by RLTOPSP1: 33;

        then

         A13: ( 0. TRn) = ( 0* n) & TA is convex by CONVEX1: 7, EUCLID: 70;

        reconsider TT = (T | A) as Function of TRnA, (TRn | TA) by JORDAN24: 12;

        

         A14: (TT .: ( Int A)) = (T .: ( Int A)) by RELAT_1: 129, TOPS_1: 16;

        ( 0. TRn) = (( - p) + p) by RLVECT_1: 5;

        then

         A15: ( 0. TRn) in { (( - p) + q) where q be Element of TRn : q in ( Int A) } by A2;

        ( Int TA) = (( - p) + ( Int A)) by A12, RLTOPSP1: 37;

        then ( 0. TRn) in ( Int TA) by A15, RUSUB_4:def 8;

        then

        consider h be Function of (TRn | TA), ( Tdisk (( 0. TRn),1)) such that

         A16: h is being_homeomorphism and

         A17: (h .: ( Fr TA)) = ( Sphere (( 0. TRn),1)) by A1, A11, A12, A13, Lm4;

        reconsider hTT = (h * TT) as Function of (TRn | A), ( Tdisk (( 0. TRn),1)) by A4;

        take hTT;

        

         A18: ( Int TA) = (( - p) + ( Int A)) by A12, RLTOPSP1: 37

        .= (T .: ( Int A)) by RLTOPSP1: 33;

        

         A19: TT is being_homeomorphism by JORDAN24: 14;

        then ( dom TT) = ( [#] TRnA) 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;

        ( rng TT) = ( [#] (TRn | TA)) by A19, TOPS_2:def 5;

        then

         A21: ( rng TT) = TA 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 TA) = (TA \ ( Int TA)) by A1, A12, TOPS_1: 43

        .= (TT .: ( Fr A)) by A18, A22, A20, A21, A14, RELAT_1: 113;

        hence (hTT .: ( Fr A)) = ( Sphere (( 0. TRn),1)) by A17, RELAT_1: 126;

      end;

    end;

    theorem :: BROUWER2:7

    

     Th7: for A, B st A is compact non boundary & B is compact non boundary holds ex h be Function of (( TOP-REAL n) | A), (( TOP-REAL n) | B) st h is being_homeomorphism & (h .: ( Fr A)) = ( Fr B)

    proof

      set T = ( TOP-REAL n);

      let A,B be convex Subset of T such that

       A1: A is compact non boundary and

       A2: B is compact non boundary;

      

       A3: (A is non empty) & B is non empty by A1, A2;

      reconsider N = n as Element of NAT by ORDINAL1:def 12;

      set TN = ( TOP-REAL N);

      consider hA be Function of (T | A), ( Tdisk (( 0. TN),1)) such that

       A4: hA is being_homeomorphism and

       A5: (hA .: ( Fr A)) = ( Sphere (( 0. T),1)) by A1, Th6;

      consider hB be Function of (T | B), ( Tdisk (( 0. TN),1)) such that

       A6: hB is being_homeomorphism and

       A7: (hB .: ( Fr B)) = ( Sphere (( 0. T),1)) by A2, Th6;

      reconsider h = ((hB " ) * hA) as Function of (T | A), (T | B);

      take h;

      (hB " ) is being_homeomorphism by A6, TOPS_2: 56;

      hence h is being_homeomorphism by A3, A4, TOPS_2: 57;

      

       A8: ( rng hB) = ( [#] ( Tdisk (( 0. TN),1))) by A6, TOPS_2:def 5;

      ( dom hB) = ( [#] (T | B)) by A6, TOPS_2:def 5;

      then

       A9: ( dom hB) = B by PRE_TOPC:def 5;

      the carrier of ( Tdisk (( 0. TN),1)) = ( cl_Ball (( 0. TN),1)) by BROUWER: 3;

      then

       A10: ( Sphere (( 0. T),1)) is Subset of ( Tdisk (( 0. TN),1)) by TOPREAL9: 17;

      

      thus (h .: ( Fr A)) = ((hB " ) .: ( Sphere (( 0. T),1))) by A5, RELAT_1: 126

      .= (hB " ( Sphere (( 0. T),1))) by A6, A8, A10, TOPS_2: 55

      .= ( Fr B) by A2, A6, A7, A9, FUNCT_1: 94, TOPS_1: 35;

    end;

    theorem :: BROUWER2:8

    

     Th8: for A st A is compact non boundary holds for h be continuous Function of (( TOP-REAL n) | A), (( TOP-REAL n) | A) holds h is with_fixpoint

    proof

      set T = ( TOP-REAL n);

      consider I be affinely-independent Subset of T such that ( {} T) c= I and I c= ( [#] T) and

       A1: ( Affin I) = ( Affin ( [#] T)) by RLAFFIN1: 60;

      reconsider TT = T as non empty RLSStruct;

      reconsider i = I as Subset of TT;

      set II = ( Int i);

      

       A2: I is non empty by A1;

      then

       A3: II is non empty by RLAFFIN2: 20;

      reconsider ii = II as Subset of T;

      

       A4: ( Int ii) c= ( Int ( conv I)) by RLAFFIN2: 5, TOPS_1: 19;

      let A be convex Subset of T such that

       A5: A is compact non boundary;

      

       A6: A is non empty by A5;

      let h be continuous Function of (T | A), (T | A);

      ( [#] T) is Affine by RUSUB_4: 22;

      then ( dim T) = n & ( Affin ( [#] T)) = ( [#] T) by RLAFFIN1: 50, RLAFFIN3: 4;

      then

       A7: ( card I) = (n + 1) by A1, RLAFFIN3: 6;

      then ii is open by RLAFFIN3: 33;

      then ( conv I) is non boundary by A3, A4, TOPS_1: 23;

      then

      consider f be Function of (T | A), (T | ( 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 (T | ( conv I)), (T | ( conv I)) by A6;

      (f " ) is continuous by A8, TOPS_2:def 5;

      then

      consider p be Point of T 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) = ( [#] (T | ( conv I))) by A8, TOPS_2:def 5;

      

       A13: (f " ) = (F " ) by A8, TOPS_2:def 4;

      consider x be object 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) = ( [#] (T | 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 thesis by ABIAN:def 5;

    end;

    

     Lm5: ( cl_Ball (( 0. ( TOP-REAL n)),1)) is non boundary

    proof

      set TR = ( TOP-REAL n);

      reconsider tr = TR as TopStruct;

      reconsider cB = ( cl_Ball (( 0. TR),1)) as Subset of tr;

      ( Ball (( 0. TR),1)) c= ( Int cB) by TOPREAL9: 16, TOPS_1: 24;

      hence thesis;

    end;

    reconsider jj = 1 as Real;

    

     Lm6: for n be Element of NAT holds for X be 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 ;

      set TR = ( TOP-REAL n);

      set Td = ( Tdisk (( 0. TR),1));

      

       A1: ( Sphere (( 0. TR),1)) c= ( cl_Ball (( 0. TR),1)) by TOPREAL9: 17;

      set M = ( mlt (( - jj),TR));

      let X be non empty SubSpace of ( Tdisk (( 0. TR),1)) such that

       A2: X = ( Tcircle (( 0. TR),1));

      

       A3: the carrier of X = ( Sphere (( 0. TR),1)) by A2, TOPREALB: 9;

      assume X is_a_retract_of Td;

      then

      consider F be continuous Function of Td, X such that

       A4: F is being_a_retraction;

      

       A5: the carrier of Td = ( cl_Ball (( 0. TR),1)) by BROUWER: 3;

      then

      reconsider f = F as Function of Td, Td by A3, A1, FUNCT_2: 7;

      set Mf = ((M | Td) * f);

      

       A6: (M | Td) = (M | the carrier of Td) by TMAP_1:def 4;

      

       A7: ( rng Mf) c= ( Sphere (( 0. TR),1))

      proof

        let y be object;

        assume y in ( rng Mf);

        then

        consider x be object such that

         A8: x in ( dom Mf) and

         A9: (Mf . x) = y by FUNCT_1:def 3;

        

         A10: (f . x) in ( dom (M | Td)) by A8, FUNCT_1: 11;

        then (f . x) in ( dom M) by A6, RELAT_1: 57;

        then

        reconsider fx = (f . x) as Point of TR;

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

        y = ((M | Td) . (f . x)) by A8, A9, FUNCT_1: 12;

        then y = (M . (f . x)) by A6, A10, FUNCT_1: 47;

        

        then y = (( - 1) * fx) by RLTOPSP1:def 13

        .= ( - fx) by RLVECT_1: 16;

        hence thesis by A11;

      end;

      then ( rng Mf) c= ( cl_Ball (( 0. TR),1)) by A1;

      then

      reconsider MF = Mf as Function of Td, Td by A5, FUNCT_2: 6;

      

       A12: ( cl_Ball (( 0. TR),1)) is non 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 be object 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 as Point of TR by A7;

      

       A17: (f . p) = p by A4, A3, A7, A16;

      then

       A18: p in ( dom (M | Td)) by A14, FUNCT_1: 11;

      p = ((M | Td) . p) by A14, A15, A17, FUNCT_1: 12;

      then p = (M . p) by A6, A18, FUNCT_1: 47;

      

      then p = (( - 1) * p) by RLTOPSP1:def 13

      .= ( - p) by RLVECT_1: 16;

      then

       A19: p = ( 0. TR) by RLVECT_1: 19;

       |.p.| = 1 by A7, A16, TOPREAL9: 12;

      hence contradiction by A19, TOPRNS_1: 23;

    end;

    theorem :: BROUWER2:9

    for A be non empty convex Subset of ( TOP-REAL n) st A is compact non boundary holds for FR be non empty SubSpace of (( TOP-REAL n) | A) st ( [#] FR) = ( Fr A) holds not FR is_a_retract_of (( TOP-REAL n) | A)

    proof

      set T = ( TOP-REAL n);

      set cB = ( cl_Ball (( 0. T),1)), S = ( Sphere (( 0. T),1));

      

       A1: ( [#] (T | cB)) = cB by PRE_TOPC:def 5;

      then

      reconsider s = S as Subset of (T | cB) by TOPREAL9: 17;

      

       A2: (T | S) = ((T | cB) | s) by PRE_TOPC: 7, TOPREAL9: 17;

      let A be non empty convex Subset of T such that

       A3: A is compact non boundary;

      

       A4: ( [#] (T | A)) = A & ( Fr A) c= A by A3, PRE_TOPC:def 5, TOPS_1: 35;

      let FR be non empty SubSpace of (T | A) such that

       A5: ( [#] FR) = ( Fr A);

      n > 0

      proof

        assume n <= 0 ;

        then n = 0 ;

        then {( 0. T)} = the carrier of T by EUCLID: 22, EUCLID: 77;

        then

         A6: A = ( [#] T) by ZFMISC_1: 33;

        then ( Fr A) = (( Cl A) \ A) by TOPS_1: 42;

        hence contradiction by A5, A6, XBOOLE_1: 37;

      end;

      then

      reconsider Ts = ((T | cB) | s) as non empty SubSpace of (T | cB);

      assume FR is_a_retract_of (T | A);

      then

      consider F be continuous Function of (T | A), FR such that

       A7: F is being_a_retraction;

      reconsider f = F as Function of (T | A), (T | A) by A5, A4, FUNCT_2: 7;

      

       A8: f is continuous by PRE_TOPC: 26;

      

       A9: ( rng F) c= ( Fr A) by A5;

      reconsider N = n as Element of NAT by ORDINAL1:def 12;

      set TN = ( TOP-REAL N);

      

       A10: ( [#] (T | S)) = S by PRE_TOPC:def 5;

      (T | cB) = ( Tdisk (( 0. TN),1)) & (T | S) = ( Tcircle (( 0. TN),1)) by TOPREALB:def 6;

      then

       A11: not Ts is_a_retract_of (T | cB) by A2, Lm6;

      cB is non boundary by Lm5;

      then

      consider h be Function of (T | cB), (T | A) such that

       A12: h is being_homeomorphism and

       A13: (h .: ( Fr cB)) = ( Fr A) by A3, Th7;

      

       A14: ( dom h) = ( [#] (T | cB)) by A12, TOPS_2:def 5;

      ( rng ((h " ) * f)) = (((h " ) * f) .: ( dom ((h " ) * f))) by RELAT_1: 113;

      then

       A15: ( rng ((h " ) * f)) c= (((h " ) * f) .: ( dom f)) by RELAT_1: 25, RELAT_1: 123;

      reconsider H = h as Function;

      

       A16: ( Fr cB) = S by Th5;

      ( rng h) = ( [#] (T | A)) by A12, TOPS_2:def 5;

      

      then

       A17: ((h " ) .: ( Fr A)) = (h " ( Fr A)) by A12, A4, TOPS_2: 55

      .= ( Fr cB) by A12, A13, A1, A14, 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 cB) by A17, A9, RELAT_1: 123;

      then ( rng (((h " ) * f) * h)) c= ( rng ((h " ) * f)) & ( rng ((h " ) * f)) c= ( Fr cB) by A15, RELAT_1: 26;

      then ( rng (((h " ) * f) * h)) c= ( Fr cB);

      then

      reconsider hfh = (((h " ) * f) * h) as Function of (T | cB), Ts by A2, A16, A10, FUNCT_2: 6;

      (h " ) is continuous by A12, TOPS_2:def 5;

      then hfh is continuous by A12, A8, PRE_TOPC: 27;

      then not hfh is being_a_retraction by A11;

      then

      consider x be Point of (T | cB) such that

       A18: x in S and

       A19: (hfh . x) <> x by A2, A10;

      set hx = (h . x);

      

       A20: ( dom hfh) = the carrier of (T | cB) by FUNCT_2:def 1;

      then

       A21: (hfh . x) = (((h " ) * f) . hx) by FUNCT_1: 12;

      x in ( dom h) by A20, FUNCT_1: 11;

      then

       A22: hx in the carrier of FR by A5, A13, A16, A18, FUNCT_1:def 6;

      hx in ( dom ((h " ) * f)) by A20, FUNCT_1: 11;

      then

       A23: (((h " ) * f) . hx) = ((h " ) . (f . hx)) by FUNCT_1: 12;

      

       A24: (H " ) = (h " ) by A12, TOPS_2:def 4;

      ((H " ) . hx) = x by A12, A14, FUNCT_1: 34;

      hence contradiction by A7, A24, A19, A21, A23, A22;

    end;