:: BROUWER semantic presentation begin set T2 = TOP-REAL 2; definition let S, T be non empty TopSpace; func DiffElems (S,T) -> Subset of [:S,T:] equals :: BROUWER:def 1 { [s,t] where s is Point of S, t is Point of T : s <> t } ; coherence { [s,t] where s is Point of S, t is Point of T : s <> t } is Subset of [:S,T:] proof set A = { [s,t] where s is Point of S, t is Point of T : s <> t } ; { [s,t] where s is Point of S, t is Point of T : s <> t } c= the carrier of [:S,T:] proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { [s,t] where s is Point of S, t is Point of T : s <> t } or a in the carrier of [:S,T:] ) assume a in { [s,t] where s is Point of S, t is Point of T : s <> t } ; ::_thesis: a in the carrier of [:S,T:] then ex s being Point of S ex t being Point of T st ( a = [s,t] & s <> t ) ; hence a in the carrier of [:S,T:] ; ::_thesis: verum end; hence { [s,t] where s is Point of S, t is Point of T : s <> t } is Subset of [:S,T:] ; ::_thesis: verum end; end; :: deftheorem defines DiffElems BROUWER:def_1_:_ for S, T being non empty TopSpace holds DiffElems (S,T) = { [s,t] where s is Point of S, t is Point of T : s <> t } ; theorem :: BROUWER:1 for S, T being non empty TopSpace for x being set holds ( x in DiffElems (S,T) iff ex s being Point of S ex 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 not DiffElems (S,T) is empty proof set t1 = the Element of T; consider s1, s2 being Element of S such that A1: s1 <> s2 by SUBSET_1:def_7; percases ( s1 = the Element of T or s1 <> the Element of T ) ; suppose s1 = the Element of T ; ::_thesis: not DiffElems (S,T) is empty then [s2, the Element of T] in DiffElems (S,T) by A1; hence not DiffElems (S,T) is empty ; ::_thesis: verum end; suppose s1 <> the Element of T ; ::_thesis: not DiffElems (S,T) is empty then [s1, the Element of T] in DiffElems (S,T) ; hence not DiffElems (S,T) is empty ; ::_thesis: verum end; end; end; end; registration let S be non empty TopSpace; let T be non trivial TopSpace; cluster DiffElems (S,T) -> non empty ; coherence not DiffElems (S,T) is empty proof set s1 = the Element of S; consider t1, t2 being Element of T such that A1: t1 <> t2 by SUBSET_1:def_7; percases ( the Element of S = t1 or the Element of S <> t1 ) ; suppose the Element of S = t1 ; ::_thesis: not DiffElems (S,T) is empty then [ the Element of S,t2] in DiffElems (S,T) by A1; hence not DiffElems (S,T) is empty ; ::_thesis: verum end; suppose the Element of S <> t1 ; ::_thesis: not DiffElems (S,T) is empty then [ the Element of S,t1] in DiffElems (S,T) ; hence not DiffElems (S,T) is empty ; ::_thesis: verum end; end; end; end; theorem Th2: :: BROUWER:2 for n being Element of NAT for x being Point of (TOP-REAL n) holds cl_Ball (x,0) = {x} proof let n be Element of NAT ; ::_thesis: for x being Point of (TOP-REAL n) holds cl_Ball (x,0) = {x} let x be Point of (TOP-REAL n); ::_thesis: cl_Ball (x,0) = {x} thus cl_Ball (x,0) c= {x} :: according to XBOOLE_0:def_10 ::_thesis: {x} c= cl_Ball (x,0) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in cl_Ball (x,0) or a in {x} ) assume A1: a in cl_Ball (x,0) ; ::_thesis: a in {x} then reconsider a = a as Point of (TOP-REAL n) ; |.(a - x).| = 0 by A1, TOPREAL9:8; then a = x by TOPRNS_1:28; hence a in {x} by TARSKI:def_1; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {x} or a in cl_Ball (x,0) ) assume a in {x} ; ::_thesis: a in cl_Ball (x,0) then A2: a = x by TARSKI:def_1; |.(x - x).| = 0 by TOPRNS_1:28; hence a in cl_Ball (x,0) by A2, TOPREAL9:8; ::_thesis: verum end; definition let n be Element of NAT ; let x be Point of (TOP-REAL n); let r be real number ; func Tdisk (x,r) -> SubSpace of TOP-REAL n equals :: BROUWER:def 2 (TOP-REAL n) | (cl_Ball (x,r)); coherence (TOP-REAL n) | (cl_Ball (x,r)) is SubSpace of TOP-REAL n ; end; :: deftheorem defines Tdisk BROUWER:def_2_:_ for n being Element of NAT for x being Point of (TOP-REAL n) for r being real number holds Tdisk (x,r) = (TOP-REAL n) | (cl_Ball (x,r)); registration let n be Element of NAT ; let x be Point of (TOP-REAL n); let r be non negative real number ; cluster Tdisk (x,r) -> non empty ; coherence not Tdisk (x,r) is empty ; end; theorem Th3: :: BROUWER:3 for n being Element of NAT for r being real number for x being Point of (TOP-REAL n) holds the carrier of (Tdisk (x,r)) = cl_Ball (x,r) proof let n be Element of NAT ; ::_thesis: for r being real number for x being Point of (TOP-REAL n) holds the carrier of (Tdisk (x,r)) = cl_Ball (x,r) let r be real number ; ::_thesis: for x being Point of (TOP-REAL n) holds the carrier of (Tdisk (x,r)) = cl_Ball (x,r) let x be Point of (TOP-REAL n); ::_thesis: the carrier of (Tdisk (x,r)) = cl_Ball (x,r) [#] (Tdisk (x,r)) = cl_Ball (x,r) by PRE_TOPC:def_5; hence the carrier of (Tdisk (x,r)) = cl_Ball (x,r) ; ::_thesis: verum end; registration let n be Element of NAT ; let x be Point of (TOP-REAL n); let r be real number ; cluster Tdisk (x,r) -> convex ; coherence Tdisk (x,r) is convex proof thus [#] (Tdisk (x,r)) is convex Subset of (TOP-REAL n) by Th3; :: according to TOPALG_2:def_1 ::_thesis: verum end; end; theorem Th4: :: BROUWER:4 for n being Element of NAT for r being non negative real number for s, t, x being Point of (TOP-REAL n) st s <> t & s is Point of (Tdisk (x,r)) & s is not Point of (Tcircle (x,r)) holds ex e being Point of (Tcircle (x,r)) st {e} = (halfline (s,t)) /\ (Sphere (x,r)) proof let n be Element of NAT ; ::_thesis: for r being non negative real number for s, t, x being Point of (TOP-REAL n) st s <> t & s is Point of (Tdisk (x,r)) & s is not Point of (Tcircle (x,r)) holds ex e being Point of (Tcircle (x,r)) st {e} = (halfline (s,t)) /\ (Sphere (x,r)) let r be non negative real number ; ::_thesis: for s, t, x being Point of (TOP-REAL n) st s <> t & s is Point of (Tdisk (x,r)) & s is not Point of (Tcircle (x,r)) holds ex e being Point of (Tcircle (x,r)) st {e} = (halfline (s,t)) /\ (Sphere (x,r)) let s, t, x be Point of (TOP-REAL n); ::_thesis: ( 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)) ) assume that A1: s <> t and A2: s is Point of (Tdisk (x,r)) and A3: s is not Point of (Tcircle (x,r)) ; ::_thesis: ex e being Point of (Tcircle (x,r)) st {e} = (halfline (s,t)) /\ (Sphere (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 - (((- (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)))))) * s) + ((((- (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))))) * 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 ex e being Point of (Tcircle (x,r)) st {e} = (halfline (s,t)) /\ (Sphere (x,r)) by A5, A6; ::_thesis: verum end; theorem Th5: :: BROUWER:5 for n being Element of NAT for r being non negative real number for s, t, x being Point of (TOP-REAL n) st s <> t & s in the carrier of (Tcircle (x,r)) & t is Point of (Tdisk (x,r)) holds ex e being Point of (Tcircle (x,r)) st ( e <> s & {s,e} = (halfline (s,t)) /\ (Sphere (x,r)) ) proof let n be Element of NAT ; ::_thesis: for r being non negative real number for s, t, x being Point of (TOP-REAL n) st s <> t & s in the carrier of (Tcircle (x,r)) & t is Point of (Tdisk (x,r)) holds ex e being Point of (Tcircle (x,r)) st ( e <> s & {s,e} = (halfline (s,t)) /\ (Sphere (x,r)) ) let r be non negative real number ; ::_thesis: for s, t, x being Point of (TOP-REAL n) st s <> t & s in the carrier of (Tcircle (x,r)) & t is Point of (Tdisk (x,r)) holds ex e being Point of (Tcircle (x,r)) st ( e <> s & {s,e} = (halfline (s,t)) /\ (Sphere (x,r)) ) let s, t, x be Point of (TOP-REAL n); ::_thesis: ( 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)) ) ) assume A1: ( s <> t & s in the carrier of (Tcircle (x,r)) & t is Point of (Tdisk (x,r)) ) ; ::_thesis: ex e being Point of (Tcircle (x,r)) st ( e <> s & {s,e} = (halfline (s,t)) /\ (Sphere (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) & ((- (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)))) = ((- (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 - (((- (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)))))) * (((1 / 2) * s) + ((1 / 2) * t))) + ((((- (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))))) * 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 ex e being Point of (Tcircle (x,r)) st ( e <> s & {s,e} = (halfline (s,t)) /\ (Sphere (x,r)) ) by A2, A3, A4; ::_thesis: verum end; definition let n be non empty Element of NAT ; let o be Point of (TOP-REAL n); let s, t be Point of (TOP-REAL n); let 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: :: BROUWER:def 3 ( it in (halfline (s,t)) /\ (Sphere (o,r)) & it <> s ); existence ex b1 being Point of (TOP-REAL n) st ( b1 in (halfline (s,t)) /\ (Sphere (o,r)) & b1 <> s ) proof percases ( s is Point of (Tcircle (o,r)) or not s is Point of (Tcircle (o,r)) ) ; suppose s is Point of (Tcircle (o,r)) ; ::_thesis: ex b1 being Point of (TOP-REAL n) st ( b1 in (halfline (s,t)) /\ (Sphere (o,r)) & b1 <> s ) 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 = e as Point of (TOP-REAL n) by PRE_TOPC:25; take e ; ::_thesis: ( e in (halfline (s,t)) /\ (Sphere (o,r)) & e <> s ) thus ( e in (halfline (s,t)) /\ (Sphere (o,r)) & e <> s ) by A4, TARSKI:def_2; ::_thesis: verum end; supposeA5: s is not Point of (Tcircle (o,r)) ; ::_thesis: ex b1 being Point of (TOP-REAL n) st ( b1 in (halfline (s,t)) /\ (Sphere (o,r)) & b1 <> s ) 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 = e1 as Point of (TOP-REAL n) by PRE_TOPC:25; take e1 ; ::_thesis: ( e1 in (halfline (s,t)) /\ (Sphere (o,r)) & e1 <> s ) thus ( e1 in (halfline (s,t)) /\ (Sphere (o,r)) & e1 <> s ) by A5, A6, TARSKI:def_1; ::_thesis: verum end; end; end; uniqueness for b1, b2 being Point of (TOP-REAL n) st b1 in (halfline (s,t)) /\ (Sphere (o,r)) & b1 <> s & b2 in (halfline (s,t)) /\ (Sphere (o,r)) & b2 <> s holds b1 = b2 proof let m, u be Point of (TOP-REAL n); ::_thesis: ( m in (halfline (s,t)) /\ (Sphere (o,r)) & m <> s & u in (halfline (s,t)) /\ (Sphere (o,r)) & u <> s implies m = u ) assume 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 ; ::_thesis: m = u percases ( s is Point of (Tcircle (o,r)) or not s is Point of (Tcircle (o,r)) ) ; suppose s is Point of (Tcircle (o,r)) ; ::_thesis: m = u 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; percases ( ( m = f1 & u = f1 ) or ( m = f1 & u = s ) or ( m = s & u = f1 ) or ( m = s & u = s ) ) by A7, A9, A11, TARSKI:def_2; suppose ( m = f1 & u = f1 ) ; ::_thesis: m = u hence m = u ; ::_thesis: verum end; suppose ( m = f1 & u = s ) ; ::_thesis: m = u hence m = u by A10; ::_thesis: verum end; suppose ( m = s & u = f1 ) ; ::_thesis: m = u hence m = u by A8; ::_thesis: verum end; suppose ( m = s & u = s ) ; ::_thesis: m = u hence m = u ; ::_thesis: verum end; end; end; suppose s is not Point of (Tcircle (o,r)) ; ::_thesis: m = u 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 m = u by A9, A12, TARSKI:def_1; ::_thesis: verum end; end; end; end; :: deftheorem Def3 defines HC BROUWER:def_3_:_ for n being non empty Element of NAT for o, s, t being Point of (TOP-REAL n) for r being non negative real number st s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t holds for b6 being Point of (TOP-REAL n) holds ( b6 = HC (s,t,o,r) iff ( b6 in (halfline (s,t)) /\ (Sphere (o,r)) & b6 <> s ) ); theorem Th6: :: BROUWER:6 for r being non negative real number for n being non empty Element of NAT for s, o, t being Point of (TOP-REAL n) st s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t holds HC (s,t,o,r) is Point of (Tcircle (o,r)) proof let r be non negative real number ; ::_thesis: for n being non empty Element of NAT for s, o, t being Point of (TOP-REAL n) st s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t holds HC (s,t,o,r) is Point of (Tcircle (o,r)) let n be non empty Element of NAT ; ::_thesis: for s, o, t being Point of (TOP-REAL n) st s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t holds HC (s,t,o,r) is Point of (Tcircle (o,r)) let s, o, t be Point of (TOP-REAL n); ::_thesis: ( 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)) ) assume ( s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t ) ; ::_thesis: HC (s,t,o,r) is Point of (Tcircle (o,r)) 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 HC (s,t,o,r) is Point of (Tcircle (o,r)) by XBOOLE_0:def_4; ::_thesis: verum end; theorem :: BROUWER:7 for a being real number for r being non negative real number for n being non empty Element of NAT for s, t, o being Point of (TOP-REAL n) for S, T, O being Element of REAL n st S = s & T = t & O = o & 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))) holds HC (s,t,o,r) = ((1 - a) * s) + (a * t) proof let a be real number ; ::_thesis: for r being non negative real number for n being non empty Element of NAT for s, t, o being Point of (TOP-REAL n) for S, T, O being Element of REAL n st S = s & T = t & O = o & 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))) holds HC (s,t,o,r) = ((1 - a) * s) + (a * t) let r be non negative real number ; ::_thesis: for n being non empty Element of NAT for s, t, o being Point of (TOP-REAL n) for S, T, O being Element of REAL n st S = s & T = t & O = o & 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))) holds HC (s,t,o,r) = ((1 - a) * s) + (a * t) let n be non empty Element of NAT ; ::_thesis: for s, t, o being Point of (TOP-REAL n) for S, T, O being Element of REAL n st S = s & T = t & O = o & 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))) holds HC (s,t,o,r) = ((1 - a) * s) + (a * t) let s, t, o be Point of (TOP-REAL n); ::_thesis: for S, T, O being Element of REAL n st S = s & T = t & O = o & 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))) holds HC (s,t,o,r) = ((1 - a) * s) + (a * t) let S, T, O be Element of REAL n; ::_thesis: ( S = s & T = t & O = o & 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) ) assume 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 ; ::_thesis: ( not 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))) or HC (s,t,o,r) = ((1 - a) * s) + (a * 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: HC (s,t,o,r) in (halfline (s,t)) /\ (Sphere (o,r)) by A4, A5, A6, Def3; then HC (s,t,o,r) in halfline (s,t) by XBOOLE_0:def_4; then consider l being real number such that A9: HC (s,t,o,r) = ((1 - l) * s) + (l * t) and A10: 0 <= l by TOPREAL9:26; HC (s,t,o,r) 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__::_thesis:_not_Sum_(sqr_(T_-_S))_<=_0 assume Sum (sqr (T - S)) <= 0 ; ::_thesis: contradiction then Sum (sqr (T - S)) = 0 by RVSUM_1:86; hence contradiction by A12, EUCLID:def_5, SQUARE_1:17; ::_thesis: verum end; set C = (Sum (sqr (S - O))) - (r ^2); set M = |((t - s),(s - o))|; set B = 2 * |((t - s),(s - o))|; set l1 = ((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))); set l2 = ((- (2 * |((t - s),(s - o))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))); 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 ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2))) = ((2 * |((t - s),(s - o))|) ^2) - ((4 * (Sum (sqr (T - S)))) * ((Sum (sqr (S - O))) - (r ^2))) 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: (Sum (sqr (S - O))) - (r ^2) <= 0 by A14, A15, XREAL_1:47; now__::_thesis:_for_x_being_real_number_holds_Polynom_((Sum_(sqr_(T_-_S))),(2_*_|((t_-_s),(s_-_o))|),((Sum_(sqr_(S_-_O)))_-_(r_^2)),x)_=_Quard_((Sum_(sqr_(T_-_S))),(((-_(2_*_|((t_-_s),(s_-_o))|))_-_(sqrt_(delta_((Sum_(sqr_(T_-_S))),(2_*_|((t_-_s),(s_-_o))|),((Sum_(sqr_(S_-_O)))_-_(r_^2))))))_/_(2_*_(Sum_(sqr_(T_-_S))))),(((-_(2_*_|((t_-_s),(s_-_o))|))_+_(sqrt_(delta_((Sum_(sqr_(T_-_S))),(2_*_|((t_-_s),(s_-_o))|),((Sum_(sqr_(S_-_O)))_-_(r_^2))))))_/_(2_*_(Sum_(sqr_(T_-_S))))),x) let x be real number ; ::_thesis: Polynom ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)),x) = Quard ((Sum (sqr (T - S))),(((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))),(((- (2 * |((t - s),(s - o))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))),x) thus Polynom ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)),x) = (((Sum (sqr (T - S))) * (x ^2)) + ((2 * |((t - s),(s - o))|) * x)) + ((Sum (sqr (S - O))) - (r ^2)) by POLYEQ_1:def_2 .= ((Sum (sqr (T - S))) * (x - (((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))))) * (x - (((- (2 * |((t - s),(s - o))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))) by A13, A18, A16, QUIN_1:16 .= (Sum (sqr (T - S))) * ((x - (((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))) * (x - (((- (2 * |((t - s),(s - o))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))))) .= Quard ((Sum (sqr (T - S))),(((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))),(((- (2 * |((t - s),(s - o))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))),x) by POLYEQ_1:def_3 ; ::_thesis: verum end; then A19: ((Sum (sqr (S - O))) - (r ^2)) / (Sum (sqr (T - S))) = (((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * (((- (2 * |((t - s),(s - o))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) by A13, POLYEQ_1:11; A20: now__::_thesis:_not_((-_(2_*_|((t_-_s),(s_-_o))|))_-_(sqrt_(delta_((Sum_(sqr_(T_-_S))),(2_*_|((t_-_s),(s_-_o))|),((Sum_(sqr_(S_-_O)))_-_(r_^2))))))_/_(2_*_(Sum_(sqr_(T_-_S))))_>_((-_(2_*_|((t_-_s),(s_-_o))|))_+_(sqrt_(delta_((Sum_(sqr_(T_-_S))),(2_*_|((t_-_s),(s_-_o))|),((Sum_(sqr_(S_-_O)))_-_(r_^2))))))_/_(2_*_(Sum_(sqr_(T_-_S)))) set D = sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))); assume ((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) > ((- (2 * |((t - s),(s - o))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) ; ::_thesis: contradiction then (- (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) - (2 * |((t - s),(s - o))|) > (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2))))) - (2 * |((t - s),(s - o))|) by A13, XREAL_1:72; hence contradiction by A13, A18, A16, XREAL_1:9; ::_thesis: verum end; assume A21: 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))) ; ::_thesis: HC (s,t,o,r) = ((1 - a) * s) + (a * t) delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2))) = ((2 * |((t - s),(s - o))|) ^2) - ((4 * (Sum (sqr (T - S)))) * ((Sum (sqr (S - O))) - (r ^2))) by QUIN_1:def_1 .= 4 * ((|((t - s),(s - o))| ^2) - ((Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2)))) ; then A22: ((- (2 * |((t - s),(s - o))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) = ((- (2 * |((t - s),(s - o))|)) + ((sqrt 4) * (sqrt ((|((t - s),(s - o))| ^2) - ((Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2))))))) / (2 * (Sum (sqr (T - S)))) by A13, A18, SQUARE_1:29 .= (2 * (- (|((t - s),(s - o))| - (sqrt ((|((t - s),(s - o))| ^2) - ((Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2)))))))) / (2 * (Sum (sqr (T - S)))) by SQUARE_1:20 .= a by A21, XCMPLX_1:91 ; A23: HC (s,t,o,r) = ((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 ; (((Sum (sqr (T - S))) * (l ^2)) + ((2 * |((t - s),(s - o))|) * l)) + ((Sum (sqr (S - O))) - (r ^2)) = (((Sum (sqr (T - S))) * (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 ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)),l) = 0 by POLYEQ_1:def_2; then A25: ( l = ((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) or l = ((- (2 * |((t - s),(s - o))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) ) by A13, A18, A16, POLYEQ_1:5; percases ( (Sum (sqr (S - O))) - (r ^2) < 0 or ((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) = ((- (2 * |((t - s),(s - o))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) or (Sum (sqr (S - O))) - (r ^2) = 0 ) by A14, A15, A17, XREAL_1:47; suppose (Sum (sqr (S - O))) - (r ^2) < 0 ; ::_thesis: HC (s,t,o,r) = ((1 - a) * s) + (a * t) hence HC (s,t,o,r) = ((1 - a) * s) + (a * t) by A9, A10, A13, A22, A25, A19, A20, XREAL_1:141; ::_thesis: verum end; suppose ((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) = ((- (2 * |((t - s),(s - o))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) ; ::_thesis: HC (s,t,o,r) = ((1 - a) * s) + (a * t) hence HC (s,t,o,r) = ((1 - a) * s) + (a * t) by A9, A22, A25; ::_thesis: verum end; supposeA26: (Sum (sqr (S - O))) - (r ^2) = 0 ; ::_thesis: HC (s,t,o,r) = ((1 - a) * s) + (a * t) now__::_thesis:_not_l_=_((-_(2_*_|((t_-_s),(s_-_o))|))_-_(sqrt_(delta_((Sum_(sqr_(T_-_S))),(2_*_|((t_-_s),(s_-_o))|),((Sum_(sqr_(S_-_O)))_-_(r_^2))))))_/_(2_*_(Sum_(sqr_(T_-_S)))) A27: now__::_thesis:_not_l_=_0 assume l = 0 ; ::_thesis: contradiction then HC (s,t,o,r) = s + (0. (TOP-REAL n)) by A23, EUCLID:29 .= s by EUCLID:27 ; hence contradiction by A4, A5, A6, Def3; ::_thesis: verum end; assume A28: l = ((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) ; ::_thesis: contradiction percases ( 0 < 2 * |((t - s),(s - o))| or 2 * |((t - s),(s - o))| <= 0 ) ; supposeA29: 0 < 2 * |((t - s),(s - o))| ; ::_thesis: contradiction then ((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) = ((- (2 * |((t - s),(s - o))|)) - (2 * |((t - s),(s - o))|)) / (2 * (Sum (sqr (T - S)))) by A16, A26, SQUARE_1:22; hence contradiction by A10, A13, A28, A29, XREAL_1:129, XREAL_1:141; ::_thesis: verum end; suppose 2 * |((t - s),(s - o))| <= 0 ; ::_thesis: contradiction then ((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) = ((- (2 * |((t - s),(s - o))|)) - (- (2 * |((t - s),(s - o))|))) / (2 * (Sum (sqr (T - S)))) by A16, A26, SQUARE_1:23 .= 0 ; hence contradiction by A28, A27; ::_thesis: verum end; end; end; hence HC (s,t,o,r) = ((1 - a) * s) + (a * t) by A9, A22, A25; ::_thesis: verum end; end; end; theorem Th8: :: BROUWER:8 for a being real number for r being non negative real number for r1, r2, s1, s2 being real number for s, t, o being Point of (TOP-REAL 2) st 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)) holds HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]| proof let a be real number ; ::_thesis: for r being non negative real number for r1, r2, s1, s2 being real number for s, t, o being Point of (TOP-REAL 2) st 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)) holds HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]| let r be non negative real number ; ::_thesis: for r1, r2, s1, s2 being real number for s, t, o being Point of (TOP-REAL 2) st 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)) holds HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]| let r1, r2, s1, s2 be real number ; ::_thesis: for s, t, o being Point of (TOP-REAL 2) st 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)) holds HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]| let s, t, o be Point of (TOP-REAL 2); ::_thesis: ( 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))]| ) assume 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)) ; ::_thesis: HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]| 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 * ((s1 * r1) + (s2 * r2)); set l1 = ((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))); set l2 = ((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))); A9: delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2))) = ((2 * ((s1 * r1) + (s2 * r2))) ^2) - ((4 * ((r1 ^2) + (r2 ^2))) * (((s1 ^2) + (s2 ^2)) - (r ^2))) 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: ((s1 ^2) + (s2 ^2)) - (r ^2) <= (r ^2) - (r ^2) by A8, XREAL_1:9; then A11: ((2 * ((s1 * r1) + (s2 * r2))) ^2) - ((4 * ((r1 ^2) + (r2 ^2))) * (((s1 ^2) + (s2 ^2)) - (r ^2))) >= 0 ; A12: now__::_thesis:_not_((-_(2_*_((s1_*_r1)_+_(s2_*_r2))))_-_(sqrt_(delta_(((r1_^2)_+_(r2_^2)),(2_*_((s1_*_r1)_+_(s2_*_r2))),(((s1_^2)_+_(s2_^2))_-_(r_^2))))))_/_(2_*_((r1_^2)_+_(r2_^2)))_>_((-_(2_*_((s1_*_r1)_+_(s2_*_r2))))_+_(sqrt_(delta_(((r1_^2)_+_(r2_^2)),(2_*_((s1_*_r1)_+_(s2_*_r2))),(((s1_^2)_+_(s2_^2))_-_(r_^2))))))_/_(2_*_((r1_^2)_+_(r2_^2))) set D = sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))); assume ((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) > ((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) ; ::_thesis: contradiction then (- (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) - (2 * ((s1 * r1) + (s2 * r2))) > (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2))))) - (2 * ((s1 * r1) + (s2 * r2))) by XREAL_1:72; then - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2))))) > sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))) by XREAL_1:9; then (- (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2))))) > (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2))))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2))))) by XREAL_1:6; hence contradiction by A9, A11; ::_thesis: verum end; ( r1 <> 0 or r2 <> 0 ) by A3, A4, TOPREAL3:6; then A13: 0 + 0 < (r1 ^2) + (r2 ^2) by SQUARE_1:12, XREAL_1:8; for x being real number holds Polynom (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)),x) = Quard (((r1 ^2) + (r2 ^2)),(((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)))),(((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)))),x) proof let x be real number ; ::_thesis: Polynom (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)),x) = Quard (((r1 ^2) + (r2 ^2)),(((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)))),(((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)))),x) thus Polynom (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)),x) = ((((r1 ^2) + (r2 ^2)) * (x ^2)) + ((2 * ((s1 * r1) + (s2 * r2))) * x)) + (((s1 ^2) + (s2 ^2)) - (r ^2)) by POLYEQ_1:def_2 .= (((r1 ^2) + (r2 ^2)) * (x - (((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)))))) * (x - (((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))))) by A13, A9, A10, QUIN_1:16 .= ((r1 ^2) + (r2 ^2)) * ((x - (((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))))) * (x - (((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)))))) .= Quard (((r1 ^2) + (r2 ^2)),(((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)))),(((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)))),x) by POLYEQ_1:def_3 ; ::_thesis: verum end; then A14: (((s1 ^2) + (s2 ^2)) - (r ^2)) / ((r1 ^2) + (r2 ^2)) = (((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)))) * (((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)))) by A13, POLYEQ_1:11; delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2))) = ((2 * ((s1 * r1) + (s2 * r2))) ^2) - ((4 * ((r1 ^2) + (r2 ^2))) * (((s1 ^2) + (s2 ^2)) - (r ^2))) by QUIN_1:def_1 .= 4 * ((((s1 * r1) + (s2 * r2)) ^2) - (((r1 ^2) + (r2 ^2)) * (((s1 ^2) + (s2 ^2)) - (r ^2)))) ; then A15: ((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) = ((- (2 * ((s1 * r1) + (s2 * r2)))) + ((sqrt 4) * (sqrt ((((s1 * r1) + (s2 * r2)) ^2) - (((r1 ^2) + (r2 ^2)) * (((s1 ^2) + (s2 ^2)) - (r ^2))))))) / (2 * ((r1 ^2) + (r2 ^2))) by A10, SQUARE_1:29 .= (2 * (- (((s1 * r1) + (s2 * r2)) - (sqrt ((((s1 * r1) + (s2 * r2)) ^2) - (((r1 ^2) + (r2 ^2)) * (((s1 ^2) + (s2 ^2)) - (r ^2)))))))) / (2 * ((r1 ^2) + (r2 ^2))) by SQUARE_1:20 .= a by A7, XCMPLX_1:91 ; set H = HC (s,t,o,r); A16: HC (s,t,o,r) in (halfline (s,t)) /\ (Sphere (o,r)) by A1, A2, A3, Def3; then HC (s,t,o,r) in halfline (s,t) by XBOOLE_0:def_4; then consider l being real number such that A17: HC (s,t,o,r) = ((1 - l) * s) + (l * t) and A18: 0 <= l by TOPREAL9:26; A19: HC (s,t,o,r) = ((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: (HC (s,t,o,r)) `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 ; HC (s,t,o,r) in Sphere (o,r) by A16, XBOOLE_0:def_4; then |.((HC (s,t,o,r)) - o).| = r by TOPREAL9:9; then r ^2 = ((((HC (s,t,o,r)) - o) `1) ^2) + ((((HC (s,t,o,r)) - o) `2) ^2) by JGRAPH_1:29 .= ((((HC (s,t,o,r)) `1) - (o `1)) ^2) + ((((HC (s,t,o,r)) - o) `2) ^2) by TOPREAL3:3 .= ((((HC (s,t,o,r)) `1) - (o `1)) ^2) + ((((HC (s,t,o,r)) `2) - (o `2)) ^2) by TOPREAL3:3 .= (((((1 - l) * (s `1)) + (l * (t `1))) - (o `1)) ^2) + ((((HC (s,t,o,r)) `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) * ((s1 * r1) + (s2 * r2)))) + (s1 ^2)) + (s2 ^2) by A4, A5, A6 ; then ((((r1 ^2) + (r2 ^2)) * (l ^2)) + ((2 * ((s1 * r1) + (s2 * r2))) * l)) + (((s1 ^2) + (s2 ^2)) - (r ^2)) = 0 ; then Polynom (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)),l) = 0 by POLYEQ_1:def_2; then A21: ( l = ((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) or l = ((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) ) by A13, A9, A10, POLYEQ_1:5; A22: (HC (s,t,o,r)) `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 ; percases ( ((s1 ^2) + (s2 ^2)) - (r ^2) < 0 or ((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) = ((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) or ((s1 ^2) + (s2 ^2)) - (r ^2) = 0 ) by A10; suppose ((s1 ^2) + (s2 ^2)) - (r ^2) < 0 ; ::_thesis: HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]| hence HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]| by A4, A18, A20, A22, A13, A15, A21, A14, A12, EUCLID:53, XREAL_1:141; ::_thesis: verum end; suppose ((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) = ((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) ; ::_thesis: HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]| hence HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]| by A4, A20, A22, A15, A21, EUCLID:53; ::_thesis: verum end; supposeA23: ((s1 ^2) + (s2 ^2)) - (r ^2) = 0 ; ::_thesis: HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]| now__::_thesis:_not_l_=_((-_(2_*_((s1_*_r1)_+_(s2_*_r2))))_-_(sqrt_(delta_(((r1_^2)_+_(r2_^2)),(2_*_((s1_*_r1)_+_(s2_*_r2))),(((s1_^2)_+_(s2_^2))_-_(r_^2))))))_/_(2_*_((r1_^2)_+_(r2_^2))) A24: now__::_thesis:_not_l_=_0 assume l = 0 ; ::_thesis: contradiction then HC (s,t,o,r) = s + (0. (TOP-REAL 2)) by A19, EUCLID:29 .= s by EUCLID:27 ; hence contradiction by A1, A2, A3, Def3; ::_thesis: verum end; assume A25: l = ((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) ; ::_thesis: contradiction percases ( 0 < 2 * ((s1 * r1) + (s2 * r2)) or 2 * ((s1 * r1) + (s2 * r2)) <= 0 ) ; supposeA26: 0 < 2 * ((s1 * r1) + (s2 * r2)) ; ::_thesis: contradiction then ((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) = ((- (2 * ((s1 * r1) + (s2 * r2)))) - (2 * ((s1 * r1) + (s2 * r2)))) / (2 * ((r1 ^2) + (r2 ^2))) by A9, A23, SQUARE_1:22; hence contradiction by A18, A13, A25, A26, XREAL_1:129, XREAL_1:141; ::_thesis: verum end; suppose 2 * ((s1 * r1) + (s2 * r2)) <= 0 ; ::_thesis: contradiction then ((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) = ((- (2 * ((s1 * r1) + (s2 * r2)))) - (- (2 * ((s1 * r1) + (s2 * r2))))) / (2 * ((r1 ^2) + (r2 ^2))) by A9, A23, SQUARE_1:23 .= 0 ; hence contradiction by A25, A24; ::_thesis: verum end; end; end; hence HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]| by A4, A20, A22, A15, A21, EUCLID:53; ::_thesis: verum end; end; end; definition let n be non empty Element of NAT ; let o be Point of (TOP-REAL n); let 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)); assume A1: not x is_a_fixpoint_of f ; func HC (x,f) -> Point of (Tcircle (o,r)) means :Def4: :: BROUWER:def 4 ex y, z being Point of (TOP-REAL n) st ( y = x & z = f . x & it = HC (z,y,o,r) ); existence ex b1 being Point of (Tcircle (o,r)) ex y, z being Point of (TOP-REAL n) st ( y = x & z = f . x & b1 = HC (z,y,o,r) ) 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 ; ::_thesis: ex y, z being Point of (TOP-REAL n) st ( y = x & z = f . x & a = HC (z,y,o,r) ) thus ex y, z being Point of (TOP-REAL n) st ( y = x & z = f . x & a = HC (z,y,o,r) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Point of (Tcircle (o,r)) st ex y, z being Point of (TOP-REAL n) st ( y = x & z = f . x & b1 = HC (z,y,o,r) ) & ex y, z being Point of (TOP-REAL n) st ( y = x & z = f . x & b2 = HC (z,y,o,r) ) holds b1 = b2 ; end; :: deftheorem Def4 defines HC BROUWER:def_4_:_ for n being non empty Element of NAT for o being Point of (TOP-REAL n) for r being non negative real number for x being Point of (Tdisk (o,r)) for f being Function of (Tdisk (o,r)),(Tdisk (o,r)) st not x is_a_fixpoint_of f holds for b6 being Point of (Tcircle (o,r)) holds ( b6 = HC (x,f) iff ex y, z being Point of (TOP-REAL n) st ( y = x & z = f . x & b6 = HC (z,y,o,r) ) ); theorem Th9: :: BROUWER:9 for r being non negative real number for n being non empty Element of NAT for o being Point of (TOP-REAL n) for x being Point of (Tdisk (o,r)) for 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 r be non negative real number ; ::_thesis: for n being non empty Element of NAT for o being Point of (TOP-REAL n) for x being Point of (Tdisk (o,r)) for 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 let n be non empty Element of NAT ; ::_thesis: for o being Point of (TOP-REAL n) for x being Point of (Tdisk (o,r)) for 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 let o be Point of (TOP-REAL n); ::_thesis: for x being Point of (Tdisk (o,r)) for 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 let x be Point of (Tdisk (o,r)); ::_thesis: for 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 let f be Function of (Tdisk (o,r)),(Tdisk (o,r)); ::_thesis: ( not x is_a_fixpoint_of f & x is Point of (Tcircle (o,r)) implies HC (x,f) = x ) assume that A1: not x is_a_fixpoint_of f and A2: x is Point of (Tcircle (o,r)) ; ::_thesis: HC (x,f) = x 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 HC (x,f) = x by A3, A5, A6, Def3; ::_thesis: verum end; theorem Th10: :: BROUWER:10 for r being positive real number for o being Point of (TOP-REAL 2) for 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 ; ::_thesis: for o being Point of (TOP-REAL 2) for Y being non empty SubSpace of Tdisk (o,r) st Y = Tcircle (o,r) holds not Y is_a_retract_of Tdisk (o,r) let o be Point of (TOP-REAL 2); ::_thesis: for Y being non empty SubSpace of Tdisk (o,r) st Y = Tcircle (o,r) holds not Y is_a_retract_of Tdisk (o,r) let Y be non empty SubSpace of Tdisk (o,r); ::_thesis: ( Y = Tcircle (o,r) implies not Y is_a_retract_of Tdisk (o,r) ) assume A1: Y = Tcircle (o,r) ; ::_thesis: not Y is_a_retract_of Tdisk (o,r) set y0 = the Point of Y; set X = Tdisk (o,r); A2: the Point of Y 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 = the Point of Y as Point of (Tdisk (o,r)) 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: the constant Loop of x0 = I[01] --> x0 by BORSUK_2:5 .= the carrier of I[01] --> the Point of Y ; then reconsider D = the constant Loop of x0 as Function of I[01],Y ; A4: ( D = I[01] --> the Point of Y & D . a0 = the Point of Y ) by A3, FUNCOP_1:7; ( the Point of Y, the Point of Y are_connected & D . a1 = the Point of Y ) by A3, FUNCOP_1:7; then reconsider D = D as constant Loop of the Point of Y by A4, BORSUK_2:def_2; given R being continuous Function of (Tdisk (o,r)),Y such that A5: R is being_a_retraction ; :: according to BORSUK_1:def_17 ::_thesis: contradiction the carrier of (pi_1 (Y, the Point of Y)) = {(Class ((EqRel (Y, the Point of Y)),D))} proof set E = EqRel (Y, the Point of Y); hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {(Class ((EqRel (Y, the Point of Y)),D))} c= the carrier of (pi_1 (Y, the Point of Y)) let x be set ; ::_thesis: ( x in the carrier of (pi_1 (Y, the Point of Y)) implies x in {(Class ((EqRel (Y, the Point of Y)),D))} ) assume x in the carrier of (pi_1 (Y, the Point of Y)) ; ::_thesis: x in {(Class ((EqRel (Y, the Point of Y)),D))} then consider f0 being Loop of the Point of Y such that A6: x = Class ((EqRel (Y, the Point of Y)),f0) by TOPALG_1:47; reconsider g0 = f0 as Loop of x0 by TOPALG_2:1; g0, the constant Loop of x0 are_homotopic by TOPALG_2:2; then consider f being Function of [:I[01],I[01]:],(Tdisk (o,r)) such that A7: f is continuous and A8: for s being Point of I[01] holds ( f . (s,0) = g0 . s & f . (s,1) = the constant Loop of x0 . 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; :: according to BORSUK_2:def_7 ::_thesis: ( F is continuous & ( for b1 being Element of the carrier of K582() holds ( F . (b1,0) = f0 . b1 & F . (b1,1) = D . b1 & F . (0,b1) = the Point of Y & F . (1,b1) = the Point of Y ) ) ) thus F is continuous by A7; ::_thesis: for b1 being Element of the carrier of K582() holds ( F . (b1,0) = f0 . b1 & F . (b1,1) = D . b1 & F . (0,b1) = the Point of Y & F . (1,b1) = the Point of Y ) let s be Point of I[01]; ::_thesis: ( F . (s,0) = f0 . s & F . (s,1) = D . s & F . (0,s) = the Point of Y & F . (1,s) = the Point of Y ) 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 ; ::_thesis: ( F . (s,1) = D . s & F . (0,s) = the Point of Y & F . (1,s) = the Point of Y ) thus F . (s,1) = F . [s,a1] .= R . (f . (s,1)) by FUNCT_2:15 .= R . ( the constant Loop of x0 . s) by A8 .= D . s by A5, BORSUK_1:def_16 ; ::_thesis: ( F . (0,s) = the Point of Y & F . (1,s) = the Point of Y ) thus F . (0,s) = F . [a0,s] .= R . (f . (0,s)) by FUNCT_2:15 .= R . x0 by A8 .= the Point of Y by A5, BORSUK_1:def_16 ; ::_thesis: F . (1,s) = the Point of Y thus F . (1,s) = F . [a1,s] .= R . (f . (1,s)) by FUNCT_2:15 .= R . x0 by A8 .= the Point of Y by A5, BORSUK_1:def_16 ; ::_thesis: verum end; then x = Class ((EqRel (Y, the Point of Y)),D) by A6, TOPALG_1:46; hence x in {(Class ((EqRel (Y, the Point of Y)),D))} by TARSKI:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(Class ((EqRel (Y, the Point of Y)),D))} or x in the carrier of (pi_1 (Y, the Point of Y)) ) assume x in {(Class ((EqRel (Y, the Point of Y)),D))} ; ::_thesis: x in the carrier of (pi_1 (Y, the Point of Y)) then A9: x = Class ((EqRel (Y, the Point of Y)),D) by TARSKI:def_1; D in Loops the Point of Y by TOPALG_1:def_1; then x in Class (EqRel (Y, the Point of Y)) by A9, EQREL_1:def_3; hence x in the carrier of (pi_1 (Y, the Point of Y)) by TOPALG_1:def_5; ::_thesis: verum end; hence contradiction by A1; ::_thesis: verum 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: :: BROUWER:def 5 for x being Point of (Tdisk (o,r)) holds it . x = HC (x,f); existence ex b1 being Function of (Tdisk (o,r)),(Tcircle (o,r)) st for x being Point of (Tdisk (o,r)) holds b1 . x = HC (x,f) proof defpred S1[ 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 S1[x,m] ; ex h being Function of (Tdisk (o,r)),(Tcircle (o,r)) st for x being Point of (Tdisk (o,r)) holds S1[x,h . x] from FUNCT_2:sch_3(A1); hence ex b1 being Function of (Tdisk (o,r)),(Tcircle (o,r)) st for x being Point of (Tdisk (o,r)) holds b1 . x = HC (x,f) ; ::_thesis: verum end; uniqueness for b1, b2 being Function of (Tdisk (o,r)),(Tcircle (o,r)) st ( for x being Point of (Tdisk (o,r)) holds b1 . x = HC (x,f) ) & ( for x being Point of (Tdisk (o,r)) holds b2 . x = HC (x,f) ) holds b1 = b2 proof let f1, f2 be Function of (Tdisk (o,r)),(Tcircle (o,r)); ::_thesis: ( ( for x being Point of (Tdisk (o,r)) holds f1 . x = HC (x,f) ) & ( for x being Point of (Tdisk (o,r)) holds f2 . x = HC (x,f) ) implies f1 = f2 ) assume 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) ; ::_thesis: f1 = f2 for x being Point of (Tdisk (o,r)) holds f1 . x = f2 . x proof let x be Point of (Tdisk (o,r)); ::_thesis: f1 . x = f2 . x thus f1 . x = HC (x,f) by A2 .= f2 . x by A3 ; ::_thesis: verum end; hence f1 = f2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def5 defines BR-map BROUWER:def_5_:_ for n being non empty Element of NAT for r being non negative real number for o being Point of (TOP-REAL n) for f being Function of (Tdisk (o,r)),(Tdisk (o,r)) for b5 being Function of (Tdisk (o,r)),(Tcircle (o,r)) holds ( b5 = BR-map f iff for x being Point of (Tdisk (o,r)) holds b5 . x = HC (x,f) ); theorem Th11: :: BROUWER:11 for r being non negative real number for n being non empty Element of NAT for o being Point of (TOP-REAL n) for x being Point of (Tdisk (o,r)) for 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 r be non negative real number ; ::_thesis: for n being non empty Element of NAT for o being Point of (TOP-REAL n) for x being Point of (Tdisk (o,r)) for 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 let n be non empty Element of NAT ; ::_thesis: for o being Point of (TOP-REAL n) for x being Point of (Tdisk (o,r)) for 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 let o be Point of (TOP-REAL n); ::_thesis: for x being Point of (Tdisk (o,r)) for 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 let x be Point of (Tdisk (o,r)); ::_thesis: for 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 let f be Function of (Tdisk (o,r)),(Tdisk (o,r)); ::_thesis: ( not x is_a_fixpoint_of f & x is Point of (Tcircle (o,r)) implies (BR-map f) . x = x ) assume A1: ( not x is_a_fixpoint_of f & x is Point of (Tcircle (o,r)) ) ; ::_thesis: (BR-map f) . x = x thus (BR-map f) . x = HC (x,f) by Def5 .= x by A1, Th9 ; ::_thesis: verum end; theorem :: BROUWER:12 for r being non negative real number for n being non empty Element of NAT for o being Point of (TOP-REAL n) for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) st f is without_fixpoints holds (BR-map f) | (Sphere (o,r)) = id (Tcircle (o,r)) proof let r be non negative real number ; ::_thesis: for n being non empty Element of NAT for o being Point of (TOP-REAL n) for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) st f is without_fixpoints holds (BR-map f) | (Sphere (o,r)) = id (Tcircle (o,r)) let n be non empty Element of NAT ; ::_thesis: for o being Point of (TOP-REAL n) for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) st f is without_fixpoints holds (BR-map f) | (Sphere (o,r)) = id (Tcircle (o,r)) let o be Point of (TOP-REAL n); ::_thesis: for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) st f is without_fixpoints holds (BR-map f) | (Sphere (o,r)) = id (Tcircle (o,r)) let f be continuous Function of (Tdisk (o,r)),(Tdisk (o,r)); ::_thesis: ( f is without_fixpoints implies (BR-map f) | (Sphere (o,r)) = id (Tcircle (o,r)) ) assume A1: f is without_fixpoints ; ::_thesis: (BR-map f) | (Sphere (o,r)) = id (Tcircle (o,r)) set D = cl_Ball (o,r); set C = Sphere (o,r); set g = BR-map f; ( dom (BR-map f) = the carrier of (Tdisk (o,r)) & the carrier of (Tdisk (o,r)) = cl_Ball (o,r) ) by Th3, FUNCT_2:def_1; then A2: dom ((BR-map f) | (Sphere (o,r))) = Sphere (o,r) by RELAT_1:62, TOPREAL9:17; A3: the carrier of (Tcircle (o,r)) = Sphere (o,r) by TOPREALB:9; A4: for x being set st x in dom ((BR-map f) | (Sphere (o,r))) holds ((BR-map f) | (Sphere (o,r))) . x = (id (Tcircle (o,r))) . x proof let x be set ; ::_thesis: ( x in dom ((BR-map f) | (Sphere (o,r))) implies ((BR-map f) | (Sphere (o,r))) . x = (id (Tcircle (o,r))) . x ) assume A5: x in dom ((BR-map f) | (Sphere (o,r))) ; ::_thesis: ((BR-map f) | (Sphere (o,r))) . x = (id (Tcircle (o,r))) . x x in dom (BR-map f) 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 ((BR-map f) | (Sphere (o,r))) . x = (BR-map f) . x by A5, FUNCT_1:49 .= y by A3, A5, A6, Th11 .= (id (Tcircle (o,r))) . x by A3, A5, FUNCT_1:18 ; ::_thesis: verum end; dom (id (Tcircle (o,r))) = the carrier of (Tcircle (o,r)) by RELAT_1:45; hence (BR-map f) | (Sphere (o,r)) = id (Tcircle (o,r)) by A2, A3, A4, FUNCT_1:2; ::_thesis: verum end; Lm1: now__::_thesis:_for_T_being_non_empty_TopSpace for_a_being_Real_holds_the_carrier_of_T_-->_a_is_continuous let T be non empty TopSpace; ::_thesis: for a being Real holds the carrier of T --> a is continuous let a be Real; ::_thesis: the carrier of T --> a is continuous set c = the carrier of T; set f = the carrier of T --> a; thus the carrier of T --> a is continuous ::_thesis: verum proof let Y be Subset of REAL; :: according to PSCOMP_1:def_3 ::_thesis: ( not Y is closed or ( the carrier of T --> a) " Y is closed ) A1: dom ( the carrier of T --> a) = the carrier of T by FUNCT_2:def_1; assume Y is closed ; ::_thesis: ( the carrier of T --> a) " Y is closed A2: rng ( the carrier of T --> a) = {a} by FUNCOP_1:8; percases ( a in Y or not a in Y ) ; suppose a in Y ; ::_thesis: ( the carrier of T --> a) " Y is closed then A3: rng ( the carrier of T --> a) c= Y by A2, ZFMISC_1:31; ( the carrier of T --> a) " Y = ( the carrier of T --> a) " ((rng ( the carrier of T --> a)) /\ Y) by RELAT_1:133 .= ( the carrier of T --> a) " (rng ( the carrier of T --> a)) by A3, XBOOLE_1:28 .= [#] T by A1, RELAT_1:134 ; hence ( the carrier of T --> a) " Y is closed ; ::_thesis: verum end; suppose not a in Y ; ::_thesis: ( the carrier of T --> a) " Y is closed then A4: rng ( the carrier of T --> a) misses Y by A2, ZFMISC_1:50; ( the carrier of T --> a) " Y = ( the carrier of T --> a) " ((rng ( the carrier of T --> a)) /\ Y) by RELAT_1:133 .= ( the carrier of T --> a) " {} by A4, XBOOLE_0:def_7 .= {} T ; hence ( the carrier of T --> a) " Y is closed ; ::_thesis: verum end; end; end; end; theorem Th13: :: BROUWER:13 for r being positive real number for o being Point of (TOP-REAL 2) for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) st f is without_fixpoints holds BR-map f is continuous proof set R = R2Homeomorphism ; defpred S1[ set , set ] means ex x1, x2 being Point of (TOP-REAL 2) st ( $1 = [x1,x2] & $2 = x2 `1 ); defpred S2[ set , set ] means ex x1, x2 being Point of (TOP-REAL 2) st ( $1 = [x1,x2] & $2 = (x1 `1) - (x2 `1) ); let r be positive real number ; ::_thesis: for o being Point of (TOP-REAL 2) for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) st f is without_fixpoints holds BR-map f is continuous let o be Point of (TOP-REAL 2); ::_thesis: for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) st f is without_fixpoints holds BR-map f is continuous defpred S3[ set , set ] means ex x1, x2 being Point of (TOP-REAL 2) st ( $1 = [x1,x2] & $2 = (x2 `1) - (o `1) ); defpred S4[ set , set ] means ex x1, x2 being Point of (TOP-REAL 2) 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 [:(TOP-REAL 2),(TOP-REAL 2):] --> rr; A1: for x being Element of [:(TOP-REAL 2),(TOP-REAL 2):] ex r being Real st S3[x,r] proof let x be Element of [:(TOP-REAL 2),(TOP-REAL 2):]; ::_thesis: ex r being Real st S3[x,r] consider x1, x2 being Point of (TOP-REAL 2) such that A2: x = [x1,x2] by BORSUK_1:10; take (x2 `1) - (o `1) ; ::_thesis: S3[x,(x2 `1) - (o `1)] take x1 ; ::_thesis: ex x2 being Point of (TOP-REAL 2) st ( x = [x1,x2] & (x2 `1) - (o `1) = (x2 `1) - (o `1) ) take x2 ; ::_thesis: ( x = [x1,x2] & (x2 `1) - (o `1) = (x2 `1) - (o `1) ) thus ( x = [x1,x2] & (x2 `1) - (o `1) = (x2 `1) - (o `1) ) by A2; ::_thesis: verum end; consider xo being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] such that A3: for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds S3[x,xo . x] from FUNCT_2:sch_3(A1); A4: for x being Element of [:(TOP-REAL 2),(TOP-REAL 2):] ex r being Real st S1[x,r] proof let x be Element of [:(TOP-REAL 2),(TOP-REAL 2):]; ::_thesis: ex r being Real st S1[x,r] consider x1, x2 being Point of (TOP-REAL 2) such that A5: x = [x1,x2] by BORSUK_1:10; take x2 `1 ; ::_thesis: S1[x,x2 `1 ] take x1 ; ::_thesis: ex x2 being Point of (TOP-REAL 2) st ( x = [x1,x2] & x2 `1 = x2 `1 ) take x2 ; ::_thesis: ( x = [x1,x2] & x2 `1 = x2 `1 ) thus ( x = [x1,x2] & x2 `1 = x2 `1 ) by A5; ::_thesis: verum end; consider fx2 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] such that A6: for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds S1[x,fx2 . x] from FUNCT_2:sch_3(A4); A7: for x being Element of [:(TOP-REAL 2),(TOP-REAL 2):] ex r being Real st S4[x,r] proof let x be Element of [:(TOP-REAL 2),(TOP-REAL 2):]; ::_thesis: ex r being Real st S4[x,r] consider x1, x2 being Point of (TOP-REAL 2) such that A8: x = [x1,x2] by BORSUK_1:10; take (x2 `2) - (o `2) ; ::_thesis: S4[x,(x2 `2) - (o `2)] take x1 ; ::_thesis: ex x2 being Point of (TOP-REAL 2) st ( x = [x1,x2] & (x2 `2) - (o `2) = (x2 `2) - (o `2) ) take x2 ; ::_thesis: ( x = [x1,x2] & (x2 `2) - (o `2) = (x2 `2) - (o `2) ) thus ( x = [x1,x2] & (x2 `2) - (o `2) = (x2 `2) - (o `2) ) by A8; ::_thesis: verum end; consider yo being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] such that A9: for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds S4[x,yo . x] from FUNCT_2:sch_3(A7); reconsider f1 = the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] --> rr as continuous RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] by Lm1; set D2 = Tdisk (o,r); set S1 = Tcircle (o,r); set OK = (DiffElems ((TOP-REAL 2),(TOP-REAL 2))) /\ the carrier of [:(Tdisk (o,r)),(Tdisk (o,r)):]; set s = the Point of (Tcircle (o,r)); A10: |.(o - o).| = |.(0. (TOP-REAL 2)).| by EUCLID:42 .= 0 by TOPRNS_1:23 ; A11: the carrier of (Tcircle (o,r)) = Sphere (o,r) by TOPREALB:9; A12: now__::_thesis:_not_o_=_the_Point_of_(Tcircle_(o,r)) assume A13: o = the Point of (Tcircle (o,r)) ; ::_thesis: contradiction ( 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; ::_thesis: verum end; the carrier of (Tdisk (o,r)) = cl_Ball (o,r) by Th3; then A14: o is Point of (Tdisk (o,r)) by A10, TOPREAL9:8; ( the Point of (Tcircle (o,r)) in the carrier of (Tcircle (o,r)) & Sphere (o,r) c= cl_Ball (o,r) ) by TOPREAL9:17; then the Point of (Tcircle (o,r)) is Point of (Tdisk (o,r)) by A11, Th3; then [o, the Point of (Tcircle (o,r))] in [: the carrier of (Tdisk (o,r)), the carrier of (Tdisk (o,r)):] by A14, ZFMISC_1:87; then A15: [o, the Point of (Tcircle (o,r))] in the carrier of [:(Tdisk (o,r)),(Tdisk (o,r)):] by BORSUK_1:def_2; the Point of (Tcircle (o,r)) is Point of (TOP-REAL 2) by PRE_TOPC:25; then [o, the Point of (Tcircle (o,r))] in DiffElems ((TOP-REAL 2),(TOP-REAL 2)) by A12; then reconsider OK = (DiffElems ((TOP-REAL 2),(TOP-REAL 2))) /\ the carrier of [:(Tdisk (o,r)),(Tdisk (o,r)):] as non empty Subset of [:(TOP-REAL 2),(TOP-REAL 2):] by A15, XBOOLE_0:def_4; set Zf1 = f1 | OK; defpred S5[ set , set ] means ex x1, x2 being Point of (TOP-REAL 2) st ( $1 = [x1,x2] & $2 = x2 `2 ); defpred S6[ set , set ] means ex y1, y2 being Point of (TOP-REAL 2) st ( $1 = [y1,y2] & $2 = (y1 `2) - (y2 `2) ); set TD = [:(TOP-REAL 2),(TOP-REAL 2):] | OK; let f be continuous Function of (Tdisk (o,r)),(Tdisk (o,r)); ::_thesis: ( f is without_fixpoints implies BR-map f is continuous ) assume A16: f is without_fixpoints ; ::_thesis: BR-map f is continuous A17: for x being Element of [:(TOP-REAL 2),(TOP-REAL 2):] ex r being Real st S6[x,r] proof let x be Element of [:(TOP-REAL 2),(TOP-REAL 2):]; ::_thesis: ex r being Real st S6[x,r] consider x1, x2 being Point of (TOP-REAL 2) such that A18: x = [x1,x2] by BORSUK_1:10; take (x1 `2) - (x2 `2) ; ::_thesis: S6[x,(x1 `2) - (x2 `2)] take x1 ; ::_thesis: ex y2 being Point of (TOP-REAL 2) st ( x = [x1,y2] & (x1 `2) - (x2 `2) = (x1 `2) - (y2 `2) ) take x2 ; ::_thesis: ( x = [x1,x2] & (x1 `2) - (x2 `2) = (x1 `2) - (x2 `2) ) thus ( x = [x1,x2] & (x1 `2) - (x2 `2) = (x1 `2) - (x2 `2) ) by A18; ::_thesis: verum end; consider dy being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] such that A19: for y being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds S6[y,dy . y] from FUNCT_2:sch_3(A17); A20: for x being Element of [:(TOP-REAL 2),(TOP-REAL 2):] ex r being Real st S5[x,r] proof let x be Element of [:(TOP-REAL 2),(TOP-REAL 2):]; ::_thesis: ex r being Real st S5[x,r] consider x1, x2 being Point of (TOP-REAL 2) such that A21: x = [x1,x2] by BORSUK_1:10; take x2 `2 ; ::_thesis: S5[x,x2 `2 ] take x1 ; ::_thesis: ex x2 being Point of (TOP-REAL 2) st ( x = [x1,x2] & x2 `2 = x2 `2 ) take x2 ; ::_thesis: ( x = [x1,x2] & x2 `2 = x2 `2 ) thus ( x = [x1,x2] & x2 `2 = x2 `2 ) by A21; ::_thesis: verum end; consider fy2 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] such that A22: for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds S5[x,fy2 . x] from FUNCT_2:sch_3(A20); A23: for x being Element of [:(TOP-REAL 2),(TOP-REAL 2):] ex r being Real st S2[x,r] proof let x be Element of [:(TOP-REAL 2),(TOP-REAL 2):]; ::_thesis: ex r being Real st S2[x,r] consider x1, x2 being Point of (TOP-REAL 2) such that A24: x = [x1,x2] by BORSUK_1:10; take (x1 `1) - (x2 `1) ; ::_thesis: S2[x,(x1 `1) - (x2 `1)] take x1 ; ::_thesis: ex x2 being Point of (TOP-REAL 2) st ( x = [x1,x2] & (x1 `1) - (x2 `1) = (x1 `1) - (x2 `1) ) take x2 ; ::_thesis: ( x = [x1,x2] & (x1 `1) - (x2 `1) = (x1 `1) - (x2 `1) ) thus ( x = [x1,x2] & (x1 `1) - (x2 `1) = (x1 `1) - (x2 `1) ) by A24; ::_thesis: verum end; consider dx being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] such that A25: for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds S2[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 [:(TOP-REAL 2),(TOP-REAL 2):],R^1 by TOPMETR:17; for p being Point of [:(TOP-REAL 2),(TOP-REAL 2):] for V being Subset of R^1 st Yo . p in V & V is open holds ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st ( p in W & W is open & Yo .: W c= V ) proof let p be Point of [:(TOP-REAL 2),(TOP-REAL 2):]; ::_thesis: for V being Subset of R^1 st Yo . p in V & V is open holds ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st ( p in W & W is open & Yo .: W c= V ) let V be Subset of R^1; ::_thesis: ( Yo . p in V & V is open implies ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st ( p in W & W is open & Yo .: W c= V ) ) assume that A26: Yo . p in V and A27: V is open ; ::_thesis: ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st ( p in W & W is open & Yo .: W c= V ) reconsider V1 = V as open Subset of REAL by A27, BORSUK_5:39, TOPMETR:17; consider p1, p2 being Point of (TOP-REAL 2) 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: ].(((p2 `2) - (o `2)) - g),(((p2 `2) - (o `2)) + g).[ c= V1 by A26, A29, RCOMP_1:19; reconsider g = 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 ) } ; { |[x,y]| where x, y is Element of REAL : ( (p2 `2) - g < y & y < (p2 `2) + g ) } c= the carrier of (TOP-REAL 2) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { |[x,y]| where x, y is Element of REAL : ( (p2 `2) - g < y & y < (p2 `2) + g ) } or a in the carrier of (TOP-REAL 2) ) assume a in { |[x,y]| where x, y is Element of REAL : ( (p2 `2) - g < y & y < (p2 `2) + g ) } ; ::_thesis: a in the carrier of (TOP-REAL 2) then ex x, y being Element of REAL st ( a = |[x,y]| & (p2 `2) - g < y & y < (p2 `2) + g ) ; hence a in the carrier of (TOP-REAL 2) ; ::_thesis: verum end; then reconsider W2 = { |[x,y]| where x, y is Element of REAL : ( (p2 `2) - g < y & y < (p2 `2) + g ) } as Subset of (TOP-REAL 2) ; take [:([#] (TOP-REAL 2)),W2:] ; ::_thesis: ( p in [:([#] (TOP-REAL 2)),W2:] & [:([#] (TOP-REAL 2)),W2:] is open & Yo .: [:([#] (TOP-REAL 2)),W2:] c= V ) A32: p2 = |[(p2 `1),(p2 `2)]| by EUCLID:53; ( (p2 `2) - g < (p2 `2) - 0 & (p2 `2) + 0 < (p2 `2) + g ) by A30, XREAL_1:6, XREAL_1:15; then p2 in W2 by A32; hence p in [:([#] (TOP-REAL 2)),W2:] by A28, ZFMISC_1:def_2; ::_thesis: ( [:([#] (TOP-REAL 2)),W2:] is open & Yo .: [:([#] (TOP-REAL 2)),W2:] c= V ) W2 is open by PSCOMP_1:21; hence [:([#] (TOP-REAL 2)),W2:] is open by BORSUK_1:6; ::_thesis: Yo .: [:([#] (TOP-REAL 2)),W2:] c= V let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Yo .: [:([#] (TOP-REAL 2)),W2:] or b in V ) assume b in Yo .: [:([#] (TOP-REAL 2)),W2:] ; ::_thesis: b in V then consider a being Point of [:(TOP-REAL 2),(TOP-REAL 2):] such that A33: a in [:([#] (TOP-REAL 2)),W2:] and A34: Yo . a = b by FUNCT_2:65; consider a1, a2 being Point of (TOP-REAL 2) 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 ].(((p2 `2) - (o `2)) - g),(((p2 `2) - (o `2)) + g).[ by XXREAL_1:4; hence b in V by A31, A34, A36; ::_thesis: verum end; then Yo is continuous by JGRAPH_2:10; then reconsider yo = yo as continuous RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] by JORDAN5A:27; for p being Point of [:(TOP-REAL 2),(TOP-REAL 2):] for V being Subset of R^1 st Xo . p in V & V is open holds ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st ( p in W & W is open & Xo .: W c= V ) proof let p be Point of [:(TOP-REAL 2),(TOP-REAL 2):]; ::_thesis: for V being Subset of R^1 st Xo . p in V & V is open holds ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st ( p in W & W is open & Xo .: W c= V ) let V be Subset of R^1; ::_thesis: ( Xo . p in V & V is open implies ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st ( p in W & W is open & Xo .: W c= V ) ) assume that A39: Xo . p in V and A40: V is open ; ::_thesis: ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st ( p in W & W is open & Xo .: W c= V ) reconsider V1 = V as open Subset of REAL by A40, BORSUK_5:39, TOPMETR:17; consider p1, p2 being Point of (TOP-REAL 2) 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: ].(((p2 `1) - (o `1)) - g),(((p2 `1) - (o `1)) + g).[ c= V1 by A39, A42, RCOMP_1:19; reconsider g = 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 ) } ; { |[x,y]| where x, y is Element of REAL : ( (p2 `1) - g < x & x < (p2 `1) + g ) } c= the carrier of (TOP-REAL 2) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { |[x,y]| where x, y is Element of REAL : ( (p2 `1) - g < x & x < (p2 `1) + g ) } or a in the carrier of (TOP-REAL 2) ) assume a in { |[x,y]| where x, y is Element of REAL : ( (p2 `1) - g < x & x < (p2 `1) + g ) } ; ::_thesis: a in the carrier of (TOP-REAL 2) then ex x, y being Element of REAL st ( a = |[x,y]| & (p2 `1) - g < x & x < (p2 `1) + g ) ; hence a in the carrier of (TOP-REAL 2) ; ::_thesis: verum end; then reconsider W2 = { |[x,y]| where x, y is Element of REAL : ( (p2 `1) - g < x & x < (p2 `1) + g ) } as Subset of (TOP-REAL 2) ; take [:([#] (TOP-REAL 2)),W2:] ; ::_thesis: ( p in [:([#] (TOP-REAL 2)),W2:] & [:([#] (TOP-REAL 2)),W2:] is open & Xo .: [:([#] (TOP-REAL 2)),W2:] c= V ) A45: p2 = |[(p2 `1),(p2 `2)]| by EUCLID:53; ( (p2 `1) - g < (p2 `1) - 0 & (p2 `1) + 0 < (p2 `1) + g ) by A43, XREAL_1:6, XREAL_1:15; then p2 in W2 by A45; hence p in [:([#] (TOP-REAL 2)),W2:] by A41, ZFMISC_1:def_2; ::_thesis: ( [:([#] (TOP-REAL 2)),W2:] is open & Xo .: [:([#] (TOP-REAL 2)),W2:] c= V ) W2 is open by PSCOMP_1:19; hence [:([#] (TOP-REAL 2)),W2:] is open by BORSUK_1:6; ::_thesis: Xo .: [:([#] (TOP-REAL 2)),W2:] c= V let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Xo .: [:([#] (TOP-REAL 2)),W2:] or b in V ) assume b in Xo .: [:([#] (TOP-REAL 2)),W2:] ; ::_thesis: b in V then consider a being Point of [:(TOP-REAL 2),(TOP-REAL 2):] such that A46: a in [:([#] (TOP-REAL 2)),W2:] and A47: Xo . a = b by FUNCT_2:65; consider a1, a2 being Point of (TOP-REAL 2) 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 ].(((p2 `1) - (o `1)) - g),(((p2 `1) - (o `1)) + g).[ by XXREAL_1:4; hence b in V by A44, A47, A49; ::_thesis: verum end; then Xo is continuous by JGRAPH_2:10; then reconsider xo = xo as continuous RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] by JORDAN5A:27; set Zyo = yo | OK; set Zxo = xo | OK; set p2 = (((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK); set g = BR-map f; A52: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) = OK by PRE_TOPC:8; for p being Point of [:(TOP-REAL 2),(TOP-REAL 2):] for V being Subset of R^1 st Dy . p in V & V is open holds ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st ( p in W & W is open & Dy .: W c= V ) proof let p be Point of [:(TOP-REAL 2),(TOP-REAL 2):]; ::_thesis: for V being Subset of R^1 st Dy . p in V & V is open holds ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st ( p in W & W is open & Dy .: W c= V ) let V be Subset of R^1; ::_thesis: ( Dy . p in V & V is open implies ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st ( p in W & W is open & Dy .: W c= V ) ) assume that A53: Dy . p in V and A54: V is open ; ::_thesis: ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st ( p in W & W is open & Dy .: W c= V ) reconsider V1 = V as open Subset of REAL by A54, BORSUK_5:39, TOPMETR:17; consider p1, p2 being Point of (TOP-REAL 2) 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: ].(((p1 `2) - (p2 `2)) - g),(((p1 `2) - (p2 `2)) + g).[ c= V1 by A53, A56, RCOMP_1:19; reconsider g = 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: { |[x,y]| where x, y is Element of REAL : ( (p2 `2) - (g / 2) < y & y < (p2 `2) + (g / 2) ) } c= the carrier of (TOP-REAL 2) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { |[x,y]| where x, y is Element of REAL : ( (p2 `2) - (g / 2) < y & y < (p2 `2) + (g / 2) ) } or a in the carrier of (TOP-REAL 2) ) assume a in { |[x,y]| where x, y is Element of REAL : ( (p2 `2) - (g / 2) < y & y < (p2 `2) + (g / 2) ) } ; ::_thesis: a in the carrier of (TOP-REAL 2) then ex x, y being Element of REAL st ( a = |[x,y]| & (p2 `2) - (g / 2) < y & y < (p2 `2) + (g / 2) ) ; hence a in the carrier of (TOP-REAL 2) ; ::_thesis: verum end; A60: p2 = |[(p2 `1),(p2 `2)]| by EUCLID:53; reconsider W2 = { |[x,y]| where x, y is Element of REAL : ( (p2 `2) - (g / 2) < y & y < (p2 `2) + (g / 2) ) } as Subset of (TOP-REAL 2) by A59; A61: 0 / 2 < g / 2 by A57, XREAL_1:74; then ( (p2 `2) - (g / 2) < (p2 `2) - 0 & (p2 `2) + 0 < (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 is Element of REAL : ( (p1 `2) - (g / 2) < y & y < (p1 `2) + (g / 2) ) } ; { |[x,y]| where x, y is Element of REAL : ( (p1 `2) - (g / 2) < y & y < (p1 `2) + (g / 2) ) } c= the carrier of (TOP-REAL 2) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { |[x,y]| where x, y is Element of REAL : ( (p1 `2) - (g / 2) < y & y < (p1 `2) + (g / 2) ) } or a in the carrier of (TOP-REAL 2) ) assume a in { |[x,y]| where x, y is Element of REAL : ( (p1 `2) - (g / 2) < y & y < (p1 `2) + (g / 2) ) } ; ::_thesis: a in the carrier of (TOP-REAL 2) then ex x, y being Element of REAL st ( a = |[x,y]| & (p1 `2) - (g / 2) < y & y < (p1 `2) + (g / 2) ) ; hence a in the carrier of (TOP-REAL 2) ; ::_thesis: verum end; then reconsider W1 = { |[x,y]| where x, y is Element of REAL : ( (p1 `2) - (g / 2) < y & y < (p1 `2) + (g / 2) ) } as Subset of (TOP-REAL 2) ; take [:W1,W2:] ; ::_thesis: ( p in [:W1,W2:] & [:W1,W2:] is open & Dy .: [:W1,W2:] c= V ) A63: p1 = |[(p1 `1),(p1 `2)]| by EUCLID:53; ( (p1 `2) - (g / 2) < (p1 `2) - 0 & (p1 `2) + 0 < (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; ::_thesis: ( [:W1,W2:] is open & Dy .: [:W1,W2:] c= V ) ( W1 is open & W2 is open ) by PSCOMP_1:21; hence [:W1,W2:] is open by BORSUK_1:6; ::_thesis: Dy .: [:W1,W2:] c= V let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Dy .: [:W1,W2:] or b in V ) assume b in Dy .: [:W1,W2:] ; ::_thesis: b in V then consider a being Point of [:(TOP-REAL 2),(TOP-REAL 2):] such that A64: a in [:W1,W2:] and A65: Dy . a = b by FUNCT_2:65; consider a1, a2 being Point of (TOP-REAL 2) 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) - ((p1 `2) - (p2 `2))) < g by A78, XXREAL_0:2; a1 `2 = y1 by A74, EUCLID:52; then (a1 `2) - (a2 `2) in ].(((p1 `2) - (p2 `2)) - g),(((p1 `2) - (p2 `2)) + g).[ by A71, A79, RCOMP_1:1; hence b in V by A58, A65, A67; ::_thesis: verum end; then Dy is continuous by JGRAPH_2:10; then reconsider dy = dy as continuous RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] by JORDAN5A:27; for p being Point of [:(TOP-REAL 2),(TOP-REAL 2):] for V being Subset of R^1 st Dx . p in V & V is open holds ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st ( p in W & W is open & Dx .: W c= V ) proof let p be Point of [:(TOP-REAL 2),(TOP-REAL 2):]; ::_thesis: for V being Subset of R^1 st Dx . p in V & V is open holds ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st ( p in W & W is open & Dx .: W c= V ) let V be Subset of R^1; ::_thesis: ( Dx . p in V & V is open implies ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st ( p in W & W is open & Dx .: W c= V ) ) assume that A80: Dx . p in V and A81: V is open ; ::_thesis: ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st ( p in W & W is open & Dx .: W c= V ) reconsider V1 = V as open Subset of REAL by A81, BORSUK_5:39, TOPMETR:17; consider p1, p2 being Point of (TOP-REAL 2) 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: ].(((p1 `1) - (p2 `1)) - g),(((p1 `1) - (p2 `1)) + g).[ c= V1 by A80, A83, RCOMP_1:19; reconsider g = 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: { |[x,y]| where x, y is Element of REAL : ( (p2 `1) - (g / 2) < x & x < (p2 `1) + (g / 2) ) } c= the carrier of (TOP-REAL 2) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { |[x,y]| where x, y is Element of REAL : ( (p2 `1) - (g / 2) < x & x < (p2 `1) + (g / 2) ) } or a in the carrier of (TOP-REAL 2) ) assume a in { |[x,y]| where x, y is Element of REAL : ( (p2 `1) - (g / 2) < x & x < (p2 `1) + (g / 2) ) } ; ::_thesis: a in the carrier of (TOP-REAL 2) then ex x, y being Element of REAL st ( a = |[x,y]| & (p2 `1) - (g / 2) < x & x < (p2 `1) + (g / 2) ) ; hence a in the carrier of (TOP-REAL 2) ; ::_thesis: verum end; A87: p2 = |[(p2 `1),(p2 `2)]| by EUCLID:53; reconsider W2 = { |[x,y]| where x, y is Element of REAL : ( (p2 `1) - (g / 2) < x & x < (p2 `1) + (g / 2) ) } as Subset of (TOP-REAL 2) by A86; A88: 0 / 2 < g / 2 by A84, XREAL_1:74; then ( (p2 `1) - (g / 2) < (p2 `1) - 0 & (p2 `1) + 0 < (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 is Element of REAL : ( (p1 `1) - (g / 2) < x & x < (p1 `1) + (g / 2) ) } ; { |[x,y]| where x, y is Element of REAL : ( (p1 `1) - (g / 2) < x & x < (p1 `1) + (g / 2) ) } c= the carrier of (TOP-REAL 2) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { |[x,y]| where x, y is Element of REAL : ( (p1 `1) - (g / 2) < x & x < (p1 `1) + (g / 2) ) } or a in the carrier of (TOP-REAL 2) ) assume a in { |[x,y]| where x, y is Element of REAL : ( (p1 `1) - (g / 2) < x & x < (p1 `1) + (g / 2) ) } ; ::_thesis: a in the carrier of (TOP-REAL 2) then ex x, y being Element of REAL st ( a = |[x,y]| & (p1 `1) - (g / 2) < x & x < (p1 `1) + (g / 2) ) ; hence a in the carrier of (TOP-REAL 2) ; ::_thesis: verum end; then reconsider W1 = { |[x,y]| where x, y is Element of REAL : ( (p1 `1) - (g / 2) < x & x < (p1 `1) + (g / 2) ) } as Subset of (TOP-REAL 2) ; take [:W1,W2:] ; ::_thesis: ( p in [:W1,W2:] & [:W1,W2:] is open & Dx .: [:W1,W2:] c= V ) A90: p1 = |[(p1 `1),(p1 `2)]| by EUCLID:53; ( (p1 `1) - (g / 2) < (p1 `1) - 0 & (p1 `1) + 0 < (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; ::_thesis: ( [:W1,W2:] is open & Dx .: [:W1,W2:] c= V ) ( W1 is open & W2 is open ) by PSCOMP_1:19; hence [:W1,W2:] is open by BORSUK_1:6; ::_thesis: Dx .: [:W1,W2:] c= V let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Dx .: [:W1,W2:] or b in V ) assume b in Dx .: [:W1,W2:] ; ::_thesis: b in V then consider a being Point of [:(TOP-REAL 2),(TOP-REAL 2):] such that A91: a in [:W1,W2:] and A92: Dx . a = b by FUNCT_2:65; consider a1, a2 being Point of (TOP-REAL 2) 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) - ((p1 `1) - (p2 `1))) < g by A105, XXREAL_0:2; a1 `1 = x1 by A101, EUCLID:52; then (a1 `1) - (a2 `1) in ].(((p1 `1) - (p2 `1)) - g),(((p1 `1) - (p2 `1)) + g).[ by A98, A106, RCOMP_1:1; hence b in V by A85, A92, A94; ::_thesis: verum end; then Dx is continuous by JGRAPH_2:10; then reconsider dx = dx as continuous RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] by JORDAN5A:27; set Zdy = dy | OK; set Zdx = dx | OK; set m = ((dx | OK) (#) (dx | OK)) + ((dy | OK) (#) (dy | OK)); for p being Point of [:(TOP-REAL 2),(TOP-REAL 2):] for V being Subset of R^1 st fY2 . p in V & V is open holds ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st ( p in W & W is open & fY2 .: W c= V ) proof let p be Point of [:(TOP-REAL 2),(TOP-REAL 2):]; ::_thesis: for V being Subset of R^1 st fY2 . p in V & V is open holds ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st ( p in W & W is open & fY2 .: W c= V ) let V be Subset of R^1; ::_thesis: ( fY2 . p in V & V is open implies ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st ( p in W & W is open & fY2 .: W c= V ) ) assume that A107: fY2 . p in V and A108: V is open ; ::_thesis: ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st ( p in W & W is open & fY2 .: W c= V ) reconsider V1 = V as open Subset of REAL by A108, BORSUK_5:39, TOPMETR:17; consider p1, p2 being Point of (TOP-REAL 2) 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 = 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 ) } ; { |[x,y]| where x, y is Element of REAL : ( (p2 `2) - g < y & y < (p2 `2) + g ) } c= the carrier of (TOP-REAL 2) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { |[x,y]| where x, y is Element of REAL : ( (p2 `2) - g < y & y < (p2 `2) + g ) } or a in the carrier of (TOP-REAL 2) ) assume a in { |[x,y]| where x, y is Element of REAL : ( (p2 `2) - g < y & y < (p2 `2) + g ) } ; ::_thesis: a in the carrier of (TOP-REAL 2) then ex x, y being Element of REAL st ( a = |[x,y]| & (p2 `2) - g < y & y < (p2 `2) + g ) ; hence a in the carrier of (TOP-REAL 2) ; ::_thesis: verum end; then reconsider W1 = { |[x,y]| where x, y is Element of REAL : ( (p2 `2) - g < y & y < (p2 `2) + g ) } as Subset of (TOP-REAL 2) ; take [:([#] (TOP-REAL 2)),W1:] ; ::_thesis: ( p in [:([#] (TOP-REAL 2)),W1:] & [:([#] (TOP-REAL 2)),W1:] is open & fY2 .: [:([#] (TOP-REAL 2)),W1:] c= V ) A113: p2 = |[(p2 `1),(p2 `2)]| by EUCLID:53; ( (p2 `2) - g < (p2 `2) - 0 & (p2 `2) + 0 < (p2 `2) + g ) by A111, XREAL_1:6, XREAL_1:15; then p2 in W1 by A113; hence p in [:([#] (TOP-REAL 2)),W1:] by A109, ZFMISC_1:def_2; ::_thesis: ( [:([#] (TOP-REAL 2)),W1:] is open & fY2 .: [:([#] (TOP-REAL 2)),W1:] c= V ) W1 is open by PSCOMP_1:21; hence [:([#] (TOP-REAL 2)),W1:] is open by BORSUK_1:6; ::_thesis: fY2 .: [:([#] (TOP-REAL 2)),W1:] c= V let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in fY2 .: [:([#] (TOP-REAL 2)),W1:] or b in V ) assume b in fY2 .: [:([#] (TOP-REAL 2)),W1:] ; ::_thesis: b in V then consider a being Point of [:(TOP-REAL 2),(TOP-REAL 2):] such that A114: a in [:([#] (TOP-REAL 2)),W1:] and A115: fY2 . a = b by FUNCT_2:65; consider a1, a2 being Point of (TOP-REAL 2) 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 b in V by A112, A115, A117; ::_thesis: verum end; then fY2 is continuous by JGRAPH_2:10; then reconsider fy2 = fy2 as continuous RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] by JORDAN5A:27; for p being Point of [:(TOP-REAL 2),(TOP-REAL 2):] for V being Subset of R^1 st fX2 . p in V & V is open holds ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st ( p in W & W is open & fX2 .: W c= V ) proof let p be Point of [:(TOP-REAL 2),(TOP-REAL 2):]; ::_thesis: for V being Subset of R^1 st fX2 . p in V & V is open holds ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st ( p in W & W is open & fX2 .: W c= V ) let V be Subset of R^1; ::_thesis: ( fX2 . p in V & V is open implies ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st ( p in W & W is open & fX2 .: W c= V ) ) assume that A123: fX2 . p in V and A124: V is open ; ::_thesis: ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st ( p in W & W is open & fX2 .: W c= V ) reconsider V1 = V as open Subset of REAL by A124, BORSUK_5:39, TOPMETR:17; consider p1, p2 being Point of (TOP-REAL 2) 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 = 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 ) } ; { |[x,y]| where x, y is Element of REAL : ( (p2 `1) - g < x & x < (p2 `1) + g ) } c= the carrier of (TOP-REAL 2) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { |[x,y]| where x, y is Element of REAL : ( (p2 `1) - g < x & x < (p2 `1) + g ) } or a in the carrier of (TOP-REAL 2) ) assume a in { |[x,y]| where x, y is Element of REAL : ( (p2 `1) - g < x & x < (p2 `1) + g ) } ; ::_thesis: a in the carrier of (TOP-REAL 2) then ex x, y being Element of REAL st ( a = |[x,y]| & (p2 `1) - g < x & x < (p2 `1) + g ) ; hence a in the carrier of (TOP-REAL 2) ; ::_thesis: verum end; then reconsider W1 = { |[x,y]| where x, y is Element of REAL : ( (p2 `1) - g < x & x < (p2 `1) + g ) } as Subset of (TOP-REAL 2) ; take [:([#] (TOP-REAL 2)),W1:] ; ::_thesis: ( p in [:([#] (TOP-REAL 2)),W1:] & [:([#] (TOP-REAL 2)),W1:] is open & fX2 .: [:([#] (TOP-REAL 2)),W1:] c= V ) A129: p2 = |[(p2 `1),(p2 `2)]| by EUCLID:53; ( (p2 `1) - g < (p2 `1) - 0 & (p2 `1) + 0 < (p2 `1) + g ) by A127, XREAL_1:6, XREAL_1:15; then p2 in W1 by A129; hence p in [:([#] (TOP-REAL 2)),W1:] by A125, ZFMISC_1:def_2; ::_thesis: ( [:([#] (TOP-REAL 2)),W1:] is open & fX2 .: [:([#] (TOP-REAL 2)),W1:] c= V ) W1 is open by PSCOMP_1:19; hence [:([#] (TOP-REAL 2)),W1:] is open by BORSUK_1:6; ::_thesis: fX2 .: [:([#] (TOP-REAL 2)),W1:] c= V let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in fX2 .: [:([#] (TOP-REAL 2)),W1:] or b in V ) assume b in fX2 .: [:([#] (TOP-REAL 2)),W1:] ; ::_thesis: b in V then consider a being Point of [:(TOP-REAL 2),(TOP-REAL 2):] such that A130: a in [:([#] (TOP-REAL 2)),W1:] and A131: fX2 . a = b by FUNCT_2:65; consider a1, a2 being Point of (TOP-REAL 2) 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 b in V by A128, A131, A133; ::_thesis: verum end; then fX2 is continuous by JGRAPH_2:10; then reconsider fx2 = fx2 as continuous RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] by JORDAN5A:27; set yy = (yo | OK) (#) (dy | OK); set xx = (xo | OK) (#) (dx | OK); set Zfy2 = fy2 | OK; set Zfx2 = fx2 | OK; set p1 = (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))); A139: dom ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK)) = the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) by FUNCT_2:def_1; A140: for y, z being Point of (Tdisk (o,r)) st y <> z holds [y,z] in OK proof let y, z be Point of (Tdisk (o,r)); ::_thesis: ( y <> z implies [y,z] in OK ) A141: ( y is Point of (TOP-REAL 2) & z is Point of (TOP-REAL 2) ) by PRE_TOPC:25; assume y <> z ; ::_thesis: [y,z] in OK then [y,z] in DiffElems ((TOP-REAL 2),(TOP-REAL 2)) by A141; hence [y,z] in OK by XBOOLE_0:def_4; ::_thesis: verum end; A142: now__::_thesis:_for_b_being_real_number_st_b_in_rng_((((xo_|_OK)_(#)_(xo_|_OK))_+_((yo_|_OK)_(#)_(yo_|_OK)))_-_(f1_|_OK))_holds_ 0_>=_b let b be real number ; ::_thesis: ( b in rng ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK)) implies 0 >= b ) assume b in rng ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK)) ; ::_thesis: 0 >= b then consider a being set such that A143: a in dom ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK)) and A144: ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK)) . a = b by FUNCT_1:def_3; a in DiffElems ((TOP-REAL 2),(TOP-REAL 2)) by A143, XBOOLE_0:def_4; then consider y, z being Point of (TOP-REAL 2) such that A145: a = [y,z] and A146: y <> z ; a in the carrier of [:(Tdisk (o,r)),(Tdisk (o,r)):] by A143, XBOOLE_0:def_4; then consider a1, a2 being Point of (Tdisk (o,r)) 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: (f1 | OK) . [y,z] = f1 . [y,z] by A140, A146, A148, FUNCT_1:49; set r3 = (z `1) - (o `1); set r4 = (z `2) - (o `2); consider x9, x10 being Point of (TOP-REAL 2) 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 (Tdisk (o,r)) = 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 (TOP-REAL 2) 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: ( (xo | OK) . [y,z] = xo . [y,z] & (yo | OK) . [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 .= (((z `1) - (o `1)) ^2) + (((z - o) `2) ^2) by TOPREAL3:3 .= (((z `1) - (o `1)) ^2) + (((z `2) - (o `2)) ^2) by TOPREAL3:3 ; then A159: ((((z `1) - (o `1)) ^2) + (((z `2) - (o `2)) ^2)) - (r ^2) <= (r ^2) - (r ^2) by A154, XREAL_1:9; A160: [y,z] is Element of [#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) by A143, A145, PRE_TOPC:def_5; ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK)) . [y,z] = ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) . [y,z]) - ((f1 | OK) . [y,z]) by A143, A145, VALUED_1:13 .= ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) . [y,z]) - (r ^2) by A150, FUNCOP_1:7 .= ((((xo | OK) (#) (xo | OK)) . [y,z]) + (((yo | OK) (#) (yo | OK)) . [y,z])) - (r ^2) by A160, VALUED_1:1 .= ((((xo | OK) . [y,z]) * ((xo | OK) . [y,z])) + (((yo | OK) (#) (yo | OK)) . [y,z])) - (r ^2) by VALUED_1:5 .= ((((z `1) - (o `1)) ^2) + (((z `2) - (o `2)) ^2)) - (r ^2) by A158, A152, A153, A156, A157, VALUED_1:5 ; hence 0 >= b by A144, A145, A159; ::_thesis: verum end; now__::_thesis:_for_b_being_real_number_st_b_in_rng_(((dx_|_OK)_(#)_(dx_|_OK))_+_((dy_|_OK)_(#)_(dy_|_OK)))_holds_ 0_<_b let b be real number ; ::_thesis: ( b in rng (((dx | OK) (#) (dx | OK)) + ((dy | OK) (#) (dy | OK))) implies 0 < b ) assume b in rng (((dx | OK) (#) (dx | OK)) + ((dy | OK) (#) (dy | OK))) ; ::_thesis: 0 < b then consider a being set such that A161: a in dom (((dx | OK) (#) (dx | OK)) + ((dy | OK) (#) (dy | OK))) and A162: (((dx | OK) (#) (dx | OK)) + ((dy | OK) (#) (dy | OK))) . a = b by FUNCT_1:def_3; a in DiffElems ((TOP-REAL 2),(TOP-REAL 2)) by A161, XBOOLE_0:def_4; then consider y, z being Point of (TOP-REAL 2) such that A163: a = [y,z] and A164: y <> z ; a in the carrier of [:(Tdisk (o,r)),(Tdisk (o,r)):] by A161, XBOOLE_0:def_4; then consider a1, a2 being Point of (Tdisk (o,r)) such that A165: a = [a1,a2] by BORSUK_1:10; set r1 = (y `1) - (z `1); set r2 = (y `2) - (z `2); A166: now__::_thesis:_not_(((y_`1)_-_(z_`1))_^2)_+_(((y_`2)_-_(z_`2))_^2)_=_0 assume (((y `1) - (z `1)) ^2) + (((y `2) - (z `2)) ^2) = 0 ; ::_thesis: contradiction then ( (y `1) - (z `1) = 0 & (y `2) - (z `2) = 0 ) by COMPLEX1:1; hence contradiction by A164, TOPREAL3:6; ::_thesis: verum end; consider x3, x4 being Point of (TOP-REAL 2) 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: ( (dx | OK) . [y,z] = dx . [y,z] & (dy | OK) . [y,z] = dy . [y,z] ) by A140, A164, FUNCT_1:49; consider x5, x6 being Point of (TOP-REAL 2) 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 [#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) by A161, A163, PRE_TOPC:def_5; (((dx | OK) (#) (dx | OK)) + ((dy | OK) (#) (dy | OK))) . [y,z] = (((dx | OK) (#) (dx | OK)) . [y,z]) + (((dy | OK) (#) (dy | OK)) . [y,z]) by A174, VALUED_1:1 .= (((dx | OK) . [y,z]) * ((dx | OK) . [y,z])) + (((dy | OK) (#) (dy | OK)) . [y,z]) by VALUED_1:5 .= (((y `1) - (z `1)) ^2) + (((y `2) - (z `2)) ^2) by A168, A169, A172, A173, A170, VALUED_1:5 ; hence 0 < b by A162, A163, A166; ::_thesis: verum end; then reconsider m = ((dx | OK) (#) (dx | OK)) + ((dy | OK) (#) (dy | OK)) as positive-yielding continuous RealMap of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) by PARTFUN3:def_1; reconsider p2 = (((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK) as nonpositive-yielding continuous RealMap of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) by A142, PARTFUN3:def_3; set pp = ((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2); set k = ((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m; set x3 = (fx2 | OK) + ((((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m) (#) (dx | OK)); set y3 = (fy2 | OK) + ((((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m) (#) (dy | OK)); reconsider X3 = (fx2 | OK) + ((((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m) (#) (dx | OK)), Y3 = (fy2 | OK) + ((((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m) (#) (dy | OK)) as Function of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),R^1 by TOPMETR:17; set F = <:X3,Y3:>; A175: for x being Point of (Tdisk (o,r)) holds (BR-map f) . x = (R2Homeomorphism * <:X3,Y3:>) . [x,(f . x)] proof A176: dom (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)) = the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) by FUNCT_2:def_1; let x be Point of (Tdisk (o,r)); ::_thesis: (BR-map f) . x = (R2Homeomorphism * <:X3,Y3:>) . [x,(f . x)] A177: ( dom X3 = the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) & dom Y3 = the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) ) 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 (TOP-REAL 2) such that A180: ( y = x & z = f . x ) and A181: HC (x,f) = HC (z,y,o,r) by A178, Def4; A182: (f1 | OK) . [y,z] = f1 . [y,z] by A140, A180, A179, FUNCT_1:49; A183: ( (xo | OK) . [y,z] = xo . [y,z] & (yo | OK) . [y,z] = yo . [y,z] ) by A140, A180, A179, FUNCT_1:49; set r1 = (y `1) - (z `1); set r2 = (y `2) - (z `2); set r3 = (z `1) - (o `1); set r4 = (z `2) - (o `2); consider x9, x10 being Point of (TOP-REAL 2) 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 (TOP-REAL 2) 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 ((TOP-REAL 2),(TOP-REAL 2)) by A180, A179; then A190: [y,z] in OK by A180, XBOOLE_0:def_4; then A191: p2 . [y,z] = ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) . [y,z]) - ((f1 | OK) . [y,z]) by A52, A139, VALUED_1:13 .= ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) . [y,z]) - (r ^2) by A182, FUNCOP_1:7 .= ((((xo | OK) (#) (xo | OK)) . [y,z]) + (((yo | OK) (#) (yo | OK)) . [y,z])) - (r ^2) by A52, A190, VALUED_1:1 .= ((((xo | OK) . [y,z]) * ((xo | OK) . [y,z])) + (((yo | OK) (#) (yo | OK)) . [y,z])) - (r ^2) by VALUED_1:5 .= ((((z `1) - (o `1)) ^2) + (((z `2) - (o `2)) ^2)) - (r ^2) by A185, A186, A188, A189, A183, VALUED_1:5 ; A192: (dx | OK) . [y,z] = dx . [y,z] by A140, A180, A179, FUNCT_1:49; consider x7, x8 being Point of (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 = ((- ((((z `1) - (o `1)) * ((y `1) - (z `1))) + (((z `2) - (o `2)) * ((y `2) - (z `2))))) + (sqrt ((((((z `1) - (o `1)) * ((y `1) - (z `1))) + (((z `2) - (o `2)) * ((y `2) - (z `2)))) ^2) - (((((y `1) - (z `1)) ^2) + (((y `2) - (z `2)) ^2)) * (((((z `1) - (o `1)) ^2) + (((z `2) - (o `2)) ^2)) - (r ^2)))))) / ((((y `1) - (z `1)) ^2) + (((y `2) - (z `2)) ^2)); A202: ( ((xo | OK) (#) (dx | OK)) . [y,z] = ((xo | OK) . [y,z]) * ((dx | OK) . [y,z]) & ((yo | OK) (#) (dy | OK)) . [y,z] = ((yo | OK) . [y,z]) * ((dy | OK) . [y,z]) ) by VALUED_1:5; A203: (dy | OK) . [y,z] = dy . [y,z] by A140, A180, A179, FUNCT_1:49; consider x5, x6 being Point of (TOP-REAL 2) 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] = (((dx | OK) (#) (dx | OK)) . [y,z]) + (((dy | OK) (#) (dy | OK)) . [y,z]) by A52, A190, VALUED_1:1 .= (((dx | OK) . [y,z]) * ((dx | OK) . [y,z])) + (((dy | OK) (#) (dy | OK)) . [y,z]) by VALUED_1:5 .= (((y `1) - (z `1)) ^2) + (((y `2) - (z `2)) ^2) by A200, A201, A205, A206, A192, A203, VALUED_1:5 ; A208: (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) . [y,z] = (((xo | OK) (#) (dx | OK)) . [y,z]) + (((yo | OK) (#) (dy | OK)) . [y,z]) by A52, A190, VALUED_1:1; then A209: ((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) . [y,z] = ((((z `1) - (o `1)) * ((y `1) - (z `1))) + (((z `2) - (o `2)) * ((y `2) - (z `2)))) ^2 by A200, A201, A205, A206, A185, A186, A188, A189, A192, A203, A183, A202, VALUED_1:5; dom (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2))) = the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) by FUNCT_2:def_1; then A210: (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2))) . [y,z] = sqrt ((((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)) . [y,z]) by A52, A190, PARTFUN3:def_5 .= sqrt ((((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) . [y,z]) - ((m (#) p2) . [y,z])) by A52, A190, A176, VALUED_1:13 .= sqrt ((((((z `1) - (o `1)) * ((y `1) - (z `1))) + (((z `2) - (o `2)) * ((y `2) - (z `2)))) ^2) - (((((y `1) - (z `1)) ^2) + (((y `2) - (z `2)) ^2)) * (((((z `1) - (o `1)) ^2) + (((z `2) - (o `2)) ^2)) - (r ^2)))) by A207, A209, A191, VALUED_1:5 ; dom (((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m) = the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) by FUNCT_2:def_1; then A211: (((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m) . [y,z] = (((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) . [y,z]) * ((m . [y,z]) ") by A52, A190, RFUNCT_1:def_1 .= (((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) . [y,z]) / (m . [y,z]) by XCMPLX_0:def_9 .= (((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) . [y,z]) + ((sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2))) . [y,z])) / ((((y `1) - (z `1)) ^2) + (((y `2) - (z `2)) ^2)) by A52, A190, A207, VALUED_1:1 .= ((- ((((z `1) - (o `1)) * ((y `1) - (z `1))) + (((z `2) - (o `2)) * ((y `2) - (z `2))))) + (sqrt ((((((z `1) - (o `1)) * ((y `1) - (z `1))) + (((z `2) - (o `2)) * ((y `2) - (z `2)))) ^2) - (((((y `1) - (z `1)) ^2) + (((y `2) - (z `2)) ^2)) * (((((z `1) - (o `1)) ^2) + (((z `2) - (o `2)) ^2)) - (r ^2)))))) / ((((y `1) - (z `1)) ^2) + (((y `2) - (z `2)) ^2)) by A200, A201, A205, A206, A185, A186, A188, A189, A192, A203, A183, A202, A208, A210, VALUED_1:8 ; A212: Y3 . [y,z] = ((fy2 | OK) . [y,z]) + (((((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m) (#) (dy | OK)) . [y,z]) by A52, A190, VALUED_1:1 .= (z `2) + (((((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m) (#) (dy | OK)) . [y,z]) by A140, A180, A179, A194, A195, FUNCT_1:49 .= (z `2) + ((((- ((((z `1) - (o `1)) * ((y `1) - (z `1))) + (((z `2) - (o `2)) * ((y `2) - (z `2))))) + (sqrt ((((((z `1) - (o `1)) * ((y `1) - (z `1))) + (((z `2) - (o `2)) * ((y `2) - (z `2)))) ^2) - (((((y `1) - (z `1)) ^2) + (((y `2) - (z `2)) ^2)) * (((((z `1) - (o `1)) ^2) + (((z `2) - (o `2)) ^2)) - (r ^2)))))) / ((((y `1) - (z `1)) ^2) + (((y `2) - (z `2)) ^2))) * ((y `2) - (z `2))) by A205, A206, A203, A211, VALUED_1:5 ; A213: X3 . [y,z] = ((fx2 | OK) . [y,z]) + (((((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m) (#) (dx | OK)) . [y,z]) by A52, A190, VALUED_1:1 .= (z `1) + (((((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m) (#) (dx | OK)) . [y,z]) by A140, A180, A179, A197, A198, FUNCT_1:49 .= (z `1) + ((((- ((((z `1) - (o `1)) * ((y `1) - (z `1))) + (((z `2) - (o `2)) * ((y `2) - (z `2))))) + (sqrt ((((((z `1) - (o `1)) * ((y `1) - (z `1))) + (((z `2) - (o `2)) * ((y `2) - (z `2)))) ^2) - (((((y `1) - (z `1)) ^2) + (((y `2) - (z `2)) ^2)) * (((((z `1) - (o `1)) ^2) + (((z `2) - (o `2)) ^2)) - (r ^2)))))) / ((((y `1) - (z `1)) ^2) + (((y `2) - (z `2)) ^2))) * ((y `1) - (z `1))) by A200, A201, A192, A211, VALUED_1:5 ; thus (BR-map f) . x = HC (x,f) by Def5 .= |[((z `1) + ((((- ((((z `1) - (o `1)) * ((y `1) - (z `1))) + (((z `2) - (o `2)) * ((y `2) - (z `2))))) + (sqrt ((((((z `1) - (o `1)) * ((y `1) - (z `1))) + (((z `2) - (o `2)) * ((y `2) - (z `2)))) ^2) - (((((y `1) - (z `1)) ^2) + (((y `2) - (z `2)) ^2)) * (((((z `1) - (o `1)) ^2) + (((z `2) - (o `2)) ^2)) - (r ^2)))))) / ((((y `1) - (z `1)) ^2) + (((y `2) - (z `2)) ^2))) * ((y `1) - (z `1)))),((z `2) + ((((- ((((z `1) - (o `1)) * ((y `1) - (z `1))) + (((z `2) - (o `2)) * ((y `2) - (z `2))))) + (sqrt ((((((z `1) - (o `1)) * ((y `1) - (z `1))) + (((z `2) - (o `2)) * ((y `2) - (z `2)))) ^2) - (((((y `1) - (z `1)) ^2) + (((y `2) - (z `2)) ^2)) * (((((z `1) - (o `1)) ^2) + (((z `2) - (o `2)) ^2)) - (r ^2)))))) / ((((y `1) - (z `1)) ^2) + (((y `2) - (z `2)) ^2))) * ((y `2) - (z `2))))]| by A180, A181, A179, Th8 .= R2Homeomorphism . [(X3 . [y,z]),(Y3 . [y,z])] by A213, A212, TOPREALA:def_2 .= R2Homeomorphism . (<:X3,Y3:> . [y,z]) by A52, A190, A177, FUNCT_3:49 .= (R2Homeomorphism * <:X3,Y3:>) . [x,(f . x)] by A52, A180, A190, FUNCT_2:15 ; ::_thesis: verum end; ( X3 is continuous & Y3 is continuous ) by JORDAN5A:27; then reconsider F = <:X3,Y3:> as continuous Function of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),[:R^1,R^1:] by YELLOW12:41; for p being Point of (Tdisk (o,r)) for V being Subset of (Tcircle (o,r)) st (BR-map f) . p in V & V is open holds ex W being Subset of (Tdisk (o,r)) st ( p in W & W is open & (BR-map f) .: W c= V ) proof let p be Point of (Tdisk (o,r)); ::_thesis: for V being Subset of (Tcircle (o,r)) st (BR-map f) . p in V & V is open holds ex W being Subset of (Tdisk (o,r)) st ( p in W & W is open & (BR-map f) .: W c= V ) let V be Subset of (Tcircle (o,r)); ::_thesis: ( (BR-map f) . p in V & V is open implies ex W being Subset of (Tdisk (o,r)) st ( p in W & W is open & (BR-map f) .: W c= V ) ) assume that A214: (BR-map f) . p in V and A215: V is open ; ::_thesis: ex W being Subset of (Tdisk (o,r)) st ( p in W & W is open & (BR-map f) .: W c= V ) consider V1 being Subset of (TOP-REAL 2) such that A216: V1 is open and A217: V1 /\ ([#] (Tcircle (o,r))) = V by A215, TOPS_2:24; reconsider p1 = p, fp = f . p as Point of (TOP-REAL 2) by PRE_TOPC:25; A218: rng R2Homeomorphism = [#] (TOP-REAL 2) by TOPREALA:34, TOPS_2:def_5; R2Homeomorphism " is being_homeomorphism by TOPREALA:34, TOPS_2:56; then A219: (R2Homeomorphism ") .: 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 ((TOP-REAL 2),(TOP-REAL 2)) ; then A220: [p,(f . p)] in OK by XBOOLE_0:def_4; (BR-map f) . p = (R2Homeomorphism * F) . [p,(f . p)] by A175; then (R2Homeomorphism * F) . [p1,fp] in V1 by A214, A217, XBOOLE_0:def_4; then A221: (R2Homeomorphism ") . ((R2Homeomorphism * F) . [p1,fp]) in (R2Homeomorphism ") .: V1 by FUNCT_2:35; A222: R2Homeomorphism is one-to-one by TOPREALA:34, TOPS_2:def_5; A223: dom R2Homeomorphism = the carrier of [:R^1,R^1:] by FUNCT_2:def_1; then A224: rng F c= dom R2Homeomorphism ; then ( dom F = the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) & dom (R2Homeomorphism * F) = dom F ) by FUNCT_2:def_1, RELAT_1:27; then A225: ((R2Homeomorphism ") * (R2Homeomorphism * F)) . [p1,fp] in (R2Homeomorphism ") .: V1 by A52, A220, A221, FUNCT_1:13; A226: for x being set st x in dom F holds ((id (dom R2Homeomorphism)) * F) . x = F . x proof let x be set ; ::_thesis: ( x in dom F implies ((id (dom R2Homeomorphism)) * F) . x = F . x ) assume A227: x in dom F ; ::_thesis: ((id (dom R2Homeomorphism)) * F) . x = F . x A228: F . x in rng F by A227, FUNCT_1:def_3; thus ((id (dom R2Homeomorphism)) * F) . x = (id (dom R2Homeomorphism)) . (F . x) by A227, FUNCT_1:13 .= F . x by A223, A228, FUNCT_1:18 ; ::_thesis: verum end; dom (id (dom R2Homeomorphism)) = dom R2Homeomorphism ; then dom ((id (dom R2Homeomorphism)) * F) = dom F by A224, RELAT_1:27; then A229: (id (dom R2Homeomorphism)) * F = F by A226, FUNCT_1:2; (R2Homeomorphism ") * (R2Homeomorphism * F) = ((R2Homeomorphism ") * R2Homeomorphism) * F by RELAT_1:36 .= (id (dom R2Homeomorphism)) * F by A218, A222, TOPS_2:52 ; then consider W being Subset of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) such that A230: [p1,fp] in W and A231: W is open and A232: F .: W c= (R2Homeomorphism ") .: V1 by A52, A220, A219, A229, A225, JGRAPH_2:10; consider WW being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] such that A233: WW is open and A234: WW /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) = W by A231, TOPS_2:24; consider SF being Subset-Family of [:(TOP-REAL 2),(TOP-REAL 2):] such that A235: WW = union SF and A236: for e being set st e in SF holds ex X1, Y1 being Subset of (TOP-REAL 2) 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 /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)); Z c= WW by A235, A238, ZFMISC_1:74; then Z /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) c= WW /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) by XBOOLE_1:27; then A239: F .: (Z /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK))) c= F .: W by A234, RELAT_1:123; consider X1, Y1 being Subset of (TOP-REAL 2) such that A240: Z = [:X1,Y1:] and A241: ( X1 is open & Y1 is open ) by A236, A238; reconsider XX = X1 /\ ([#] (Tdisk (o,r))), YY = Y1 /\ ([#] (Tdisk (o,r))) as open Subset of (Tdisk (o,r)) 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 (Tdisk (o,r)) 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; ::_thesis: ( p in W1 & W1 is open & (BR-map f) .: W1 c= V ) 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; ::_thesis: ( W1 is open & (BR-map f) .: W1 c= V ) thus W1 is open by A243; ::_thesis: (BR-map f) .: W1 c= V let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in (BR-map f) .: W1 or b in V ) assume b in (BR-map f) .: W1 ; ::_thesis: b in V then consider a being Point of (Tdisk (o,r)) such that A245: a in W1 and A246: b = (BR-map f) . a by FUNCT_2:65; reconsider a1 = a, fa = f . a as Point of (TOP-REAL 2) 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 ((TOP-REAL 2),(TOP-REAL 2)) ; 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 Z /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) by A52, A248, XBOOLE_0:def_4; then F . [a1,fa] in F .: (Z /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK))) by FUNCT_2:35; then F . [a1,fa] in F .: W by A239; then R2Homeomorphism . (F . [a1,fa]) in R2Homeomorphism .: ((R2Homeomorphism ") .: V1) by A232, FUNCT_2:35; then A249: (R2Homeomorphism * F) . [a1,fa] in R2Homeomorphism .: ((R2Homeomorphism ") .: V1) by A52, A248, FUNCT_2:15; R2Homeomorphism is onto by A218, FUNCT_2:def_3; then ( R2Homeomorphism " = R2Homeomorphism " & dom (R2Homeomorphism ") = [#] (TOP-REAL 2) ) by A218, A222, TOPS_2:49, TOPS_2:def_4; then (R2Homeomorphism * F) . [a1,fa] in V1 by A222, A249, PARTFUN3:1; then (BR-map f) . a in V1 by A175; hence b in V by A217, A246, XBOOLE_0:def_4; ::_thesis: verum end; hence BR-map f is continuous by JGRAPH_2:10; ::_thesis: verum end; theorem Th14: :: BROUWER:14 for r being non negative real number for o being Point of (TOP-REAL 2) for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) holds f is with_fixpoint proof let r be non negative real number ; ::_thesis: for o being Point of (TOP-REAL 2) for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) holds f is with_fixpoint let o be Point of (TOP-REAL 2); ::_thesis: for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) holds f is with_fixpoint let f be continuous Function of (Tdisk (o,r)),(Tdisk (o,r)); ::_thesis: f is with_fixpoint 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; percases ( r is positive or not r is positive ) ; suppose r is positive ; ::_thesis: f is with_fixpoint then reconsider r = 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 ; ::_thesis: contradiction A5: g is being_a_retraction proof let W be Point of (Tdisk (o,r)); :: according to BORSUK_1:def_16 ::_thesis: ( not W in the carrier of Y or g . W = W ) assume A6: W in the carrier of Y ; ::_thesis: g . W = W not W is_a_fixpoint_of f by A4, ABIAN:def_5; hence g . W = W by A6, Th11; ::_thesis: verum end; g is continuous by A4, Th13; hence contradiction by A3, A5, BORSUK_1:def_17; ::_thesis: verum end; suppose not r is positive ; ::_thesis: f is with_fixpoint then reconsider r = r as non positive non negative real number ; take o ; :: according to ABIAN:def_5 ::_thesis: o is_a_fixpoint_of f 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; :: according to ABIAN:def_3 ::_thesis: o = f . o then f . o in rng f by FUNCT_1:def_3; hence o = f . o by A2, A7, TARSKI:def_1; ::_thesis: verum end; end; end; theorem :: BROUWER:15 for r being non negative real number for o being Point of (TOP-REAL 2) for 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 ; ::_thesis: for o being Point of (TOP-REAL 2) for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) ex x being Point of (Tdisk (o,r)) st f . x = x let o be Point of (TOP-REAL 2); ::_thesis: for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) ex x being Point of (Tdisk (o,r)) st f . x = x let f be continuous Function of (Tdisk (o,r)),(Tdisk (o,r)); ::_thesis: ex x being Point of (Tdisk (o,r)) st f . x = x 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 ; ::_thesis: ( x is Point of (Tdisk (o,r)) & f . x = x ) x in dom f by A1, ABIAN:def_3; hence x is Point of (Tdisk (o,r)) ; ::_thesis: f . x = x thus f . x = x by A1, ABIAN:def_3; ::_thesis: verum end;