tietze_2.miz



    begin

    reserve n,m,i for Nat,

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

r,s for Real,

R for real-valued FinSequence;

    registration

      cluster empty -> nonnegative-yielding for FinSequence;

      coherence

      proof

        let F be FinSequence;

        assume F is empty;

        then for r st r in ( rng F) holds r >= 0 ;

        hence thesis by PARTFUN3:def 4;

      end;

    end

    definition

      let n be non zero Nat;

      let X be set;

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

      :: original: <:

      redefine

      func <:F:> -> Function of X, ( TOP-REAL n) ;

      coherence

      proof

        set Y = the carrier of R^1 , TR = the carrier of ( TOP-REAL n);

         A1:

        now

          let x be object;

          assume

           A2: x in ( dom F);

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

          then ex Fx be Function st Fx = (F . x) & ( dom Fx) = X & ( rng Fx) c= Y by FUNCT_2:def 2;

          hence (( doms F) . x) = X by A2, FUNCT_6: 22;

        end;

        

         A3: ( rng <:F:>) c= ( product ( rngs F)) by FUNCT_6: 29;

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

        then

         A4: ( dom F) = ( Seg n) by FINSEQ_1:def 3;

        

         A5: ( dom ( rngs F)) = ( dom F) by FUNCT_6: 60;

        

         A6: ( product ( rngs F)) c= TR

        proof

          let y be object;

          assume y in ( product ( rngs F));

          then

          consider g be Function such that

           A7: y = g and

           A8: ( dom g) = ( dom F) and

           A9: for z be object st z in ( dom F) holds (g . z) in (( rngs F) . z) by CARD_3:def 5, A5;

          reconsider g as FinSequence by A4, A8, FINSEQ_1:def 2;

          ( rng g) c= REAL

          proof

            let z be object;

            assume z in ( rng g);

            then

            consider x be object such that

             A10: x in ( dom g) and

             A11: z = (g . x) by FUNCT_1:def 3;

            

             A12: (( rngs F) . x) = ( rng (F . x)) by A8, A10, FUNCT_6:def 3;

            (g . x) in (( rngs F) . x) by A8, A9, A10;

            hence thesis by A12, A11;

          end;

          then

          reconsider g as FinSequence of REAL by FINSEQ_1:def 4;

          n in NAT by ORDINAL1:def 12;

          then ( len g) = n by A8, A4, FINSEQ_1:def 3;

          hence thesis by A7, TOPREAL7: 17;

        end;

        ( dom ( doms F)) = ( dom F) by FUNCT_6: 59;

        then ( doms F) = (( dom F) --> X) by A1, FUNCOP_1: 11;

        then ( dom <:F:>) = ( meet (( dom F) --> X)) by FUNCT_6: 29;

        then ( dom <:F:>) = X by FUNCT_6: 27;

        hence thesis by A6, A3, XBOOLE_1: 1, FUNCT_2: 2;

      end;

    end

    theorem :: TIETZE_2:1

    

     Th20: for X,Y be set holds for F be Function-yielding Function holds for x,y be object st F is ( Funcs (X,Y)) -valued or y in ( dom <:F:>) holds ((F . x) . y) = (( <:F:> . y) . x)

    proof

      let X,Y be set;

      let F be Function-yielding Function;

      set FF = ( dom F);

      

       A1: ( dom ( doms F)) = ( dom F) by FUNCT_6: 59;

      let x,y be object such that

       A2: F is ( Funcs (X,Y)) -valued or y in ( dom <:F:>);

      per cases by A2;

        suppose y in ( dom <:F:>) & x in ( dom F);

        hence ((F . x) . y) = (( <:F:> . y) . x) by FUNCT_6: 34;

      end;

        suppose

         A3: y in ( dom <:F:>) & not x in ( dom F);

        then ( dom ( <:F:> . y)) = FF by FUNCT_6: 31;

        then

         A4: (( <:F:> . y) . x) = {} by A3, FUNCT_1:def 2;

        (F . x) = {} by A3, FUNCT_1:def 2;

        hence thesis by A4;

      end;

        suppose

         A5: not y in ( dom <:F:>) & x in ( dom F) & F is ( Funcs (X,Y)) -valued;

        then

         A6: ( <:F:> . y) = {} by FUNCT_1:def 2;

        

         A7: ( rng F) c= ( Funcs (X,Y)) by RELAT_1:def 19, A5;

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

        then

        consider Fx be Function such that

         A8: Fx = (F . x) and

         A9: ( dom Fx) = X and ( rng Fx) c= Y by A7, FUNCT_2:def 2;

        now

          let x be object;

          assume

           A10: x in ( dom F);

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

          then ex Fx be Function st Fx = (F . x) & ( dom Fx) = X & ( rng Fx) c= Y by A7, FUNCT_2:def 2;

          hence (( doms F) . x) = X by A10, FUNCT_6: 22;

        end;

        then ( doms F) = (( dom F) --> X) by A1, FUNCOP_1: 11;

        then ( dom <:F:>) = ( meet (( dom F) --> X)) by FUNCT_6: 29;

        then ( dom <:F:>) = X by A5, FUNCT_6: 27;

        then (Fx . y) = {} by A9, A5, FUNCT_1:def 2;

        hence thesis by A6, A8;

      end;

        suppose

         A11: not y in ( dom <:F:>) & not x in ( dom F);

        then

         A12: (F . x) = {} by FUNCT_1:def 2;

        

         A13: ( {} . x) = {} ;

        ( <:F:> . y) = {} by A11, FUNCT_1:def 2;

        hence thesis by A12, A13;

      end;

    end;

    definition

      let n, p, r;

      :: TIETZE_2:def1

      func OpenHypercube (p,r) -> open Subset of ( TOP-REAL n) means

      : Def1: ex e be Point of ( Euclid n) st p = e & it = ( OpenHypercube (e,r));

      existence

      proof

        reconsider e = p as Point of ( Euclid n) by EUCLID: 67;

        

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

        then

        reconsider O = ( OpenHypercube (e,r)) as Subset of ( TOP-REAL n);

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

        then O is open;

        hence thesis;

      end;

      uniqueness ;

    end

    theorem :: TIETZE_2:2

    

     Th1: q in ( OpenHypercube (p,r)) & s in ].((p . i) - r), ((p . i) + r).[ implies (q +* (i,s)) in ( OpenHypercube (p,r))

    proof

      assume that

       A1: q in ( OpenHypercube (p,r)) and

       A2: s in ].((p . i) - r), ((p . i) + r).[;

      consider e be Point of ( Euclid n) such that

       A3: p = e and

       A4: ( OpenHypercube (p,r)) = ( OpenHypercube (e,r)) by Def1;

      set OH = ( OpenHypercube (e,r)), I = ( Intervals (e,r)), qs = (q +* (i,s));

      

       A5: OH = ( product I) by EUCLID_9:def 4;

      then

       A6: ( dom q) = ( dom I) by A4, A1, CARD_3: 9;

      

       A7: ( dom I) = ( dom e) by EUCLID_9:def 3;

      

       A8: for x be object st x in ( dom I) holds (qs . x) in (I . x)

      proof

        let x be object;

        assume

         A9: x in ( dom I);

        then

         A10: (I . x) = ].((e . x) - r), ((e . x) + r).[ by A7, EUCLID_9:def 3;

        

         A11: (q . x) in (I . x) by A9, A1, A5, A4, CARD_3: 9;

        i = x or i <> x;

        hence thesis by A6, A9, A3, FUNCT_7: 31, FUNCT_7: 32, A2, A10, A11;

      end;

      ( dom qs) = ( dom q) by FUNCT_7: 30;

      hence thesis by A4, A8, CARD_3: 9, A6, A5;

    end;

    theorem :: TIETZE_2:3

    

     Th2: i in ( Seg n) implies (( PROJ (n,i)) .: ( OpenHypercube (p,r))) = ].((p . i) - r), ((p . i) + r).[

    proof

      assume

       A1: i in ( Seg n);

      consider e be Point of ( Euclid n) such that

       A2: p = e and

       A3: ( OpenHypercube (p,r)) = ( OpenHypercube (e,r)) by Def1;

      set OH = ( OpenHypercube (e,r)), I = ( Intervals (e,r));

      

       A4: OH = ( product I) by EUCLID_9:def 4;

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

      then

       A5: ( dom e) = ( Seg n) by FINSEQ_1:def 3;

      then

       A6: (I . i) = ].((e . i) - r), ((e . i) + r).[ by A1, EUCLID_9:def 3;

      hereby

        let y be object;

        assume y in (( PROJ (n,i)) .: ( OpenHypercube (p,r)));

        then

        consider x be object such that

         A7: x in ( dom ( PROJ (n,i))) and

         A8: x in OH and

         A9: (( PROJ (n,i)) . x) = y by A3, FUNCT_1:def 6;

        reconsider x as Point of ( TOP-REAL n) by A7;

        

         A10: ( dom I) = ( dom x) by A8, A4, CARD_3: 9;

        then

         A11: ( dom x) = ( Seg n) by EUCLID_9:def 3, A5;

        then

         A12: (x /. i) = (x . i) by A1, PARTFUN1:def 6;

        (x . i) in (I . i) by A11, A10, CARD_3: 9, A8, A4, A1;

        hence y in ].((p . i) - r), ((p . i) + r).[ by A2, TOPREALC:def 6, A12, A6, A9;

      end;

      let y be object;

      assume

       A13: y in ].((p . i) - r), ((p . i) + r).[;

      then

      reconsider s = y as Real;

      

       A14: s < ((e . i) + r) by A2, A13, XXREAL_1: 4;

      set ps = (p +* (i,s));

      ((e . i) - r) < s by A2, A13, XXREAL_1: 4;

      then ((e . i) + ( - r)) < ((e . i) + r) by A14, XXREAL_0: 2;

      then r > 0 by XREAL_1: 6;

      then

       A15: ps in OH by A2, A3, EUCLID_9: 11, Th1, A13;

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

      then

       A16: ( dom ps) = ( Seg n) by FINSEQ_1:def 3;

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

      then

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

      

       A18: ( dom ( PROJ (n,i))) = the carrier of ( TOP-REAL n) by FUNCT_2:def 1;

      (( PROJ (n,i)) . ps) = (ps /. i) by TOPREALC:def 6

      .= (ps . i) by A16, A1, PARTFUN1:def 6

      .= s by A17, A1, FUNCT_7: 31;

      hence thesis by A3, A18, A15, FUNCT_1:def 6;

    end;

    theorem :: TIETZE_2:4

    

     Th3: q in ( OpenHypercube (p,r)) iff for i st i in ( Seg n) holds (q . i) in ].((p . i) - r), ((p . i) + r).[

    proof

      

       A1: ( len q) = n by CARD_1:def 7;

      thus q in ( OpenHypercube (p,r)) implies for i st i in ( Seg n) holds (q . i) in ].((p . i) - r), ((p . i) + r).[

      proof

        assume

         A2: q in ( OpenHypercube (p,r));

        let i such that

         A3: i in ( Seg n);

        set P = ( PROJ (n,i));

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

        then

         A4: (P . q) in (P .: ( OpenHypercube (p,r))) by A2, FUNCT_1:def 6;

        

         A5: (P . q) = (q /. i) by TOPREALC:def 6;

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

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

        then (q /. i) = (q . i) by A3, PARTFUN1:def 6;

        hence thesis by A5, Th2, A3, A4;

      end;

      assume

       A6: for i st i in ( Seg n) holds (q . i) in ].((p . i) - r), ((p . i) + r).[;

      consider e be Point of ( Euclid n) such that

       A7: p = e and

       A8: ( OpenHypercube (p,r)) = ( OpenHypercube (e,r)) by Def1;

      set I = ( Intervals (e,r));

      

       A9: ( dom I) = ( dom e) by EUCLID_9:def 3;

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

      then

       A10: ( dom p) = ( dom q) by A1, FINSEQ_3: 29;

      

       A11: ( dom q) = ( Seg n) by A1, FINSEQ_1:def 3;

       A12:

      now

        let x be object;

        assume

         A13: x in ( dom q);

        then

        reconsider i = x as Nat;

        (q . i) in ].((p . i) - r), ((p . i) + r).[ by A6, A13, A11;

        hence (q . x) in (I . x) by EUCLID_9:def 3, A7, A13, A10;

      end;

      ( product I) = ( OpenHypercube (p,r)) by A8, EUCLID_9:def 4;

      hence thesis by A12, A7, A10, A9, CARD_3: 9;

    end;

    definition

      let n, p, R;

      :: TIETZE_2:def2

      func ClosedHypercube (p,R) -> Subset of ( TOP-REAL n) means

      : Def2: q in it iff for i st i in ( Seg n) holds (q . i) in [.((p . i) - (R . i)), ((p . i) + (R . i)).];

      existence

      proof

        set TR = ( TOP-REAL n);

        set H = { q : for i st i in ( Seg n) holds (q . i) in [.((p . i) - (R . i)), ((p . i) + (R . i)).] };

        H c= the carrier of TR

        proof

          let x be object;

          assume x in H;

          then ex q st q = x & for i st i in ( Seg n) holds (q . i) in [.((p . i) - (R . i)), ((p . i) + (R . i)).];

          hence thesis;

        end;

        then

        reconsider H as Subset of TR;

        take H;

        let q;

        hereby

          assume q in H;

          then ex Q be Point of TR st q = Q & for i st i in ( Seg n) holds (Q . i) in [.((p . i) - (R . i)), ((p . i) + (R . i)).];

          hence for i st i in ( Seg n) holds (q . i) in [.((p . i) - (R . i)), ((p . i) + (R . i)).];

        end;

        thus thesis;

      end;

      uniqueness

      proof

        set TR = ( TOP-REAL n);

        let H1,H2 be Subset of ( TOP-REAL n) such that

         A1: q in H1 iff for i st i in ( Seg n) holds (q . i) in [.((p . i) - (R . i)), ((p . i) + (R . i)).] and

         A2: q in H2 iff for i st i in ( Seg n) holds (q . i) in [.((p . i) - (R . i)), ((p . i) + (R . i)).];

        hereby

          let x be object;

          assume

           A3: x in H1;

          then

          reconsider q = x as Point of TR;

          for i st i in ( Seg n) holds (q . i) in [.((p . i) - (R . i)), ((p . i) + (R . i)).] by A1, A3;

          hence x in H2 by A2;

        end;

        let x be object;

        assume

         A4: x in H2;

        then

        reconsider q = x as Point of TR;

        for i st i in ( Seg n) holds (q . i) in [.((p . i) - (R . i)), ((p . i) + (R . i)).] by A2, A4;

        hence x in H1 by A1;

      end;

    end

    theorem :: TIETZE_2:5

    

     Th4: (ex i st i in (( Seg n) /\ ( dom R)) & (R . i) < 0 ) implies ( ClosedHypercube (p,R)) is empty

    proof

      given i such that

       A1: i in (( Seg n) /\ ( dom R)) and

       A2: (R . i) < 0 ;

      assume ( ClosedHypercube (p,R)) is non empty;

      then

      consider x be object such that

       A3: x in ( ClosedHypercube (p,R));

      reconsider x as Point of ( TOP-REAL n) by A3;

      i in ( Seg n) by A1, XBOOLE_0:def 4;

      then

       A4: (x . i) in [.((p . i) - (R . i)), ((p . i) + (R . i)).] by Def2, A3;

      then

       A5: (x . i) <= ((p . i) + (R . i)) by XXREAL_1: 1;

      ((p . i) - (R . i)) <= (x . i) by A4, XXREAL_1: 1;

      then ((p . i) + ( - (R . i))) <= ((p . i) + (R . i)) by A5, XXREAL_0: 2;

      hence contradiction by A2, XREAL_1: 8;

    end;

    theorem :: TIETZE_2:6

    

     Th5: (for i st i in (( Seg n) /\ ( dom R)) holds (R . i) >= 0 ) implies p in ( ClosedHypercube (p,R))

    proof

      assume

       A1: for i st i in (( Seg n) /\ ( dom R)) holds (R . i) >= 0 ;

      now

        let i;

        assume

         A2: i in ( Seg n);

         A3:

        now

          per cases ;

            suppose i in ( dom R);

            then i in (( Seg n) /\ ( dom R)) by A2, XBOOLE_0:def 4;

            hence (R . i) >= 0 by A1;

          end;

            suppose not i in ( dom R);

            hence (R . i) >= 0 by FUNCT_1:def 2;

          end;

        end;

        then

         A4: ((p . i) + (R . i)) >= (p . i) by XREAL_1: 40;

        ((p . i) - (R . i)) <= (p . i) by A3, XREAL_1: 43;

        hence (p . i) in [.((p . i) - (R . i)), ((p . i) + (R . i)).] by A4, XXREAL_1: 1;

      end;

      hence thesis by Def2;

    end;

    registration

      let n, p;

      let R be nonnegative-yielding real-valued FinSequence;

      cluster ( ClosedHypercube (p,R)) -> non empty;

      coherence

      proof

        now

          let i;

          assume i in (( Seg n) /\ ( dom R));

          then i in ( dom R) by XBOOLE_0:def 4;

          then (R . i) in ( rng R) by FUNCT_1:def 3;

          hence (R . i) >= 0 by PARTFUN3:def 4;

        end;

        hence thesis by Th5;

      end;

    end

    registration

      let n, p, R;

      cluster ( ClosedHypercube (p,R)) -> convex compact;

      coherence

      proof

        set E = ( Euclid n), TE = ( TopSpaceMetr E), TR = ( TOP-REAL n);

        

         A1: the carrier of TR = the carrier of E by EUCLID: 67;

        

         A2: the TopStruct of ( TOP-REAL n) = TE by EUCLID:def 8;

        then

        reconsider H = ( ClosedHypercube (p,R)) as Subset of the TopStruct of TE;

        

         A3: (H ` ) = (( [#] TE) \ H) by SUBSET_1:def 4;

        for e be Point of E st e in (H ` ) holds ex r st r > 0 & ( OpenHypercube (e,r)) c= (H ` )

        proof

          let e be Point of E;

          reconsider ee = e as Point of TR by EUCLID: 67;

          assume e in (H ` );

          then not e in H by A3, XBOOLE_0:def 5;

          then

          consider i such that

           A4: i in ( Seg n) and

           A5: not (e . i) in [.((p . i) - (R . i)), ((p . i) + (R . i)).] by A1, Def2;

          per cases by A5, XXREAL_1: 1;

            suppose

             A6: (e . i) < ((p . i) - (R . i));

            take r = (((p . i) - (R . i)) - (e . i));

            ((e . i) - (e . i)) < r by A6, XREAL_1: 9;

            hence r > 0 ;

            set I = ( Intervals (e,r));

            let x be object;

            assume

             A7: x in ( OpenHypercube (e,r));

            then

             A8: x in ( product I) by EUCLID_9:def 4;

            assume not x in (H ` );

            then not x in (( [#] TE) \ H) by SUBSET_1:def 4;

            then

             A9: x in H by A7, XBOOLE_0:def 5;

            reconsider x as Point of E by TOPMETR: 12, A7;

            reconsider xx = x as Point of TR by EUCLID: 67;

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

            then

             A10: ( dom e) = ( Seg n) by FINSEQ_1:def 3;

            ( dom e) = ( dom I) by EUCLID_9:def 3;

            then (x . i) in (I . i) by A10, A4, A8, CARD_3: 9;

            then (x . i) in ].((e . i) - r), ((e . i) + r).[ by A10, A4, EUCLID_9:def 3;

            then

             A11: (x . i) < ((p . i) - (R . i)) by XXREAL_1: 4;

            (xx . i) in [.((p . i) - (R . i)), ((p . i) + (R . i)).] by A4, A9, Def2;

            hence contradiction by A11, XXREAL_1: 1;

          end;

            suppose

             A12: (e . i) > ((p . i) + (R . i));

            take r = ((e . i) - ((p . i) + (R . i)));

            ((e . i) - (e . i)) < r by A12, XREAL_1: 10;

            hence r > 0 ;

            set I = ( Intervals (e,r));

            let x be object;

            assume

             A13: x in ( OpenHypercube (e,r));

            then

             A14: x in ( product I) by EUCLID_9:def 4;

            assume not x in (H ` );

            then not x in (( [#] TE) \ H) by SUBSET_1:def 4;

            then

             A15: x in H by A13, XBOOLE_0:def 5;

            reconsider x as Point of E by TOPMETR: 12, A13;

            reconsider xx = x as Point of TR by EUCLID: 67;

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

            then

             A16: ( dom e) = ( Seg n) by FINSEQ_1:def 3;

            ( dom e) = ( dom I) by EUCLID_9:def 3;

            then (x . i) in (I . i) by A16, A4, A14, CARD_3: 9;

            then (x . i) in ].((e . i) - r), ((e . i) + r).[ by A16, A4, EUCLID_9:def 3;

            then

             A17: (x . i) > ((p . i) + (R . i)) by XXREAL_1: 4;

            (xx . i) in [.((p . i) - (R . i)), ((p . i) + (R . i)).] by A4, A15, Def2;

            hence contradiction by A17, XXREAL_1: 1;

          end;

        end;

        then (H ` ) is open by EUCLID_9: 24;

        then (( ClosedHypercube (p,R)) ` ) is open by A2;

        then

         A18: ( ClosedHypercube (p,R)) is closed by TOPS_1: 3;

        reconsider h = H as Subset of E by EUCLID: 67;

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

        ( ClosedHypercube (p,R)) is convex

        proof

          let u,w be Point of TR;

          let r be Real;

          assume that

           A19: 0 < r and

           A20: r < 1 and

           A21: u in ( ClosedHypercube (p,R)) and

           A22: w in ( ClosedHypercube (p,R));

          set ru = (r * u), rw = ((1 - r) * w);

          

           A23: (1 - r) > (1 - 1) by A20, XREAL_1: 10;

          now

            let i;

            

             A24: ( len rw) = n by CARD_1:def 7;

            assume

             A25: i in ( Seg n);

            then

             A26: (u . i) in [.((p . i) - (R . i)), ((p . i) + (R . i)).] by A21, Def2;

            then (u . i) >= ((p . i) - (R . i)) by XXREAL_1: 1;

            then

             A27: (r * (u . i)) >= (r * ((p . i) - (R . i))) by A19, XREAL_1: 64;

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

            then ( dom ru) = ( dom rw) by A24, FINSEQ_3: 29;

            then i in (( dom ru) /\ ( dom rw)) by A24, FINSEQ_1:def 3, A25;

            then i in ( dom (ru + rw)) by VALUED_1:def 1;

            then

             A28: ((ru + rw) . i) = ((ru . i) + (rw . i)) by VALUED_1:def 1;

            (u . i) <= ((p . i) + (R . i)) by A26, XXREAL_1: 1;

            then

             A29: (r * (u . i)) <= (r * ((p . i) + (R . i))) by A19, XREAL_1: 64;

            

             A30: (ru . i) = (r * (u . i)) by VALUED_1: 6;

            

             A31: (rw . i) = ((1 - r) * (w . i)) by VALUED_1: 6;

            

             A32: (w . i) in [.((p . i) - (R . i)), ((p . i) + (R . i)).] by A25, A22, Def2;

            then (w . i) <= ((p . i) + (R . i)) by XXREAL_1: 1;

            then ((1 - r) * (w . i)) <= ((1 - r) * ((p . i) + (R . i))) by A23, XREAL_1: 64;

            then

             A33: ((ru + rw) . i) <= ((r * ((p . i) + (R . i))) + ((1 - r) * ((p . i) + (R . i)))) by A29, A30, A31, A28, XREAL_1: 7;

            (w . i) >= ((p . i) - (R . i)) by A32, XXREAL_1: 1;

            then ((1 - r) * (w . i)) >= ((1 - r) * ((p . i) - (R . i))) by A23, XREAL_1: 64;

            then ((ru + rw) . i) >= ((r * ((p . i) - (R . i))) + ((1 - r) * ((p . i) - (R . i)))) by A27, A30, A31, A28, XREAL_1: 7;

            hence ((ru + rw) . i) in [.((p . i) - (R . i)), ((p . i) + (R . i)).] by A33, XXREAL_1: 1;

          end;

          hence thesis by Def2;

        end;

        hence ( ClosedHypercube (p,R)) is convex;

        per cases ;

          suppose

           A34: (R .: ( Seg n)) is empty;

          H c= {p}

          proof

            let x be object;

            

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

            assume

             A36: x in H;

            then

            reconsider x as Point of TR;

             A37:

            now

              let i;

              assume that

               A38: 1 <= i and

               A39: i <= n;

              

               A40: i in ( Seg n) by A38, A39, FINSEQ_1: 1;

               not (R . i) in (R .: ( Seg n)) by A34;

              then not i in ( dom R) by A40, FUNCT_1:def 6;

              then

               A41: (R . i) = 0 by FUNCT_1:def 2;

              (x . i) in [.((p . i) - (R . i)), ((p . i) + (R . i)).] by A40, A36, Def2;

              then (x . i) in {(p . i)} by A41, XXREAL_1: 17;

              hence (x . i) = (p . i) by TARSKI:def 1;

            end;

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

            then x = p by A35, A37, FINSEQ_1: 14;

            hence thesis by TARSKI:def 1;

          end;

          then h is bounded;

          then ( ClosedHypercube (p,R)) is bounded by JORDAN2C: 11;

          hence thesis by A18;

        end;

          suppose

           A42: (R .: ( Seg n)) is non empty;

          then

          reconsider RS = (R .: ( Seg n)) as right_end real-membered set;

          set m = (( max RS) + 1);

          set O = ( OpenHypercube (P,m));

          set I = ( Intervals (P,m));

          

           A43: H c= O

          proof

            let x be object;

            

             A44: ( dom I) = ( dom P) by EUCLID_9:def 3;

            assume

             A45: x in H;

            then

            reconsider x as Point of TR;

            

             A46: ( len x) = n by CARD_1:def 7;

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

            then

             A47: ( dom x) = ( dom p) by A46, FINSEQ_3: 29;

            

             A48: ( dom x) = ( Seg n) by A46, FINSEQ_1:def 3;

            for z be object st z in ( dom I) holds (x . z) in (I . z)

            proof

              let z be object;

              assume

               A49: z in ( dom I);

              then

               A50: (x . z) in [.((P . z) - (R . z)), ((p . z) + (R . z)).] by A45, A47, A48, A44, Def2;

              then

               A51: ((P . z) - (R . z)) <= (x . z) by XXREAL_1: 1;

               A52:

              now

                per cases ;

                  suppose z in ( dom R);

                  then (R . z) in RS by A49, A47, A48, A44, FUNCT_1:def 6;

                  then (R . z) <= ( max RS) by XXREAL_2:def 8;

                  then ((R . z) + 0 ) < m by XREAL_1: 8;

                  hence (R . z) < m;

                end;

                  suppose

                   A53: not z in ( dom R);

                  ( Seg n) meets ( dom R) by A42, RELAT_1: 118;

                  then

                  consider i be object such that

                   A54: i in ( Seg n) and

                   A55: i in ( dom R) by XBOOLE_0: 3;

                  reconsider i as Nat by A54;

                  i in (( Seg n) /\ ( dom R)) by A54, A55, XBOOLE_0:def 4;

                  then

                   A56: (R . i) >= 0 by Th4, A45;

                  (R . i) in RS by A54, A55, FUNCT_1:def 6;

                  then (R . i) <= ( max RS) by XXREAL_2:def 8;

                  then ( 0 + 0 ) < m by A56;

                  hence (R . z) < m by A53, FUNCT_1:def 2;

                end;

              end;

              then ((P . z) - m) < ((P . z) - (R . z)) by XREAL_1: 10;

              then

               A57: ((P . z) - m) < (x . z) by A51, XXREAL_0: 2;

              

               A58: (x . z) <= ((p . z) + (R . z)) by A50, XXREAL_1: 1;

              ((P . z) + m) > ((P . z) + (R . z)) by A52, XREAL_1: 8;

              then

               A59: (x . z) < ((P . z) + m) by A58, XXREAL_0: 2;

              (I . z) = ].((P . z) - m), ((P . z) + m).[ by A49, A44, EUCLID_9:def 3;

              hence (x . z) in (I . z) by A57, A59, XXREAL_1: 4;

            end;

            then x in ( product I) by A47, A44, CARD_3: 9;

            hence thesis by EUCLID_9:def 4;

          end;

          n <> 0 by A42;

          then O c= ( Ball (P,(m * ( sqrt n)))) by EUCLID_9: 18;

          then h is bounded by A43, XBOOLE_1: 1, TBSP_1: 14;

          then ( ClosedHypercube (p,R)) is bounded by JORDAN2C: 11;

          hence thesis by A18;

        end;

      end;

    end

    theorem :: TIETZE_2:7

    

     Th6: i in ( Seg n) & q in ( ClosedHypercube (p,R)) & r in [.((p . i) - (R . i)), ((p . i) + (R . i)).] implies (q +* (i,r)) in ( ClosedHypercube (p,R))

    proof

      set H = ( ClosedHypercube (p,R)), pr = (q +* (i,r));

      assume that

       A1: i in ( Seg n) and

       A2: q in H and

       A3: r in [.((p . i) - (R . i)), ((p . i) + (R . i)).];

      for j be Nat st j in ( Seg n) holds (pr . j) in [.((p . j) - (R . j)), ((p . j) + (R . j)).]

      proof

        let j be Nat;

        assume

         A4: j in ( Seg n);

        

         A5: ( dom q) = ( Seg ( len q)) by FINSEQ_1:def 3;

        

         A6: ( len q) = n by CARD_1:def 7;

        per cases ;

          suppose i <> j;

          then (pr . j) = (q . j) by FUNCT_7: 32;

          hence thesis by Def2, A4, A2;

        end;

          suppose i = j;

          hence thesis by FUNCT_7: 31, A1, A5, A6, A3;

        end;

      end;

      hence thesis by Def2;

    end;

    theorem :: TIETZE_2:8

    

     Th7: i in ( Seg n) & ( ClosedHypercube (p,R)) is non empty implies (( PROJ (n,i)) .: ( ClosedHypercube (p,R))) = [.((p . i) - (R . i)), ((p . i) + (R . i)).]

    proof

      set P = ( PROJ (n,i)), H = ( ClosedHypercube (p,R)), TR = ( TOP-REAL n);

      assume that

       A1: i in ( Seg n) and

       A2: H is non empty;

      hereby

        let y be object;

        assume y in (P .: H);

        then

        consider x be object such that

         A3: x in ( dom P) and

         A4: x in H and

         A5: (P . x) = y by FUNCT_1:def 6;

        reconsider x as Point of TR by A3;

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

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

        then

         A6: (x /. i) = (x . i) by A1, PARTFUN1:def 6;

        (P . x) = (x /. i) by TOPREALC:def 6;

        hence y in [.((p . i) - (R . i)), ((p . i) + (R . i)).] by A6, A1, A4, A5, Def2;

      end;

      let y be object;

      assume

       A7: y in [.((p . i) - (R . i)), ((p . i) + (R . i)).];

      then

      reconsider r = y as Real;

      set pr = (p +* (i,r));

      

       A8: ( dom P) = the carrier of TR by FUNCT_2:def 1;

      

       A9: ( dom pr) = ( Seg ( len pr)) by FINSEQ_1:def 3;

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

      then

       A10: (pr /. i) = (pr . i) by A9, A1, PARTFUN1:def 6;

      

       A11: ( dom p) = ( Seg ( len p)) by FINSEQ_1:def 3;

      for i st i in (( Seg n) /\ ( dom R)) holds (R . i) >= 0 by A2, Th4;

      then pr in H by A1, Th6, A7, Th5;

      then

       A12: (P . pr) in (P .: H) by A8, FUNCT_1:def 6;

      

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

      (P . pr) = (pr /. i) by TOPREALC:def 6;

      hence thesis by A13, A11, A10, A1, FUNCT_7: 31, A12;

    end;

    theorem :: TIETZE_2:9

    

     Th8: n <= ( len R) & r <= ( inf ( rng R)) implies ( OpenHypercube (p,r)) c= ( ClosedHypercube (p,R))

    proof

      set H = ( ClosedHypercube (p,R));

      assume that

       A1: n <= ( len R) and

       A2: r <= ( inf ( rng R));

      

       A3: ( Seg n) c= ( Seg ( len R)) by A1, FINSEQ_1: 5;

      set E = ( Euclid n), TE = ( TopSpaceMetr E), TR = ( TOP-REAL n);

      let x be object;

      

       A4: ( Seg ( len R)) = ( dom R) by FINSEQ_1:def 3;

      assume

       A5: x in ( OpenHypercube (p,r));

      then

      reconsider q = x as Point of TR;

      consider e be Point of ( Euclid n) such that

       A6: p = e and

       A7: ( OpenHypercube (p,r)) = ( OpenHypercube (e,r)) by Def1;

      set I = ( Intervals (e,r));

      

       A8: x in ( product I) by A5, A7, EUCLID_9:def 4;

      now

        let i;

        

         A9: ( dom I) = ( dom e) by EUCLID_9:def 3;

        assume

         A10: i in ( Seg n);

        then (R . i) in ( rng R) by A3, A4, FUNCT_1:def 3;

        then ( inf ( rng R)) <= (R . i) by XXREAL_2: 3;

        then

         A11: r <= (R . i) by A2, XXREAL_0: 2;

        then

         A12: ((e . i) + r) <= ((e . i) + (R . i)) by XREAL_1: 6;

        

         A13: ( dom p) = ( Seg ( len p)) by FINSEQ_1:def 3;

        

         A14: ((e . i) - r) >= ((e . i) - (R . i)) by A11, XREAL_1: 10;

        

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

        then (I . i) = ].((e . i) - r), ((e . i) + r).[ by A13, A6, A10, EUCLID_9:def 3;

        then

         A16: (q . i) in ].((e . i) - r), ((e . i) + r).[ by A9, CARD_3: 9, A6, A10, A15, A13, A8;

        then ((e . i) - r) < (q . i) by XXREAL_1: 4;

        then

         A17: ((p . i) - (R . i)) < (q . i) by A14, A6, XXREAL_0: 2;

        (q . i) < ((e . i) + r) by A16, XXREAL_1: 4;

        then (q . i) < ((p . i) + (R . i)) by A12, A6, XXREAL_0: 2;

        hence (q . i) in [.((p . i) - (R . i)), ((p . i) + (R . i)).] by A17, XXREAL_1: 1;

      end;

      hence thesis by Def2;

    end;

    theorem :: TIETZE_2:10

    

     Th9: q in ( Fr ( ClosedHypercube (p,R))) iff q in ( ClosedHypercube (p,R)) & ex i st i in ( Seg n) & ((q . i) = ((p . i) - (R . i)) or (q . i) = ((p . i) + (R . i)))

    proof

      set TR = ( TOP-REAL n);

      

       A1: ( Fr ( ClosedHypercube (p,R))) c= ( ClosedHypercube (p,R)) by TOPS_1: 35;

      thus q in ( Fr ( ClosedHypercube (p,R))) implies q in ( ClosedHypercube (p,R)) & ex i st i in ( Seg n) & ((q . i) = ((p . i) - (R . i)) or (q . i) = ((p . i) + (R . i)))

      proof

        deffunc l1( set) = ((q . $1) - ((p . $1) - (R . $1)));

        deffunc r1( set) = (((p . $1) + (R . $1)) - (q . $1));

        consider L1 be FinSequence such that

         A2: ( len L1) = n & for i st i in ( dom L1) holds (L1 . i) = l1(i) from FINSEQ_1:sch 2;

        now

          let y be object;

          assume y in ( rng L1);

          then

          consider x be object such that

           A3: x in ( dom L1) and

           A4: (L1 . x) = y by FUNCT_1:def 3;

          reconsider x as Nat by A3;

          (L1 . x) = l1(x) by A2, A3;

          hence y is real by A4;

        end;

        then

         A5: ( rng L1) is real-membered by MEMBERED:def 3;

        consider R1 be FinSequence such that

         A6: ( len R1) = n & for i st i in ( dom R1) holds (R1 . i) = r1(i) from FINSEQ_1:sch 2;

        now

          let y be object;

          assume y in ( rng R1);

          then

          consider x be object such that

           A7: x in ( dom R1) and

           A8: (R1 . x) = y by FUNCT_1:def 3;

          reconsider x as Nat by A7;

          (R1 . x) = r1(x) by A7, A6;

          hence y is real by A8;

        end;

        then

         A9: ( rng R1) is real-membered by MEMBERED:def 3;

        

         A10: ( dom L1) = ( Seg n) by A2, FINSEQ_1:def 3;

        assume

         A11: q in ( Fr ( ClosedHypercube (p,R)));

        hence q in ( ClosedHypercube (p,R)) by A1;

        assume

         A12: for i st i in ( Seg n) holds (q . i) <> ((p . i) - (R . i)) & (q . i) <> ((p . i) + (R . i));

        n > 0

        proof

          assume n <= 0 ;

          then n = 0 ;

          then

           A13: {( 0. TR)} = the carrier of TR by EUCLID: 22, JORDAN2C: 105;

          ( [#] TR) is open;

          hence thesis by A13, A11, ZFMISC_1: 33;

        end;

        then n in ( Seg n) by FINSEQ_1: 3;

        then (L1 . n) in ( rng L1) by A10, FUNCT_1:def 3;

        then

        reconsider D = (( rng L1) \/ ( rng R1)) as non empty finite real-membered set by A9, A5;

        set m = ( min D);

        consider e be Point of ( Euclid n) such that

         A14: q = e and

         A15: ( OpenHypercube (q,m)) = ( OpenHypercube (e,m)) by Def1;

        

         A16: ( dom R1) = ( Seg n) by A6, FINSEQ_1:def 3;

        

         A17: m in D by XXREAL_2:def 7;

        

         A18: m > 0

        proof

          per cases by A17, XBOOLE_0:def 3;

            suppose ( min D) in ( rng L1);

            then

            consider x be object such that

             A19: x in ( dom L1) and

             A20: (L1 . x) = m by FUNCT_1:def 3;

            reconsider x as Nat by A19;

            (q . x) in [.((p . x) - (R . x)), ((p . x) + (R . x)).] by A11, A1, A19, A10, Def2;

            then (q . x) >= ((p . x) - (R . x)) by XXREAL_1: 1;

            then

             A21: (q . x) > ((p . x) - (R . x)) by A19, A10, A12, XXREAL_0: 1;

            (L1 . x) = l1(x) by A2, A19;

            hence thesis by A21, XREAL_1: 50, A20;

          end;

            suppose ( min D) in ( rng R1);

            then

            consider x be object such that

             A22: x in ( dom R1) and

             A23: (R1 . x) = m by FUNCT_1:def 3;

            reconsider x as Nat by A22;

            (q . x) in [.((p . x) - (R . x)), ((p . x) + (R . x)).] by A11, A1, A22, A16, Def2;

            then (q . x) <= ((p . x) + (R . x)) by XXREAL_1: 1;

            then

             A24: (q . x) < ((p . x) + (R . x)) by A22, A16, A12, XXREAL_0: 1;

            (R1 . x) = r1(x) by A6, A22;

            hence thesis by A24, XREAL_1: 50, A23;

          end;

        end;

        set O = ( OpenHypercube (e,m));

        O c= ( ClosedHypercube (p,R))

        proof

          let x be object;

          assume

           A25: x in O;

          then

          reconsider w = x as Point of ( Euclid n) by TOPMETR: 12;

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

          for i st i in ( Seg n) holds (W . i) in [.((p . i) - (R . i)), ((p . i) + (R . i)).]

          proof

            let i;

            set P = ( PROJ (n,i));

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

            then

             A26: ( dom W) = ( Seg n) by FINSEQ_1:def 3;

            ( dom P) = the carrier of TR by FUNCT_2:def 1;

            then

             A27: (P . W) in (P .: O) by A25, FUNCT_1:def 6;

            assume

             A28: i in ( Seg n);

            then (L1 . i) in ( rng L1) by A10, FUNCT_1:def 3;

            then

             A29: (L1 . i) in D by XBOOLE_0:def 3;

            (L1 . i) = l1(i) by A10, A2, A28;

            then m <= l1(i) by A29, XXREAL_2:def 7;

            then

             A30: ((q . i) - m) >= ((q . i) - l1(i)) by XREAL_1: 10;

            (P . W) = (W /. i) by TOPREALC:def 6

            .= (W . i) by A28, A26, PARTFUN1:def 6;

            then

             A31: (W . i) in ].((e . i) - m), ((e . i) + m).[ by A14, A15, A28, Th2, A27;

            then (W . i) > ((q . i) - m) by A14, XXREAL_1: 4;

            then

             A32: (W . i) > ((p . i) - (R . i)) by A30, XXREAL_0: 2;

            (R1 . i) in ( rng R1) by A28, A16, FUNCT_1:def 3;

            then

             A33: (R1 . i) in D by XBOOLE_0:def 3;

            (R1 . i) = r1(i) by A16, A6, A28;

            then m <= r1(i) by A33, XXREAL_2:def 7;

            then

             A34: ((q . i) + m) <= ((q . i) + r1(i)) by XREAL_1: 6;

            (W . i) < ((q . i) + m) by A31, A14, XXREAL_1: 4;

            then (W . i) < ((p . i) + (R . i)) by A34, XXREAL_0: 2;

            hence thesis by A32, XXREAL_1: 1;

          end;

          hence thesis by Def2;

        end;

        then q in ( Int ( ClosedHypercube (p,R))) by A18, A14, A15, EUCLID_9: 11, TOPS_1: 22;

        hence contradiction by TOPS_1: 39, A11, XBOOLE_0: 3;

      end;

      assume

       A35: q in ( ClosedHypercube (p,R));

      given i such that

       A36: i in ( Seg n) and

       A37: (q . i) = ((p . i) - (R . i)) or (q . i) = ((p . i) + (R . i));

      for S be Subset of TR st S is open & q in S holds ( ClosedHypercube (p,R)) meets S & (( ClosedHypercube (p,R)) ` ) meets S

      proof

        let S be Subset of TR;

        reconsider Q = q as Point of ( Euclid n) by EUCLID: 67;

        assume that

         A38: S is open and

         A39: q in S;

        thus ( ClosedHypercube (p,R)) meets S by A39, A35, XBOOLE_0: 3;

        ( Int S) = S by A38, TOPS_1: 23;

        then

        consider s be Real such that

         A40: s > 0 and

         A41: ( Ball (Q,s)) c= S by A39, GOBOARD6: 5;

        set s2 = (s / 2);

        

         A42: 0 < s2 & s2 < s by XREAL_1: 216, A40;

        

         A43: ( Ball (Q,s)) = ( Ball (q,s)) by TOPREAL9: 13;

        per cases by A37;

          suppose

           A44: (q . i) = ((p . i) - (R . i));

          set q1 = (q +* (i,((q . i) - s2)));

          reconsider q1 as Point of TR;

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

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

          then (q1 . i) = ((q . i) - s2) by A36, FUNCT_7: 31;

          then (q1 . i) < ((q . i) + 0 ) by A40, XREAL_1: 6;

          then not (q1 . i) in [.((p . i) - (R . i)), ((p . i) + (R . i)).] by A44, XXREAL_1: 1;

          then not q1 in ( ClosedHypercube (p,R)) by A36, Def2;

          then q1 in (( [#] TR) \ ( ClosedHypercube (p,R))) by XBOOLE_0:def 5;

          then

           A45: q1 in (( ClosedHypercube (p,R)) ` ) by SUBSET_1:def 4;

          (q1 - q) = (( 0* n) +* (i,(((q . i) - s2) - (q . i)))) by TOPREALC: 17;

          

          then |.(q1 - q).| = |.(((q . i) - s2) - (q . i)).| by A36, TOPREALC: 13

          .= ( - ( - s2)) by A40, ABSVALUE:def 1

          .= s2;

          then q1 in ( Ball (q,s)) by A42;

          hence (( ClosedHypercube (p,R)) ` ) meets S by A43, A41, XBOOLE_0: 3, A45;

        end;

          suppose

           A46: (q . i) = ((p . i) + (R . i));

          set q1 = (q +* (i,((q . i) + s2)));

          reconsider q1 as Point of TR;

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

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

          then (q1 . i) = ((q . i) + s2) by A36, FUNCT_7: 31;

          then (q1 . i) > ((q . i) + 0 ) by A40, XREAL_1: 6;

          then not (q1 . i) in [.((p . i) - (R . i)), ((p . i) + (R . i)).] by A46, XXREAL_1: 1;

          then not q1 in ( ClosedHypercube (p,R)) by A36, Def2;

          then q1 in (( [#] TR) \ ( ClosedHypercube (p,R))) by XBOOLE_0:def 5;

          then

           A47: q1 in (( ClosedHypercube (p,R)) ` ) by SUBSET_1:def 4;

          (q1 - q) = (( 0* n) +* (i,(((q . i) + s2) - (q . i)))) by TOPREALC: 17;

          

          then |.(q1 - q).| = |.(((q . i) + s2) - (q . i)).| by A36, TOPREALC: 13

          .= s2 by A40, ABSVALUE:def 1;

          then q1 in ( Ball (q,s)) by A42;

          hence (( ClosedHypercube (p,R)) ` ) meets S by A43, A41, XBOOLE_0: 3, A47;

        end;

      end;

      hence thesis by TOPS_1: 28;

    end;

    theorem :: TIETZE_2:11

    r >= 0 implies p in ( ClosedHypercube (p,(n |-> r)))

    proof

      set R = (n |-> r);

      assume r >= 0 ;

      then for i st i in (( Seg n) /\ ( dom R)) holds (R . i) >= 0 by FINSEQ_2: 57;

      hence thesis by Th5;

    end;

    theorem :: TIETZE_2:12

    

     Th11: r > 0 implies ( Int ( ClosedHypercube (p,(n |-> r)))) = ( OpenHypercube (p,r))

    proof

      assume r > 0 ;

      set O = ( OpenHypercube (p,r));

      set C = ( ClosedHypercube (p,(n |-> r)));

      set TR = ( TOP-REAL n), R = (n |-> r);

      

       A1: ( Int C) c= C by TOPS_1: 16;

      consider e be Point of ( Euclid n) such that

       A2: p = e and

       A3: ( OpenHypercube (p,r)) = ( OpenHypercube (e,r)) by Def1;

      set I = ( Intervals (e,r));

      

       A4: O = ( product I) by A3, EUCLID_9:def 4;

      thus ( Int C) c= O

      proof

        let x be object;

        

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

        then

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

        assume

         A7: x in ( Int C);

        then

        reconsider q = x as Point of TR;

        

         A8: ( dom p) = ( dom I) by A2, EUCLID_9:def 3;

        

         A9: not q in ( Fr C) by TOPS_1: 39, A7, XBOOLE_0: 3;

        

         A10: for z be object st z in ( dom I) holds (q . z) in (I . z)

        proof

          let z be object;

          assume

           A11: z in ( dom I);

          then

           A12: (I . z) = ].((e . z) - r), ((e . z) + r).[ by A2, A8, EUCLID_9:def 3;

          reconsider z as Nat by A11;

          

           A13: (R . z) = r by FINSEQ_2: 57, A8, A6, A11;

          

           A14: (q . z) in [.((p . z) - (R . z)), ((p . z) + (R . z)).] by A1, A7, A8, A6, A11, Def2;

          then ((p . z) - r) <= (q . z) by A13, XXREAL_1: 1;

          then

           A15: ((p . z) - r) < (q . z) by A13, A9, A1, A7, Th9, A8, A6, A11, XXREAL_0: 1;

          (q . z) <= ((p . z) + r) by A14, A13, XXREAL_1: 1;

          then (q . z) < ((p . z) + r) by A13, A9, A1, A7, Th9, A8, A6, A11, XXREAL_0: 1;

          hence thesis by A15, A2, A12, XXREAL_1: 4;

        end;

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

        then ( dom q) = ( dom p) by A5, FINSEQ_3: 29;

        hence thesis by A10, CARD_3: 9, A8, A4;

      end;

      let x be object;

      assume

       A16: x in O;

      then

      reconsider q = x as Point of TR;

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

      then

       A17: ( dom q) = ( Seg n) by FINSEQ_1:def 3;

      for i st i in ( Seg n) holds (q . i) in [.((p . i) - (R . i)), ((p . i) + (R . i)).]

      proof

        let i;

        

         A18: ( dom ( PROJ (n,i))) = ( [#] TR) by FUNCT_2:def 1;

        assume

         A19: i in ( Seg n);

        then

         A20: (R . i) = r by FINSEQ_2: 57;

        (( PROJ (n,i)) .: O) = ].((e . i) - r), ((e . i) + r).[ by A19, A2, Th2;

        then

         A21: (( PROJ (n,i)) . q) in ].((e . i) - r), ((e . i) + r).[ by A18, A16, FUNCT_1:def 6;

        

         A22: (( PROJ (n,i)) . q) = (q /. i) by TOPREALC:def 6;

        

         A23: (q /. i) = (q . i) by A19, A17, PARTFUN1:def 6;

        then

         A24: (q . i) <= ((p . i) + (R . i)) by A20, A22, A21, A2, XXREAL_1: 4;

        (q . i) >= ((p . i) - (R . i)) by A20, A23, A22, A21, A2, XXREAL_1: 4;

        hence thesis by A24, XXREAL_1: 1;

      end;

      then

       A25: q in C by Def2;

      assume not x in ( Int C);

      then q in (C \ ( Int C)) by A25, XBOOLE_0:def 5;

      then q in ( Fr C) by TOPS_1: 43;

      then

      consider i such that

       A26: i in ( Seg n) and

       A27: (q . i) = ((p . i) - (R . i)) or (q . i) = ((p . i) + (R . i)) by Th9;

      

       A28: ( dom ( PROJ (n,i))) = ( [#] TR) by FUNCT_2:def 1;

      (( PROJ (n,i)) .: O) = ].((e . i) - r), ((e . i) + r).[ by A2, A26, Th2;

      then

       A29: (( PROJ (n,i)) . q) in ].((e . i) - r), ((e . i) + r).[ by A28, A16, FUNCT_1:def 6;

      

       A30: (R . i) = r by A26, FINSEQ_2: 57;

      (( PROJ (n,i)) . q) = (q /. i) by TOPREALC:def 6;

      then (q . i) in ].((e . i) - r), ((e . i) + r).[ by A17, A26, PARTFUN1:def 6, A29;

      hence contradiction by A2, A30, XXREAL_1: 4, A27;

      reconsider oo = O as Subset of TR;

    end;

    theorem :: TIETZE_2:13

    

     Th12: ( OpenHypercube (p,r)) c= ( ClosedHypercube (p,(n |-> r)))

    proof

      set TR = ( TOP-REAL n);

      per cases ;

        suppose

         A1: n = 0 ;

        then for i st i in ( Seg n) holds (( 0. TR) . i) in [.((p . i) - ((n |-> r) . i)), ((p . i) + ((n |-> r) . i)).];

        then

         A2: ( 0. TR) in ( ClosedHypercube (p,(n |-> r))) by Def2;

        the carrier of TR = {( 0. TR)} by JORDAN2C: 105, A1, EUCLID: 22;

        then ( ClosedHypercube (p,(n |-> r))) = ( [#] TR) by A2, ZFMISC_1: 33;

        hence thesis;

      end;

        suppose n > 0 ;

        then ( rng (n |-> r)) = {r} by FUNCOP_1: 8;

        then

         A3: ( inf ( rng (n |-> r))) = r by XXREAL_2: 13;

        ( len (n |-> r)) = n by CARD_1:def 7;

        hence thesis by Th8, A3;

      end;

    end;

    theorem :: TIETZE_2:14

    r < s implies ( ClosedHypercube (p,(n |-> r))) c= ( OpenHypercube (p,s))

    proof

      assume

       A1: r < s;

      let x be object such that

       A2: x in ( ClosedHypercube (p,(n |-> r)));

      reconsider q = x as Point of ( TOP-REAL n) by A2;

      now

        let i such that

         A3: i in ( Seg n);

        ((n |-> r) . i) = r by A3, FINSEQ_2: 57;

        then

         A4: (q . i) in [.((p . i) - r), ((p . i) + r).] by A2, A3, Def2;

        

         A5: ((p . i) + r) < ((p . i) + s) by A1, XREAL_1: 6;

        (q . i) <= ((p . i) + r) by A4, XXREAL_1: 1;

        then

         A6: (q . i) < ((p . i) + s) by A5, XXREAL_0: 2;

        

         A7: ((p . i) - r) > ((p . i) - s) by A1, XREAL_1: 10;

        (q . i) >= ((p . i) - r) by A4, XXREAL_1: 1;

        then (q . i) > ((p . i) - s) by A7, XXREAL_0: 2;

        hence (q . i) in ].((p . i) - s), ((p . i) + s).[ by A6, XXREAL_1: 4;

      end;

      hence thesis by Th3;

    end;

    registration

      let n, p;

      let r be positive Real;

      cluster ( ClosedHypercube (p,(n |-> r))) -> non boundary;

      coherence

      proof

        

         A1: ex e be Point of ( Euclid n) st p = e & ( OpenHypercube (p,r)) = ( OpenHypercube (e,r)) by Def1;

        ( OpenHypercube (p,r)) c= ( Int ( ClosedHypercube (p,(n |-> r)))) by Th12, TOPS_1: 24;

        hence thesis by A1;

      end;

    end

    begin

    reserve T1,T2,S1,S2 for non empty TopSpace,

t1 for Point of T1,

t2 for Point of T2,

pn,qn for Point of ( TOP-REAL n),

pm,qm for Point of ( TOP-REAL m);

    theorem :: TIETZE_2:15

    

     Th14: for f be Function of T1, T2 holds for g be Function of S1, S2 st f is being_homeomorphism & g is being_homeomorphism holds [:f, g:] is being_homeomorphism

    proof

      let f be Function of T1, T2;

      let g be Function of S1, S2 such that

       A1: f is being_homeomorphism and

       A2: g is being_homeomorphism;

      

       A3: ( rng g) = ( [#] S2) by A2, TOPS_2:def 5;

      

       A4: (g " ) is continuous by A2, TOPS_2:def 5;

      

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

      

       A6: the carrier of [:T2, S2:] = [:the carrier of T2, the carrier of S2:] by BORSUK_1:def 2;

      set fg = [:f, g:];

      

       A7: ( rng f) = ( [#] T2) by A1, TOPS_2:def 5;

      then

       A8: ( rng fg) = ( [#] [:T2, S2:]) by A3, FUNCT_3: 67, A6;

      reconsider F = f, G = g, FG = fg as Function;

      

       A9: (FG " ) = [:(F " ), (G " ):] by A1, A2, FUNCTOR0: 6;

      

       A10: (F " ) = (f " ) by A1, TOPS_2:def 4;

      

       A11: ( rng fg) = [:( rng f), ( rng g):] by FUNCT_3: 67;

      then fg is onto by A6, A7, A3, FUNCT_2:def 3;

      then

       A12: (FG " ) = (fg " ) by A1, A2, TOPS_2:def 4;

       A13:

      now

        let P be Subset of [:T2, S2:];

        thus P is open implies (fg " P) is open by BORSUK_2: 10, A1, A2;

        thus (fg " P) is open implies P is open

        proof

          assume

           A14: (fg " P) is open;

          ( [:(f " ), (g " ):] " (fg " P)) = ((fg " ) " (fg " P)) by A10, A2, TOPS_2:def 4, A9, A12

          .= (fg .: (fg " P)) by TOPS_2: 54, A1, A2, A8

          .= P by FUNCT_1: 77, A7, A3, A11, A6;

          hence thesis by BORSUK_2: 10, A5, A4, A14;

        end;

      end;

      

       A15: ( dom g) = ( [#] S1) by A2, TOPS_2:def 5;

      

       A16: the carrier of [:T1, S1:] = [:the carrier of T1, the carrier of S1:] by BORSUK_1:def 2;

      ( dom f) = ( [#] T1) by A1, TOPS_2:def 5;

      then ( dom fg) = ( [#] [:T1, S1:]) by A15, FUNCT_3:def 8, A16;

      hence thesis by A13, TOPGRP_1: 26, A1, A2, A8;

    end;

    theorem :: TIETZE_2:16

    

     Th15: for r, s st r > 0 & s > 0 holds ex h be Function of [:(( TOP-REAL n) | ( ClosedHypercube (pn,(n |-> r)))), (( TOP-REAL m) | ( ClosedHypercube (pm,(m |-> s)))):], (( TOP-REAL (n + m)) | ( ClosedHypercube (( 0. ( TOP-REAL (n + m))),((n + m) |-> 1)))) st h is being_homeomorphism & (h .: [:( OpenHypercube (pn,r)), ( OpenHypercube (pm,s)):]) = ( OpenHypercube (( 0. ( TOP-REAL (n + m))),1))

    proof

      let r, s such that

       A1: r > 0 and

       A2: s > 0 ;

      set TRn = ( TOP-REAL n), TRm = ( TOP-REAL m), nm = (n + m), TRnm = ( TOP-REAL nm);

      set RN = ( ClosedHypercube (( 0. TRn),(n |-> 1))), RR = ( ClosedHypercube (pn,(n |-> r))), RS = ( ClosedHypercube (pm,(m |-> s))), RM = ( ClosedHypercube (( 0. TRm),(m |-> 1))), RNM = ( ClosedHypercube (( 0. TRnm),(nm |-> 1)));

      reconsider Rs = RS, Rm = RM as non empty Subset of TRm by A2;

      consider hm be Function of (TRm | Rs), (TRm | Rm) such that

       A3: hm is being_homeomorphism and

       A4: (hm .: ( Fr Rs)) = ( Fr Rm) by A2, BROUWER2: 7;

      

       A5: ( dom hm) = ( [#] (TRm | Rs)) by A3, TOPS_2:def 5;

      ( 0. TRm) = ( 0* m) by EUCLID: 70;

      then

       A6: ( 0. TRm) = (m |-> 0 ) by EUCLID:def 4;

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

      then

       A7: ( 0. TRn) = (n |-> 0 ) by EUCLID:def 4;

      reconsider Rr = RR, Rn = RN as non empty Subset of TRn by A1;

      consider hn be Function of (TRn | Rr), (TRn | Rn) such that

       A8: hn is being_homeomorphism and

       A9: (hn .: ( Fr Rr)) = ( Fr Rn) by A1, BROUWER2: 7;

      

       A10: ( dom hn) = ( [#] (TRn | Rr)) by A8, TOPS_2:def 5;

      set Or = ( OpenHypercube (pn,r)), Os = ( OpenHypercube (pm,s)), OO = ( OpenHypercube (( 0. TRnm),1));

      

       A11: ( [#] (TRnm | RNM)) = RNM by PRE_TOPC:def 5;

      

       A12: ( Int Rs) = Os by A2, Th11;

      then

       A13: (hm .: Os) misses (hm .: ( Fr Rs)) by TOPS_1: 39, FUNCT_1: 66, A3;

      

       A14: ( [#] (TRm | Rm)) = Rm by PRE_TOPC:def 5;

      ( 0. TRnm) = ( 0* nm) by EUCLID: 70;

      then

       A15: ( 0. TRnm) = (nm |-> 0 ) by EUCLID:def 4;

      set ON = ( OpenHypercube (( 0. TRn),1)), Om = ( OpenHypercube (( 0. TRm),1));

      reconsider Rnm = RNM as non empty Subset of TRnm;

      

       A16: n in NAT by ORDINAL1:def 12;

      m in NAT by ORDINAL1:def 12;

      then

      consider f be Function of [:TRn, TRm:], TRnm such that

       A17: f is being_homeomorphism and

       A18: for fi be Element of TRn, fj be Element of TRm holds (f . (fi,fj)) = (fi ^ fj) by A16, SIMPLEX2: 19;

      

       A19: ( [#] (TRm | Rs)) = Rs by PRE_TOPC:def 5;

      

       A20: the carrier of [:TRn, TRm:] = [:the carrier of TRn, the carrier of TRm:] by BORSUK_1:def 2;

      

       A21: (f .: [:Rn, Rm:]) c= Rnm

      proof

        let y be object;

        assume

         A22: y in (f .: [:Rn, Rm:]);

        then

        consider x be object such that

         A23: x in ( dom f) and

         A24: x in [:Rn, Rm:] and

         A25: (f . x) = y by FUNCT_1:def 6;

        consider p,q be object such that

         A26: p in the carrier of TRn and

         A27: q in the carrier of TRm and

         A28: x = [p, q] by A20, A23, ZFMISC_1:def 2;

        reconsider q as Point of TRm by A27;

        

         A29: q in Rm by A24, A28, ZFMISC_1: 87;

        reconsider p as Point of TRn by A26;

        

         A30: (f . x) = (f . (p,q)) by A28

        .= (p ^ q) by A18;

        then

        reconsider pq = (p ^ q) as Point of TRnm by A25, A22;

        

         A31: p in Rn by A24, A28, ZFMISC_1: 87;

        for i st i in ( Seg nm) holds (pq . i) in [.((( 0. TRnm) . i) - ((nm |-> 1) . i)), ((( 0. TRnm) . i) + ((nm |-> 1) . i)).]

        proof

          ( len q) = m by CARD_1:def 7;

          then

           A32: ( dom q) = ( Seg m) by FINSEQ_1:def 3;

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

          then

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

          ( len pq) = nm by CARD_1:def 7;

          then

           A34: ( dom pq) = ( Seg nm) by FINSEQ_1:def 3;

          let i such that

           A35: i in ( Seg nm);

          

           A36: ((nm |-> 1) . i) = 1 by A35, FINSEQ_2: 57;

          

           A37: (( 0. TRnm) . i) = 0 by A15;

          per cases by A34, A35, FINSEQ_1: 25;

            suppose

             A38: i in ( dom p);

            then

             A39: (pq . i) = (p . i) by FINSEQ_1:def 7;

            

             A40: (( 0. TRn) . i) = 0 by A7;

            ((n |-> 1) . i) = 1 by A38, A33, FINSEQ_2: 57;

            hence thesis by A40, A39, A38, Def2, A33, A31, A37, A36;

          end;

            suppose ex k be Nat st k in ( dom q) & i = (( len p) + k);

            then

            consider k be Nat such that

             A41: k in ( dom q) and

             A42: i = (( len p) + k);

            

             A43: ((m |-> 1) . k) = 1 by A41, A32, FINSEQ_2: 57;

            

             A44: (( 0. TRm) . k) = 0 by A6;

            (pq . i) = (q . k) by FINSEQ_1:def 7, A41, A42;

            hence thesis by A44, A43, Def2, A32, A29, A41, A37, A36;

          end;

        end;

        hence thesis by Def2, A30, A25;

      end;

      

       A45: ( dom f) = ( [#] [:TRn, TRm:]) by A17, TOPS_2:def 5;

      Rnm c= (f .: [:Rn, Rm:])

      proof

        let x be object;

        assume

         A46: x in Rnm;

        then

        reconsider pq = x as Point of TRnm;

        ( rng pq) c= REAL ;

        then

        reconsider pq as FinSequence of REAL by FINSEQ_1:def 4;

        ( len pq) = nm by CARD_1:def 7;

        then

        consider p,q be FinSequence of REAL such that

         A47: ( len p) = n and

         A48: ( len q) = m and

         A49: pq = (p ^ q) by FINSEQ_2: 23;

        reconsider p as Point of TRn by TOPREAL7: 17, A47;

        reconsider q as Point of TRm by TOPREAL7: 17, A48;

        

         A50: (f . [p, q]) = (f . (p,q))

        .= (p ^ q) by A18;

        

         A51: ( dom p) = ( Seg n) by A47, FINSEQ_1:def 3;

        now

          let i such that

           A52: i in ( Seg n);

          

           A53: (( 0. TRnm) . i) = 0 by A15;

          

           A54: ( Seg n) c= ( Seg nm) by NAT_1: 11, FINSEQ_1: 5;

          then ((nm |-> 1) . i) = 1 by A52, FINSEQ_2: 57;

          then

           A55: (pq . i) in [.( 0 - 1), ( 0 + 1).] by A53, A54, A52, A46, Def2;

          

           A56: (( 0. TRn) . i) = 0 by A7;

          ((n |-> 1) . i) = 1 by A52, FINSEQ_2: 57;

          hence (p . i) in [.((( 0. TRn) . i) - ((n |-> 1) . i)), ((( 0. TRn) . i) + ((n |-> 1) . i)).] by A49, FINSEQ_1:def 7, A51, A52, A56, A55;

        end;

        then

         A57: p in Rn by Def2;

        

         A58: ( dom q) = ( Seg m) by A48, FINSEQ_1:def 3;

        now

          let i such that

           A59: i in ( Seg m);

          

           A60: ((m |-> 1) . i) = 1 by A59, FINSEQ_2: 57;

          

           A61: ((nm |-> 1) . (i + n)) = 1 by A59, FINSEQ_1: 60, FINSEQ_2: 57;

          

           A62: (( 0. TRm) . i) = 0 by A6;

          

           A63: (( 0. TRnm) . (i + n)) = 0 by A15;

          (i + n) in ( Seg nm) by A59, FINSEQ_1: 60;

          then (pq . (i + n)) in [.( 0 - 1), ( 0 + 1).] by A61, A63, A46, Def2;

          hence (q . i) in [.((( 0. TRm) . i) - ((m |-> 1) . i)), ((( 0. TRm) . i) + ((m |-> 1) . i)).] by A47, A49, FINSEQ_1:def 7, A58, A59, A60, A62;

        end;

        then q in Rm by Def2;

        then [p, q] in [:Rn, Rm:] by A57, ZFMISC_1: 87;

        hence thesis by A50, A49, A45, FUNCT_1:def 6;

      end;

      then

       A64: Rnm = (f .: [:Rn, Rm:]) by A21;

      

       A65: ( [#] (TRn | Rr)) = Rr by PRE_TOPC:def 5;

      then

       A66: the carrier of [:(TRn | Rr), (TRm | Rs):] = [:Rr, Rs:] by BORSUK_1:def 2, A19;

      set hnm = [:hn, hm:];

      

       A67: hnm is being_homeomorphism by A8, A3, Th14;

      then

       A68: ( dom hnm) = ( [#] [:(TRn | Rr), (TRm | Rs):]) by TOPS_2:def 5;

      

       A69: ( Int Rn) = ON by Th11;

      then

       A70: ON c= Rn by TOPS_1: 16;

      

       A71: ( [:TRn, TRm:] | [:Rn, Rm:]) = [:(TRn | Rn), (TRm | Rm):] by BORSUK_3: 22;

      then

      reconsider f1 = (f | [:Rn, Rm:]) as Function of [:(TRn | Rn), (TRm | Rm):], (TRnm | Rnm) by A64, JORDAN24: 12;

      reconsider h = (f1 * hnm) as Function of [:(TRn | RR), (TRm | RS):], (TRnm | RNM);

      take h;

      

       A72: f1 is being_homeomorphism by A17, A71, METRIZTS: 2, A64;

      hence h is being_homeomorphism by A67, TOPS_2: 57;

      

       A73: ( [#] (TRn | Rn)) = Rn by PRE_TOPC:def 5;

      ( dom f1) = ( [#] [:(TRn | Rn), (TRm | Rm):]) by A72, TOPS_2:def 5;

      then

       A74: ( dom f1) = [:Rn, Rm:] by BORSUK_1:def 2, A73, A14;

      

       A75: ( Int Rm) = Om by Th11;

      then

       A76: Om c= Rm by TOPS_1: 16;

      

       A77: ( Int Rr) = Or by A1, Th11;

      then

       A78: (hn .: Or) misses (hn .: ( Fr Rr)) by TOPS_1: 39, FUNCT_1: 66, A8;

      thus (h .: [:Or, Os:]) c= OO

      proof

        let y be object;

        assume

         A79: y in (h .: [:Or, Os:]);

        then

        consider x be object such that

         A80: x in ( dom h) and

         A81: x in [:Or, Os:] and

         A82: (h . x) = y by FUNCT_1:def 6;

        consider p,q be object such that

         A83: p in Rr and

         A84: q in Rs and

         A85: [p, q] = x by A80, A66, ZFMISC_1:def 2;

        reconsider p as Point of TRn by A83;

        

         A86: (hn . p) in ( rng hn) by A83, A10, A65, FUNCT_1:def 3;

        reconsider q as Point of TRm by A84;

        

         A87: (hm . q) in ( rng hm) by A84, A5, A19, FUNCT_1:def 3;

        p in Or by A81, A85, ZFMISC_1: 87;

        then (hn . p) in (hn .: Or) by A83, A10, A65, FUNCT_1:def 6;

        then not (hn . p) in ( Fr Rn) by XBOOLE_0: 3, A78, A9;

        then

         A88: (hn . p) in (Rn \ ( Fr Rn)) by A86, A73, XBOOLE_0:def 5;

        then

        reconsider hnp = (hn . p) as Point of TRn;

        

         A89: (h . x) = (f1 . (hnm . x)) by A80, FUNCT_1: 12;

        q in Os by A81, A85, ZFMISC_1: 87;

        then (hm . q) in (hm .: Os) by A84, A5, A19, FUNCT_1:def 6;

        then not (hm . q) in ( Fr Rm) by XBOOLE_0: 3, A13, A4;

        then

         A90: (hm . q) in (Rm \ ( Fr Rm)) by A87, A14, XBOOLE_0:def 5;

        then

        reconsider hmq = (hm . q) as Point of TRm;

        

         A91: (hm . q) in Om by A90, TOPS_1: 40, A75;

        (hnm . x) = (hnm . (p,q)) by A85;

        then

         A92: y = (f1 . [hnp, hmq]) by A82, A89, A83, A84, A10, A65, A5, A19, FUNCT_3:def 8;

        

         A93: (f1 . [hnp, hmq]) = (f . (hnp,hmq)) by A86, A87, A73, A14, ZFMISC_1: 87, FUNCT_1: 49

        .= (hnp ^ hmq) by A18;

        then (hnp ^ hmq) in ( [#] (TRnm | RNM)) by A92, A79;

        then

        reconsider hpq = (hnp ^ hmq) as Point of TRnm by A11;

        

         A94: (hn . p) in ON by A88, TOPS_1: 40, A69;

        for i st i in ( Seg nm) holds (hpq . i) in ].((( 0. TRnm) . i) - 1), ((( 0. TRnm) . i) + 1).[

        proof

          ( len hmq) = m by CARD_1:def 7;

          then

           A95: ( dom hmq) = ( Seg m) by FINSEQ_1:def 3;

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

          then

           A96: ( dom hnp) = ( Seg n) by FINSEQ_1:def 3;

          ( len hpq) = nm by CARD_1:def 7;

          then

           A97: ( dom hpq) = ( Seg nm) by FINSEQ_1:def 3;

          let i such that

           A98: i in ( Seg nm);

          

           A99: (( 0. TRnm) . i) = 0 by A15;

          per cases by A97, A98, FINSEQ_1: 25;

            suppose

             A100: i in ( dom hnp);

            

             A101: (( 0. TRn) . i) = 0 by A7;

            (hnp . i) in ].((( 0. TRn) . i) - 1), ((( 0. TRn) . i) + 1).[ by A100, A94, A96, Th3;

            hence thesis by A101, A100, FINSEQ_1:def 7, A99;

          end;

            suppose ex k be Nat st k in ( dom hmq) & i = (( len hnp) + k);

            then

            consider k be Nat such that

             A102: k in ( dom hmq) and

             A103: i = (( len hnp) + k);

            

             A104: (( 0. TRm) . k) = 0 by A6;

            (hmq . k) in ].((( 0. TRm) . k) - 1), ((( 0. TRm) . k) + 1).[ by A95, A102, Th3, A91;

            hence thesis by A104, FINSEQ_1:def 7, A102, A103, A99;

          end;

        end;

        hence thesis by Th3, A93, A92;

      end;

      let y be object;

      assume

       A105: y in OO;

      then

      reconsider pq = y as Point of TRnm;

      ( rng pq) c= REAL ;

      then

      reconsider pq as FinSequence of REAL by FINSEQ_1:def 4;

      ( len pq) = nm by CARD_1:def 7;

      then

      consider p,q be FinSequence of REAL such that

       A106: ( len p) = n and

       A107: ( len q) = m and

       A108: pq = (p ^ q) by FINSEQ_2: 23;

      reconsider q as Point of TRm by TOPREAL7: 17, A107;

      

       A109: ( dom q) = ( Seg m) by A107, FINSEQ_1:def 3;

       A110:

      now

        let i such that

         A111: i in ( Seg m);

        

         A112: (( 0. TRnm) . (i + n)) = 0 by A15;

        

         A113: (( 0. TRm) . i) = 0 by A6;

        (i + n) in ( Seg nm) by A111, FINSEQ_1: 60;

        then (pq . (i + n)) in ].( 0 - 1), ( 0 + 1).[ by A112, A105, Th3;

        hence (q . i) in ].((( 0. TRm) . i) - 1), ((( 0. TRm) . i) + 1).[ by A106, A108, FINSEQ_1:def 7, A109, A111, A113;

      end;

      then

       A114: q in Om by Th3;

      q in Rm by A76, Th3, A110;

      then q in ( rng hm) by A3, TOPS_2:def 5, A14;

      then

      consider xq be object such that

       A115: xq in ( dom hm) and

       A116: (hm . xq) = q by FUNCT_1:def 3;

      reconsider p as Point of TRn by TOPREAL7: 17, A106;

      

       A117: ( dom p) = ( Seg n) by A106, FINSEQ_1:def 3;

       A118:

      now

        

         A119: ( Seg n) c= ( Seg nm) by NAT_1: 11, FINSEQ_1: 5;

        let i such that

         A120: i in ( Seg n);

        

         A121: (( 0. TRn) . i) = 0 by A7;

        (( 0. TRnm) . i) = 0 by A15;

        then (pq . i) in ].( 0 - 1), ( 0 + 1).[ by A119, A120, A105, Th3;

        hence (p . i) in ].((( 0. TRn) . i) - 1), ((( 0. TRn) . i) + 1).[ by A108, FINSEQ_1:def 7, A117, A120, A121;

      end;

      then

       A122: p in ON by Th3;

      p in Rn by Th3, A118, A70;

      then p in ( rng hn) by A8, TOPS_2:def 5, A73;

      then

      consider xp be object such that

       A123: xp in ( dom hn) and

       A124: (hn . xp) = p by FUNCT_1:def 3;

      reconsider xq as Point of TRm by A115, A5, A19;

      reconsider xp as Point of TRn by A123, A10, A65;

      

       A125: [xp, xq] in [:Rr, Rs:] by A65, A123, A115, A19, ZFMISC_1: 87;

      

       A126: [p, q] = (hnm . (xp,xq)) by FUNCT_3:def 8, A115, A116, A123, A124

      .= (hnm . [xp, xq]);

       [p, q] in [:Rn, Rm:] by A70, A122, A76, A114, ZFMISC_1: 87;

      then

       A127: [xp, xq] in ( dom h) by A125, A68, A66, A126, A74, FUNCT_1: 11;

       not q in ( Fr Rm) by A114, A75, TOPS_1: 39, XBOOLE_0: 3;

      then not xq in ( Fr Rs) by A4, A115, A116, FUNCT_1:def 6;

      then xq in (Rs \ ( Fr Rs)) by A115, A19, XBOOLE_0:def 5;

      then

       A128: xq in Os by A12, TOPS_1: 40;

       not p in ( Fr Rn) by A122, A69, TOPS_1: 39, XBOOLE_0: 3;

      then not xp in ( Fr Rr) by A9, A123, A124, FUNCT_1:def 6;

      then xp in (Rr \ ( Fr Rr)) by A123, A65, XBOOLE_0:def 5;

      then xp in Or by A77, TOPS_1: 40;

      then

       A129: [xp, xq] in [:Or, Os:] by A128, ZFMISC_1: 87;

      (f1 . [p, q]) = (f . (p,q)) by A70, A122, A76, A114, ZFMISC_1: 87, FUNCT_1: 49

      .= (p ^ q) by A18;

      then (h . [xp, xq]) = y by A127, A126, FUNCT_1: 12, A108;

      hence y in (h .: [:Or, Os:]) by A129, A127, FUNCT_1:def 6;

    end;

    theorem :: TIETZE_2:17

    

     Th16: for r, s st r > 0 & s > 0 holds for f be Function of T1, (( TOP-REAL n) | ( ClosedHypercube (pn,(n |-> r)))) holds for g be Function of T2, (( TOP-REAL m) | ( ClosedHypercube (pm,(m |-> s)))) st f is being_homeomorphism & g is being_homeomorphism holds ex h be Function of [:T1, T2:], (( TOP-REAL (n + m)) | ( ClosedHypercube (( 0. ( TOP-REAL (n + m))),((n + m) |-> 1)))) st h is being_homeomorphism & for t1, t2 holds (f . t1) in ( OpenHypercube (pn,r)) & (g . t2) in ( OpenHypercube (pm,s)) iff (h . (t1,t2)) in ( OpenHypercube (( 0. ( TOP-REAL (n + m))),1))

    proof

      set nm = (n + m), TRn = ( TOP-REAL n), TRm = ( TOP-REAL m), TRnm = ( TOP-REAL nm);

      let r, s such that

       A1: r > 0 and

       A2: s > 0 ;

      set Rn = (n |-> r), Rm = (m |-> s), Rnm = (nm |-> 1);

      set RR = ( ClosedHypercube (pn,Rn)), RS = ( ClosedHypercube (pm,Rm)), CL = ( ClosedHypercube (( 0. TRnm),Rnm));

      reconsider Rs = RS as non empty Subset of TRm by A2;

      reconsider Rr = RR as non empty Subset of TRn by A1;

      set Or = ( OpenHypercube (pn,r)), Os = ( OpenHypercube (pm,s)), O = ( OpenHypercube (( 0. TRnm),1));

      consider h be Function of [:(TRn | Rr), (TRm | Rs):], (TRnm | CL) such that

       A3: h is being_homeomorphism and

       A4: (h .: [:Or, Os:]) = O by Th15, A1, A2;

      let f be Function of T1, (TRn | RR);

      let g be Function of T2, (TRm | RS) such that

       A5: f is being_homeomorphism and

       A6: g is being_homeomorphism;

      

       A7: ( dom g) = ( [#] T2) by A6, TOPS_2:def 5;

      reconsider G = g as Function of T2, (TRm | Rs);

      reconsider F = f as Function of T1, (TRn | Rr);

      reconsider fgh = (h * [:F, G:]) as Function of [:T1, T2:], (TRnm | CL);

      take fgh;

       [:F, G:] is being_homeomorphism by A5, A6, Th14;

      hence fgh is being_homeomorphism by A3, TOPS_2: 57;

      then

       A8: ( dom fgh) = ( [#] [:T1, T2:]) by TOPS_2:def 5;

      let t1, t2;

      ( dom f) = ( [#] T1) by A5, TOPS_2:def 5;

      

      then

       A9: [(f . t1), (g . t2)] = ( [:F, G:] . (t1,t2)) by A7, FUNCT_3:def 8

      .= ( [:F, G:] . [t1, t2]);

      

       A10: ( [#] (TRm | Rs)) = Rs by PRE_TOPC:def 5;

      ( [#] (TRn | Rr)) = Rr by PRE_TOPC:def 5;

      then

       A11: ( [#] [:(TRn | Rr), (TRm | Rs):]) = [:Rr, Rs:] by A10, BORSUK_1:def 2;

      

       A12: Os c= Rs by Th12;

      

       A13: Or c= Rr by Th12;

      

       A14: ( dom h) = ( [#] [:(TRn | Rr), (TRm | Rs):]) by A3, TOPS_2:def 5;

      thus (f . t1) in Or & (g . t2) in Os implies (fgh . (t1,t2)) in O

      proof

        assume that

         A15: (f . t1) in Or and

         A16: (g . t2) in Os;

        

         A17: [(f . t1), (g . t2)] in [:Or, Os:] by ZFMISC_1: 87, A15, A16;

         [(f . t1), (g . t2)] in ( dom h) by A15, A13, A16, A12, A11, A14, ZFMISC_1: 87;

        then (h . [(f . t1), (g . t2)]) in O by A17, A4, FUNCT_1:def 6;

        hence thesis by A8, A9, FUNCT_1: 12;

      end;

      assume

       A18: (fgh . (t1,t2)) in O;

      (fgh . (t1,t2)) = (h . [(f . t1), (g . t2)]) by A8, FUNCT_1: 12, A9;

      then

      consider xy be object such that

       A19: xy in ( dom h) and

       A20: xy in [:Or, Os:] and

       A21: (h . xy) = (h . [(f . t1), (g . t2)]) by A18, FUNCT_1:def 6, A4;

       [(f . t1), (g . t2)] in ( dom h) by A8, FUNCT_1: 11, A9;

      then xy = [(f . t1), (g . t2)] by A19, A21, A3, FUNCT_1:def 4;

      hence thesis by A20, ZFMISC_1: 87;

    end;

    registration

      let n;

      cluster non boundary convex compact for Subset of ( TOP-REAL n);

      existence

      proof

        ( ClosedHypercube (( 0. ( TOP-REAL n)),(n |-> 1))) is non boundary convex compact;

        hence thesis;

      end;

    end

    theorem :: TIETZE_2:18

    

     Th17: for A be non boundary convex compact Subset of ( TOP-REAL n), B be non boundary convex compact Subset of ( TOP-REAL m), C be non boundary convex compact Subset of ( TOP-REAL (n + m)) holds for f be Function of T1, (( TOP-REAL n) | A), g be Function of T2, (( TOP-REAL m) | B) st f is being_homeomorphism & g is being_homeomorphism holds ex h be Function of [:T1, T2:], (( TOP-REAL (n + m)) | C) st h is being_homeomorphism & for t1, t2 holds (f . t1) in ( Int A) & (g . t2) in ( Int B) iff (h . (t1,t2)) in ( Int C)

    proof

      set TRn = ( TOP-REAL n), TRm = ( TOP-REAL m), nm = (n + m), TRnm = ( TOP-REAL nm);

      let A be non boundary convex compact Subset of TRn, B be non boundary convex compact Subset of TRm, C be non boundary convex compact Subset of TRnm;

      let f be Function of T1, (TRn | A), g be Function of T2, (TRm | B) such that

       A1: f is being_homeomorphism and

       A2: g is being_homeomorphism;

      set Rn = ( ClosedHypercube (( 0. TRn),(n |-> 1))), Rm = ( ClosedHypercube (( 0. TRm),(m |-> 1))), Rnm = ( ClosedHypercube (( 0. TRnm),(nm |-> 1)));

      consider gm be Function of (TRm | B), (TRm | Rm) such that

       A3: gm is being_homeomorphism and

       A4: (gm .: ( Fr B)) = ( Fr Rm) by BROUWER2: 7;

      

       A5: (gm .: ( Int B)) misses (gm .: ( Fr B)) by A3, TOPS_1: 39, FUNCT_1: 66;

      

       A6: B is non empty;

      then

      reconsider gmg = (gm * g) as Function of T2, (TRm | Rm);

      

       A7: gmg is being_homeomorphism by A2, A3, A6, TOPS_2: 57;

      then

       A8: ( dom gmg) = ( [#] T2) by TOPS_2:def 5;

      reconsider Rn as non empty Subset of TRn;

      consider fn be Function of (TRn | A), (TRn | Rn) such that

       A9: fn is being_homeomorphism and

       A10: (fn .: ( Fr A)) = ( Fr Rn) by BROUWER2: 7;

      

       A11: (fn .: ( Int A)) misses (fn .: ( Fr A)) by A9, TOPS_1: 39, FUNCT_1: 66;

      

       A12: A is non empty;

      then

      reconsider fnf = (fn * f) as Function of T1, (TRn | Rn);

      

       A13: fnf is being_homeomorphism by A1, A9, A12, TOPS_2: 57;

      then

       A14: ( dom fnf) = ( [#] T1) by TOPS_2:def 5;

      

       A15: ( [#] (TRm | Rm)) = Rm by PRE_TOPC:def 5;

      

       A16: ( Int C) = (C \ ( Fr C)) by TOPS_1: 40;

      

       A17: ( [#] (TRnm | C)) = C by PRE_TOPC:def 5;

      

       A18: ( Int Rm) = (Rm \ ( Fr Rm)) by TOPS_1: 40;

      set OHn = ( OpenHypercube (( 0. TRn),1)), OHm = ( OpenHypercube (( 0. TRm),1)), OHnm = ( OpenHypercube (( 0. TRnm),1));

      consider H be Function of (TRnm | Rnm), (TRnm | C) such that

       A19: H is being_homeomorphism and

       A20: (H .: ( Fr Rnm)) = ( Fr C) by BROUWER2: 7;

      

       A21: (H .: ( Int Rnm)) misses (H .: ( Fr Rnm)) by A19, TOPS_1: 39, FUNCT_1: 66;

      

       A22: ( Int Rm) = OHm by Th11;

      consider P be Function of [:T1, T2:], (TRnm | Rnm) such that

       A23: P is being_homeomorphism and

       A24: for t1, t2 holds (fnf . t1) in OHn & (gmg . t2) in OHm iff (P . (t1,t2)) in OHnm by A7, A13, Th16;

      reconsider HP = (H * P) as Function of [:T1, T2:], (TRnm | C);

      take HP;

      C is non empty;

      hence HP is being_homeomorphism by A23, A19, TOPS_2: 57;

      then

       A25: ( dom HP) = ( [#] [:T1, T2:]) by TOPS_2:def 5;

      

       A26: ( [#] (TRn | Rn)) = Rn by PRE_TOPC:def 5;

      

       A27: ( Int Rn) = (Rn \ ( Fr Rn)) by TOPS_1: 40;

      let t1, t2;

      

       A28: (P . [t1, t2]) in ( dom H) by A25, FUNCT_1: 11;

      

       A29: ( Int Rnm) = OHnm by Th11;

      

       A30: (HP . [t1, t2]) in ( rng HP) by A25, FUNCT_1:def 3;

      thus (f . t1) in ( Int A) & (g . t2) in ( Int B) implies (HP . (t1,t2)) in ( Int C)

      proof

        

         A31: (f . t1) in ( dom fn) by A14, FUNCT_1: 11;

        assume that

         A32: (f . t1) in ( Int A) and

         A33: (g . t2) in ( Int B);

        (fnf . t1) = (fn . (f . t1)) by A14, FUNCT_1: 12;

        then (fnf . t1) in (fn .: ( Int A)) by A31, A32, FUNCT_1:def 6;

        then not (fnf . t1) in ( Fr Rn) by A10, A11, XBOOLE_0: 3;

        then (fnf . t1) in (Rn \ ( Fr Rn)) by A26, XBOOLE_0:def 5;

        then

         A34: (fnf . t1) in OHn by Th11, A27;

        

         A35: (g . t2) in ( dom gm) by A8, FUNCT_1: 11;

        

         A36: (P . [t1, t2]) in ( dom H) by A25, FUNCT_1: 11;

        

         A37: (HP . [t1, t2]) = (H . (P . [t1, t2])) by A25, FUNCT_1: 12;

        (gmg . t2) = (gm . (g . t2)) by A8, FUNCT_1: 12;

        then (gmg . t2) in (gm .: ( Int B)) by A35, A33, FUNCT_1:def 6;

        then not (gmg . t2) in ( Fr Rm) by A4, A5, XBOOLE_0: 3;

        then (gmg . t2) in (Rm \ ( Fr Rm)) by A15, XBOOLE_0:def 5;

        then (P . (t1,t2)) in OHnm by A24, A34, A22, A18;

        then (HP . [t1, t2]) in (H .: ( Int Rnm)) by A37, A36, FUNCT_1:def 6, A29;

        then not (HP . [t1, t2]) in ( Fr C) by XBOOLE_0: 3, A21, A20;

        hence thesis by A16, A30, A17, XBOOLE_0:def 5;

      end;

      assume (HP . (t1,t2)) in ( Int C);

      then

       A38: not (HP . [t1, t2]) in (H .: ( Fr Rnm)) by XBOOLE_0:def 5, A16, A20;

      

       A39: ( [#] (TRn | A)) = A by PRE_TOPC:def 5;

      

       A40: ( [#] (TRnm | Rnm)) = Rnm by PRE_TOPC:def 5;

      

       A41: (gmg . t2) = (gm . (g . t2)) by A8, FUNCT_1: 12;

      

       A42: ( Int Rnm) = (Rnm \ ( Fr Rnm)) by TOPS_1: 40;

      

       A43: (f . t1) in ( dom fn) by A14, FUNCT_1: 11;

      

       A44: (HP . [t1, t2]) = (H . (P . [t1, t2])) by A25, FUNCT_1: 12;

      (P . [t1, t2]) in ( Int Rnm)

      proof

        assume not (P . [t1, t2]) in ( Int Rnm);

        then (P . [t1, t2]) in ( Fr Rnm) by A40, A42, XBOOLE_0:def 5;

        hence thesis by A44, A28, FUNCT_1:def 6, A38;

      end;

      then

       A45: (P . (t1,t2)) in OHnm by Th11;

      then (gmg . t2) in (Rm \ ( Fr Rm)) by A24, A22, A18;

      then

       A46: not (gmg . t2) in ( Fr Rm) by XBOOLE_0:def 5;

      ( Int Rn) = OHn by Th11;

      then (fnf . t1) in (Rn \ ( Fr Rn)) by A45, A24, A27;

      then

       A47: not (fnf . t1) in ( Fr Rn) by XBOOLE_0:def 5;

      

       A48: (fnf . t1) = (fn . (f . t1)) by A14, FUNCT_1: 12;

      thus (f . t1) in ( Int A)

      proof

        assume not (f . t1) in ( Int A);

        then not (f . t1) in (A \ ( Fr A)) by TOPS_1: 40;

        then (f . t1) in ( Fr A) by A39, A43, XBOOLE_0:def 5;

        hence thesis by A48, A43, FUNCT_1:def 6, A47, A10;

      end;

      assume not (g . t2) in ( Int B);

      then

       A49: not (g . t2) in (B \ ( Fr B)) by TOPS_1: 40;

      

       A50: (g . t2) in ( dom gm) by A8, FUNCT_1: 11;

      ( [#] (TRm | B)) = B by PRE_TOPC:def 5;

      then (g . t2) in ( Fr B) by A49, A50, XBOOLE_0:def 5;

      hence thesis by A41, A50, FUNCT_1:def 6, A46, A4;

    end;

    

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

    theorem :: TIETZE_2:19

    

     Th18: for pn be Point of ( TOP-REAL n), pm be Point of ( TOP-REAL m) holds for r, s st r > 0 & s > 0 holds ex h be Function of [:( Tdisk (pn,r)), ( Tdisk (pm,s)):], ( Tdisk (( 0. ( TOP-REAL (n + m))),1)) st h is being_homeomorphism & (h .: [:( Ball (pn,r)), ( Ball (pm,s)):]) = ( Ball (( 0. ( TOP-REAL (n + m))),1))

    proof

      

       A1: n in NAT & m in NAT & (n + m) in NAT by ORDINAL1:def 12;

      set TRn = ( TOP-REAL n), TRm = ( TOP-REAL m), nm = (n + m), TRnm = ( TOP-REAL nm);

      let pn be Point of TRn, pm be Point of TRm;

      let r, s such that

       A2: r > 0 and

       A3: s > 0 ;

      reconsider CLn = ( cl_Ball (pn,r)) as non empty Subset of TRn by A2;

      

       A4: ( Int CLn) = (CLn \ ( Fr CLn)) by TOPS_1: 40

      .= (CLn \ ( Sphere (pn,r))) by A2, BROUWER2: 5

      .= (CLn \ (CLn \ ( Ball (pn,r)))) by A1, JORDAN: 19

      .= (CLn /\ ( Ball (pn,r))) by XBOOLE_1: 48

      .= ( Ball (pn,r)) by TOPREAL9: 16, XBOOLE_1: 28;

      reconsider CLm = ( cl_Ball (pm,s)) as non empty Subset of TRm by A3;

      

       A5: ( Int CLm) = (CLm \ ( Fr CLm)) by TOPS_1: 40

      .= (CLm \ ( Sphere (pm,s))) by A3, BROUWER2: 5

      .= (CLm \ (CLm \ ( Ball (pm,s)))) by A1, JORDAN: 19

      .= (CLm /\ ( Ball (pm,s))) by XBOOLE_1: 48

      .= ( Ball (pm,s)) by TOPREAL9: 16, XBOOLE_1: 28;

      reconsider CLnm = ( cl_Ball (( 0. TRnm),1)) as non empty Subset of TRnm;

      

       A6: (TRn | CLn) = ( Tdisk (pn,r)) by BROUWER:def 2;

      

       A7: ( Ball (( 0. TRnm),1)) c= CLnm by TOPREAL9: 16;

      

       A8: ( [#] ( Tdisk (( 0. TRnm),1))) = CLnm by A1, BROUWER: 3;

      

       A9: (TRnm | CLnm) = ( Tdisk (( 0. TRnm),1)) by BROUWER:def 2;

      

       A10: ( Int CLnm) = (CLnm \ ( Fr CLnm)) by TOPS_1: 40

      .= (CLnm \ ( Sphere (( 0. TRnm),1))) by BROUWER2: 5

      .= (CLnm \ (CLnm \ ( Ball (( 0. TRnm),1)))) by A1, JORDAN: 19

      .= (CLnm /\ ( Ball (( 0. TRnm),1))) by XBOOLE_1: 48

      .= ( Ball (( 0. TRnm),1)) by TOPREAL9: 16, XBOOLE_1: 28;

      set Rn = ( ClosedHypercube (( 0. TRn),(n |-> 1))), Rm = ( ClosedHypercube (( 0. TRm),(m |-> 1))), Rnm = ( ClosedHypercube (( 0. TRnm),(nm |-> 1)));

      

       A11: ( [#] (TRm | Rm)) = Rm by PRE_TOPC:def 5;

      

       A12: ( Ball (pn,r)) c= CLn by TOPREAL9: 16;

      CLn is non boundary convex compact Subset of TRn by A2, Lm1;

      then

      consider fn be Function of (TRn | CLn), (TRn | Rn) such that

       A13: fn is being_homeomorphism and

       A14: (fn .: ( Fr CLn)) = ( Fr Rn) by BROUWER2: 7;

      

       A15: (fn .: ( Int CLn)) misses (fn .: ( Fr CLn)) by TOPS_1: 39, A13, FUNCT_1: 66;

      ( [#] (TRn | Rn)) = Rn by PRE_TOPC:def 5;

      then

       A16: ( rng fn) = Rn by A13, TOPS_2:def 5;

      CLm is non boundary convex compact by A3, Lm1;

      then

      consider gm be Function of (TRm | CLm), (TRm | Rm) such that

       A17: gm is being_homeomorphism and

       A18: (gm .: ( Fr CLm)) = ( Fr Rm) by BROUWER2: 7;

      

       A19: (TRm | CLm) = ( Tdisk (pm,s)) by BROUWER:def 2;

      ( [#] (TRm | Rm)) = Rm by PRE_TOPC:def 5;

      then

       A20: ( rng gm) = Rm by A17, TOPS_2:def 5;

      

       A21: ( Ball (pm,s)) c= CLm by TOPREAL9: 16;

      

       A22: ( [#] ( Tdisk (pn,r))) = CLn by A1, BROUWER: 3;

      then

       A23: ( dom fn) = CLn by A6, A13, TOPS_2:def 5;

      CLnm is non boundary convex compact by Lm1;

      then

      consider P be Function of [:( Tdisk (pn,r)), ( Tdisk (pm,s)):], ( Tdisk (( 0. TRnm),1)) such that

       A24: P is being_homeomorphism and

       A25: for t1 be Point of (TRn | CLn), t2 be Point of (TRm | CLm) holds (fn . t1) in ( Int Rn) & (gm . t2) in ( Int Rm) iff (P . (t1,t2)) in ( Int CLnm) by A6, A19, A9, Th17, A13, A17;

      take P;

      thus P is being_homeomorphism by A24;

      

       A26: (gm .: ( Int CLm)) misses (gm .: ( Fr CLm)) by TOPS_1: 39, A17, FUNCT_1: 66;

      

       A27: ( [#] ( Tdisk (pm,s))) = CLm by A1, BROUWER: 3;

      then

       A28: ( dom gm) = CLm by A19, A17, TOPS_2:def 5;

      

       A29: ( dom gm) = CLm by A19, A17, A27, TOPS_2:def 5;

      thus (P .: [:( Ball (pn,r)), ( Ball (pm,s)):]) c= ( Ball (( 0. TRnm),1))

      proof

        let y be object;

        assume y in (P .: [:( Ball (pn,r)), ( Ball (pm,s)):]);

        then

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

         A30: x in [:( Ball (pn,r)), ( Ball (pm,s)):] and

         A31: (P . x) = y by FUNCT_1:def 6;

        consider y1,y2 be object such that

         A32: y1 in ( Ball (pn,r)) and

         A33: y2 in ( Ball (pm,s)) and

         A34: x = [y1, y2] by A30, ZFMISC_1:def 2;

        reconsider y1 as Point of (TRn | CLn) by A32, A12, A1, BROUWER: 3, A6;

        (fn . y1) in (fn .: ( Int CLn)) by A32, A4, A12, A23, FUNCT_1:def 6;

        then

         A35: not (fn . y1) in ( Fr Rn) by A15, XBOOLE_0: 3, A14;

        reconsider y2 as Point of (TRm | CLm) by A33, A21, A1, BROUWER: 3, A19;

        (gm . y2) in (gm .: ( Int CLm)) by A33, A5, A21, A29, FUNCT_1:def 6;

        then not (gm . y2) in ( Fr Rm) by XBOOLE_0: 3, A26, A18;

        then (gm . y2) in (Rm \ ( Fr Rm)) by A11, XBOOLE_0:def 5;

        then

         A36: (gm . y2) in ( Int Rm) by TOPS_1: 40;

        (fn . y1) in Rn by A32, A12, A23, FUNCT_1:def 3, A16;

        then (fn . y1) in (Rn \ ( Fr Rn)) by A35, XBOOLE_0:def 5;

        then (fn . y1) in ( Int Rn) by TOPS_1: 40;

        then (P . (y1,y2)) in ( Int CLnm) by A25, A36;

        hence thesis by A31, A34, A10;

      end;

      let y be object;

      assume

       A37: y in ( Ball (( 0. TRnm),1));

      ( rng P) = ( [#] ( Tdisk (( 0. TRnm),1))) by TOPS_2:def 5, A24;

      then

      consider x be object such that

       A38: x in ( dom P) and

       A39: (P . x) = y by A37, A7, A8, FUNCT_1:def 3;

      ( [#] [:( Tdisk (pn,r)), ( Tdisk (pm,s)):]) = [:( [#] ( Tdisk (pn,r))), ( [#] ( Tdisk (pm,s))):] by BORSUK_1:def 2;

      then

      consider y1,y2 be object such that

       A40: y1 in CLn and

       A41: y2 in CLm and

       A42: x = [y1, y2] by A38, A22, A27, ZFMISC_1:def 2;

      reconsider y2 as Point of (TRm | CLm) by A19, A1, BROUWER: 3, A41;

      reconsider y1 as Point of (TRn | CLn) by A6, A40, A1, BROUWER: 3;

      

       A43: (P . x) = (P . (y1,y2)) by A42;

      then (fn . y1) in ( Int Rn) by A25, A39, A37, A10;

      then (fn . y1) in (Rn \ (fn .: ( Fr CLn))) by TOPS_1: 40, A14;

      then (fn . y1) in ((fn .: CLn) \ (fn .: ( Fr CLn))) by RELAT_1: 113, A23, A16;

      then (fn . y1) in (fn .: (CLn \ ( Fr CLn))) by A13, FUNCT_1: 64;

      then (fn . y1) in (fn .: ( Int CLn)) by TOPS_1: 40;

      then ex z1 be object st z1 in ( dom fn) & z1 in ( Int CLn) & (fn . z1) = (fn . y1) by FUNCT_1:def 6;

      then

       A44: y1 in ( Int CLn) by A23, A40, A13, FUNCT_1:def 4;

      (gm . y2) in ( Int Rm) by A43, A25, A39, A37, A10;

      then (gm . y2) in (Rm \ (gm .: ( Fr CLm))) by TOPS_1: 40, A18;

      then (gm . y2) in ((gm .: CLm) \ (gm .: ( Fr CLm))) by RELAT_1: 113, A28, A20;

      then (gm . y2) in (gm .: (CLm \ ( Fr CLm))) by A17, FUNCT_1: 64;

      then (gm . y2) in (gm .: ( Int CLm)) by TOPS_1: 40;

      then ex z2 be object st z2 in ( dom gm) & z2 in ( Int CLm) & (gm . z2) = (gm . y2) by FUNCT_1:def 6;

      then y2 in ( Int CLm) by A28, A41, A17, FUNCT_1:def 4;

      then [y1, y2] in [:( Ball (pn,r)), ( Ball (pm,s)):] by A44, A5, A4, ZFMISC_1: 87;

      hence thesis by A38, A39, A42, FUNCT_1:def 6;

    end;

    theorem :: TIETZE_2:20

    r > 0 & s > 0 & (T1,(( TOP-REAL n) | ( Ball (pn,r)))) are_homeomorphic & (T2,(( TOP-REAL m) | ( Ball (pm,s)))) are_homeomorphic implies ( [:T1, T2:],(( TOP-REAL (n + m)) | ( Ball (( 0. ( TOP-REAL (n + m))),1)))) are_homeomorphic

    proof

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

      set TRn = ( TOP-REAL N), TRm = ( TOP-REAL M), NM = (N + M), TRnm = ( TOP-REAL NM);

      reconsider Pn = pn as Point of TRn;

      reconsider Pm = pm as Point of TRm;

      assume that

       A1: r > 0 and

       A2: s > 0 ;

      reconsider Bm = ( Ball (Pm,s)) as non empty Subset of TRm by A2;

      

       A3: ( [#] ( Tdisk (Pm,s))) = ( cl_Ball (Pm,s)) by BROUWER: 3;

      then

      reconsider BBm = ( Ball (Pm,s)) as Subset of ( Tdisk (Pm,s)) by TOPREAL9: 16;

      

       A4: ( Tdisk (Pm,s)) = (TRm | ( cl_Ball (Pm,s))) by BROUWER:def 2;

      then

       A5: (( Tdisk (Pm,s)) | BBm) = (TRm | ( Ball (Pm,s))) by A3, PRE_TOPC: 7;

      reconsider Bn = ( Ball (Pn,r)) as non empty Subset of TRn by A1;

      reconsider Bnm = ( Ball (( 0. TRnm),1)) as non empty Subset of TRnm;

      

       A6: ( [#] ( Tdisk (Pn,r))) = ( cl_Ball (pn,r)) by BROUWER: 3;

      then

      reconsider BBn = ( Ball (Pn,r)) as Subset of ( Tdisk (Pn,r)) by TOPREAL9: 16;

      

       A7: ( [#] ( Tdisk (( 0. TRnm),1))) = ( cl_Ball (( 0. TRnm),1)) by BROUWER: 3;

      then

      reconsider BBnm = ( Ball (( 0. TRnm),1)) as Subset of ( Tdisk (( 0. TRnm),1)) by TOPREAL9: 16;

      

       A8: ( Tdisk (( 0. TRnm),1)) = (TRnm | ( cl_Ball (( 0. TRnm),1))) by BROUWER:def 2;

      then

       A9: (( Tdisk (( 0. TRnm),1)) | BBnm) = (TRnm | ( Ball (( 0. TRnm),1))) by A7, PRE_TOPC: 7;

      assume (T1,(( TOP-REAL n) | ( Ball (pn,r)))) are_homeomorphic ;

      then

      consider f1 be Function of T1, (TRn | Bn) such that

       A10: f1 is being_homeomorphism by T_0TOPSP:def 1;

      assume (T2,(( TOP-REAL m) | ( Ball (pm,s)))) are_homeomorphic ;

      then

      consider f2 be Function of T2, (TRm | Bm) such that

       A11: f2 is being_homeomorphism by T_0TOPSP:def 1;

      

       A12: [:f1, f2:] is being_homeomorphism by A10, A11, Th14;

      consider h be Function of [:( Tdisk (Pn,r)), ( Tdisk (Pm,s)):], ( Tdisk (( 0. TRnm),1)) such that

       A13: h is being_homeomorphism and

       A14: (h .: [:( Ball (Pn,r)), ( Ball (Pm,s)):]) = ( Ball (( 0. TRnm),1)) by A1, A2, Th18;

      

       A15: ( Tdisk (Pn,r)) = (TRn | ( cl_Ball (Pn,r))) by BROUWER:def 2;

      then (( Tdisk (Pn,r)) | BBn) = (TRn | ( Ball (Pn,r))) by A6, PRE_TOPC: 7;

      then

       A16: ( [:( Tdisk (Pn,r)), ( Tdisk (Pm,s)):] | [:BBn, BBm:]) = [:(TRn | Bn), (TRm | Bm):] by A5, BORSUK_3: 22;

      then

      reconsider h1 = (h | [:BBn, BBm:]) as Function of [:(TRn | Bn), (TRm | Bm):], (TRnm | Bnm) by JORDAN24: 12, A9, A14, A1, A15, A2, A4, A8;

      reconsider hf = (h1 * [:f1, f2:]) as Function of [:T1, T2:], (TRnm | Bnm);

      h1 is being_homeomorphism by A9, A16, A13, A14, METRIZTS: 2;

      then hf is being_homeomorphism by A12, TOPS_2: 57;

      hence thesis by T_0TOPSP:def 1;

    end;

    begin

    reserve T,S for TopSpace,

A for closed Subset of T,

B for Subset of S;

    

     Lm2: 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 A2, A3, XBOOLE_1: 1, A4;

      end;

        suppose

         A5: n = 0 ;

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

        

         A6: ( OpenHypercube (e,1)) = {Z} by EUCLID_9: 12, A5;

        

         A7: the carrier of TR = ( REAL 0 ) by EUCLID: 22;

        the carrier of ( Euclid 0 ) = the carrier of TR by EUCLID: 67;

        then ( Ball (e,r)) = {} or ( Ball (e,r)) = {Z} by A7, EUCLID: 77, ZFMISC_1: 33, A5;

        hence thesis by A6, A2, A3;

      end;

    end;

    theorem :: TIETZE_2:21

    

     Th21: for n be non zero Nat holds for F be Element of (n -tuples_on ( Funcs (the carrier of T,the carrier of R^1 ))) st for i st i in ( dom F) holds for h be Function of T, R^1 st h = (F . i) holds h is continuous holds <:F:> is continuous

    proof

      let n be non zero Nat;

      let F be Element of (n -tuples_on ( Funcs (the carrier of T,the carrier of R^1 ))) such that

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

      set TR = ( TOP-REAL n), FF = <:F:>;

      

       A2: for Y be Subset of TR st Y is open holds (FF " Y) is open

      proof

        let Y be Subset of TR;

        set E = ( Euclid n);

        

         A3: the TopStruct of TR = ( TopSpaceMetr E) by EUCLID:def 8;

        then

        reconsider YY = Y as Subset of ( TopSpaceMetr E);

        assume Y is open;

        then Y in the topology of TR;

        then

        reconsider YY as open Subset of ( TopSpaceMetr E) by PRE_TOPC:def 2, A3;

        

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

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

        proof

          let x be set;

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

          then

           A5: ( dom F) = ( Seg n) by FINSEQ_1:def 3;

          hereby

            assume

             A6: x in (FF " Y);

            then

             A7: (FF . x) in Y by FUNCT_1:def 7;

            then

            reconsider FFx = (FF . x) as Point of E by EUCLID: 67;

            consider m be Real such that

             A8: m > 0 and

             A9: ( OpenHypercube (FFx,m)) c= YY by A7, Lm2;

            defpred P[ Nat, object] means ex h be Function of T, R^1 st h = (F . $1) & $2 = (h " ].((FFx . $1) - m), ((FFx . $1) + m).[);

            

             A10: for k be Nat st k in ( Seg n) holds ex x be object st P[k, x]

            proof

              let k be Nat such that

               A11: k in ( Seg n);

              (F . k) in ( rng F) by A5, A11, FUNCT_1:def 3;

              then

              consider h be Function such that

               A12: (F . k) = h and

               A13: ( dom h) = the carrier of T and

               A14: ( rng h) c= the carrier of R^1 by FUNCT_2:def 2;

              reconsider h as Function of T, R^1 by A13, A14, FUNCT_2: 2;

              take (h " ].((FFx . k) - m), ((FFx . k) + m).[);

              thus thesis by A12;

            end;

            consider p be FinSequence such that

             A15: ( dom p) = ( Seg n) & for k be Nat st k in ( Seg n) holds P[k, (p . k)] from FINSEQ_1:sch 1( A10);

            

             A16: for Y be set holds Y in ( rng p) implies x in Y

            proof

              let Y be set;

              assume Y in ( rng p);

              then

              consider k be object such that

               A17: k in ( dom p) and

               A18: (p . k) = Y by FUNCT_1:def 3;

              reconsider k as Nat by A17;

              consider h be Function of T, R^1 such that

               A19: h = (F . k) and

               A20: (p . k) = (h " ].((FFx . k) - m), ((FFx . k) + m).[) by A17, A15;

              

               A21: ( dom h) = the carrier of T by FUNCT_2:def 1;

              

               A22: (FFx . k) > ((FFx . k) - m) by A8, XREAL_1: 44;

              ((FFx . k) + m) > (FFx . k) by A8, XREAL_1: 39;

              then

               A23: (FFx . k) in ].((FFx . k) - m), ((FFx . k) + m).[ by A22, XXREAL_1: 4;

              (h . x) = (FFx . k) by A19, Th20;

              hence thesis by A21, A6, A23, A20, A18, FUNCT_1:def 7;

            end;

            ( rng p) c= ( bool the carrier of T)

            proof

              let y be object;

              assume y in ( rng p);

              then

              consider k be object such that

               A24: k in ( dom p) and

               A25: (p . k) = y by FUNCT_1:def 3;

              reconsider k as Nat by A24;

              ex h be Function of T, R^1 st h = (F . k) & (p . k) = (h " ].((FFx . k) - m), ((FFx . k) + m).[) by A24, A15;

              hence thesis by A25;

            end;

            then

            reconsider R = ( rng p) as finite Subset-Family of T;

            take M = ( meet R);

            now

              let A be Subset of T;

              

               A26: ( [#] R^1 ) = REAL by TOPMETR: 17;

              assume A in R;

              then

              consider k be object such that

               A27: k in ( dom p) and

               A28: (p . k) = A by FUNCT_1:def 3;

              reconsider k as Nat by A27;

              consider h be Function of T, R^1 such that

               A29: h = (F . k) and

               A30: (p . k) = (h " ].((FFx . k) - m), ((FFx . k) + m).[) by A27, A15;

              reconsider P = ].((FFx . k) - m), ((FFx . k) + m).[ as Subset of R^1 by TOPMETR: 17;

              

               A31: P is open by JORDAN6: 35;

              h is continuous by A1, A5, A27, A29, A15;

              hence A is open by A31, A26, TOPS_2: 43, A28, A30;

            end;

            hence M is open by TOPS_2:def 1, TOPS_2: 20;

            thus M c= (FF " Y)

            proof

              let q be object;

              set I = ( Intervals (FFx,m));

              

               A32: ( dom I) = ( dom FFx) by EUCLID_9:def 3;

              assume

               A33: q in M;

              then

              reconsider q as Point of T;

              (FF . q) in ( rng FF) by A4, A33, FUNCT_1:def 3;

              then

              reconsider FFq = (FF . q) as Point of TR;

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

              then

               A34: ( dom FFx) = ( Seg n) by FINSEQ_1:def 3;

              

               A35: for y be object st y in ( dom I) holds (FFq . y) in (I . y)

              proof

                let y be object;

                assume

                 A36: y in ( dom I);

                then

                reconsider i = y as Nat;

                consider h be Function of T, R^1 such that

                 A37: h = (F . i) and

                 A38: (p . i) = (h " ].((FFx . i) - m), ((FFx . i) + m).[) by A36, A15, A34, A32;

                

                 A39: (h . q) = (FFq . i) by A37, Th20;

                (p . i) in ( rng p) by A36, A34, A32, A15, FUNCT_1:def 3;

                then ( meet ( rng p)) c= (p . i) by SETFAM_1: 3;

                then (h . q) in ].((FFx . i) - m), ((FFx . i) + m).[ by A38, A33, FUNCT_1:def 7;

                hence thesis by A39, A32, A36, EUCLID_9:def 3;

              end;

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

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

              then FFq in ( product I) by A35, CARD_3:def 5, A32, A34;

              then FFq in ( OpenHypercube (FFx,m)) by EUCLID_9:def 4;

              hence thesis by A9, A4, A33, FUNCT_1:def 7;

            end;

            ( rng p) <> {} by A15, RELAT_1: 42;

            hence x in M by A16, SETFAM_1:def 1;

          end;

          thus thesis;

        end;

        hence thesis by TOPS_1: 25;

      end;

      ( [#] TR) <> {} ;

      hence thesis by A2, TOPS_2: 43;

    end;

    theorem :: TIETZE_2:22

    

     Th22: for T, A st T is normal holds for f be Function of (T | A), (( TOP-REAL n) | ( ClosedHypercube (( 0. ( TOP-REAL n)),(n |-> 1)))) st f is continuous holds ex g be Function of T, (( TOP-REAL n) | ( ClosedHypercube (( 0. ( TOP-REAL n)),(n |-> 1)))) st g is continuous & (g | A) = f

    proof

      let T, A such that

       A1: T is normal;

      set TR = ( TOP-REAL n);

      set N = ( 0. ( TOP-REAL n));

      set H = ( ClosedHypercube (N,(n |-> 1)));

      let f be Function of (T | A), (TR | H) such that

       A2: f is continuous;

      

       A3: ( [#] (TR | H)) = H by PRE_TOPC:def 5;

      

       A4: ( [#] (T | A)) = A by PRE_TOPC:def 5;

      per cases ;

        suppose

         A5: A is empty;

        reconsider TRH = (TR | H) as non empty TopSpace;

        set g = the continuous Function of T, TRH;

        

         A6: (g | A) = {} by A5;

        f = {} by A5;

        hence thesis by A6;

      end;

        suppose

         A7: A is non empty;

        set CC = ( Closed-Interval-TSpace (( - 1),1));

        per cases ;

          suppose

           A8: n = 0 ;

          reconsider TRH = (TR | H) as non empty TopSpace;

          

           A9: {( 0. ( TOP-REAL n))} = the carrier of TR by EUCLID: 22, A8, JORDAN2C: 105;

          then

          reconsider Z = ( 0. ( TOP-REAL n)) as Point of TRH by A3, ZFMISC_1: 33;

          H = the carrier of TR by A9, ZFMISC_1: 33;

          then

           A10: ( rng f) = the carrier of TR by A4, A7, A3, A9, ZFMISC_1: 33;

          reconsider g = (T --> Z) as Function of T, (TR | H);

          take g;

          

           A11: (the carrier of T /\ A) = A by XBOOLE_1: 28;

          ( dom f) = A by FUNCT_2:def 1, A4;

          then f = (A --> ( 0. ( TOP-REAL n))) by A10, FUNCOP_1: 9, EUCLID: 22, A8, JORDAN2C: 105;

          hence thesis by A11, FUNCOP_1: 12;

        end;

          suppose n <> 0 ;

          then

          reconsider nn = n as non zero Element of NAT by ORDINAL1:def 12;

          set CC = ( Closed-Interval-TSpace (( - 1),1));

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

          defpred F[ Nat, object] means ex g be continuous Function of T, R^1 st $2 = g & ( rng g) c= ( [#] CC) & (g | A) = (( PROJ (n,$1)) * F);

          

           A12: ( dom f) = A by A4, FUNCT_2:def 1;

          N = ( 0* n) by EUCLID: 70;

          then

           A13: N = (n |-> 0 ) by EUCLID:def 4;

          

           A14: for k be Nat st k in ( Seg n) holds ex x be object st F[k, x]

          proof

            

             A15: the carrier of CC = [.( - 1), 1.] by TOPMETR: 18;

            

             A16: T is non empty by A7;

            let k be Nat such that

             A17: k in ( Seg n);

            ( rng f) c= H by A3;

            then (( PROJ (n,k)) .: ( rng F)) c= (( PROJ (n,k)) .: H) by RELAT_1: 123;

            then

             A18: (( PROJ (n,k)) .: ( rng F)) c= [.((N . k) - ((n |-> 1) . k)), ((N . k) + ((n |-> 1) . k)).] by A17, Th7;

            

             A19: ( dom (( PROJ (n,k)) * F)) = the carrier of (T | A) by FUNCT_2:def 1;

            

             A20: (N . k) = 0 by A13;

            ((n |-> 1) . k) = 1 by A17, FINSEQ_2: 57;

            then ( rng (( PROJ (n,k)) * F)) c= [.( - 1), 1.] by A20, A18, RELAT_1: 127;

            then

            reconsider PF = (( PROJ (n,k)) * F) as Function of (T | A), CC by A19, A15, FUNCT_2: 2;

            

             A21: F is continuous by A2, PRE_TOPC: 26;

            ( PROJ (n,k)) is continuous by TOPREALC: 57, A17;

            then

            consider g be continuous Function of T, CC such that

             A22: (g | A) = PF by A21, A16, A7, PRE_TOPC: 27, A1, TIETZE: 23;

            

             A23: ( rng g) c= REAL ;

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

            then

            reconsider G = g as Function of T, R^1 by A23, TOPMETR: 17, FUNCT_2: 2;

            

             A24: G is continuous by PRE_TOPC: 26;

            ( rng g) c= the carrier of CC by RELAT_1:def 19;

            hence thesis by A24, A22;

          end;

          consider pp be FinSequence such that

           A25: ( dom pp) = ( Seg n) and

           A26: for k be Nat st k in ( Seg n) holds F[k, (pp . k)] from FINSEQ_1:sch 1( A14);

          

           A27: ( len pp) = nn by A25, FINSEQ_1:def 3;

          ( rng pp) c= ( Funcs (the carrier of T,the carrier of R^1 ))

          proof

            let y be object;

            assume y in ( rng pp);

            then

            consider k be object such that

             A28: k in ( dom pp) and

             A29: (pp . k) = y by FUNCT_1:def 3;

            reconsider k as Nat by A28;

            consider g be continuous Function of T, R^1 such that

             A30: (pp . k) = g and ( rng g) c= ( [#] CC) and (g | A) = (( PROJ (n,k)) * F) by A25, A26, A28;

            

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

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

            hence thesis by A31, FUNCT_2:def 2, A29, A30;

          end;

          then pp is FinSequence of ( Funcs (the carrier of T,the carrier of R^1 )) by FINSEQ_1:def 4;

          then

          reconsider pp as Element of (nn -tuples_on ( Funcs (the carrier of T,the carrier of R^1 ))) by A27, FINSEQ_2: 92;

          

           A32: ( dom <:pp:>) = the carrier of T by FUNCT_2:def 1;

          

           A33: the carrier of CC = [.( - 1), 1.] by TOPMETR: 18;

          ( rng <:pp:>) c= H

          proof

            let y be object;

            assume

             A34: y in ( rng <:pp:>);

            then

            consider x be object such that

             A35: x in ( dom <:pp:>) and

             A36: ( <:pp:> . x) = y by FUNCT_1:def 3;

            reconsider p = ( <:pp:> . x) as Point of TR by A34, A36;

            now

              let j be Nat;

              

               A37: (N . j) = 0 by A13;

              assume

               A38: j in ( Seg n);

              then

              consider g be continuous Function of T, R^1 such that

               A39: g = (pp . j) and

               A40: ( rng g) c= ( [#] CC) and (g | A) = (( PROJ (n,j)) * F) by A26;

              

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

              (g . x) = (p . j) by Th20, A39;

              then

               A42: (p . j) in ( rng g) by A41, A35, FUNCT_1:def 3;

              ((n |-> 1) . j) = 1 by A38, FINSEQ_2: 57;

              hence (p . j) in [.((N . j) - ((n |-> 1) . j)), ((N . j) + ((n |-> 1) . j)).] by A37, A42, A40, A33;

            end;

            hence thesis by Def2, A36;

          end;

          then

          reconsider G = <:pp:> as Function of T, (TR | H) by A3, A32, FUNCT_2: 2;

          take G;

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

          proof

            let k be Nat such that

             A43: k in ( dom pp);

            ex g be continuous Function of T, R^1 st (pp . k) = g & ( rng g) c= ( [#] CC) & (g | A) = (( PROJ (n,k)) * F) by A25, A26, A43;

            hence thesis;

          end;

          hence G is continuous by Th21, PRE_TOPC: 27;

          

           A44: ( dom (G | A)) = A by A32, RELAT_1: 62;

          for e be set st e in ( dom f) holds ((G | A) . e) = (f . e)

          proof

            let e be set;

            

             A45: ( rng F) c= the carrier of TR;

            assume

             A46: e in ( dom f);

            then (G . e) in ( rng G) by A32, A12, FUNCT_1:def 3;

            then

             A47: (G . e) in H by A3;

            (f . e) in ( rng f) by A46, FUNCT_1:def 3;

            then

            reconsider Ge = (G . e), fe = (f . e) as Point of TR by A45, A47;

            

             A48: ( len fe) = n by CARD_1:def 7;

             A49:

            now

              

               A50: ( dom fe) = ( Seg n) by A48, FINSEQ_1:def 3;

              let w be Nat;

              assume that

               A51: 1 <= w and

               A52: w <= n;

              consider g be continuous Function of T, R^1 such that

               A53: g = (pp . w) and ( rng g) c= ( [#] CC) and

               A54: (g | A) = (( PROJ (n,w)) * F) by A51, A52, FINSEQ_1: 1, A26;

              

               A55: (Ge . w) = (g . e) by Th20, A53;

              

               A56: e in ( dom (g | A)) by A46, A12, FUNCT_2:def 1;

              ((g | A) . e) = (g . e) by A46, A4, FUNCT_1: 49;

              then (Ge . w) = (( PROJ (n,w)) . fe) by A55, A56, A54, FUNCT_1: 12;

              

              hence (Ge . w) = (fe /. w) by TOPREALC:def 6

              .= (fe . w) by PARTFUN1:def 6, A51, A52, FINSEQ_1: 1, A50;

            end;

            

             A57: ( len Ge) = n by CARD_1:def 7;

            ((G | A) . e) = (G . e) by A46, A44, A4, FUNCT_1: 47;

            hence thesis by A49, FINSEQ_1: 14, A57, A48;

          end;

          hence thesis by A44, A12;

        end;

      end;

    end;

    theorem :: TIETZE_2:23

    

     Th23: for T, A st T is normal holds for X be Subset of ( TOP-REAL n) st X is compact non boundary convex holds for f be Function of (T | A), (( TOP-REAL n) | X) st f is continuous holds ex g be Function of T, (( TOP-REAL n) | X) st g is continuous & (g | A) = f

    proof

      set TR = ( TOP-REAL n);

      let T, A such that

       A1: T is normal;

      let S be Subset of TR such that

       A2: S is compact non boundary convex;

      let f be Function of (T | A), (TR | S) such that

       A3: f is continuous;

      

       A4: ( [#] (T | A)) = A by PRE_TOPC:def 5;

      

       A5: ( [#] (TR | S)) = S by PRE_TOPC:def 5;

      per cases ;

        suppose

         A6: A is empty;

        reconsider TRS = (TR | S) as non empty TopSpace by A2, A5;

        set g = the continuous Function of T, TRS;

        

         A7: (g | A) = {} by A6;

        f = {} by A6;

        hence thesis by A7;

      end;

        suppose

         A8: A is non empty;

        set H = ( ClosedHypercube (( 0. ( TOP-REAL n)),(n |-> 1)));

        consider h be Function of (TR | S), (TR | H) such that

         A9: h is being_homeomorphism and (h .: ( Fr S)) = ( Fr H) by BROUWER2: 7, A2;

        

         A10: ( rng h) = ( [#] (TR | H)) by A9, TOPS_2:def 5;

        

         A11: (TR | S) is non empty by A5, A2;

        then

        reconsider hf = (h * f) as Function of (T | A), (TR | H);

        consider g be Function of T, (TR | H) such that

         A12: g is continuous and

         A13: (g | A) = hf by A3, A9, A4, A8, A11, A1, Th22;

        reconsider hg = ((h " ) * g) as Function of T, (TR | S);

        take hg;

        (h " ) is being_homeomorphism by A9, TOPS_2: 56;

        hence hg is continuous by A12, TOPS_2: 46;

        

         A14: ( rng f) c= the carrier of (TR | S);

        

         A15: ( dom h) = ( [#] (TR | S)) by A9, TOPS_2:def 5;

        

        thus (hg | A) = ((h " ) * hf) by RELAT_1: 83, A13

        .= (((h " ) * h) * f) by RELAT_1: 36

        .= (( id ( [#] (TR | S))) * f) by A9, A10, A15, TOPS_2: 52

        .= f by A14, RELAT_1: 53;

      end;

    end;

    ::$Notion-Name

    ::$Notion-Name

    theorem :: TIETZE_2:24

    for T, S, A, B st T is normal holds for X be Subset of ( TOP-REAL n) st X is compact non boundary convex & (B,X) are_homeomorphic holds for f be Function of (T | A), (S | B) st f is continuous holds ex g be Function of T, (S | B) st g is continuous & (g | A) = f

    proof

      let T, S, A, B such that

       A1: T is normal;

      

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

      

       A3: ( [#] (S | B)) = B by PRE_TOPC:def 5;

      set TR = ( TOP-REAL n);

      let X be Subset of TR such that

       A4: X is compact non boundary convex and

       A5: (B,X) are_homeomorphic ;

      consider h be Function of (S | B), (TR | X) such that

       A6: h is being_homeomorphism by METRIZTS:def 1, A5, T_0TOPSP:def 1;

      

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

      let f be Function of (T | A), (S | B) such that

       A8: f is continuous;

      

       A9: ( rng f) c= the carrier of (S | B);

      

       A10: ( dom h) = ( [#] (S | B)) by TOPS_2:def 5, A6;

      

       A11: X is non empty by A4;

      

       A12: ( rng h) = ( [#] (TR | X)) by TOPS_2:def 5, A6;

      then

       A13: B is non empty by A11;

      per cases ;

        suppose

         A14: A is empty;

        reconsider SB = (S | B) as non empty TopSpace by A11, A12;

        set h = the continuous Function of T, SB;

        reconsider h as Function of T, (S | B);

        take h;

        f = {} by A14;

        hence thesis by A14;

      end;

        suppose

         A15: A is non empty;

        reconsider hf = (h * f) as Function of (T | A), (TR | X) by A3, A13;

        consider g be Function of T, (TR | X) such that

         A16: g is continuous and

         A17: (g | A) = hf by A3, A13, A2, A11, A15, A8, A6, A1, A4, Th23;

        reconsider hg = ((h " ) * g) as Function of T, (S | B) by A11;

        take hg;

        (hg | A) = ((h " ) * (g | A)) by RELAT_1: 83

        .= (((h " ) * h) * f) by A17, RELAT_1: 36

        .= (( id ( dom h)) * f) by TOPS_2: 52, A12, A6

        .= f by A10, A9, RELAT_1: 53;

        hence thesis by A7, A11, A16, TOPS_2: 46;

      end;

    end;

    ::$Notion-Name

    theorem :: TIETZE_2:25

    for T be non empty TopSpace, n st n >= 1 & for S be TopSpace, A be non empty closed Subset of T, B be Subset of S st ex X be Subset of ( TOP-REAL n) st X is compact non boundary convex & (B,X) are_homeomorphic holds for f be Function of (T | A), (S | B) st f is continuous holds ex g be Function of T, (S | B) st g is continuous & (g | A) = f holds T is normal

    proof

      let T be non empty TopSpace, n;

      set TR = ( TOP-REAL n);

      assume that

       A1: n >= 1 and

       A2: for S be TopSpace, A be non empty closed Subset of T, B be Subset of S st ex X be Subset of TR st X is compact non boundary convex & (B,X) are_homeomorphic holds for f be Function of (T | A), (S | B) st f is continuous holds ex g be Function of T, (S | B) st g is continuous & (g | A) = f;

      set CC = ( Closed-Interval-TSpace (( - 1),1));

      for A be non empty closed Subset of T holds for f be continuous Function of (T | A), CC holds ex g be continuous Function of T, ( Closed-Interval-TSpace (( - 1),1)) st (g | A) = f

      proof

        let A be non empty closed Subset of T;

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

        

         A3: the carrier of CC = [.( - 1), 1.] by TOPMETR: 18;

        

         A4: ( rng f) c= REAL ;

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

        then

        reconsider F = f as Function of (T | A), R^1 by A4, TOPMETR: 17, FUNCT_2: 2;

        reconsider F as continuous Function of (T | A), R^1 by PRE_TOPC: 26;

        set IF1 = ( incl (F,n));

        set n1 = (n |-> 1);

        set CH = ( ClosedHypercube (( 0. TR),n1));

        

         A5: ( dom IF1) = the carrier of (T | A) by FUNCT_2:def 1;

        

         A6: ( [#] (TR | CH)) = CH by PRE_TOPC:def 5;

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

        then

         A7: ( 0. TR) = (n |-> 0 ) by EUCLID:def 4;

        

         A8: ( rng IF1) c= CH

        proof

          let y be object;

          assume

           A9: y in ( rng IF1);

          then

          reconsider y as Point of TR;

          consider x be object such that

           A10: x in ( dom IF1) & (IF1 . x) = y by A9, FUNCT_1:def 3;

          reconsider x as Point of (T | A) by A10;

          now

            let i;

            assume

             A11: i in ( Seg n);

            then

             A12: (y . i) = (f . x) by A10, TOPREALC: 47;

            

             A13: (( 0. TR) . i) = 0 by A7;

            (n1 . i) = 1 by A11, FINSEQ_2: 57;

            hence (y . i) in [.((( 0. TR) . i) - (n1 . i)), ((( 0. TR) . i) + (n1 . i)).] by A3, A13, A12;

          end;

          hence thesis by Def2;

        end;

        then

        reconsider IF = IF1 as Function of (T | A), (TR | CH) by A6, A5, FUNCT_2: 2;

        

         A14: IF is continuous by PRE_TOPC: 27;

        

         A15: n in ( Seg n) by A1, FINSEQ_1: 1;

        consider g be Function of T, (TR | CH) such that

         A16: g is continuous & (g | A) = IF by A2, A14, METRIZTS:def 1;

        set P = ( PROJ (n,n));

        

         A17: (P | CH) = (P | (TR | CH)) by A6, TMAP_1:def 4;

        reconsider Pch = (P | CH) as Function of (TR | CH), R^1 by PRE_TOPC: 9;

        reconsider Pg = (Pch * g) as Function of T, R^1 ;

        

         A18: P is continuous by A15, TOPREALC: 57;

        

         A19: ( dom Pg) = the carrier of T by FUNCT_2:def 1;

        

         A20: ( rng Pg) c= ( rng Pch) by RELAT_1: 26;

        

         A21: (( 0. TR) . n) = 0 by A7;

        

         A22: (n1 . n) = 1 by A1, FINSEQ_1: 1, FINSEQ_2: 57;

        (P .: CH) = [.((( 0. TR) . n) - (n1 . n)), ((( 0. TR) . n) + (n1 . n)).] by A1, FINSEQ_1: 1, Th7;

        then ( rng Pg) c= [.( - 1), 1.] by RELAT_1: 115, A20, A21, A22;

        then

        reconsider Pg as Function of T, CC by A19, A3, FUNCT_2: 2;

        

         A23: Pg is continuous by A18, A17, A16, PRE_TOPC: 27;

        

         A24: ( dom Pch) = CH by FUNCT_2:def 1;

        ((Pch * g) | A) = (Pch * (g | A)) by RELAT_1: 83

        .= (P * IF) by A16, A8, A24, RELAT_1: 165

        .= F by TOPREALC: 56, A1;

        hence thesis by A23;

      end;

      hence thesis by TIETZE: 24;

    end;