:: The Brouwer Fixed Point Theorem for Intervals :: by Toshihiko Watanabe :: :: Received August 17, 1992 :: Copyright (c) 1992-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, XXREAL_1, REAL_1, PRE_TOPC, TOPMETR, XXREAL_0, STRUCT_0, SUBSET_1, RCOMP_1, PCOMPS_1, METRIC_1, CARD_1, TARSKI, ARYTM_1, ARYTM_3, FUNCT_1, COMPLEX1, SETFAM_1, XBOOLE_0, VALUED_1, BORSUK_1, RELAT_1, ORDINAL2, TMAP_1, TOPS_2, RELAT_2, XXREAL_2, SEQ_4, FUNCT_3, TREAL_1, FUNCT_2, FUNCT_7; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XXREAL_2, XREAL_0, COMPLEX1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, REAL_1, SEQ_4, RCOMP_1, PRE_TOPC, TOPS_2, CONNSP_1, METRIC_1, DOMAIN_1, STRUCT_0, PCOMPS_1, TOPMETR, TSEP_1, TMAP_1, BORSUK_1; constructors REAL_1, SQUARE_1, COMPLEX1, SEQ_4, RCOMP_1, CONNSP_1, TOPS_2, TMAP_1, TOPMETR, XXREAL_2, BINOP_2, RVSUM_1, PCOMPS_1, BINOP_1; registrations XBOOLE_0, RELSET_1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, STRUCT_0, PRE_TOPC, METRIC_1, BORSUK_1, TOPMETR, CONNSP_1, ORDINAL1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; definitions TARSKI, FUNCT_2, XXREAL_2; equalities SUBSET_1, STRUCT_0; expansions TARSKI, FUNCT_2, XXREAL_2; theorems TARSKI, SUBSET_1, FUNCT_1, FUNCT_2, ABSVALUE, RCOMP_1, SEQ_2, SEQ_4, METRIC_1, PRE_TOPC, TOPS_1, TOPS_2, CONNSP_1, PCOMPS_1, BORSUK_1, TOPMETR, HEINE, TSEP_1, TMAP_1, RELAT_1, TBSP_1, RELSET_1, XREAL_0, XBOOLE_0, XBOOLE_1, XCMPLX_1, XREAL_1, XXREAL_0, XXREAL_1; schemes FUNCT_2; begin :: 1. Properties of Topological Intervals. reserve a,b,c,d for Real; Lm1: for x being set st x in [.a,b.] holds x is Element of REAL; Lm2: for x being Point of Closed-Interval-TSpace(a,b) st a <= b holds x is Element of REAL proof let x be Point of Closed-Interval-TSpace(a,b); assume a <= b; then the carrier of Closed-Interval-TSpace(a,b) = [.a,b.] by TOPMETR:18; hence thesis by Lm1; end; theorem Th1: for A being Subset of R^1 st A = [.a,b.] holds A is closed proof let A be Subset of R^1; assume A1: A = [.a,b.]; reconsider B = A` as Subset of TopSpaceMetr(RealSpace) by TOPMETR:def 6; reconsider a, b as Real; reconsider D = B as Subset of RealSpace by TOPMETR:12; set C = D`; A2: the carrier of RealSpace = the carrier of TopSpaceMetr(RealSpace) by TOPMETR:12; for c being Point of RealSpace st c in B ex r being Real st r > 0 & Ball(c,r) c= B proof let c be Point of RealSpace; reconsider n = c as Element of REAL by METRIC_1:def 13; assume c in B; then not n in [.a,b.] by A1,XBOOLE_0:def 5; then A3: not n in {p where p is Real : a <= p & p <= b} by RCOMP_1:def 1; now per cases by A3; suppose A4: not a <= n; take r = a - n; now let x be object; assume A5: x in Ball(c,r); then reconsider t = x as Element of REAL by METRIC_1:def 13; reconsider u = x as Point of RealSpace by A5; Ball(c,r) = {q where q is Element of RealSpace :dist(c,q) 0 & Ball(c,r) c= B by A4,XREAL_1:50; end; suppose A7: not n <= b; take r = n - b; now let x be object; assume A8: x in Ball(c,r); then reconsider t = x as Element of REAL by METRIC_1:def 13; reconsider u = x as Point of RealSpace by A8; Ball(c,r) = {q where q is Element of RealSpace :dist(c,q) 0 & Ball(c,r) c= B by A7,XREAL_1:50; end; end; hence ex r being Real st r > 0 & Ball(c,r) c= B; end; then A` is open by TOPMETR:15,def 6; hence thesis by TOPS_1:3; end; theorem Th2: a <= b implies Closed-Interval-TSpace(a,b) is closed proof assume a <= b; then the carrier of Closed-Interval-TSpace(a,b) = [.a,b.] by TOPMETR:18; then for A be Subset of R^1 holds A = the carrier of Closed-Interval-TSpace(a ,b) implies A is closed by Th1; hence thesis by BORSUK_1:def 11; end; theorem a <= c & d <= b & c <= d implies Closed-Interval-TSpace(c,d) is closed SubSpace of Closed-Interval-TSpace(a,b) proof assume that A1: a <= c and A2: d <= b and A3: c <= d; [.c,d.] c= [.a,b.] by A1,A2,XXREAL_1:34; then A4: the carrier of Closed-Interval-TSpace(c,d) c= [.a,b.] by A3,TOPMETR:18; A5: Closed-Interval-TSpace(c,d) is closed SubSpace of R^1 by A3,Th2; a <= d by A1,A3,XXREAL_0:2; then the carrier of Closed-Interval-TSpace(c,d) c= the carrier of Closed-Interval-TSpace(a,b) by A2,A4,TOPMETR:18,XXREAL_0:2; hence thesis by A5,TSEP_1:14; end; theorem a <= c & b <= d & c <= b implies Closed-Interval-TSpace(a,d) = Closed-Interval-TSpace(a,b) union Closed-Interval-TSpace(c,d) & Closed-Interval-TSpace(c,b) = Closed-Interval-TSpace(a,b) meet Closed-Interval-TSpace(c,d) proof assume that A1: a <= c and A2: b <= d and A3: c <= b; A4: the carrier of Closed-Interval-TSpace(a,b) = [.a,b.] & the carrier of Closed-Interval-TSpace(c,d) = [.c,d.] by A1,A2,A3,TOPMETR:18,XXREAL_0:2; a <= b by A1,A3,XXREAL_0:2; then A5: the carrier of Closed-Interval-TSpace(a,d) = [.a,d.] by A2,TOPMETR:18 ,XXREAL_0:2; A6: the carrier of Closed-Interval-TSpace(c,b) = [.c,b.] by A3,TOPMETR:18; [.a,b.] \/ [.c,d.] = [.a,d.] by A1,A2,A3,XXREAL_1:174; hence Closed-Interval-TSpace(a,d) = Closed-Interval-TSpace(a,b) union Closed-Interval-TSpace(c,d) by A4,A5,TSEP_1:def 2; A7: [.a,b.] /\ [.c,d.] = [.c,b.] by A1,A2,XXREAL_1:143; then (the carrier of Closed-Interval-TSpace(a,b)) /\ (the carrier of Closed-Interval-TSpace(c,d)) <> {} by A3,A4,XXREAL_1:1; then (the carrier of Closed-Interval-TSpace(a,b)) meets (the carrier of Closed-Interval-TSpace(c,d)) by XBOOLE_0:def 7; then Closed-Interval-TSpace(a,b) meets Closed-Interval-TSpace(c,d) by TSEP_1:def 3; hence thesis by A4,A6,A7,TSEP_1:def 4; end; definition let a,b be Real; assume A1: a <= b; func (#)(a,b) -> Point of Closed-Interval-TSpace(a,b) equals :Def1: a; coherence proof a in [.a,b.] by A1,XXREAL_1:1; hence thesis by A1,TOPMETR:18; end; correctness; func (a,b)(#) -> Point of Closed-Interval-TSpace(a,b) equals :Def2: b; coherence proof b in [.a,b.] by A1,XXREAL_1:1; hence thesis by A1,TOPMETR:18; end; correctness; end; theorem 0[01] = (#)(0,1) & 1[01] = (0,1)(#) by Def1,Def2,BORSUK_1:def 14,def 15; theorem a <= b & b <= c implies (#)(a,b) = (#)(a,c) & (b,c)(#) = (a,c)(#) proof assume that A1: a <= b and A2: b <= c; thus (#)(a,b) = a by A1,Def1 .= (#)(a,c) by A1,A2,Def1,XXREAL_0:2; thus (b,c)(#) = c by A2,Def2 .= (a,c)(#) by A1,A2,Def2,XXREAL_0:2; end; begin :: 2. Continuous Mappings Between Topological Intervals. definition let a,b be Real such that A1: a <= b; let t1,t2 be Point of Closed-Interval-TSpace(a,b); func L[01](t1,t2) -> Function of Closed-Interval-TSpace(0,1), Closed-Interval-TSpace(a,b) means :Def3: for s being Point of Closed-Interval-TSpace(0,1) holds it.s = (1-s)*t1 + s*t2; existence proof reconsider r1 = t1, r2 = t2 as Element of REAL by A1,Lm2; deffunc U(Real) = In((1-\$1)*r1 + \$1*r2,REAL); consider LI being Function of REAL,REAL such that A2: for r being Element of REAL holds LI.r= U(r) from FUNCT_2:sch 4; A3: [.a,b.] = the carrier of Closed-Interval-TSpace(a,b) by A1,TOPMETR:18; now let y be object; assume A4: y in rng(LI|[.0,1.]); then reconsider d = y as Element of REAL; y in LI.:[.0,1.] by A4,RELAT_1:115; then consider x being object such that x in dom LI and A5: x in [.0,1.] and A6: y = LI.x by FUNCT_1:def 6; reconsider c = x as Element of REAL by A5; A7: d = U(c) by A2,A6; r1 in [.a,b.] by A3; then r1 in { p where p is Real: a <= p & p <= b} by RCOMP_1:def 1; then A8: ex v1 being Real st v1 = r1 & a <= v1 & v1 <= b; c in { p where p is Real: 0 <= p & p <= 1} by A5,RCOMP_1:def 1; then A9: ex u being Real st u = c & 0 <= u & u <= 1; r2 in [.a,b.] by A3; then r2 in { p where p is Real: a <= p & p <= b} by RCOMP_1:def 1; then A10: ex v2 being Real st v2 = r2 & a <= v2 & v2 <= b; then A11: c*a <= c*r2 by A9,XREAL_1:64; A12: c*r2 <= c*b by A9,A10,XREAL_1:64; A13: 0 <= 1 - c by A9,XREAL_1:48; then (1 - c)*r1 <= (1 - c)*b by A8,XREAL_1:64; then A14: d <= (1 - c)*b + c*b by A7,A12,XREAL_1:7; (1 - c)*a <= (1 - c)*r1 by A8,A13,XREAL_1:64; then (1 - c)*a + c*a <= d by A7,A11,XREAL_1:7; then y in { q where q is Real: a <= q & q <= b} by A14; hence y in [.a,b.] by RCOMP_1:def 1; end; then A15: rng(LI|[.0,1.]) c= the carrier of Closed-Interval-TSpace(a,b) by A3; A16: dom(LI|[.0,1.]) = (dom LI) /\ [.0,1.] by RELAT_1:61; [.0,1.] = REAL /\ [.0,1.] & dom LI = REAL by FUNCT_2:def 1,XBOOLE_1:28; then dom(LI|[.0,1.]) = the carrier of Closed-Interval-TSpace(0,1) by A16, TOPMETR:18; then reconsider F = LI|[.0,1.] as Function of Closed-Interval-TSpace(0,1), Closed-Interval-TSpace(a,b) by A15,FUNCT_2:def 1,RELSET_1:4; take F; let s be Point of Closed-Interval-TSpace(0,1); A17: s in REAL by XREAL_0:def 1; the carrier of Closed-Interval-TSpace(0,1) = [.0,1.] by TOPMETR:18; hence F.s = LI.s by FUNCT_1:49 .= U(s) by A2,A17 .= (1-s)*t1 + s*t2; end; uniqueness proof let F1, F2 be Function of Closed-Interval-TSpace(0,1), Closed-Interval-TSpace(a,b); assume A18: for s being Point of Closed-Interval-TSpace(0,1) holds F1.s = (1-s)*t1 + s*t2; assume A19: for s being Point of Closed-Interval-TSpace(0,1) holds F2.s = (1-s)*t1 + s*t2; for s being Point of Closed-Interval-TSpace(0,1) holds F1.s = F2.s proof reconsider r1 = t1, r2 = t2 as Real; let s be Point of Closed-Interval-TSpace(0,1); reconsider r = s as Real; thus F1.s = (1-r)*r1 + r*r2 by A18 .= F2.s by A19; end; hence F1 = F2; end; end; theorem Th7: a <= b implies for t1,t2 being Point of Closed-Interval-TSpace(a,b) for s being Point of Closed-Interval-TSpace(0,1) holds L[01](t1,t2).s = (t2 - t1)*s + t1 proof assume A1: a <= b; let t1,t2 be Point of Closed-Interval-TSpace(a,b); let s be Point of Closed-Interval-TSpace(0,1); thus L[01](t1,t2).s = (1-s)*t1 + s*t2 by A1,Def3 .= (t2 - t1)*s + t1; end; theorem Th8: a <= b implies for t1,t2 being Point of Closed-Interval-TSpace(a,b) holds L[01](t1,t2) is continuous proof assume A1: a <= b; let t1,t2 be Point of Closed-Interval-TSpace(a,b); reconsider r1 = t1, r2 = t2 as Real; deffunc U(Real) = In((r2 - r1)*\$1 + r1,REAL); consider L being Function of REAL,REAL such that A2: for r being Element of REAL holds L.r= U(r) from FUNCT_2:sch 4; A3: for r being Real holds L.r= (r2 - r1)*r + r1 proof let r be Real; reconsider r as Element of REAL by XREAL_0:def 1; L.r= U(r) by A2; hence thesis; end; reconsider f = L as Function of R^1, R^1 by TOPMETR:17; A4: for s being Point of Closed-Interval-TSpace(0,1), w being Point of R^1 st s = w holds L[01](t1,t2).s = f.w proof let s be Point of Closed-Interval-TSpace(0,1), w be Point of R^1; reconsider r = s as Real; assume A5: s = w; thus L[01](t1,t2).s = U(r) by A1,Th7 .= f.w by A3,A5; end; A6: [.0,1.] = the carrier of Closed-Interval-TSpace(0,1) by TOPMETR:18; A7: f is continuous by A3,TOPMETR:21; for s being Point of Closed-Interval-TSpace(0,1) holds L[01](t1,t2) is_continuous_at s proof let s be Point of Closed-Interval-TSpace(0,1); reconsider w = s as Point of R^1 by A6,TARSKI:def 3,TOPMETR:17; for G being Subset of Closed-Interval-TSpace(a,b) st G is open & L[01] (t1,t2).s in G ex H being Subset of Closed-Interval-TSpace(0,1) st H is open & s in H & L[01](t1,t2).:H c= G proof let G be Subset of Closed-Interval-TSpace(a,b); assume G is open; then consider G0 being Subset of R^1 such that A8: G0 is open and A9: G0 /\ [#] Closed-Interval-TSpace(a,b) = G by TOPS_2:24; A10: f is_continuous_at w by A7,TMAP_1:44; assume L[01](t1,t2).s in G; then f.w in G by A4; then f.w in G0 by A9,XBOOLE_0:def 4; then consider H0 being Subset of R^1 such that A11: H0 is open and A12: w in H0 and A13: f.:H0 c= G0 by A8,A10,TMAP_1:43; now reconsider H = H0 /\ [#] Closed-Interval-TSpace(0,1) as Subset of Closed-Interval-TSpace(0,1); take H; thus H is open by A11,TOPS_2:24; thus s in H by A12,XBOOLE_0:def 4; thus L[01](t1,t2).:H c= G proof let t be object; assume t in L[01](t1,t2).:H; then consider r be object such that r in dom L[01](t1,t2) and A14: r in H and A15: t = L[01](t1,t2).r by FUNCT_1:def 6; A16: r in the carrier of Closed-Interval-TSpace(0,1) by A14; reconsider r as Point of Closed-Interval-TSpace(0,1) by A14; r in dom L[01](t1,t2) by A16,FUNCT_2:def 1; then A17: t in L[01](t1,t2).:(the carrier of Closed-Interval-TSpace(0,1)) by A15,FUNCT_1:def 6; reconsider p = r as Point of R^1 by A6,TARSKI:def 3,TOPMETR:17; p in [#] R^1; then A18: p in dom f by FUNCT_2:def 1; t=f.p & p in H0 by A4,A14,A15,XBOOLE_0:def 4; then t in f.:H0 by A18,FUNCT_1:def 6; hence thesis by A9,A13,A17,XBOOLE_0:def 4; end; end; hence thesis; end; hence thesis by TMAP_1:43; end; hence thesis by TMAP_1:44; end; theorem a <= b implies for t1,t2 being Point of Closed-Interval-TSpace(a,b) holds L[01](t1,t2).(#)(0,1) = t1 & L[01](t1,t2).(0,1)(#) = t2 proof assume A1: a <= b; let t1,t2 be Point of Closed-Interval-TSpace(a,b); reconsider r1 = t1, r2 = t2 as Real; 0 = (#)(0,1) by Def1; hence L[01](t1,t2).(#)(0,1) = (1-0)*r1 + 0*r2 by A1,Def3 .= t1; 1 = (0,1)(#) by Def2; hence L[01](t1,t2).(0,1)(#) = (1-1)*r1 + 1*r2 by A1,Def3 .= t2; end; theorem L[01]((#)(0,1),(0,1)(#)) = id Closed-Interval-TSpace(0,1) proof for x being Point of Closed-Interval-TSpace(0,1) holds L[01]((#)(0,1),(0 ,1)(#)).x = x proof let x be Point of Closed-Interval-TSpace(0,1); reconsider y = x as Real; (#)(0,1) = 0 & (0,1)(#) = 1 by Def1,Def2; hence L[01]((#)(0,1),(0,1)(#)).x = (1-y)*0 + y*1 by Def3 .= x; end; hence thesis by FUNCT_2:124; end; definition let a,b be Real such that A1: a < b; let t1,t2 be Point of Closed-Interval-TSpace(0,1); func P[01](a,b,t1,t2) -> Function of Closed-Interval-TSpace(a,b), Closed-Interval-TSpace(0,1) means :Def4: for s being Point of Closed-Interval-TSpace(a,b) holds it.s = ((b-s)*t1 + (s-a)*t2)/(b-a); existence proof reconsider a1 = a, b1 = b as Real; reconsider r1 = t1, r2 = t2 as Real; deffunc U(Real) = In(((b1-\$1)*r1 + (\$1-a1)*r2)/(b1-a1),REAL); consider PI being Function of REAL,REAL such that A2: for r being Element of REAL holds PI.r= U(r) from FUNCT_2:sch 4; A3: [.0,1.] = the carrier of Closed-Interval-TSpace(0,1) by TOPMETR:18; now let y be object; assume A4: y in rng(PI|[.a,b.]); then reconsider d = y as Real; y in PI.:[.a,b.] by A4,RELAT_1:115; then consider x being object such that x in dom PI and A5: x in [.a,b.] and A6: y = PI.x by FUNCT_1:def 6; reconsider c = x as Element of REAL by A5; A7: d = U(c) by A2,A6; r1 in [.0,1.] by A3; then r1 in { p where p is Real: 0 <= p & p <= 1} by RCOMP_1:def 1; then A8: ex v1 being Real st v1 = r1 & 0 <= v1 & v1 <= 1; c in { p where p is Real: a <= p & p <= b} by A5,RCOMP_1:def 1; then A9: ex u being Real st u = c & a <= u & u <= b; then A10: 0 <= c - a by XREAL_1:48; r2 in [.0,1.] by A3; then r2 in { p where p is Real: 0 <= p & p <= 1} by RCOMP_1:def 1; then A11: ex v2 being Real st v2 = r2 & 0 <= v2 & v2 <= 1; then A12: (c - a)*r2 <= c - a by A10,XREAL_1:153; A13: 0 < b - a by A1,XREAL_1:50; A14: 0 <= b - c by A9,XREAL_1:48; then (b - c)*r1 <= b - c by A8,XREAL_1:153; then (b - c)*r1 + (c - a)*r2 <= (b + - c) + (c - a) by A12,XREAL_1:7; then d <= (b - a)/(b - a) by A13,A7,XREAL_1:72; then d <= 1 by A13,XCMPLX_1:60; then y in { q where q is Real: 0 <= q & q <= 1} by A8,A11,A13,A7,A14,A10; hence y in [.0,1.] by RCOMP_1:def 1; end; then A15: rng(PI|[.a,b.]) c= the carrier of Closed-Interval-TSpace(0,1) by A3; A16: dom(PI|[.a,b.]) = (dom PI) /\ [.a,b.] by RELAT_1:61; [.a,b.] = REAL /\ [.a,b.] & dom PI = REAL by FUNCT_2:def 1,XBOOLE_1:28; then dom(PI|[.a,b.]) = the carrier of Closed-Interval-TSpace(a,b) by A1,A16 ,TOPMETR:18; then reconsider F = PI|[.a,b.] as Function of Closed-Interval-TSpace(a,b), Closed-Interval-TSpace(0,1) by A15,FUNCT_2:def 1,RELSET_1:4; take F; let s be Point of Closed-Interval-TSpace(a,b); A17: s in REAL by XREAL_0:def 1; the carrier of Closed-Interval-TSpace(a,b) = [.a,b.] by A1,TOPMETR:18; hence F.s = PI.s by FUNCT_1:49 .= U(s) by A2,A17 .= ((b-s)*t1 + (s-a)*t2)/(b-a); end; uniqueness proof let F1, F2 be Function of Closed-Interval-TSpace(a,b), Closed-Interval-TSpace(0,1); assume A18: for s being Point of Closed-Interval-TSpace(a,b) holds F1.s = ((b-s)*t1 + (s-a)*t2)/(b-a); assume A19: for s being Point of Closed-Interval-TSpace(a,b) holds F2.s = ((b-s)*t1 + (s-a)*t2)/(b-a); let s be Point of Closed-Interval-TSpace(a,b); reconsider r = s as Real; reconsider r1 = t1, r2 = t2 as Real; thus F1.s = ((b-r)*r1 + (r-a)*r2)/(b-a) by A18 .= F2.s by A19; end; end; theorem Th11: a < b implies for t1,t2 being Point of Closed-Interval-TSpace(0,1) for s being Point of Closed-Interval-TSpace(a,b) holds P[01](a,b,t1,t2).s = ((t2 - t1)/(b-a))*s + (b*t1 -a*t2)/(b-a) proof assume A1: a < b; let t1,t2 be Point of Closed-Interval-TSpace(0,1); let s be Point of Closed-Interval-TSpace(a,b); thus P[01](a,b,t1,t2).s = ((b-s)*t1 + (s-a)*t2)/(b-a) by A1,Def4 .= (s*(t2 - t1) + (b*t1 -a*t2))/(b-a) .= (s*(t2 - t1))/(b-a) + (b*t1 -a*t2)/(b-a) by XCMPLX_1:62 .= (s*(t2 - t1))* (1/(b-a)) + (b*t1 -a*t2)/(b-a) by XCMPLX_1:99 .= ((t2 - t1)* (1/(b-a)))*s + (b*t1 -a*t2)/(b-a) .= ((t2 - t1)/(b-a))*s + (b*t1 -a*t2)/(b-a) by XCMPLX_1:99; end; theorem Th12: a < b implies for t1,t2 being Point of Closed-Interval-TSpace(0,1) holds P[01](a,b,t1,t2) is continuous proof assume A1: a < b; reconsider a, b as Real; A2: [.a,b.] = the carrier of Closed-Interval-TSpace(a,b) by A1,TOPMETR:18; let t1,t2 be Point of Closed-Interval-TSpace(0,1); reconsider r1 = t1, r2 = t2 as Real; deffunc U(Real) = In(((r2 - r1)/(b-a))*\$1 + (b*r1 -a*r2)/(b-a),REAL); consider P being Function of REAL,REAL such that A3: for r being Element of REAL holds P.r= U(r) from FUNCT_2:sch 4; A4: for r being Real holds P.r= ((r2 - r1)/(b-a))*r + (b*r1 -a*r2)/(b-a) proof let r be Real; reconsider r as Element of REAL by XREAL_0:def 1; P.r= U(r) by A3; hence thesis; end; reconsider f = P as Function of R^1, R^1 by TOPMETR:17; A5: for s being Point of Closed-Interval-TSpace(a,b), w being Point of R^1 st s = w holds P[01](a,b,t1,t2).s = f.w proof let s be Point of Closed-Interval-TSpace(a,b), w be Point of R^1; reconsider r = s as Real; assume A6: s = w; thus P[01](a,b,t1,t2).s = ((r2 - r1)/(b-a))*r + (b*r1 -a*r2)/(b-a) by A1 ,Th11 .= U(r) .= f.w by A4,A6; end; A7: f is continuous by A4,TOPMETR:21; for s being Point of Closed-Interval-TSpace(a,b) holds P[01](a,b,t1,t2) is_continuous_at s proof let s be Point of Closed-Interval-TSpace(a,b); reconsider w = s as Point of R^1 by A2,TARSKI:def 3,TOPMETR:17; for G being Subset of Closed-Interval-TSpace(0,1) st G is open & P[01] (a,b,t1,t2).s in G ex H being Subset of Closed-Interval-TSpace(a,b) st H is open & s in H & P[01](a,b,t1,t2).:H c= G proof let G be Subset of Closed-Interval-TSpace(0,1); assume G is open; then consider G0 being Subset of R^1 such that A8: G0 is open and A9: G0 /\ [#] Closed-Interval-TSpace(0,1) = G by TOPS_2:24; A10: f is_continuous_at w by A7,TMAP_1:44; assume P[01](a,b,t1,t2).s in G; then f.w in G by A5; then f.w in G0 by A9,XBOOLE_0:def 4; then consider H0 being Subset of R^1 such that A11: H0 is open and A12: w in H0 and A13: f.: H0 c= G0 by A8,A10,TMAP_1:43; now reconsider H = H0 /\ [#] Closed-Interval-TSpace(a,b) as Subset of Closed-Interval-TSpace(a,b); take H; thus H is open by A11,TOPS_2:24; thus s in H by A12,XBOOLE_0:def 4; thus P[01](a,b,t1,t2).:H c= G proof let t be object; assume t in P[01](a,b,t1,t2).:H; then consider r be object such that r in dom P[01](a,b,t1,t2) and A14: r in H and A15: t = P[01](a,b,t1,t2).r by FUNCT_1:def 6; A16: r in the carrier of Closed-Interval-TSpace(a,b) by A14; reconsider r as Point of Closed-Interval-TSpace(a,b) by A14; r in dom P[01](a,b,t1,t2) by A16,FUNCT_2:def 1; then A17: t in P[01](a,b,t1,t2).: (the carrier of Closed-Interval-TSpace( a,b)) by A15,FUNCT_1:def 6; reconsider p = r as Point of R^1 by A2,TARSKI:def 3,TOPMETR:17; p in [#] R^1; then A18: p in dom f by FUNCT_2:def 1; t=f.p & p in H0 by A5,A14,A15,XBOOLE_0:def 4; then t in f.:H0 by A18,FUNCT_1:def 6; hence thesis by A9,A13,A17,XBOOLE_0:def 4; end; end; hence thesis; end; hence thesis by TMAP_1:43; end; hence thesis by TMAP_1:44; end; theorem a < b implies for t1,t2 being Point of Closed-Interval-TSpace(0,1) holds P[01](a,b,t1,t2).(#)(a,b) = t1 & P[01](a,b,t1,t2).(a,b)(#) = t2 proof assume A1: a < b; then A2: b - a <> 0; let t1,t2 be Point of Closed-Interval-TSpace(0,1); reconsider r1 = t1, r2 = t2 as Real; a = (#)(a,b) by A1,Def1; hence P[01](a,b,t1,t2).(#)(a,b) = ((b-a)*r1 + (a-a)*r2)/(b-a) by A1,Def4 .= t1 by A2,XCMPLX_1:89; b = (a,b)(#) by A1,Def2; hence P[01](a,b,t1,t2).(a,b)(#) = ((b-b)*r1 + (b-a)*r2)/(b-a) by A1,Def4 .= t2 by A2,XCMPLX_1:89; end; theorem P[01](0,1,(#)(0,1),(0,1)(#)) = id Closed-Interval-TSpace(0,1) proof for x being Point of Closed-Interval-TSpace(0,1) holds P[01](0,1,(#)(0,1 ),(0,1)(#)).x = x proof let x be Point of Closed-Interval-TSpace(0,1); reconsider y = x as Real; (#)(0,1)=0 & (0,1)(#) = 1 by Def1,Def2; hence P[01](0,1,(#)(0,1),(0,1)(#)).x = ((1-y)*0 + (y-0)*1)/(1-0) by Def4 .= x; end; hence thesis by FUNCT_2:124; end; theorem Th15: a < b implies id Closed-Interval-TSpace(a,b) = L[01]((#)(a,b),(a,b)(#)) * P[01](a,b,(#)(0,1),(0,1)(#)) & id Closed-Interval-TSpace(0,1) = P[01](a,b,(#)(0,1),(0,1)(#)) * L[01]((#)(a,b),(a,b)(#)) proof A1: 0 = (#)(0,1) & 1 = (0,1)(#) by Def1,Def2; set L = L[01]((#)(a,b),(a,b)(#)), P = P[01](a,b,(#)(0,1),(0,1)(#)); assume A2: a < b; then A3: b - a <> 0; A4: a = (#)(a,b) & b = (a,b)(#) by A2,Def1,Def2; for c being Point of Closed-Interval-TSpace(a,b) holds (L*P).c = c proof let c be Point of Closed-Interval-TSpace(a,b); reconsider r = c as Real; A5: P.c = ((b-r)*0 + (r-a)*1)/(b-a) by A2,A1,Def4 .= (r-a)/(b-a); thus (L*P).c = L.(P.c) by FUNCT_2:15 .= (1-((r-a)/(b-a)))*a + ((r-a)/(b-a))*b by A2,A4,A5,Def3 .= ((1*(b-a)-(r-a))/(b-a))*a + ((r-a)/(b-a))*b by A3,XCMPLX_1:127 .= ((b-r)/(b-a))*(a/1) + ((r-a)/(b-a))*b .= ((b-r)*a)/(1*(b-a)) + ((r-a)/(b-a))*b by XCMPLX_1:76 .= ((b-r)*a)/(b-a) + ((r-a)/(b-a))*(b/1) .= ((b-r)*a)/(b-a) + ((r-a)*b)/(1*(b-a)) by XCMPLX_1:76 .= ((a*b-a*r) + (r-a)*b)/(b-a) by XCMPLX_1:62 .= ((b-a)*r)/(b-a) .= c by A3,XCMPLX_1:89; end; hence id Closed-Interval-TSpace(a,b) = L*P by FUNCT_2:124; for c being Point of Closed-Interval-TSpace(0,1) holds (P*L).c = c proof let c be Point of Closed-Interval-TSpace(0,1); reconsider r = c as Real; A6: L.c = (1-r)*a + r*b by A2,A4,Def3 .= r*(b-a) + a; thus (P*L).c = P.(L.c) by FUNCT_2:15 .= ((b-(r*(b-a) + a))*0 + ((r*(b-a) + a)-a)*1)/(b-a) by A2,A1,A6,Def4 .= c by A3,XCMPLX_1:89; end; hence thesis by FUNCT_2:124; end; theorem Th16: a < b implies id Closed-Interval-TSpace(a,b) = L[01]((a,b)(#),(#)(a,b)) * P[01](a,b,(0,1)(#),(#)(0,1)) & id Closed-Interval-TSpace(0,1) = P[01](a,b,(0,1)(#),(#)(0,1)) * L[01]((a,b)(#),(#)(a,b)) proof A1: 0 = (#)(0,1) & 1 = (0,1)(#) by Def1,Def2; set L = L[01]((a,b)(#),(#)(a,b)), P = P[01](a,b,(0,1)(#),(#)(0,1)); assume A2: a < b; then A3: b - a <> 0; A4: a = (#)(a,b) & b = (a,b)(#) by A2,Def1,Def2; for c being Point of Closed-Interval-TSpace(a,b) holds (L*P).c = c proof let c be Point of Closed-Interval-TSpace(a,b); reconsider r = c as Real; A5: P.c = ((b-r)*1 + (r-a)*0)/(b-a) by A2,A1,Def4 .= (b-r)/(b-a); thus (L*P).c = L.(P.c) by FUNCT_2:15 .= (1-((b-r)/(b-a)))*b + ((b-r)/(b-a))*a by A2,A4,A5,Def3 .= ((1*(b-a)-(b-r))/(b-a))*b + ((b-r)/(b-a))*a by A3,XCMPLX_1:127 .= ((r-a)/(b-a))*(b/1) + ((b-r)/(b-a))*a .= ((r-a)*b)/(1*(b-a)) + ((b-r)/(b-a))*a by XCMPLX_1:76 .= ((r-a)*b)/(b-a) + ((b-r)/(b-a))*(a/1) .= ((r-a)*b)/(b-a) + ((b-r)*a)/(1*(b-a)) by XCMPLX_1:76 .= ((b*r-b*a) + (b-r)*a)/(b-a) by XCMPLX_1:62 .= ((b-a)*r)/(b-a) .= c by A3,XCMPLX_1:89; end; hence id Closed-Interval-TSpace(a,b) = L*P by FUNCT_2:124; for c being Point of Closed-Interval-TSpace(0,1) holds (P*L).c = c proof let c be Point of Closed-Interval-TSpace(0,1); reconsider r = c as Real; A6: L.c = (1-r)*b + r*a by A2,A4,Def3 .= r*(a-b) + b; thus (P*L).c = P.(L.c) by FUNCT_2:15 .= ((b-(r*(a-b) + b))*1 + ((r*(a-b) + b)-a)*0)/(b-a) by A2,A1,A6,Def4 .= (r*(-(a-b)))/(b-a) .= c by A3,XCMPLX_1:89; end; hence thesis by FUNCT_2:124; end; theorem Th17: a < b implies L[01]((#)(a,b),(a,b)(#)) is being_homeomorphism & L[01]((#)(a,b),(a,b)(#))" = P[01](a,b,(#)(0,1),(0,1)(#)) & P[01](a,b,(#)(0,1),(0,1)(#)) is being_homeomorphism & P[01](a,b,(#)(0,1),(0,1)(#))" = L[01]((#)(a,b),(a,b)(#)) proof set L = L[01]((#)(a,b),(a,b)(#)), P = P[01](a,b,(#)(0,1),(0,1)(#)); assume A1: a < b; then A2: id (the carrier of Closed-Interval-TSpace(0,1)) = P * L by Th15; then A3: L is one-to-one by FUNCT_2:23; A4: L is continuous & P is continuous Function of Closed-Interval-TSpace(a, b), Closed-Interval-TSpace(0,1) by A1,Th8,Th12; A5: id (the carrier of Closed-Interval-TSpace(a,b)) = id Closed-Interval-TSpace(a,b) .= L * P by A1,Th15; then A6: L is onto by FUNCT_2:23; then A7: rng L = [#](Closed-Interval-TSpace(a,b)); A8: L" = L qua Function" by A3,A6,TOPS_2:def 4; dom L = [#]Closed-Interval-TSpace(0,1) & P = L qua Function" by A2,A3,A7, FUNCT_2:30,def 1; hence L[01]((#)(a,b),(a,b)(#)) is being_homeomorphism by A3,A7,A8,A4, TOPS_2:def 5; thus L[01]((#)(a,b),(a,b)(#))" = P[01](a,b,(#)(0,1),(0,1)(#)) by A2,A3,A7,A8, FUNCT_2:30; A9: P is onto by A2,FUNCT_2:23; then A10: rng P = [#](Closed-Interval-TSpace(0,1)); A11: L is continuous Function of Closed-Interval-TSpace(0,1), Closed-Interval-TSpace(a,b) & P is continuous by A1,Th8,Th12; A12: P is one-to-one by A5,FUNCT_2:23; A13: P" = P qua Function" by A12,A9,TOPS_2:def 4; dom P = [#]Closed-Interval-TSpace(a,b) & L = P qua Function" by A10,A5,A12, FUNCT_2:30,def 1; hence P[01](a,b,(#)(0,1),(0,1)(#)) is being_homeomorphism by A10,A12,A13,A11, TOPS_2:def 5; thus thesis by A10,A5,A12,A13,FUNCT_2:30; end; theorem a < b implies L[01]((a,b)(#),(#)(a,b)) is being_homeomorphism & L[01]((a,b)(#),(#)(a,b))" = P[01](a,b,(0,1)(#),(#)(0,1)) & P[01](a,b,(0,1)(#),(#)(0,1)) is being_homeomorphism & P[01](a,b,(0,1)(#),(#)(0,1))" = L[01]((a,b)(#),(#)(a,b)) proof set L = L[01]((a,b)(#),(#)(a,b)), P = P[01](a,b,(0,1)(#),(#)(0,1)); assume A1: a < b; then A2: id (the carrier of Closed-Interval-TSpace(0,1)) = P * L by Th16; then A3: L is one-to-one by FUNCT_2:23; A4: L is continuous & P is continuous Function of Closed-Interval-TSpace(a, b), Closed-Interval-TSpace(0,1) by A1,Th8,Th12; A5: id (the carrier of Closed-Interval-TSpace(a,b)) = id Closed-Interval-TSpace(a,b) .= L * P by A1,Th16; then A6: L is onto by FUNCT_2:23; then A7: rng L = [#](Closed-Interval-TSpace(a,b)); A8: L" = L qua Function" by A3,A6,TOPS_2:def 4; dom L = [#]Closed-Interval-TSpace(0,1) & P = L qua Function" by A2,A3,A7, FUNCT_2:30,def 1; hence L[01]((a,b)(#),(#)(a,b)) is being_homeomorphism by A3,A7,A8,A4, TOPS_2:def 5; thus L[01]((a,b)(#),(#)(a,b))" = P[01](a,b,(0,1)(#),(#)(0,1)) by A2,A3,A7,A8, FUNCT_2:30; A9: P is onto by A2,FUNCT_2:23; then A10: rng P = [#](Closed-Interval-TSpace(0,1)); A11: L is continuous Function of Closed-Interval-TSpace(0,1), Closed-Interval-TSpace(a,b) & P is continuous by A1,Th8,Th12; A12: P is one-to-one by A5,FUNCT_2:23; A13: P" = P qua Function" by A12,A9,TOPS_2:def 4; dom P = [#]Closed-Interval-TSpace(a,b) & L = P qua Function" by A10,A5,A12, FUNCT_2:30,def 1; hence P[01](a,b,(0,1)(#),(#)(0,1)) is being_homeomorphism by A10,A12,A13,A11, TOPS_2:def 5; thus thesis by A10,A5,A12,A13,FUNCT_2:30; end; begin :: 3. Connectedness of Intervals and Brouwer Fixed Point Theorem for Intervals. theorem Th19: I[01] is connected proof for A,B being Subset of I[01] st [#]I[01] = A \/ B & A <> {}I[01] & B <> {}I[01] & A is closed & B is closed holds A meets B proof let A,B be Subset of I[01]; assume that A1: [#]I[01] = A \/ B and A2: A <> {}I[01] and A3: B <> {}I[01] and A4: A is closed and A5: B is closed; reconsider P = A, Q = B as Subset of REAL by BORSUK_1:40,XBOOLE_1:1; assume A6: A misses B; set x = the Element of P; reconsider x as Real; A7: now take x; thus x in P by A2; end; set x = the Element of Q; reconsider x as Real; A8: now take x; thus x in Q by A3; end; A9: the carrier of RealSpace = the carrier of TopSpaceMetr(RealSpace) by TOPMETR:12; 0 is LowerBound of P proof let r be ExtReal; assume r in P; then r in [.0,1.] by BORSUK_1:40; then r in {w where w is Real: 0<=w & w<=1} by RCOMP_1:def 1; then ex u being Real st u = r & 0<=u & u<=1; hence 0 <= r; end; then A10: P is bounded_below; 0 is LowerBound of Q proof let r be ExtReal; assume r in Q; then r in [.0,1.] by BORSUK_1:40; then r in {w where w is Real : 0<=w & w<=1} by RCOMP_1:def 1; then ex u being Real st u = r & 0<=u & u<=1; hence 0 <= r; end; then A11: Q is bounded_below; reconsider A0 = P, B0 = Q as Subset of R^1 by METRIC_1:def 13,TOPMETR:12 ,def 6; A12: I[01] is closed SubSpace of R^1 by Th2,TOPMETR:20; then A13: A0 is closed by A4,TSEP_1:12; A14: B0 is closed by A5,A12,TSEP_1:12; 0 in {w where w is Real: 0<=w & w<=1}; then A15: 0 in [.0,1.] by RCOMP_1:def 1; now per cases by A1,A15,BORSUK_1:40,XBOOLE_0:def 3; suppose A16: 0 in P; reconsider B00 = B0` as Subset of R^1; set l = lower_bound Q; l in REAL by XREAL_0:def 1; then reconsider m = l as Point of RealSpace by METRIC_1:def 13; reconsider t = m as Point of R^1 by TOPMETR:12,def 6; set W = {w where w is Real : 0<=w & w 0 and A20: Ball(m,s) c= B0` by A18,TOPMETR:15,def 6; consider r being Real such that A21: r in Q and A22: r < l+s by A8,A11,A19,SEQ_4:def 2; reconsider r as Element of REAL by XREAL_0:def 1; l <= r by A11,A21,SEQ_4:def 2; then l - r <= 0 by XREAL_1:47; then A23: -s < -(l - r) by A19,XREAL_1:24; reconsider rm = r as Point of RealSpace by METRIC_1:def 13; r - l < s by A22,XREAL_1:19; then |.r - l.| < s by A23,SEQ_2:1; then (the distance of RealSpace).(rm,m) < s by METRIC_1:def 12,def 13 ; then dist(m,rm) < s by METRIC_1:def 1; then rm in {q where q is Element of RealSpace : dist(m,q) 0 and A32: Ball(m,e) c= G by A30,TOPMETR:15,def 6; reconsider e as Element of REAL by XREAL_0:def 1; reconsider e0 = max(0,l - (e/2)) as Element of REAL by XREAL_0:def 1; reconsider e1 = e0 as Point of RealSpace by METRIC_1:def 13; A33: e*(1/2) < e*1 by A31,XREAL_1:68; now per cases by XXREAL_0:16; suppose A34: e0 = 0; then l <= e/2 by XREAL_1:50,XXREAL_0:25; then l < e by A33,XXREAL_0:2; hence |.l-e0.| < e by A24,A34,ABSVALUE:def 1; end; suppose e0 = l - (e/2); hence |.l-e0.| < e by A31,A33,ABSVALUE:def 1; end; end; then (the distance of RealSpace).(m,e1) < e by METRIC_1:def 12,def 13 ; then dist(m,e1) < e by METRIC_1:def 1; then e1 in {z where z is Element of RealSpace : dist(m,z) 0 and A42: Ball(m,s) c= A0` by A40,TOPMETR:15,def 6; consider r being Real such that A43: r in P and A44: r < l+s by A7,A10,A41,SEQ_4:def 2; reconsider r as Element of REAL by XREAL_0:def 1; l <= r by A10,A43,SEQ_4:def 2; then l - r <= 0 by XREAL_1:47; then A45: -s < -(l - r) by A41,XREAL_1:24; reconsider rm = r as Point of RealSpace by METRIC_1:def 13; A46: (real_dist).(r,l) = dist(rm,m) by METRIC_1:def 1,def 13; r - l < s by A44,XREAL_1:19; then |.r - l.| < s by A45,SEQ_2:1; then dist(rm,m) < s by METRIC_1:def 12,A46; then rm in {q where q is Element of RealSpace : dist(m,q) 0 and A55: Ball(m,e) c= G by A53,TOPMETR:15,def 6; reconsider e as Element of REAL by XREAL_0:def 1; reconsider e0 = max(0,l - (e/2)) as Element of REAL by XREAL_0:def 1; reconsider e1 = e0 as Point of RealSpace by METRIC_1:def 13; A56: e*(1/2) < e*1 by A54,XREAL_1:68; A57: (real_dist).(l,e0) = dist(m,e1) by METRIC_1:def 1,def 13; now per cases by XXREAL_0:16; suppose A58: e0 = 0; then l <= e/2 by XREAL_1:50,XXREAL_0:25; then l < e by A56,XXREAL_0:2; hence |.l-e0.| < e by A47,A58,ABSVALUE:def 1; end; suppose e0 = l - (e/2); hence |.l-e0.| < e by A54,A56,ABSVALUE:def 1; end; end; then dist(m,e1) < e by METRIC_1:def 12,A57; then e1 in {z where z is Element of RealSpace : dist(m,z) {} by XXREAL_1:1; then [.0,1.] = dom F by FUNCT_2:def 1; then F.0 in rng F by A5,FUNCT_1:def 3; then A7: 0 in B by A5; A8: [.0,1.] = {q where q is Real: 0<=q & q<=1 } by RCOMP_1:def 1; A9: [.0,1.] c= A \/ B proof let x be object; assume A10: x in [.0,1.]; then reconsider y = x as Real; ex p being Real st p = y & 0<=p & p<=1 by A8,A10; then A11: [.0,1.] = [.0,y.] \/ [.y,1.] by XXREAL_1:174; [.0,1.] = dom F by A6,FUNCT_2:def 1; then A12: F.y in rng F by A10,FUNCT_1:def 3; now per cases by A11,A12,XBOOLE_0:def 3; suppose A13: F.y in [.0,y.]; A14: A c= A \/ B by XBOOLE_1:7; y in A by A10,A13; hence y in A \/ B by A14; end; suppose A15: F.y in [.y,1.]; A16: B c= A \/ B by XBOOLE_1:7; y in B by A10,A15; hence y in A \/ B by A16; end; end; hence thesis; end; 1 in {w where w is Real: 0<=w & w<=1}; then A17: 1 in [.0,1.] by RCOMP_1:def 1; A18: B c= [.0,1.] proof let x be object; assume A19: x in B; then reconsider x as Real; ex b0 being Real st b0 = x & b0 in [.0,1.] & F.b0 in [.b0,1.] by A19; hence thesis; end; assume A20: for x being Point of I[01] holds f.x <> x; A21: A /\ B = {} proof set x = the Element of A /\ B; assume A22: A /\ B <> {}; then x in A by XBOOLE_0:def 4; then A23: ex z being Real st z = x & z in [.0,1.] & F.z in [.0,z.]; reconsider x as Real; x in B by A22,XBOOLE_0:def 4; then ex b0 being Real st b0 = x & b0 in [.0,1.] & F.b0 in [.b0,1.]; then A24: F.x in [.0,x.] /\ [.x,1.] by A23,XBOOLE_0:def 4; x in {q where q is Real: 0<=q & q<=1 } by A23,RCOMP_1:def 1; then ex u being Real st u = x & 0<=u & u<=1; then F.x in {x} by A24,XXREAL_1:418; then F.x = x by TARSKI:def 1; hence contradiction by A20,A23,BORSUK_1:40; end; then A25: A misses B by XBOOLE_0:def 7; [.0,1.] = dom F by A6,FUNCT_2:def 1; then F.1 in rng F by A17,FUNCT_1:def 3; then A26: 1 in A by A17; ex P,Q being Subset of I[01] st [#] I[01] = P \/ Q & P <> {}I[01] & Q <> {}I[01] & P is closed & Q is closed & P misses Q proof reconsider P = A, Q = B as Subset of I[01] by A2,A18,BORSUK_1:40; take P,Q; thus A27: [#]I[01] = P \/ Q by A9,BORSUK_1:40,XBOOLE_0:def 10; thus P <> {}I[01] & Q <> {}I[01] by A26,A7; thus P is closed proof set z = the Element of (Cl P) /\ Q; assume not P is closed; then A28: Cl P <> P by PRE_TOPC:22; A29: (Cl P) /\ Q <> {} proof assume (Cl P) /\ Q = {}; then (Cl P) misses Q by XBOOLE_0:def 7; then A30: Cl P c= Q` by SUBSET_1:23; P c= Cl P & P = Q` by A25,A27,PRE_TOPC:5,18; hence contradiction by A28,A30,XBOOLE_0:def 10; end; then A31: z in Cl P by XBOOLE_0:def 4; A32: z in Q by A29,XBOOLE_0:def 4; reconsider z as Point of I[01] by A31; reconsider t0 = z as Real; A33: ex c being Real st c = t0 & c in [.0,1.] & F.c in [.c,1.] by A32; then reconsider s0 = F.t0 as Real; t0 <= s0 by A33,XXREAL_1:1; then A34: 0 <= s0 - t0 by XREAL_1:48; set r = (s0 - t0) * 2"; reconsider m = z, n = f.z as Point of Closed-Interval-MSpace(0,1) by BORSUK_1:40,TOPMETR:10; reconsider W = Ball(n,r) as Subset of I[01] by BORSUK_1:40,TOPMETR:10; A35: W is open & f is_continuous_at z by A1,TMAP_1:50,TOPMETR:14,20; A36: s0 - t0 <> 0 by A20; then A37: 0 / 2 < (s0 - t0) / 2 by A34,XREAL_1:74; then f.z in W by TBSP_1:11; then consider V being Subset of I[01] such that A38: V is open & z in V and A39: f.:V c= W by A35,TMAP_1:43; consider s being Real such that A40: s > 0 and A41: Ball(m,s) c= V by A1,A38,TOPMETR:15,20; reconsider s as Real; set r0 = min(s,r); reconsider W0 = Ball(m,r0) as Subset of I[01] by BORSUK_1:40,TOPMETR:10; r0 > 0 by A37,A40,XXREAL_0:15; then A42: z in W0 by TBSP_1:11; set w = the Element of P /\ W0; W0 is open by A1,TOPMETR:14,20; then P meets W0 by A31,A42,PRE_TOPC:24; then A43: P /\ W0 <> {}I[01] by XBOOLE_0:def 7; then A44: w in P by XBOOLE_0:def 4; A45: w in W0 by A43,XBOOLE_0:def 4; then reconsider w as Point of Closed-Interval-MSpace(0,1); reconsider w1 = w as Point of I[01] by A44; reconsider d = w1 as Real; A46: d in A by A43,XBOOLE_0:def 4; Ball(m,r0) = {q where q is Element of Closed-Interval-MSpace(0,1): dist(m,q) Q by PRE_TOPC:22; A60: (Cl Q) /\ P <> {} proof assume (Cl Q) /\ P = {}; then (Cl Q) misses P by XBOOLE_0:def 7; then A61: Cl Q c= P` by SUBSET_1:23; Q c= Cl Q & Q = P` by A25,A27,PRE_TOPC:5,18; hence contradiction by A59,A61,XBOOLE_0:def 10; end; then A62: z in Cl Q by XBOOLE_0:def 4; A63: z in P by A60,XBOOLE_0:def 4; reconsider z as Point of I[01] by A62; reconsider t0 = z as Real; A64: ex c being Real st c = t0 & c in [.0,1.] & F.c in [.0,c.] by A63; then reconsider s0 = F.t0 as Real; s0 <= t0 by A64,XXREAL_1:1; then A65: 0 <= t0 - s0 by XREAL_1:48; set r = (t0 - s0) * 2"; reconsider m = z, n = f.z as Point of Closed-Interval-MSpace(0,1) by BORSUK_1:40,TOPMETR:10; reconsider W = Ball(n,r) as Subset of I[01] by BORSUK_1:40,TOPMETR:10; A66: W is open & f is_continuous_at z by A1,TMAP_1:50,TOPMETR:14,20; A67: t0 - s0 <> 0 by A20; then A68: 0 / 2 < (t0 - s0) / 2 by A65,XREAL_1:74; then f.z in W by TBSP_1:11; then consider V being Subset of I[01] such that A69: V is open & z in V and A70: f.:V c= W by A66,TMAP_1:43; consider s being Real such that A71: s > 0 and A72: Ball(m,s) c= V by A1,A69,TOPMETR:15,20; reconsider s as Real; set r0 = min(s,r); reconsider W0 = Ball(m,r0) as Subset of I[01] by BORSUK_1:40,TOPMETR:10; r0 > 0 by A68,A71,XXREAL_0:15; then A73: z in W0 by TBSP_1:11; set w = the Element of Q /\ W0; W0 is open by A1,TOPMETR:14,20; then Q meets W0 by A62,A73,PRE_TOPC:24; then A74: Q /\ W0 <> {}I[01] by XBOOLE_0:def 7; then A75: w in Q by XBOOLE_0:def 4; A76: w in W0 by A74,XBOOLE_0:def 4; then reconsider w as Point of Closed-Interval-MSpace(0,1); reconsider w1 = w as Point of I[01] by A75; reconsider d = w1 as Real; A77: d in B by A74,XBOOLE_0:def 4; Ball(m,r0) = {q where q is Element of Closed-Interval-MSpace(0,1): dist(m,q)