brouwer.miz



    begin

    set T2 = ( TOP-REAL 2);

    reserve n for Element of NAT ,

a,r for Real,

x for Point of ( TOP-REAL n);

    definition

      let S,T be non empty TopSpace;

      :: BROUWER:def1

      func DiffElems (S,T) -> Subset of [:S, T:] equals { [s, t] where s be Point of S, t be Point of T : s <> t };

      coherence

      proof

        set A = { [s, t] where s be Point of S, t be Point of T : s <> t };

        A c= the carrier of [:S, T:]

        proof

          let a be object;

          assume a in A;

          then ex s be Point of S, t be Point of T st a = [s, t] & s <> t;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: BROUWER:1

    for S,T be non empty TopSpace, x be set holds x in ( DiffElems (S,T)) iff ex s be Point of S, t be Point of T st x = [s, t] & s <> t;

    registration

      let S be non trivial TopSpace;

      let T be non empty TopSpace;

      cluster ( DiffElems (S,T)) -> non empty;

      coherence

      proof

        set t1 = the Element of T;

        consider s1,s2 be Element of S such that

         A1: s1 <> s2 by SUBSET_1:def 7;

        per cases ;

          suppose s1 = t1;

          then [s2, t1] in ( DiffElems (S,T)) by A1;

          hence thesis;

        end;

          suppose s1 <> t1;

          then [s1, t1] in ( DiffElems (S,T));

          hence thesis;

        end;

      end;

    end

    registration

      let S be non empty TopSpace;

      let T be non trivial TopSpace;

      cluster ( DiffElems (S,T)) -> non empty;

      coherence

      proof

        set s1 = the Element of S;

        consider t1,t2 be Element of T such that

         A1: t1 <> t2 by SUBSET_1:def 7;

        per cases ;

          suppose s1 = t1;

          then [s1, t2] in ( DiffElems (S,T)) by A1;

          hence thesis;

        end;

          suppose s1 <> t1;

          then [s1, t1] in ( DiffElems (S,T));

          hence thesis;

        end;

      end;

    end

    theorem :: BROUWER:2

    

     Th2: ( cl_Ball (x, 0 )) = {x}

    proof

      thus ( cl_Ball (x, 0 )) c= {x}

      proof

        let a be object;

        assume

         A1: a in ( cl_Ball (x, 0 ));

        then

        reconsider a as Point of ( TOP-REAL n);

         |.(a - x).| = 0 by A1, TOPREAL9: 8;

        then a = x by TOPRNS_1: 28;

        hence thesis by TARSKI:def 1;

      end;

      let a be object;

      assume a in {x};

      then

       A2: a = x by TARSKI:def 1;

       |.(x - x).| = 0 by TOPRNS_1: 28;

      hence thesis by A2, TOPREAL9: 8;

    end;

    definition

      let n be Nat, x be Point of ( TOP-REAL n), r be Real;

      :: BROUWER:def2

      func Tdisk (x,r) -> SubSpace of ( TOP-REAL n) equals (( TOP-REAL n) | ( cl_Ball (x,r)));

      coherence ;

    end

    registration

      let n be Nat, x be Point of ( TOP-REAL n);

      let r be non negative Real;

      cluster ( Tdisk (x,r)) -> non empty;

      coherence ;

    end

    theorem :: BROUWER:3

    

     Th3: the carrier of ( Tdisk (x,r)) = ( cl_Ball (x,r))

    proof

      ( [#] ( Tdisk (x,r))) = ( cl_Ball (x,r)) by PRE_TOPC:def 5;

      hence thesis;

    end;

    registration

      let n be Element of NAT , x be Point of ( TOP-REAL n), r be Real;

      cluster ( Tdisk (x,r)) -> convex;

      coherence by Th3;

    end

    reserve n for Element of NAT ,

r for non negative Real,

s,t,x for Point of ( TOP-REAL n);

    theorem :: BROUWER:4

    

     Th4: s <> t & s is Point of ( Tdisk (x,r)) & not s is Point of ( Tcircle (x,r)) implies ex e be Point of ( Tcircle (x,r)) st {e} = (( halfline (s,t)) /\ ( Sphere (x,r)))

    proof

      assume that

       A1: s <> t and

       A2: s is Point of ( Tdisk (x,r)) and

       A3: not s is Point of ( Tcircle (x,r));

      reconsider S = s, T = t, X = x as Element of ( REAL n) by EUCLID: 22;

      set a = ((( - (2 * |((t - s), (s - x))|)) + ( sqrt ( delta (( Sum ( sqr (T - S))),(2 * |((t - s), (s - x))|),(( Sum ( sqr (S - X))) - (r ^2 )))))) / (2 * ( Sum ( sqr (T - S)))));

      the carrier of ( Tdisk (x,r)) = ( cl_Ball (x,r)) by Th3;

      then

       A4: |.(s - x).| <= r by A2, TOPREAL9: 8;

      

       A5: the carrier of ( Tcircle (x,r)) = ( Sphere (x,r)) by TOPREALB: 9;

      then |.(s - x).| <> r by A3, TOPREAL9: 9;

      then |.(s - x).| < r by A4, XXREAL_0: 1;

      then s in ( Ball (x,r)) by TOPREAL9: 7;

      then

      consider e1 be Point of ( TOP-REAL n) such that

       A6: {e1} = (( halfline (s,t)) /\ ( Sphere (x,r))) and e1 = (((1 - a) * s) + (a * t)) by A1, TOPREAL9: 37;

      e1 in {e1} by TARSKI:def 1;

      then e1 in ( Sphere (x,r)) by A6, XBOOLE_0:def 4;

      hence thesis by A5, A6;

    end;

    theorem :: BROUWER:5

    

     Th5: s <> t & s in the carrier of ( Tcircle (x,r)) & t is Point of ( Tdisk (x,r)) implies ex e be Point of ( Tcircle (x,r)) st e <> s & {s, e} = (( halfline (s,t)) /\ ( Sphere (x,r)))

    proof

      assume

       A1: s <> t & s in the carrier of ( Tcircle (x,r)) & t is Point of ( Tdisk (x,r));

      reconsider S = (((1 / 2) * s) + ((1 / 2) * t)), T = t, X = x as Element of ( REAL n) by EUCLID: 22;

      

       A2: the carrier of ( Tcircle (x,r)) = ( Sphere (x,r)) by TOPREALB: 9;

      set a = ((( - (2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))), ((((1 / 2) * s) + ((1 / 2) * t)) - x))|)) + ( sqrt ( delta (( Sum ( sqr (T - S))),(2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))), ((((1 / 2) * s) + ((1 / 2) * t)) - x))|),(( Sum ( sqr (S - X))) - (r ^2 )))))) / (2 * ( Sum ( sqr (T - S)))));

      the carrier of ( Tdisk (x,r)) = ( cl_Ball (x,r)) by Th3;

      then

      consider e1 be Point of ( TOP-REAL n) such that

       A3: e1 <> s and

       A4: {s, e1} = (( halfline (s,t)) /\ ( Sphere (x,r))) and t in ( Sphere (x,r)) implies e1 = t and not t in ( Sphere (x,r)) & a = ((( - (2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))), ((((1 / 2) * s) + ((1 / 2) * t)) - x))|)) + ( sqrt ( delta (( Sum ( sqr (T - S))),(2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))), ((((1 / 2) * s) + ((1 / 2) * t)) - x))|),(( Sum ( sqr (S - X))) - (r ^2 )))))) / (2 * ( Sum ( sqr (T - S))))) implies e1 = (((1 - a) * (((1 / 2) * s) + ((1 / 2) * t))) + (a * t)) by A1, A2, TOPREAL9: 38;

      e1 in {s, e1} by TARSKI:def 2;

      then e1 in ( Sphere (x,r)) by A4, XBOOLE_0:def 4;

      hence thesis by A2, A3, A4;

    end;

    definition

      let n be non zero Element of NAT , o be Point of ( TOP-REAL n), s,t be Point of ( TOP-REAL n), r be non negative Real;

      assume that

       A1: s is Point of ( Tdisk (o,r)) and

       A2: t is Point of ( Tdisk (o,r)) and

       A3: s <> t;

      :: BROUWER:def3

      func HC (s,t,o,r) -> Point of ( TOP-REAL n) means

      : Def3: it in (( halfline (s,t)) /\ ( Sphere (o,r))) & it <> s;

      existence

      proof

        per cases ;

          suppose s is Point of ( Tcircle (o,r));

          then

          consider e be Point of ( Tcircle (o,r)) such that

           A4: e <> s & {s, e} = (( halfline (s,t)) /\ ( Sphere (o,r))) by A2, A3, Th5;

          reconsider e as Point of ( TOP-REAL n) by PRE_TOPC: 25;

          take e;

          thus thesis by A4, TARSKI:def 2;

        end;

          suppose

           A5: not s is Point of ( Tcircle (o,r));

          then

          consider e1 be Point of ( Tcircle (o,r)) such that

           A6: {e1} = (( halfline (s,t)) /\ ( Sphere (o,r))) by A1, A3, Th4;

          reconsider e1 as Point of ( TOP-REAL n) by PRE_TOPC: 25;

          take e1;

          thus thesis by A5, A6, TARSKI:def 1;

        end;

      end;

      uniqueness

      proof

        let m,u be Point of ( TOP-REAL n) such that

         A7: m in (( halfline (s,t)) /\ ( Sphere (o,r))) and

         A8: m <> s and

         A9: u in (( halfline (s,t)) /\ ( Sphere (o,r))) and

         A10: u <> s;

        per cases ;

          suppose s is Point of ( Tcircle (o,r));

          then

          consider f1 be Point of ( Tcircle (o,r)) such that f1 <> s and

           A11: {s, f1} = (( halfline (s,t)) /\ ( Sphere (o,r))) by A2, A3, Th5;

          per cases by A7, A9, A11, TARSKI:def 2;

            suppose m = f1 & u = f1;

            hence thesis;

          end;

            suppose m = f1 & u = s;

            hence thesis by A10;

          end;

            suppose m = s & u = f1;

            hence thesis by A8;

          end;

            suppose m = s & u = s;

            hence thesis;

          end;

        end;

          suppose not s is Point of ( Tcircle (o,r));

          then

          consider e be Point of ( Tcircle (o,r)) such that

           A12: {e} = (( halfline (s,t)) /\ ( Sphere (o,r))) by A1, A3, Th4;

          m = e by A7, A12, TARSKI:def 1;

          hence thesis by A9, A12, TARSKI:def 1;

        end;

      end;

    end

    reserve n for non zero Element of NAT ,

s,t,o for Point of ( TOP-REAL n);

    theorem :: BROUWER:6

    

     Th6: s is Point of ( Tdisk (o,r)) & t is Point of ( Tdisk (o,r)) & s <> t implies ( HC (s,t,o,r)) is Point of ( Tcircle (o,r))

    proof

      assume s is Point of ( Tdisk (o,r)) & t is Point of ( Tdisk (o,r)) & s <> t;

      then the carrier of ( Tcircle (o,r)) = ( Sphere (o,r)) & ( HC (s,t,o,r)) in (( halfline (s,t)) /\ ( Sphere (o,r))) by Def3, TOPREALB: 9;

      hence thesis by XBOOLE_0:def 4;

    end;

    theorem :: BROUWER:7

    for S,T,O be Element of ( REAL n) st S = s & T = t & O = o holds s is Point of ( Tdisk (o,r)) & t is Point of ( Tdisk (o,r)) & s <> t & a = ((( - |((t - s), (s - o))|) + ( sqrt (( |((t - s), (s - o))| ^2 ) - (( Sum ( sqr (T - S))) * (( Sum ( sqr (S - O))) - (r ^2 )))))) / ( Sum ( sqr (T - S)))) implies ( HC (s,t,o,r)) = (((1 - a) * s) + (a * t))

    proof

      let S,T,O be Element of ( REAL n) such that

       A1: S = s and

       A2: T = t and

       A3: O = o and

       A4: s is Point of ( Tdisk (o,r)) and

       A5: t is Point of ( Tdisk (o,r)) and

       A6: s <> t;

      

       A7: |.(T - S).| = ( sqrt ( Sum ( sqr (T - S)))) & ( Sum ( sqr (T - S))) >= 0 by EUCLID:def 5, RVSUM_1: 86;

      set H = ( HC (s,t,o,r));

      

       A8: H in (( halfline (s,t)) /\ ( Sphere (o,r))) by A4, A5, A6, Def3;

      then H in ( halfline (s,t)) by XBOOLE_0:def 4;

      then

      consider l be Real such that

       A9: H = (((1 - l) * s) + (l * t)) and

       A10: 0 <= l by TOPREAL9: 26;

      H in ( Sphere (o,r)) by A8, XBOOLE_0:def 4;

      

      then r = |.((((1 - l) * s) + (l * t)) - o).| by A9, TOPREAL9: 9

      .= |.((((1 * s) - (l * s)) + (l * t)) - o).| by RLVECT_1: 35

      .= |.(((s - (l * s)) + (l * t)) - o).| by RLVECT_1:def 8

      .= |.((s - ((l * s) - (l * t))) - o).| by RLVECT_1: 29

      .= |.((s + ( - ((l * s) - (l * t)))) + ( - o)).|

      .= |.((s + ( - o)) + ( - ((l * s) - (l * t)))).| by RLVECT_1:def 3

      .= |.((s - o) - ((l * s) - (l * t))).|

      .= |.((s - o) + ( - (l * (s - t)))).| by RLVECT_1: 34

      .= |.((s - o) + (l * ( - (s - t)))).| by RLVECT_1: 25

      .= |.((s - o) + (l * (t - s))).| by RLVECT_1: 33;

      

      then

       A11: (r ^2 ) = ((( |.(s - o).| ^2 ) + (2 * |((l * (t - s)), (s - o))|)) + ( |.(l * (t - s)).| ^2 )) by EUCLID_2: 45

      .= ((( |.(s - o).| ^2 ) + (2 * (l * |((t - s), (s - o))|))) + ( |.(l * (t - s)).| ^2 )) by EUCLID_2: 19;

      set A = ( Sum ( sqr (T - S)));

      

       A12: |.(T - S).| <> 0 by A1, A2, A6, EUCLID: 16;

       A13:

      now

        assume A <= 0 ;

        then A = 0 by RVSUM_1: 86;

        hence contradiction by A12, EUCLID:def 5, SQUARE_1: 17;

      end;

      set C = (( Sum ( sqr (S - O))) - (r ^2 ));

      set M = |((t - s), (s - o))|;

      set B = (2 * M);

      set l1 = ((( - B) - ( sqrt ( delta (A,B,C)))) / (2 * A));

      set l2 = ((( - B) + ( sqrt ( delta (A,B,C)))) / (2 * A));

      

       A14: |.(S - O).| = ( sqrt ( Sum ( sqr (S - O)))) by EUCLID:def 5;

      ( Sum ( sqr (S - O))) >= 0 by RVSUM_1: 86;

      then

       A15: ( |.(S - O).| ^2 ) = ( Sum ( sqr (S - O))) by A14, SQUARE_1:def 2;

      

       A16: ( delta (A,B,C)) = ((B ^2 ) - ((4 * A) * C)) by QUIN_1:def 1;

      the carrier of ( Tdisk (o,r)) = ( cl_Ball (o,r)) by Th3;

      then |.(s - o).| <= r by A4, TOPREAL9: 8;

      then

       A17: (( sqrt ( Sum ( sqr (S - O)))) ^2 ) <= (r ^2 ) by A1, A3, A14, SQUARE_1: 15;

      then

       A18: C <= 0 by A14, A15, XREAL_1: 47;

      now

        let x be Real;

        

        thus ( Polynom (A,B,C,x)) = (((A * (x ^2 )) + (B * x)) + C) by POLYEQ_1:def 2

        .= ((A * (x - l1)) * (x - l2)) by A13, A18, A16, QUIN_1: 16

        .= (A * ((x - l1) * (x - l2)))

        .= ( Quard (A,l1,l2,x)) by POLYEQ_1:def 3;

      end;

      then

       A19: (C / A) = (l1 * l2) by A13, POLYEQ_1: 11;

       A20:

      now

        set D = ( sqrt ( delta (A,B,C)));

        assume l1 > l2;

        then (( - D) - B) > (D - B) by A13, XREAL_1: 72;

        hence contradiction by A13, A18, A16, XREAL_1: 9;

      end;

      assume

       A21: a = ((( - M) + ( sqrt ((M ^2 ) - (A * C)))) / A);

      ( delta (A,B,C)) = ((B ^2 ) - ((4 * A) * C)) by QUIN_1:def 1

      .= (4 * ((M ^2 ) - (A * C)));

      

      then

       A22: l2 = ((( - B) + (( sqrt 4) * ( sqrt ((M ^2 ) - (A * C))))) / (2 * A)) by A13, A18, SQUARE_1: 29

      .= ((2 * ( - (M - ( sqrt ((M ^2 ) - (A * C)))))) / (2 * A)) by SQUARE_1: 20

      .= a by A21, XCMPLX_1: 91;

      

       A23: H = (((1 * s) - (l * s)) + (l * t)) by A9, RLVECT_1: 35

      .= ((s - (l * s)) + (l * t)) by RLVECT_1:def 8

      .= ((s + (l * t)) - (l * s)) by RLVECT_1:def 3

      .= (s + ((l * t) - (l * s))) by RLVECT_1:def 3

      .= (s + (l * (t - s))) by RLVECT_1: 34;

      

       A24: ( |.(l * (t - s)).| ^2 ) = (( |.l.| * |.(t - s).|) ^2 ) by TOPRNS_1: 7

      .= (( |.l.| ^2 ) * ( |.(t - s).| ^2 ))

      .= ((l ^2 ) * ( |.(t - s).| ^2 )) by COMPLEX1: 75;

      (((A * (l ^2 )) + (B * l)) + C) = (((A * (l ^2 )) + ((2 * |((t - s), (s - o))|) * l)) + (( Sum ( sqr (S - O))) - (r ^2 )))

      .= (((( |.(T - S).| ^2 ) * (l ^2 )) + ((2 * |((t - s), (s - o))|) * l)) + (( |.(S - O).| ^2 ) - (r ^2 ))) by A7, A15, SQUARE_1:def 2

      .= (((( |.(t - s).| ^2 ) * (l ^2 )) + ((2 * |((t - s), (s - o))|) * l)) + (( |.(s - o).| ^2 ) - (r ^2 ))) by A1, A2, A3

      .= 0 by A24, A11;

      then ( Polynom (A,B,C,l)) = 0 by POLYEQ_1:def 2;

      then

       A25: l = l1 or l = l2 by A13, A18, A16, POLYEQ_1: 5;

      per cases by A14, A15, A17, XREAL_1: 47;

        suppose C < 0 ;

        hence thesis by A9, A10, A13, A22, A25, A19, A20, XREAL_1: 141;

      end;

        suppose l1 = l2;

        hence thesis by A9, A22, A25;

      end;

        suppose

         A26: C = 0 ;

        now

           A27:

          now

            assume l = 0 ;

            

            then H = (s + ( 0. ( TOP-REAL n))) by A23, RLVECT_1: 10

            .= s by RLVECT_1: 4;

            hence contradiction by A4, A5, A6, Def3;

          end;

          assume

           A28: l = l1;

          per cases ;

            suppose

             A29: 0 < B;

            then l1 = ((( - B) - B) / (2 * A)) by A16, A26, SQUARE_1: 22;

            hence contradiction by A10, A13, A28, A29, XREAL_1: 129, XREAL_1: 141;

          end;

            suppose B <= 0 ;

            

            then l1 = ((( - B) - ( - B)) / (2 * A)) by A16, A26, SQUARE_1: 23

            .= 0 ;

            hence contradiction by A28, A27;

          end;

        end;

        hence thesis by A9, A22, A25;

      end;

    end;

    theorem :: BROUWER:8

    

     Th8: for r1,r2,s1,s2 be Real, s,t,o be Point of ( TOP-REAL 2) holds s is Point of ( Tdisk (o,r)) & t is Point of ( Tdisk (o,r)) & s <> t & r1 = ((t `1 ) - (s `1 )) & r2 = ((t `2 ) - (s `2 )) & s1 = ((s `1 ) - (o `1 )) & s2 = ((s `2 ) - (o `2 )) & a = ((( - ((s1 * r1) + (s2 * r2))) + ( sqrt ((((s1 * r1) + (s2 * r2)) ^2 ) - (((r1 ^2 ) + (r2 ^2 )) * (((s1 ^2 ) + (s2 ^2 )) - (r ^2 )))))) / ((r1 ^2 ) + (r2 ^2 ))) implies ( HC (s,t,o,r)) = |[((s `1 ) + (a * r1)), ((s `2 ) + (a * r2))]|

    proof

      let r1,r2,s1,s2 be Real, s,t,o be Point of ( TOP-REAL 2) such that

       A1: s is Point of ( Tdisk (o,r)) and

       A2: t is Point of ( Tdisk (o,r)) and

       A3: s <> t and

       A4: r1 = ((t `1 ) - (s `1 )) & r2 = ((t `2 ) - (s `2 )) and

       A5: s1 = ((s `1 ) - (o `1 )) and

       A6: s2 = ((s `2 ) - (o `2 )) and

       A7: a = ((( - ((s1 * r1) + (s2 * r2))) + ( sqrt ((((s1 * r1) + (s2 * r2)) ^2 ) - (((r1 ^2 ) + (r2 ^2 )) * (((s1 ^2 ) + (s2 ^2 )) - (r ^2 )))))) / ((r1 ^2 ) + (r2 ^2 )));

      the carrier of ( Tdisk (o,r)) = ( cl_Ball (o,r)) by Th3;

      then |.(s - o).| <= r by A1, TOPREAL9: 8;

      then

       A8: ( |.(s - o).| ^2 ) <= (r ^2 ) by SQUARE_1: 15;

      set C = (((s1 ^2 ) + (s2 ^2 )) - (r ^2 ));

      set A = ((r1 ^2 ) + (r2 ^2 ));

      set M = ((s1 * r1) + (s2 * r2));

      set B = (2 * M);

      set l1 = ((( - B) - ( sqrt ( delta (A,B,C)))) / (2 * A));

      set l2 = ((( - B) + ( sqrt ( delta (A,B,C)))) / (2 * A));

      

       A9: ( delta (A,B,C)) = ((B ^2 ) - ((4 * A) * C)) by QUIN_1:def 1;

      ( |.(s - o).| ^2 ) = ((((s - o) `1 ) ^2 ) + (((s - o) `2 ) ^2 )) by JGRAPH_1: 29

      .= ((s1 ^2 ) + (((s - o) `2 ) ^2 )) by A5, TOPREAL3: 3

      .= ((s1 ^2 ) + (s2 ^2 )) by A6, TOPREAL3: 3;

      then

       A10: C <= ((r ^2 ) - (r ^2 )) by A8, XREAL_1: 9;

      then

       A11: ((B ^2 ) - ((4 * A) * C)) >= 0 ;

       A12:

      now

        set D = ( sqrt ( delta (A,B,C)));

        assume l1 > l2;

        then (( - D) - B) > (D - B) by XREAL_1: 72;

        then ( - D) > D by XREAL_1: 9;

        then (( - D) + D) > (D + D) by XREAL_1: 6;

        hence contradiction by A9, A11;

      end;

      r1 <> 0 or r2 <> 0 by A3, A4, TOPREAL3: 6;

      then

       A13: ( 0 qua Nat + 0 qua Nat) < A by SQUARE_1: 12, XREAL_1: 8;

      for x be Real holds ( Polynom (A,B,C,x)) = ( Quard (A,l1,l2,x))

      proof

        let x be Real;

        

        thus ( Polynom (A,B,C,x)) = (((A * (x ^2 )) + (B * x)) + C) by POLYEQ_1:def 2

        .= ((A * (x - l1)) * (x - l2)) by A13, A9, A10, QUIN_1: 16

        .= (A * ((x - l1) * (x - l2)))

        .= ( Quard (A,l1,l2,x)) by POLYEQ_1:def 3;

      end;

      then

       A14: (C / A) = (l1 * l2) by A13, POLYEQ_1: 11;

      ( delta (A,B,C)) = ((B ^2 ) - ((4 * A) * C)) by QUIN_1:def 1

      .= (4 * ((M ^2 ) - (A * C)));

      

      then

       A15: l2 = ((( - B) + (( sqrt 4) * ( sqrt ((M ^2 ) - (A * C))))) / (2 * A)) by A10, SQUARE_1: 29

      .= ((2 * ( - (M - ( sqrt ((M ^2 ) - (A * C)))))) / (2 * A)) by SQUARE_1: 20

      .= a by A7, XCMPLX_1: 91;

      set H = ( HC (s,t,o,r));

      

       A16: H in (( halfline (s,t)) /\ ( Sphere (o,r))) by A1, A2, A3, Def3;

      then H in ( halfline (s,t)) by XBOOLE_0:def 4;

      then

      consider l be Real such that

       A17: H = (((1 - l) * s) + (l * t)) and

       A18: 0 <= l by TOPREAL9: 26;

      

       A19: H = (((1 * s) - (l * s)) + (l * t)) by A17, RLVECT_1: 35

      .= ((s - (l * s)) + (l * t)) by RLVECT_1:def 8

      .= ((s + (l * t)) - (l * s)) by RLVECT_1:def 3

      .= (s + ((l * t) - (l * s))) by RLVECT_1:def 3

      .= (s + (l * (t - s))) by RLVECT_1: 34;

      

      then

       A20: (H `1 ) = ((s `1 ) + ((l * (t - s)) `1 )) by TOPREAL3: 2

      .= ((s `1 ) + (l * ((t - s) `1 ))) by TOPREAL3: 4

      .= ((s `1 ) + (l * ((t `1 ) - (s `1 )))) by TOPREAL3: 3;

      H in ( Sphere (o,r)) by A16, XBOOLE_0:def 4;

      then |.(H - o).| = r by TOPREAL9: 9;

      

      then (r ^2 ) = ((((H - o) `1 ) ^2 ) + (((H - o) `2 ) ^2 )) by JGRAPH_1: 29

      .= ((((H `1 ) - (o `1 )) ^2 ) + (((H - o) `2 ) ^2 )) by TOPREAL3: 3

      .= ((((H `1 ) - (o `1 )) ^2 ) + (((H `2 ) - (o `2 )) ^2 )) by TOPREAL3: 3

      .= ((((((1 - l) * (s `1 )) + (l * (t `1 ))) - (o `1 )) ^2 ) + (((H `2 ) - (o `2 )) ^2 )) by A17, TOPREAL9: 41

      .= ((((((1 - l) * (s `1 )) + (l * (t `1 ))) - (o `1 )) ^2 ) + (((((1 - l) * (s `2 )) + (l * (t `2 ))) - (o `2 )) ^2 )) by A17, TOPREAL9: 42

      .= (((((l ^2 ) * ((r1 ^2 ) + (r2 ^2 ))) + ((l * 2) * M)) + (s1 ^2 )) + (s2 ^2 )) by A4, A5, A6;

      then (((A * (l ^2 )) + (B * l)) + C) = 0 ;

      then ( Polynom (A,B,C,l)) = 0 by POLYEQ_1:def 2;

      then

       A21: l = l1 or l = l2 by A13, A9, A10, POLYEQ_1: 5;

      

       A22: (H `2 ) = ((s `2 ) + ((l * (t - s)) `2 )) by A19, TOPREAL3: 2

      .= ((s `2 ) + (l * ((t - s) `2 ))) by TOPREAL3: 4

      .= ((s `2 ) + (l * ((t `2 ) - (s `2 )))) by TOPREAL3: 3;

      per cases by A10;

        suppose C < 0 ;

        hence thesis by A4, A18, A20, A22, A13, A15, A21, A14, A12, EUCLID: 53, XREAL_1: 141;

      end;

        suppose l1 = l2;

        hence thesis by A4, A20, A22, A15, A21, EUCLID: 53;

      end;

        suppose

         A23: C = 0 ;

        now

           A24:

          now

            assume l = 0 ;

            

            then H = (s + ( 0. ( TOP-REAL 2))) by A19, RLVECT_1: 10

            .= s by RLVECT_1: 4;

            hence contradiction by A1, A2, A3, Def3;

          end;

          assume

           A25: l = l1;

          per cases ;

            suppose

             A26: 0 < B;

            then l1 = ((( - B) - B) / (2 * A)) by A9, A23, SQUARE_1: 22;

            hence contradiction by A18, A13, A25, A26, XREAL_1: 129, XREAL_1: 141;

          end;

            suppose B <= 0 ;

            

            then l1 = ((( - B) - ( - B)) / (2 * A)) by A9, A23, SQUARE_1: 23

            .= 0 ;

            hence contradiction by A25, A24;

          end;

        end;

        hence thesis by A4, A20, A22, A15, A21, EUCLID: 53;

      end;

    end;

    definition

      let n be non zero Element of NAT , o be Point of ( TOP-REAL n), r be non negative Real;

      let x be Point of ( Tdisk (o,r));

      let f be Function of ( Tdisk (o,r)), ( Tdisk (o,r));

      :: BROUWER:def4

      func HC (x,f) -> Point of ( Tcircle (o,r)) means

      : Def4: ex y,z be Point of ( TOP-REAL n) st y = x & z = (f . x) & it = ( HC (z,y,o,r));

      existence

      proof

        reconsider y = x, z = (f . x) as Point of ( TOP-REAL n) by PRE_TOPC: 25;

        x <> (f . x) by A1;

        then

        reconsider a = ( HC (z,y,o,r)) as Point of ( Tcircle (o,r)) by Th6;

        take a;

        thus thesis;

      end;

      uniqueness ;

    end

    theorem :: BROUWER:9

    

     Th9: for x be Point of ( Tdisk (o,r)), f be Function of ( Tdisk (o,r)), ( Tdisk (o,r)) st not x is_a_fixpoint_of f & x is Point of ( Tcircle (o,r)) holds ( HC (x,f)) = x

    proof

      let x be Point of ( Tdisk (o,r));

      let f be Function of ( Tdisk (o,r)), ( Tdisk (o,r)) such that

       A1: not x is_a_fixpoint_of f and

       A2: x is Point of ( Tcircle (o,r));

      

       A3: x <> (f . x) by A1;

      

       A4: the carrier of ( Tcircle (o,r)) = ( Sphere (o,r)) by TOPREALB: 9;

      consider y,z be Point of ( TOP-REAL n) such that

       A5: y = x and

       A6: z = (f . x) & ( HC (x,f)) = ( HC (z,y,o,r)) by A1, Def4;

      x in ( halfline (z,y)) by A5, TOPREAL9: 28;

      then x in (( halfline (z,y)) /\ ( Sphere (o,r))) by A2, A4, XBOOLE_0:def 4;

      hence thesis by A3, A5, A6, Def3;

    end;

    theorem :: BROUWER:10

    

     Th10: for r be positive Real, o be Point of ( TOP-REAL 2), Y be non empty SubSpace of ( Tdisk (o,r)) st Y = ( Tcircle (o,r)) holds not Y is_a_retract_of ( Tdisk (o,r))

    proof

      let r be positive Real, o be Point of ( TOP-REAL 2), Y be non empty SubSpace of ( Tdisk (o,r)) such that

       A1: Y = ( Tcircle (o,r));

      set y0 = the Point of Y;

      set X = ( Tdisk (o,r));

      

       A2: y0 in the carrier of Y;

      the carrier of ( Tcircle (o,r)) = ( Sphere (o,r)) & ( Sphere (o,r)) c= ( cl_Ball (o,r)) by TOPREAL9: 17, TOPREALB: 9;

      then

      reconsider x0 = y0 as Point of X by A1, A2, Th3;

      reconsider a0 = 0 , a1 = 1 as Point of I[01] by BORSUK_1:def 14, BORSUK_1:def 15;

      set C = the constant Loop of x0;

      

       A3: C = ( I[01] --> x0) by BORSUK_2: 5

      .= (the carrier of I[01] --> y0);

      then

      reconsider D = C as Function of I[01] , Y;

      

       A4: D = ( I[01] --> y0) & (D . a0) = y0 by A3, FUNCOP_1: 7;

      (y0,y0) are_connected & (D . a1) = y0 by A3, FUNCOP_1: 7;

      then

      reconsider D as constant Loop of y0 by A4, BORSUK_2:def 2;

      given R be continuous Function of X, Y such that

       A5: R is being_a_retraction;

      the carrier of ( pi_1 (Y,y0)) = {( Class (( EqRel (Y,y0)),D))}

      proof

        set E = ( EqRel (Y,y0));

        hereby

          let x be object;

          assume x in the carrier of ( pi_1 (Y,y0));

          then

          consider f0 be Loop of y0 such that

           A6: x = ( Class (E,f0)) by TOPALG_1: 47;

          reconsider g0 = f0 as Loop of x0 by TOPALG_2: 1;

          (g0,C) are_homotopic by TOPALG_2: 2;

          then

          consider f be Function of [: I[01] , I[01] :], X such that

           A7: f is continuous and

           A8: for s be Point of I[01] holds (f . (s, 0 )) = (g0 . s) & (f . (s,1)) = (C . s) & for t be Point of I[01] holds (f . ( 0 ,t)) = x0 & (f . (1,t)) = x0;

          (f0,D) are_homotopic

          proof

            take F = (R * f);

            thus F is continuous by A7;

            let s be Point of I[01] ;

            

            thus (F . (s, 0 )) = (F . [s, a0])

            .= (R . (f . (s, 0 ))) by FUNCT_2: 15

            .= (R . (g0 . s)) by A8

            .= (f0 . s) by A5;

            

            thus (F . (s,1)) = (F . [s, a1])

            .= (R . (f . (s,1))) by FUNCT_2: 15

            .= (R . (C . s)) by A8

            .= (D . s) by A5;

            

            thus (F . ( 0 ,s)) = (F . [a0, s])

            .= (R . (f . ( 0 ,s))) by FUNCT_2: 15

            .= (R . x0) by A8

            .= y0 by A5;

            

            thus (F . (1,s)) = (F . [a1, s])

            .= (R . (f . (1,s))) by FUNCT_2: 15

            .= (R . x0) by A8

            .= y0 by A5;

          end;

          then x = ( Class (E,D)) by A6, TOPALG_1: 46;

          hence x in {( Class (E,D))} by TARSKI:def 1;

        end;

        let x be object;

        assume x in {( Class (E,D))};

        then

         A9: x = ( Class (E,D)) by TARSKI:def 1;

        D in ( Loops y0) by TOPALG_1:def 1;

        then x in ( Class E) by A9, EQREL_1:def 3;

        hence thesis by TOPALG_1:def 5;

      end;

      hence contradiction by A1;

    end;

    definition

      let n be non zero Element of NAT ;

      let r be non negative Real;

      let o be Point of ( TOP-REAL n);

      let f be Function of ( Tdisk (o,r)), ( Tdisk (o,r));

      :: BROUWER:def5

      func BR-map (f) -> Function of ( Tdisk (o,r)), ( Tcircle (o,r)) means

      : Def5: for x be Point of ( Tdisk (o,r)) holds (it . x) = ( HC (x,f));

      existence

      proof

        defpred P[ Point of ( Tdisk (o,r)), set] means $2 = ( HC ($1,f));

        

         A1: for x be Point of ( Tdisk (o,r)) holds ex m be Point of ( Tcircle (o,r)) st P[x, m];

        ex h be Function of ( Tdisk (o,r)), ( Tcircle (o,r)) st for x be Point of ( Tdisk (o,r)) holds P[x, (h . x)] from FUNCT_2:sch 3( A1);

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be Function of ( Tdisk (o,r)), ( Tcircle (o,r)) such that

         A2: for x be Point of ( Tdisk (o,r)) holds (f1 . x) = ( HC (x,f)) and

         A3: for x be Point of ( Tdisk (o,r)) holds (f2 . x) = ( HC (x,f));

        for x be Point of ( Tdisk (o,r)) holds (f1 . x) = (f2 . x)

        proof

          let x be Point of ( Tdisk (o,r));

          

          thus (f1 . x) = ( HC (x,f)) by A2

          .= (f2 . x) by A3;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    theorem :: BROUWER:11

    

     Th11: for o be Point of ( TOP-REAL n), x be Point of ( Tdisk (o,r)), f be Function of ( Tdisk (o,r)), ( Tdisk (o,r)) st not x is_a_fixpoint_of f & x is Point of ( Tcircle (o,r)) holds (( BR-map f) . x) = x

    proof

      let o be Point of ( TOP-REAL n);

      let x be Point of ( Tdisk (o,r));

      let f be Function of ( Tdisk (o,r)), ( Tdisk (o,r)) such that

       A1: ( not x is_a_fixpoint_of f) & x is Point of ( Tcircle (o,r));

      

      thus (( BR-map f) . x) = ( HC (x,f)) by Def5

      .= x by A1, Th9;

    end;

    theorem :: BROUWER:12

    for f be continuous Function of ( Tdisk (o,r)), ( Tdisk (o,r)) holds f is without_fixpoints implies (( BR-map f) | ( Sphere (o,r))) = ( id ( Tcircle (o,r)))

    proof

      let f be continuous Function of ( Tdisk (o,r)), ( Tdisk (o,r)) such that

       A1: f is without_fixpoints;

      set D = ( cl_Ball (o,r));

      set C = ( Sphere (o,r));

      set g = ( BR-map f);

      ( dom g) = the carrier of ( Tdisk (o,r)) & the carrier of ( Tdisk (o,r)) = D by Th3, FUNCT_2:def 1;

      then

       A2: ( dom (g | C)) = C by RELAT_1: 62, TOPREAL9: 17;

      

       A3: the carrier of ( Tcircle (o,r)) = C by TOPREALB: 9;

      

       A4: for x be object st x in ( dom (g | C)) holds ((g | C) . x) = (( id ( Tcircle (o,r))) . x)

      proof

        let x be object such that

         A5: x in ( dom (g | C));

        x in ( dom g) by A5, RELAT_1: 57;

        then

        reconsider y = x as Point of ( Tdisk (o,r));

        

         A6: not x is_a_fixpoint_of f by A1;

        

        thus ((g | C) . x) = (g . x) by A5, FUNCT_1: 49

        .= y by A3, A5, A6, Th11

        .= (( id ( Tcircle (o,r))) . x) by A3, A5, FUNCT_1: 18;

      end;

      ( dom ( id ( Tcircle (o,r)))) = the carrier of ( Tcircle (o,r));

      hence thesis by A2, A3, A4, FUNCT_1: 2;

    end;

     Lm1:

    now

      let T be non empty TopSpace;

      let a be Element of REAL ;

      set c = the carrier of T;

      set f = (c --> a);

      thus f is continuous

      proof

        let Y be Subset of REAL ;

        

         A1: ( dom f) = c by FUNCT_2:def 1;

        assume Y is closed;

        

         A2: ( rng f) = {a} by FUNCOP_1: 8;

        per cases ;

          suppose a in Y;

          then

           A3: ( rng f) c= Y by A2, ZFMISC_1: 31;

          (f " Y) = (f " (( rng f) /\ Y)) by RELAT_1: 133

          .= (f " ( rng f)) by A3, XBOOLE_1: 28

          .= ( [#] T) by A1, RELAT_1: 134;

          hence thesis;

        end;

          suppose not a in Y;

          then

           A4: ( rng f) misses Y by A2, ZFMISC_1: 50;

          (f " Y) = (f " (( rng f) /\ Y)) by RELAT_1: 133

          .= (f " {} ) by A4

          .= ( {} T);

          hence thesis;

        end;

      end;

    end;

    theorem :: BROUWER:13

    

     Th13: for r be positive Real, o be Point of ( TOP-REAL 2), f be continuous Function of ( Tdisk (o,r)), ( Tdisk (o,r)) holds f is without_fixpoints implies ( BR-map f) is continuous

    proof

      set R = R2Homeomorphism ;

      defpred fx2[ set, set] means ex x1,x2 be Point of T2 st $1 = [x1, x2] & $2 = (x2 `1 );

      defpred dx[ set, set] means ex x1,x2 be Point of T2 st $1 = [x1, x2] & $2 = ((x1 `1 ) - (x2 `1 ));

      let r be positive Real, o be Point of ( TOP-REAL 2);

      defpred xo[ set, set] means ex x1,x2 be Point of T2 st $1 = [x1, x2] & $2 = ((x2 `1 ) - (o `1 ));

      defpred yo[ set, set] means ex x1,x2 be Point of T2 st $1 = [x1, x2] & $2 = ((x2 `2 ) - (o `2 ));

      reconsider rr = (r ^2 ) as Element of REAL by XREAL_0:def 1;

      set f1 = (the carrier of [:T2, T2:] --> rr);

      

       A1: for x be Element of [:T2, T2:] holds ex r be Element of REAL st xo[x, r]

      proof

        let x be Element of [:T2, T2:];

        consider x1,x2 be Point of T2 such that

         A2: x = [x1, x2] by BORSUK_1: 10;

        reconsider x2o = ((x2 `1 ) - (o `1 )) as Element of REAL by XREAL_0:def 1;

        take x2o, x1, x2;

        thus thesis by A2;

      end;

      consider xo be RealMap of [:T2, T2:] such that

       A3: for x be Point of [:T2, T2:] holds xo[x, (xo . x)] from FUNCT_2:sch 3( A1);

      

       A4: for x be Element of [:T2, T2:] holds ex r be Element of REAL st fx2[x, r]

      proof

        let x be Element of [:T2, T2:];

        consider x1,x2 be Point of T2 such that

         A5: x = [x1, x2] by BORSUK_1: 10;

        reconsider x21 = (x2 `1 ) as Element of REAL by XREAL_0:def 1;

        take x21, x1, x2;

        thus thesis by A5;

      end;

      consider fx2 be RealMap of [:T2, T2:] such that

       A6: for x be Point of [:T2, T2:] holds fx2[x, (fx2 . x)] from FUNCT_2:sch 3( A4);

      

       A7: for x be Element of [:T2, T2:] holds ex r be Element of REAL st yo[x, r]

      proof

        let x be Element of [:T2, T2:];

        consider x1,x2 be Point of T2 such that

         A8: x = [x1, x2] by BORSUK_1: 10;

        reconsider x2o = ((x2 `2 ) - (o `2 )) as Element of REAL by XREAL_0:def 1;

        take x2o, x1, x2;

        thus thesis by A8;

      end;

      consider yo be RealMap of [:T2, T2:] such that

       A9: for x be Point of [:T2, T2:] holds yo[x, (yo . x)] from FUNCT_2:sch 3( A7);

      reconsider f1 as continuous RealMap of [:T2, T2:] by Lm1;

      set D2 = ( Tdisk (o,r));

      set S1 = ( Tcircle (o,r));

      set OK = (( DiffElems (T2,T2)) /\ the carrier of [:D2, D2:]);

      set s = the Point of S1;

      

       A10: |.(o - o).| = |.( 0. ( TOP-REAL 2)).| by RLVECT_1: 5

      .= 0 by TOPRNS_1: 23;

      

       A11: the carrier of S1 = ( Sphere (o,r)) by TOPREALB: 9;

       A12:

      now

        assume

         A13: o = s;

        ( Ball (o,r)) misses ( Sphere (o,r)) & o in ( Ball (o,r)) by A10, TOPREAL9: 7, TOPREAL9: 19;

        hence contradiction by A11, A13, XBOOLE_0: 3;

      end;

      the carrier of D2 = ( cl_Ball (o,r)) by Th3;

      then

       A14: o is Point of D2 by A10, TOPREAL9: 8;

      s in the carrier of S1 & ( Sphere (o,r)) c= ( cl_Ball (o,r)) by TOPREAL9: 17;

      then s is Point of D2 by A11, Th3;

      then [o, s] in [:the carrier of D2, the carrier of D2:] by A14, ZFMISC_1: 87;

      then

       A15: [o, s] in the carrier of [:D2, D2:] by BORSUK_1:def 2;

      s is Point of T2 by PRE_TOPC: 25;

      then [o, s] in ( DiffElems (T2,T2)) by A12;

      then

      reconsider OK as non empty Subset of [:T2, T2:] by A15, XBOOLE_0:def 4;

      set Zf1 = (f1 | OK);

      defpred fy2[ set, set] means ex x1,x2 be Point of T2 st $1 = [x1, x2] & $2 = (x2 `2 );

      defpred dy[ set, set] means ex y1,y2 be Point of T2 st $1 = [y1, y2] & $2 = ((y1 `2 ) - (y2 `2 ));

      set TD = ( [:T2, T2:] | OK);

      let f be continuous Function of D2, D2 such that

       A16: f is without_fixpoints;

      

       A17: for x be Element of [:T2, T2:] holds ex r be Element of REAL st dy[x, r]

      proof

        let x be Element of [:T2, T2:];

        consider x1,x2 be Point of T2 such that

         A18: x = [x1, x2] by BORSUK_1: 10;

        reconsider x12 = ((x1 `2 ) - (x2 `2 )) as Element of REAL by XREAL_0:def 1;

        take x12, x1, x2;

        thus thesis by A18;

      end;

      consider dy be RealMap of [:T2, T2:] such that

       A19: for y be Point of [:T2, T2:] holds dy[y, (dy . y)] from FUNCT_2:sch 3( A17);

      

       A20: for x be Element of [:T2, T2:] holds ex r be Element of REAL st fy2[x, r]

      proof

        let x be Element of [:T2, T2:];

        consider x1,x2 be Point of T2 such that

         A21: x = [x1, x2] by BORSUK_1: 10;

        reconsider x22 = (x2 `2 ) as Element of REAL by XREAL_0:def 1;

        take x22, x1, x2;

        thus thesis by A21;

      end;

      consider fy2 be RealMap of [:T2, T2:] such that

       A22: for x be Point of [:T2, T2:] holds fy2[x, (fy2 . x)] from FUNCT_2:sch 3( A20);

      

       A23: for x be Element of [:T2, T2:] holds ex r be Element of REAL st dx[x, r]

      proof

        let x be Element of [:T2, T2:];

        consider x1,x2 be Point of T2 such that

         A24: x = [x1, x2] by BORSUK_1: 10;

        reconsider x12 = ((x1 `1 ) - (x2 `1 )) as Element of REAL by XREAL_0:def 1;

        take x12, x1, x2;

        thus thesis by A24;

      end;

      consider dx be RealMap of [:T2, T2:] such that

       A25: for x be Point of [:T2, T2:] holds dx[x, (dx . x)] from FUNCT_2:sch 3( A23);

      reconsider Dx = dx, Dy = dy, fX2 = fx2, fY2 = fy2, Xo = xo, Yo = yo as Function of [:T2, T2:], R^1 by TOPMETR: 17;

      for p be Point of [:T2, T2:], V be Subset of R^1 st (Yo . p) in V & V is open holds ex W be Subset of [:T2, T2:] st p in W & W is open & (Yo .: W) c= V

      proof

        let p be Point of [:T2, T2:], V be Subset of R^1 such that

         A26: (Yo . p) in V and

         A27: V is open;

        reconsider V1 = V as open Subset of REAL by A27, BORSUK_5: 39, TOPMETR: 17;

        consider p1,p2 be Point of T2 such that

         A28: p = [p1, p2] and

         A29: (Yo . p) = ((p2 `2 ) - (o `2 )) by A9;

        set r = ((p2 `2 ) - (o `2 ));

        consider g be Real such that

         A30: 0 < g and

         A31: ].(r - g), (r + g).[ c= V1 by A26, A29, RCOMP_1: 19;

        reconsider g as Element of REAL by XREAL_0:def 1;

        set W2 = { |[x, y]| where x,y be Real : ((p2 `2 ) - g) < y & y < ((p2 `2 ) + g) };

        W2 c= the carrier of T2

        proof

          let a be object;

          assume a in W2;

          then ex x,y be Real st a = |[x, y]| & ((p2 `2 ) - g) < y & y < ((p2 `2 ) + g);

          hence thesis;

        end;

        then

        reconsider W2 as Subset of T2;

        take [:( [#] T2), W2:];

        

         A32: p2 = |[(p2 `1 ), (p2 `2 )]| by EUCLID: 53;

        ((p2 `2 ) - g) < ((p2 `2 ) - 0 ) & ((p2 `2 ) + 0 qua Nat) < ((p2 `2 ) + g) by A30, XREAL_1: 6, XREAL_1: 15;

        then p2 in W2 by A32;

        hence p in [:( [#] T2), W2:] by A28, ZFMISC_1:def 2;

        W2 is open by PSCOMP_1: 21;

        hence [:( [#] T2), W2:] is open by BORSUK_1: 6;

        let b be object;

        assume b in (Yo .: [:( [#] T2), W2:]);

        then

        consider a be Point of [:T2, T2:] such that

         A33: a in [:( [#] T2), W2:] and

         A34: (Yo . a) = b by FUNCT_2: 65;

        consider a1,a2 be Point of T2 such that

         A35: a = [a1, a2] and

         A36: (yo . a) = ((a2 `2 ) - (o `2 )) by A9;

        a2 in W2 by A33, A35, ZFMISC_1: 87;

        then

        consider x2,y2 be Real such that

         A37: a2 = |[x2, y2]| and

         A38: ((p2 `2 ) - g) < y2 & y2 < ((p2 `2 ) + g);

        (a2 `2 ) = y2 by A37, EUCLID: 52;

        then (((p2 `2 ) - g) - (o `2 )) < ((a2 `2 ) - (o `2 )) & ((a2 `2 ) - (o `2 )) < (((p2 `2 ) + g) - (o `2 )) by A38, XREAL_1: 9;

        then ((a2 `2 ) - (o `2 )) in ].(r - g), (r + g).[ by XXREAL_1: 4;

        hence thesis by A31, A34, A36;

      end;

      then Yo is continuous by JGRAPH_2: 10;

      then

      reconsider yo as continuous RealMap of [:T2, T2:] by JORDAN5A: 27;

      for p be Point of [:T2, T2:], V be Subset of R^1 st (Xo . p) in V & V is open holds ex W be Subset of [:T2, T2:] st p in W & W is open & (Xo .: W) c= V

      proof

        let p be Point of [:T2, T2:], V be Subset of R^1 such that

         A39: (Xo . p) in V and

         A40: V is open;

        reconsider V1 = V as open Subset of REAL by A40, BORSUK_5: 39, TOPMETR: 17;

        consider p1,p2 be Point of T2 such that

         A41: p = [p1, p2] and

         A42: (Xo . p) = ((p2 `1 ) - (o `1 )) by A3;

        set r = ((p2 `1 ) - (o `1 ));

        consider g be Real such that

         A43: 0 < g and

         A44: ].(r - g), (r + g).[ c= V1 by A39, A42, RCOMP_1: 19;

        reconsider g as Element of REAL by XREAL_0:def 1;

        set W2 = { |[x, y]| where x,y be Real : ((p2 `1 ) - g) < x & x < ((p2 `1 ) + g) };

        W2 c= the carrier of T2

        proof

          let a be object;

          assume a in W2;

          then ex x,y be Real st a = |[x, y]| & ((p2 `1 ) - g) < x & x < ((p2 `1 ) + g);

          hence thesis;

        end;

        then

        reconsider W2 as Subset of T2;

        take [:( [#] T2), W2:];

        

         A45: p2 = |[(p2 `1 ), (p2 `2 )]| by EUCLID: 53;

        ((p2 `1 ) - g) < ((p2 `1 ) - 0 ) & ((p2 `1 ) + 0 qua Nat) < ((p2 `1 ) + g) by A43, XREAL_1: 6, XREAL_1: 15;

        then p2 in W2 by A45;

        hence p in [:( [#] T2), W2:] by A41, ZFMISC_1:def 2;

        W2 is open by PSCOMP_1: 19;

        hence [:( [#] T2), W2:] is open by BORSUK_1: 6;

        let b be object;

        assume b in (Xo .: [:( [#] T2), W2:]);

        then

        consider a be Point of [:T2, T2:] such that

         A46: a in [:( [#] T2), W2:] and

         A47: (Xo . a) = b by FUNCT_2: 65;

        consider a1,a2 be Point of T2 such that

         A48: a = [a1, a2] and

         A49: (xo . a) = ((a2 `1 ) - (o `1 )) by A3;

        a2 in W2 by A46, A48, ZFMISC_1: 87;

        then

        consider x2,y2 be Real such that

         A50: a2 = |[x2, y2]| and

         A51: ((p2 `1 ) - g) < x2 & x2 < ((p2 `1 ) + g);

        (a2 `1 ) = x2 by A50, EUCLID: 52;

        then (((p2 `1 ) - g) - (o `1 )) < ((a2 `1 ) - (o `1 )) & ((a2 `1 ) - (o `1 )) < (((p2 `1 ) + g) - (o `1 )) by A51, XREAL_1: 9;

        then ((a2 `1 ) - (o `1 )) in ].(r - g), (r + g).[ by XXREAL_1: 4;

        hence thesis by A44, A47, A49;

      end;

      then Xo is continuous by JGRAPH_2: 10;

      then

      reconsider xo as continuous RealMap of [:T2, T2:] by JORDAN5A: 27;

      set Zyo = (yo | OK);

      set Zxo = (xo | OK);

      set p2 = (((Zxo (#) Zxo) + (Zyo (#) Zyo)) - Zf1);

      set g = ( BR-map f);

      

       A52: the carrier of TD = OK by PRE_TOPC: 8;

      for p be Point of [:T2, T2:], V be Subset of R^1 st (Dy . p) in V & V is open holds ex W be Subset of [:T2, T2:] st p in W & W is open & (Dy .: W) c= V

      proof

        let p be Point of [:T2, T2:], V be Subset of R^1 such that

         A53: (Dy . p) in V and

         A54: V is open;

        reconsider V1 = V as open Subset of REAL by A54, BORSUK_5: 39, TOPMETR: 17;

        consider p1,p2 be Point of T2 such that

         A55: p = [p1, p2] and

         A56: (dy . p) = ((p1 `2 ) - (p2 `2 )) by A19;

        set r = ((p1 `2 ) - (p2 `2 ));

        consider g be Real such that

         A57: 0 < g and

         A58: ].(r - g), (r + g).[ c= V1 by A53, A56, RCOMP_1: 19;

        reconsider g as Element of REAL by XREAL_0:def 1;

        set W2 = { |[x, y]| where x,y be Real : ((p2 `2 ) - (g / 2)) < y & y < ((p2 `2 ) + (g / 2)) };

        

         A59: W2 c= the carrier of T2

        proof

          let a be object;

          assume a in W2;

          then ex x,y be Real st a = |[x, y]| & ((p2 `2 ) - (g / 2)) < y & y < ((p2 `2 ) + (g / 2));

          hence thesis;

        end;

        

         A60: p2 = |[(p2 `1 ), (p2 `2 )]| by EUCLID: 53;

        reconsider W2 as Subset of T2 by A59;

        

         A61: ( 0 / 2) < (g / 2) by A57, XREAL_1: 74;

        then ((p2 `2 ) - (g / 2)) < ((p2 `2 ) - 0 ) & ((p2 `2 ) + 0 qua Nat) < ((p2 `2 ) + (g / 2)) by XREAL_1: 6, XREAL_1: 15;

        then

         A62: p2 in W2 by A60;

        set W1 = { |[x, y]| where x,y be Real : ((p1 `2 ) - (g / 2)) < y & y < ((p1 `2 ) + (g / 2)) };

        W1 c= the carrier of T2

        proof

          let a be object;

          assume a in W1;

          then ex x,y be Real st a = |[x, y]| & ((p1 `2 ) - (g / 2)) < y & y < ((p1 `2 ) + (g / 2));

          hence thesis;

        end;

        then

        reconsider W1 as Subset of T2;

        take [:W1, W2:];

        

         A63: p1 = |[(p1 `1 ), (p1 `2 )]| by EUCLID: 53;

        ((p1 `2 ) - (g / 2)) < ((p1 `2 ) - 0 ) & ((p1 `2 ) + 0 qua Nat) < ((p1 `2 ) + (g / 2)) by A61, XREAL_1: 6, XREAL_1: 15;

        then p1 in W1 by A63;

        hence p in [:W1, W2:] by A55, A62, ZFMISC_1:def 2;

        W1 is open & W2 is open by PSCOMP_1: 21;

        hence [:W1, W2:] is open by BORSUK_1: 6;

        let b be object;

        assume b in (Dy .: [:W1, W2:]);

        then

        consider a be Point of [:T2, T2:] such that

         A64: a in [:W1, W2:] and

         A65: (Dy . a) = b by FUNCT_2: 65;

        consider a1,a2 be Point of T2 such that

         A66: a = [a1, a2] and

         A67: (dy . a) = ((a1 `2 ) - (a2 `2 )) by A19;

        a2 in W2 by A64, A66, ZFMISC_1: 87;

        then

        consider x2,y2 be Real such that

         A68: a2 = |[x2, y2]| and

         A69: ((p2 `2 ) - (g / 2)) < y2 and

         A70: y2 < ((p2 `2 ) + (g / 2));

        

         A71: (a2 `2 ) = y2 by A68, EUCLID: 52;

        ((p2 `2 ) - y2) > ((p2 `2 ) - ((p2 `2 ) + (g / 2))) by A70, XREAL_1: 15;

        then

         A72: ((p2 `2 ) - y2) > ( - (g / 2));

        (((p2 `2 ) - (g / 2)) + (g / 2)) < (y2 + (g / 2)) by A69, XREAL_1: 6;

        then ((p2 `2 ) - y2) < ((y2 + (g / 2)) - y2) by XREAL_1: 9;

        then

         A73: |.((p2 `2 ) - y2).| < (g / 2) by A72, SEQ_2: 1;

        a1 in W1 by A64, A66, ZFMISC_1: 87;

        then

        consider x1,y1 be Real such that

         A74: a1 = |[x1, y1]| and

         A75: ((p1 `2 ) - (g / 2)) < y1 and

         A76: y1 < ((p1 `2 ) + (g / 2));

        ((p1 `2 ) - y1) > ((p1 `2 ) - ((p1 `2 ) + (g / 2))) by A76, XREAL_1: 15;

        then

         A77: ((p1 `2 ) - y1) > ( - (g / 2));

         |.(((p1 `2 ) - y1) - ((p2 `2 ) - y2)).| <= ( |.((p1 `2 ) - y1).| + |.((p2 `2 ) - y2).|) by COMPLEX1: 57;

        then

         A78: |.( - (((p1 `2 ) - y1) - ((p2 `2 ) - y2))).| <= ( |.((p1 `2 ) - y1).| + |.((p2 `2 ) - y2).|) by COMPLEX1: 52;

        (((p1 `2 ) - (g / 2)) + (g / 2)) < (y1 + (g / 2)) by A75, XREAL_1: 6;

        then ((p1 `2 ) - y1) < ((y1 + (g / 2)) - y1) by XREAL_1: 9;

        then |.((p1 `2 ) - y1).| < (g / 2) by A77, SEQ_2: 1;

        then ( |.((p1 `2 ) - y1).| + |.((p2 `2 ) - y2).|) < ((g / 2) + (g / 2)) by A73, XREAL_1: 8;

        then

         A79: |.((y1 - y2) - r).| < g by A78, XXREAL_0: 2;

        (a1 `2 ) = y1 by A74, EUCLID: 52;

        then ((a1 `2 ) - (a2 `2 )) in ].(r - g), (r + g).[ by A71, A79, RCOMP_1: 1;

        hence thesis by A58, A65, A67;

      end;

      then Dy is continuous by JGRAPH_2: 10;

      then

      reconsider dy as continuous RealMap of [:T2, T2:] by JORDAN5A: 27;

      for p be Point of [:T2, T2:], V be Subset of R^1 st (Dx . p) in V & V is open holds ex W be Subset of [:T2, T2:] st p in W & W is open & (Dx .: W) c= V

      proof

        let p be Point of [:T2, T2:], V be Subset of R^1 such that

         A80: (Dx . p) in V and

         A81: V is open;

        reconsider V1 = V as open Subset of REAL by A81, BORSUK_5: 39, TOPMETR: 17;

        consider p1,p2 be Point of T2 such that

         A82: p = [p1, p2] and

         A83: (dx . p) = ((p1 `1 ) - (p2 `1 )) by A25;

        set r = ((p1 `1 ) - (p2 `1 ));

        consider g be Real such that

         A84: 0 < g and

         A85: ].(r - g), (r + g).[ c= V1 by A80, A83, RCOMP_1: 19;

        reconsider g as Element of REAL by XREAL_0:def 1;

        set W2 = { |[x, y]| where x,y be Real : ((p2 `1 ) - (g / 2)) < x & x < ((p2 `1 ) + (g / 2)) };

        

         A86: W2 c= the carrier of T2

        proof

          let a be object;

          assume a in W2;

          then ex x,y be Real st a = |[x, y]| & ((p2 `1 ) - (g / 2)) < x & x < ((p2 `1 ) + (g / 2));

          hence thesis;

        end;

        

         A87: p2 = |[(p2 `1 ), (p2 `2 )]| by EUCLID: 53;

        reconsider W2 as Subset of T2 by A86;

        

         A88: ( 0 / 2) < (g / 2) by A84, XREAL_1: 74;

        then ((p2 `1 ) - (g / 2)) < ((p2 `1 ) - 0 ) & ((p2 `1 ) + 0 qua Nat) < ((p2 `1 ) + (g / 2)) by XREAL_1: 6, XREAL_1: 15;

        then

         A89: p2 in W2 by A87;

        set W1 = { |[x, y]| where x,y be Real : ((p1 `1 ) - (g / 2)) < x & x < ((p1 `1 ) + (g / 2)) };

        W1 c= the carrier of T2

        proof

          let a be object;

          assume a in W1;

          then ex x,y be Real st a = |[x, y]| & ((p1 `1 ) - (g / 2)) < x & x < ((p1 `1 ) + (g / 2));

          hence thesis;

        end;

        then

        reconsider W1 as Subset of T2;

        take [:W1, W2:];

        

         A90: p1 = |[(p1 `1 ), (p1 `2 )]| by EUCLID: 53;

        ((p1 `1 ) - (g / 2)) < ((p1 `1 ) - 0 ) & ((p1 `1 ) + 0 qua Nat) < ((p1 `1 ) + (g / 2)) by A88, XREAL_1: 6, XREAL_1: 15;

        then p1 in W1 by A90;

        hence p in [:W1, W2:] by A82, A89, ZFMISC_1:def 2;

        W1 is open & W2 is open by PSCOMP_1: 19;

        hence [:W1, W2:] is open by BORSUK_1: 6;

        let b be object;

        assume b in (Dx .: [:W1, W2:]);

        then

        consider a be Point of [:T2, T2:] such that

         A91: a in [:W1, W2:] and

         A92: (Dx . a) = b by FUNCT_2: 65;

        consider a1,a2 be Point of T2 such that

         A93: a = [a1, a2] and

         A94: (dx . a) = ((a1 `1 ) - (a2 `1 )) by A25;

        a2 in W2 by A91, A93, ZFMISC_1: 87;

        then

        consider x2,y2 be Real such that

         A95: a2 = |[x2, y2]| and

         A96: ((p2 `1 ) - (g / 2)) < x2 and

         A97: x2 < ((p2 `1 ) + (g / 2));

        

         A98: (a2 `1 ) = x2 by A95, EUCLID: 52;

        ((p2 `1 ) - x2) > ((p2 `1 ) - ((p2 `1 ) + (g / 2))) by A97, XREAL_1: 15;

        then

         A99: ((p2 `1 ) - x2) > ( - (g / 2));

        (((p2 `1 ) - (g / 2)) + (g / 2)) < (x2 + (g / 2)) by A96, XREAL_1: 6;

        then ((p2 `1 ) - x2) < ((x2 + (g / 2)) - x2) by XREAL_1: 9;

        then

         A100: |.((p2 `1 ) - x2).| < (g / 2) by A99, SEQ_2: 1;

        a1 in W1 by A91, A93, ZFMISC_1: 87;

        then

        consider x1,y1 be Real such that

         A101: a1 = |[x1, y1]| and

         A102: ((p1 `1 ) - (g / 2)) < x1 and

         A103: x1 < ((p1 `1 ) + (g / 2));

        ((p1 `1 ) - x1) > ((p1 `1 ) - ((p1 `1 ) + (g / 2))) by A103, XREAL_1: 15;

        then

         A104: ((p1 `1 ) - x1) > ( - (g / 2));

         |.(((p1 `1 ) - x1) - ((p2 `1 ) - x2)).| <= ( |.((p1 `1 ) - x1).| + |.((p2 `1 ) - x2).|) by COMPLEX1: 57;

        then

         A105: |.( - (((p1 `1 ) - x1) - ((p2 `1 ) - x2))).| <= ( |.((p1 `1 ) - x1).| + |.((p2 `1 ) - x2).|) by COMPLEX1: 52;

        (((p1 `1 ) - (g / 2)) + (g / 2)) < (x1 + (g / 2)) by A102, XREAL_1: 6;

        then ((p1 `1 ) - x1) < ((x1 + (g / 2)) - x1) by XREAL_1: 9;

        then |.((p1 `1 ) - x1).| < (g / 2) by A104, SEQ_2: 1;

        then ( |.((p1 `1 ) - x1).| + |.((p2 `1 ) - x2).|) < ((g / 2) + (g / 2)) by A100, XREAL_1: 8;

        then

         A106: |.((x1 - x2) - r).| < g by A105, XXREAL_0: 2;

        (a1 `1 ) = x1 by A101, EUCLID: 52;

        then ((a1 `1 ) - (a2 `1 )) in ].(r - g), (r + g).[ by A98, A106, RCOMP_1: 1;

        hence thesis by A85, A92, A94;

      end;

      then Dx is continuous by JGRAPH_2: 10;

      then

      reconsider dx as continuous RealMap of [:T2, T2:] by JORDAN5A: 27;

      set Zdy = (dy | OK);

      set Zdx = (dx | OK);

      set m = ((Zdx (#) Zdx) + (Zdy (#) Zdy));

      for p be Point of [:T2, T2:], V be Subset of R^1 st (fY2 . p) in V & V is open holds ex W be Subset of [:T2, T2:] st p in W & W is open & (fY2 .: W) c= V

      proof

        let p be Point of [:T2, T2:], V be Subset of R^1 such that

         A107: (fY2 . p) in V and

         A108: V is open;

        reconsider V1 = V as open Subset of REAL by A108, BORSUK_5: 39, TOPMETR: 17;

        consider p1,p2 be Point of T2 such that

         A109: p = [p1, p2] and

         A110: (fY2 . p) = (p2 `2 ) by A22;

        consider g be Real such that

         A111: 0 < g and

         A112: ].((p2 `2 ) - g), ((p2 `2 ) + g).[ c= V1 by A107, A110, RCOMP_1: 19;

        reconsider g as Element of REAL by XREAL_0:def 1;

        set W1 = { |[x, y]| where x,y be Real : ((p2 `2 ) - g) < y & y < ((p2 `2 ) + g) };

        W1 c= the carrier of T2

        proof

          let a be object;

          assume a in W1;

          then ex x,y be Real st a = |[x, y]| & ((p2 `2 ) - g) < y & y < ((p2 `2 ) + g);

          hence thesis;

        end;

        then

        reconsider W1 as Subset of T2;

        take [:( [#] T2), W1:];

        

         A113: p2 = |[(p2 `1 ), (p2 `2 )]| by EUCLID: 53;

        ((p2 `2 ) - g) < ((p2 `2 ) - 0 ) & ((p2 `2 ) + 0 qua Nat) < ((p2 `2 ) + g) by A111, XREAL_1: 6, XREAL_1: 15;

        then p2 in W1 by A113;

        hence p in [:( [#] T2), W1:] by A109, ZFMISC_1:def 2;

        W1 is open by PSCOMP_1: 21;

        hence [:( [#] T2), W1:] is open by BORSUK_1: 6;

        let b be object;

        assume b in (fY2 .: [:( [#] T2), W1:]);

        then

        consider a be Point of [:T2, T2:] such that

         A114: a in [:( [#] T2), W1:] and

         A115: (fY2 . a) = b by FUNCT_2: 65;

        consider a1,a2 be Point of T2 such that

         A116: a = [a1, a2] and

         A117: (fY2 . a) = (a2 `2 ) by A22;

        a2 in W1 by A114, A116, ZFMISC_1: 87;

        then

        consider x1,y1 be Real such that

         A118: a2 = |[x1, y1]| and

         A119: ((p2 `2 ) - g) < y1 and

         A120: y1 < ((p2 `2 ) + g);

        ((p2 `2 ) - y1) > ((p2 `2 ) - ((p2 `2 ) + g)) by A120, XREAL_1: 15;

        then

         A121: ((p2 `2 ) - y1) > ( - g);

        (((p2 `2 ) - g) + g) < (y1 + g) by A119, XREAL_1: 6;

        then ((p2 `2 ) - y1) < ((y1 + g) - y1) by XREAL_1: 9;

        then |.((p2 `2 ) - y1).| < g by A121, SEQ_2: 1;

        then |.( - ((p2 `2 ) - y1)).| < g by COMPLEX1: 52;

        then

         A122: |.(y1 - (p2 `2 )).| < g;

        (a2 `2 ) = y1 by A118, EUCLID: 52;

        then (a2 `2 ) in ].((p2 `2 ) - g), ((p2 `2 ) + g).[ by A122, RCOMP_1: 1;

        hence thesis by A112, A115, A117;

      end;

      then fY2 is continuous by JGRAPH_2: 10;

      then

      reconsider fy2 as continuous RealMap of [:T2, T2:] by JORDAN5A: 27;

      for p be Point of [:T2, T2:], V be Subset of R^1 st (fX2 . p) in V & V is open holds ex W be Subset of [:T2, T2:] st p in W & W is open & (fX2 .: W) c= V

      proof

        let p be Point of [:T2, T2:], V be Subset of R^1 such that

         A123: (fX2 . p) in V and

         A124: V is open;

        reconsider V1 = V as open Subset of REAL by A124, BORSUK_5: 39, TOPMETR: 17;

        consider p1,p2 be Point of T2 such that

         A125: p = [p1, p2] and

         A126: (fX2 . p) = (p2 `1 ) by A6;

        consider g be Real such that

         A127: 0 < g and

         A128: ].((p2 `1 ) - g), ((p2 `1 ) + g).[ c= V1 by A123, A126, RCOMP_1: 19;

        reconsider g as Element of REAL by XREAL_0:def 1;

        set W1 = { |[x, y]| where x,y be Real : ((p2 `1 ) - g) < x & x < ((p2 `1 ) + g) };

        W1 c= the carrier of T2

        proof

          let a be object;

          assume a in W1;

          then ex x,y be Real st a = |[x, y]| & ((p2 `1 ) - g) < x & x < ((p2 `1 ) + g);

          hence thesis;

        end;

        then

        reconsider W1 as Subset of T2;

        take [:( [#] T2), W1:];

        

         A129: p2 = |[(p2 `1 ), (p2 `2 )]| by EUCLID: 53;

        ((p2 `1 ) - g) < ((p2 `1 ) - 0 ) & ((p2 `1 ) + 0 qua Nat) < ((p2 `1 ) + g) by A127, XREAL_1: 6, XREAL_1: 15;

        then p2 in W1 by A129;

        hence p in [:( [#] T2), W1:] by A125, ZFMISC_1:def 2;

        W1 is open by PSCOMP_1: 19;

        hence [:( [#] T2), W1:] is open by BORSUK_1: 6;

        let b be object;

        assume b in (fX2 .: [:( [#] T2), W1:]);

        then

        consider a be Point of [:T2, T2:] such that

         A130: a in [:( [#] T2), W1:] and

         A131: (fX2 . a) = b by FUNCT_2: 65;

        consider a1,a2 be Point of T2 such that

         A132: a = [a1, a2] and

         A133: (fX2 . a) = (a2 `1 ) by A6;

        a2 in W1 by A130, A132, ZFMISC_1: 87;

        then

        consider x1,y1 be Real such that

         A134: a2 = |[x1, y1]| and

         A135: ((p2 `1 ) - g) < x1 and

         A136: x1 < ((p2 `1 ) + g);

        ((p2 `1 ) - x1) > ((p2 `1 ) - ((p2 `1 ) + g)) by A136, XREAL_1: 15;

        then

         A137: ((p2 `1 ) - x1) > ( - g);

        (((p2 `1 ) - g) + g) < (x1 + g) by A135, XREAL_1: 6;

        then ((p2 `1 ) - x1) < ((x1 + g) - x1) by XREAL_1: 9;

        then |.((p2 `1 ) - x1).| < g by A137, SEQ_2: 1;

        then |.( - ((p2 `1 ) - x1)).| < g by COMPLEX1: 52;

        then

         A138: |.(x1 - (p2 `1 )).| < g;

        (a2 `1 ) = x1 by A134, EUCLID: 52;

        then (a2 `1 ) in ].((p2 `1 ) - g), ((p2 `1 ) + g).[ by A138, RCOMP_1: 1;

        hence thesis by A128, A131, A133;

      end;

      then fX2 is continuous by JGRAPH_2: 10;

      then

      reconsider fx2 as continuous RealMap of [:T2, T2:] by JORDAN5A: 27;

      set yy = (Zyo (#) Zdy);

      set xx = (Zxo (#) Zdx);

      set Zfy2 = (fy2 | OK);

      set Zfx2 = (fx2 | OK);

      set p1 = ((xx + yy) (#) (xx + yy));

      

       A139: ( dom p2) = the carrier of TD by FUNCT_2:def 1;

      

       A140: for y,z be Point of D2 st y <> z holds [y, z] in OK

      proof

        let y,z be Point of D2;

        

         A141: y is Point of T2 & z is Point of T2 by PRE_TOPC: 25;

        assume y <> z;

        then [y, z] in ( DiffElems (T2,T2)) by A141;

        hence thesis by XBOOLE_0:def 4;

      end;

       A142:

      now

        let b be Real;

        assume b in ( rng p2);

        then

        consider a be object such that

         A143: a in ( dom p2) and

         A144: (p2 . a) = b by FUNCT_1:def 3;

        a in ( DiffElems (T2,T2)) by A143, XBOOLE_0:def 4;

        then

        consider y,z be Point of T2 such that

         A145: a = [y, z] and

         A146: y <> z;

        a in the carrier of [:D2, D2:] by A143, XBOOLE_0:def 4;

        then

        consider a1,a2 be Point of D2 such that

         A147: a = [a1, a2] by BORSUK_1: 10;

        

         A148: a2 = z by A145, A147, XTUPLE_0: 1;

        

         A149: a1 = y by A145, A147, XTUPLE_0: 1;

        then

         A150: (Zf1 . [y, z]) = (f1 . [y, z]) by A140, A146, A148, FUNCT_1: 49;

        set r3 = ((z `1 ) - (o `1 )), r4 = ((z `2 ) - (o `2 ));

        consider x9,x10 be Point of T2 such that

         A151: [y, z] = [x9, x10] and

         A152: (xo . [y, z]) = ((x10 `1 ) - (o `1 )) by A3;

        

         A153: z = x10 by A151, XTUPLE_0: 1;

        the carrier of D2 = ( cl_Ball (o,r)) by Th3;

        then |.(z - o).| <= r by A148, TOPREAL9: 8;

        then

         A154: ( |.(z - o).| ^2 ) <= (r ^2 ) by SQUARE_1: 15;

        consider x11,x12 be Point of T2 such that

         A155: [y, z] = [x11, x12] and

         A156: (yo . [y, z]) = ((x12 `2 ) - (o `2 )) by A9;

        

         A157: z = x12 by A155, XTUPLE_0: 1;

        

         A158: (Zxo . [y, z]) = (xo . [y, z]) & (Zyo . [y, z]) = (yo . [y, z]) by A140, A146, A149, A148, FUNCT_1: 49;

        ( |.(z - o).| ^2 ) = ((((z - o) `1 ) ^2 ) + (((z - o) `2 ) ^2 )) by JGRAPH_1: 29

        .= ((r3 ^2 ) + (((z - o) `2 ) ^2 )) by TOPREAL3: 3

        .= ((r3 ^2 ) + (r4 ^2 )) by TOPREAL3: 3;

        then

         A159: (((r3 ^2 ) + (r4 ^2 )) - (r ^2 )) <= ((r ^2 ) - (r ^2 )) by A154, XREAL_1: 9;

        

         A160: [y, z] is Element of ( [#] TD) by A143, A145, PRE_TOPC:def 5;

        (p2 . [y, z]) = ((((Zxo (#) Zxo) + (Zyo (#) Zyo)) . [y, z]) - (Zf1 . [y, z])) by A143, A145, VALUED_1: 13

        .= ((((Zxo (#) Zxo) + (Zyo (#) Zyo)) . [y, z]) - (r ^2 )) by A150, FUNCOP_1: 7

        .= ((((Zxo (#) Zxo) . [y, z]) + ((Zyo (#) Zyo) . [y, z])) - (r ^2 )) by A160, VALUED_1: 1

        .= ((((Zxo . [y, z]) * (Zxo . [y, z])) + ((Zyo (#) Zyo) . [y, z])) - (r ^2 )) by VALUED_1: 5

        .= (((r3 ^2 ) + (r4 ^2 )) - (r ^2 )) by A158, A152, A153, A156, A157, VALUED_1: 5;

        hence 0 >= b by A144, A145, A159;

      end;

      now

        let b be Real;

        assume b in ( rng m);

        then

        consider a be object such that

         A161: a in ( dom m) and

         A162: (m . a) = b by FUNCT_1:def 3;

        a in ( DiffElems (T2,T2)) by A161, XBOOLE_0:def 4;

        then

        consider y,z be Point of T2 such that

         A163: a = [y, z] and

         A164: y <> z;

        a in the carrier of [:D2, D2:] by A161, XBOOLE_0:def 4;

        then

        consider a1,a2 be Point of D2 such that

         A165: a = [a1, a2] by BORSUK_1: 10;

        set r1 = ((y `1 ) - (z `1 )), r2 = ((y `2 ) - (z `2 ));

         A166:

        now

          assume ((r1 ^2 ) + (r2 ^2 )) = 0 ;

          then r1 = 0 & r2 = 0 by COMPLEX1: 1;

          hence contradiction by A164, TOPREAL3: 6;

        end;

        consider x3,x4 be Point of T2 such that

         A167: [y, z] = [x3, x4] and

         A168: (dx . [y, z]) = ((x3 `1 ) - (x4 `1 )) by A25;

        

         A169: y = x3 & z = x4 by A167, XTUPLE_0: 1;

        a1 = y & a2 = z by A163, A165, XTUPLE_0: 1;

        then

         A170: (Zdx . [y, z]) = (dx . [y, z]) & (Zdy . [y, z]) = (dy . [y, z]) by A140, A164, FUNCT_1: 49;

        consider x5,x6 be Point of T2 such that

         A171: [y, z] = [x5, x6] and

         A172: (dy . [y, z]) = ((x5 `2 ) - (x6 `2 )) by A19;

        

         A173: y = x5 & z = x6 by A171, XTUPLE_0: 1;

        

         A174: [y, z] is Element of ( [#] TD) by A161, A163, PRE_TOPC:def 5;

        (m . [y, z]) = (((Zdx (#) Zdx) . [y, z]) + ((Zdy (#) Zdy) . [y, z])) by A174, VALUED_1: 1

        .= (((Zdx . [y, z]) * (Zdx . [y, z])) + ((Zdy (#) Zdy) . [y, z])) by VALUED_1: 5

        .= ((r1 ^2 ) + (r2 ^2 )) by A168, A169, A172, A173, A170, VALUED_1: 5;

        hence 0 < b by A162, A163, A166;

      end;

      then

      reconsider m as positive-yielding continuous RealMap of TD by PARTFUN3:def 1;

      reconsider p2 as nonpositive-yielding continuous RealMap of TD by A142, PARTFUN3:def 3;

      set pp = (p1 - (m (#) p2));

      set k = ((( - (xx + yy)) + ( sqrt pp)) / m);

      set x3 = (Zfx2 + (k (#) Zdx));

      set y3 = (Zfy2 + (k (#) Zdy));

      reconsider X3 = x3, Y3 = y3 as Function of TD, R^1 by TOPMETR: 17;

      set F = <:X3, Y3:>;

      

       A175: for x be Point of D2 holds (g . x) = ((R * F) . [x, (f . x)])

      proof

        

         A176: ( dom pp) = the carrier of TD by FUNCT_2:def 1;

        let x be Point of D2;

        

         A177: ( dom X3) = the carrier of TD & ( dom Y3) = the carrier of TD by FUNCT_2:def 1;

        

         A178: not x is_a_fixpoint_of f by A16;

        then

         A179: x <> (f . x);

        consider y,z be Point of T2 such that

         A180: y = x & z = (f . x) and

         A181: ( HC (x,f)) = ( HC (z,y,o,r)) by A178, Def4;

        

         A182: (Zf1 . [y, z]) = (f1 . [y, z]) by A140, A180, A179, FUNCT_1: 49;

        

         A183: (Zxo . [y, z]) = (xo . [y, z]) & (Zyo . [y, z]) = (yo . [y, z]) by A140, A180, A179, FUNCT_1: 49;

        set r1 = ((y `1 ) - (z `1 )), r2 = ((y `2 ) - (z `2 )), r3 = ((z `1 ) - (o `1 )), r4 = ((z `2 ) - (o `2 ));

        consider x9,x10 be Point of T2 such that

         A184: [y, z] = [x9, x10] and

         A185: (xo . [y, z]) = ((x10 `1 ) - (o `1 )) by A3;

        

         A186: z = x10 by A184, XTUPLE_0: 1;

        consider x11,x12 be Point of T2 such that

         A187: [y, z] = [x11, x12] and

         A188: (yo . [y, z]) = ((x12 `2 ) - (o `2 )) by A9;

        

         A189: z = x12 by A187, XTUPLE_0: 1;

         [x, (f . x)] in ( DiffElems (T2,T2)) by A180, A179;

        then

         A190: [y, z] in OK by A180, XBOOLE_0:def 4;

        

        then

         A191: (p2 . [y, z]) = ((((Zxo (#) Zxo) + (Zyo (#) Zyo)) . [y, z]) - (Zf1 . [y, z])) by A52, A139, VALUED_1: 13

        .= ((((Zxo (#) Zxo) + (Zyo (#) Zyo)) . [y, z]) - (r ^2 )) by A182, FUNCOP_1: 7

        .= ((((Zxo (#) Zxo) . [y, z]) + ((Zyo (#) Zyo) . [y, z])) - (r ^2 )) by A52, A190, VALUED_1: 1

        .= ((((Zxo . [y, z]) * (Zxo . [y, z])) + ((Zyo (#) Zyo) . [y, z])) - (r ^2 )) by VALUED_1: 5

        .= (((r3 ^2 ) + (r4 ^2 )) - (r ^2 )) by A185, A186, A188, A189, A183, VALUED_1: 5;

        

         A192: (Zdx . [y, z]) = (dx . [y, z]) by A140, A180, A179, FUNCT_1: 49;

        consider x7,x8 be Point of T2 such that

         A193: [y, z] = [x7, x8] and

         A194: (fy2 . [y, z]) = (x8 `2 ) by A22;

        

         A195: z = x8 by A193, XTUPLE_0: 1;

        consider x1,x2 be Point of T2 such that

         A196: [y, z] = [x1, x2] and

         A197: (fx2 . [y, z]) = (x2 `1 ) by A6;

        

         A198: z = x2 by A196, XTUPLE_0: 1;

        consider x3,x4 be Point of T2 such that

         A199: [y, z] = [x3, x4] and

         A200: (dx . [y, z]) = ((x3 `1 ) - (x4 `1 )) by A25;

        

         A201: y = x3 & z = x4 by A199, XTUPLE_0: 1;

        set l = ((( - ((r3 * r1) + (r4 * r2))) + ( sqrt ((((r3 * r1) + (r4 * r2)) ^2 ) - (((r1 ^2 ) + (r2 ^2 )) * (((r3 ^2 ) + (r4 ^2 )) - (r ^2 )))))) / ((r1 ^2 ) + (r2 ^2 )));

        

         A202: (xx . [y, z]) = ((Zxo . [y, z]) * (Zdx . [y, z])) & (yy . [y, z]) = ((Zyo . [y, z]) * (Zdy . [y, z])) by VALUED_1: 5;

        

         A203: (Zdy . [y, z]) = (dy . [y, z]) by A140, A180, A179, FUNCT_1: 49;

        consider x5,x6 be Point of T2 such that

         A204: [y, z] = [x5, x6] and

         A205: (dy . [y, z]) = ((x5 `2 ) - (x6 `2 )) by A19;

        

         A206: y = x5 & z = x6 by A204, XTUPLE_0: 1;

        

         A207: (m . [y, z]) = (((Zdx (#) Zdx) . [y, z]) + ((Zdy (#) Zdy) . [y, z])) by A52, A190, VALUED_1: 1

        .= (((Zdx . [y, z]) * (Zdx . [y, z])) + ((Zdy (#) Zdy) . [y, z])) by VALUED_1: 5

        .= ((r1 ^2 ) + (r2 ^2 )) by A200, A201, A205, A206, A192, A203, VALUED_1: 5;

        

         A208: ((xx + yy) . [y, z]) = ((xx . [y, z]) + (yy . [y, z])) by A52, A190, VALUED_1: 1;

        then

         A209: (p1 . [y, z]) = (((r3 * r1) + (r4 * r2)) ^2 ) by A200, A201, A205, A206, A185, A186, A188, A189, A192, A203, A183, A202, VALUED_1: 5;

        ( dom ( sqrt pp)) = the carrier of TD by FUNCT_2:def 1;

        

        then

         A210: (( sqrt pp) . [y, z]) = ( sqrt (pp . [y, z])) by A52, A190, PARTFUN3:def 5

        .= ( sqrt ((p1 . [y, z]) - ((m (#) p2) . [y, z]))) by A52, A190, A176, VALUED_1: 13

        .= ( sqrt ((((r3 * r1) + (r4 * r2)) ^2 ) - (((r1 ^2 ) + (r2 ^2 )) * (((r3 ^2 ) + (r4 ^2 )) - (r ^2 ))))) by A207, A209, A191, VALUED_1: 5;

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

        

        then

         A211: (k . [y, z]) = (((( - (xx + yy)) + ( sqrt pp)) . [y, z]) * ((m . [y, z]) " )) by A52, A190, RFUNCT_1:def 1

        .= (((( - (xx + yy)) + ( sqrt pp)) . [y, z]) / (m . [y, z])) by XCMPLX_0:def 9

        .= (((( - (xx + yy)) . [y, z]) + (( sqrt pp) . [y, z])) / ((r1 ^2 ) + (r2 ^2 ))) by A52, A190, A207, VALUED_1: 1

        .= l by A200, A201, A205, A206, A185, A186, A188, A189, A192, A203, A183, A202, A208, A210, VALUED_1: 8;

        

         A212: (Y3 . [y, z]) = ((Zfy2 . [y, z]) + ((k (#) Zdy) . [y, z])) by A52, A190, VALUED_1: 1

        .= ((z `2 ) + ((k (#) Zdy) . [y, z])) by A140, A180, A179, A194, A195, FUNCT_1: 49

        .= ((z `2 ) + (l * r2)) by A205, A206, A203, A211, VALUED_1: 5;

        

         A213: (X3 . [y, z]) = ((Zfx2 . [y, z]) + ((k (#) Zdx) . [y, z])) by A52, A190, VALUED_1: 1

        .= ((z `1 ) + ((k (#) Zdx) . [y, z])) by A140, A180, A179, A197, A198, FUNCT_1: 49

        .= ((z `1 ) + (l * r1)) by A200, A201, A192, A211, VALUED_1: 5;

        

        thus (g . x) = ( HC (x,f)) by Def5

        .= |[((z `1 ) + (l * r1)), ((z `2 ) + (l * r2))]| by A180, A181, A179, Th8

        .= (R . [(X3 . [y, z]), (Y3 . [y, z])]) by A213, A212, TOPREALA:def 2

        .= (R . (F . [y, z])) by A52, A190, A177, FUNCT_3: 49

        .= ((R * F) . [x, (f . x)]) by A52, A180, A190, FUNCT_2: 15;

      end;

      X3 is continuous & Y3 is continuous by JORDAN5A: 27;

      then

      reconsider F as continuous Function of TD, [: R^1 , R^1 :] by YELLOW12: 41;

      for p be Point of D2, V be Subset of S1 st (g . p) in V & V is open holds ex W be Subset of D2 st p in W & W is open & (g .: W) c= V

      proof

        let p be Point of D2, V be Subset of S1 such that

         A214: (g . p) in V and

         A215: V is open;

        consider V1 be Subset of T2 such that

         A216: V1 is open and

         A217: (V1 /\ ( [#] S1)) = V by A215, TOPS_2: 24;

        reconsider p1 = p, fp = (f . p) as Point of T2 by PRE_TOPC: 25;

        

         A218: ( rng R) = ( [#] T2) by TOPREALA: 34, TOPS_2:def 5;

        (R " ) is being_homeomorphism by TOPREALA: 34, TOPS_2: 56;

        then

         A219: ((R " ) .: V1) is open by A216, TOPGRP_1: 25;

         not p is_a_fixpoint_of f by A16;

        then p <> (f . p);

        then [p1, fp] in ( DiffElems (T2,T2));

        then

         A220: [p, (f . p)] in OK by XBOOLE_0:def 4;

        (g . p) = ((R * F) . [p, (f . p)]) by A175;

        then ((R * F) . [p1, fp]) in V1 by A214, A217, XBOOLE_0:def 4;

        then

         A221: ((R " ) . ((R * F) . [p1, fp])) in ((R " ) .: V1) by FUNCT_2: 35;

        

         A222: R is one-to-one by TOPREALA: 34, TOPS_2:def 5;

        

         A223: ( dom R) = the carrier of [: R^1 , R^1 :] by FUNCT_2:def 1;

        then

         A224: ( rng F) c= ( dom R);

        then ( dom F) = the carrier of ( [:T2, T2:] | OK) & ( dom (R * F)) = ( dom F) by FUNCT_2:def 1, RELAT_1: 27;

        then

         A225: (((R " ) * (R * F)) . [p1, fp]) in ((R " ) .: V1) by A52, A220, A221, FUNCT_1: 13;

        

         A226: for x be object st x in ( dom F) holds ((( id ( dom R)) * F) . x) = (F . x)

        proof

          let x be object such that

           A227: x in ( dom F);

          

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

          

          thus ((( id ( dom R)) * F) . x) = (( id ( dom R)) . (F . x)) by A227, FUNCT_1: 13

          .= (F . x) by A223, A228, FUNCT_1: 18;

        end;

        ( dom ( id ( dom R))) = ( dom R);

        then ( dom (( id ( dom R)) * F)) = ( dom F) by A224, RELAT_1: 27;

        then

         A229: (( id ( dom R)) * F) = F by A226, FUNCT_1: 2;

        ((R " ) * (R * F)) = (((R " ) * R) * F) by RELAT_1: 36

        .= (( id ( dom R)) * F) by A218, A222, TOPS_2: 52;

        then

        consider W be Subset of TD such that

         A230: [p1, fp] in W and

         A231: W is open and

         A232: (F .: W) c= ((R " ) .: V1) by A52, A220, A219, A229, A225, JGRAPH_2: 10;

        consider WW be Subset of [:T2, T2:] such that

         A233: WW is open and

         A234: (WW /\ ( [#] TD)) = W by A231, TOPS_2: 24;

        consider SF be Subset-Family of [:T2, T2:] such that

         A235: WW = ( union SF) and

         A236: for e be set st e in SF holds ex X1 be Subset of T2, Y1 be Subset of T2 st e = [:X1, Y1:] & X1 is open & Y1 is open by A233, BORSUK_1: 5;

         [p1, fp] in WW by A230, A234, XBOOLE_0:def 4;

        then

        consider Z be set such that

         A237: [p1, fp] in Z and

         A238: Z in SF by A235, TARSKI:def 4;

        set ZZ = (Z /\ ( [#] TD));

        Z c= WW by A235, A238, ZFMISC_1: 74;

        then ZZ c= (WW /\ ( [#] TD)) by XBOOLE_1: 27;

        then

         A239: (F .: ZZ) c= (F .: W) by A234, RELAT_1: 123;

        consider X1,Y1 be Subset of T2 such that

         A240: Z = [:X1, Y1:] and

         A241: X1 is open & Y1 is open by A236, A238;

        reconsider XX = (X1 /\ ( [#] D2)), YY = (Y1 /\ ( [#] D2)) as open Subset of D2 by A241, TOPS_2: 24;

        fp in Y1 by A237, A240, ZFMISC_1: 87;

        then fp in YY by XBOOLE_0:def 4;

        then

        consider M be Subset of D2 such that

         A242: p in M and

         A243: M is open and

         A244: (f .: M) c= YY by JGRAPH_2: 10;

        take W1 = (XX /\ M);

        p in X1 by A237, A240, ZFMISC_1: 87;

        then p in XX by XBOOLE_0:def 4;

        hence p in W1 by A242, XBOOLE_0:def 4;

        thus W1 is open by A243;

        let b be object;

        assume b in (g .: W1);

        then

        consider a be Point of D2 such that

         A245: a in W1 and

         A246: b = (g . a) by FUNCT_2: 65;

        reconsider a1 = a, fa = (f . a) as Point of T2 by PRE_TOPC: 25;

        a in M by A245, XBOOLE_0:def 4;

        then fa in (f .: M) by FUNCT_2: 35;

        then

         A247: (f . a) in Y1 by A244, XBOOLE_0:def 4;

         not a is_a_fixpoint_of f by A16;

        then a <> (f . a);

        then [a1, fa] in ( DiffElems (T2,T2));

        then

         A248: [a, (f . a)] in OK by XBOOLE_0:def 4;

        a in XX by A245, XBOOLE_0:def 4;

        then a in X1 by XBOOLE_0:def 4;

        then [a, fa] in Z by A240, A247, ZFMISC_1:def 2;

        then [a, fa] in ZZ by A52, A248, XBOOLE_0:def 4;

        then (F . [a1, fa]) in (F .: ZZ) by FUNCT_2: 35;

        then (F . [a1, fa]) in (F .: W) by A239;

        then (R . (F . [a1, fa])) in (R .: ((R " ) .: V1)) by A232, FUNCT_2: 35;

        then

         A249: ((R * F) . [a1, fa]) in (R .: ((R " ) .: V1)) by A52, A248, FUNCT_2: 15;

        R is onto by A218, FUNCT_2:def 3;

        then (R qua Function " ) = (R " ) & ( dom (R " )) = ( [#] T2) by A218, A222, TOPS_2: 49, TOPS_2:def 4;

        then ((R * F) . [a1, fa]) in V1 by A222, A249, PARTFUN3: 1;

        then (g . a) in V1 by A175;

        hence thesis by A217, A246, XBOOLE_0:def 4;

      end;

      hence thesis by JGRAPH_2: 10;

    end;

    ::$Notion-Name

    theorem :: BROUWER:14

    

     Th14: for r be non negative Real, o be Point of ( TOP-REAL 2), f be continuous Function of ( Tdisk (o,r)), ( Tdisk (o,r)) holds f is with_fixpoint

    proof

      let r be non negative Real, o be Point of ( TOP-REAL 2), f be continuous Function of ( Tdisk (o,r)), ( Tdisk (o,r));

      

       A1: the carrier of ( Tcircle (o,r)) = ( Sphere (o,r)) by TOPREALB: 9;

      

       A2: the carrier of ( Tdisk (o,r)) = ( cl_Ball (o,r)) by Th3;

      per cases ;

        suppose r is positive;

        then

        reconsider r as positive Real;

        ( Sphere (o,r)) c= ( cl_Ball (o,r)) by TOPREAL9: 17;

        then

        reconsider Y = ( Tcircle (o,r)) as non empty SubSpace of ( Tdisk (o,r)) by A1, A2, TSEP_1: 4;

        reconsider g = ( BR-map f) as Function of ( Tdisk (o,r)), Y;

        

         A3: not Y is_a_retract_of ( Tdisk (o,r)) by Th10;

        assume

         A4: f is without_fixpoints;

        

         A5: g is being_a_retraction by A4, Th11;

        g is continuous by A4, Th13;

        hence contradiction by A3, A5;

      end;

        suppose r is non positive;

        then

        reconsider r as non negative non positive Real;

        take o;

        

         A6: ( cl_Ball (o,r)) = {o} by Th2;

        ( dom f) = the carrier of ( Tdisk (o,r)) by FUNCT_2:def 1;

        hence o in ( dom f) by A2, A6, TARSKI:def 1;

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

        hence thesis by A2, A6, TARSKI:def 1;

      end;

    end;

    ::$Notion-Name

    theorem :: BROUWER:15

    for r be non negative Real, o be Point of ( TOP-REAL 2), f be continuous Function of ( Tdisk (o,r)), ( Tdisk (o,r)) holds ex x be Point of ( Tdisk (o,r)) st (f . x) = x

    proof

      let r be non negative Real, o be Point of ( TOP-REAL 2), f be continuous Function of ( Tdisk (o,r)), ( Tdisk (o,r));

      f is with_fixpoint by Th14;

      then

      consider x be object such that

       A1: x is_a_fixpoint_of f;

      reconsider x as set by TARSKI: 1;

      take x;

      x in ( dom f) by A1;

      hence x is Point of ( Tdisk (o,r));

      thus (f . x) = x by A1;

    end;