brouwer3.miz



    begin

    reserve x,X for set,

n,m,i for Nat,

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

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

r,s for Real;

    

     Lm1: for V be Subset of ( TopSpaceMetr ( Euclid n)) holds V is open implies for e be Point of ( Euclid n) st e in V holds ex r be Real st r > 0 & ( OpenHypercube (e,r)) c= V

    proof

      let V be Subset of ( TopSpaceMetr ( Euclid n));

      assume

       A1: V is open;

      let e be Point of ( Euclid n);

      assume e in V;

      then

      consider r be Real such that

       A2: r > 0 and

       A3: ( Ball (e,r)) c= V by A1, TOPMETR: 15;

      per cases ;

        suppose

         A4: n <> 0 ;

        ( OpenHypercube (e,(r / ( sqrt n)))) c= ( Ball (e,r)) by A4, EUCLID_9: 17;

        hence thesis by A3, XBOOLE_1: 1, A4, A2;

      end;

        suppose

         A6: n = 0 ;

        set TR = ( TOP-REAL 0 ), Z = ( 0. TR);

        

         A9: ( Ball (e,r)) = {} or ( Ball (e,r)) = {Z} by EUCLID: 77, ZFMISC_1: 33, A6;

        the carrier of ( TopSpaceMetr ( Euclid 0 )) = the carrier of ( Euclid 0 ) by TOPMETR: 12;

        then ( OpenHypercube (e,1)) = {Z} by EUCLID: 77, ZFMISC_1: 33, A6;

        hence thesis by A9, A2, A3;

      end;

    end;

    

     Lm2: r > 0 implies ( cl_Ball (p,r)) is non boundary compact

    proof

      assume

       A1: r > 0 ;

      ( Ball (p,r)) c= ( Int ( cl_Ball (p,r))) by TOPREAL9: 16, TOPS_1: 24;

      hence thesis by A1;

    end;

    registration

      let X;

      let n;

      cluster -> FinSequence-yielding for Function of X, ( TOP-REAL n);

      coherence

      proof

        let F be Function of X, ( TOP-REAL n);

        now

          let x be object;

          assume x in ( dom F);

          then (F . x) in ( rng F) by FUNCT_1:def 3;

          hence (F . x) is FinSequence;

        end;

        hence thesis by PRE_POLY:def 3;

      end;

    end

    definition

      let X, n, m;

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

      let g be Function of X, ( TOP-REAL m);

      :: original: ^^

      redefine

      func f ^^ g -> Function of X, ( TOP-REAL (n + m)) ;

      coherence

      proof

        set fg = (f ^^ g);

        

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

        

         A2: ( dom f) = X by FUNCT_2:def 1;

        then

         A3: ( dom fg) = (X /\ X) by A1, PRE_POLY:def 4;

        ( rng fg) c= the carrier of ( TOP-REAL (n + m))

        proof

          let y be object;

          assume y in ( rng fg);

          then

          consider x be object such that

           A4: x in ( dom fg) and

           A5: (fg . x) = y by FUNCT_1:def 3;

          (g . x) in ( rng g) by A1, A4, A3, FUNCT_1:def 3;

          then

          reconsider gx = (g . x) as Point of ( TOP-REAL m);

          (f . x) in ( rng f) by A2, A4, A3, FUNCT_1:def 3;

          then

          reconsider fx = (f . x) as Point of ( TOP-REAL n);

          ( rng (fx ^ gx)) c= REAL ;

          then

           A7: (fx ^ gx) is FinSequence of REAL by FINSEQ_1:def 4;

          

           Z: ( len (fx ^ gx)) = (n + m) by CARD_1:def 7;

          (fg . x) = (fx ^ gx) by PRE_POLY:def 4, A4;

          hence thesis by A5, Z, A7, TOPREAL7: 17;

        end;

        hence thesis by A3, FUNCT_2: 2;

      end;

    end

    registration

      let T be TopSpace;

      let n, m;

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

      let g be continuous Function of T, ( TOP-REAL m);

      cluster (f ^^ g) -> continuous;

      coherence

      proof

        set fg = (f ^^ g);

        set Tn = ( TOP-REAL n), Tm = ( TOP-REAL m), Tnm = ( TOP-REAL (n + m));

        

         A1: ( [#] ( TOP-REAL n)) = the carrier of ( TOP-REAL n);

        

         A2: the TopStruct of ( TOP-REAL (n + m)) = ( TopSpaceMetr ( Euclid (n + m))) by EUCLID:def 8;

        

         A3: the TopStruct of ( TOP-REAL m) = ( TopSpaceMetr ( Euclid m)) by EUCLID:def 8;

        

         A4: ( [#] ( TOP-REAL m)) = the carrier of ( TOP-REAL m);

        

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

         A6:

        now

          let P be Subset of ( TOP-REAL (n + m));

          assume P is open;

          then P in the topology of ( TopSpaceMetr ( Euclid (n + m))) by A2, PRE_TOPC:def 2;

          then

          reconsider p = P as open Subset of ( TopSpaceMetr ( Euclid (n + m))) by PRE_TOPC:def 2;

          for x holds x in (fg " P) iff ex Q be Subset of T st Q is open & Q c= (fg " P) & x in Q

          proof

            let y be set;

            hereby

              assume

               A7: y in (fg " P);

              then

               A8: y in ( dom fg) by FUNCT_1:def 7;

              (fg . y) in p by A7, FUNCT_1:def 7;

              then

              reconsider e = (fg . y) as Point of ( Euclid (n + m)) by EUCLID: 67;

              ( rng e) c= REAL ;

              then

               A9: e is FinSequence of REAL by FINSEQ_1:def 4;

              

               A10: ( dom fg) = (( dom f) /\ ( dom g)) by PRE_POLY:def 4;

              then

               A11: y in ( dom f) by A8, XBOOLE_0:def 4;

              then (f . y) in ( rng f) by FUNCT_1:def 3;

              then

              reconsider fy = (f . y) as Point of ( TOP-REAL n);

              

               A12: y in ( dom g) by A10, A8, XBOOLE_0:def 4;

              then (g . y) in ( rng g) by FUNCT_1:def 3;

              then

              reconsider gy = (g . y) as Point of ( TOP-REAL m);

              ( len e) = (n + m) by CARD_1:def 7;

              then

              consider e1,e2 be FinSequence of REAL such that

               A13: ( len e1) = n and

               A14: ( len e2) = m and

               A15: e = (e1 ^ e2) by FINSEQ_2: 23, A9;

              reconsider e2 as Point of ( Euclid m) by TOPREAL7: 16, A14;

              reconsider e1 as Point of ( Euclid n) by TOPREAL7: 16, A13;

              

               A16: (fy ^ gy) = (e1 ^ e2) by PRE_POLY:def 4, A8, A15;

              (fg . y) in p by A7, FUNCT_1:def 7;

              then

              consider r be Real such that

               A17: r > 0 and

               A18: ( OpenHypercube (e,r)) c= p by Lm1;

              ( OpenHypercube (e2,r)) in the topology of ( TOP-REAL m) by A3, PRE_TOPC:def 2;

              then

              reconsider O2 = ( OpenHypercube (e2,r)) as open Subset of ( TOP-REAL m) by PRE_TOPC:def 2;

              

               A19: (g " O2) is open by A4, TOPS_2: 43;

              ( OpenHypercube (e1,r)) in the topology of ( TOP-REAL n) by A5, PRE_TOPC:def 2;

              then

              reconsider O1 = ( OpenHypercube (e1,r)) as open Subset of ( TOP-REAL n) by PRE_TOPC:def 2;

              take Q = ((f " O1) /\ (g " O2));

              

               A20: O2 = ( product ( Intervals (e2,r))) by EUCLID_9:def 4;

              (f " O1) is open by A1, TOPS_2: 43;

              hence Q is open by A19;

              

               A21: ( OpenHypercube (e,r)) = ( product ( Intervals (e,r))) by EUCLID_9:def 4;

              ( len fy) = n by CARD_1:def 7;

              then ( dom fy) = ( dom e1) by A13, FINSEQ_3: 29;

              

              then

               A22: fy = ((e1 ^ e2) | ( dom e1)) by FINSEQ_1: 21, A16

              .= e1 by FINSEQ_1: 21;

              then gy = e2 by A16, FINSEQ_1: 33;

              then gy in O2 by EUCLID_9: 11, A17;

              then

               A23: y in (g " O2) by A12, FUNCT_1:def 7;

              

               A24: O1 = ( product ( Intervals (e1,r))) by EUCLID_9:def 4;

              thus Q c= (fg " P)

              proof

                let x be object;

                assume

                 A25: x in Q;

                then

                 A26: x in (f " O1) by XBOOLE_0:def 4;

                then

                 A27: (f . x) in O1 by FUNCT_1:def 7;

                then

                reconsider fx = (f . x) as Point of ( TOP-REAL n);

                

                 A28: x in (g " O2) by A25, XBOOLE_0:def 4;

                then

                 A29: x in ( dom g) by FUNCT_1:def 7;

                

                 A30: (g . x) in O2 by A28, FUNCT_1:def 7;

                then

                reconsider gx = (g . x) as Point of ( TOP-REAL m);

                

                 A31: (fx ^ gx) in ( product (( Intervals (e1,r)) ^ ( Intervals (e2,r)))) by A24, A20, A27, A30, RLAFFIN3: 2;

                x in ( dom f) by A26, FUNCT_1:def 7;

                then

                 A32: x in ( dom fg) by A29, A10, XBOOLE_0:def 4;

                then (fg . x) = (fx ^ gx) by PRE_POLY:def 4;

                then (fg . x) in ( OpenHypercube (e,r)) by A31, A15, RLAFFIN3: 1, A21;

                hence thesis by A18, A32, FUNCT_1:def 7;

              end;

              fy in O1 by A22, EUCLID_9: 11, A17;

              then y in (f " O1) by A11, FUNCT_1:def 7;

              hence y in Q by A23, XBOOLE_0:def 4;

            end;

            thus thesis;

          end;

          hence (fg " P) is open by TOPS_1: 25;

        end;

        ( [#] ( TOP-REAL (n + m))) = the carrier of ( TOP-REAL (n + m));

        hence thesis by A6, TOPS_2: 43;

      end;

    end

    definition

      let f be real-valued Function;

      :: BROUWER3:def1

      func |[f]| -> Function means

      : Def1: ( dom it ) = ( dom f) & for x be object st x in ( dom it ) holds (it . x) = |[(f . x)]|;

      existence

      proof

        deffunc F( object) = |[(f . $1)]|;

        ex F be Function st ( dom F) = ( dom f) & for x be object st x in ( dom f) holds (F . x) = F(x) from FUNCT_1:sch 3;

        hence thesis;

      end;

      uniqueness

      proof

        let F1,F2 be Function such that

         A1: ( dom F1) = ( dom f) and

         A2: for x be object st x in ( dom F1) holds (F1 . x) = |[(f . x)]| and

         A3: ( dom F2) = ( dom f) and

         A4: for x be object st x in ( dom F2) holds (F2 . x) = |[(f . x)]|;

        now

          let x;

          assume

           A5: x in ( dom F1);

          

          hence (F1 . x) = |[(f . x)]| by A2

          .= (F2 . x) by A1, A3, A4, A5;

        end;

        hence thesis by A1, A3;

      end;

    end

    registration

      let f be real-valued Function;

      cluster |[f]| -> the carrier of ( TOP-REAL 1) -valued;

      coherence

      proof

        set F = |[f]|;

        ( rng F) c= the carrier of ( TOP-REAL 1)

        proof

          let y be object;

          assume y in ( rng F);

          then

          consider x be object such that

           A1: x in ( dom F) and

           A2: (F . x) = y by FUNCT_1:def 3;

          (F . x) = |[(f . x)]| by A1, Def1;

          hence thesis by A2;

        end;

        hence thesis by RELAT_1:def 19;

      end;

    end

    definition

      let X;

      let Y be non empty real-membered set;

      let f be Function of X, Y;

      :: original: |[

      redefine

      func |[f]| -> Function of X, ( TOP-REAL 1) ;

      coherence

      proof

        ( dom f) = X by FUNCT_2:def 1;

        then

         A1: ( dom |[f]|) = X by Def1;

        ( rng |[f]|) c= the carrier of ( TOP-REAL 1);

        hence thesis by A1, FUNCT_2: 2;

      end;

    end

    registration

      let T be non empty TopSpace;

      let f be continuous Function of T, R^1 ;

      cluster |[f]| -> continuous;

      coherence

      proof

        defpred P[ Element of ( TOP-REAL 1), object] means $2 = ($1 /. 1);

        

         A1: for x be Element of ( TOP-REAL 1) holds ex y be Element of R^1 st P[x, y] by TOPMETR: 17;

        consider P be Function of ( TOP-REAL 1), R^1 such that

         A2: for x be Element of ( TOP-REAL 1) holds P[x, (P . x)] from FUNCT_2:sch 3( A1);

        

         A3: P is being_homeomorphism by A2, JORDAN2B: 28;

        then

        reconsider PP = (P " ) as continuous Function of R^1 , ( TOP-REAL 1) by TOPS_2:def 5;

        

         A4: ( dom PP) = the carrier of R^1 by FUNCT_2:def 1;

        

         A5: ( dom |[f]|) = ( dom f) by Def1;

        reconsider PPf = (PP * f) as Function of T, ( TOP-REAL 1);

        

         A6: ( dom f) = the carrier of T by FUNCT_2:def 1;

         A7:

        now

          

           A8: PP = (P qua Function " ) by A3, TOPS_2:def 4;

          let x be object;

          

           A9: ( rng P) = ( [#] R^1 ) by A3, TOPS_2:def 5;

          assume

           A10: x in ( dom PPf);

          then

           A11: (PPf . x) = (PP . (f . x)) by FUNCT_1: 12;

          (PPf . x) in ( rng PPf) by A10, FUNCT_1:def 3;

          then

          reconsider PPfx = (PPf . x) as Point of ( TOP-REAL 1);

          (f . x) in ( dom PP) by A10, FUNCT_1: 11;

          then (P . (PPf . x)) = (f . x) by A11, A8, A3, A9, FUNCT_1: 35;

          then

           A12: (PPfx /. 1) = (f . x) by A2;

          consider R be Real such that

           B: <*R*> = PPfx by JORDAN2B: 20;

          R is Element of REAL by XREAL_0:def 1;

          then R = (f . x) by A12, B, FINSEQ_4: 16;

          hence (PPf . x) = ( |[f]| . x) by B, A10, A6, A5, Def1;

        end;

        ( rng f) c= the carrier of R^1 by RELAT_1:def 19;

        hence thesis by A4, A7, RELAT_1: 27, A5, FUNCT_1: 2;

      end;

    end

    registration

      let T be non empty TopSpace;

      let f be continuous RealMap of T;

      cluster |[f]| -> continuous;

      coherence

      proof

        reconsider F = f as Function of T, R^1 by TOPMETR: 17;

        F is continuous by JORDAN5A: 27;

        hence thesis;

      end;

    end

    begin

    reserve N for non zero Nat,

u,t for Point of ( TOP-REAL (N + 1));

    theorem :: BROUWER3:1

    

     Th1: for F be Element of (N -tuples_on ( Funcs (the carrier of ( TOP-REAL (N + 1)),the carrier of R^1 ))) st for i st i in ( dom F) holds (F . i) = ( PROJ ((N + 1),i)) holds (for t holds ( <:F:> . t) = (t | N)) & for Sp,Sn be Subset of ( TOP-REAL (N + 1)) st Sp = { u : (u . (N + 1)) >= 0 & |.u.| = 1 } & Sn = { t : (t . (N + 1)) <= 0 & |.t.| = 1 } holds ( <:F:> .: Sp) = ( cl_Ball (( 0. ( TOP-REAL N)),1)) & ( <:F:> .: Sn) = ( cl_Ball (( 0. ( TOP-REAL N)),1)) & ( <:F:> .: (Sp /\ Sn)) = ( Sphere (( 0. ( TOP-REAL N)),1)) & (for H be Function of (( TOP-REAL (N + 1)) | Sp), ( Tdisk (( 0. ( TOP-REAL N)),1)) st H = ( <:F:> | Sp) holds H is being_homeomorphism) & for H be Function of (( TOP-REAL (N + 1)) | Sn), ( Tdisk (( 0. ( TOP-REAL N)),1)) st H = ( <:F:> | Sn) holds H is being_homeomorphism

    proof

      set N1 = (N + 1), Tn1 = ( TOP-REAL N1), Tn = ( TOP-REAL N);

      

       N: N in NAT by ORDINAL1:def 12;

      set N0 = (( 0* N1) +* (N1,( - 1)));

      

       A1: ( len N0) = N1 by CARD_1:def 7;

      ( rng N0) c= REAL ;

      then N0 is FinSequence of REAL by FINSEQ_1:def 4;

      then

      reconsider N0 as Point of Tn1 by A1, TOPREAL7: 17;

      set NF = (N NormF ), NNF = (NF (#) NF);

      reconsider ONE = 1 as Element of NAT ;

      set TD = ( Tdisk (( 0. ( TOP-REAL N)),1));

      

       A2: ( [#] TD) = ( cl_Ball (( 0. Tn),1)) by PRE_TOPC:def 5;

      reconsider NNF as Function of Tn, R^1 by TOPMETR: 17;

      reconsider mNNF = ( - NNF) as Function of Tn, R^1 by TOPMETR: 17;

      reconsider m1 = (1 + mNNF) as Function of Tn, R^1 by TOPMETR: 17;

      1 <= N1 by NAT_1: 11;

      then

       A3: N1 in ( Seg N1);

      ( dom ( 0* N1)) = ( Seg N1);

      then

       A4: (N0 . N1) = ( - 1) by A3, FUNCT_7: 31;

      let F be Element of (N -tuples_on ( Funcs (the carrier of Tn1,the carrier of R^1 )));

      set FF = <:F:>;

      

       A5: N < N1 by NAT_1: 13;

      ( len F) = N by CARD_1:def 7;

      then

       A6: ( dom F) = ( Seg N) by FINSEQ_1:def 3;

      assume

       A7: for i st i in ( dom F) holds (F . i) = ( PROJ (N1,i));

      thus

       A8: for t holds ( <:F:> . t) = (t | N)

      proof

        let s be Point of Tn1;

        reconsider Fs = (FF . s) as Point of Tn;

        

         A9: ( len Fs) = N by CARD_1:def 7;

        

         A10: ( len s) = N1 by CARD_1:def 7;

        now

          let i;

          assume that

           A12: 1 <= i and

           A13: i <= N;

          

           A14: (Fs . i) = ((F . i) . s) by TIETZE_2: 1;

          i < N1 by A13, NAT_1: 13;

          then

           A15: i in ( dom s) by A10, A12, FINSEQ_3: 25;

          (F . i) = ( PROJ (N1,i)) by A12, A13, FINSEQ_1: 1, A7, A6;

          then

           A16: (Fs . i) = (s /. i) by A14, TOPREALC:def 6;

          ((s | N) . i) = (s . i) by A12, A13, FINSEQ_1: 1, FUNCT_1: 49;

          hence (Fs . i) = ((s | N) . i) by A16, A15, PARTFUN1:def 6;

        end;

        hence thesis by A9, A10, FINSEQ_1: 59, A5;

      end;

      let Sp,Sn be Subset of Tn1;

      assume

       A17: Sp = { u : (u . N1) >= 0 & |.u.| = 1 };

      

       A18: ( dom FF) = the carrier of Tn1 by FUNCT_2:def 1;

      

       A19: ( cl_Ball (( 0. Tn),1)) c= (FF .: Sp)

      proof

        let x be object;

        assume

         A20: x in ( cl_Ball (( 0. Tn),1));

        then

        reconsider s = x as Element of ( REAL N) by EUCLID: 22;

        set sq = ( sqrt (1 - ( |.s.| ^2 ))), s1 = (s ^ <*sq*>);

         |.s.| <= 1 by TOPREAL9: 11, A20;

        then ( |.s.| * |.s.|) <= (1 * 1) by XREAL_1: 66;

        then

         A21: (1 - ( |.s.| ^2 )) >= (( |.s.| ^2 ) - ( |.s.| ^2 )) by XREAL_1: 13;

        then

         A22: (sq ^2 ) = (1 - ( |.s.| ^2 )) by SQUARE_1:def 2;

        

         A23: ( len s1) = (( len s) + 1) by FINSEQ_2: 16;

        

         A24: ( len s) = N by CARD_1:def 7;

        s1 is FinSequence of REAL by RVSUM_1: 145;

        then

        reconsider s1 as Element of ( REAL N1) by A23, A24, FINSEQ_2: 92;

        ((s1 | N) ^ <*(s1 . N1)*>) = s1 by FINSEQ_3: 55, A23, CARD_1:def 7;

        then

         A25: (s1 | N) = s by FINSEQ_2: 17;

        reconsider ss1 = s1 as Point of Tn1 by EUCLID: 22;

        

         A26: (s1 . N1) = sq by A24, FINSEQ_1: 42;

        

        then ( |.s1.| ^2 ) = (( |.s.| ^2 ) + (sq ^2 )) by A25, REAL_NS1: 10

        .= (1 ^2 ) by A22;

        then |.s1.| = 1 or |.s1.| = ( - 1) by SQUARE_1: 40;

        then

         A27: ss1 in Sp by A17, A26, A21;

        (FF . ss1) = s by A25, A8;

        hence thesis by A27, A18, FUNCT_1:def 6;

      end;

      assume

       A28: Sn = { t : (t . N1) <= 0 & |.t.| = 1 };

      

       A29: ( cl_Ball (( 0. Tn),1)) c= (FF .: Sn)

      proof

        let x be object;

        assume

         A30: x in ( cl_Ball (( 0. Tn),1));

        then

        reconsider s = x as Element of ( REAL N) by EUCLID: 22;

         |.s.| <= 1 by TOPREAL9: 11, A30;

        then ( |.s.| * |.s.|) <= (1 * 1) by XREAL_1: 66;

        then

         A31: (1 - ( |.s.| ^2 )) >= (( |.s.| ^2 ) - ( |.s.| ^2 )) by XREAL_1: 13;

        set sq = ( - ( sqrt (1 - ( |.s.| ^2 )))), s1 = (s ^ <*sq*>);

        

         A32: ( len s1) = (( len s) + 1) by FINSEQ_2: 16;

        (sq ^2 ) = (( - sq) ^2 );

        then

         A33: (sq ^2 ) = (1 - ( |.s.| ^2 )) by SQUARE_1:def 2, A31;

        

         A34: ( len s) = N by CARD_1:def 7;

        s1 is FinSequence of REAL by RVSUM_1: 145;

        then

        reconsider s1 as Element of ( REAL N1) by A32, A34, FINSEQ_2: 92;

        ((s1 | N) ^ <*(s1 . N1)*>) = s1 by FINSEQ_3: 55, A32, CARD_1:def 7;

        then

         A35: (s1 | N) = s by FINSEQ_2: 17;

        reconsider ss1 = s1 as Point of Tn1 by EUCLID: 22;

        

         A36: (s1 . N1) = sq by A34, FINSEQ_1: 42;

        

        then ( |.s1.| ^2 ) = (( |.s.| ^2 ) + (sq ^2 )) by A35, REAL_NS1: 10

        .= (1 ^2 ) by A33;

        then |.s1.| = 1 or |.s1.| = ( - 1) by SQUARE_1: 40;

        then

         A37: ss1 in Sn by A28, A36, A31;

        (FF . ss1) = s by A35, A8;

        hence thesis by A37, A18, FUNCT_1:def 6;

      end;

      

       A38: ( Sphere (( 0. Tn),1)) c= (FF .: (Sn /\ Sp))

      proof

        reconsider Z = 0 as Element of REAL by XREAL_0:def 1;

        let x be object;

        assume

         A39: x in ( Sphere (( 0. Tn),1));

        then

        reconsider s = x as Element of ( REAL N) by EUCLID: 22;

        

         A40: |.s.| = 1 by TOPREAL9: 12, A39;

        set s1 = (s ^ <*Z*>);

        

         A41: ( len s) = N by CARD_1:def 7;

        

         A42: ( len s1) = (( len s) + 1) by FINSEQ_2: 16;

        then

        reconsider s1 as Element of ( REAL N1) by A41, FINSEQ_2: 92;

        

         A43: (s1 . N1) = 0 by A41, FINSEQ_1: 42;

        reconsider ss1 = s1 as Point of Tn1 by EUCLID: 22;

        ((s1 | N) ^ <*(s1 . N1)*>) = s1 by FINSEQ_3: 55, A42, CARD_1:def 7;

        then

         A44: (s1 | N) = s by FINSEQ_2: 17;

        then ( |.s1.| ^2 ) = (( |.s.| ^2 ) + ( 0 ^2 )) by A43, REAL_NS1: 10;

        then

         A45: |.s1.| = 1 or |.s1.| = ( - 1) by A40, SQUARE_1: 40;

        then

         A46: ss1 in Sn by A28, A43;

        ss1 in Sp by A45, A17, A43;

        then

         A47: ss1 in (Sp /\ Sn) by A46, XBOOLE_0:def 4;

        (FF . ss1) = s by A44, A8;

        hence thesis by A47, A18, FUNCT_1:def 6;

      end;

      

       A48: (FF .: Sp) c= ( cl_Ball (( 0. Tn),1))

      proof

        let y be object;

        assume y in (FF .: Sp);

        then

        consider x be object such that x in ( dom FF) and

         A49: x in Sp and

         A50: (FF . x) = y by FUNCT_1:def 6;

        consider s be Point of Tn1 such that

         A51: s = x and (s . N1) >= 0 and

         A52: |.s.| = 1 by A49, A17;

        reconsider ss = s as Element of ( REAL N1) by EUCLID: 22;

        ( len ss) = N1 by CARD_1:def 7;

        then ( len (ss | N)) = N by A5, FINSEQ_1: 59;

        then

        reconsider sN = (ss | N) as Point of Tn by TOPREAL7: 17;

        ( |.ss.| ^2 ) = (( |.sN.| ^2 ) + ((s . N1) ^2 )) by REAL_NS1: 10;

        then ( |.ss.| ^2 ) >= (( |.sN.| ^2 ) + 0 ) by XREAL_1: 6;

        then

         A53: 1 >= |.sN.| by SQUARE_1: 16, A52;

        (sN - ( 0. Tn)) = sN by RLVECT_1: 13;

        then sN in ( cl_Ball (( 0. Tn),1)) by A53;

        hence thesis by A8, A51, A50;

      end;

      hence (FF .: Sp) = ( cl_Ball (( 0. Tn),1)) by A19;

      

       A54: (FF .: Sn) c= ( cl_Ball (( 0. Tn),1))

      proof

        let y be object;

        assume y in (FF .: Sn);

        then

        consider x be object such that x in ( dom FF) and

         A55: x in Sn and

         A56: (FF . x) = y by FUNCT_1:def 6;

        consider s be Point of Tn1 such that

         A57: s = x and (s . N1) <= 0 and

         A58: |.s.| = 1 by A55, A28;

        reconsider ss = s as Element of ( REAL N1) by EUCLID: 22;

        ( len ss) = N1 by CARD_1:def 7;

        then ( len (ss | N)) = N by A5, FINSEQ_1: 59;

        then

        reconsider sN = (ss | N) as Point of Tn by TOPREAL7: 17;

        ( |.ss.| ^2 ) = (( |.sN.| ^2 ) + ((s . N1) ^2 )) by REAL_NS1: 10;

        then ( |.ss.| ^2 ) >= (( |.sN.| ^2 ) + 0 ) by XREAL_1: 6;

        then

         A59: 1 >= |.sN.| by SQUARE_1: 16, A58;

        (sN - ( 0. Tn)) = sN by RLVECT_1: 13;

        then sN in ( cl_Ball (( 0. Tn),1)) by A59;

        hence thesis by A8, A57, A56;

      end;

      hence (FF .: Sn) = ( cl_Ball (( 0. Tn),1)) by A29;

      (FF .: (Sn /\ Sp)) c= ( Sphere (( 0. Tn),1))

      proof

        let y be object;

        assume y in (FF .: (Sn /\ Sp));

        then

        consider x be object such that x in ( dom FF) and

         A60: x in (Sn /\ Sp) and

         A61: (FF . x) = y by FUNCT_1:def 6;

        x in Sn by A60, XBOOLE_0:def 4;

        then

        consider s be Point of Tn1 such that

         A62: s = x and

         A63: (s . N1) <= 0 and

         A64: |.s.| = 1 by A28;

        reconsider ss = s as Element of ( REAL N1) by EUCLID: 22;

        ( len ss) = N1 by CARD_1:def 7;

        then ( len (ss | N)) = N by A5, FINSEQ_1: 59;

        then

        reconsider sN = (ss | N) as Point of Tn by TOPREAL7: 17;

        

         A65: ( |.ss.| ^2 ) = (( |.sN.| ^2 ) + ((s . N1) ^2 )) by REAL_NS1: 10;

        x in Sp by A60, XBOOLE_0:def 4;

        then ex s1 be Point of Tn1 st s1 = x & (s1 . N1) >= 0 & |.s1.| = 1 by A17;

        then ((s . N1) ^2 ) = 0 by A62, A63;

        then

         A66: |.ss.| = |.sN.| or |.ss.| = ( - |.sN.|) by A65, SQUARE_1: 40;

        (sN - ( 0. Tn)) = sN by RLVECT_1: 13;

        then sN in ( Sphere (( 0. Tn),1)) by A66, A64;

        hence thesis by A8, A62, A61;

      end;

      hence (FF .: (Sp /\ Sn)) = ( Sphere (( 0. Tn),1)) by A38;

      thus for H be Function of (( TOP-REAL (N + 1)) | Sp), ( Tdisk (( 0. ( TOP-REAL N)),1)) st H = ( <:F:> | Sp) holds H is being_homeomorphism

      proof

        set N0 = (( 0* N1) +* (N1,1));

        ( rng N0) c= REAL ;

        then

         W: N0 is FinSequence of REAL by FINSEQ_1:def 4;

        ( len N0) = N1 by CARD_1:def 7;

        then

        reconsider N0 as Point of Tn1 by W, TOPREAL7: 17;

        reconsider ONE = 1 as Element of NAT ;

        set NF = (N NormF ), NNF = (NF (#) NF);

        

         A67: ( [#] TD) = ( cl_Ball (( 0. Tn),1)) by PRE_TOPC:def 5;

        reconsider NNF as Function of Tn, R^1 by TOPMETR: 17;

        reconsider mNNF = ( - NNF) as Function of Tn, R^1 by TOPMETR: 17;

        reconsider m1 = (1 + mNNF) as Function of Tn, R^1 by TOPMETR: 17;

        1 <= N1 by NAT_1: 11;

        then

         A68: N1 in ( Seg N1);

        

        then

         A69: |.N0.| = |.1.| by TOPREALC: 13

        .= 1 by ABSVALUE:def 1;

        let H be Function of (Tn1 | Sp), TD such that

         A70: H = (FF | Sp);

        

         A71: ( dom H) = ( [#] (Tn1 | Sp)) by FUNCT_2:def 1;

        

         A72: ( [#] (Tn1 | Sp)) = Sp by PRE_TOPC:def 5;

        

        then

         A73: ( rng H) = ((FF | Sp) .: Sp) by A71, A70, RELAT_1: 113

        .= ( cl_Ball (( 0. Tn),1)) by A19, A48, RELAT_1: 129;

        then

         A74: ( rng H) = ( [#] TD) by PRE_TOPC:def 5;

        

         A75: 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;

          assume

           A76: x1 in ( dom H);

          then

          consider s1 be Point of Tn1 such that

           A77: x1 = s1 and

           A78: (s1 . N1) >= 0 and

           A79: |.s1.| = 1 by A17, A71, A72;

          assume

           A80: x2 in ( dom H);

          then

          consider s2 be Point of Tn1 such that

           A81: x2 = s2 and

           A82: (s2 . N1) >= 0 and

           A83: |.s2.| = 1 by A17, A71, A72;

          reconsider s1, s2 as Element of ( REAL N1) by EUCLID: 22;

          

           A84: (1 ^2 ) = (( |.(s1 | N).| ^2 ) + ((s1 . N1) ^2 )) by REAL_NS1: 10, A79;

          

           A85: (H . x2) = (FF . x2) by A70, FUNCT_1: 47, A80;

          assume

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

          (H . x1) = (FF . x1) by A76, A70, FUNCT_1: 47;

          

          then

           A87: (s1 | N) = (FF . s2) by A85, A86, A8, A77, A81

          .= (s2 | N) by A8;

          then (1 ^2 ) = (( |.(s1 | N).| ^2 ) + ((s2 . N1) ^2 )) by REAL_NS1: 10, A83;

          then

           A88: (s1 . N1) = (s2 . N1) or (s1 . N1) = ( - (s2 . N1)) by A84, SQUARE_1: 40;

          

           A89: (s1 . N1) > 0 or (s1 . N1) = 0 by A78;

          

           A90: ( len s2) = N1 by CARD_1:def 7;

          ( len s1) = N1 by CARD_1:def 7;

          

          hence x1 = ((s1 | N) ^ <*(s1 . N1)*>) by FINSEQ_3: 55, A77

          .= x2 by FINSEQ_3: 55, A88, A89, A82, A90, A87, A81;

        end;

        then

         A91: H is one-to-one;

        set TD = ( Tdisk (( 0. Tn),1));

        set M = (m1 | TD);

        

         A92: ( dom M) = the carrier of TD by FUNCT_2:def 1;

        reconsider MM = M as continuous Function of TD, REAL by TOPMETR: 17, JORDAN5A: 27;

        

         A93: M = (m1 | the carrier of TD) by TMAP_1:def 4;

        

         A94: for p be Point of Tn st p in the carrier of TD holds (MM . p) = (1 - ( |.p.| * |.p.|))

        proof

          let x be Point of Tn;

          (NF . x) = |.x.| by JGRAPH_4:def 1;

          then (NNF . x) = ( |.x.| * |.x.|) by VALUED_1: 5;

          then (mNNF . x) = ( - ( |.x.| * |.x.|)) by VALUED_1: 8;

          then (m1 . x) = (1 + ( - ( |.x.| * |.x.|))) by VALUED_1: 2;

          hence thesis by A93, FUNCT_1: 49;

        end;

        

         A95: the carrier of TD = ( cl_Ball (( 0. Tn),1)) by N, BROUWER: 3;

         A96:

        now

          let r be Real;

          assume r in ( rng MM);

          then

          consider x be object such that

           A97: x in ( dom MM) and

           A98: (MM . x) = r by FUNCT_1:def 3;

          reconsider x as Point of Tn by A92, A95, A97;

           |.x.| <= 1 by A97, A95, TOPREAL9: 11;

          then ( |.x.| * |.x.|) <= (1 * 1) by XREAL_1: 66;

          then (1 - ( |.x.| * |.x.|)) >= (1 - (1 * 1)) by XREAL_1: 10;

          hence r >= 0 by A94, A97, A98;

        end;

        then MM is nonnegative-yielding by PARTFUN3:def 4;

        then

        reconsider SQR = |[( sqrt MM)]| as continuous Function of TD, ( TOP-REAL 1);

        

         A99: ( dom ( sqrt MM)) = ( dom MM) by PARTFUN3:def 5;

        

         A100: ( rng ( id TD)) = the carrier of TD;

        ( dom ( id TD)) = the carrier of TD;

        then

        reconsider ID = ( id TD) as continuous Function of TD, Tn by A100, FUNCT_2: 2, A95, PRE_TOPC: 26;

        reconsider SQR as continuous Function of TD, ( TOP-REAL ONE);

        reconsider II = (ID ^^ SQR) as continuous Function of TD, ( TOP-REAL (N + ONE));

        reconsider II as continuous Function of TD, Tn1;

        

         A101: ( dom II) = the carrier of TD by FUNCT_2:def 1;

        

         A102: ( dom SQR) = ( dom ( sqrt MM)) by Def1;

        for y,x be object holds y in ( rng H) & x = (II . y) iff x in ( dom H) & y = (H . x)

        proof

          let y,x be object;

          hereby

            assume that

             A103: y in ( rng H) and

             A104: x = (II . y);

            reconsider p = y as Point of Tn by A103, A73;

            set p1 = (1 - ( |.p.| * |.p.|)), sp = ( sqrt p1), ssp = |[sp]|;

            

             A105: (ID . p) = p by A103, FUNCT_1: 17;

            

             A106: (MM . p) = (1 - ( |.p.| * |.p.|)) by A103, A94;

            then (( sqrt MM) . p) = sp by A103, A92, PARTFUN3:def 5, A99;

            then (SQR . p) = ssp by Def1, A99, A102, A103, A92;

            then

             A107: (II . p) = (p ^ ssp) by A103, A101, A105, PRE_POLY:def 4;

            (II . p) in ( rng II) by A103, A101, FUNCT_1:def 3;

            then

            reconsider IIp = (II . p) as Point of Tn1;

            (MM . p) in ( rng MM) by A103, A92, FUNCT_1:def 3;

            then

             A109: (MM . p) >= 0 by A96;

            

             A110: ( sqr ssp) = <*(sp ^2 )*> by RVSUM_1: 55

            .= <*(MM . p)*> by A109, SQUARE_1:def 2, A106;

            ( sqr IIp) = (( sqr p) ^ ( sqr ssp)) by RVSUM_1: 144, A107;

            

            then ( Sum ( sqr IIp)) = (( Sum ( sqr p)) + (MM . p)) by A110, RVSUM_1: 74

            .= (( |.p.| ^2 ) + (MM . p)) by TOPREAL9: 5

            .= 1 by A106;

            then

             A111: |.IIp.| = 1 by SQUARE_1: 18;

            

             A112: ( len p) = N by CARD_1:def 7;

            then (IIp . N1) = sp by A107, FINSEQ_1: 42;

            then

             A113: IIp in Sp by A106, A109, A17, A111;

            hence x in ( dom H) by A104, A71, PRE_TOPC:def 5;

            (FF . IIp) = (H . IIp) by A113, A71, A72, A70, FUNCT_1: 47;

            

            hence (H . x) = ((p ^ ssp) | N) by A8, A107, A104

            .= ((p ^ ssp) | ( dom p)) by A112, FINSEQ_1:def 3

            .= y by FINSEQ_1: 21;

          end;

          assume that

           A114: x in ( dom H) and

           A115: y = (H . x);

          consider p be Point of Tn1 such that

           A116: x = p and

           A117: (p . N1) >= 0 and

           A118: |.p.| = 1 by A114, A17, A71, A72;

          

           A119: (p | N) is FinSequence of REAL by RVSUM_1: 145;

          ( len p) = N1 by CARD_1:def 7;

          then ( len (p | N)) = N by NAT_1: 11, FINSEQ_1: 59;

          then

          reconsider pN = (p | N) as Point of Tn by A119, TOPREAL7: 17;

          

           A121: p = (pN ^ <*(p . N1)*>) by CARD_1:def 7, FINSEQ_3: 55;

          set p1 = (1 - ( |.pN.| * |.pN.|)), sp = ( sqrt p1), ssp = |[sp]|;

          

           A122: ( sqr <*(p . N1)*>) = <*((p . N1) ^2 )*> by RVSUM_1: 55;

          

           A123: (pN - ( 0. Tn)) = pN by VECTSP_1: 18;

          ( sqr p) = (( sqr pN) ^ ( sqr <*(p . N1)*>)) by A121, RVSUM_1: 144;

          

          then ( Sum ( sqr p)) = (( Sum ( sqr pN)) + ((p . N1) ^2 )) by RVSUM_1: 74, A122

          .= (( |.pN.| ^2 ) + ((p . N1) ^2 )) by TOPREAL9: 5;

          then

           A124: ( |.p.| ^2 ) = (( |.pN.| ^2 ) + ((p . N1) ^2 )) by TOPREAL9: 5;

          then ( |.p.| ^2 ) >= ( |.pN.| ^2 ) by XREAL_1: 38;

          then |.pN.| <= 1 by SQUARE_1: 47, A118;

          then

           A125: pN in ( rng H) by A123, A73;

          then (MM . pN) = (1 - ( |.pN.| * |.pN.|)) by A94;

          then (( sqrt MM) . pN) = sp by A125, A92, PARTFUN3:def 5, A99;

          then

           A126: (SQR . pN) = ssp by Def1, A99, A102, A125, A92;

          

           A127: (FF . p) = (p | N) by A8;

          hence y in ( rng H) by A125, A115, A116, A114, A70, FUNCT_1: 47;

          (ID . pN) = pN by A125, FUNCT_1: 17;

          then (II . pN) = (pN ^ ssp) by A125, A101, A126, PRE_POLY:def 4;

          then (II . pN) = p by A118, A124, A117, SQUARE_1:def 2, A121;

          hence x = (II . y) by A115, A116, A127, A114, A70, FUNCT_1: 47;

        end;

        then

         A128: (H qua Function " ) = II by A91, A101, A74, FUNCT_1: 32;

        ( dom ( 0* N1)) = ( Seg N1);

        then (N0 . N1) = 1 by A68, FUNCT_7: 31;

        then

         A129: N0 in Sp by A69, A17;

        for P be Subset of (Tn1 | Sp) holds P is open iff (H .: P) is open

        proof

          let P be Subset of (Tn1 | Sp);

          for i st i in ( dom F) holds for h be Function of Tn1, R^1 st h = (F . i) holds h is continuous

          proof

            let i such that

             A130: i in ( dom F);

            i <= N by A130, A6, FINSEQ_1: 1;

            then

             A131: i <= N1 by NAT_1: 13;

            let h be Function of Tn1, R^1 such that

             A132: h = (F . i);

            

             A133: h = ( PROJ (N1,i)) by A130, A132, A7;

            1 <= i by A130, A6, FINSEQ_1: 1;

            then i in ( Seg N1) by A131;

            hence thesis by A133, TOPREALC: 57;

          end;

          then

           A134: FF is continuous by TIETZE_2: 21;

          (FF | (Tn1 | Sp)) = (FF | Sp) by TMAP_1:def 4, A72;

          then

           A135: H is continuous by A134, A129, A70, PRE_TOPC: 27;

          hereby

            ( rng II) = ( dom H) by A128, A91, FUNCT_1: 33;

            then

            reconsider ii = II as Function of TD, (Tn1 | Sp) by FUNCT_2: 2, A101;

            assume

             A136: P is open;

            

             A137: ii is continuous by PRE_TOPC: 27;

            ( dom H) is non empty by A73, A71;

            then (ii " P) is open by A137, A71, A136, TOPS_2: 43;

            hence (H .: P) is open by A75, FUNCT_1:def 4, FUNCT_1: 84, A128;

          end;

          assume

           A138: (H .: P) is open;

          (H " (H .: P)) = P by A71, A75, FUNCT_1:def 4, FUNCT_1: 94;

          hence P is open by A138, TOPS_2: 43, A135, A67;

        end;

        hence thesis by A71, A74, A91, A129, TOPGRP_1: 25;

      end;

      let H be Function of (Tn1 | Sn), TD such that

       A139: H = (FF | Sn);

      

       A140: ( dom H) = ( [#] (Tn1 | Sn)) by FUNCT_2:def 1;

      

       A141: ( [#] (Tn1 | Sn)) = Sn by PRE_TOPC:def 5;

      

      then

       A142: ( rng H) = ((FF | Sn) .: Sn) by A140, A139, RELAT_1: 113

      .= ( cl_Ball (( 0. Tn),1)) by A29, A54, RELAT_1: 129;

      then

       A143: ( rng H) = ( [#] TD) by PRE_TOPC:def 5;

      

       A144: 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;

        assume

         A145: x1 in ( dom H);

        then

        consider s1 be Point of Tn1 such that

         A146: x1 = s1 and

         A147: (s1 . N1) <= 0 and

         A148: |.s1.| = 1 by A28, A140, A141;

        assume

         A149: x2 in ( dom H);

        then

        consider s2 be Point of Tn1 such that

         A150: x2 = s2 and

         A151: (s2 . N1) <= 0 and

         A152: |.s2.| = 1 by A28, A140, A141;

        reconsider s1, s2 as Element of ( REAL N1) by EUCLID: 22;

        

         A153: (1 ^2 ) = (( |.(s1 | N).| ^2 ) + ((s1 . N1) ^2 )) by REAL_NS1: 10, A148;

        

         A154: (H . x2) = (FF . x2) by A139, FUNCT_1: 47, A149;

        assume

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

        (H . x1) = (FF . x1) by A145, A139, FUNCT_1: 47;

        

        then

         A156: (s1 | N) = (FF . s2) by A154, A155, A8, A146, A150

        .= (s2 | N) by A8;

        then (1 ^2 ) = (( |.(s1 | N).| ^2 ) + ((s2 . N1) ^2 )) by REAL_NS1: 10, A152;

        then

         A157: (s1 . N1) = (s2 . N1) or (s1 . N1) = ( - (s2 . N1)) by A153, SQUARE_1: 40;

        

         A158: (s1 . N1) < 0 or (s1 . N1) = 0 by A147;

        

         A159: ( len s2) = N1 by CARD_1:def 7;

        ( len s1) = N1 by CARD_1:def 7;

        

        hence x1 = ((s1 | N) ^ <*(s1 . N1)*>) by FINSEQ_3: 55, A146

        .= x2 by FINSEQ_3: 55, A157, A158, A151, A159, A156, A150;

      end;

      then

       A160: H is one-to-one;

      set TD = ( Tdisk (( 0. Tn),1));

      set M = (m1 | TD);

      

       A161: ( dom M) = the carrier of TD by FUNCT_2:def 1;

      reconsider MM = M as continuous Function of TD, REAL by TOPMETR: 17, JORDAN5A: 27;

      reconsider Msqr = ( - ( sqrt MM)) as Function of TD, REAL ;

      

       A162: M = (m1 | the carrier of TD) by TMAP_1:def 4;

      

       A163: for p be Point of Tn st p in the carrier of TD holds (MM . p) = (1 - ( |.p.| * |.p.|))

      proof

        let x be Point of Tn;

        (NF . x) = |.x.| by JGRAPH_4:def 1;

        then (NNF . x) = ( |.x.| * |.x.|) by VALUED_1: 5;

        then (mNNF . x) = ( - ( |.x.| * |.x.|)) by VALUED_1: 8;

        then (m1 . x) = (1 + ( - ( |.x.| * |.x.|))) by VALUED_1: 2;

        hence thesis by A162, FUNCT_1: 49;

      end;

      

       A164: the carrier of TD = ( cl_Ball (( 0. Tn),1)) by N, BROUWER: 3;

       A165:

      now

        let r be Real;

        assume r in ( rng MM);

        then

        consider x be object such that

         A166: x in ( dom MM) and

         A167: (MM . x) = r by FUNCT_1:def 3;

        reconsider x as Point of Tn by A161, A164, A166;

         |.x.| <= 1 by A166, A164, TOPREAL9: 11;

        then ( |.x.| * |.x.|) <= (1 * 1) by XREAL_1: 66;

        then (1 - ( |.x.| * |.x.|)) >= (1 - (1 * 1)) by XREAL_1: 10;

        hence r >= 0 by A163, A166, A167;

      end;

      then MM is nonnegative-yielding by PARTFUN3:def 4;

      then

      reconsider SQR = |[Msqr]| as continuous Function of TD, ( TOP-REAL 1);

      

       A168: ( dom ( sqrt MM)) = ( dom MM) by PARTFUN3:def 5;

      

       A169: ( rng ( id TD)) = the carrier of TD;

      ( dom ( id TD)) = the carrier of TD;

      then

      reconsider ID = ( id TD) as continuous Function of TD, Tn by A169, FUNCT_2: 2, A164, PRE_TOPC: 26;

      reconsider SQR as continuous Function of TD, ( TOP-REAL ONE);

      reconsider II = (ID ^^ SQR) as continuous Function of TD, ( TOP-REAL (N + ONE));

      reconsider II as continuous Function of TD, Tn1;

      

       A170: ( dom II) = the carrier of TD by FUNCT_2:def 1;

      ( dom ( - ( sqrt MM))) = ( dom ( sqrt MM)) by VALUED_1: 8;

      then

       A171: ( dom SQR) = ( dom ( sqrt MM)) by Def1;

      for y,x be object holds y in ( rng H) & x = (II . y) iff x in ( dom H) & y = (H . x)

      proof

        let y,x be object;

        hereby

          assume that

           A172: y in ( rng H) and

           A173: x = (II . y);

          reconsider p = y as Point of Tn by A172, A142;

          set p1 = (1 - ( |.p.| * |.p.|)), sp = ( sqrt p1), ssp = |[( - sp)]|;

          

           A174: (ID . p) = p by A172, FUNCT_1: 17;

          

           A175: (MM . p) = (1 - ( |.p.| * |.p.|)) by A172, A163;

          then (( sqrt MM) . p) = sp by A172, A161, PARTFUN3:def 5, A168;

          then (Msqr . p) = ( - sp) by VALUED_1: 8;

          then (SQR . p) = ssp by Def1, A168, A171, A172, A161;

          then

           A176: (II . p) = (p ^ ssp) by A172, A170, A174, PRE_POLY:def 4;

          (II . p) in ( rng II) by A172, A170, FUNCT_1:def 3;

          then

          reconsider IIp = (II . p) as Point of Tn1;

          (MM . p) in ( rng MM) by A172, A161, FUNCT_1:def 3;

          then

           A178: (MM . p) >= 0 by A165;

          

           A179: ( sqr IIp) = (( sqr p) ^ ( sqr ssp)) by RVSUM_1: 144, A176;

          (sp ^2 ) = (( - sp) ^2 );

          

          then ( sqr ssp) = <*(sp ^2 )*> by RVSUM_1: 55

          .= <*(MM . p)*> by A178, SQUARE_1:def 2, A175;

          

          then ( Sum ( sqr IIp)) = (( Sum ( sqr p)) + (MM . p)) by A179, RVSUM_1: 74

          .= (( |.p.| ^2 ) + (MM . p)) by TOPREAL9: 5

          .= 1 by A175;

          then

           A180: |.IIp.| = 1 by SQUARE_1: 18;

          

           A181: ( len p) = N by CARD_1:def 7;

          then (IIp . N1) = ( - sp) by A176, FINSEQ_1: 42;

          then

           A182: IIp in Sn by A175, A178, A28, A180;

          hence x in ( dom H) by A173, A140, PRE_TOPC:def 5;

          (FF . IIp) = (H . IIp) by A182, A140, A141, A139, FUNCT_1: 47;

          

          hence (H . x) = ((p ^ ssp) | N) by A8, A176, A173

          .= ((p ^ ssp) | ( dom p)) by A181, FINSEQ_1:def 3

          .= y by FINSEQ_1: 21;

        end;

        assume that

         A183: x in ( dom H) and

         A184: y = (H . x);

        consider p be Point of Tn1 such that

         A185: x = p and

         A186: (p . N1) <= 0 and

         A187: |.p.| = 1 by A183, A28, A140, A141;

        

         A188: (p | N) is FinSequence of REAL by RVSUM_1: 145;

        ( len p) = N1 by CARD_1:def 7;

        then ( len (p | N)) = N by NAT_1: 11, FINSEQ_1: 59;

        then

        reconsider pN = (p | N) as Point of Tn by A188, TOPREAL7: 17;

        

         A190: p = (pN ^ <*(p . N1)*>) by CARD_1:def 7, FINSEQ_3: 55;

        

         A191: ( sqr <*(p . N1)*>) = <*((p . N1) ^2 )*> by RVSUM_1: 55;

        ( sqr p) = (( sqr pN) ^ ( sqr <*(p . N1)*>)) by A190, RVSUM_1: 144;

        

        then

         A192: ( Sum ( sqr p)) = (( Sum ( sqr pN)) + ((p . N1) ^2 )) by RVSUM_1: 74, A191

        .= (( |.pN.| ^2 ) + ((p . N1) ^2 )) by TOPREAL9: 5;

        then ( |.p.| ^2 ) = (( |.pN.| ^2 ) + ((p . N1) ^2 )) by TOPREAL9: 5;

        then ( |.p.| ^2 ) >= ( |.pN.| ^2 ) by XREAL_1: 38;

        then

         A193: |.pN.| <= 1 by SQUARE_1: 47, A187;

        set p1 = (1 - ( |.pN.| * |.pN.|)), sp = ( sqrt p1), ssp = |[( - sp)]|;

        (pN - ( 0. Tn)) = pN by VECTSP_1: 18;

        then

         A194: pN in ( rng H) by A193, A142;

        then (MM . pN) = (1 - ( |.pN.| * |.pN.|)) by A163;

        then (( sqrt MM) . pN) = sp by A194, A161, PARTFUN3:def 5, A168;

        then (Msqr . pN) = ( - sp) by VALUED_1: 8;

        then

         A195: (SQR . pN) = ssp by Def1, A168, A171, A194, A161;

        (1 ^2 ) = (( |.pN.| ^2 ) + ((p . N1) ^2 )) by A187, A192, TOPREAL9: 5;

        then

         A196: ( - (p . N1)) = ( sqrt (1 - ( |.pN.| ^2 ))) by A186, SQUARE_1: 23;

        

         A197: (FF . p) = (p | N) by A8;

        hence y in ( rng H) by A194, A184, A185, A183, A139, FUNCT_1: 47;

        (ID . pN) = pN by A194, FUNCT_1: 17;

        then (II . pN) = (pN ^ ssp) by A194, A170, A195, PRE_POLY:def 4;

        hence x = (II . y) by A196, A190, A184, A185, A197, A183, A139, FUNCT_1: 47;

      end;

      then

       A198: (H qua Function " ) = II by A160, A170, A143, FUNCT_1: 32;

       |.N0.| = |.( - 1).| by TOPREALC: 13, A3

      .= ( - ( - 1)) by ABSVALUE:def 1;

      then

       A199: N0 in Sn by A28, A4;

      for P be Subset of (Tn1 | Sn) holds P is open iff (H .: P) is open

      proof

        let P be Subset of (Tn1 | Sn);

        for i st i in ( dom F) holds for h be Function of Tn1, R^1 st h = (F . i) holds h is continuous

        proof

          let i such that

           A200: i in ( dom F);

          i <= N by A200, A6, FINSEQ_1: 1;

          then

           A201: i <= N1 by NAT_1: 13;

          let h be Function of Tn1, R^1 such that

           A202: h = (F . i);

          

           A203: h = ( PROJ (N1,i)) by A200, A202, A7;

          1 <= i by A200, A6, FINSEQ_1: 1;

          then i in ( Seg N1) by A201;

          hence thesis by A203, TOPREALC: 57;

        end;

        then

         A204: FF is continuous by TIETZE_2: 21;

        (FF | (Tn1 | Sn)) = (FF | Sn) by TMAP_1:def 4, A141;

        then

         A205: H is continuous by A204, A199, A139, PRE_TOPC: 27;

        hereby

          ( rng II) = ( dom H) by A198, A160, FUNCT_1: 33;

          then

          reconsider ii = II as Function of TD, (Tn1 | Sn) by FUNCT_2: 2, A170;

          assume

           A206: P is open;

          

           A207: ii is continuous by PRE_TOPC: 27;

          ( dom H) is non empty by A142, A140;

          then (ii " P) is open by A207, A140, A206, TOPS_2: 43;

          hence (H .: P) is open by A144, FUNCT_1:def 4, FUNCT_1: 84, A198;

        end;

        assume

         A208: (H .: P) is open;

        (H " (H .: P)) = P by A140, A144, FUNCT_1:def 4, FUNCT_1: 94;

        hence P is open by A208, TOPS_2: 43, A205, A2;

      end;

      hence thesis by A140, A143, A160, A199, TOPGRP_1: 25;

    end;

    theorem :: BROUWER3:2

    

     Th2: for Sp,Sn be Subset of ( TOP-REAL n) st Sp = { s where s be Point of ( TOP-REAL n) : (s . n) >= 0 & |.s.| = 1 } & Sn = { t where t be Point of ( TOP-REAL n) : (t . n) <= 0 & |.t.| = 1 } holds Sp is closed & Sn is closed

    proof

      let Sp,Sn be Subset of ( TOP-REAL n) such that

       A1: Sp = { s where s be Point of ( TOP-REAL n) : (s . n) >= 0 & |.s.| = 1 } and

       A2: Sn = { t where t be Point of ( TOP-REAL n) : (t . n) <= 0 & |.t.| = 1 };

      set Tn = ( TOP-REAL n);

      per cases ;

        suppose

         A4: n = 0 ;

        

         A5: Sn = {}

        proof

          assume Sn <> {} ;

          then

          consider x be object such that

           A6: x in Sn by XBOOLE_0:def 1;

          ex p be Point of Tn st x = p & (p . n) <= 0 & |.p.| = 1 by A2, A6;

          hence contradiction by A4;

        end;

        Sp = {}

        proof

          assume Sp <> {} ;

          then

          consider x be object such that

           A7: x in Sp by XBOOLE_0:def 1;

          ex p be Point of Tn st x = p & (p . n) >= 0 & |.p.| = 1 by A1, A7;

          hence contradiction by A4;

        end;

        hence thesis by A5;

      end;

        suppose

         A8: n > 0 ;

        set P2 = { p where p be Point of Tn : 0 < (p /. n) };

        set P1 = { p where p be Point of Tn : 0 > (p /. n) };

        

         A9: P1 c= the carrier of Tn

        proof

          let x be object;

          assume x in P1;

          then ex p be Point of Tn st p = x & 0 > (p /. n);

          hence thesis;

        end;

        P2 c= the carrier of Tn

        proof

          let x be object;

          assume x in P2;

          then ex p be Point of Tn st p = x & 0 < (p /. n);

          hence thesis;

        end;

        then

        reconsider P1, P2 as Subset of Tn by A9;

        n in ( Seg n) by FINSEQ_1: 3, A8;

        then

        reconsider P1, P2 as open Subset of Tn by JORDAN2B: 13, JORDAN2B: 12;

        set S2 = ((P2 ` ) /\ ( Sphere (( 0. Tn),1)));

        

         A10: Sn c= S2

        proof

          let xx be object;

          assume xx in Sn;

          then

          consider p be Point of Tn such that

           A11: xx = p and

           A12: (p . n) <= 0 and

           A13: |.p.| = 1 by A2;

          (p - ( 0. Tn)) = p by RLVECT_1: 13;

          then

           A14: p in ( Sphere (( 0. Tn),1)) by A13;

          ( len p) = n by CARD_1:def 7;

          then

           A15: ( dom p) = ( Seg n) by FINSEQ_1:def 3;

          

           A16: not p in P2

          proof

            assume p in P2;

            then ex q be Point of Tn st p = q & 0 < (q /. n);

            hence thesis by A15, PARTFUN1:def 6, FINSEQ_1: 3, A8, A12;

          end;

          (P2 ` ) = (( [#] Tn) \ P2) by SUBSET_1:def 4;

          then p in (P2 ` ) by A16, XBOOLE_0:def 5;

          hence thesis by A14, XBOOLE_0:def 4, A11;

        end;

        

         A17: S2 c= Sn

        proof

          let xx be object;

          

           A18: (P2 ` ) = (( [#] Tn) \ P2) by SUBSET_1:def 4;

          assume

           A19: xx in S2;

          then

          reconsider p = xx as Point of Tn;

          ( len p) = n by CARD_1:def 7;

          then ( dom p) = ( Seg n) by FINSEQ_1:def 3;

          then

           A20: (p /. n) = (p . n) by PARTFUN1:def 6, FINSEQ_1: 3, A8;

          

           A21: p in (P2 ` ) by A19, XBOOLE_0:def 4;

          

           A22: (p . n) <= 0

          proof

            assume (p . n) > 0 ;

            then p in P2 by A20;

            hence thesis by A21, A18, XBOOLE_0:def 5;

          end;

          p in ( Sphere (( 0. Tn),1)) by A19, XBOOLE_0:def 4;

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

          hence thesis by A22, A2;

        end;

        set S1 = ((P1 ` ) /\ ( Sphere (( 0. Tn),1)));

        

         A23: S1 c= Sp

        proof

          let xx be object;

          

           A24: (P1 ` ) = (( [#] Tn) \ P1) by SUBSET_1:def 4;

          assume

           A25: xx in S1;

          then

          reconsider p = xx as Point of Tn;

          ( len p) = n by CARD_1:def 7;

          then ( dom p) = ( Seg n) by FINSEQ_1:def 3;

          then

           A26: (p /. n) = (p . n) by PARTFUN1:def 6, FINSEQ_1: 3, A8;

          

           A27: p in (P1 ` ) by A25, XBOOLE_0:def 4;

          

           A28: (p . n) >= 0

          proof

            assume (p . n) < 0 ;

            then p in P1 by A26;

            hence thesis by A27, A24, XBOOLE_0:def 5;

          end;

          p in ( Sphere (( 0. Tn),1)) by A25, XBOOLE_0:def 4;

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

          hence thesis by A28, A1;

        end;

        Sp c= S1

        proof

          let xx be object;

          assume xx in Sp;

          then

          consider p be Point of Tn such that

           A29: xx = p and

           A30: (p . n) >= 0 and

           A31: |.p.| = 1 by A1;

          (p - ( 0. Tn)) = p by RLVECT_1: 13;

          then

           A32: p in ( Sphere (( 0. Tn),1)) by A31;

          ( len p) = n by CARD_1:def 7;

          then

           A33: ( dom p) = ( Seg n) by FINSEQ_1:def 3;

          

           A34: not p in P1

          proof

            assume p in P1;

            then ex q be Point of Tn st p = q & 0 > (q /. n);

            hence thesis by A33, PARTFUN1:def 6, FINSEQ_1: 3, A8, A30;

          end;

          (P1 ` ) = (( [#] Tn) \ P1) by SUBSET_1:def 4;

          then p in (P1 ` ) by A34, XBOOLE_0:def 5;

          hence thesis by A32, XBOOLE_0:def 4, A29;

        end;

        hence thesis by A10, A17, XBOOLE_0:def 10, A23;

      end;

    end;

    theorem :: BROUWER3:3

    

     Th3: for TM be metrizable TopSpace st TM is finite-ind second-countable holds for F be closed Subset of TM st ( ind (F ` )) <= n holds for f be continuous Function of (TM | F), ( Tunit_circle (n + 1)) holds ex g be continuous Function of TM, ( Tunit_circle (n + 1)) st (g | F) = f

    proof

      defpred P[ Nat] means for TM be metrizable TopSpace st TM is finite-ind second-countable holds for F be closed Subset of TM st ( ind (F ` )) <= $1 holds for f be continuous Function of (TM | F), ( Tunit_circle ($1 + 1)) holds ex g be Function of TM, ( Tunit_circle ($1 + 1)) st g is continuous & (g | F) = f;

      let TM be metrizable TopSpace such that

       A1: TM is finite-ind second-countable;

      let F be closed Subset of TM such that

       A2: ( ind (F ` )) <= n;

      

       A3: for n st P[n] holds P[(n + 1)]

      proof

        let n;

        set n1 = (n + 1), n2 = (n1 + 1);

        assume

         A4: P[n];

        set Tn1 = ( TOP-REAL n1), Tn2 = ( TOP-REAL n2), U = ( Tunit_circle (n1 + 1));

        let TM be metrizable TopSpace;

        assume

         A5: TM is finite-ind second-countable;

        let F be closed Subset of TM such that

         A6: ( ind (F ` )) <= n1;

        let f be continuous Function of (TM | F), U;

        

         A7: ( [#] (TM | F)) = F by PRE_TOPC:def 5;

        

         A8: ( dom f) = the carrier of (TM | F) by FUNCT_2:def 1;

        

         A9: ( dom f) = the carrier of (TM | F) by FUNCT_2:def 1;

        

         A10: ( [#] (TM | F)) = F by PRE_TOPC:def 5;

        per cases ;

          suppose

           A11: F is empty;

          take g = (TM --> the Point of U);

          (g | F) = {} by A11;

          hence thesis by A11;

        end;

          suppose

           A12: F is non empty;

          set Sn = { p where p be Point of Tn2 : (p . n2) <= 0 & |.p.| = 1 };

          set Sp = { p where p be Point of Tn2 : (p . n2) >= 0 & |.p.| = 1 };

          

           A13: Sp c= the carrier of Tn2

          proof

            let x be object;

            assume x in Sp;

            then ex p be Point of Tn2 st p = x & (p . n2) >= 0 & |.p.| = 1;

            hence thesis;

          end;

          Sn c= the carrier of Tn2

          proof

            let x be object;

            assume x in Sn;

            then ex p be Point of Tn2 st p = x & (p . n2) <= 0 & |.p.| = 1;

            hence thesis;

          end;

          then

          reconsider Sp, Sn as Subset of Tn2 by A13;

          

           A14: Sn = { t where t be Point of Tn2 : (t . (n1 + 1)) <= 0 & |.t.| = 1 };

          

           A15: Sp = { l where l be Point of Tn2 : (l . (n1 + 1)) >= 0 & |.l.| = 1 };

          then

          reconsider s1 = Sp, s2 = Sn as closed Subset of Tn2 by A14, Th2;

          

           A16: ( [#] (Tn2 | s2)) = s2 by PRE_TOPC:def 5;

          U = ( Tcircle (( 0. Tn2),1)) by TOPREALB:def 7;

          then

           A17: the carrier of U = ( Sphere (( 0. Tn2),1)) by TOPREALB: 9;

          

           A18: s1 c= the carrier of U

          proof

            let x be object;

            assume x in s1;

            then

            consider p be Point of Tn2 such that

             A19: x = p and (p . (n1 + 1)) >= 0 and

             A20: |.p.| = 1;

            (p - ( 0. Tn2)) = p by RLVECT_1: 13;

            hence thesis by A20, A19, A17;

          end;

          

           A21: s2 c= the carrier of U

          proof

            let x be object;

            assume x in s2;

            then

            consider p be Point of Tn2 such that

             A22: x = p and (p . (n1 + 1)) <= 0 and

             A23: |.p.| = 1;

            (p - ( 0. Tn2)) = p by RLVECT_1: 13;

            hence thesis by A23, A22, A17;

          end;

          then

          reconsider S1 = s1, S2 = s2 as Subset of U by A18;

          reconsider A1 = (f " S1), A2 = (f " S2) as Subset of TM by A7, XBOOLE_1: 1;

          

           A24: (f .: (A1 /\ A2)) c= ((f .: A1) /\ (f .: A2)) by RELAT_1: 121;

          

           A25: (f .: A2) c= s2 by FUNCT_1: 75;

          S1 is closed by TSEP_1: 8;

          then (f " S1) is closed by PRE_TOPC:def 6;

          then

           A26: A1 is closed by A7, TSEP_1: 8;

          ( Sphere (( 0. Tn2),1)) c= (S1 \/ S2)

          proof

            let x be object;

            assume

             A27: x in ( Sphere (( 0. Tn2),1));

            then

            reconsider p = x as Point of Tn2;

            

             A28: (p . n2) >= 0 or (p . n2) <= 0 ;

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

            then p in Sp or p in Sn by A28;

            hence thesis by XBOOLE_0:def 3;

          end;

          then ( rng f) c= (S1 \/ S2) by A17;

          then

           A29: (f " ( rng f)) c= (f " (S1 \/ S2)) by RELAT_1: 143;

          (f " ( rng f)) = ( dom f) by RELAT_1: 134;

          then

           A30: F = (f " (S1 \/ S2)) by A29, A7, FUNCT_2:def 1;

          then

           A31: F = (A1 \/ A2) by RELAT_1: 140;

          then

          reconsider TFA12 = (A1 /\ A2) as Subset of (TM | F) by XBOOLE_1: 29, A10;

          

           A32: ( [#] ((TM | F) | TFA12)) = TFA12 by PRE_TOPC:def 5;

          reconsider fa = (f | TFA12) as Function of ((TM | F) | TFA12), (U | (f .: TFA12)) by A10, A12, JORDAN24: 12;

          

           A33: fa is continuous by JORDAN24: 13, A10, A12;

          (( dom f) /\ TFA12) = TFA12 by A8, XBOOLE_1: 28;

          then

           A34: ( dom fa) = the carrier of ((TM | F) | TFA12) by A32, RELAT_1: 61;

          

           A35: ((TM | F) | (f " S1)) = (TM | A1) by PRE_TOPC: 7, A7;

          then

          reconsider f1 = (f | A1) as Function of (TM | A1), (U | (f .: A1)) by A12, A7, JORDAN24: 12;

          

           A36: f1 is continuous by A35, A12, A10, JORDAN24: 13;

          

           A37: ( rng f1) c= the carrier of (U | (f .: A1));

          

           A38: ( [#] (U | (f .: A1))) = (f .: A1) by PRE_TOPC:def 5;

          then

           A39: ( rng f1) c= the carrier of U by XBOOLE_1: 1;

          

           A40: ((TM | F) | (f " S2)) = (TM | A2) by PRE_TOPC: 7, A7;

          then

          reconsider f2 = (f | A2) as Function of (TM | A2), (U | (f .: A2)) by A12, A7, JORDAN24: 12;

          

           A41: f2 is continuous by A40, A12, A10, JORDAN24: 13;

          

           A42: ( [#] (U | (f .: A2))) = (f .: A2) by PRE_TOPC:def 5;

          then

           A43: ( rng f2) c= the carrier of U by XBOOLE_1: 1;

          ( dom f1) = (( dom f) /\ A1) by RELAT_1: 61;

          then

           A44: ( dom f1) = A1 by A9, XBOOLE_1: 28;

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

          then

          reconsider f1 as Function of (TM | A1), U by A39, FUNCT_2: 2, A44;

          

           A45: ( rng f2) c= the carrier of (U | (f .: A2));

          ( dom f2) = (( dom f) /\ A2) by RELAT_1: 61;

          then

           A46: ( dom f2) = A2 by A9, XBOOLE_1: 28;

          ( [#] (TM | A2)) = A2 by PRE_TOPC:def 5;

          then

          reconsider f2 as Function of (TM | A2), U by A43, A46, FUNCT_2: 2;

          (f .: A2) c= s2 by FUNCT_1: 75;

          then

           A47: ( rng f2) c= s2 by A42, A45;

          S2 is closed by TSEP_1: 8;

          then (f " S2) is closed by PRE_TOPC:def 6;

          then

           A48: A2 is closed by A7, TSEP_1: 8;

          (TM | (F ` )) is second-countable by A5;

          then

          consider X1,X2 be closed Subset of TM such that

           A49: ( [#] TM) = (X1 \/ X2) and

           A50: A1 c= X1 and

           A51: A2 c= X2 and

           A52: (A1 /\ X2) = (A1 /\ A2) and

           A53: (A1 /\ A2) = (X1 /\ A2) and

           A54: ( ind ((X1 /\ X2) \ (A1 /\ A2))) <= (n1 qua ExtReal - 1) by A31, TOPDIM_2: 24, A5, A6, A26, A48;

          set TX = (TM | (X1 /\ X2));

          

           A55: ( [#] TX) = (X1 /\ X2) by PRE_TOPC:def 5;

          then

          reconsider TXA12 = (A1 /\ A2) as Subset of TX by A50, A51, XBOOLE_1: 27;

          ((X1 /\ X2) \ (A1 /\ A2)) = (TXA12 ` ) by A55, SUBSET_1:def 4;

          then

           A56: ( ind (TXA12 ` )) <= n by A5, TOPDIM_1: 21, A54;

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

          set TD = ( Tdisk (( 0. Tn1),1));

          deffunc ff( Nat) = ( PROJ (n2,$1));

          consider FF be FinSequence such that

           A57: ( len FF) = n1 & for k be Nat st k in ( dom FF) holds (FF . k) = ff(k) from FINSEQ_1:sch 2;

          

           A58: ( rng FF) c= ( Funcs (the carrier of Tn2,the carrier of R^1 ))

          proof

            let x be object;

            assume x in ( rng FF);

            then

            consider i be object such that

             A59: i in ( dom FF) and

             A60: (FF . i) = x by FUNCT_1:def 3;

            reconsider i as Nat by A59;

             ff(i) in ( Funcs (the carrier of Tn2,the carrier of R^1 )) by FUNCT_2: 8;

            hence thesis by A57, A59, A60;

          end;

          

           A61: ( Ball (( 0. Tn1),1)) c= ( Int ( cl_Ball (( 0. Tn1),1))) by TOPREAL9: 16, TOPS_1: 24;

          then

           A62: ( cl_Ball (( 0. Tn1),1)) is compact non boundary convex;

          reconsider FF as FinSequence of ( Funcs (the carrier of Tn2,the carrier of R^1 )) by A58, FINSEQ_1:def 4;

          reconsider FF as Element of (n1 -tuples_on ( Funcs (the carrier of Tn2,the carrier of R^1 ))) by A57, FINSEQ_2: 92;

          set FFF = <:FF:>;

          

           A63: (s1 /\ s2) c= s2 by XBOOLE_1: 17;

          

           A64: (FFF .: s2) = ( cl_Ball (( 0. Tn1),1)) by A57, Th1, A15;

          then

           A65: s2 is non empty;

          

           A66: ( dom FFF) = the carrier of Tn2 by FUNCT_2:def 1;

          then (s1 /\ ( dom FFF)) = s1 by XBOOLE_1: 28;

          then

           A67: ( dom (FFF | s1)) = s1 by RELAT_1: 61;

          (s2 /\ ( dom FFF)) = s2 by XBOOLE_1: 28, A66;

          then

           A68: ( dom (FFF | s2)) = s2 by RELAT_1: 61;

          

           A69: the carrier of TD = ( cl_Ball (( 0. Tn1),1)) by BROUWER: 3;

          then ( rng (FFF | s2)) c= the carrier of TD by RELAT_1: 115, A64;

          then

          reconsider Fs2 = (FFF | s2) as Function of (Tn2 | s2), TD by FUNCT_2: 2, A16, A68;

          

           A70: ( [#] (Tn2 | s1)) = s1 by PRE_TOPC:def 5;

          Fs2 is being_homeomorphism by A57, Th1, A15;

          then

           A71: (s2,( cl_Ball (( 0. Tn1),1))) are_homeomorphic by T_0TOPSP:def 1, METRIZTS:def 1;

          

           A72: (FFF .: s1) = ( cl_Ball (( 0. Tn1),1)) by A57, Th1, A14;

          then

           A73: s1 is non empty;

          ( rng (FFF | s1)) c= the carrier of TD by RELAT_1: 115, A72, A69;

          then

          reconsider Fs1 = (FFF | s1) as Function of (Tn2 | s1), TD by A67, FUNCT_2: 2, A70;

          

           A74: (Fs1 .: (s1 /\ s2)) c= (FFF .: (s1 /\ s2)) by RELAT_1: 128;

          

           A75: Fs1 is being_homeomorphism by A57, Th1, A14;

          then

           A76: ( rng Fs1) = ( [#] TD) by TOPS_2:def 5;

          (f .: A1) c= s1 by FUNCT_1: 75;

          then

           WE: ((f .: A1) /\ (f .: A2)) c= (s1 /\ s2) by A25, XBOOLE_1: 27;

          then (f .: (A1 /\ A2)) c= (s1 /\ s2) by A24;

          then

           A78: (Fs1 .: (f .: (A1 /\ A2))) c= (Fs1 .: (s1 /\ s2)) by RELAT_1: 123;

          (s1 /\ s2) c= s1 by XBOOLE_1: 17;

          then

           A79: (f .: (A1 /\ A2)) c= s1 by WE, A24;

          ( [#] (U | (f .: TFA12))) = (f .: TFA12) by PRE_TOPC:def 5;

          then

           A80: ( rng fa) c= the carrier of (Tn2 | s1) by A79, A70;

          then

          reconsider fa as Function of ((TM | F) | TFA12), U by XBOOLE_1: 1, A70, A34, FUNCT_2: 2;

          

           A81: fa is continuous by A33, PRE_TOPC: 26;

          ( rng fa) c= the carrier of Tn2 by A17, XBOOLE_1: 1;

          then

          reconsider fa as Function of ((TM | F) | TFA12), Tn2 by FUNCT_2: 2, A34;

          

           A82: fa is continuous by A81, PRE_TOPC: 26;

          

           A83: (Fs1 " ) is continuous by A75, TOPS_2:def 5;

          

           A84: (FFF .: (s1 /\ s2)) = ( Sphere (( 0. Tn1),1)) by A57, Th1;

          then (Fs1 .: (s1 /\ s2)) = ( Sphere (( 0. Tn1),1)) by XBOOLE_1: 17, RELAT_1: 129;

          

          then

           A85: ((Fs1 " ) .: ( Sphere (( 0. Tn1),1))) = (Fs1 " (Fs1 .: (s1 /\ s2))) by TOPS_2: 55, A75, A76

          .= (s1 /\ s2) by FUNCT_1: 94, A67, A75, XBOOLE_1: 17;

          set A2X = (A2 \/ (X1 /\ X2));

          set A1X = (A1 \/ (X1 /\ X2));

          

           A86: X2 = ( [#] (TM | X2)) by PRE_TOPC:def 5;

          ((TM | F) | TFA12) = (TM | (A1 /\ A2)) by PRE_TOPC: 7, A31, XBOOLE_1: 29;

          then

           A87: ((TM | F) | TFA12) = (TX | TXA12) by PRE_TOPC: 7, A50, A51, XBOOLE_1: 27;

          then

          reconsider fa as Function of (TX | TXA12), (Tn2 | s1) by A34, FUNCT_2: 2, A80;

          reconsider Ffa = (Fs1 * fa) as Function of (TX | TXA12), TD by A73;

          

           A88: ( [#] (TX | TXA12)) = TXA12 by PRE_TOPC:def 5;

          then

           A89: ( dom Ffa) = (A1 /\ A2) by FUNCT_2:def 1;

          ( rng Ffa) = (Ffa .: ( dom Ffa)) by RELAT_1: 113

          .= ((Fs1 * fa) .: (A1 /\ A2)) by A88, FUNCT_2:def 1

          .= (Fs1 .: (fa .: (A1 /\ A2))) by RELAT_1: 126;

          then

           E: ( rng Ffa) c= (Fs1 .: (f .: (A1 /\ A2))) by RELAT_1: 123, RELAT_1: 128;

          then

           A90: ( rng Ffa) c= (Fs1 .: (s1 /\ s2)) by A78;

          

           A91: ( rng Ffa) c= ( Sphere (( 0. Tn1),1)) by E, A78, A74, A84;

          fa is continuous by A82, PRE_TOPC: 27, A87;

          then

           A92: Ffa is continuous by TOPS_2: 46, A75, A73;

          reconsider Ffa as Function of (TX | TXA12), Tn1 by A91, XBOOLE_1: 1, FUNCT_2: 2, A89, A88;

          Un = ( Tcircle (( 0. Tn1),1)) by TOPREALB:def 7;

          then

           A93: the carrier of Un = ( Sphere (( 0. Tn1),1)) by TOPREALB: 9;

          then

          reconsider H = Ffa as Function of (TX | TXA12), Un by FUNCT_2: 2, A89, A88, A90, A74, XBOOLE_1: 1, A84;

          Ffa is continuous by A92, PRE_TOPC: 26;

          then

          reconsider H as continuous Function of (TX | TXA12), Un by PRE_TOPC: 27;

          TXA12 is closed by A26, A48, TSEP_1: 8;

          then

          consider g be Function of TX, Un such that

           A94: g is continuous and

           A95: (g | TXA12) = H by A5, A56, A4;

          

           A96: ( rng g) c= the carrier of Tn1 by A93, XBOOLE_1: 1;

          

           A97: ( dom g) = the carrier of TX by FUNCT_2:def 1;

          

           A98: ( rng g) c= the carrier of Un;

          reconsider g as Function of TX, Tn1 by A97, A96, FUNCT_2: 2;

          

           A99: g is continuous by A94, PRE_TOPC: 26;

          the carrier of Un c= the carrier of TD by A93, A69, TOPREAL9: 17;

          then

          reconsider g as Function of TX, TD by A98, XBOOLE_1: 1, FUNCT_2: 2, A97;

          reconsider G = ((Fs1 " ) * g) as Function of TX, (Tn2 | s1);

          

           A100: ( dom G) = the carrier of TX by FUNCT_2:def 1, A73;

          g is continuous by A99, PRE_TOPC: 27;

          then

           A101: G is continuous by A83, TOPS_2: 46;

          

           A102: ( rng G) c= s1 by A70;

          then

          reconsider G as Function of TX, Tn2 by XBOOLE_1: 1, FUNCT_2: 2, A100;

          

           A103: G is continuous by PRE_TOPC: 26, A101;

          reconsider G as Function of TX, U by A18, A102, XBOOLE_1: 1, FUNCT_2: 2, A100;

          

           A104: G is continuous by PRE_TOPC: 27, A103;

          

           A105: ( rng fa) c= ( dom Fs1) by A67, A70;

          

           A106: (G | TXA12) = ((Fs1 " ) * (g | TXA12)) by RELAT_1: 83

          .= (((Fs1 " ) * Fs1) * fa) by RELAT_1: 36, A95

          .= (( id ( dom Fs1)) * fa) by TOPS_2: 52, A75, A76

          .= fa by RELAT_1: 53, A105;

           A107:

          now

            let xx be object;

            assume

             A108: xx in (( dom f1) /\ ( dom G));

            then

             A109: xx in A1 by A44, XBOOLE_0:def 4;

            xx in X2 by A108, A55, XBOOLE_0:def 4;

            then

             A110: xx in (A1 /\ A2) by A109, A52, XBOOLE_0:def 4;

            

            hence (G . xx) = ((G | TXA12) . xx) by FUNCT_1: 49

            .= (f . xx) by A110, FUNCT_1: 49, A106

            .= (f1 . xx) by A109, FUNCT_1: 49;

          end;

           A111:

          now

            let xx be object;

            assume

             A112: xx in (( dom f2) /\ ( dom G));

            then

             A113: xx in A2 by A46, XBOOLE_0:def 4;

            xx in X1 by A112, A55, XBOOLE_0:def 4;

            then

             A114: xx in (A1 /\ A2) by A113, A53, XBOOLE_0:def 4;

            

            hence (G . xx) = ((G | TXA12) . xx) by FUNCT_1: 49

            .= (f . xx) by A114, FUNCT_1: 49, A106

            .= (f2 . xx) by A113, FUNCT_1: 49;

          end;

          ( rng G) = (G .: ( dom G)) by RELAT_1: 113

          .= ((Fs1 " ) .: (g .: ( dom G))) by RELAT_1: 126

          .= ((Fs1 " ) .: ( rng g)) by A97, A100, RELAT_1: 113;

          then ( rng G) c= (s1 /\ s2) by A85, A93, A98, RELAT_1: 123;

          then ( rng G) c= s2 by A63;

          then

           A115: (( rng f2) \/ ( rng G)) c= s2 by XBOOLE_1: 8, A47;

          f2 is continuous by A41, PRE_TOPC: 26;

          then

          reconsider f2G = (f2 +* G) as continuous Function of (TM | A2X), U by A111, PARTFUN1:def 4, A104, A48, TOPGEN_5: 10;

          

           A116: ( dom f2G) = the carrier of (TM | A2X) by FUNCT_2:def 1;

          

           A117: ( rng f2G) c= (( rng f2) \/ ( rng G)) by FUNCT_4: 17;

          then ( rng f2G) c= s2 by A115;

          then

          reconsider f2G as Function of (TM | A2X), Tn2 by XBOOLE_1: 1, FUNCT_2: 2, A116;

          

           A118: f2G is continuous by PRE_TOPC: 26;

          reconsider f2G as Function of (TM | A2X), (Tn2 | s2) by FUNCT_2: 2, A116, A115, A117, XBOOLE_1: 1, A16;

          ( cl_Ball (( 0. Tn1),1)) is compact non boundary convex by A61;

          then

          consider H2 be Function of TM, (Tn2 | s2) such that

           A119: H2 is continuous and

           A120: (H2 | A2X) = f2G by A118, PRE_TOPC: 27, A71, TIETZE_2: 24, A48;

          

           A121: TM is non empty by A12;

          then

          reconsider H2X = (H2 | X2) as Function of (TM | X2), ((Tn2 | s2) | (H2 .: X2)) by JORDAN24: 12, A65;

          

           A122: H2X is continuous by JORDAN24: 13, A65, A121, A119;

          ( dom H2) = the carrier of TM by FUNCT_2:def 1, A65;

          then

           A123: ( dom H2X) = (X2 /\ the carrier of TM) by RELAT_1: 61;

          then

           A124: ( dom H2X) = the carrier of (TM | X2) by XBOOLE_1: 28, A86;

          f1 is continuous by A36, PRE_TOPC: 26;

          then

          reconsider f1G = (f1 +* G) as continuous Function of (TM | A1X), U by A107, PARTFUN1:def 4, A104, A26, TOPGEN_5: 10;

          

           A125: ( dom f1G) = the carrier of (TM | A1X) by FUNCT_2:def 1;

          (f .: A1) c= s1 by FUNCT_1: 75;

          then ( rng f1) c= s1 by A38, A37;

          then

           A126: (( rng f1) \/ ( rng G)) c= s1 by A102, XBOOLE_1: 8;

          

           A127: ( rng f1G) c= (( rng f1) \/ ( rng G)) by FUNCT_4: 17;

          then ( rng f1G) c= s1 by A126;

          then

          reconsider f1G as Function of (TM | A1X), Tn2 by XBOOLE_1: 1, FUNCT_2: 2, A125;

          

           A128: f1G is continuous by PRE_TOPC: 26;

          reconsider f1G as Function of (TM | A1X), (Tn2 | s1) by FUNCT_2: 2, A125, A126, A127, XBOOLE_1: 1, A70;

          (s1,( cl_Ball (( 0. Tn1),1))) are_homeomorphic by T_0TOPSP:def 1, A75, METRIZTS:def 1;

          then

          consider H1 be Function of TM, (Tn2 | s1) such that

           A129: H1 is continuous and

           A130: (H1 | A1X) = f1G by A62, A26, A128, PRE_TOPC: 27, TIETZE_2: 24;

          reconsider H1X = (H1 | X1) as Function of (TM | X1), ((Tn2 | s1) | (H1 .: X1)) by A121, JORDAN24: 12, A73;

          

           A131: H1X is continuous by JORDAN24: 13, A73, A121, A129;

          ( [#] ((Tn2 | s1) | (H1 .: X1))) = (H1 .: X1) by PRE_TOPC:def 5;

          then

           A132: ( rng H1X) c= the carrier of (Tn2 | s1) by XBOOLE_1: 1;

          ( dom H1) = the carrier of TM by FUNCT_2:def 1, A73;

          then

           A133: ( dom H1X) = (X1 /\ the carrier of TM) by RELAT_1: 61;

          then

           A134: ( dom H1X) = X1 by XBOOLE_1: 28;

          X1 = ( [#] (TM | X1)) by PRE_TOPC:def 5;

          then

           A135: ( dom H1X) = the carrier of (TM | X1) by A133, XBOOLE_1: 28;

          then

          reconsider H1X as Function of (TM | X1), (Tn2 | s1) by A132, FUNCT_2: 2;

          

           A136: H1X is continuous by A131, PRE_TOPC: 26;

          

           A137: ( rng H1X) c= s1 by A70;

          ( [#] ((Tn2 | s2) | (H2 .: X2))) = (H2 .: X2) by PRE_TOPC:def 5;

          then ( rng H2X) c= the carrier of (Tn2 | s2) by XBOOLE_1: 1;

          then

          reconsider H2X as Function of (TM | X2), (Tn2 | s2) by A124, FUNCT_2: 2;

          

           A138: H2X is continuous by A122, PRE_TOPC: 26;

          reconsider H1X as Function of (TM | X1), Tn2 by A137, XBOOLE_1: 1, A135, FUNCT_2: 2;

          

           A139: ( rng H2X) c= s2 by A16;

          then

          reconsider H2X as Function of (TM | X2), Tn2 by XBOOLE_1: 1, A124, FUNCT_2: 2;

          

           A140: H2X is continuous by A138, PRE_TOPC: 26;

           A141:

          now

            let xx be object;

            assume

             A142: xx in (( dom H1X) /\ ( dom H2X));

            then

             A143: (H2X . xx) = (H2 . xx) by A86, FUNCT_1: 49;

            xx in X1 by A142, A134, XBOOLE_0:def 4;

            then

             A144: (H1X . xx) = (H1 . xx) by FUNCT_1: 49;

            

             A145: xx in (X1 /\ X2) by A142, A123, XBOOLE_1: 28, A134;

            then

             A146: xx in A2X by XBOOLE_0:def 3;

            xx in A1X by A145, XBOOLE_0:def 3;

            then

             A147: (H1 . xx) = ((H1 | A1X) . xx) by FUNCT_1: 49;

            

             A148: (f2G . xx) = (G . xx) by A145, A100, A55, FUNCT_4: 13;

            (f1G . xx) = (G . xx) by A145, A100, A55, FUNCT_4: 13;

            hence (H1X . xx) = (H2X . xx) by A148, A147, A146, FUNCT_1: 49, A144, A143, A120, A130;

          end;

          H1X is continuous by A136, PRE_TOPC: 26;

          then

          reconsider H12 = (H1X +* H2X) as continuous Function of (TM | (X1 \/ X2)), Tn2 by A140, A141, PARTFUN1:def 4, TOPGEN_5: 10;

          

           A149: (TM | (X1 \/ X2)) = the TopStruct of TM by A49, TSEP_1: 93;

          then

          reconsider H12 as Function of TM, Tn2;

          

           A150: ( rng H12) c= (( rng H1X) \/ ( rng H2X)) by FUNCT_4: 17;

          (F /\ X1) = ((A1 \/ A2) /\ X1) by A30, RELAT_1: 140

          .= ((A1 /\ X1) \/ (A2 /\ X1)) by XBOOLE_1: 23

          .= (A1 \/ (A2 /\ X1)) by A50, XBOOLE_1: 28

          .= A1 by A53, XBOOLE_1: 17, XBOOLE_1: 12;

          then

           A151: (H1X | F) = (H1 | A1) by RELAT_1: 71;

          f1G = (G +* f1) by A107, PARTFUN1:def 4, FUNCT_4: 34;

          then

           A152: (f1G | A1) = f1 by FUNCT_4: 23, A44;

          

           A153: (F /\ X2) = ((A1 \/ A2) /\ X2) by A30, RELAT_1: 140

          .= ((A1 /\ X2) \/ (A2 /\ X2)) by XBOOLE_1: 23

          .= ((A1 /\ X2) \/ A2) by A51, XBOOLE_1: 28

          .= A2 by A52, XBOOLE_1: 17, XBOOLE_1: 12;

          

           A154: (H2 | A2) = (f2G | A2) by A120, RELAT_1: 74, XBOOLE_1: 7;

          (( rng H1X) \/ ( rng H2X)) c= (s1 \/ s2) by A139, A137, XBOOLE_1: 13;

          then

           A155: ( rng H12) c= (s1 \/ s2) by A150;

          

           A156: ( dom H12) = the carrier of TM by FUNCT_2:def 1;

          

           A157: H12 is continuous by PRE_TOPC: 32, A149;

          (s1 \/ s2) c= ( Sphere (( 0. Tn2),1)) by A18, A21, A17, XBOOLE_1: 8;

          then

          reconsider H12 as Function of TM, U by A155, XBOOLE_1: 1, A17, A156, FUNCT_2: 2;

          take H12;

          thus H12 is continuous by PRE_TOPC: 27, A157;

          

           A158: (H1 | A1) = (f1G | A1) by A130, XBOOLE_1: 7, RELAT_1: 74;

          f2G = (G +* f2) by A111, PARTFUN1:def 4, FUNCT_4: 34;

          then

           A159: (f2G | A2) = f2 by FUNCT_4: 23, A46;

          

          thus (H12 | F) = ((H1X | F) +* (H2X | F)) by FUNCT_4: 71

          .= (f1 +* f2) by A152, A159, A158, A154, A151, RELAT_1: 71, A153

          .= (f | (A1 \/ A2)) by FUNCT_4: 78

          .= f by A31, A10;

        end;

      end;

      let f be continuous Function of (TM | F), ( Tunit_circle (n + 1));

      

       A160: P[ 0 qua Nat]

      proof

        reconsider Z = 0 as Real;

        set TR = ( TOP-REAL 1), U = ( Tunit_circle ( 0 + 1));

        let TM be metrizable TopSpace;

        assume

         A161: TM is finite-ind second-countable;

        let F be closed Subset of TM;

        assume

         A162: ( ind (F ` )) <= 0 ;

        let f be continuous Function of (TM | F), U;

        

         A164: (f " ( rng f)) = (f " the carrier of U) by RELAT_1: 143, RELAT_1: 135;

        U = ( Tcircle (( 0. TR),1)) by TOPREALB:def 7;

        then

         A165: the carrier of U = ( Sphere (( 0. TR),1)) by TOPREALB: 9;

        ( 0. TR) = ( 0* ( 0 + 1)) by EUCLID: 70

        .= <* 0 *> by FINSEQ_2: 59;

        then

         A166: { <*(Z qua ExtReal - 1)*>, <*(Z qua ExtReal + 1)*>} = ( Fr ( Ball (( 0. TR),1))) by TOPDIM_2: 18;

        

         A167: ( Fr ( Ball (( 0. TR),1))) = ( Sphere (( 0. TR),1)) by JORDAN: 24;

        then

        reconsider mONE = <*( - 1)*>, ONE = <*1*> as Point of U by A165, TARSKI:def 2, A166;

        reconsider Q = {ONE}, Q1 = {mONE} as closed Subset of U;

        set F1 = (f " Q), F2 = (f " Q1);

        

         A168: ( [#] (TM | F)) = F by PRE_TOPC:def 5;

        then

        reconsider A1 = F1, A2 = F2 as Subset of TM by XBOOLE_1: 1;

        

         A169: ( dom f) = F by A168, FUNCT_2:def 1;

        (Q \/ Q1) = the carrier of U by A166, A167, A165, ENUMSET1: 1;

        

        then

         A170: (F1 \/ F2) = (f " the carrier of U) by RELAT_1: 140

        .= F by A164, RELAT_1: 134, A169;

        F2 is closed by PRE_TOPC:def 6;

        then

         A171: A2 is closed by TSEP_1: 8, A168;

        F1 is closed by PRE_TOPC:def 6;

        then

         A172: A1 is closed by TSEP_1: 8, A168;

        ONE <> mONE

        proof

          assume ONE = mONE;

          then ( <*1*> . 1) = ( - 1) by FINSEQ_1: 40;

          hence thesis;

        end;

        then

         W: F1 misses F2 by ZFMISC_1: 11, FUNCT_1: 71;

        (TM | (F ` )) is second-countable by A161;

        then

        consider X1,X2 be closed Subset of TM such that

         A174: ( [#] TM) = (X1 \/ X2) and

         A175: A1 c= X1 and

         A176: A2 c= X2 and (A1 /\ X2) = (A1 /\ A2) & (A1 /\ A2) = (X1 /\ A2) and

         A177: ( ind ((X1 /\ X2) \ (A1 /\ A2))) <= ( 0 qua ExtReal - 1) by A161, A162, A170, TOPDIM_2: 24, A172, A171;

        ( ind (X1 /\ X2)) >= ( - 1) by TOPDIM_1: 5, A161;

        then

         A178: (X1 /\ X2) is empty by A177, W, XXREAL_0: 1, TOPDIM_1: 6, A161;

        set h1 = ((TM | X1) --> ONE), h2 = ((TM | X2) --> mONE);

        

         A179: ( [#] (TM | X1)) = X1 by PRE_TOPC:def 5;

        

         A180: ( dom h2) = the carrier of (TM | X2);

        

         A181: ( [#] (TM | X2)) = X2 by PRE_TOPC:def 5;

        ( dom h1) = the carrier of (TM | X1);

        then h1 tolerates h2 by A178, A179, A180, A181, XBOOLE_0:def 7, PARTFUN1: 56;

        then

        reconsider h12 = (h1 +* h2) as continuous Function of (TM | ( [#] TM)), U by A174, TOPGEN_5: 10;

        ( [#] (TM | ( [#] TM))) = ( [#] TM) by PRE_TOPC:def 5;

        then

        reconsider H12 = h12 as Function of TM, U;

        

         A182: for x be object st x in F holds ((H12 | F) . x) = (f . x)

        proof

          let x be object;

          assume

           A183: x in F;

          then

           A184: ((H12 | F) . x) = (h12 . x) by FUNCT_1: 49;

          per cases by A183, A170, XBOOLE_0:def 3;

            suppose

             A185: x in F1;

            then not x in ( dom h2) by A175, A178, XBOOLE_0:def 4, A181;

            then

             A186: (H12 . x) = (h1 . x) by FUNCT_4: 11;

            

             A187: (f . x) in {ONE} by A185, FUNCT_1:def 7;

            (h1 . x) = ONE by A185, A175, A179, FUNCOP_1: 7;

            hence thesis by A187, TARSKI:def 1, A186, A184;

          end;

            suppose

             A188: x in F2;

            then

             A189: (f . x) in {mONE} by FUNCT_1:def 7;

            

             A190: (h2 . x) = mONE by A188, A176, A181, FUNCOP_1: 7;

            (H12 . x) = (h2 . x) by A188, A176, A180, A181, FUNCT_4: 13;

            hence thesis by A189, TARSKI:def 1, A190, A184;

          end;

        end;

        take H12;

        (TM | ( [#] TM)) = the TopStruct of TM by TSEP_1: 93;

        hence H12 is continuous by PRE_TOPC: 32;

        ( dom H12) = the carrier of TM by FUNCT_2:def 1;

        then ( dom (H12 | F)) = F by RELAT_1: 62;

        hence thesis by A182, A168, FUNCT_2:def 1;

      end;

      for n holds P[n] from NAT_1:sch 2( A160, A3);

      then ex g be Function of TM, ( Tunit_circle (n + 1)) st g is continuous & (g | F) = f by A1, A2;

      hence thesis;

    end;

    theorem :: BROUWER3:4

    

     Th4: not p in A & r > 0 implies ex h be Function of (( TOP-REAL n) | A), (( TOP-REAL n) | ( Sphere (p,r))) st h is continuous & (h | ( Sphere (p,r))) = ( id (A /\ ( Sphere (p,r))))

    proof

      set TR = ( TOP-REAL n);

      assume that

       A1: not p in A and

       A2: r > 0 ;

      set S = ( Sphere (p,r));

      per cases ;

        suppose

         A3: A is empty;

        set h = the continuous Function of (TR | A), TR;

        reconsider H = h as Function of (TR | A), (TR | S) by A3;

        take H;

        thus thesis by A3, PRE_TOPC: 27;

      end;

        suppose

         A4: A is non empty;

        A <> {p} by A1, TARSKI:def 1;

        then

         A5: (A \ {p}) <> {} by A4, ZFMISC_1: 58;

        set TRS = (TR | S);

        set nN = (n NormF ), t = ( transl (( - p),TR)), P = ( transl (p,TR));

        

         A6: (A \ {p}) c= (the carrier of TR \ {p}) by XBOOLE_1: 33;

        (the carrier of TR \ {p}) = ( {p} ` ) by SUBSET_1:def 4;

        then

        reconsider cTRp = (the carrier of TR \ {p}) as non empty open Subset of TR by A5, A6;

        set TRp = (TR | cTRp), tt = (t | TRp);

        

         A7: ( [#] TRp) = cTRp by PRE_TOPC:def 5;

        then

        reconsider AA = A as Subset of TRp by A1, ZFMISC_1: 57, A6;

        reconsider Ir = (tt [#] r) as Function of TRp, TR by TOPREALC: 37;

        reconsider IrNt = (Ir </> (nN * tt)) as Function of TRp, TR by TOPREALC: 46;

        

         A8: tt = (t | the carrier of TRp) by TMAP_1:def 4;

         not 0 in ( rng (nN * tt))

        proof

          assume 0 in ( rng (nN * tt));

          then

          consider x be object such that

           A9: x in ( dom (nN * tt)) and

           A10: ((nN * tt) . x) = 0 by FUNCT_1:def 3;

          (tt . x) in ( dom nN) by A9, FUNCT_1: 11;

          then

          reconsider Tx = (tt . x) as Point of TR;

          reconsider Tx as Element of ( REAL n) by EUCLID: 22;

          

           A11: x in ( dom tt) by A9, FUNCT_1: 11;

          then

           A12: (t . x) = (tt . x) by A8, FUNCT_1: 47;

          x in ( dom t) by A11, A8, RELAT_1: 57;

          then

          reconsider X = x as Point of TR;

           0 = (nN . Tx) by A9, FUNCT_1: 12, A10

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

          then ( 0* n) = Tx by EUCLID: 8;

          

          then ( 0. TR) = Tx by EUCLID: 70

          .= (( - p) + X) by A12, RLTOPSP1:def 10;

          

          then X = ( - ( - p)) by RLVECT_1:def 10

          .= p;

          then x in {p} by TARSKI:def 1;

          hence contradiction by A9, A7, XBOOLE_0:def 5;

        end;

        then (nN * tt) is non-empty by RELAT_1:def 9;

        then

        reconsider IrNt as continuous Function of TRp, TR;

        set h = ((P * IrNt) | (TRp | AA));

        

         A13: h = ((P * IrNt) | the carrier of (TRp | AA)) by TMAP_1:def 4;

        reconsider h as continuous Function of (TRp | AA), TR by A4;

        (TRp | AA) = (TR | A) by PRE_TOPC: 7, A7;

        then

        reconsider h as continuous Function of (TR | A), TR;

        

         A14: ( [#] (TR | A)) = A by PRE_TOPC:def 5;

        then

         A15: ( dom h) = A by FUNCT_2:def 1;

        

         A16: ( dom tt) = cTRp by A7, FUNCT_2:def 1;

        

         A17: ( rng h) c= S

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A18: x in ( dom h) and

           A19: (h . x) = y by FUNCT_1:def 3;

          reconsider x as Point of TR by A18, A15;

          (tt . x) = (t . x) by A7, A18, A15, FUNCT_1: 47, A8, A16;

          then

           A20: (tt . x) = (( - p) + x) by RLTOPSP1:def 10;

          ( dom (nN * tt)) = cTRp by A7, FUNCT_2:def 1;

          then ((nN * tt) . x) = (nN . (tt . x)) by A7, A18, A15, FUNCT_1: 12;

          then

           A21: ((nN * tt) . x) = |.(( - p) + x).| by A20, JGRAPH_4:def 1;

          

           A22: x in ( dom (P * IrNt)) by A13, A18, RELAT_1: 57;

          then x in ( dom IrNt) by FUNCT_1: 11;

          then

           A23: (IrNt . x) = ((Ir . x) (/) ((nN * tt) . x)) by VALUED_2: 72;

          ( dom Ir) = cTRp by A7, FUNCT_2:def 1;

          then (Ir . x) = (r * (( - p) + x)) by A20, A7, A18, A15, VALUED_2:def 39;

          then

           A24: (IrNt . x) = ((1 / |.(( - p) + x).|) * (r * (( - p) + x))) by A21, A23, VALUED_2:def 32;

          then

          reconsider Fx = (IrNt . x) as Point of TR;

          (h . x) = ((P * IrNt) . x) by A13, A18, FUNCT_1: 47;

          

          then

           A25: (h . x) = (P . Fx) by A22, FUNCT_1: 12

          .= (p + Fx) by RLTOPSP1:def 10;

          ( - ( - p)) = p;

          then (( - p) + x) <> ( 0. TR) by A18, A1, A15, RLVECT_1: 6;

          then

           A26: (( - p) + x) <> ( 0* n) by EUCLID: 70;

          

           A27: (( - p) + x) is Element of ( REAL n) by EUCLID: 22;

          

           A28: ((p + Fx) - p) = (Fx + (p + ( - p))) by RLVECT_1:def 3

          .= (Fx + ( 0. TR)) by RLVECT_1:def 10

          .= Fx by RLVECT_1:def 4;

           |.Fx.| = |.(((1 / |.(( - p) + x).|) * r) * (( - p) + x)).| by A24, RLVECT_1:def 7

          .= ( |.((1 / |.(( - p) + x).|) * r).| * |.(( - p) + x).|) by EUCLID: 11

          .= (( |.(1 / |.(( - p) + x).|).| * |.r.|) * |.(( - p) + x).|) by COMPLEX1: 65

          .= (( |.(1 / |.(( - p) + x).|).| * r) * |.(( - p) + x).|) by ABSVALUE:def 1, A2

          .= (( |.(1 / |.(( - p) + x).|).| * r) * |. |.(( - p) + x).|.|) by ABSVALUE:def 1

          .= (( |.(1 / |.(( - p) + x).|).| * |. |.(( - p) + x).|.|) * r)

          .= (1 * r) by ABSVALUE: 6, A26, EUCLID: 8, A27

          .= r;

          hence thesis by A28, A25, A19;

        end;

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

        then

        reconsider h as Function of (TR | A), (TR | S) by A17, A14, A15, FUNCT_2: 2;

        

         A29: ( dom (h | S)) = (A /\ S) by A15, RELAT_1: 61;

        

         A31: for x be object st x in ( dom (h | S)) holds ((h | S) . x) = (( id (A /\ S)) . x)

        proof

          let y be object;

          assume

           A32: y in ( dom (h | S));

          then

          reconsider x = y as Point of TR by A29;

          

           A33: x in ( dom h) by A32, RELAT_1: 57;

          then

           A34: (h . x) = ((P * IrNt) . x) by A13, FUNCT_1: 47;

          (tt . x) = (t . x) by A7, A33, A15, FUNCT_1: 47, A8, A16;

          then

           A35: (tt . x) = (( - p) + x) by RLTOPSP1:def 10;

          (x - p) = (( - p) + x);

          then

           A36: |.(( - p) + x).| = r by A32, TOPREAL9: 9;

          

           A37: x in ( dom (P * IrNt)) by A13, A33, RELAT_1: 57;

          then x in ( dom IrNt) by FUNCT_1: 11;

          then

           A38: (IrNt . x) = ((Ir . x) (/) ((nN * tt) . x)) by VALUED_2: 72;

          ( dom (nN * tt)) = cTRp by A7, FUNCT_2:def 1;

          then ((nN * tt) . x) = (nN . (tt . x)) by A7, A33, A15, FUNCT_1: 12;

          then

           A39: ((nN * tt) . x) = |.(( - p) + x).| by A35, JGRAPH_4:def 1;

          ( dom Ir) = cTRp by A7, FUNCT_2:def 1;

          then (Ir . x) = (r * (( - p) + x)) by A35, A7, A33, A15, VALUED_2:def 39;

          

          then

           A40: (IrNt . x) = ((1 / |.(( - p) + x).|) * (r * (( - p) + x))) by A39, A38, VALUED_2:def 32

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

          .= (1 * (( - p) + x)) by XCMPLX_1: 87, A2

          .= (( - p) + x) by RLVECT_1:def 8;

          

          thus ((h | S) . y) = (h . x) by A32, FUNCT_1: 47

          .= (P . (( - p) + x)) by A34, A37, FUNCT_1: 12, A40

          .= (p + (( - p) + x)) by RLTOPSP1:def 10

          .= ((p + ( - p)) + x) by RLVECT_1:def 3

          .= (( 0. TR) + x) by RLVECT_1:def 10

          .= x by RLVECT_1:def 4

          .= (( id (A /\ S)) . y) by A32, A29, FUNCT_1: 17;

        end;

        take h;

        thus thesis by A31, A15, PRE_TOPC: 27, RELAT_1: 61;

      end;

    end;

    theorem :: BROUWER3:5

    

     Th5: (r + |.(p - q).|) <= s implies ( Ball (p,r)) c= ( Ball (q,s))

    proof

      assume

       A1: (r + |.(p - q).|) <= s;

      let x be object;

      assume

       A2: x in ( Ball (p,r));

      then

      reconsider x as Point of ( TOP-REAL n);

      ( |.(x - p).| + |.(p - q).|) < (r + |.(p - q).|) by A2, TOPREAL9: 7, XREAL_1: 6;

      then

       A3: ( |.(x - p).| + |.(p - q).|) < s by A1, XXREAL_0: 2;

      

       A4: x is Element of ( REAL n) by EUCLID: 22;

      

       A5: p is Element of ( REAL n) by EUCLID: 22;

      q is Element of ( REAL n) by EUCLID: 22;

      then |.(x - q).| <= ( |.(x - p).| + |.(p - q).|) by A4, A5, EUCLID: 19;

      then |.(x - q).| < s by A3, XXREAL_0: 2;

      hence thesis;

    end;

    theorem :: BROUWER3:6

    

     Th6: A is non boundary implies ( ind A) = n

    proof

      set TR = ( TOP-REAL n);

      set E = the empty Subset of TR;

      consider Ia be affinely-independent Subset of TR such that E c= Ia & Ia c= ( [#] TR) and

       A1: ( Affin Ia) = ( Affin ( [#] TR)) by RLAFFIN1: 60;

      

       A2: the TopStruct of TR = ( TopSpaceMetr ( Euclid n)) by EUCLID:def 8;

      then

      reconsider IA = Ia as finite Subset of ( Euclid n) by TOPMETR: 12;

      IA <> {} by A1;

      then

      consider X be object such that

       A3: X in IA by XBOOLE_0:def 1;

      reconsider X as Point of ( Euclid n) by A3;

      reconsider x = X as Point of TR by A2, TOPMETR: 12;

      

       A4: ( dim TR) = n by RLAFFIN3: 4;

      ( [#] TR) c= ( Affin ( [#] TR)) by RLAFFIN1: 49;

      then ( card Ia) = (( dim TR) + 1) by A1, XBOOLE_0:def 10, RLAFFIN3: 6;

      then

       A5: ( ind ( conv Ia)) = n by A4, SIMPLEX2: 25;

      set d = ( diameter IA);

      

       A6: ( ind TR) = n by SIMPLEX2: 26;

      Ia c= ( conv Ia) by RLAFFIN1: 2;

      then

       A7: ( conv Ia) c= ( cl_Ball (X,d)) by A3, SIMPLEX2: 13;

      assume A is non boundary;

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

      then

      consider y be object such that

       A8: y in ( Int A) by XBOOLE_0:def 1;

      reconsider y as Point of TR by A8;

      reconsider Y = y as Point of ( Euclid n) by A2, TOPMETR: 12;

      consider r be Real such that

       A9: r > 0 and

       A10: ( Ball (Y,r)) c= A by A8, GOBOARD6: 5;

      set r2 = (r / 2);

      

       A11: n in NAT by ORDINAL1:def 12;

      

       A12: ( Ball (Y,r)) = ( Ball (y,r)) by TOPREAL9: 13;

      (d + 0 ) < (d + 1) by XREAL_1: 6;

      then

       A13: ( cl_Ball (x,d)) c= ( Ball (x,(d + 1))) by A11, JORDAN: 21;

      ( cl_Ball (X,d)) = ( cl_Ball (x,d)) by TOPREAL9: 14;

      then ( conv Ia) c= ( Ball (x,(d + 1))) by A13, A7;

      then

       A14: n <= ( ind ( Ball (x,(d + 1)))) by A5, TOPDIM_1: 19;

      d >= 0 by TBSP_1: 21;

      then

       A15: ( cl_Ball (x,(d + 1))) is compact non boundary by Lm2;

      ( cl_Ball (y,r2)) c= ( Ball (y,r)) by A9, XREAL_1: 216, A11, JORDAN: 21;

      then ( cl_Ball (y,r2)) c= A by A10, A12;

      then

       A16: ( ind ( cl_Ball (y,r2))) <= ( ind A) by TOPDIM_1: 19;

      ( cl_Ball (y,r2)) is compact non boundary by A9, Lm2;

      then ex h be Function of (TR | ( cl_Ball (x,(d + 1)))), (TR | ( cl_Ball (y,r2))) st h is being_homeomorphism & (h .: ( Fr ( cl_Ball (x,(d + 1))))) = ( Fr ( cl_Ball (y,r2))) by A15, BROUWER2: 7;

      then (( cl_Ball (x,(d + 1))),( cl_Ball (y,r2))) are_homeomorphic by T_0TOPSP:def 1, METRIZTS:def 1;

      then

       A17: ( ind ( cl_Ball (x,(d + 1)))) = ( ind ( cl_Ball (y,r2))) by TOPDIM_1: 27;

      ( Ball (x,(d + 1))) c= ( cl_Ball (x,(d + 1))) by TOPREAL9: 16;

      then ( ind ( Ball (x,(d + 1)))) <= ( ind ( cl_Ball (x,(d + 1)))) by TOPDIM_1: 19;

      then n <= ( ind ( cl_Ball (y,r2))) by A17, A14, XXREAL_0: 2;

      then

       A18: n <= ( ind A) by A16, XXREAL_0: 2;

      ( ind A) <= ( ind TR) by TOPDIM_1: 20;

      hence thesis by A6, XXREAL_0: 1, A18;

    end;

    ::$Notion-Name

    theorem :: BROUWER3:7

    

     Th7: r > 0 implies ( ind ( Sphere (p,r))) = (n - 1)

    proof

      set TR = ( TOP-REAL n);

      

       A1: ( ind A) <= i & ( ind B) <= i & A is closed implies ( ind (A \/ B)) <= i

      proof

        set TT = the TopStruct of TR;

        assume that

         A2: ( ind A) <= i and

         A3: ( ind B) <= i and

         A4: A is closed;

        reconsider a = A, b = B, AB = (A \/ B) as Subset of TT;

        

         A5: a is closed by A4, PRE_TOPC: 31;

        

         A6: (TT | AB) is second-countable;

        

         A7: TT = ( TopSpaceMetr ( Euclid n)) by EUCLID:def 8;

        

         A8: TT = (TR | ( [#] TR)) by TSEP_1: 93;

        then

         A9: ( ind b) <= i by TOPDIM_1: 22, A3;

        ( ind a) <= i by A8, TOPDIM_1: 22, A2;

        then ( ind AB) <= i by A9, A5, A8, A7, A6, TOPDIM_2: 5;

        hence thesis by TOPDIM_1: 22, A8;

      end;

      assume

       A10: r > 0 ;

      per cases by NAT_1: 25;

        suppose

         A11: n = 0 ;

        then

         A12: p = ( 0. TR) by EUCLID: 77;

        ( Sphere (p,r)) = {}

        proof

          assume ( Sphere (p,r)) <> {} ;

          then

          consider x be object such that

           A13: x in ( Sphere (p,r)) by XBOOLE_0:def 1;

          reconsider x as Point of TR by A13;

          x = ( 0. TR) by A11, EUCLID: 77

          .= ( 0* n) by EUCLID: 66;

          then |.x.| = 0 by EUCLID: 7;

          hence contradiction by A12, A13, TOPREAL9: 12, A10;

        end;

        hence thesis by TOPDIM_1: 6, A11;

      end;

        suppose

         A15: n = 1;

        then

        consider u be Real such that

         A16: p = <*u*> by JORDAN2B: 20;

        set u1 = |[(u - r)]|, u2 = |[(u + r)]|;

        ( card {u2}) = 1 by CARD_1: 30;

        then

         A17: ( ind {u2}) = 0 by TOPDIM_1: 8, NAT_1: 14;

        ( card {u1}) = 1 by CARD_1: 30;

        then ( ind {u1}) = 0 by TOPDIM_1: 8, NAT_1: 14;

        then

         A18: ( ind ( {u1} \/ {u2})) = 0 by A17, A15, A1;

         { <*(u qua ExtReal - r)*>, <*(u qua ExtReal + r)*>} = ( Fr ( Ball (p,r))) by A15, TOPDIM_2: 18, A16, A10

        .= ( Sphere (p,r)) by A15, A10, JORDAN: 24;

        hence thesis by A18, ENUMSET1: 1, A15;

      end;

        suppose

         A19: n > 1;

        then

        reconsider n1 = (n - 1) as Element of NAT by NAT_1: 20;

        reconsider n1 as non zero Element of NAT by A19;

        set n2 = (n1 + 1);

        set Tn1 = ( TOP-REAL n1), Tn2 = ( TOP-REAL n2), S = ( Sphere (( 0. Tn2),1));

        set Sp = { s where s be Point of Tn2 : (s . n2) >= 0 & |.s.| = 1 }, Sn = { t where t be Point of Tn2 : (t . n2) <= 0 & |.t.| = 1 };

        

         A20: Sp c= S

        proof

          let x be object;

          assume x in Sp;

          then

          consider s be Point of Tn2 such that

           A21: x = s and (s . n2) >= 0 and

           A22: |.s.| = 1;

          (s - ( 0. Tn2)) = s by RLVECT_1: 13;

          hence thesis by A22, A21;

        end;

        

         A23: ( [#] (TR | ( cl_Ball (p,r)))) = ( cl_Ball (p,r)) by PRE_TOPC:def 5;

        reconsider Spr = ( Sphere (p,r)) as Subset of (TR | ( cl_Ball (p,r))) by A23, TOPREAL9: 17;

        

         A24: ( cl_Ball (( 0. Tn2),1)) is compact non boundary by Lm2;

        ( cl_Ball (p,r)) is compact non boundary by Lm2, A10;

        then

        consider h be Function of (TR | ( cl_Ball (p,r))), (Tn2 | ( cl_Ball (( 0. Tn2),1))) such that

         A25: h is being_homeomorphism and

         A26: (h .: ( Fr ( cl_Ball (p,r)))) = ( Fr ( cl_Ball (( 0. Tn2),1))) by A24, BROUWER2: 7;

        

         A27: ( ind Spr) = ( ind (h .: Spr)) by A25, METRIZTS: 3, TOPDIM_1: 27;

        

         A28: Sn c= S

        proof

          let x be object;

          assume x in Sn;

          then

          consider s be Point of Tn2 such that

           A29: x = s and (s . n2) <= 0 and

           A30: |.s.| = 1;

          (s - ( 0. Tn2)) = s by RLVECT_1: 13;

          hence thesis by A30, A29;

        end;

        then

        reconsider Sp, Sn as Subset of ( TOP-REAL n2) by A20, XBOOLE_1: 1;

        

         A31: S c= (Sp \/ Sn)

        proof

          let x be object;

          assume

           A32: x in S;

          then

          reconsider x as Point of Tn2;

          

           A33: (x . n2) >= 0 or (x . n2) <= 0 ;

           |.x.| = 1 by A32, TOPREAL9: 12;

          then x in Sp or x in Sn by A33;

          hence thesis by XBOOLE_0:def 3;

        end;

        

         A34: Sn = { t where t be Point of ( TOP-REAL n2) : (t . n2) <= 0 & |.t.| = 1 };

        then

         A35: Sp is closed by Th2;

        

         A36: Sp = { s where s be Point of ( TOP-REAL n2) : (s . n2) >= 0 & |.s.| = 1 };

        

         A37: (Sp,( cl_Ball (( 0. Tn1),1))) are_homeomorphic & (Sn,( cl_Ball (( 0. Tn1),1))) are_homeomorphic

        proof

          set TD = ( Tdisk (( 0. Tn1),1));

          deffunc ff( Nat) = ( PROJ (n2,$1));

          consider FF be FinSequence such that

           A38: ( len FF) = n1 & for k be Nat st k in ( dom FF) holds (FF . k) = ff(k) from FINSEQ_1:sch 2;

          ( rng FF) c= ( Funcs (the carrier of Tn2,the carrier of R^1 ))

          proof

            let x be object;

            assume x in ( rng FF);

            then

            consider i be object such that

             A39: i in ( dom FF) and

             A40: (FF . i) = x by FUNCT_1:def 3;

            reconsider i as Nat by A39;

             ff(i) in ( Funcs (the carrier of Tn2,the carrier of R^1 )) by FUNCT_2: 8;

            hence thesis by A38, A39, A40;

          end;

          then

          reconsider FF as FinSequence of ( Funcs (the carrier of Tn2,the carrier of R^1 )) by FINSEQ_1:def 4;

          reconsider FF as Element of (n1 -tuples_on ( Funcs (the carrier of Tn2,the carrier of R^1 ))) by A38, FINSEQ_2: 92;

          set FFF = <:FF:>;

          

           A41: ( [#] TD) = ( cl_Ball (( 0. Tn1),1)) by PRE_TOPC:def 5;

          (FFF .: Sp) = ( cl_Ball (( 0. Tn1),1)) by A38, Th1, A34;

          then

           A42: ( rng (FFF | Sp)) c= the carrier of TD by RELAT_1: 115, A41;

          

           A43: ( dom FFF) = the carrier of Tn2 by FUNCT_2:def 1;

          then (Sn /\ ( dom FFF)) = Sn by XBOOLE_1: 28;

          then

           A44: ( dom (FFF | Sn)) = Sn by RELAT_1: 61;

          (Sp /\ ( dom FFF)) = Sp by A43, XBOOLE_1: 28;

          then

           A45: ( dom (FFF | Sp)) = Sp by RELAT_1: 61;

          ( [#] (Tn2 | Sp)) = Sp by PRE_TOPC:def 5;

          then

          reconsider Fsp = (FFF | Sp) as Function of (Tn2 | Sp), TD by A42, A45, FUNCT_2: 2;

          

           A46: ( [#] (Tn2 | Sn)) = Sn by PRE_TOPC:def 5;

          (FFF .: Sn) = ( cl_Ball (( 0. Tn1),1)) by A38, Th1, A36;

          then ( rng (FFF | Sn)) c= the carrier of TD by RELAT_1: 115, A41;

          then

          reconsider Fsn = (FFF | Sn) as Function of (Tn2 | Sn), TD by A46, FUNCT_2: 2, A44;

          

           A47: Fsn is being_homeomorphism by A38, Th1, A36;

          Fsp is being_homeomorphism by A38, Th1, A34;

          hence thesis by A47, T_0TOPSP:def 1, METRIZTS:def 1;

        end;

        

         A48: ( ind ( cl_Ball (( 0. Tn1),1))) = n1 by Lm2, Th6;

        then

         A49: ( ind Sp) = n1 by A37, TOPDIM_1: 27;

        Sp c= (Sp \/ Sn) by XBOOLE_1: 7;

        then

         A50: n1 <= ( ind (Sp \/ Sn)) by A49, TOPDIM_1: 19;

        ( ind Sn) = n1 by A37, A48, TOPDIM_1: 27;

        then ( ind (Sp \/ Sn)) <= n1 by A35, A49, A1;

        then

         A51: ( ind (Sp \/ Sn)) = n1 by A50, XXREAL_0: 1;

        ( Fr ( cl_Ball (p,r))) = ( Sphere (p,r)) by BROUWER2: 5, A10;

        then (h .: Spr) = S by A26, BROUWER2: 5;

        then

         A52: ( ind (h .: Spr)) = ( ind S) by TOPDIM_1: 21;

        (Sp \/ Sn) c= S by A20, A28, XBOOLE_1: 8;

        then ( ind S) = n1 by A31, XBOOLE_0:def 10, A51;

        hence thesis by TOPDIM_1: 21, A52, A27;

      end;

    end;

    begin

    theorem :: BROUWER3:8

    

     Th8: for p st n > 0 & p in A & for r st r > 0 holds ex U be open Subset of (( TOP-REAL n) | A) st p in U & U c= ( Ball (p,r)) & for f be Function of (( TOP-REAL n) | (A \ U)), ( Tunit_circle n) st f is continuous holds ex h be Function of (( TOP-REAL n) | A), ( Tunit_circle n) st h is continuous & (h | (A \ U)) = f holds p in ( Fr A)

    proof

      let p;

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

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

      set TS = ( Tunit_circle n);

      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 nN = (n NormF );

      set TRn0 = (TRn | cTR0);

      

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

      set G = ( transl (p,TRn));

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

      

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

      

       A4: (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

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

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

        x in ( dom nN) by A4, A5, 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 A4, A5, A6, FUNCT_1: 47

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

        then x = ( 0* n) by EUCLID: 8;

        then x = ( 0. TRn) by EUCLID: 70;

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

        hence contradiction by A3, A5, 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;

      

       A7: ( Int A) in the topology of TRn by PRE_TOPC:def 2;

      set En = ( Euclid n), TM = ( TopSpaceMetr En);

      assume that

       A8: p in A and

       A9: for r st r > 0 holds ex U be open Subset of (TRn | A) st p in U & U c= ( Ball (p,r)) & for f be Function of (TRn | (A \ U)), ( Tunit_circle n) st f is continuous holds ex h be Function of (TRn | A), ( Tunit_circle n) st h is continuous & (h | (A \ U)) = f;

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

      

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

      then

      reconsider IA = ( Int A) as Subset of TM;

      TS = ( Tcircle (( 0. TRn),1)) by TOPREALB:def 7;

      then TS = (TRn | S) by TOPREALB:def 6;

      then

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

      assume not p in ( Fr A);

      then p in (A \ ( Fr A)) by A8, XBOOLE_0:def 5;

      then p in ( Int A) by TOPS_1: 40;

      then

      consider r be Real such that

       A12: r > 0 and

       A13: ( Ball (e,r)) c= IA by A7, A10, PRE_TOPC:def 2, TOPMETR: 15;

      set r2 = (r / 2);

      consider U be open Subset of (TRn | A) such that

       A14: p in U and

       A15: U c= ( Ball (p,r2)) and

       A16: for f be Function of (TRn | (A \ U)), TS st f is continuous holds ex h be Function of (TRn | A), TS st h is continuous & (h | (A \ U)) = f by A12, A9;

      reconsider Sph = ( Sphere (p,r2)) as non empty Subset of TRn by A1, A12;

      consider au be object such that

       A17: au in Sph by XBOOLE_0:def 1;

      

       A18: n in NAT by ORDINAL1:def 12;

      

       A19: ( Ball (e,r)) = ( Ball (p,r)) by TOPREAL9: 13;

      

       A20: ( cl_Ball (p,r2)) c= ( Ball (p,r)) by JORDAN: 21, A18, A12, XREAL_1: 216;

      

       A21: Sph = (( cl_Ball (p,r2)) \ ( Ball (p,r2))) by JORDAN: 19, A18;

      then

       W: au in ( cl_Ball (p,r2)) by A17, XBOOLE_0:def 5;

      

       A22: au in IA by W, A20, A19, A13;

      reconsider r2 as non zero Real by A12;

      reconsider CL2 = ( cl_Ball (p,r2)) as non empty Subset of TRn by A12;

      

       A23: Sph c= CL2 by A21, XBOOLE_1: 36;

      ( [#] (TRn | CL2)) = CL2 by PRE_TOPC:def 5;

      then

      reconsider sph = Sph as non empty Subset of (TRn | CL2) by A21, XBOOLE_1: 36;

      

       A24: ((TRn | CL2) | sph) = (TRn | Sph) by PRE_TOPC: 7, A21, XBOOLE_1: 36;

       not au in U by A15, A21, A17, XBOOLE_0:def 5;

      then

      reconsider AU = (A \ U) as non empty Subset of TRn by A22, A2, XBOOLE_0:def 5;

      set TAU = (TRn | AU);

      set t = ( transl (( - p),TRn)), T = (t | TAU);

      

       A25: ( [#] TAU) = (A \ U) by PRE_TOPC:def 5;

      then

       A26: ( dom T) = (A \ U) by FUNCT_2:def 1;

      

       A27: T = (t | the carrier of TAU) by TMAP_1:def 4;

      

       A28: ( rng T) c= cTR0

      proof

        let y be object;

        assume y in ( rng T);

        then

        consider x be object such that

         A29: x in ( dom T) and

         A30: (T . x) = y by FUNCT_1:def 3;

        reconsider x as Point of TRn by A29, A26;

        

         A31: (T . x) = (t . x) by A29, A27, FUNCT_1: 47;

        

         A32: (t . x) = (x + ( - p)) by RLTOPSP1:def 10;

        assume not y in cTR0;

        then (T . x) in {( 0. TRn)} by A31, XBOOLE_0:def 5, A30;

        then (x - p) = ( 0. TRn) by TARSKI:def 1, A32, A31;

        then x = p by RLVECT_1: 21;

        hence thesis by A29, A25, XBOOLE_0:def 5, A14;

      end;

      then

      reconsider T0 = T as continuous Function of TAU, TRn0 by A26, FUNCT_2: 2, A3, A25, PRE_TOPC: 27;

      

       A33: ( [#] (TRn | Sph)) = Sph by PRE_TOPC:def 5;

      

       A34: CL2 c= IA by A20, A19, A13;

      

       A35: CL2 c= A by A2, A20, A19, A13;

      

       A36: ( dom b) = cTR0 by A3, FUNCT_2:def 1;

      

       A37: 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;

        

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

        assume

         A39: p in cTR0;

        then

         A40: (I . p) = p by A3, TMAP_1: 84;

        

         A41: (nN0 . p) = (nN . p) by A39, A3, A4, FUNCT_1: 49;

        

        thus (b . p) = ((I . p) (/) (nN0 . p)) by A36, A39, VALUED_2: 72

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

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

        

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

        

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

        .= 1 by A38, A42, TOPRNS_1: 24, XCMPLX_1: 87;

      end;

      ( rng b) c= S

      proof

        let y be object;

        assume y in ( rng b);

        then

        consider x be object such that

         A43: x in ( dom b) and

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

        reconsider x as Point of TRn by A36, A43;

        

         A45: |.((1 / |.x.|) * x).| = 1 by A3, A37, A43;

        

         A46: (((1 / |.x.|) * x) - ( 0. TRn)) = ((1 / |.x.|) * x) by RLVECT_1: 13;

        y = ((1 / |.x.|) * x) by A3, A37, A43, A44;

        hence thesis by A46, A45;

      end;

      then

      reconsider B = b as Function of TRn0, TS by A3, A11, A36, FUNCT_2: 2;

      

       A47: ( [#] ((TRn | CL2) | sph)) = sph by PRE_TOPC:def 5;

      set m = ( mlt (r2,TRn)), M = (m | TS);

      reconsider M = (m | TS) as continuous Function of TS, TRn by A1;

      

       A48: M = (m | the carrier of TS) by TMAP_1:def 4;

      

       A49: ( [#] (TRn | A)) = A by PRE_TOPC:def 5;

      then

      reconsider clB = CL2 as Subset of (TRn | A) by A34, A2, XBOOLE_1: 1;

      

       A50: ((TRn | A) | clB) = (TRn | CL2) by PRE_TOPC: 7, A34, A2, XBOOLE_1: 1;

      B is continuous by PRE_TOPC: 27;

      then (B * T0) is continuous by TOPS_2: 46;

      then

      consider h be Function of (TRn | A), TS such that

       A51: h is continuous and

       A52: (h | (A \ U)) = (B * T0) by A16;

      (M * h) is continuous Function of (TRn | A), TRn by A1, A51, TOPS_2: 46;

      then

      reconsider GHM = (G * (M * h)) as continuous Function of (TRn | A), TRn by TOPS_2: 46;

      

       A53: ( dom h) = the carrier of (TRn | A) by A1, FUNCT_2:def 1;

      

       A54: |.r2.| = r2 by A12, ABSVALUE:def 1;

      

       A55: ( rng GHM) c= Sph

      proof

        let y be object;

        assume y in ( rng GHM);

        then

        consider q be object such that

         A56: q in ( dom GHM) and

         A57: (GHM . q) = y by FUNCT_1:def 3;

        

         A58: y = (G . ((M * h) . q)) by A56, A57, FUNCT_1: 12;

        

         A59: q in A by A56, A49;

        

         A60: q in ( dom (M * h)) by A56, FUNCT_1: 11;

        then

         A61: q in ( dom h) by FUNCT_1: 11;

        

         A62: ((M * h) . q) = (M . (h . q)) by A60, FUNCT_1: 12;

        

         A63: (h . q) in ( dom M) by A60, FUNCT_1: 11;

        reconsider q as Point of TRn by A59;

        (h . q) in S by A63, A11;

        then

        reconsider hq = (h . q) as Point of TRn;

        

         A64: (m . (h . q)) = (r2 * hq) by RLTOPSP1:def 13;

        (M . (h . q)) = (m . (h . q)) by A63, A48, FUNCT_1: 47;

        then

         A65: y = (p + (r2 * hq)) by A58, A62, A64, RLTOPSP1:def 10;

        

         A66: ((p + (r2 * hq)) - p) = ((r2 * hq) + (p - p)) by RLVECT_1: 28

        .= ((r2 * hq) + ( 0. TRn)) by RLVECT_1: 15

        .= (r2 * hq) by RLVECT_1:def 4;

        

         A67: (h . q) in ( rng h) by FUNCT_1:def 3, A61;

         |.(r2 * hq).| = ( |.r2.| * |.hq.|) by EUCLID: 11

        .= ( |.r2.| * 1) by A67, A11, TOPREAL9: 12;

        hence thesis by A66, A65, A54;

      end;

      ( dom GHM) = A by A49, FUNCT_2:def 1;

      then

      reconsider ghm = GHM as Function of (TRn | A), (TRn | Sph) by A55, A49, A33, FUNCT_2: 2;

      ghm is continuous by PRE_TOPC: 27;

      then

      reconsider ghM = (ghm | ((TRn | A) | clB)) as continuous Function of (TRn | CL2), ((TRn | CL2) | sph) by A8, A50, A24;

      

       A68: ( dom ghM) = the carrier of (TRn | CL2) by FUNCT_2:def 1;

      

       A69: ghM = (ghm | the carrier of ((TRn | A) | clB)) by TMAP_1:def 4, A8;

      for w be Point of (TRn | CL2) st w in Sph holds (ghM . w) = w

      proof

        let w be Point of (TRn | CL2);

        assume

         A70: w in Sph;

        then

        reconsider q = w as Point of TRn;

        

         A71: w in CL2 by A70, A23;

        w in A by A35, A70, A23;

        then

         A72: q in ( dom GHM) by A49, FUNCT_2:def 1;

        then

         A73: q in ( dom (M * h)) by FUNCT_1: 11;

        then

         A74: ((M * h) . q) = (M . (h . q)) by FUNCT_1: 12;

         not q in U by A70, A21, XBOOLE_0:def 5, A15;

        then

         A75: q in (A \ U) by A71, A35, XBOOLE_0:def 5;

        then q in ((A \ U) /\ ( dom h)) by A71, A35, A53, A49, XBOOLE_0:def 4;

        then

         A76: q in ( dom (B * T0)) by A52, RELAT_1: 61;

        then

         A77: ((B * T0) . q) = (B . (T0 . q)) by FUNCT_1: 12;

        

         A78: (h . q) in ( dom M) by A73, FUNCT_1: 11;

        then

         A79: (M . (h . q)) = (m . (h . q)) by A48, FUNCT_1: 47;

        (t . q) = (q + ( - p)) by RLTOPSP1:def 10;

        then

         A80: (T . q) = (q - p) by A26, A27, A75, FUNCT_1: 47;

        q in ( dom T0) by A76, FUNCT_1: 11;

        then

         A81: (T . q) in ( rng T) by FUNCT_1:def 3;

        (h . q) in S by A78, A11;

        then

        reconsider hq = (h . q) as Point of TRn;

        (ghM . q) = (ghm . q) by A68, A69, FUNCT_1: 47;

        then

         A82: (ghM . q) = (G . ((M * h) . q)) by A72, FUNCT_1: 12;

        hq = ((B * T0) . q) by A76, A52, FUNCT_1: 47;

        then

         A83: hq = ((1 / |.(q - p).|) * (q - p)) by A80, A77, A37, A81, A28;

        (m . (h . q)) = (r2 * hq) by RLTOPSP1:def 13

        .= (r2 * ((1 / r2) * (q - p))) by A83, A70, TOPREAL9: 9

        .= ((r2 * (1 / r2)) * (q - p)) by RLVECT_1:def 7

        .= (1 * (q - p)) by XCMPLX_1: 106

        .= (q - p) by RLVECT_1:def 8;

        

        then (ghM . w) = (p + (q - p)) by A82, A74, A79, RLTOPSP1:def 10

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

        .= (q + ( 0. TRn)) by RLVECT_1:def 10

        .= q by RLVECT_1: 4;

        hence thesis;

      end;

      then

       A84: ghM is being_a_retraction by BORSUK_1:def 16, A33, A24;

      ( Ball (p,r2)) c= ( Int CL2) by TOPREAL9: 16, TOPS_1: 24;

      then

       A85: CL2 is non boundary by A12;

      ( Fr CL2) = Sph by A12, BROUWER2: 5;

      hence contradiction by A84, A85, A47, BROUWER2: 9, BORSUK_1:def 17;

    end;

    theorem :: BROUWER3:9

    

     Th9: for p st p in ( Fr A) & A is closed holds for r st r > 0 holds ex U be open Subset of (( TOP-REAL n) | A) st p in U & U c= ( Ball (p,r)) & for f be Function of (( TOP-REAL n) | (A \ U)), ( Tunit_circle n) st f is continuous holds ex h be Function of (( TOP-REAL n) | A), ( Tunit_circle n) st h is continuous & (h | (A \ U)) = f

    proof

      set TR = ( TOP-REAL n);

      let p;

      assume that

       A1: p in ( Fr A) and

       A2: A is closed;

      

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

      n > 0

      proof

        assume n <= 0 ;

        then n = 0 ;

        then

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

        ( [#] TR) is open;

        hence thesis by A4, A1, ZFMISC_1: 33;

      end;

      then

      reconsider n1 = (n - 1) as Element of NAT by NAT_1: 20;

      set TU = ( Tunit_circle n);

      

       A5: p is Element of ( REAL n) by EUCLID: 22;

      let r;

      assume

       A6: r > 0 ;

      set r3 = (r / 3), r2 = (2 * r3);

      set B = ( Ball (p,r3));

      p is Element of ( REAL n) by EUCLID: 22;

      then |.(p - p).| = 0 ;

      then p in B by A6;

      then (A ` ) meets B by A1, TOPS_1: 28;

      then

      consider x be object such that

       A7: x in (A ` ) and

       A8: x in B by XBOOLE_0: 3;

      reconsider x as Element of TR by A7;

      set u = ( Ball (x,r2)), clU = ( cl_Ball (x,r2));

      

       A9: n in NAT by ORDINAL1:def 12;

      

       A10: u c= clU by TOPREAL9: 16;

      

       A11: ( [#] (TR | A)) = A by PRE_TOPC:def 5;

      then

      reconsider U = (u /\ A) as Subset of (TR | A) by XBOOLE_1: 17;

      u in the topology of TR by PRE_TOPC:def 2;

      then U in the topology of (TR | A) by PRE_TOPC:def 4, A11;

      then

      reconsider U as open Subset of (TR | A) by PRE_TOPC:def 2;

      take U;

      x is Element of ( REAL n) by EUCLID: 22;

      then

       A12: |.(x - p).| = |.(p - x).| by EUCLID: 18, A5;

      ( |.(x - p).| + r2) < (r3 + r2) by A8, TOPREAL9: 7, XREAL_1: 6;

      then

       A13: u c= ( Ball (p,r)) by Th5;

      r2 > r3 by A6, XREAL_1: 155;

      then |.(x - p).| < r2 by A8, TOPREAL9: 7, XXREAL_0: 2;

      then

       A14: p in u by A12;

      hence p in U by A3, A1, XBOOLE_0:def 4;

      U c= u by XBOOLE_1: 17;

      hence U c= ( Ball (p,r)) by A13;

      let f be Function of (TR | (A \ U)), TU such that

       A15: f is continuous;

      per cases ;

        suppose

         A16: (A \ U) is empty;

        set h = the continuous Function of (TR | A), ( Tunit_circle (n1 + 1));

        reconsider H = h as Function of (( TOP-REAL n) | A), TU;

        take H;

        f = {} by A16;

        hence thesis by A16;

      end;

        suppose

         A17: (A \ U) is non empty;

        set S = ( Sphere (x,r2));

        reconsider AUS = ((A \ U) \/ S) as non empty Subset of TR by A17;

        

         A18: (TR | AUS) is metrizable & (TR | AUS) is finite-ind second-countable

        proof

          reconsider aus = AUS as Subset of the TopStruct of TR;

          

           A19: the TopStruct of TR = ( TopSpaceMetr ( Euclid n)) by EUCLID:def 8;

          (TR | AUS) = ( the TopStruct of TR | aus) by PRE_TOPC: 36;

          hence thesis by A19;

        end;

        

         A20: ( [#] (TR | AUS)) = AUS by PRE_TOPC:def 5;

        then

        reconsider AU = (A \ U), SS = S as Subset of (TR | AUS) by XBOOLE_1: 7;

        (AU ` ) = (AUS \ AU) by SUBSET_1:def 4, A20

        .= (S \ AU) by XBOOLE_1: 40;

        then

         A21: (AU ` ) c= SS by XBOOLE_1: 36;

        ( ind S) = n1 by A6, Th7;

        then ( ind SS) = n1 by TOPDIM_1: 21;

        then

         A22: ( ind (AU ` )) <= n1 by TOPDIM_1: 19, A21;

        

         A23: (TR | (A \ U)) = ((TR | AUS) | AU) by A20, PRE_TOPC: 7;

        then

        reconsider F = f as Function of ((TR | AUS) | AU), TU;

        (A \ U) = (A \ u) by XBOOLE_1: 47;

        then

         A24: (A \ U) is closed by A2, YELLOW_8: 20;

        then AU is closed by TSEP_1: 8;

        then

        consider g be continuous Function of (TR | AUS), ( Tunit_circle (n1 + 1)) such that

         A25: (g | AU) = F by Th3, A23, A15, A18, A22;

        

         A26: ( [#] (TR | A)) = A by PRE_TOPC:def 5;

        then

        reconsider AclU = (A /\ clU), au = (A \ U) as Subset of (TR | A) by XBOOLE_1: 17, XBOOLE_1: 36;

        set T3 = ((TR | A) | AclU), T4 = ((TR | A) | au);

        

         A27: ((A /\ U) \/ au) = A by XBOOLE_1: 51;

        (A ` ) = (( [#] TR) \ A) by SUBSET_1:def 4;

        then not x in A by A7, XBOOLE_0:def 5;

        then

        consider h be Function of (TR | A), (TR | S) such that

         A28: h is continuous and

         A29: (h | S) = ( id (A /\ S)) by A6, Th4;

        

         A30: (n1 + 1) = n;

        then

         A31: ( dom h) = the carrier of (TR | A) by A6, FUNCT_2:def 1;

        

         A32: ( [#] (TR | S)) = S by PRE_TOPC:def 5;

        then ( rng h) c= the carrier of TR by XBOOLE_1: 1;

        then

        reconsider h1 = h as Function of (TR | A), TR by A31, FUNCT_2: 2;

        

         A33: S c= AUS by XBOOLE_1: 7;

        ( rng h) c= ( [#] (TR | S));

        then

        reconsider h2 = h1 as Function of (TR | A), (TR | AUS) by A33, A32, XBOOLE_1: 1, A31, FUNCT_2: 2, A20;

        h1 is continuous by A28, PRE_TOPC: 26;

        then

         A34: h2 is continuous by PRE_TOPC: 27;

        set T2 = ((TR | AUS) | AU);

        

         A35: ((TR | AUS) | AU) = (TR | (A \ U)) by PRE_TOPC: 7, XBOOLE_1: 7;

        

         A36: (clU \ u) = S by JORDAN: 19, A9;

        

         A37: ((A /\ A) /\ u) = (A /\ (A /\ u)) by XBOOLE_1: 16;

        

         A38: (g | T2) = (g | the carrier of T2) by TMAP_1:def 4;

        ((TR | A) | au) = (TR | (A \ U)) by XBOOLE_1: 36, PRE_TOPC: 7;

        then

        reconsider gT2 = (g | T2) as continuous Function of T4, ( Tunit_circle (n1 + 1)) by A35, A17;

        

         A39: ( [#] T3) = AclU by PRE_TOPC:def 5;

        AclU is non empty by A10, A14, A3, A1, XBOOLE_0:def 4;

        then

        reconsider gh2T3 = (g * (h2 | T3)) as continuous Function of T3, ( Tunit_circle (n1 + 1)) by A34;

        

         A40: ( [#] T4) = au by PRE_TOPC:def 5;

        

         A41: (h2 | T3) = (h2 | the carrier of T3) by A3, A1, TMAP_1:def 4;

         A42:

        now

          let x be object such that

           A43: x in (( dom gh2T3) /\ ( dom gT2));

          

           A44: not x in U by A43, A40, XBOOLE_0:def 5;

          x in A by A43, A40, XBOOLE_0:def 5;

          then

           A45: not x in u by A44, XBOOLE_0:def 4;

          

           A46: x in ( dom gh2T3) by A43, XBOOLE_0:def 4;

          then x in clU by A39, XBOOLE_0:def 4;

          then

           A47: x in S by A45, A36, XBOOLE_0:def 5;

          

           A48: x in ( dom gT2) by A43, XBOOLE_0:def 4;

          x in A by A46, A39, XBOOLE_0:def 4;

          then

           A49: x in (A /\ S) by A47, XBOOLE_0:def 4;

          x in ( dom (h2 | T3)) by A46, FUNCT_1: 11;

          

          then ((h2 | T3) . x) = (h2 . x) by A41, FUNCT_1: 47

          .= ((h | S) . x) by A47, FUNCT_1: 49

          .= x by A29, A49, FUNCT_1: 17;

          

          hence (gh2T3 . x) = (g . x) by A46, FUNCT_1: 12

          .= (gT2 . x) by A38, A48, FUNCT_1: 47;

        end;

        

         A50: AclU is closed by A2, TSEP_1: 8;

        au is closed by A24, TSEP_1: 8;

        then

        reconsider G = (gh2T3 +* gT2) as continuous Function of ((TR | A) | (AclU \/ au)), ( Tunit_circle (n1 + 1)) by A50, A42, PARTFUN1:def 4, TOPGEN_5: 10;

        

         W: (A /\ u) c= AclU by TOPREAL9: 16, XBOOLE_1: 26;

        A = (AclU \/ au) by A26, W, A27, A37, XBOOLE_1: 9;

        then

         A51: ((TR | A) | (AclU \/ au)) = (TR | A) by A26, TSEP_1: 93;

        then

        reconsider GG = G as Function of (TR | A), TU;

        take GG;

        thus GG is continuous by A51;

        

         A52: ( [#] (TR | (A \ U))) = (A \ U) by PRE_TOPC:def 5;

        

         A53: ( dom gT2) = the carrier of T4 by FUNCT_2:def 1;

         A54:

        now

          let x;

          assume

           A55: x in ( dom f);

          

          hence ((GG | (A \ U)) . x) = (GG . x) by A52, FUNCT_1: 49

          .= (gT2 . x) by FUNCT_4: 13, A55, A52, A40, A53

          .= (g . x) by A38, A40, A52, A53, A55, FUNCT_1: 47

          .= (f . x) by A25, A55, A52, FUNCT_1: 49;

        end;

        ( dom GG) = A by A26, FUNCT_2:def 1;

        

        then

         A56: ( dom (GG | (A \ U))) = (A /\ (A \ U)) by RELAT_1: 61

        .= (A \ U) by XBOOLE_1: 36, XBOOLE_1: 28;

        ( dom f) = (A \ U) by A30, A52, FUNCT_2:def 1;

        hence thesis by A54, A56;

      end;

    end;

    

     Lm3: for A,B be Subset of ( TOP-REAL n) st n = 0 holds for h be Function of (( TOP-REAL n) | A), (( TOP-REAL n) | B) st h is being_homeomorphism holds for p be Point of ( TOP-REAL n) holds (p in ( Fr A) implies (h . p) in ( Fr B)) & (p in ( Int A) implies (h . p) in ( Int B))

    proof

      set TR = ( TOP-REAL n);

      

       A1: ( Int ( [#] TR)) = ( [#] TR) by TOPS_1: 15;

      let A,B be Subset of TR such that

       A2: n = 0 ;

      

       A3: the carrier of TR = {( 0. TR)} by A2, EUCLID: 77, EUCLID: 22;

      let h be Function of (TR | A), (TR | B) such that

       A4: h is being_homeomorphism;

      

       A5: ( dom h) = ( [#] (TR | A)) by A4, TOPS_2:def 5;

      let p be Point of TR;

      ( [#] TR) is open;

      hence p in ( Fr A) implies (h . p) in ( Fr B) by A3, ZFMISC_1: 33;

      

       A6: A = ( [#] (TR | A)) by PRE_TOPC:def 5;

      

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

      assume p in ( Int A);

      then

       A8: (h . p) in ( rng h) by A7, A5, A6, FUNCT_1:def 3;

      

       A9: B = ( [#] (TR | B)) by PRE_TOPC:def 5;

      then B = ( [#] TR) by A8, ZFMISC_1: 33, A3;

      hence thesis by A8, A1, A9;

    end;

    begin

    theorem :: BROUWER3:10

    

     Th10: A is closed & p in ( Fr A) implies for h be Function of (( TOP-REAL n) | A), (( TOP-REAL n) | B) st h is being_homeomorphism holds (h . p) in ( Fr B)

    proof

      set TRn = ( TOP-REAL n);

      assume that

       A1: A is closed and

       A2: p in ( Fr A);

      

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

      let h be Function of (TRn | A), (TRn | B) such that

       A4: h is being_homeomorphism;

      

       A5: ( [#] (TRn | A)) = A by PRE_TOPC:def 5;

      then

       A6: ( dom h) = A by A4, TOPS_2:def 5;

      then

       A7: (h . p) in ( rng h) by A3, A2, FUNCT_1:def 3;

      

       A8: ( [#] (TRn | B)) = B by PRE_TOPC:def 5;

      then

       A9: ( rng h) = B by A4, TOPS_2:def 5;

      then

      reconsider hp = (h . p) as Point of TRn by A7;

      per cases ;

        suppose n = 0 ;

        hence thesis by Lm3, A4, A2;

      end;

        suppose

         A10: n > 0 ;

        then

        reconsider n1 = (n - 1) as Element of NAT by NAT_1: 20;

        

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

        for r st r > 0 holds ex U be open Subset of (TRn | B) st hp in U & U c= ( Ball (hp,r)) & for f be Function of (TRn | (B \ U)), ( Tunit_circle n) st f is continuous holds ex h be Function of (TRn | B), ( Tunit_circle n) st h is continuous & (h | (B \ U)) = f

        proof

          reconsider P = p as Point of ( Euclid n) by A11, TOPMETR: 12;

          let r such that

           A13: r > 0 ;

          reconsider BB = (B /\ ( Ball (hp,r))) as Subset of (TRn | B) by A8, XBOOLE_1: 17;

          ( Ball (hp,r)) in the topology of TRn by PRE_TOPC:def 2;

          then BB in the topology of (TRn | B) by A8, PRE_TOPC:def 4;

          then

          reconsider BB as open Subset of (TRn | B) by PRE_TOPC:def 2;

          (h " BB) is open by A7, A4, A8, TOPS_2: 43;

          then (h " BB) in the topology of (TRn | A) by PRE_TOPC:def 2;

          then

          consider U be Subset of TRn such that

           A14: U in the topology of TRn and

           A15: (h " BB) = (U /\ ( [#] (TRn | A))) by PRE_TOPC:def 4;

          reconsider U as open Subset of TRn by A14, PRE_TOPC:def 2;

          

           A16: ( Int U) = U by TOPS_1: 23;

          hp is Element of ( REAL n) by EUCLID: 22;

          then |.(hp - hp).| = 0 ;

          then hp in ( Ball (hp,r)) by A13;

          then hp in BB by A7, A8, XBOOLE_0:def 4;

          then p in (h " BB) by A3, A2, A6, FUNCT_1:def 7;

          then p in U by A15, XBOOLE_0:def 4;

          then

          consider s be Real such that

           A17: s > 0 and

           A18: ( Ball (P,s)) c= U by A16, GOBOARD6: 5;

          consider W be open Subset of (TRn | A) such that

           A19: p in W and

           A20: W c= ( Ball (p,s)) and

           A21: for f be Function of (TRn | (A \ W)), ( Tunit_circle n) st f is continuous holds ex h be Function of (( TOP-REAL n) | A), ( Tunit_circle n) st h is continuous & (h | (A \ W)) = f by A1, A17, Th9, A2;

          ( Ball (p,s)) = ( Ball (P,s)) by TOPREAL9: 13;

          then

           A22: (( Ball (p,s)) /\ A) c= (U /\ A) by A18, XBOOLE_1: 27;

          (W /\ A) = W by A5, XBOOLE_1: 28;

          then W c= (( Ball (p,s)) /\ A) by A20, XBOOLE_1: 27;

          then W c= (U /\ A) by A22;

          then (h .: W) c= (h .: (U /\ A)) by RELAT_1: 123;

          then

           A23: (h .: W) c= BB by FUNCT_1: 77, A8, A9, A15, A5;

          (TRn | B) is non empty by A3, A2, A6;

          then

          reconsider hW = (h .: W) as open Subset of (TRn | B) by A3, A2, A4, TOPGRP_1: 25;

          take hW;

          BB c= ( Ball (hp,r)) by XBOOLE_1: 17;

          hence hp in hW & hW c= ( Ball (hp,r)) by A3, A2, A6, FUNCT_1:def 6, A19, A23;

          set AW = (A \ W), haw = (h | AW), T = ( Tunit_circle n);

          

           A24: ( [#] (TRn | (B \ hW))) = (B \ hW) by PRE_TOPC:def 5;

          reconsider aw = AW as Subset of (TRn | A) by XBOOLE_1: 36, A5;

          let f be Function of (TRn | (B \ hW)), T such that

           A25: f is continuous;

          per cases ;

            suppose

             A26: (B \ hW) is empty;

            set h = the continuous Function of (TRn | B), ( Tunit_circle (n1 + 1));

            reconsider H = h as Function of (( TOP-REAL n) | B), T;

            take H;

            f = {} by A26;

            hence thesis by A26;

          end;

            suppose

             A27: (B \ hW) is non empty;

            set AW = (A \ W), haw = (h | AW), T = ( Tunit_circle n);

            reconsider haw as Function of ((TRn | A) | aw), ((TRn | B) | (h .: AW)) by A3, A2, A7, JORDAN24: 12;

            

             A28: (h .: AW) = ((h .: A) \ (h .: W)) by A4, FUNCT_1: 64

            .= (B \ hW) by RELAT_1: 113, A6, A9;

            then

             A29: ((TRn | B) | (h .: AW)) = (TRn | (B \ hW)) by XBOOLE_1: 36, PRE_TOPC: 7;

            

             A30: ((TRn | A) | aw) = (TRn | AW) by PRE_TOPC: 7, XBOOLE_1: 36;

            then

            reconsider HAW = haw as Function of (TRn | AW), (TRn | (B \ hW)) by A29;

            reconsider fhW = (f * HAW) as Function of (TRn | AW), ( Tunit_circle n) by A27;

            fhW is continuous by A27, JORDAN24: 13, A4, A3, A2, A7, A29, A30, A25, TOPS_2: 46;

            then

            consider HW be Function of (TRn | A), T such that

             A31: HW is continuous and

             A32: (HW | AW) = fhW by A21;

            reconsider HWh = (HW * (h " )) as Function of (TRn | B), T by A3, A2;

            take HWh;

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

            hence HWh is continuous by TOPS_2: 46, A3, A2, A31;

            

             A33: ( dom f) = (B \ hW) by A10, A24, FUNCT_2:def 1;

            

             A34: ( rng ((h " ) | (B \ hW))) = ((h " ) .: (B \ hW)) by RELAT_1: 115

            .= (h " (h .: AW)) by A28, A8, A9, A4, TOPS_2: 55

            .= AW by FUNCT_1: 94, A6, A4, XBOOLE_1: 36;

            

            thus (HWh | (B \ hW)) = (HW * ((h " ) | (B \ hW))) by RELAT_1: 83

            .= (HW * (( id AW) * ((h " ) | (B \ hW)))) by A34, RELAT_1: 53

            .= ((HW * ( id AW)) * ((h " ) | (B \ hW))) by RELAT_1: 36

            .= ((HW | AW) * ((h " ) | (B \ hW))) by RELAT_1: 65

            .= (((f * h) | AW) * ((h " ) | (B \ hW))) by A32, RELAT_1: 83

            .= (((f * h) * ( id AW)) * ((h " ) | (B \ hW))) by RELAT_1: 65

            .= ((f * h) * (( id AW) * ((h " ) | (B \ hW)))) by RELAT_1: 36

            .= ((f * h) * ((h " ) | (B \ hW))) by A34, RELAT_1: 53

            .= (((f * h) * (h " )) | (B \ hW)) by RELAT_1: 83

            .= ((f * (h * (h " ))) | (B \ hW)) by RELAT_1: 36

            .= ((f * ( id B)) | (B \ hW)) by TOPS_2: 52, A9, A4, A8

            .= (f | ( dom f)) by A33, XBOOLE_1: 36, RELAT_1: 51

            .= f;

          end;

        end;

        hence thesis by Th8, A7, A8, A10;

      end;

    end;

    theorem :: BROUWER3:11

    

     Th11: B is closed & p in ( Int A) implies for h be Function of (( TOP-REAL n) | A), (( TOP-REAL n) | B) st h is being_homeomorphism holds (h . p) in ( Int B)

    proof

      set TRn = ( TOP-REAL n), T = ( Tunit_circle n);

      assume that

       A1: B is closed and

       A2: p in ( Int A);

      

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

      

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

      let h be Function of (TRn | A), (TRn | B) such that

       A5: h is being_homeomorphism;

      

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

      

       A7: ( [#] (TRn | A)) = A by PRE_TOPC:def 5;

      then

       A8: ( dom h) = A by A5, TOPS_2:def 5;

      

       A9: ( [#] (TRn | B)) = B by PRE_TOPC:def 5;

      then

       A10: ( rng h) = B by A5, TOPS_2:def 5;

      per cases ;

        suppose n = 0 ;

        hence thesis by Lm3, A2, A5;

      end;

        suppose

         A11: n > 0 ;

        

         A12: (h . p) in ( rng h) by A2, A3, A8, FUNCT_1:def 3;

        then

        reconsider hp = (h . p) as Point of TRn by A10;

        ex r st r > 0 & for U be open Subset of (TRn | B) st hp in U & U c= ( Ball (hp,r)) holds ex f be Function of (TRn | (B \ U)), T st f is continuous & for h be Function of (TRn | B), T st h is continuous holds (h | (B \ U)) <> f

        proof

          reconsider hP = hp as Point of ( Euclid n) by A4, TOPMETR: 12;

           not p in ( Fr A) by A2, TOPS_1: 39, XBOOLE_0: 3;

          then

          consider r such that

           A14: r > 0 and

           A15: for U be open Subset of (TRn | A) st p in U & U c= ( Ball (p,r)) holds ex f be Function of (TRn | (A \ U)), T st f is continuous & for h be Function of (TRn | A), T st h is continuous holds (h | (A \ U)) <> f by A11, A2, A3, Th8;

          reconsider BA = (( Ball (p,r)) /\ A) as Subset of (TRn | A) by A7, XBOOLE_1: 17;

          ( Ball (p,r)) in the topology of TRn by PRE_TOPC:def 2;

          then BA in the topology of (TRn | A) by A7, PRE_TOPC:def 4;

          then

          reconsider BA as open Subset of (TRn | A) by PRE_TOPC:def 2;

          (h .: BA) is open by A5, A2, A3, A12, TOPGRP_1: 25;

          then (h .: BA) in the topology of (TRn | B) by PRE_TOPC:def 2;

          then

          consider U be Subset of TRn such that

           A16: U in the topology of TRn and

           A17: (h .: BA) = (U /\ ( [#] (TRn | B))) by PRE_TOPC:def 4;

          reconsider U as open Subset of TRn by A16, PRE_TOPC:def 2;

          

           A18: ( Int U) = U by TOPS_1: 23;

          p is Element of ( REAL n) by EUCLID: 22;

          then |.(p - p).| = 0 ;

          then p in ( Ball (p,r)) by A14;

          then p in BA by A2, A3, XBOOLE_0:def 4;

          then hp in (h .: BA) by A7, A8, FUNCT_1:def 6;

          then hp in U by A17, XBOOLE_0:def 4;

          then

          consider s be Real such that

           A19: s > 0 and

           A20: ( Ball (hP,s)) c= U by A18, GOBOARD6: 5;

          take s;

          thus s > 0 by A19;

          let W be open Subset of (TRn | B) such that

           A21: hp in W and

           A22: W c= ( Ball (hp,s));

          

           A23: (W /\ B) = W by A9, XBOOLE_1: 28;

          ( Ball (hp,s)) = ( Ball (hP,s)) by TOPREAL9: 13;

          then W c= U by A22, A20;

          then

           A24: W c= (U /\ B) by A23, XBOOLE_1: 27;

          (h " (U /\ B)) = (h " (h .: BA)) by A17, PRE_TOPC:def 5

          .= BA by FUNCT_1: 94, XBOOLE_1: 17, A8, A5;

          then

           A25: (h " W) c= BA by A24, RELAT_1: 143;

          reconsider hW = (h " W) as open Subset of (TRn | A) by TOPS_2: 43, A5, A9, A12;

          

           A26: BA c= ( Ball (p,r)) by XBOOLE_1: 17;

          set BW = (B \ W);

          reconsider bw = BW as Subset of (TRn | B) by XBOOLE_1: 36, A9;

          

           A27: ( [#] (TRn | (A \ hW))) = (A \ hW) by PRE_TOPC:def 5;

          p in (h " W) by A8, A2, A3, A21, FUNCT_1:def 7;

          then

          consider F be Function of (TRn | (A \ hW)), T such that

           A28: F is continuous and

           A29: for h be Function of (TRn | A), T st h is continuous holds (h | (A \ hW)) <> F by A15, A25, A26, XBOOLE_1: 1;

          

           A30: BW c= B by XBOOLE_1: 36;

          

          then

           A31: ((h " ) .: BW) = (h " BW) by TOPS_2: 55, A9, A10, A5

          .= ((h " B) \ hW) by FUNCT_1: 69

          .= (A \ hW) by RELAT_1: 134, A8, A10;

          per cases ;

            suppose

             A32: (A \ hW) is empty;

            reconsider n1 = (n - 1) as Element of NAT by NAT_1: 20, A11;

            set h = the continuous Function of (TRn | A), ( Tunit_circle (n1 + 1));

            reconsider H = h as Function of (TRn | A), T;

            

             A33: (H | (A \ hW)) = {} by A32;

            (H | (A \ hW)) <> F by A29;

            hence thesis by A33, A32;

          end;

            suppose

             A34: (A \ hW) is non empty;

            reconsider hbw = ((h " ) | (B \ W)) as Function of ((TRn | B) | bw), ((TRn | A) | ((h " ) .: BW)) by A2, A3, A12, JORDAN24: 12;

            

             A35: ((TRn | B) | bw) = (TRn | BW) by PRE_TOPC: 7, XBOOLE_1: 36;

            

             A36: ((TRn | A) | ((h " ) .: BW)) = (TRn | (A \ hW)) by A31, PRE_TOPC: 7, A7;

            then

            reconsider HBW = hbw as Function of (TRn | BW), (TRn | (A \ hW)) by A35;

            reconsider fhW = (F * HBW) as Function of (TRn | BW), ( Tunit_circle n) by A34;

            take fhW;

            thus fhW is continuous by A34, JORDAN24: 13, A6, A2, A3, A12, A36, A35, A28, TOPS_2: 46;

            let g be Function of (TRn | B), T such that

             A37: g is continuous;

            reconsider gh = (g * h) as Function of (TRn | A), T by A12;

            

             A38: gh is continuous by A5, A12, A37, TOPS_2: 46;

            assume

             A39: (g | BW) = fhW;

            

             A40: ( dom F) = (A \ hW) by FUNCT_2:def 1, A11, A27;

            

             A41: ( rng (h | (A \ hW))) = (h .: (A \ hW)) by RELAT_1: 115

            .= (h .: (h " BW)) by TOPS_2: 55, A9, A10, A31, A5, A30

            .= BW by FUNCT_1: 77, A10, XBOOLE_1: 36;

            (gh | (A \ hW)) = (g * (h | (A \ hW))) by RELAT_1: 83

            .= (g * (( id BW) * (h | (A \ hW)))) by A41, RELAT_1: 53

            .= ((g * ( id BW)) * (h | (A \ hW))) by RELAT_1: 36

            .= ((g | BW) * (h | (A \ hW))) by RELAT_1: 65

            .= (F * (((h " ) | (B \ W)) * (h | (A \ hW)))) by A39, RELAT_1: 36

            .= (F * (((h " ) * ( id BW)) * (h | (A \ hW)))) by RELAT_1: 65

            .= (F * ((h " ) * (( id BW) * (h | (A \ hW))))) by RELAT_1: 36

            .= (F * ((h " ) * (h | (A \ hW)))) by A41, RELAT_1: 53

            .= (F * (((h " ) * h) | (A \ hW))) by RELAT_1: 83

            .= ((F * ((h " ) * h)) | (A \ hW)) by RELAT_1: 83

            .= ((F * ( id A)) | (A \ hW)) by TOPS_2: 52, A8, A10, A5, A9

            .= (F | ( dom F)) by A40, XBOOLE_1: 36, RELAT_1: 51

            .= F;

            hence contradiction by A38, A29;

          end;

        end;

        then not hp in ( Fr B) by A1, Th9;

        then hp in (B \ ( Fr B)) by A12, A9, XBOOLE_0:def 5;

        hence thesis by TOPS_1: 40;

      end;

    end;

    theorem :: BROUWER3:12

    A is closed & B is closed implies for h be Function of (( TOP-REAL n) | A), (( TOP-REAL n) | B) st h is being_homeomorphism holds (h .: ( Int A)) = ( Int B) & (h .: ( Fr A)) = ( Fr B)

    proof

      assume that

       A1: A is closed and

       A2: B is closed;

      set TR = ( TOP-REAL n);

      

       A3: ( [#] (TR | A)) = A by PRE_TOPC:def 5;

      

       A4: ( Int B) c= B by TOPS_1: 16;

      

       A5: ( [#] (TR | B)) = B by PRE_TOPC:def 5;

      let h be Function of (TR | A), (TR | B) such that

       A6: h is being_homeomorphism;

      

       A7: ( dom h) = ( [#] (TR | A)) by A6, TOPS_2:def 5;

      

       A8: ( rng h) = ( [#] (TR | B)) by A6, TOPS_2:def 5;

      

       A9: (( Fr A) \/ ( Int A)) = ((A \ ( Int A)) \/ ( Int A)) by A1, TOPS_1: 43

      .= (A \/ ( Int A)) by XBOOLE_1: 39

      .= A by TOPS_1: 16, XBOOLE_1: 12;

      thus

       A10: (h .: ( Int A)) = ( Int B)

      proof

        thus (h .: ( Int A)) c= ( Int B)

        proof

          let y be object;

          assume y in (h .: ( Int A));

          then ex x be object st x in ( dom h) & x in ( Int A) & (h . x) = y by FUNCT_1:def 6;

          hence thesis by A2, A6, Th11;

        end;

        let y be object;

        assume

         A11: y in ( Int B);

        then

        consider x be object such that

         A12: x in ( dom h) and

         A13: (h . x) = y by A4, A8, A5, FUNCT_1:def 3;

        reconsider x as Point of TR by A7, A3, A12;

        assume

         A14: not y in (h .: ( Int A));

         not x in ( Int A) by A12, FUNCT_1:def 6, A14, A13;

        then x in ( Fr A) by A12, A9, A3, XBOOLE_0:def 3;

        then (h . x) in ( Fr B) by Th10, A1, A6;

        hence thesis by A11, A13, TOPS_1: 39, XBOOLE_0: 3;

      end;

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

      

      then (h .: ( Fr A)) = ((h .: A) \ (h .: ( Int A))) by A6, FUNCT_1: 64

      .= (B \ (h .: ( Int A))) by RELAT_1: 113, A7, A8, A3, A5

      .= ( Fr B) by A10, A2, TOPS_1: 43;

      hence thesis;

    end;

    begin

    theorem :: BROUWER3:13

    

     Th13: for r st r > 0 holds for U be Subset of ( Tdisk (p,r)) st U is open non empty holds for A be Subset of ( TOP-REAL n) st A = U holds ( Int A) is non empty

    proof

      set TR = ( TOP-REAL n);

      let r be Real such that

       A1: r > 0 ;

      let U be Subset of ( Tdisk (p,r)) such that

       A2: U is open non empty;

      consider q be object such that

       A3: q in U by A2;

      

       A4: ( [#] ( Tdisk (p,r))) = ( cl_Ball (p,r)) by PRE_TOPC:def 5;

      then q in ( cl_Ball (p,r)) by A3;

      then

      reconsider q as Point of TR;

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

      then

      reconsider Q = q as Point of ( Euclid n) by TOPMETR: 12;

      

       A5: |.(q - p).| <= r by A3, A4, TOPREAL9: 8;

      U in the topology of ( Tdisk (p,r)) by A2, PRE_TOPC:def 2;

      then

      consider W be Subset of TR such that

       A6: W in the topology of TR and

       A7: U = (W /\ ( [#] ( Tdisk (p,r)))) by PRE_TOPC:def 4;

      reconsider W as open Subset of TR by A6, PRE_TOPC:def 2;

      ( Int W) = W by TOPS_1: 23;

      then q in ( Int W) by A3, A7, XBOOLE_0:def 4;

      then

      consider s be Real such that

       A8: s > 0 and

       A9: ( Ball (Q,s)) c= W by GOBOARD6: 5;

      set m = ( min (s,r)), mr = (m / (2 * r));

      

       A10: 0 < m by A8, A1, XXREAL_0: 21;

      then

       A11: (m / 2) < m by XREAL_1: 216;

      set qp = ((( - mr) * (q - p)) + q);

      

       A12: (qp - q) = ((( - mr) * (q - p)) + (q - q)) by RLVECT_1:def 3

      .= ((( - mr) * (q - p)) + ( 0. TR)) by RLVECT_1:def 10

      .= (( - mr) * (q - p)) by RLVECT_1:def 4;

       |.( - mr).| = ( - ( - mr)) by A10, A1, ABSVALUE:def 1;

      then

       A13: |.(qp - q).| = (mr * |.(q - p).|) by A12, EUCLID: 11;

      (mr * r) = (((m / 2) / r) * r) by XCMPLX_1: 78

      .= ((m / 2) * (r / r))

      .= ((m / 2) * 1) by XCMPLX_1: 60, A1

      .= (m / 2);

      then |.(qp - q).| <= (m / 2) by A5, XREAL_1: 66, A10, A13;

      then

       A14: |.(qp - q).| < m by A11, XXREAL_0: 2;

      m <= s by XXREAL_0: 17;

      then |.(qp - q).| < s by A14, XXREAL_0: 2;

      then

       A15: qp in ( Ball (q,s));

      let A be Subset of TR such that

       A16: A = U;

      

       A17: ( Ball (p,r)) c= ( cl_Ball (p,r)) by TOPREAL9: 16;

      

       A18: (( - mr) + 1) < ( 0 + 1) by XREAL_1: 8, A10, A1;

      

       A19: ((1 - mr) * |.(q - p).|) < r

      proof

        per cases ;

          suppose |.(q - p).| = 0 ;

          hence thesis by A1;

        end;

          suppose |.(q - p).| > 0 ;

          then ((1 - mr) * |.(q - p).|) < (1 * |.(q - p).|) by A18, XREAL_1: 68;

          hence thesis by A5, XXREAL_0: 2;

        end;

      end;

      

       A20: (r / (2 * r)) = ((r / r) / 2) by XCMPLX_1: 78

      .= (1 / 2) by XCMPLX_1: 60, A1;

      mr <= (r / (2 * r)) by A1, XXREAL_0: 17, XREAL_1: 72;

      then (1 - mr) >= (1 - (1 / 2)) by A20, XREAL_1: 10;

      then

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

      (qp - p) = ((( - mr) * (q - p)) + (q - p)) by RLVECT_1:def 3

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

      .= ((1 - mr) * (q - p)) by RLVECT_1:def 6;

      then |.(qp - p).| < r by A19, A21, EUCLID: 11;

      then qp in ( Ball (p,r));

      then

       A22: qp in (( Ball (q,s)) /\ ( Ball (p,r))) by A15, XBOOLE_0:def 4;

      ( Ball (q,s)) c= W by A9, TOPREAL9: 13;

      hence thesis by A17, XBOOLE_1: 27, A7, A4, A16, A22, TOPS_1: 22;

    end;

    theorem :: BROUWER3:14

    for T be non empty TopSpace holds for A,B be Subset of T holds for r, s st r > 0 & s > 0 holds for pA be Point of ( TOP-REAL n), pB be Point of ( TOP-REAL m) st ((T | A),( Tdisk (pA,r))) are_homeomorphic & ((T | B),( Tdisk (pB,s))) are_homeomorphic & ( Int A) meets ( Int B) holds n = m

    proof

      let T be non empty TopSpace;

      let A,B be Subset of T;

      let r,s be Real such that

       A1: r > 0 and

       A2: s > 0 ;

      

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

      

       A4: (( Int A) /\ ( Int B)) c= ( Int B) by XBOOLE_1: 17;

      

       A5: ( [#] (T | B)) = B by PRE_TOPC:def 5;

      then

      reconsider IB = (( Int A) /\ ( Int B)) as Subset of (T | B) by A3, A4, XBOOLE_1: 1;

      let pA be Point of ( TOP-REAL n), pB be Point of ( TOP-REAL m) such that

       A6: ((T | A),( Tdisk (pA,r))) are_homeomorphic and

       A7: ((T | B),( Tdisk (pB,s))) are_homeomorphic and

       A8: ( Int A) meets ( Int B);

      consider hB be Function of (T | B), ( Tdisk (pB,s)) such that

       A9: hB is being_homeomorphism by A7, T_0TOPSP:def 1;

      

       A10: ((T | B) | IB) = (T | (( Int A) /\ ( Int B))) by A3, A4, XBOOLE_1: 1, PRE_TOPC: 7;

      

       A11: ( [#] ( Tdisk (pB,s))) = ( cl_Ball (pB,s)) by PRE_TOPC:def 5;

      then

      reconsider hBI = (hB .: IB) as Subset of ( TOP-REAL m) by XBOOLE_1: 1;

      

       A12: (( Int A) /\ ( Int B)) in the topology of T by PRE_TOPC:def 2;

      (( Int A) /\ ( Int B)) is non empty by A8;

      then

      consider p be set such that

       A13: p in (( Int A) /\ ( Int B));

      reconsider p as Point of T by A13;

      

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

      then

       A15: (hB . p) in (hB .: IB) by A13, FUNCT_1:def 6;

      p in ( Int B) by A13, XBOOLE_0:def 4;

      then ( Tdisk (pB,s)) is non empty by A14, A3;

      then

      reconsider f = (hB | IB) as Function of ((T | B) | IB), (( Tdisk (pB,s)) | (hB .: IB)) by A13, JORDAN24: 12;

      

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

      (IB /\ B) = IB by A3, A4, XBOOLE_1: 1, XBOOLE_1: 28;

      then IB in the topology of (T | B) by A12, A5, PRE_TOPC:def 4;

      then IB is open by PRE_TOPC:def 2;

      then (hB .: IB) is open by A13, A9, TOPGRP_1: 25, A2;

      then ( Int hBI) is non empty by A13, A2, Th13;

      then hBI is non boundary;

      then

       A17: ( ind hBI) = m by Th6;

      

       A18: (( Int A) /\ ( Int B)) c= ( Int A) by XBOOLE_1: 17;

      

       A19: (( Tdisk (pB,s)) | (hB .: IB)) = (( TOP-REAL m) | hBI) by PRE_TOPC: 7, A11;

      then

      reconsider F = f as Function of (T | (( Int A) /\ ( Int B))), (( TOP-REAL m) | hBI) by A10;

      F is being_homeomorphism by A9, METRIZTS: 2, A19, A10;

      then

       A20: (F " ) is being_homeomorphism by TOPS_2: 56, A15;

      consider hA be Function of (T | A), ( Tdisk (pA,r)) such that

       A21: hA is being_homeomorphism by A6, T_0TOPSP:def 1;

      

       A22: ( [#] (T | A)) = A by PRE_TOPC:def 5;

      then

      reconsider IA = (( Int A) /\ ( Int B)) as Subset of (T | A) by A16, A18, XBOOLE_1: 1;

      

       A23: ((T | A) | IA) = (T | (( Int A) /\ ( Int B))) by A16, A18, XBOOLE_1: 1, PRE_TOPC: 7;

      

       A24: ( dom hA) = ( [#] (T | A)) by A21, TOPS_2:def 5;

      then

       A25: (hA . p) in (hA .: IA) by A13, FUNCT_1:def 6;

      p in ( Int A) by A13, XBOOLE_0:def 4;

      then ( Tdisk (pA,r)) is non empty by A24, A16;

      then

      reconsider g = (hA | IA) as Function of ((T | A) | IA), (( Tdisk (pA,r)) | (hA .: IA)) by A13, JORDAN24: 12;

      

       A26: ( [#] ( Tdisk (pA,r))) = ( cl_Ball (pA,r)) by PRE_TOPC:def 5;

      then

      reconsider hAI = (hA .: IA) as Subset of ( TOP-REAL n) by XBOOLE_1: 1;

      

       A27: (( Tdisk (pA,r)) | (hA .: IA)) = (( TOP-REAL n) | hAI) by PRE_TOPC: 7, A26;

      then

      reconsider G = g as Function of (T | (( Int A) /\ ( Int B))), (( TOP-REAL n) | hAI) by A23;

      reconsider GF = (G * (F " )) as Function of (( TOP-REAL m) | hBI), (( TOP-REAL n) | hAI) by A13;

      G is being_homeomorphism by A21, METRIZTS: 2, A27, A23;

      then GF is being_homeomorphism by A20, TOPS_2: 57, A25, A15, A13;

      then (hBI,hAI) are_homeomorphic by T_0TOPSP:def 1, METRIZTS:def 1;

      then

       A28: ( ind hBI) = ( ind hAI) by TOPDIM_1: 27;

      (IA /\ A) = IA by A16, A18, XBOOLE_1: 1, XBOOLE_1: 28;

      then IA in the topology of (T | A) by A12, A22, PRE_TOPC:def 4;

      then IA is open by PRE_TOPC:def 2;

      then (hA .: IA) is open by A13, A21, TOPGRP_1: 25, A1;

      then ( Int hAI) is non empty by A13, A1, Th13;

      then hAI is non boundary;

      hence thesis by A17, Th6, A28;

    end;

    theorem :: BROUWER3:15

    for T be non empty TopSpace holds for A,B be Subset of T holds for r, s st r > 0 & s > 0 holds for pA be Point of ( TOP-REAL n), pB be Point of ( TOP-REAL m) st ((T | A),(( TOP-REAL n) | ( Ball (pA,r)))) are_homeomorphic & ((T | B),( Tdisk (pB,s))) are_homeomorphic & ( Int A) meets ( Int B) holds n = m

    proof

      let T be non empty TopSpace;

      let A,B be Subset of T;

      let r,s be Real such that

       A1: r > 0 and

       A2: s > 0 ;

      let pA be Point of ( TOP-REAL n), pB be Point of ( TOP-REAL m) such that

       A3: ((T | A),(( TOP-REAL n) | ( Ball (pA,r)))) are_homeomorphic and

       A4: ((T | B),( Tdisk (pB,s))) are_homeomorphic and

       A5: ( Int A) meets ( Int B);

      

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

      set TBALL = (( TOP-REAL n) | ( Ball (pA,r)));

      consider hA be Function of (T | A), TBALL such that

       A7: hA is being_homeomorphism by A3, T_0TOPSP:def 1;

      

       A8: (( Int A) /\ ( Int B)) c= ( Int A) by XBOOLE_1: 17;

      

       A9: ( [#] (T | A)) = A by PRE_TOPC:def 5;

      then

      reconsider IA = (( Int A) /\ ( Int B)) as Subset of (T | A) by A6, A8, XBOOLE_1: 1;

      

       A10: ((T | A) | IA) = (T | (( Int A) /\ ( Int B))) by A6, A8, XBOOLE_1: 1, PRE_TOPC: 7;

      

       A11: ( [#] TBALL) = ( Ball (pA,r)) by PRE_TOPC:def 5;

      then

      reconsider hAI = (hA .: IA) as Subset of ( TOP-REAL n) by XBOOLE_1: 1;

      

       A12: (( Int A) /\ ( Int B)) in the topology of T by PRE_TOPC:def 2;

      (( Int A) /\ ( Int B)) is non empty by A5;

      then

      consider p be set such that

       A13: p in (( Int A) /\ ( Int B));

      reconsider p as Point of T by A13;

      

       A14: ( dom hA) = ( [#] (T | A)) by A7, TOPS_2:def 5;

      then

       A15: (hA . p) in (hA .: IA) by A13, FUNCT_1:def 6;

      p in ( Int A) by A13, XBOOLE_0:def 4;

      then TBALL is non empty by A14, A6;

      then

      reconsider g = (hA | IA) as Function of ((T | A) | IA), (TBALL | (hA .: IA)) by A13, JORDAN24: 12;

      

       A16: ( Int B) c= B by TOPS_1: 16;

      (IA /\ A) = IA by A6, A8, XBOOLE_1: 1, XBOOLE_1: 28;

      then IA in the topology of (T | A) by A12, A9, PRE_TOPC:def 4;

      then IA is open by PRE_TOPC:def 2;

      then (hA .: IA) is open by A13, A7, TOPGRP_1: 25, A1;

      then hAI is open by A11, TSEP_1: 9;

      then ( Int hAI) is non empty by TOPS_1: 23, A15;

      then

       A17: hAI is non boundary;

      consider hB be Function of (T | B), ( Tdisk (pB,s)) such that

       A18: hB is being_homeomorphism by A4, T_0TOPSP:def 1;

      

       A19: (TBALL | (hA .: IA)) = (( TOP-REAL n) | hAI) by PRE_TOPC: 7, A11;

      then

      reconsider G = g as Function of (T | (( Int A) /\ ( Int B))), (( TOP-REAL n) | hAI) by A10;

      

       A20: (( Int A) /\ ( Int B)) c= ( Int B) by XBOOLE_1: 17;

      

       A21: ( [#] (T | B)) = B by PRE_TOPC:def 5;

      then

      reconsider IB = (( Int A) /\ ( Int B)) as Subset of (T | B) by A16, A20, XBOOLE_1: 1;

      

       A22: ((T | B) | IB) = (T | (( Int A) /\ ( Int B))) by A16, A20, XBOOLE_1: 1, PRE_TOPC: 7;

      

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

      then

       A24: (hB . p) in (hB .: IB) by A13, FUNCT_1:def 6;

      p in ( Int B) by A13, XBOOLE_0:def 4;

      then ( Tdisk (pB,s)) is non empty by A23, A16;

      then

      reconsider f = (hB | IB) as Function of ((T | B) | IB), (( Tdisk (pB,s)) | (hB .: IB)) by A13, JORDAN24: 12;

      

       A25: ( [#] ( Tdisk (pB,s))) = ( cl_Ball (pB,s)) by PRE_TOPC:def 5;

      then

      reconsider hBI = (hB .: IB) as Subset of ( TOP-REAL m) by XBOOLE_1: 1;

      

       A26: (( Tdisk (pB,s)) | (hB .: IB)) = (( TOP-REAL m) | hBI) by PRE_TOPC: 7, A25;

      then

      reconsider F = f as Function of (T | (( Int A) /\ ( Int B))), (( TOP-REAL m) | hBI) by A22;

      F is being_homeomorphism by A18, METRIZTS: 2, A26, A22;

      then

       A27: (F " ) is being_homeomorphism by TOPS_2: 56, A24;

      reconsider GF = (G * (F " )) as Function of (( TOP-REAL m) | hBI), (( TOP-REAL n) | hAI) by A13;

      G is being_homeomorphism by A7, METRIZTS: 2, A19, A10;

      then GF is being_homeomorphism by A27, TOPS_2: 57, A15, A24, A13;

      then (hBI,hAI) are_homeomorphic by T_0TOPSP:def 1, METRIZTS:def 1;

      then

       A28: ( ind hBI) = ( ind hAI) by TOPDIM_1: 27;

      (IB /\ B) = IB by A16, A20, XBOOLE_1: 1, XBOOLE_1: 28;

      then IB in the topology of (T | B) by A12, A21, PRE_TOPC:def 4;

      then IB is open by PRE_TOPC:def 2;

      then (hB .: IB) is open by A13, A18, TOPGRP_1: 25, A2;

      then ( Int hBI) is non empty by A13, A2, Th13;

      then hBI is non boundary;

      then ( ind hBI) = m by Th6;

      hence thesis by A17, Th6, A28;

    end;

    theorem :: BROUWER3:16

    

     Th15: (( transl (p,( TOP-REAL n))) .: ( Ball (q,r))) = ( Ball ((q + p),r)) & (( transl (p,( TOP-REAL n))) .: ( cl_Ball (q,r))) = ( cl_Ball ((q + p),r)) & (( transl (p,( TOP-REAL n))) .: ( Sphere (q,r))) = ( Sphere ((q + p),r))

    proof

      set TR = ( TOP-REAL n), T = ( transl (p,TR));

       A2:

      now

        let q;

        ((q - p) + p) = (q - (p - p)) by RLVECT_1: 29

        .= (q - ( 0. TR)) by RLVECT_1:def 10

        .= q by RLVECT_1: 13;

        hence (( transl (p,TR)) . (q - p)) = q by RLTOPSP1:def 10;

      end;

       A3:

      now

        let x be Point of TR;

        

        thus ((x + p) - (q + p)) = (((x + p) - p) - q) by RLVECT_1: 27

        .= ((x + (p - p)) - q) by RLVECT_1: 28

        .= ((x + ( 0. TR)) - q) by RLVECT_1:def 10

        .= (x - q) by RLVECT_1:def 4;

      end;

      

       A4: ( dom T) = ( [#] TR) by FUNCT_2:def 1;

      thus (T .: ( Ball (q,r))) = ( Ball ((q + p),r))

      proof

        thus (T .: ( Ball (q,r))) c= ( Ball ((q + p),r))

        proof

          let y be object;

          assume y in (( transl (p,TR)) .: ( Ball (q,r)));

          then

          consider x be object such that

           A5: x in ( dom T) and

           A6: x in ( Ball (q,r)) and

           A7: (T . x) = y by FUNCT_1:def 6;

          reconsider x as Point of TR by A5;

          

           A8: y = (x + p) by A7, RLTOPSP1:def 10;

          

           A9: ((x + p) - (q + p)) = (x - q) by A3;

           |.(x - q).| < r by A6, TOPREAL9: 7;

          hence thesis by A9, A8;

        end;

        let y be object;

        assume

         A10: y in ( Ball ((q + p),r));

        then

        reconsider y as Point of TR;

        

         A11: ((y - p) - q) = (y - (p + q)) by RLVECT_1: 27;

         |.(y - (q + p)).| < r by A10, TOPREAL9: 7;

        then

         A12: (y - p) in ( Ball (q,r)) by A11;

        (T . (y - p)) = y by A2;

        hence thesis by A12, A4, FUNCT_1:def 6;

      end;

      thus (T .: ( cl_Ball (q,r))) = ( cl_Ball ((q + p),r))

      proof

        thus (T .: ( cl_Ball (q,r))) c= ( cl_Ball ((q + p),r))

        proof

          let y be object;

          assume y in (T .: ( cl_Ball (q,r)));

          then

          consider x be object such that

           A13: x in ( dom T) and

           A14: x in ( cl_Ball (q,r)) and

           A15: (T . x) = y by FUNCT_1:def 6;

          reconsider x as Point of TR by A13;

          

           A16: y = (x + p) by A15, RLTOPSP1:def 10;

          

           A17: ((x + p) - (q + p)) = (x - q) by A3;

           |.(x - q).| <= r by A14, TOPREAL9: 8;

          hence thesis by A17, A16;

        end;

        let y be object;

        assume

         A18: y in ( cl_Ball ((q + p),r));

        then

        reconsider y as Point of TR;

        

         A19: ((y - p) - q) = (y - (p + q)) by RLVECT_1: 27;

         |.(y - (q + p)).| <= r by A18, TOPREAL9: 8;

        then

         A20: (y - p) in ( cl_Ball (q,r)) by A19;

        (T . (y - p)) = y by A2;

        hence thesis by A20, A4, FUNCT_1:def 6;

      end;

      thus (T .: ( Sphere (q,r))) c= ( Sphere ((q + p),r))

      proof

        let y be object;

        assume y in (T .: ( Sphere (q,r)));

        then

        consider x be object such that

         A21: x in ( dom T) and

         A22: x in ( Sphere (q,r)) and

         A23: (T . x) = y by FUNCT_1:def 6;

        reconsider x as Point of TR by A21;

        

         A24: y = (x + p) by A23, RLTOPSP1:def 10;

        

         A25: ((x + p) - (q + p)) = (x - q) by A3;

         |.(x - q).| = r by A22, TOPREAL9: 9;

        hence thesis by A25, A24;

      end;

      let y be object;

      assume

       A26: y in ( Sphere ((q + p),r));

      then

      reconsider y as Point of TR;

      

       A27: ((y - p) - q) = (y - (p + q)) by RLVECT_1: 27;

       |.(y - (q + p)).| = r by A26, TOPREAL9: 9;

      then

       A28: (y - p) in ( Sphere (q,r)) by A27;

      (T . (y - p)) = y by A2;

      hence thesis by A28, A4, FUNCT_1:def 6;

    end;

    theorem :: BROUWER3:17

    

     Th16: for s st s > 0 holds (( mlt (s,( TOP-REAL n))) .: ( Ball (p,r))) = ( Ball ((s * p),(r * s))) & (( mlt (s,( TOP-REAL n))) .: ( cl_Ball (p,r))) = ( cl_Ball ((s * p),(r * s))) & (( mlt (s,( TOP-REAL n))) .: ( Sphere (p,r))) = ( Sphere ((s * p),(r * s)))

    proof

      let s such that

       A1: s > 0 ;

      set TR = ( TOP-REAL n), M = ( mlt (s,TR)), ss = |.s.|, s1 = (1 / s);

      

       A2: ss = s by A1, ABSVALUE:def 1;

      

       A4: ( dom M) = ( [#] TR) by FUNCT_2:def 1;

      

       A5: (s * s1) = 1 by A1, XCMPLX_1: 87;

      thus (M .: ( Ball (p,r))) = ( Ball ((s * p),(r * s)))

      proof

        thus (M .: ( Ball (p,r))) c= ( Ball ((s * p),(r * s)))

        proof

          let y be object;

          assume y in (M .: ( Ball (p,r)));

          then

          consider x be object such that

           A6: x in ( dom M) and

           A7: x in ( Ball (p,r)) and

           A8: (M . x) = y by FUNCT_1:def 6;

          reconsider q = x as Point of TR by A6;

          

           A9: y = (s * q) by A8, RLTOPSP1:def 13;

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

          then

           A10: |.((s * q) - (s * p)).| = (s * |.(q - p).|) by A2, EUCLID: 11;

          (s * |.(q - p).|) < (r * s) by A7, TOPREAL9: 7, A1, XREAL_1: 68;

          hence thesis by A10, A9;

        end;

        let y be object;

        

         A11: ((r * s) * s1) = (r * (s * s1));

        assume

         A12: y in ( Ball ((s * p),(r * s)));

        then

        reconsider q = y as Point of TR;

        

         A13: (( |.((s1 * q) - p).| * s) * s1) = ( |.((s1 * q) - p).| * (s * s1));

        

         A14: (s * (s1 * q)) = ((s * s1) * q) by RLVECT_1:def 7

        .= (1 * q) by A1, XCMPLX_1: 87

        .= q by RLVECT_1:def 8;

        

        then |.(q - (s * p)).| = |.(s * ((s1 * q) - p)).| by RLVECT_1: 34

        .= (s * |.((s1 * q) - p).|) by A2, EUCLID: 11;

        then |.((s1 * q) - p).| < r by A11, A13, A5, A12, TOPREAL9: 7, A1, XREAL_1: 68;

        then

         A15: (s1 * q) in ( Ball (p,r));

        (M . (s1 * q)) = q by A14, RLTOPSP1:def 13;

        hence thesis by A4, A15, FUNCT_1:def 6;

      end;

      thus (M .: ( cl_Ball (p,r))) = ( cl_Ball ((s * p),(r * s)))

      proof

        thus (M .: ( cl_Ball (p,r))) c= ( cl_Ball ((s * p),(r * s)))

        proof

          let y be object;

          assume y in (M .: ( cl_Ball (p,r)));

          then

          consider x be object such that

           A16: x in ( dom M) and

           A17: x in ( cl_Ball (p,r)) and

           A18: (M . x) = y by FUNCT_1:def 6;

          reconsider q = x as Point of TR by A16;

          

           A19: y = (s * q) by A18, RLTOPSP1:def 13;

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

          then

           A20: |.((s * q) - (s * p)).| = (s * |.(q - p).|) by A2, EUCLID: 11;

          (s * |.(q - p).|) <= (r * s) by A17, TOPREAL9: 8, A1, XREAL_1: 64;

          hence thesis by A20, A19;

        end;

        let y be object;

        

         A21: ((r * s) * s1) = (r * (s * s1));

        assume

         A22: y in ( cl_Ball ((s * p),(r * s)));

        then

        reconsider q = y as Point of TR;

        

         A23: (( |.((s1 * q) - p).| * s) * s1) = ( |.((s1 * q) - p).| * (s * s1));

        

         A24: (s * (s1 * q)) = ((s * s1) * q) by RLVECT_1:def 7

        .= (1 * q) by A1, XCMPLX_1: 87

        .= q by RLVECT_1:def 8;

        

        then |.(q - (s * p)).| = |.(s * ((s1 * q) - p)).| by RLVECT_1: 34

        .= (s * |.((s1 * q) - p).|) by A2, EUCLID: 11;

        then |.((s1 * q) - p).| <= r by A21, A23, A5, A22, TOPREAL9: 8, A1, XREAL_1: 64;

        then

         A25: (s1 * q) in ( cl_Ball (p,r));

        (M . (s1 * q)) = q by A24, RLTOPSP1:def 13;

        hence thesis by A4, A25, FUNCT_1:def 6;

      end;

      thus (M .: ( Sphere (p,r))) c= ( Sphere ((s * p),(r * s)))

      proof

        let y be object;

        assume y in (M .: ( Sphere (p,r)));

        then

        consider x be object such that

         A26: x in ( dom M) and

         A27: x in ( Sphere (p,r)) and

         A28: (M . x) = y by FUNCT_1:def 6;

        reconsider q = x as Point of TR by A26;

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

        then

         A29: |.((s * q) - (s * p)).| = (s * |.(q - p).|) by A2, EUCLID: 11;

        (s * |.(q - p).|) = (r * s) by A27, TOPREAL9: 9;

        then (s * q) in ( Sphere ((s * p),(r * s))) by A29;

        hence thesis by A28, RLTOPSP1:def 13;

      end;

      let y be object;

      assume

       A30: y in ( Sphere ((s * p),(r * s)));

      then

      reconsider q = y as Point of TR;

      

       A31: (( |.((s1 * q) - p).| * s) * s1) = ( |.((s1 * q) - p).| * (s * s1));

      

       A32: ((r * s) * s1) = (r * (s * s1));

      

       A33: (s * (s1 * q)) = ((s * s1) * q) by RLVECT_1:def 7

      .= (1 * q) by A1, XCMPLX_1: 87

      .= q by RLVECT_1:def 8;

      

      then |.(q - (s * p)).| = |.(s * ((s1 * q) - p)).| by RLVECT_1: 34

      .= (s * |.((s1 * q) - p).|) by A2, EUCLID: 11;

      then |.((s1 * q) - p).| = r by A32, A31, A5, A30, TOPREAL9: 9;

      then

       A34: (s1 * q) in ( Sphere (p,r));

      (M . (s1 * q)) = q by A33, RLTOPSP1:def 13;

      hence thesis by A4, A34, FUNCT_1:def 6;

    end;

    theorem :: BROUWER3:18

    

     Th17: for f be rotation homogeneous additive Function of ( TOP-REAL n), ( TOP-REAL n) st f is onto holds (f .: ( Ball (p,r))) = ( Ball ((f . p),r)) & (f .: ( cl_Ball (p,r))) = ( cl_Ball ((f . p),r)) & (f .: ( Sphere (p,r))) = ( Sphere ((f . p),r))

    proof

      set TR = ( TOP-REAL n);

      let f be rotation homogeneous additive Function of TR, TR;

      assume f is onto;

      

       A2: ( - (f . p)) = (( - 1) * (f . p)) by RLVECT_1: 16

      .= (f . (( - 1) * p)) by TOPREAL9:def 4

      .= (f . ( - p)) by RLVECT_1: 16;

      

       A3: ( rng f) = the carrier of TR by FUNCT_2:def 3;

      thus (f .: ( Ball (p,r))) = ( Ball ((f . p),r))

      proof

        thus (f .: ( Ball (p,r))) c= ( Ball ((f . p),r))

        proof

          let y be object;

          assume y in (f .: ( Ball (p,r)));

          then

          consider x be object such that

           A4: x in ( dom f) and

           A5: x in ( Ball (p,r)) and

           A6: (f . x) = y by FUNCT_1:def 6;

          reconsider q = x as Point of TR by A4;

          ((f . q) - (f . p)) = (f . (q - p)) by A2, VECTSP_1:def 20;

          then

           A7: |.((f . q) - (f . p)).| = |.(q - p).| by MATRTOP3:def 4;

           |.(q - p).| < r by A5, TOPREAL9: 7;

          hence thesis by A7, A6;

        end;

        let y be object;

        assume

         A8: y in ( Ball ((f . p),r));

        then

        consider x be object such that

         A9: x in ( dom f) and

         A10: (f . x) = y by A3, FUNCT_1:def 3;

        reconsider x as Point of TR by A9;

        ((f . x) - (f . p)) = (f . (x - p)) by A2, VECTSP_1:def 20;

        then

         A11: |.((f . x) - (f . p)).| = |.(x - p).| by MATRTOP3:def 4;

         |.((f . x) - (f . p)).| < r by A8, A10, TOPREAL9: 7;

        then x in ( Ball (p,r)) by A11;

        hence thesis by A9, A10, FUNCT_1:def 6;

      end;

      thus (f .: ( cl_Ball (p,r))) = ( cl_Ball ((f . p),r))

      proof

        thus (f .: ( cl_Ball (p,r))) c= ( cl_Ball ((f . p),r))

        proof

          let y be object;

          assume y in (f .: ( cl_Ball (p,r)));

          then

          consider x be object such that

           A12: x in ( dom f) and

           A13: x in ( cl_Ball (p,r)) and

           A14: (f . x) = y by FUNCT_1:def 6;

          reconsider q = x as Point of TR by A12;

          ((f . q) - (f . p)) = (f . (q - p)) by A2, VECTSP_1:def 20;

          then

           A15: |.((f . q) - (f . p)).| = |.(q - p).| by MATRTOP3:def 4;

           |.(q - p).| <= r by A13, TOPREAL9: 8;

          hence thesis by A15, A14;

        end;

        let y be object;

        assume

         A16: y in ( cl_Ball ((f . p),r));

        then

        consider x be object such that

         A17: x in ( dom f) and

         A18: (f . x) = y by A3, FUNCT_1:def 3;

        reconsider x as Point of TR by A17;

        ((f . x) - (f . p)) = (f . (x - p)) by A2, VECTSP_1:def 20;

        then

         A19: |.((f . x) - (f . p)).| = |.(x - p).| by MATRTOP3:def 4;

         |.((f . x) - (f . p)).| <= r by A16, A18, TOPREAL9: 8;

        then x in ( cl_Ball (p,r)) by A19;

        hence thesis by A17, A18, FUNCT_1:def 6;

      end;

      thus (f .: ( Sphere (p,r))) c= ( Sphere ((f . p),r))

      proof

        let y be object;

        assume y in (f .: ( Sphere (p,r)));

        then

        consider x be object such that

         A20: x in ( dom f) and

         A21: x in ( Sphere (p,r)) and

         A22: (f . x) = y by FUNCT_1:def 6;

        reconsider q = x as Point of TR by A20;

        ((f . q) - (f . p)) = (f . (q - p)) by A2, VECTSP_1:def 20;

        then

         A23: |.((f . q) - (f . p)).| = |.(q - p).| by MATRTOP3:def 4;

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

        hence thesis by A23, A22;

      end;

      let y be object;

      assume

       A24: y in ( Sphere ((f . p),r));

      then

      consider x be object such that

       A25: x in ( dom f) and

       A26: (f . x) = y by A3, FUNCT_1:def 3;

      reconsider x as Point of TR by A25;

      ((f . x) - (f . p)) = (f . (x - p)) by A2, VECTSP_1:def 20;

      then

       A27: |.((f . x) - (f . p)).| = |.(x - p).| by MATRTOP3:def 4;

       |.((f . x) - (f . p)).| = r by A24, A26, TOPREAL9: 9;

      then x in ( Sphere (p,r)) by A27;

      hence thesis by A25, A26, FUNCT_1:def 6;

    end;

    

     Lm4: for n be non zero Element of NAT holds for p be Point of ( TOP-REAL (n + 1)) st r <= 1 & |.p.| >= 1 & |.p.| < (1 + r) & (p . (n + 1)) > 0 & (p | n) = ( 0* n) holds ex c be Real, h be Function of (( TOP-REAL (n + 1)) | (( Sphere (( 0. ( TOP-REAL (n + 1))),1)) /\ ( cl_Ball (p,r)))), ( Tdisk (( 0. ( TOP-REAL n)),c)) st c > 0 & h is being_homeomorphism & (h .: (( Sphere (( 0. ( TOP-REAL (n + 1))),1)) /\ ( Sphere (p,r)))) = ( Sphere (( 0. ( TOP-REAL n)),c))

    proof

      let n be non zero Element of NAT ;

      set n1 = (n + 1);

      set TR = ( TOP-REAL n), TR1 = ( TOP-REAL n1);

      set Sp = { q where q be Point of TR1 : (q . n1) >= 0 & |.q.| = 1 };

      set Sn = { q where q be Point of TR1 : (q . n1) <= 0 & |.q.| = 1 };

      

       A1: Sp c= the carrier of TR1

      proof

        let x be object;

        assume x in Sp;

        then ex p be Point of TR1 st p = x & (p . n1) >= 0 & |.p.| = 1;

        hence thesis;

      end;

      Sn c= the carrier of TR1

      proof

        let x be object;

        assume x in Sn;

        then ex p be Point of TR1 st p = x & (p . n1) <= 0 & |.p.| = 1;

        hence thesis;

      end;

      then

      reconsider Sp, Sn as Subset of TR1 by A1;

      deffunc f( Nat) = ( PROJ (n1,$1));

      consider F be FinSequence such that

       A2: ( len F) = n & for k be Nat st k in ( dom F) holds (F . k) = f(k) from FINSEQ_1:sch 2;

      ( rng F) c= ( Funcs (the carrier of TR1,the carrier of R^1 ))

      proof

        let x be object;

        assume x in ( rng F);

        then

        consider i be object such that

         A3: i in ( dom F) and

         A4: (F . i) = x by FUNCT_1:def 3;

        reconsider i as Nat by A3;

         f(i) in ( Funcs (the carrier of TR1,the carrier of R^1 )) by FUNCT_2: 8;

        hence thesis by A2, A3, A4;

      end;

      then

      reconsider F as FinSequence of ( Funcs (the carrier of TR1,the carrier of R^1 )) by FINSEQ_1:def 4;

      reconsider F as Element of (n -tuples_on ( Funcs (the carrier of TR1,the carrier of R^1 ))) by A2, FINSEQ_2: 92;

      set FF = <:F:>;

      let p be Point of TR1 such that

       A5: r <= 1 and

       A6: |.p.| >= 1 and

       A7: |.p.| < (1 + r) and

       A8: (p . n1) > 0 and

       A9: (p | n) = ( 0* n);

      set pn1 = (p . n1);

      

       A10: (1 + 0 ) < (1 + (pn1 * pn1)) by A8, XREAL_1: 6;

      ( rng p) c= REAL ;

      then

       A11: p is FinSequence of REAL by FINSEQ_1:def 4;

      ( len p) = n1 by CARD_1:def 7;

      then

      reconsider P = p as Element of ( REAL n1) by A11, FINSEQ_2: 92;

       |.(P | n).| = 0 by A9, EUCLID: 7;

      then ( |.(P | n).| ^2 ) = 0 ;

      then ( |.p.| ^2 ) = ( 0 + (pn1 ^2 )) by REAL_NS1: 10;

      then

       A12: |.p.| = pn1 or |.p.| = ( - pn1) by SQUARE_1: 40;

      then

       A13: (pn1 - 1) < r by A8, A7, XREAL_1: 19;

      set SP = ( Sphere (( 0. TR1),1)), CL = ( cl_Ball (p,r));

      

       A15: for q be Point of TR1 holds (p - q) = (( - q) +* (n1,(pn1 - (q . n1))))

      proof

        let q be Point of TR1;

        set q1 = (( - q) +* (n1,(pn1 - (q . n1))));

        

         A16: ( len (p - q)) = n1 by CARD_1:def 7;

        

         A17: ( len ( - q)) = n1 by CARD_1:def 7;

        for i st 1 <= i & i <= n1 holds ((p - q) . i) = (q1 . i)

        proof

          let i such that

           A19: 1 <= i and

           A20: i <= n1;

          

           A21: i in ( dom ( - q)) by A19, A20, A17, FINSEQ_3: 25;

          i in ( dom (p - q)) by A19, A20, A16, FINSEQ_3: 25;

          then

           A22: ((p - q) . i) = ((p . i) - (q . i)) by VALUED_1: 13;

          per cases by A20, NAT_1: 8;

            suppose

             A23: i <= n;

            then i < n1 by NAT_1: 13;

            

            then

             A24: (q1 . i) = (( - q) . i) by FUNCT_7: 32

            .= ( - (q . i)) by VALUED_1: 8;

            (p . i) = ((p | ( Seg n)) . i) by A23, A19, FINSEQ_1: 1, FUNCT_1: 49;

            then (p . i) = 0 by A9;

            hence thesis by A24, A22;

          end;

            suppose i = n1;

            hence thesis by A21, FUNCT_7: 31, A22;

          end;

        end;

        hence thesis by A16, CARD_1:def 7;

      end;

      set dd = ((((pn1 * pn1) + 1) - (r * r)) / (2 * pn1)), cc = (1 - (dd * dd));

      set c = ( sqrt cc);

      set TD = ( Tdisk (( 0. TR),1)), Tc = ( Tdisk (( 0. TR),c));

      

       A25: ( [#] TD) = ( cl_Ball (( 0. TR),1)) by PRE_TOPC:def 5;

      1 < (1 + r) by A6, A7, XXREAL_0: 2;

      then

       A26: r > 0 by XREAL_1: 32;

      then (r * r) <= (1 * 1) by A5, XREAL_1: 66;

      then (r * r) < (1 + (pn1 * pn1)) by A10, XXREAL_0: 2;

      then

       A27: 0 < ((1 + (pn1 * pn1)) - (r * r)) by XREAL_1: 50;

      

       A28: 1 <= n1 by NAT_1: 11;

      

       A29: for q be Point of TR1 holds ( |.(q - p).| ^2 ) = ((( |.q.| ^2 ) - ((2 * (q . n1)) * pn1)) + (pn1 * pn1))

      proof

        let q be Point of TR1;

        set pqn = (pn1 - (q . n1));

        

         A30: (( - q) . n1) = ( - (q . n1)) by VALUED_1: 8;

        ( len ( - q)) = n1 by CARD_1:def 7;

        then

         A31: n1 in ( dom ( - q)) by A28, FINSEQ_3: 25;

         |.(q - p).| = |.( - (q - p)).| by EUCLID: 10

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

        

        hence ( |.(q - p).| ^2 ) = ( Sum ( sqr (p - q))) by TOPREAL9: 5

        .= ( Sum ( sqr (( - q) +* (n1,pqn)))) by A15

        .= ((( Sum ( sqr ( - q))) - ((( - q) . n1) ^2 )) + (pqn ^2 )) by A31, MATRTOP3: 3

        .= ((( |.( - q).| ^2 ) - ((( - q) . n1) ^2 )) + (pqn ^2 )) by TOPREAL9: 5

        .= ((( |.q.| ^2 ) - (( - (q . n1)) * ( - (q . n1)))) + (pqn ^2 )) by A30, EUCLID: 10

        .= ((( |.q.| ^2 ) - ((2 * (q . n1)) * pn1)) + (pn1 * pn1));

      end;

      

       A32: (SP /\ CL) c= Sp

      proof

        let x be object;

        assume

         A33: x in (SP /\ CL);

        then

        reconsider x as Point of TR1;

        x in CL by A33, XBOOLE_0:def 4;

        then

         A34: |.(x - p).| <= r by TOPREAL9: 8;

        set xn1 = (x . n1);

        ( rng x) c= REAL ;

        then

         A35: x is FinSequence of REAL by FINSEQ_1:def 4;

        ( len x) = n1 by CARD_1:def 7;

        then

        reconsider X = x as Element of ( REAL n1) by A35, FINSEQ_2: 92;

        x in SP by A33, XBOOLE_0:def 4;

        then

         A36: |.x.| = 1 by TOPREAL9: 12;

        ( |.(x - p).| ^2 ) = ((( |.x.| ^2 ) - ((2 * xn1) * pn1)) + (pn1 * pn1)) by A29;

        then (( - ((2 * xn1) * pn1)) + (1 + (pn1 * pn1))) <= (r * r) by A34, XREAL_1: 66, A36;

        then ( - ((2 * xn1) * pn1)) <= ((r * r) - (1 + (pn1 * pn1))) by XREAL_1: 19;

        then ( - ((2 * xn1) * pn1)) <= ( - ((1 + (pn1 * pn1)) - (r * r)));

        then xn1 >= 0 by XREAL_1: 24, A8, A27;

        hence thesis by A36;

      end;

      

       A37: (FF .: (SP /\ CL)) c= ( cl_Ball (( 0. TR),c))

      proof

        let y be object;

        assume y in (FF .: (SP /\ CL));

        then

        consider x be object such that

         A38: x in ( dom FF) and

         A39: x in (SP /\ CL) and

         A40: (FF . x) = y by FUNCT_1:def 6;

        reconsider x as Point of TR1 by A38;

        ( rng x) c= REAL ;

        then

         A41: x is FinSequence of REAL by FINSEQ_1:def 4;

        ( len x) = n1 by CARD_1:def 7;

        then

        reconsider X = x as Element of ( REAL n1) by A41, FINSEQ_2: 92;

        x in SP by A39, XBOOLE_0:def 4;

        then

         A42: |.x.| = 1 by TOPREAL9: 12;

        (FF . x) in ( rng FF) by A38, FUNCT_1:def 3;

        then

        reconsider Y = y as Point of TR by A40;

        set xn1 = (x . n1);

        

         A43: (Y - ( 0. TR)) = Y by RLVECT_1: 13;

        x in CL by A39, XBOOLE_0:def 4;

        then

         A44: |.(x - p).| <= r by TOPREAL9: 8;

        ( |.(x - p).| ^2 ) = ((( |.x.| ^2 ) - ((2 * xn1) * pn1)) + (pn1 * pn1)) by A29;

        then (( - ((2 * xn1) * pn1)) + (1 + (pn1 * pn1))) <= (r * r) by A44, XREAL_1: 66, A42;

        then ( - ((2 * xn1) * pn1)) <= ((r * r) - (1 + (pn1 * pn1))) by XREAL_1: 19;

        then ( - ((2 * xn1) * pn1)) <= ( - ((1 + (pn1 * pn1)) - (r * r)));

        then ((2 * pn1) * xn1) >= ((1 + (pn1 * pn1)) - (r * r)) by XREAL_1: 24;

        then xn1 >= (((1 + (pn1 * pn1)) - (r * r)) / (2 * pn1)) by A8, XREAL_1: 79;

        then

         A45: (xn1 * xn1) >= (dd * dd) by A8, A27, XREAL_1: 66;

        ( |.x.| ^2 ) = 1 by A42;

        

        then (1 - ((X . n1) ^2 )) = ((( |.(X | n).| ^2 ) + ((X . n1) ^2 )) - ((X . n1) ^2 )) by REAL_NS1: 10

        .= ( |.(X | n).| ^2 );

        then ( |.(X | n).| ^2 ) <= cc by A45, XREAL_1: 10;

        then

         A46: ( sqrt ( |.(X | n).| ^2 )) <= ( sqrt cc) by SQUARE_1: 26;

        (FF . x) = (x | n) by A2, Th1;

        then |.Y.| <= c by SQUARE_1:def 2, A46, A40;

        hence thesis by A43;

      end;

      ( [#] (TR1 | Sp)) = Sp by PRE_TOPC:def 5;

      then

      reconsider SC = (SP /\ CL) as Subset of (TR1 | Sp) by A32;

      

       A47: ((TR1 | Sp) | SC) = (TR1 | (SP /\ CL)) by A32, PRE_TOPC: 7;

      

       A48: Sn = { t where t be Point of TR1 : (t . n1) <= 0 & |.t.| = 1 };

      then

       A49: ( <:F:> .: Sp) = ( cl_Ball (( 0. TR),1)) by A2, Th1;

      then

      reconsider FS = (FF | Sp) as Function of (TR1 | Sp), TD by JORDAN24: 12;

      Sp = { l where l be Point of TR1 : (l . n1) >= 0 & |.l.| = 1 };

      then

      reconsider s1 = Sp, s2 = Sn as closed Subset of TR1 by Th2, A48;

      

       A50: ( Ball (( 0. TR),1)) c= ( cl_Ball (( 0. TR),1)) by TOPREAL9: 16;

      

       A51: (pn1 - 1) >= 0 by A12, A8, A6, XREAL_1: 48;

      then

       A52: ((pn1 - 1) * r) < (r * r) by A13, XREAL_1: 68;

      ((pn1 - 1) * (pn1 - 1)) <= ((pn1 - 1) * r) by A13, A51, XREAL_1: 66;

      then (((pn1 * pn1) + 1) - (2 * pn1)) < (r * r) by A52, XXREAL_0: 2;

      then (((pn1 * pn1) + 1) - (r * r)) < (2 * pn1) by XREAL_1: 11;

      then

       A53: dd < 1 by A27, XREAL_1: 189;

      then (dd * dd) < (dd * 1) by A8, A27, XREAL_1: 68;

      then (dd * dd) < 1 by A53, XXREAL_0: 2;

      then

       A54: cc > 0 by XREAL_1: 50;

      then

       A55: cc = (c ^2 ) by SQUARE_1:def 2;

      (1 - (dd * dd)) < (1 - 0 ) by A8, A27, XREAL_1: 10;

      then

       A56: c < ( sqrt 1) by SQUARE_1: 27, A54;

      then ( cl_Ball (( 0. TR),c)) c= ( Ball (( 0. TR),1)) by SQUARE_1: 18, JORDAN: 21;

      then

       A57: ( cl_Ball (( 0. TR),c)) c= ( cl_Ball (( 0. TR),1)) by A50;

      ( cl_Ball (( 0. TR),c)) c= (FF .: (SP /\ CL))

      proof

        let y be object;

        

         A58: (dd ^2 ) = (dd * dd);

        assume

         A59: y in ( cl_Ball (( 0. TR),c));

        then

        consider x be object such that

         A60: x in ( dom FF) and

         A61: x in Sp and

         A62: (FF . x) = y by A57, A49, FUNCT_1:def 6;

        y in ( rng FF) by A60, A62, FUNCT_1:def 3;

        then

        reconsider Y = y as Point of TR;

        

         A63: |.Y.| <= c by A59, TOPREAL9: 11;

        consider q be Point of TR1 such that

         A64: q = x and

         A65: (q . n1) >= 0 and

         A66: |.q.| = 1 by A61;

        set qn1 = (q . n1);

        ( rng q) c= REAL ;

        then

         A67: q is FinSequence of REAL by FINSEQ_1:def 4;

        ( len q) = n1 by CARD_1:def 7;

        then

        reconsider Q = q as Element of ( REAL n1) by A67, FINSEQ_2: 92;

        

         A68: ( |.Q.| ^2 ) = 1 by A66;

        

        then 1 = (( |.(Q | n).| ^2 ) + (qn1 ^2 )) by REAL_NS1: 10

        .= (( |.Y.| ^2 ) + (qn1 * qn1)) by A2, Th1, A62, A64;

        then (1 - (qn1 * qn1)) <= (c * c) by A63, XREAL_1: 66;

        then

         A69: (qn1 * qn1) >= (dd * dd) by A55, XREAL_1: 10;

        (qn1 ^2 ) = (qn1 * qn1);

        then ((((pn1 * pn1) + 1) - (r * r)) / (2 * pn1)) <= qn1 by A69, A65, A58, SQUARE_1: 47;

        then (((((pn1 * pn1) + 1) - (r * r)) / (2 * pn1)) * (2 * pn1)) <= (qn1 * (2 * pn1)) by A8, XREAL_1: 64;

        then (((pn1 * pn1) + 1) - (r * r)) <= (qn1 * (2 * pn1)) by A8, XCMPLX_1: 87;

        then

         A70: (((pn1 * pn1) + 1) - (qn1 * (2 * pn1))) <= (r * r) by XREAL_1: 12;

        ( |.(q - p).| ^2 ) = ((1 - ((2 * qn1) * pn1)) + (pn1 * pn1)) by A68, A29;

        then ( |.(q - p).| ^2 ) <= (r ^2 ) by A70;

        then |.(q - p).| <= r by SQUARE_1: 47, A26;

        then

         A71: q in CL;

        (q - ( 0. TR1)) = q by RLVECT_1: 13;

        then q in SP by A66;

        then q in (SP /\ CL) by A71, XBOOLE_0:def 4;

        hence thesis by A60, A64, FUNCT_1:def 6, A62;

      end;

      then (FS .: SC) = ( cl_Ball (( 0. TR),c)) by A37, A32, RELAT_1: 129;

      then

       A72: (TD | (FS .: SC)) = Tc by A25, PRE_TOPC: 7;

      (SP /\ CL) is non empty

      proof

        

         A73: (pn1 - 1) <= ((1 + r) - 1) by A12, A8, A7, XREAL_1: 9;

        (pn1 - 1) >= 0 by A12, A8, A6, XREAL_1: 48;

        then

         A74: ((pn1 - 1) * (pn1 - 1)) <= (r * r) by A73, XREAL_1: 66;

        set q = (( 0* n1) +* (n1,1));

        ( rng q) c= REAL ;

        then

         W: q is FinSequence of REAL by FINSEQ_1:def 4;

        ( len q) = n1 by CARD_1:def 7;

        then

        reconsider q as Point of TR1 by W, EUCLID: 76;

        

         A75: n1 in ( Seg n1) by FINSEQ_1: 4;

        

         A76: |.q.| = |.1.| by FINSEQ_1: 4, TOPREALC: 13

        .= 1 by ABSVALUE:def 1;

        

         A77: n1 in ( dom ( 0* n1)) by A75;

        ( |.q.| ^2 ) = (1 * 1) by A76;

        

        then ( |.(q - p).| ^2 ) = (((1 * 1) - ((2 * (q . n1)) * pn1)) + (pn1 * pn1)) by A29

        .= (((1 * 1) - ((2 * 1) * pn1)) + (pn1 * pn1)) by A77, FUNCT_7: 31

        .= ((1 - pn1) * (1 - pn1));

        then ( |.(q - p).| ^2 ) <= (r ^2 ) by A74;

        then |.(q - p).| <= r by A26, SQUARE_1: 47;

        then

         A78: q in CL;

        (q - ( 0. TR1)) = q by RLVECT_1: 13;

        then q in SP by A76;

        hence thesis by A78, XBOOLE_0:def 4;

      end;

      then

      reconsider H = (FS | SC) as Function of (TR1 | (SP /\ CL)), Tc by A47, A72, JORDAN24: 12;

      take c, H;

      for H be Function of (TR1 | Sp), ( Tdisk (( 0. ( TOP-REAL n)),1)) st H = ( <:F:> | Sp) holds H is being_homeomorphism by A2, A48, Th1;

      hence c > 0 & H is being_homeomorphism by A47, A72, A54, METRIZTS: 2;

      

       A79: ( Sphere (p,r)) c= CL by TOPREAL9: 17;

      then (SP /\ ( Sphere (p,r))) c= SC by XBOOLE_1: 27;

      then

       A80: (FS .: (SP /\ ( Sphere (p,r)))) = (FF .: (SP /\ ( Sphere (p,r)))) by A32, XBOOLE_1: 1, RELAT_1: 129;

      ( Sphere (( 0. TR),c)) c= ( Ball (( 0. TR),1)) by A56, SQUARE_1: 18, JORDAN: 22;

      then

       A81: ( Sphere (( 0. TR),c)) c= ( cl_Ball (( 0. TR),1)) by A50;

      

       A82: ( Sphere (( 0. ( TOP-REAL n)),c)) c= (FF .: (SP /\ ( Sphere (p,r))))

      proof

        let y be object;

        

         A83: (dd ^2 ) = (dd * dd);

        assume

         A84: y in ( Sphere (( 0. ( TOP-REAL n)),c));

        then

        consider x be object such that

         A85: x in ( dom FF) and

         A86: x in Sp and

         A87: (FF . x) = y by A81, A49, FUNCT_1:def 6;

        y in ( rng FF) by A85, A87, FUNCT_1:def 3;

        then

        reconsider Y = y as Point of TR;

        

         A88: |.Y.| = c by A84, TOPREAL9: 12;

        consider q be Point of TR1 such that

         A89: q = x and

         A90: (q . n1) >= 0 and

         A91: |.q.| = 1 by A86;

        ( rng q) c= REAL ;

        then

         A92: q is FinSequence of REAL by FINSEQ_1:def 4;

        ( len q) = n1 by CARD_1:def 7;

        then

        reconsider Q = q as Element of ( REAL n1) by A92, FINSEQ_2: 92;

        set qn1 = (q . n1);

        

         A93: (qn1 ^2 ) = (qn1 * qn1);

        

         A94: ( |.Q.| ^2 ) = 1 by A91;

        

        then 1 = (( |.(Q | n).| ^2 ) + (qn1 ^2 )) by REAL_NS1: 10

        .= (( |.Y.| ^2 ) + (qn1 * qn1)) by A2, Th1, A87, A89;

        then dd = qn1 or dd = ( - qn1) by A88, A55, A93, A83, SQUARE_1: 40;

        then (((pn1 * pn1) + 1) - (r * r)) = (qn1 * (2 * pn1)) by A90, A8, A27, XCMPLX_1: 87;

        then

         A95: (((pn1 * pn1) + 1) - (qn1 * (2 * pn1))) = (r * r);

        ( |.(q - p).| ^2 ) = ((1 - ((2 * qn1) * pn1)) + (pn1 * pn1)) by A94, A29;

        then ( |.(q - p).| ^2 ) = (r ^2 ) by A95;

        then |.(q - p).| = r or |.(q - p).| = ( - r) by SQUARE_1: 40;

        then

         A96: q in ( Sphere (p,r)) by A26;

        (q - ( 0. TR1)) = q by RLVECT_1: 13;

        then q in SP by A91;

        then q in (SP /\ ( Sphere (p,r))) by A96, XBOOLE_0:def 4;

        hence thesis by A85, A89, FUNCT_1:def 6, A87;

      end;

      (FF .: (SP /\ ( Sphere (p,r)))) c= ( Sphere (( 0. ( TOP-REAL n)),c))

      proof

        let y be object;

        assume y in (FF .: (SP /\ ( Sphere (p,r))));

        then

        consider x be object such that

         A98: x in ( dom FF) and

         A99: x in (SP /\ ( Sphere (p,r))) and

         A100: (FF . x) = y by FUNCT_1:def 6;

        reconsider x as Point of TR1 by A98;

        (FF . x) in ( rng FF) by A98, FUNCT_1:def 3;

        then

        reconsider Y = y as Point of TR by A100;

        set xn1 = (x . n1);

        ( rng x) c= REAL ;

        then

         A101: x is FinSequence of REAL by FINSEQ_1:def 4;

        ( len x) = n1 by CARD_1:def 7;

        then

        reconsider X = x as Element of ( REAL n1) by A101, FINSEQ_2: 92;

        x in SP by A99, XBOOLE_0:def 4;

        then

         A102: |.x.| = 1 by TOPREAL9: 12;

        then ( |.x.| ^2 ) = 1;

        

        then

         A103: (1 - ((X . n1) ^2 )) = ((( |.(X | n).| ^2 ) + ((X . n1) ^2 )) - ((X . n1) ^2 )) by REAL_NS1: 10

        .= ( |.(X | n).| ^2 );

        x in ( Sphere (p,r)) by A99, XBOOLE_0:def 4;

        then

         A104: |.(x - p).| = r by TOPREAL9: 9;

        ( |.(x - p).| ^2 ) = ((( |.x.| ^2 ) - ((2 * xn1) * pn1)) + (pn1 * pn1)) by A29;

        then ((2 * pn1) * xn1) = ((1 + (pn1 * pn1)) - (r * r)) by A102, A104;

        then xn1 = (((1 + (pn1 * pn1)) - (r * r)) / (2 * pn1)) by A8, XCMPLX_1: 89;

        then |.(X | n).| = c or |.(X | n).| = ( - c) by A103, SQUARE_1:def 2;

        then

         A105: |.Y.| = c by A54, A100, A2, Th1;

        (Y - ( 0. TR)) = Y by RLVECT_1: 13;

        hence thesis by A105;

      end;

      hence thesis by A80, A82, A79, XBOOLE_1: 27, RELAT_1: 129;

    end;

    theorem :: BROUWER3:19

    for p,q be Point of ( TOP-REAL (n + 1)) holds for r, s st s <= r & r <= |.(p - q).| & s < |.(p - q).| & |.(p - q).| < (s + r) holds ex h be Function of (( TOP-REAL (n + 1)) | (( Sphere (p,r)) /\ ( cl_Ball (q,s)))), ( Tdisk (( 0. ( TOP-REAL n)),1)) st h is being_homeomorphism & (h .: (( Sphere (p,r)) /\ ( Sphere (q,s)))) = ( Sphere (( 0. ( TOP-REAL n)),1))

    proof

      

       N: n in NAT by ORDINAL1:def 12;

      set n1 = (n + 1), TR = ( TOP-REAL n), TR1 = ( TOP-REAL n1);

      let p,q be Point of TR1;

      let r,s be Real such that

       A1: s <= r and

       A2: r <= |.(p - q).| and

       A3: s < |.(p - q).| and

       A4: |.(p - q).| < (s + r);

      reconsider r1 = (1 / r) as Real;

      

       A5: r > 0 by A1, A4;

      then

       A6: (r * r1) = 1 by XCMPLX_1: 87;

      set A = (( Sphere (p,r)) /\ ( cl_Ball (q,s)));

      set TR = ( TOP-REAL n);

      set y = ((1 / r) * (q - p));

      set T = ( transl (( - p),TR1)), M = ( mlt (r1,TR1));

      

       A7: ( 0* n1) = ( 0. TR1) by EUCLID: 70;

      

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

      

       A9: |.y.| = ( |.r1.| * |.(q - p).|) by EUCLID: 11

      .= (r1 * |.(q - p).|) by A5, ABSVALUE:def 1;

      set Y = (( 0* n1) +* (n1, |.y.|));

      ( rng Y) c= REAL ;

      then

       W: Y is FinSequence of REAL by FINSEQ_1:def 4;

      

       A10: ( len Y) = n1 by CARD_1:def 7;

      then Y is Element of ( REAL n1) by W, FINSEQ_2: 92;

      then

      reconsider Y as Point of TR1 by EUCLID: 22;

      set S = ( Sphere (( 0. TR1),1)), CL = ( cl_Ball (Y,(s * r1)));

      

       A11: ( [#] (TR1 | (S /\ CL))) = (S /\ CL) by PRE_TOPC:def 5;

      

       A12: |.Y.| = |. |.y.|.| by TOPREALC: 13, FINSEQ_1: 3;

      then

       A13: |.Y.| = |.y.| by ABSVALUE:def 1;

      ex ROT be homogeneous additive rotation Function of TR1, TR1 st ROT is being_homeomorphism & (ROT . y) = Y

      proof

        per cases ;

          suppose n = 0 ;

          then ex ROT be homogeneous additive Function of TR1, TR1 st (ROT is rotation) & (ROT . y) = Y & (( AutMt ROT) = ( AxialSymmetry (n1,n1)) or ( AutMt ROT) = ( 1. ( F_Real ,n1))) by A13, MATRTOP3: 40;

          hence thesis;

        end;

          suppose n > 0 ;

          then n1 <> 1;

          then ex ROT be homogeneous additive Function of TR1, TR1 st (ROT is base_rotation) & (ROT . y) = Y by A13, MATRTOP3: 41;

          hence thesis;

        end;

      end;

      then

      consider ROT be homogeneous additive rotation Function of TR1, TR1 such that ROT is being_homeomorphism and

       A14: (ROT . y) = Y;

      set h = ((ROT * M) * T);

      

       A15: |.(ROT . ( 0. TR1)).| = |.( 0. TR1).| by MATRTOP3:def 4

      .= |.( 0* n1).| by EUCLID: 70

      .= 0 by EUCLID: 7;

      

       A16: (h .: ( Sphere (q,s))) = ((ROT * M) .: (T .: ( Sphere (q,s)))) by RELAT_1: 126

      .= ((ROT * M) .: ( Sphere ((( - p) + q),s))) by Th15

      .= (ROT .: (M .: ( Sphere ((( - p) + q),s)))) by RELAT_1: 126

      .= (ROT .: ( Sphere ((r1 * (q - p)),(s * r1)))) by Th16, A5

      .= ( Sphere (Y,(s * r1))) by A14, Th17;

      (ROT . ( 0. TR1)) is Element of ( REAL n1) by EUCLID: 22;

      then

       A17: (ROT . ( 0. TR1)) = ( 0. TR1) by A15, A7, EUCLID: 8;

      

       A18: (h .: ( Sphere (p,r))) = ((ROT * M) .: (T .: ( Sphere (p,r)))) by RELAT_1: 126

      .= ((ROT * M) .: ( Sphere ((( - p) + p),r))) by Th15

      .= (ROT .: (M .: ( Sphere (( 0. TR1),r)))) by A8, RELAT_1: 126

      .= (ROT .: ( Sphere ((r1 * ( 0. TR1)),(r * r1)))) by Th16, A5

      .= (ROT .: ( Sphere ((r1 * ( 0. TR1)),1))) by A5, XCMPLX_1: 87

      .= (ROT .: ( Sphere (( 0. TR1),1))) by RLVECT_1: 10

      .= ( Sphere (( 0. TR1),1)) by Th17, A17;

      reconsider hA = (h | A) as Function of (TR1 | A), (TR1 | (h .: A)) by JORDAN24: 12;

      (ROT * M) is being_homeomorphism by A5, TOPS_2: 57;

      then

       A19: h is being_homeomorphism by TOPS_2: 57;

      then

       A20: hA is being_homeomorphism by METRIZTS: 2;

      reconsider TD = ( Tdisk (( 0. TR),1)) as non empty TopSpace;

      

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

      (h .: ( cl_Ball (q,s))) = ((ROT * M) .: (T .: ( cl_Ball (q,s)))) by RELAT_1: 126

      .= ((ROT * M) .: ( cl_Ball ((( - p) + q),s))) by Th15

      .= (ROT .: (M .: ( cl_Ball ((( - p) + q),s)))) by RELAT_1: 126

      .= (ROT .: ( cl_Ball (y,(s * r1)))) by Th16, A5

      .= ( cl_Ball (Y,(s * r1))) by A14, Th17;

      then

       A22: (h .: A) = (S /\ CL) by A18, A5, FUNCT_1: 62;

      ( |.(p - q).| - s) < ((s + r) - s) by A4, XREAL_1: 9;

      then

       A23: (r1 * ( |.(p - q).| - s)) < 1 by A6, A5, XREAL_1: 68;

      

       A24: ( dom ( 0* n1)) = ( Seg n1);

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

      then

       A25: |.(p - q).| = |.(q - p).| by EUCLID: 10;

      ( |.(p - q).| + s) >= (r + s) by A2, XREAL_1: 6;

      then ( |.(p - q).| + s) > |.(p - q).| by A4, XXREAL_0: 2;

      then ( |.(p - q).| + s) > r by A2, XXREAL_0: 2;

      then

       A26: (r1 * ( |.(p - q).| + s)) > 1 by A6, A5, XREAL_1: 68;

      

       A27: s > 0

      proof

        assume s <= 0 ;

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

        hence thesis by A4, XXREAL_0: 2, A2;

      end;

      per cases ;

        suppose

         A28: n = 0 ;

        set E = ( Euclid n1);

        reconsider YY = Y as Point of E by EUCLID: 67;

        (Y . 1) = |.y.| by A24, FINSEQ_1: 3, A28, FUNCT_7: 31;

        then

         A29: YY = <* |.y.|*> by CARD_1:def 7, A28, FINSEQ_1: 40;

        then

         A30: ( cl_Ball (YY,(s * r1))) = { <*w*> where w be Real : ( |.y.| qua ExtReal - (s qua ExtReal * r1)) <= w & w <= ( |.y.| qua ExtReal + (s qua ExtReal * r1)) } by A28, TOPDIM_2: 17;

        

         A31: ( [#] TR) = {( 0. TR)} by A28, EUCLID: 22, EUCLID: 77;

        then

        reconsider ZZ = ( 0. TR) as Point of TD by A21, ZFMISC_1: 33;

        

         A32: ( [#] ( Tdisk (( 0. TR),1))) = {( 0. TR)} by A21, A31, ZFMISC_1: 33;

        reconsider z = 0 , yy = |.y.| as Real;

        ( 0. TR1) = <*z*> by A7, A28, FINSEQ_2: 59;

        then

         A33: ( Fr ( Ball (( 0. TR1),1))) = { <*(z qua ExtReal - 1)*>, <*(z qua ExtReal + 1)*>} by A28, TOPDIM_2: 18;

        

         A34: ( Fr ( Ball (( 0. TR1),1))) = S by JORDAN: 24;

        then

         A35: <*(z + 1)*> in S by A33, TARSKI:def 2;

        

         A36: ( cl_Ball (YY,(s * r1))) = ( cl_Ball (Y,(s * r1))) by TOPREAL9: 14;

        then

         A37: <*(z qua ExtReal + 1)*> in CL by A23, A9, A25, A26, A30;

        then

         A38: A is non empty by A22, A35, XBOOLE_0:def 4;

        reconsider SCL = (S /\ CL) as non empty Subset of TR1 by A35, A37, XBOOLE_0:def 4;

        reconsider zz = <*1*> as Point of (TR1 | SCL) by A35, A37, XBOOLE_0:def 4, A11;

        set h1 = ((TR1 | SCL) --> ZZ), h2 = (TD --> zz);

        (S /\ CL) c= { <*(z + 1)*>}

        proof

          let v be object;

          assume

           A39: v in (( Sphere (( 0. TR1),1)) /\ ( cl_Ball (Y,(s * r1))));

          then v in ( Sphere (( 0. TR1),1)) by XBOOLE_0:def 4;

          then

           A40: v = <*(z + 1)*> or v = <*(z - 1)*> by A34, A33, TARSKI:def 2;

          assume

           A41: not v in { <*(z + 1)*>};

          v in ( cl_Ball (Y,(s * r1))) by A39, XBOOLE_0:def 4;

          then ex w be Real st <*(z - 1)*> = <*w*> & ( |.y.| - (s * r1)) <= w & w <= ( |.y.| + (s * r1)) by A41, A40, TARSKI:def 1, A30, A36;

          then (r1 * ( |.(p - q).| - s)) <= ( - (r1 * r)) by FINSEQ_1: 76, A9, A25, A6;

          then (r1 * ( |.(p - q).| - s)) <= (r1 * ( - r));

          then

           A42: r <= ( - ( |.(p - q).| - s)) by A5, XREAL_1: 68, XREAL_1: 25;

          (s - |.(p - q).|) < ( |.(p - q).| - |.(p - q).|) by A3, XREAL_1: 14;

          hence thesis by A42, A5;

        end;

        then

         A43: h1 = (zz .--> ( 0. TR)) by A11, ZFMISC_1: 33;

        then ( rng h1) = {( 0. TR)} by FUNCOP_1: 88;

        then h1 is onto by A32, FUNCT_2:def 3;

        then

         A44: (h1 " ) = ((zz .--> ( 0. TR)) " ) by A43, TOPS_2:def 4;

        reconsider HA = hA as Function of (TR1 | A), (TR1 | SCL) by A22;

        reconsider HH = (h1 * HA) as Function of (TR1 | (( Sphere (p,r)) /\ ( cl_Ball (q,s)))), ( Tdisk (( 0. TR),1));

        take HH;

        

         A45: ( dom h1) = ( [#] (TR1 | (S /\ CL)));

        

         A46: HA is being_homeomorphism by A19, METRIZTS: 2, A22;

        h2 = (( 0. TR) .--> zz) by A21, A31, ZFMISC_1: 33;

        then

         A47: (h1 " ) is continuous by NECKLACE: 9, A44;

        ( rng h1) = ( [#] ( Tdisk (( 0. TR),1))) by ZFMISC_1: 33, A32;

        then h1 is being_homeomorphism by A45, A43, A47, TOPS_2:def 5;

        hence HH is being_homeomorphism by A38, TOPS_2: 57, A46;

        

         A48: ( Fr ( Ball (Y,(s * r1)))) = ( Sphere (Y,(s * r1))) by A1, A27, JORDAN: 24;

        

         A49: ( Fr ( Ball (Y,(s qua ExtReal * r1)))) = { <*( |.y.| qua ExtReal - (s * r1))*>, <*( |.y.| qua ExtReal + (s * r1))*>} by A1, A27, A29, A28, TOPDIM_2: 18;

        (S /\ ( Sphere (Y,(s * r1)))) = {}

        proof

          assume (S /\ ( Sphere (Y,(s * r1)))) <> {} ;

          then

          consider z be object such that

           A50: z in (S /\ ( Sphere (Y,(s * r1)))) by XBOOLE_0:def 1;

          

           A51: z in ( Sphere (Y,(s * r1))) by A50, XBOOLE_0:def 4;

          

           A52: z in S by A50, XBOOLE_0:def 4;

          per cases by A52, A34, A33, TARSKI:def 2, A51, A48, A49;

            suppose z = <*1*> & z = <*( |.y.| - (s * r1))*>;

            hence thesis by FINSEQ_1: 76, A23, A9, A25;

          end;

            suppose z = <*1*> & z = <*( |.y.| + (s * r1))*>;

            hence thesis by FINSEQ_1: 76, A26, A9, A25;

          end;

            suppose z = <*( - 1)*> & z = <*( |.y.| - (s * r1))*>;

            then ( - 1) = (r1 * ( |.(p - q).| - s)) by FINSEQ_1: 76, A9, A25;

            then ( |.(p - q).| - s) < 0 by A5;

            then (( |.(p - q).| - s) + s) < ( 0 + s) by XREAL_1: 6;

            hence thesis by A3;

          end;

            suppose z = <*( - 1)*> & z = <*( |.y.| + (s * r1))*>;

            hence thesis by FINSEQ_1: 76, A26, A9, A25;

          end;

        end;

        then (h .: (( Sphere (p,r)) /\ ( Sphere (q,s)))) = {} by A18, A16, FUNCT_1: 62, A5;

        then (HA .: (( Sphere (p,r)) /\ ( Sphere (q,s)))) = {} by XBOOLE_1: 3, RELAT_1: 128;

        

        then

         A53: (HH .: (( Sphere (p,r)) /\ ( Sphere (q,s)))) = (h1 .: {} ) by RELAT_1: 126

        .= {} ;

        ( Sphere (( 0. TR),1)) = {}

        proof

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

          then

          consider w be object such that

           A54: w in ( Sphere (( 0. TR),1)) by XBOOLE_0:def 1;

          w = ( 0. TR) by A54, A28, EUCLID: 77;

          then

           A55: |.( 0. TR).| = 1 by A54, TOPREAL9: 12;

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

          hence contradiction by A55, EUCLID: 7;

        end;

        hence thesis by A53;

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

      end;

        suppose

         A56: n > 0 ;

        

         A57: ( len ( 0* n)) = n by CARD_1:def 7;

        (r1 * |.(p - q).|) < (r1 * (s + r)) by A27, A1, A4, XREAL_1: 68;

        then |.Y.| < ((r1 * r) + (r1 * s)) by A9, A25, A12, ABSVALUE:def 1;

        then

         A58: |.Y.| < (1 + (r1 * s)) by A1, A27, XCMPLX_1: 106;

        

         A59: n < n1 by NAT_1: 13;

        then

         A60: ( len (Y | n)) = n by A10, FINSEQ_1: 59;

         A61:

        now

          let k be Nat;

          assume that

           A64: 1 <= k and

           A65: k <= n;

          

           A66: (Y . k) = (( 0* n1) . k) by A65, A59, FUNCT_7: 32;

          ((Y | n) . k) = (Y . k) by A64, A65, FINSEQ_1: 1, FUNCT_1: 49;

          hence ((Y | n) . k) = (( 0* n) . k) by A66;

        end;

        

         A68: (r1 * r) = 1 by A1, A27, XCMPLX_1: 106;

        then

         A69: (r1 * s) <= 1 by A1, XREAL_1: 64, A27;

         |.y.| >= 1 by XREAL_1: 64, A27, A1, A2, A9, A25, A68;

        then

         A70: |.Y.| >= 1 by A12, ABSVALUE:def 1;

        (Y . n1) > 0 by A2, A5, A9, A25, FINSEQ_1: 3, FUNCT_7: 31, A24;

        then

        consider c be Real, H be Function of (TR1 | (S /\ CL)), ( Tdisk (( 0. TR),c)) such that

         A71: c > 0 and

         A72: H is being_homeomorphism and

         A73: (H .: (S /\ ( Sphere (Y,(r1 * s))))) = ( Sphere (( 0. TR),c)) by A56, Lm4, A69, A70, A58, A61, FINSEQ_1: 14, A57, A60;

        ( rng H) = ( [#] ( Tdisk (( 0. TR),c))) by A72, TOPS_2:def 5;

        then

         A74: A is non empty by A71, A22;

        then

        reconsider HH = (H * hA) as Function of (TR1 | A), ( Tdisk (( 0. TR),c)) by A22;

        

         A75: HH is being_homeomorphism by A71, A72, A74, A20, A22, TOPS_2: 57;

        reconsider c1 = (1 / c) as Real;

        set MM = ( mlt (c1,TR));

        

         A76: (c1 * ( 0. TR)) = ( 0. TR) by RLVECT_1: 10;

        

         A77: (c1 * c) = 1 by A71, XCMPLX_1: 106;

        then

         A78: (MM .: ( cl_Ball (( 0. TR),c))) = ( cl_Ball (( 0. TR),1)) by A71, A76, Th16;

        then

        reconsider MM1 = (MM | ( cl_Ball (( 0. TR),c))) as Function of ( Tdisk (( 0. TR),c)), ( Tdisk (( 0. TR),1)) by JORDAN24: 12;

        reconsider MH = (MM1 * HH) as Function of (TR1 | A), ( Tdisk (( 0. TR),1)) by A71;

        take MH;

        MM1 is being_homeomorphism by METRIZTS: 2, A71, A78;

        hence MH is being_homeomorphism by A75, A71, A74, TOPS_2: 57;

        ( Sphere (q,s)) c= ( cl_Ball (q,s)) by TOPREAL9: 17;

        then (hA .: (( Sphere (p,r)) /\ ( Sphere (q,s)))) = (h .: (( Sphere (p,r)) /\ ( Sphere (q,s)))) by XBOOLE_1: 27, RELAT_1: 129;

        

        then (HH .: (( Sphere (p,r)) /\ ( Sphere (q,s)))) = (H .: (h .: (( Sphere (p,r)) /\ ( Sphere (q,s))))) by RELAT_1: 126

        .= ( Sphere (( 0. TR),c)) by A73, A18, A16, FUNCT_1: 62, A5;

        

        hence (MH .: (( Sphere (p,r)) /\ ( Sphere (q,s)))) = (MM1 .: ( Sphere (( 0. TR),c))) by RELAT_1: 126

        .= (MM .: ( Sphere (( 0. TR),c))) by TOPREAL9: 17, RELAT_1: 129

        .= ( Sphere (( 0. TR),1)) by Th16, A71, A76, A77;

      end;

    end;