:: Brouwer Fixed Point Theorem for Disks on the Plane
::  by Artur Korni{\l}owicz and Yasunari Shidama
::
:: Received February 22, 2005
:: Copyright (c) 2005-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, EUCLID, SUBSET_1, XREAL_0, ORDINAL1, PRE_TOPC, XBOOLE_0,
      ZFMISC_1, TARSKI, STRUCT_0, METRIC_1, CARD_1, COMPLEX1, ARYTM_1, RELAT_1,
      XXREAL_0, CONVEX1, TOPREALB, PROB_1, RVSUM_1, ARYTM_3, SQUARE_1, FUNCT_3,
      CARD_3, POLYEQ_1, REAL_1, SUPINF_2, MCART_1, FUNCT_1, ABIAN, BORSUK_1,
      ALGSTR_1, FUNCOP_1, BORSUK_2, ORDINAL2, TOPALG_1, EQREL_1, WAYBEL20,
      RCOMP_1, TOPREALA, PSCOMP_1, TOPMETR, XXREAL_1, VALUED_1, PARTFUN3,
      PARTFUN1, TOPS_2, SETFAM_1, BROUWER, FUNCT_2, NAT_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, EQREL_1, COMPLEX1,
      SQUARE_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCT_3,
      FUNCOP_1, PSCOMP_1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, RVSUM_1, RCOMP_1,
      VALUED_1, STRUCT_0, PRE_TOPC, BORSUK_1, TOPS_2, JORDAN1, QUIN_1,
      POLYEQ_1, BORSUK_2, TOPALG_1, TOPREAL9, TOPALG_2, TOPREALA, TOPREALB,
      PARTFUN3, ABIAN, XXREAL_0, RLVECT_1, EUCLID;
 constructors SQUARE_1, BINOP_2, COMPLEX1, QUIN_1, POLYEQ_1, ABIAN, MONOID_0,
      TOPALG_1, TOPREAL9, TOPREALA, TOPREALB, PARTFUN3, SEQ_1, BORSUK_6,
      CONVEX1, PSCOMP_1;
 registrations XBOOLE_0, SUBSET_1, FUNCT_1, FUNCT_2, NUMBERS, XXREAL_0,
      XREAL_0, SQUARE_1, NAT_1, MEMBERED, QUIN_1, RCOMP_1, STRUCT_0, PRE_TOPC,
      TOPS_1, BORSUK_1, TEX_1, MONOID_0, EUCLID, TOPMETR, PSCOMP_1, BORSUK_2,
      TOPALG_1, TOPALG_2, TOPREAL9, TOPREALB, PARTFUN3, TOPALG_5, VALUED_0,
      ZFMISC_1, RELSET_1, PARTFUN4, VALUED_1, RELAT_1;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
 definitions TARSKI, XBOOLE_0, BORSUK_1, BORSUK_2, TOPALG_2, PSCOMP_1, ABIAN,
      SQUARE_1, BINOP_1, STRUCT_0, RLVECT_1, TOPALG_1;
 theorems TOPRNS_1, XREAL_0, TARSKI, FUNCT_2, TSEP_1, RFUNCT_1, PRE_TOPC,
      EUCLID, RELAT_1, FUNCT_1, ABIAN, ZFMISC_1, JGRAPH_2, XBOOLE_1, XBOOLE_0,
      TOPS_2, BORSUK_1, TOPALG_1, EQREL_1, BORSUK_2, FUNCOP_1, TOPMETR,
      XCMPLX_0, SQUARE_1, XCMPLX_1, FUNCT_3, COMPLEX1, JGRAPH_1, QUIN_1,
      POLYEQ_1, TOPREAL3, TOPREAL9, TOPALG_2, TOPREALB, BORSUK_5, RCOMP_1,
      PSCOMP_1, TOPREALA, YELLOW12, TOPGRP_1, PARTFUN3, RVSUM_1, EUCLID_2,
      XREAL_1, SEQ_2, XXREAL_0, VALUED_1, XXREAL_1, SUBSET_1, JORDAN5A,
      XTUPLE_0;
 schemes FUNCT_2;

begin

set T2 = TOP-REAL 2;

reserve n for Element of NAT,
  a, r for real number,
  x for Point of TOP-REAL n;

definition
  let S, T be non empty TopSpace;
  func DiffElems(S,T) -> Subset of [:S,T:] equals
  {[s,t] where s is Point of S, t is Point of T: s <> t};
  coherence
  proof
    set A = {[s,t] where s is Point of S, t is Point of T: s <> t};
    A c= the carrier of [:S,T:]
    proof
      let a be set;
      assume a in A;
      then ex s being Point of S, t being Point of T st a = [s,t] & s <> t;
      hence thesis;
    end;
    hence thesis;
  end;
end;

theorem
  for S, T being non empty TopSpace, x being set holds x in DiffElems(S,
  T) iff ex s being Point of S, t being 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 being 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 being 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 Th2:
  cl_Ball(x,0) = {x}
proof
  thus cl_Ball(x,0) c= {x}
  proof
    let a be set;
    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 set;
  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 Element of NAT, x be Point of TOP-REAL n, r be real number;
  func Tdisk(x,r) -> SubSpace of TOP-REAL n equals
  (TOP-REAL n) | cl_Ball(x,r);
  coherence;
end;

registration
  let n be Element of NAT, x be Point of TOP-REAL n;
  let r be non negative real number;
  cluster Tdisk(x,r) -> non empty;
  coherence;
end;

theorem 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 number;
  cluster Tdisk(x,r) -> convex;
  coherence
  proof
    thus [#]Tdisk(x,r) is convex Subset of TOP-REAL n by Th3;
  end;
end;

reserve n for Element of NAT,
  r for non negative real number,
  s, t, x for Point of TOP-REAL n;

theorem Th4:
  s <> t & s is Point of Tdisk(x,r) & s is not Point of Tcircle(x,r
) implies ex e being 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: s is not 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 being 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 Th5:
  s <> t & s in the carrier of Tcircle(x,r) & t is Point of Tdisk(x
,r) implies ex e being 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 being 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 empty Element of NAT, o be Point of TOP-REAL n, s, t be Point
  of TOP-REAL n, r be non negative real number;
  assume that
A1: s is Point of Tdisk(o,r) and
A2: t is Point of Tdisk(o,r) and
A3: s <> t;
  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 being 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:   s is not Point of Tcircle(o,r);
      then consider e1 being 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 being 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
      s is not Point of Tcircle(o,r);
      then consider e being 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 empty Element of NAT,
  s, t, o for Point of TOP-REAL n;

theorem 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
  for S, T, O being 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 being real number 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 EUCLID:50
    .= |. s - l*s + l*t - o .| by EUCLID:29
    .= |. s - (l*s - l*t) - o .| by EUCLID:47
    .= |. s +- (l*s - l*t) +- o .|
    .= |. s+-o +- (l*s - l*t) .| by EUCLID:26
    .= |. s-o - (l*s - l*t) .|
    .= |. s-o +- l*(s-t) .| by EUCLID:49
    .= |. s-o + l*(-(s-t)) .| by EUCLID:40
    .= |. s-o + l*(t-s) .| by EUCLID:44;
  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 number;
    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,EUCLID:50
    .= s -l*s + l*t by EUCLID:29
    .= s+l*t-l*s by EUCLID:26
    .= s+(l*t-l*s) by EUCLID:45
    .= s+l*(t-s) by EUCLID:49;
  l is Real by XREAL_0:def 1;
  then
A24: |. l*(t-s) .|^2 = (abs(l)*|. t-s .|)^2 by TOPRNS_1:7
    .= (abs(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,EUCLID:29
          .= s by EUCLID:27;
        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,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 Th8:
  for r1, r2, s1, s2 being real number, s, t, o being 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 number, 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 being real number holds Polynom(A,B,C,x) = Quard(A,l1,l2,x)
  proof
    let x be real number;
    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 being real number 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,EUCLID:50
    .= s -l*s + l*t by EUCLID:29
    .= s+l*t-l*s by EUCLID:26
    .= s+(l*t-l*s) by EUCLID:45
    .= s+l*(t-s) by EUCLID:49;
  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,EUCLID:29
          .= s by EUCLID:27;
        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,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 empty Element of NAT, o be Point of TOP-REAL n, r be non
  negative real number;
  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;
  func HC(x,f) -> Point of Tcircle(o,r) means
  :Def4:
  ex y, z being 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,ABIAN:def 4;
    then reconsider a = HC(z,y,o,r) as Point of Tcircle(o,r) by Th6;
    take a;
    thus thesis;
  end;
  uniqueness;
end;

theorem Th9:
  for x being Point of Tdisk(o,r), f being 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,ABIAN:def 4;
A4: the carrier of Tcircle(o,r) = Sphere(o,r) by TOPREALB:9;
  consider y, z being 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 Th10:
  for r being positive real number, o being Point of TOP-REAL 2,
  Y being 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 number, 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,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 being 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 set;
      assume x in the carrier of pi_1(Y,y0);
      then consider f0 being 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 being Function of [:I[01],I[01]:], X such that
A7:   f is continuous and
A8:   for s being Point of I[01] holds f.(s,0) = g0.s & f.(s,1) = C.s
& for t being Point of I[01] holds f.(0,t) = x0 & f.(1,t) = x0 by
BORSUK_2:def 7;
      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,BORSUK_1:def 16;
        thus F.(s,1) = F. [s,a1] .= R.(f.(s,1)) by FUNCT_2:15
          .= R.(C.s) by A8
          .= D.s by A5,BORSUK_1:def 16;
        thus F.(0,s) = F. [a0,s] .= R.(f.(0,s)) by FUNCT_2:15
          .= R.x0 by A8
          .= y0 by A5,BORSUK_1:def 16;
        thus F.(1,s) = F. [a1,s] .= R.(f.(1,s)) by FUNCT_2:15
          .= R.x0 by A8
          .= y0 by A5,BORSUK_1:def 16;
      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 set;
    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 empty Element of NAT;
  let r be non negative real number;
  let o be Point of TOP-REAL n;
  let f be Function of Tdisk(o,r), Tdisk(o,r);
  func BR-map(f) -> Function of Tdisk(o,r), Tcircle(o,r) means
  :Def5:
  for x being 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 being Point of Tdisk(o,r) ex m being Point of Tcircle(o,r) st P[
    x,m];
    ex h being Function of Tdisk(o,r), Tcircle(o,r) st for x being 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 being Point of Tdisk(o,r) holds f1.x = HC(x,f) and
A3: for x being Point of Tdisk(o,r) holds f2.x = HC(x,f);
    for x being 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 Th11:
  for o being Point of TOP-REAL n, x being Point of Tdisk(o,r), f
  being 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
  for f being 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 being set st x in dom (g|C) holds (g|C).x = (id Tcircle(o,r)).x
  proof
    let x be set 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,ABIAN:def 5;
    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) by RELAT_1:45;
  hence thesis by A2,A3,A4,FUNCT_1:2;
end;

Lm1: now
  let T be non empty TopSpace;
  let a be 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,XBOOLE_0:def 7
        .= {}T;
      hence thesis;
    end;
  end;
end;

theorem Th13:
  for r being positive real number, o being Point of TOP-REAL 2,
  f being 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 being Point of T2 st $1 = [x1,x2] & $2
  = x2`1;
  defpred dx[set,set] means ex x1, x2 being Point of T2 st $1 = [x1,x2] & $2 =
  x1`1 - x2`1;
  let r be positive real number, o be Point of TOP-REAL 2;
  defpred xo[set,set] means ex x1, x2 being Point of T2 st $1 = [x1,x2] & $2 =
  x2`1 - o`1;
  defpred yo[set,set] means ex x1, x2 being Point of T2 st $1 = [x1,x2] & $2 =
  x2`2 - o`2;
  reconsider rr = r^2 as Real by XREAL_0:def 1;
  set f1 = (the carrier of [:T2,T2:]) --> rr;
A1: for x being Element of [:T2,T2:] ex r being Real st xo[x,r]
  proof
    let x be Element of [:T2,T2:];
    consider x1, x2 being Point of T2 such that
A2: x = [x1,x2] by BORSUK_1:10;
    take x2`1 - o`1, x1, x2;
    thus thesis by A2;
  end;
  consider xo being RealMap of [:T2,T2:] such that
A3: for x being Point of [:T2,T2:] holds xo[x,xo.x] from FUNCT_2:sch 3(
  A1);
A4: for x being Element of [:T2,T2:] ex r being Real st fx2[x,r]
  proof
    let x be Element of [:T2,T2:];
    consider x1, x2 being Point of T2 such that
A5: x = [x1,x2] by BORSUK_1:10;
    take x2`1, x1, x2;
    thus thesis by A5;
  end;
  consider fx2 being RealMap of [:T2,T2:] such that
A6: for x being Point of [:T2,T2:] holds fx2[x,fx2.x] from FUNCT_2:sch
  3(A4 );
A7: for x being Element of [:T2,T2:] ex r being Real st yo[x,r]
  proof
    let x be Element of [:T2,T2:];
    consider x1, x2 being Point of T2 such that
A8: x = [x1,x2] by BORSUK_1:10;
    take x2`2 - o`2, x1, x2;
    thus thesis by A8;
  end;
  consider yo being RealMap of [:T2,T2:] such that
A9: for x being 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 EUCLID:42
    .= 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,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 being Point of T2 st $1 = [x1,x2] & $2
  = x2`2;
  defpred dy[set,set] means ex y1, y2 being 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 being Element of [:T2,T2:] ex r being Real st dy[x,r]
  proof
    let x be Element of [:T2,T2:];
    consider x1, x2 being Point of T2 such that
A18: x = [x1,x2] by BORSUK_1:10;
    take x1`2 - x2`2, x1, x2;
    thus thesis by A18;
  end;
  consider dy being RealMap of [:T2,T2:] such that
A19: for y being Point of [:T2,T2:] holds dy[y,dy.y] from FUNCT_2:sch 3(
  A17);
A20: for x being Element of [:T2,T2:] ex r being Real st fy2[x,r]
  proof
    let x be Element of [:T2,T2:];
    consider x1, x2 being Point of T2 such that
A21: x = [x1,x2] by BORSUK_1:10;
    take x2`2, x1, x2;
    thus thesis by A21;
  end;
  consider fy2 being RealMap of [:T2,T2:] such that
A22: for x being Point of [:T2,T2:] holds fy2[x,fy2.x] from FUNCT_2:sch
  3(A20 );
A23: for x being Element of [:T2,T2:] ex r being Real st dx[x,r]
  proof
    let x be Element of [:T2,T2:];
    consider x1, x2 being Point of T2 such that
A24: x = [x1,x2] by BORSUK_1:10;
    take x1`1 - x2`1, x1, x2;
    thus thesis by A24;
  end;
  consider dx being RealMap of [:T2,T2:] such that
A25: for x being 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 being Point of [:T2,T2:], V being Subset of R^1 st Yo.p in V & V
is open holds ex W being 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 being 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 being real number 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 is Element of REAL: p2`2-g < y & y < p2`2+g};
    W2 c= the carrier of T2
    proof
      let a be set;
      assume a in W2;
      then ex x, y being Element of 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,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 set;
    assume b in Yo.:[:[#]T2,W2:];
    then consider a being Point of [:T2,T2:] such that
A33: a in [:[#]T2,W2:] and
A34: Yo.a = b by FUNCT_2:65;
    consider a1, a2 being 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 being Element of 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 being Point of [:T2,T2:], V being Subset of R^1 st Xo.p in V & V
is open holds ex W being 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 being 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 being real number 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 is Element of REAL: p2`1-g < x & x < p2`1+g};
    W2 c= the carrier of T2
    proof
      let a be set;
      assume a in W2;
      then ex x, y being Element of 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,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 set;
    assume b in Xo.:[:[#]T2,W2:];
    then consider a being Point of [:T2,T2:] such that
A46: a in [:[#]T2,W2:] and
A47: Xo.a = b by FUNCT_2:65;
    consider a1, a2 being 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 being Element of 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 being Point of [:T2,T2:], V being Subset of R^1 st Dy.p in V & V
is open holds ex W being 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 being 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 being real number 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 is Element of REAL: p2`2-g/2 < y & y < p2`2+g
    /2};
A59: W2 c= the carrier of T2
    proof
      let a be set;
      assume a in W2;
      then ex x, y being Element of 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,15;
    then
A62: p2 in W2 by A60;
    set W1 = {|[x,y]| where x, y is Element of REAL: p1`2-g/2 < y & y < p1`2+g
    /2};
    W1 c= the carrier of T2
    proof
      let a be set;
      assume a in W1;
      then ex x, y being Element of 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,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 set;
    assume b in Dy.:[:W1,W2:];
    then consider a being Point of [:T2,T2:] such that
A64: a in [:W1,W2:] and
A65: Dy.a = b by FUNCT_2:65;
    consider a1, a2 being 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 being Element of 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: abs(p2`2-y2) < g/2 by A72,SEQ_2:1;
    a1 in W1 by A64,A66,ZFMISC_1:87;
    then consider x1, y1 being Element of 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;
    abs(p1`2-y1-(p2`2-y2)) <= abs(p1`2-y1)+abs(p2`2-y2) by COMPLEX1:57;
    then
A78: abs-(p1`2-y1-(p2`2-y2)) <= abs(p1`2-y1)+abs(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 abs(p1`2-y1) < g/2 by A77,SEQ_2:1;
    then abs(p1`2-y1)+abs(p2`2-y2) < g/2+g/2 by A73,XREAL_1:8;
    then
A79: abs(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 being Point of [:T2,T2:], V being Subset of R^1 st Dx.p in V & V
is open holds ex W being 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 being 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 being real number 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 is Element of REAL: p2`1-g/2 < x & x < p2`1+g
    /2};
A86: W2 c= the carrier of T2
    proof
      let a be set;
      assume a in W2;
      then ex x, y being Element of 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,15;
    then
A89: p2 in W2 by A87;
    set W1 = {|[x,y]| where x, y is Element of REAL: p1`1-g/2 < x & x < p1`1+g
    /2};
    W1 c= the carrier of T2
    proof
      let a be set;
      assume a in W1;
      then ex x, y being Element of 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,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 set;
    assume b in Dx.:[:W1,W2:];
    then consider a being Point of [:T2,T2:] such that
A91: a in [:W1,W2:] and
A92: Dx.a = b by FUNCT_2:65;
    consider a1, a2 being 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 being Element of 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: abs(p2`1-x2) < g/2 by A99,SEQ_2:1;
    a1 in W1 by A91,A93,ZFMISC_1:87;
    then consider x1, y1 being Element of 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;
    abs(p1`1-x1-(p2`1-x2)) <= abs(p1`1-x1)+abs(p2`1-x2) by COMPLEX1:57;
    then
A105: abs-(p1`1-x1-(p2`1-x2)) <= abs(p1`1-x1)+abs(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 abs(p1`1-x1) < g/2 by A104,SEQ_2:1;
    then abs(p1`1-x1)+abs(p2`1-x2) < g/2+g/2 by A100,XREAL_1:8;
    then
A106: abs(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 being Point of [:T2,T2:], V being Subset of R^1 st fY2.p in V &
  V is open holds ex W being 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 being Point of T2 such that
A109: p = [p1,p2] and
A110: fY2.p = p2`2 by A22;
    consider g being real number 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 is Element of REAL: p2`2-g < y & y < p2`2+g};
    W1 c= the carrier of T2
    proof
      let a be set;
      assume a in W1;
      then ex x, y being Element of 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,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 set;
    assume b in fY2.:[:[#]T2,W1:];
    then consider a being Point of [:T2,T2:] such that
A114: a in [:[#]T2,W1:] and
A115: fY2.a = b by FUNCT_2:65;
    consider a1, a2 being 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 being Element of 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 abs(p2`2-y1) < g by A121,SEQ_2:1;
    then abs-(p2`2-y1) < g by COMPLEX1:52;
    then
A122: abs(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 being Point of [:T2,T2:], V being Subset of R^1 st fX2.p in V &
  V is open holds ex W being 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 being Point of T2 such that
A125: p = [p1,p2] and
A126: fX2.p = p2`1 by A6;
    consider g being real number 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 is Element of REAL: p2`1-g < x & x < p2`1+g};
    W1 c= the carrier of T2
    proof
      let a be set;
      assume a in W1;
      then ex x, y being Element of 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,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 set;
    assume b in fX2.:[:[#]T2,W1:];
    then consider a being Point of [:T2,T2:] such that
A130: a in [:[#]T2,W1:] and
A131: fX2.a = b by FUNCT_2:65;
    consider a1, a2 being 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 being Element of 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 abs(p2`1-x1) < g by A137,SEQ_2:1;
    then abs-(p2`1-x1) < g by COMPLEX1:52;
    then
A138: abs(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 being 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 number;
    assume b in rng p2;
    then consider a being set 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 being 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 being 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 being 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 being 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 number;
    assume b in rng m;
    then consider a being set 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 being 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 being 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 being 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 being 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 being 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,ABIAN:def 5;
    then
A179: x <> f.x by ABIAN:def 4;
    consider y, z being 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 being 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 being 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 being 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 being 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 being 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 being 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 being Point of D2, V being Subset of S1 st g.p in V & V is open
  holds ex W being 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 being 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,ABIAN:def 5;
    then p <> f.p by ABIAN:def 4;
    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 being set st x in dom F holds (id dom R*F).x = F.x
    proof
      let x be set 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 being 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 being Subset of [:T2,T2:] such that
A233: WW is open and
A234: WW /\ [#]TD = W by A231,TOPS_2:24;
    consider SF being Subset-Family of [:T2,T2:] such that
A235: WW = union SF and
A236: for e being set st e in SF ex X1 being Subset of T2, Y1 being
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 being 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 being 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 being 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 set;
    assume b in g.:W1;
    then consider a being 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,ABIAN:def 5;
    then a <> f.a by ABIAN:def 4;
    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,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;

::$N Brouwer Fixed Point Theorem
theorem Th14:
  for r being non negative real number, o being Point of
  TOP-REAL 2, f being continuous Function of Tdisk(o,r), Tdisk(o,r) holds f
  is with_fixpoint
proof
  let r be non negative real number, 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 number;
    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
    proof
      let W be Point of Tdisk(o,r);
      assume
A6:   W in the carrier of Y;
      not W is_a_fixpoint_of f by A4,ABIAN:def 5;
      hence thesis by A6,Th11;
    end;
    g is continuous by A4,Th13;
    hence contradiction by A3,A5,BORSUK_1:def 17;
  end;
  suppose
    r is non positive;
    then reconsider r as non negative non positive real number;
    take o;
A7: 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,A7,TARSKI:def 1;
    then f.o in rng f by FUNCT_1:def 3;
    hence thesis by A2,A7,TARSKI:def 1;
  end;
end;

::$N Brouwer Fixed Point Theorem for Disks on the Plane
theorem
  for r being non negative real number, o being Point of TOP-REAL 2, f
being continuous Function of Tdisk(o,r), Tdisk(o,r) ex x being Point of Tdisk(o
  ,r) st f.x = x
proof
  let r be non negative real number, 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 being set such that
A1: x is_a_fixpoint_of f by ABIAN:def 5;
  take x;
  x in dom f by A1,ABIAN:def 3;
  hence x is Point of Tdisk(o,r);
  thus f.x = x by A1,ABIAN:def 3;
end;