:: TREAL_1 semantic presentation begin Lm1: for a, b being real number for x being set st x in [.a,b.] holds x is Real ; Lm2: for a, b being real number for x being Point of (Closed-Interval-TSpace (a,b)) st a <= b holds x is Real proof let a, b be real number ; ::_thesis: for x being Point of (Closed-Interval-TSpace (a,b)) st a <= b holds x is Real let x be Point of (Closed-Interval-TSpace (a,b)); ::_thesis: ( a <= b implies x is Real ) assume a <= b ; ::_thesis: x is Real then the carrier of (Closed-Interval-TSpace (a,b)) = [.a,b.] by TOPMETR:18; hence x is Real by Lm1; ::_thesis: verum end; theorem Th1: :: TREAL_1:1 for a, b being real number for A being Subset of R^1 st A = [.a,b.] holds A is closed proof let a, b be real number ; ::_thesis: for A being Subset of R^1 st A = [.a,b.] holds A is closed let A be Subset of R^1; ::_thesis: ( A = [.a,b.] implies A is closed ) assume A1: A = [.a,b.] ; ::_thesis: A is closed reconsider B = A ` as Subset of (TopSpaceMetr RealSpace) by TOPMETR:def_6; reconsider a = a, b = b as Real by XREAL_0:def_1; 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 holds ex r being real number st ( r > 0 & Ball (c,r) c= B ) proof let c be Point of RealSpace; ::_thesis: ( c in B implies ex r being real number st ( r > 0 & Ball (c,r) c= B ) ) reconsider n = c as Real by METRIC_1:def_13; assume c in B ; ::_thesis: ex r being real number st ( r > 0 & Ball (c,r) c= 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__::_thesis:_ex_r_being_Element_of_REAL_st_ (_r_>_0_&_Ball_(c,r)_c=_B_) percases ( not a <= n or not n <= b ) by A3; supposeA4: not a <= n ; ::_thesis: ex r being Element of REAL st ( r > 0 & Ball (c,r) c= B ) take r = a - n; ::_thesis: ( r > 0 & Ball (c,r) c= B ) now__::_thesis:_for_x_being_set_st_x_in_Ball_(c,r)_holds_ x_in_B let x be set ; ::_thesis: ( x in Ball (c,r) implies x in B ) assume A5: x in Ball (c,r) ; ::_thesis: x in B then reconsider t = x as 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) < r } by METRIC_1:17; then ex v being Element of RealSpace st ( v = u & dist (c,v) < r ) by A5; then real_dist . (t,n) < r by METRIC_1:def_1, METRIC_1:def_13; then A6: abs (t - n) < r by METRIC_1:def_12; t - n <= abs (t - n) by ABSVALUE:4; then t - n < a - n by A6, XXREAL_0:2; then for q being Real holds ( not q = t or not a <= q or not q <= b ) by XREAL_1:9; then not t in { p where p is Real : ( a <= p & p <= b ) } ; then not u in D ` by A1, A2, RCOMP_1:def_1, TOPMETR:def_6; hence x in B by SUBSET_1:29; ::_thesis: verum end; hence ( r > 0 & Ball (c,r) c= B ) by A4, TARSKI:def_3, XREAL_1:50; ::_thesis: verum end; supposeA7: not n <= b ; ::_thesis: ex r being Element of REAL st ( r > 0 & Ball (c,r) c= B ) take r = n - b; ::_thesis: ( r > 0 & Ball (c,r) c= B ) now__::_thesis:_for_x_being_set_st_x_in_Ball_(c,r)_holds_ x_in_B let x be set ; ::_thesis: ( x in Ball (c,r) implies x in B ) assume A8: x in Ball (c,r) ; ::_thesis: x in B then reconsider t = x as 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) < r } by METRIC_1:17; then ex v being Element of RealSpace st ( v = u & dist (c,v) < r ) by A8; then real_dist . (n,t) < r by METRIC_1:def_1, METRIC_1:def_13; then A9: abs (n - t) < r by METRIC_1:def_12; n - t <= abs (n - t) by ABSVALUE:4; then n - t < n - b by A9, XXREAL_0:2; then for q being Real holds ( not q = t or not a <= q or not q <= b ) by XREAL_1:10; then not t in { p where p is Real : ( a <= p & p <= b ) } ; then not u in D ` by A1, A2, RCOMP_1:def_1, TOPMETR:def_6; hence x in B by SUBSET_1:29; ::_thesis: verum end; hence ( r > 0 & Ball (c,r) c= B ) by A7, TARSKI:def_3, XREAL_1:50; ::_thesis: verum end; end; end; hence ex r being real number st ( r > 0 & Ball (c,r) c= B ) ; ::_thesis: verum end; then A ` is open by TOPMETR:15, TOPMETR:def_6; hence A is closed by TOPS_1:3; ::_thesis: verum end; theorem Th2: :: TREAL_1:2 for a, b being real number st a <= b holds Closed-Interval-TSpace (a,b) is closed proof let a, b be real number ; ::_thesis: ( a <= b implies Closed-Interval-TSpace (a,b) is closed ) assume a <= b ; ::_thesis: Closed-Interval-TSpace (a,b) is closed then the carrier of (Closed-Interval-TSpace (a,b)) = [.a,b.] by TOPMETR:18; then for A being Subset of R^1 st A = the carrier of (Closed-Interval-TSpace (a,b)) holds A is closed by Th1; hence Closed-Interval-TSpace (a,b) is closed by BORSUK_1:def_11; ::_thesis: verum end; theorem :: TREAL_1:3 for a, c, d, b being real number st a <= c & d <= b & c <= d holds Closed-Interval-TSpace (c,d) is closed SubSpace of Closed-Interval-TSpace (a,b) proof let a, c, d, b be real number ; ::_thesis: ( a <= c & d <= b & c <= d implies Closed-Interval-TSpace (c,d) is closed SubSpace of Closed-Interval-TSpace (a,b) ) assume that A1: a <= c and A2: d <= b and A3: c <= d ; ::_thesis: Closed-Interval-TSpace (c,d) is closed SubSpace of Closed-Interval-TSpace (a,b) [.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 Closed-Interval-TSpace (c,d) is closed SubSpace of Closed-Interval-TSpace (a,b) by A5, TSEP_1:14; ::_thesis: verum end; theorem :: TREAL_1:4 for a, c, b, d being real number st a <= c & b <= d & c <= b holds ( 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 let a, c, b, d be real number ; ::_thesis: ( 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)) ) ) assume that A1: a <= c and A2: b <= d and A3: c <= b ; ::_thesis: ( 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)) ) 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; ::_thesis: Closed-Interval-TSpace (c,b) = (Closed-Interval-TSpace (a,b)) meet (Closed-Interval-TSpace (c,d)) 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 Closed-Interval-TSpace (c,b) = (Closed-Interval-TSpace (a,b)) meet (Closed-Interval-TSpace (c,d)) by A4, A6, A7, TSEP_1:def_4; ::_thesis: verum end; definition let a, b be real number ; assume A1: a <= b ; func (#) (a,b) -> Point of (Closed-Interval-TSpace (a,b)) equals :Def1: :: TREAL_1:def 1 a; coherence a is Point of (Closed-Interval-TSpace (a,b)) proof a in [.a,b.] by A1, XXREAL_1:1; hence a is Point of (Closed-Interval-TSpace (a,b)) by A1, TOPMETR:18; ::_thesis: verum end; correctness ; func(a,b) (#) -> Point of (Closed-Interval-TSpace (a,b)) equals :Def2: :: TREAL_1:def 2 b; coherence b is Point of (Closed-Interval-TSpace (a,b)) proof b in [.a,b.] by A1, XXREAL_1:1; hence b is Point of (Closed-Interval-TSpace (a,b)) by A1, TOPMETR:18; ::_thesis: verum end; correctness ; end; :: deftheorem Def1 defines (#) TREAL_1:def_1_:_ for a, b being real number st a <= b holds (#) (a,b) = a; :: deftheorem Def2 defines (#) TREAL_1:def_2_:_ for a, b being real number st a <= b holds (a,b) (#) = b; theorem :: TREAL_1:5 ( 0[01] = (#) (0,1) & 1[01] = (0,1) (#) ) by Def1, Def2, BORSUK_1:def_14, BORSUK_1:def_15; theorem :: TREAL_1:6 for a, b, c being real number st a <= b & b <= c holds ( (#) (a,b) = (#) (a,c) & (b,c) (#) = (a,c) (#) ) proof let a, b, c be real number ; ::_thesis: ( a <= b & b <= c implies ( (#) (a,b) = (#) (a,c) & (b,c) (#) = (a,c) (#) ) ) assume that A1: a <= b and A2: b <= c ; ::_thesis: ( (#) (a,b) = (#) (a,c) & (b,c) (#) = (a,c) (#) ) thus (#) (a,b) = a by A1, Def1 .= (#) (a,c) by A1, A2, Def1, XXREAL_0:2 ; ::_thesis: (b,c) (#) = (a,c) (#) thus (b,c) (#) = c by A2, Def2 .= (a,c) (#) by A1, A2, Def2, XXREAL_0:2 ; ::_thesis: verum end; begin definition let a, b be real number ; assume B1: 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: :: TREAL_1:def 3 for s being Point of (Closed-Interval-TSpace (0,1)) holds it . s = ((1 - s) * t1) + (s * t2); existence ex b1 being Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (a,b)) st for s being Point of (Closed-Interval-TSpace (0,1)) holds b1 . s = ((1 - s) * t1) + (s * t2) proof reconsider r1 = t1, r2 = t2 as Real by B1, Lm2; deffunc H1( Element of REAL ) -> Element of REAL = ((1 - $1) * r1) + ($1 * r2); consider LI being Function of REAL,REAL such that A1: for r being Real holds LI . r = H1(r) from FUNCT_2:sch_4(); A2: [.a,b.] = the carrier of (Closed-Interval-TSpace (a,b)) by B1, TOPMETR:18; now__::_thesis:_for_y_being_set_st_y_in_rng_(LI_|_[.0,1.])_holds_ y_in_[.a,b.] let y be set ; ::_thesis: ( y in rng (LI | [.0,1.]) implies y in [.a,b.] ) assume A3: y in rng (LI | [.0,1.]) ; ::_thesis: y in [.a,b.] then reconsider d = y as Real ; y in LI .: [.0,1.] by A3, RELAT_1:115; then consider x being set such that x in dom LI and A4: x in [.0,1.] and A5: y = LI . x by FUNCT_1:def_6; reconsider c = x as Real by A4; A6: d = ((1 - c) * r1) + (c * r2) by A1, A5; r1 in [.a,b.] by A2; then r1 in { p where p is Real : ( a <= p & p <= b ) } by RCOMP_1:def_1; then A7: ex v1 being Real st ( v1 = r1 & a <= v1 & v1 <= b ) ; c in { p where p is Real : ( 0 <= p & p <= 1 ) } by A4, RCOMP_1:def_1; then A8: ex u being Real st ( u = c & 0 <= u & u <= 1 ) ; r2 in [.a,b.] by A2; then r2 in { p where p is Real : ( a <= p & p <= b ) } by RCOMP_1:def_1; then A9: ex v2 being Real st ( v2 = r2 & a <= v2 & v2 <= b ) ; then A10: c * a <= c * r2 by A8, XREAL_1:64; A11: c * r2 <= c * b by A8, A9, XREAL_1:64; A12: 0 <= 1 - c by A8, XREAL_1:48; then (1 - c) * r1 <= (1 - c) * b by A7, XREAL_1:64; then A13: d <= ((1 - c) * b) + (c * b) by A6, A11, XREAL_1:7; (1 - c) * a <= (1 - c) * r1 by A7, A12, XREAL_1:64; then ((1 - c) * a) + (c * a) <= d by A6, A10, XREAL_1:7; then y in { q where q is Real : ( a <= q & q <= b ) } by A13; hence y in [.a,b.] by RCOMP_1:def_1; ::_thesis: verum end; then A14: rng (LI | [.0,1.]) c= the carrier of (Closed-Interval-TSpace (a,b)) by A2, TARSKI:def_3; A15: 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 A15, TOPMETR:18; then reconsider F = LI | [.0,1.] as Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (a,b)) by A14, FUNCT_2:def_1, RELSET_1:4; take F ; ::_thesis: for s being Point of (Closed-Interval-TSpace (0,1)) holds F . s = ((1 - s) * t1) + (s * t2) let s be Point of (Closed-Interval-TSpace (0,1)); ::_thesis: F . s = ((1 - s) * t1) + (s * t2) A16: s is 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 .= ((1 - s) * t1) + (s * t2) by A1, A16 ; ::_thesis: verum end; uniqueness for b1, b2 being Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (a,b)) st ( for s being Point of (Closed-Interval-TSpace (0,1)) holds b1 . s = ((1 - s) * t1) + (s * t2) ) & ( for s being Point of (Closed-Interval-TSpace (0,1)) holds b2 . s = ((1 - s) * t1) + (s * t2) ) holds b1 = b2 proof let F1, F2 be Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (a,b)); ::_thesis: ( ( for s being Point of (Closed-Interval-TSpace (0,1)) holds F1 . s = ((1 - s) * t1) + (s * t2) ) & ( for s being Point of (Closed-Interval-TSpace (0,1)) holds F2 . s = ((1 - s) * t1) + (s * t2) ) implies F1 = F2 ) assume A17: for s being Point of (Closed-Interval-TSpace (0,1)) holds F1 . s = ((1 - s) * t1) + (s * t2) ; ::_thesis: ( ex s being Point of (Closed-Interval-TSpace (0,1)) st not F2 . s = ((1 - s) * t1) + (s * t2) or F1 = F2 ) assume A18: for s being Point of (Closed-Interval-TSpace (0,1)) holds F2 . s = ((1 - s) * t1) + (s * t2) ; ::_thesis: F1 = F2 for s being Point of (Closed-Interval-TSpace (0,1)) holds F1 . s = F2 . s proof reconsider r1 = t1, r2 = t2 as Real by B1, Lm2; let s be Point of (Closed-Interval-TSpace (0,1)); ::_thesis: F1 . s = F2 . s reconsider r = s as Real by Lm2; thus F1 . s = ((1 - r) * r1) + (r * r2) by A17 .= F2 . s by A18 ; ::_thesis: verum end; hence F1 = F2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def3 defines L[01] TREAL_1:def_3_:_ for a, b being real number st a <= b holds for t1, t2 being Point of (Closed-Interval-TSpace (a,b)) for b5 being Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (a,b)) holds ( b5 = L[01] (t1,t2) iff for s being Point of (Closed-Interval-TSpace (0,1)) holds b5 . s = ((1 - s) * t1) + (s * t2) ); theorem Th7: :: TREAL_1:7 for a, b being real number st a <= b holds 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 let a, b be real number ; ::_thesis: ( 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 ) assume A1: a <= b ; ::_thesis: 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 let t1, t2 be Point of (Closed-Interval-TSpace (a,b)); ::_thesis: for s being Point of (Closed-Interval-TSpace (0,1)) holds (L[01] (t1,t2)) . s = ((t2 - t1) * s) + t1 let s be Point of (Closed-Interval-TSpace (0,1)); ::_thesis: (L[01] (t1,t2)) . s = ((t2 - t1) * s) + t1 thus (L[01] (t1,t2)) . s = ((1 - s) * t1) + (s * t2) by A1, Def3 .= ((t2 - t1) * s) + t1 ; ::_thesis: verum end; theorem Th8: :: TREAL_1:8 for a, b being real number st a <= b holds for t1, t2 being Point of (Closed-Interval-TSpace (a,b)) holds L[01] (t1,t2) is continuous proof let a, b be real number ; ::_thesis: ( a <= b implies for t1, t2 being Point of (Closed-Interval-TSpace (a,b)) holds L[01] (t1,t2) is continuous ) assume A1: a <= b ; ::_thesis: for t1, t2 being Point of (Closed-Interval-TSpace (a,b)) holds L[01] (t1,t2) is continuous let t1, t2 be Point of (Closed-Interval-TSpace (a,b)); ::_thesis: L[01] (t1,t2) is continuous reconsider r1 = t1, r2 = t2 as Real by A1, Lm2; deffunc H1( Element of REAL ) -> Element of REAL = ((r2 - r1) * $1) + r1; consider L being Function of REAL,REAL such that A2: for r being Real holds L . r = H1(r) from FUNCT_2:sch_4(); reconsider f = L as Function of R^1,R^1 by TOPMETR:17; A3: for s being Point of (Closed-Interval-TSpace (0,1)) for 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)); ::_thesis: for w being Point of R^1 st s = w holds (L[01] (t1,t2)) . s = f . w let w be Point of R^1; ::_thesis: ( s = w implies (L[01] (t1,t2)) . s = f . w ) reconsider r = s as Real by Lm2; assume A4: s = w ; ::_thesis: (L[01] (t1,t2)) . s = f . w thus (L[01] (t1,t2)) . s = ((r2 - r1) * r) + r1 by A1, Th7 .= f . w by A2, A4 ; ::_thesis: verum end; A5: [.0,1.] = the carrier of (Closed-Interval-TSpace (0,1)) by TOPMETR:18; A6: f is continuous by A2, 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)); ::_thesis: L[01] (t1,t2) is_continuous_at s reconsider w = s as Point of R^1 by A5, 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 holds 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)); ::_thesis: ( G is open & (L[01] (t1,t2)) . s in G implies ex H being Subset of (Closed-Interval-TSpace (0,1)) st ( H is open & s in H & (L[01] (t1,t2)) .: H c= G ) ) assume G is open ; ::_thesis: ( not (L[01] (t1,t2)) . s in G or ex H being Subset of (Closed-Interval-TSpace (0,1)) st ( H is open & s in H & (L[01] (t1,t2)) .: H c= G ) ) then consider G0 being Subset of R^1 such that A7: G0 is open and A8: G0 /\ ([#] (Closed-Interval-TSpace (a,b))) = G by TOPS_2:24; A9: f is_continuous_at w by A6, TMAP_1:44; assume (L[01] (t1,t2)) . s in G ; ::_thesis: ex H being Subset of (Closed-Interval-TSpace (0,1)) st ( H is open & s in H & (L[01] (t1,t2)) .: H c= G ) then f . w in G by A3; then f . w in G0 by A8, XBOOLE_0:def_4; then consider H0 being Subset of R^1 such that A10: H0 is open and A11: w in H0 and A12: f .: H0 c= G0 by A7, A9, TMAP_1:43; now__::_thesis:_ex_H_being_Subset_of_(Closed-Interval-TSpace_(0,1))_st_ (_H_is_open_&_s_in_H_&_(L[01]_(t1,t2))_.:_H_c=_G_) reconsider H = H0 /\ ([#] (Closed-Interval-TSpace (0,1))) as Subset of (Closed-Interval-TSpace (0,1)) ; take H = H; ::_thesis: ( H is open & s in H & (L[01] (t1,t2)) .: H c= G ) thus H is open by A10, TOPS_2:24; ::_thesis: ( s in H & (L[01] (t1,t2)) .: H c= G ) thus s in H by A11, XBOOLE_0:def_4; ::_thesis: (L[01] (t1,t2)) .: H c= G thus (L[01] (t1,t2)) .: H c= G ::_thesis: verum proof let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in (L[01] (t1,t2)) .: H or t in G ) assume t in (L[01] (t1,t2)) .: H ; ::_thesis: t in G then consider r being set such that r in dom (L[01] (t1,t2)) and A13: r in H and A14: t = (L[01] (t1,t2)) . r by FUNCT_1:def_6; A15: r in the carrier of (Closed-Interval-TSpace (0,1)) by A13; reconsider r = r as Point of (Closed-Interval-TSpace (0,1)) by A13; r in dom (L[01] (t1,t2)) by A15, FUNCT_2:def_1; then A16: t in (L[01] (t1,t2)) .: the carrier of (Closed-Interval-TSpace (0,1)) by A14, FUNCT_1:def_6; reconsider p = r as Point of R^1 by A5, TARSKI:def_3, TOPMETR:17; p in [#] R^1 ; then A17: p in dom f by FUNCT_2:def_1; ( t = f . p & p in H0 ) by A3, A13, A14, XBOOLE_0:def_4; then t in f .: H0 by A17, FUNCT_1:def_6; hence t in G by A8, A12, A16, XBOOLE_0:def_4; ::_thesis: verum end; end; hence ex H being Subset of (Closed-Interval-TSpace (0,1)) st ( H is open & s in H & (L[01] (t1,t2)) .: H c= G ) ; ::_thesis: verum end; hence L[01] (t1,t2) is_continuous_at s by TMAP_1:43; ::_thesis: verum end; hence L[01] (t1,t2) is continuous by TMAP_1:44; ::_thesis: verum end; theorem :: TREAL_1:9 for a, b being real number st a <= b holds 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 let a, b be real number ; ::_thesis: ( 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 ) ) assume A1: a <= b ; ::_thesis: 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 ) let t1, t2 be Point of (Closed-Interval-TSpace (a,b)); ::_thesis: ( (L[01] (t1,t2)) . ((#) (0,1)) = t1 & (L[01] (t1,t2)) . ((0,1) (#)) = t2 ) reconsider r1 = t1, r2 = t2 as Real by A1, Lm2; 0 = (#) (0,1) by Def1; hence (L[01] (t1,t2)) . ((#) (0,1)) = ((1 - 0) * r1) + (0 * r2) by A1, Def3 .= t1 ; ::_thesis: (L[01] (t1,t2)) . ((0,1) (#)) = t2 1 = (0,1) (#) by Def2; hence (L[01] (t1,t2)) . ((0,1) (#)) = ((1 - 1) * r1) + (1 * r2) by A1, Def3 .= t2 ; ::_thesis: verum end; theorem :: TREAL_1:10 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)); ::_thesis: (L[01] (((#) (0,1)),((0,1) (#)))) . x = x reconsider y = x as Real by Lm2; ( (#) (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 ; ::_thesis: verum end; hence L[01] (((#) (0,1)),((0,1) (#))) = id (Closed-Interval-TSpace (0,1)) by FUNCT_2:124; ::_thesis: verum end; definition let a, b be real number ; assume B1: 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: :: TREAL_1:def 4 for s being Point of (Closed-Interval-TSpace (a,b)) holds it . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a); existence ex b1 being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (0,1)) st for s being Point of (Closed-Interval-TSpace (a,b)) holds b1 . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) proof reconsider a1 = a, b1 = b as Real by XREAL_0:def_1; reconsider r1 = t1, r2 = t2 as Real by Lm2; deffunc H1( Element of REAL ) -> Element of REAL = (((b1 - $1) * r1) + (($1 - a1) * r2)) / (b1 - a1); consider PI being Function of REAL,REAL such that A1: for r being Real holds PI . r = H1(r) from FUNCT_2:sch_4(); A2: [.0,1.] = the carrier of (Closed-Interval-TSpace (0,1)) by TOPMETR:18; now__::_thesis:_for_y_being_set_st_y_in_rng_(PI_|_[.a,b.])_holds_ y_in_[.0,1.] let y be set ; ::_thesis: ( y in rng (PI | [.a,b.]) implies y in [.0,1.] ) assume A3: y in rng (PI | [.a,b.]) ; ::_thesis: y in [.0,1.] then reconsider d = y as Real ; y in PI .: [.a,b.] by A3, RELAT_1:115; then consider x being set such that x in dom PI and A4: x in [.a,b.] and A5: y = PI . x by FUNCT_1:def_6; reconsider c = x as Real by A4; A6: d = (((b - c) * r1) + ((c - a) * r2)) / (b - a) by A1, A5; r1 in [.0,1.] by A2; then r1 in { p where p is Real : ( 0 <= p & p <= 1 ) } by RCOMP_1:def_1; then A7: ex v1 being Real st ( v1 = r1 & 0 <= v1 & v1 <= 1 ) ; c in { p where p is Real : ( a <= p & p <= b ) } by A4, RCOMP_1:def_1; then A8: ex u being Real st ( u = c & a <= u & u <= b ) ; then A9: 0 <= c - a by XREAL_1:48; r2 in [.0,1.] by A2; then r2 in { p where p is Real : ( 0 <= p & p <= 1 ) } by RCOMP_1:def_1; then A10: ex v2 being Real st ( v2 = r2 & 0 <= v2 & v2 <= 1 ) ; then A11: (c - a) * r2 <= c - a by A9, XREAL_1:153; A12: 0 < b - a by B1, XREAL_1:50; A13: 0 <= b - c by A8, XREAL_1:48; then (b - c) * r1 <= b - c by A7, XREAL_1:153; then ((b - c) * r1) + ((c - a) * r2) <= (b + (- c)) + (c - a) by A11, XREAL_1:7; then d <= (b - a) / (b - a) by A12, A6, XREAL_1:72; then d <= 1 by A12, XCMPLX_1:60; then y in { q where q is Real : ( 0 <= q & q <= 1 ) } by A7, A10, A12, A6, A13, A9; hence y in [.0,1.] by RCOMP_1:def_1; ::_thesis: verum end; then A14: rng (PI | [.a,b.]) c= the carrier of (Closed-Interval-TSpace (0,1)) by A2, TARSKI:def_3; A15: 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 B1, A15, TOPMETR:18; then reconsider F = PI | [.a,b.] as Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (0,1)) by A14, FUNCT_2:def_1, RELSET_1:4; take F ; ::_thesis: for s being Point of (Closed-Interval-TSpace (a,b)) holds F . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) let s be Point of (Closed-Interval-TSpace (a,b)); ::_thesis: F . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) A16: s is Real by XREAL_0:def_1; the carrier of (Closed-Interval-TSpace (a,b)) = [.a,b.] by B1, TOPMETR:18; hence F . s = PI . s by FUNCT_1:49 .= (((b - s) * t1) + ((s - a) * t2)) / (b - a) by A1, A16 ; ::_thesis: verum end; uniqueness for b1, b2 being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (0,1)) st ( for s being Point of (Closed-Interval-TSpace (a,b)) holds b1 . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) ) & ( for s being Point of (Closed-Interval-TSpace (a,b)) holds b2 . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) ) holds b1 = b2 proof let F1, F2 be Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (0,1)); ::_thesis: ( ( for s being Point of (Closed-Interval-TSpace (a,b)) holds F1 . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) ) & ( for s being Point of (Closed-Interval-TSpace (a,b)) holds F2 . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) ) implies F1 = F2 ) assume A17: for s being Point of (Closed-Interval-TSpace (a,b)) holds F1 . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) ; ::_thesis: ( ex s being Point of (Closed-Interval-TSpace (a,b)) st not F2 . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) or F1 = F2 ) assume A18: for s being Point of (Closed-Interval-TSpace (a,b)) holds F2 . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) ; ::_thesis: F1 = F2 let s be Point of (Closed-Interval-TSpace (a,b)); :: according to FUNCT_2:def_8 ::_thesis: F1 . s = F2 . s reconsider r = s as Real by B1, Lm2; reconsider r1 = t1, r2 = t2 as Real by Lm2; thus F1 . s = (((b - r) * r1) + ((r - a) * r2)) / (b - a) by A17 .= F2 . s by A18 ; ::_thesis: verum end; end; :: deftheorem Def4 defines P[01] TREAL_1:def_4_:_ for a, b being real number st a < b holds for t1, t2 being Point of (Closed-Interval-TSpace (0,1)) for b5 being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (0,1)) holds ( b5 = P[01] (a,b,t1,t2) iff for s being Point of (Closed-Interval-TSpace (a,b)) holds b5 . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) ); theorem Th11: :: TREAL_1:11 for a, b being real number st a < b holds 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 let a, b be real number ; ::_thesis: ( 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)) ) assume A1: a < b ; ::_thesis: 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)) let t1, t2 be Point of (Closed-Interval-TSpace (0,1)); ::_thesis: 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)) let s be Point of (Closed-Interval-TSpace (a,b)); ::_thesis: (P[01] (a,b,t1,t2)) . s = (((t2 - t1) / (b - a)) * s) + (((b * t1) - (a * t2)) / (b - a)) 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 ; ::_thesis: verum end; theorem Th12: :: TREAL_1:12 for a, b being real number st a < b holds for t1, t2 being Point of (Closed-Interval-TSpace (0,1)) holds P[01] (a,b,t1,t2) is continuous proof let a, b be real number ; ::_thesis: ( a < b implies for t1, t2 being Point of (Closed-Interval-TSpace (0,1)) holds P[01] (a,b,t1,t2) is continuous ) assume A1: a < b ; ::_thesis: for t1, t2 being Point of (Closed-Interval-TSpace (0,1)) holds P[01] (a,b,t1,t2) is continuous reconsider a = a, b = b as Real by XREAL_0:def_1; 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)); ::_thesis: P[01] (a,b,t1,t2) is continuous reconsider r1 = t1, r2 = t2 as Real by Lm2; deffunc H1( Element of REAL ) -> Element of REAL = (((r2 - r1) / (b - a)) * $1) + (((b * r1) - (a * r2)) / (b - a)); consider P being Function of REAL,REAL such that A3: for r being Real holds P . r = H1(r) from FUNCT_2:sch_4(); reconsider f = P as Function of R^1,R^1 by TOPMETR:17; A4: for s being Point of (Closed-Interval-TSpace (a,b)) for 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)); ::_thesis: for w being Point of R^1 st s = w holds (P[01] (a,b,t1,t2)) . s = f . w let w be Point of R^1; ::_thesis: ( s = w implies (P[01] (a,b,t1,t2)) . s = f . w ) reconsider r = s as Real by A1, Lm2; assume A5: s = w ; ::_thesis: (P[01] (a,b,t1,t2)) . s = f . w thus (P[01] (a,b,t1,t2)) . s = (((r2 - r1) / (b - a)) * r) + (((b * r1) - (a * r2)) / (b - a)) by A1, Th11 .= f . w by A3, A5 ; ::_thesis: verum end; A6: f is continuous by A3, 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)); ::_thesis: P[01] (a,b,t1,t2) is_continuous_at s 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 holds 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)); ::_thesis: ( G is open & (P[01] (a,b,t1,t2)) . s in G implies 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 ) ) assume G is open ; ::_thesis: ( not (P[01] (a,b,t1,t2)) . s in G or 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 ) ) then consider G0 being Subset of R^1 such that A7: G0 is open and A8: G0 /\ ([#] (Closed-Interval-TSpace (0,1))) = G by TOPS_2:24; A9: f is_continuous_at w by A6, TMAP_1:44; assume (P[01] (a,b,t1,t2)) . s in G ; ::_thesis: 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 ) then f . w in G by A4; then f . w in G0 by A8, XBOOLE_0:def_4; then consider H0 being Subset of R^1 such that A10: H0 is open and A11: w in H0 and A12: f .: H0 c= G0 by A7, A9, TMAP_1:43; now__::_thesis:_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_) reconsider H = H0 /\ ([#] (Closed-Interval-TSpace (a,b))) as Subset of (Closed-Interval-TSpace (a,b)) ; take H = H; ::_thesis: ( H is open & s in H & (P[01] (a,b,t1,t2)) .: H c= G ) thus H is open by A10, TOPS_2:24; ::_thesis: ( s in H & (P[01] (a,b,t1,t2)) .: H c= G ) thus s in H by A11, XBOOLE_0:def_4; ::_thesis: (P[01] (a,b,t1,t2)) .: H c= G thus (P[01] (a,b,t1,t2)) .: H c= G ::_thesis: verum proof let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in (P[01] (a,b,t1,t2)) .: H or t in G ) assume t in (P[01] (a,b,t1,t2)) .: H ; ::_thesis: t in G then consider r being set such that r in dom (P[01] (a,b,t1,t2)) and A13: r in H and A14: t = (P[01] (a,b,t1,t2)) . r by FUNCT_1:def_6; A15: r in the carrier of (Closed-Interval-TSpace (a,b)) by A13; reconsider r = r as Point of (Closed-Interval-TSpace (a,b)) by A13; r in dom (P[01] (a,b,t1,t2)) by A15, FUNCT_2:def_1; then A16: t in (P[01] (a,b,t1,t2)) .: the carrier of (Closed-Interval-TSpace (a,b)) by A14, FUNCT_1:def_6; reconsider p = r as Point of R^1 by A2, TARSKI:def_3, TOPMETR:17; p in [#] R^1 ; then A17: p in dom f by FUNCT_2:def_1; ( t = f . p & p in H0 ) by A4, A13, A14, XBOOLE_0:def_4; then t in f .: H0 by A17, FUNCT_1:def_6; hence t in G by A8, A12, A16, XBOOLE_0:def_4; ::_thesis: verum end; end; hence 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 ) ; ::_thesis: verum end; hence P[01] (a,b,t1,t2) is_continuous_at s by TMAP_1:43; ::_thesis: verum end; hence P[01] (a,b,t1,t2) is continuous by TMAP_1:44; ::_thesis: verum end; theorem :: TREAL_1:13 for a, b being real number st a < b holds 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 let a, b be real number ; ::_thesis: ( 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 ) ) assume A1: a < b ; ::_thesis: 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 ) then A2: b - a <> 0 ; let t1, t2 be Point of (Closed-Interval-TSpace (0,1)); ::_thesis: ( (P[01] (a,b,t1,t2)) . ((#) (a,b)) = t1 & (P[01] (a,b,t1,t2)) . ((a,b) (#)) = t2 ) reconsider r1 = t1, r2 = t2 as Real by Lm2; 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 ; ::_thesis: (P[01] (a,b,t1,t2)) . ((a,b) (#)) = t2 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 ; ::_thesis: verum end; theorem :: TREAL_1:14 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)); ::_thesis: (P[01] (0,1,((#) (0,1)),((0,1) (#)))) . x = x reconsider y = x as Real by Lm2; ( (#) (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 ; ::_thesis: verum end; hence P[01] (0,1,((#) (0,1)),((0,1) (#))) = id (Closed-Interval-TSpace (0,1)) by FUNCT_2:124; ::_thesis: verum end; theorem Th15: :: TREAL_1:15 for a, b being real number st a < b holds ( 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 let a, b be real number ; ::_thesis: ( 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) (#)))) ) ) A1: ( 0 = (#) (0,1) & 1 = (0,1) (#) ) by Def1, Def2; set L = L[01] (((#) (a,b)),((a,b) (#))); set P = P[01] (a,b,((#) (0,1)),((0,1) (#))); assume A2: a < b ; ::_thesis: ( 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) (#)))) ) 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[01] (((#) (a,b)),((a,b) (#)))) * (P[01] (a,b,((#) (0,1)),((0,1) (#))))) . c = c proof let c be Point of (Closed-Interval-TSpace (a,b)); ::_thesis: ((L[01] (((#) (a,b)),((a,b) (#)))) * (P[01] (a,b,((#) (0,1)),((0,1) (#))))) . c = c reconsider r = c as Real by A2, Lm2; A5: (P[01] (a,b,((#) (0,1)),((0,1) (#)))) . c = (((b - r) * 0) + ((r - a) * 1)) / (b - a) by A2, A1, Def4 .= (r - a) / (b - a) ; thus ((L[01] (((#) (a,b)),((a,b) (#)))) * (P[01] (a,b,((#) (0,1)),((0,1) (#))))) . c = (L[01] (((#) (a,b)),((a,b) (#)))) . ((P[01] (a,b,((#) (0,1)),((0,1) (#)))) . 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 ; ::_thesis: verum end; hence id (Closed-Interval-TSpace (a,b)) = (L[01] (((#) (a,b)),((a,b) (#)))) * (P[01] (a,b,((#) (0,1)),((0,1) (#)))) by FUNCT_2:124; ::_thesis: id (Closed-Interval-TSpace (0,1)) = (P[01] (a,b,((#) (0,1)),((0,1) (#)))) * (L[01] (((#) (a,b)),((a,b) (#)))) for c being Point of (Closed-Interval-TSpace (0,1)) holds ((P[01] (a,b,((#) (0,1)),((0,1) (#)))) * (L[01] (((#) (a,b)),((a,b) (#))))) . c = c proof let c be Point of (Closed-Interval-TSpace (0,1)); ::_thesis: ((P[01] (a,b,((#) (0,1)),((0,1) (#)))) * (L[01] (((#) (a,b)),((a,b) (#))))) . c = c reconsider r = c as Real by Lm2; A6: (L[01] (((#) (a,b)),((a,b) (#)))) . c = ((1 - r) * a) + (r * b) by A2, A4, Def3 .= (r * (b - a)) + a ; thus ((P[01] (a,b,((#) (0,1)),((0,1) (#)))) * (L[01] (((#) (a,b)),((a,b) (#))))) . c = (P[01] (a,b,((#) (0,1)),((0,1) (#)))) . ((L[01] (((#) (a,b)),((a,b) (#)))) . 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 ; ::_thesis: verum end; hence id (Closed-Interval-TSpace (0,1)) = (P[01] (a,b,((#) (0,1)),((0,1) (#)))) * (L[01] (((#) (a,b)),((a,b) (#)))) by FUNCT_2:124; ::_thesis: verum end; theorem Th16: :: TREAL_1:16 for a, b being real number st a < b holds ( 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 let a, b be real number ; ::_thesis: ( 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)))) ) ) A1: ( 0 = (#) (0,1) & 1 = (0,1) (#) ) by Def1, Def2; set L = L[01] (((a,b) (#)),((#) (a,b))); set P = P[01] (a,b,((0,1) (#)),((#) (0,1))); assume A2: a < b ; ::_thesis: ( 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)))) ) 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[01] (((a,b) (#)),((#) (a,b)))) * (P[01] (a,b,((0,1) (#)),((#) (0,1))))) . c = c proof let c be Point of (Closed-Interval-TSpace (a,b)); ::_thesis: ((L[01] (((a,b) (#)),((#) (a,b)))) * (P[01] (a,b,((0,1) (#)),((#) (0,1))))) . c = c reconsider r = c as Real by A2, Lm2; A5: (P[01] (a,b,((0,1) (#)),((#) (0,1)))) . c = (((b - r) * 1) + ((r - a) * 0)) / (b - a) by A2, A1, Def4 .= (b - r) / (b - a) ; thus ((L[01] (((a,b) (#)),((#) (a,b)))) * (P[01] (a,b,((0,1) (#)),((#) (0,1))))) . c = (L[01] (((a,b) (#)),((#) (a,b)))) . ((P[01] (a,b,((0,1) (#)),((#) (0,1)))) . 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 ; ::_thesis: verum end; hence id (Closed-Interval-TSpace (a,b)) = (L[01] (((a,b) (#)),((#) (a,b)))) * (P[01] (a,b,((0,1) (#)),((#) (0,1)))) by FUNCT_2:124; ::_thesis: id (Closed-Interval-TSpace (0,1)) = (P[01] (a,b,((0,1) (#)),((#) (0,1)))) * (L[01] (((a,b) (#)),((#) (a,b)))) for c being Point of (Closed-Interval-TSpace (0,1)) holds ((P[01] (a,b,((0,1) (#)),((#) (0,1)))) * (L[01] (((a,b) (#)),((#) (a,b))))) . c = c proof let c be Point of (Closed-Interval-TSpace (0,1)); ::_thesis: ((P[01] (a,b,((0,1) (#)),((#) (0,1)))) * (L[01] (((a,b) (#)),((#) (a,b))))) . c = c reconsider r = c as Real by Lm2; A6: (L[01] (((a,b) (#)),((#) (a,b)))) . c = ((1 - r) * b) + (r * a) by A2, A4, Def3 .= (r * (a - b)) + b ; thus ((P[01] (a,b,((0,1) (#)),((#) (0,1)))) * (L[01] (((a,b) (#)),((#) (a,b))))) . c = (P[01] (a,b,((0,1) (#)),((#) (0,1)))) . ((L[01] (((a,b) (#)),((#) (a,b)))) . 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 ; ::_thesis: verum end; hence id (Closed-Interval-TSpace (0,1)) = (P[01] (a,b,((0,1) (#)),((#) (0,1)))) * (L[01] (((a,b) (#)),((#) (a,b)))) by FUNCT_2:124; ::_thesis: verum end; theorem Th17: :: TREAL_1:17 for a, b being real number st a < b holds ( 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 let a, b be real number ; ::_thesis: ( 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) (#))) ) ) set L = L[01] (((#) (a,b)),((a,b) (#))); set P = P[01] (a,b,((#) (0,1)),((0,1) (#))); assume A1: a < b ; ::_thesis: ( 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) (#))) ) then A2: id the carrier of (Closed-Interval-TSpace (0,1)) = (P[01] (a,b,((#) (0,1)),((0,1) (#)))) * (L[01] (((#) (a,b)),((a,b) (#)))) by Th15; then A3: L[01] (((#) (a,b)),((a,b) (#))) is one-to-one by FUNCT_2:23; A4: ( L[01] (((#) (a,b)),((a,b) (#))) is continuous & P[01] (a,b,((#) (0,1)),((0,1) (#))) 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[01] (((#) (a,b)),((a,b) (#)))) * (P[01] (a,b,((#) (0,1)),((0,1) (#)))) by A1, Th15 ; then A6: L[01] (((#) (a,b)),((a,b) (#))) is onto by FUNCT_2:23; then A7: rng (L[01] (((#) (a,b)),((a,b) (#)))) = [#] (Closed-Interval-TSpace (a,b)) by FUNCT_2:def_3; A8: (L[01] (((#) (a,b)),((a,b) (#)))) " = (L[01] (((#) (a,b)),((a,b) (#)))) " by A3, A6, TOPS_2:def_4; ( dom (L[01] (((#) (a,b)),((a,b) (#)))) = [#] (Closed-Interval-TSpace (0,1)) & P[01] (a,b,((#) (0,1)),((0,1) (#))) = (L[01] (((#) (a,b)),((a,b) (#)))) " ) by A2, A3, A7, FUNCT_2:30, FUNCT_2:def_1; hence L[01] (((#) (a,b)),((a,b) (#))) is being_homeomorphism by A3, A7, A8, A4, TOPS_2:def_5; ::_thesis: ( (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) (#))) ) thus (L[01] (((#) (a,b)),((a,b) (#)))) " = P[01] (a,b,((#) (0,1)),((0,1) (#))) by A2, A3, A7, A8, FUNCT_2:30; ::_thesis: ( 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) (#))) ) A9: P[01] (a,b,((#) (0,1)),((0,1) (#))) is onto by A2, FUNCT_2:23; then A10: rng (P[01] (a,b,((#) (0,1)),((0,1) (#)))) = [#] (Closed-Interval-TSpace (0,1)) by FUNCT_2:def_3; A11: ( L[01] (((#) (a,b)),((a,b) (#))) is continuous Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (a,b)) & P[01] (a,b,((#) (0,1)),((0,1) (#))) is continuous ) by A1, Th8, Th12; A12: P[01] (a,b,((#) (0,1)),((0,1) (#))) is one-to-one by A5, FUNCT_2:23; A13: (P[01] (a,b,((#) (0,1)),((0,1) (#)))) " = (P[01] (a,b,((#) (0,1)),((0,1) (#)))) " by A12, A9, TOPS_2:def_4; ( dom (P[01] (a,b,((#) (0,1)),((0,1) (#)))) = [#] (Closed-Interval-TSpace (a,b)) & L[01] (((#) (a,b)),((a,b) (#))) = (P[01] (a,b,((#) (0,1)),((0,1) (#)))) " ) by A10, A5, A12, FUNCT_2:30, FUNCT_2:def_1; hence P[01] (a,b,((#) (0,1)),((0,1) (#))) is being_homeomorphism by A10, A12, A13, A11, TOPS_2:def_5; ::_thesis: (P[01] (a,b,((#) (0,1)),((0,1) (#)))) " = L[01] (((#) (a,b)),((a,b) (#))) thus (P[01] (a,b,((#) (0,1)),((0,1) (#)))) " = L[01] (((#) (a,b)),((a,b) (#))) by A10, A5, A12, A13, FUNCT_2:30; ::_thesis: verum end; theorem :: TREAL_1:18 for a, b being real number st a < b holds ( 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 let a, b be real number ; ::_thesis: ( 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))) ) ) set L = L[01] (((a,b) (#)),((#) (a,b))); set P = P[01] (a,b,((0,1) (#)),((#) (0,1))); assume A1: a < b ; ::_thesis: ( 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))) ) then A2: id the carrier of (Closed-Interval-TSpace (0,1)) = (P[01] (a,b,((0,1) (#)),((#) (0,1)))) * (L[01] (((a,b) (#)),((#) (a,b)))) by Th16; then A3: L[01] (((a,b) (#)),((#) (a,b))) is one-to-one by FUNCT_2:23; A4: ( L[01] (((a,b) (#)),((#) (a,b))) is continuous & P[01] (a,b,((0,1) (#)),((#) (0,1))) 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[01] (((a,b) (#)),((#) (a,b)))) * (P[01] (a,b,((0,1) (#)),((#) (0,1)))) by A1, Th16 ; then A6: L[01] (((a,b) (#)),((#) (a,b))) is onto by FUNCT_2:23; then A7: rng (L[01] (((a,b) (#)),((#) (a,b)))) = [#] (Closed-Interval-TSpace (a,b)) by FUNCT_2:def_3; A8: (L[01] (((a,b) (#)),((#) (a,b)))) " = (L[01] (((a,b) (#)),((#) (a,b)))) " by A3, A6, TOPS_2:def_4; ( dom (L[01] (((a,b) (#)),((#) (a,b)))) = [#] (Closed-Interval-TSpace (0,1)) & P[01] (a,b,((0,1) (#)),((#) (0,1))) = (L[01] (((a,b) (#)),((#) (a,b)))) " ) by A2, A3, A7, FUNCT_2:30, FUNCT_2:def_1; hence L[01] (((a,b) (#)),((#) (a,b))) is being_homeomorphism by A3, A7, A8, A4, TOPS_2:def_5; ::_thesis: ( (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))) ) thus (L[01] (((a,b) (#)),((#) (a,b)))) " = P[01] (a,b,((0,1) (#)),((#) (0,1))) by A2, A3, A7, A8, FUNCT_2:30; ::_thesis: ( 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))) ) A9: P[01] (a,b,((0,1) (#)),((#) (0,1))) is onto by A2, FUNCT_2:23; then A10: rng (P[01] (a,b,((0,1) (#)),((#) (0,1)))) = [#] (Closed-Interval-TSpace (0,1)) by FUNCT_2:def_3; A11: ( L[01] (((a,b) (#)),((#) (a,b))) is continuous Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (a,b)) & P[01] (a,b,((0,1) (#)),((#) (0,1))) is continuous ) by A1, Th8, Th12; A12: P[01] (a,b,((0,1) (#)),((#) (0,1))) is one-to-one by A5, FUNCT_2:23; A13: (P[01] (a,b,((0,1) (#)),((#) (0,1)))) " = (P[01] (a,b,((0,1) (#)),((#) (0,1)))) " by A12, A9, TOPS_2:def_4; ( dom (P[01] (a,b,((0,1) (#)),((#) (0,1)))) = [#] (Closed-Interval-TSpace (a,b)) & L[01] (((a,b) (#)),((#) (a,b))) = (P[01] (a,b,((0,1) (#)),((#) (0,1)))) " ) by A10, A5, A12, FUNCT_2:30, FUNCT_2:def_1; hence P[01] (a,b,((0,1) (#)),((#) (0,1))) is being_homeomorphism by A10, A12, A13, A11, TOPS_2:def_5; ::_thesis: (P[01] (a,b,((0,1) (#)),((#) (0,1)))) " = L[01] (((a,b) (#)),((#) (a,b))) thus (P[01] (a,b,((0,1) (#)),((#) (0,1)))) " = L[01] (((a,b) (#)),((#) (a,b))) by A10, A5, A12, A13, FUNCT_2:30; ::_thesis: verum end; begin theorem Th19: :: TREAL_1:19 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]; ::_thesis: ( [#] I[01] = A \/ B & A <> {} I[01] & B <> {} I[01] & A is closed & B is closed implies A meets B ) 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 ; ::_thesis: A meets B reconsider P = A, Q = B as Subset of REAL by BORSUK_1:40, XBOOLE_1:1; assume A6: A misses B ; ::_thesis: contradiction set x = the Element of P; reconsider x = the Element of P as Real by A2, TARSKI:def_3; A7: now__::_thesis:_ex_x_being_Real_st_x_in_P take x = x; ::_thesis: x in P thus x in P by A2; ::_thesis: verum end; set x = the Element of Q; reconsider x = the Element of Q as Real by A3, TARSKI:def_3; A8: now__::_thesis:_ex_x_being_Real_st_x_in_Q take x = x; ::_thesis: x in Q thus x in Q by A3; ::_thesis: verum end; A9: the carrier of RealSpace = the carrier of (TopSpaceMetr RealSpace) by TOPMETR:12; 0 is LowerBound of P proof let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in P or 0 <= r ) assume r in P ; ::_thesis: 0 <= r 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 ; ::_thesis: verum end; then A10: P is bounded_below by XXREAL_2:def_9; 0 is LowerBound of Q proof let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in Q or 0 <= r ) assume r in Q ; ::_thesis: 0 <= r 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 ; ::_thesis: verum end; then A11: Q is bounded_below by XXREAL_2:def_9; reconsider A0 = P, B0 = Q as Subset of R^1 by METRIC_1:def_13, TOPMETR:12, TOPMETR: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__::_thesis:_contradiction percases ( 0 in P or 0 in Q ) by A1, A15, BORSUK_1:40, XBOOLE_0:def_3; supposeA16: 0 in P ; ::_thesis: contradiction reconsider B00 = B0 ` as Subset of R^1 ; set l = lower_bound Q; reconsider m = lower_bound Q as Point of RealSpace by METRIC_1:def_13; reconsider t = m as Point of R^1 by TOPMETR:12, TOPMETR:def_6; set W = { w where w is Real : ( 0 <= w & w < lower_bound Q ) } ; A17: lower_bound Q in Q proof assume not lower_bound Q in Q ; ::_thesis: contradiction then A18: t in B00 by SUBSET_1:29; B00 is open by A14, TOPS_1:3; then consider s being real number such that A19: s > 0 and A20: Ball (m,s) c= B0 ` by A18, TOPMETR:15, TOPMETR:def_6; consider r being real number such that A21: r in Q and A22: r < (lower_bound Q) + s by A8, A11, A19, SEQ_4:def_2; reconsider r = r as Real by XREAL_0:def_1; lower_bound Q <= r by A11, A21, SEQ_4:def_2; then (lower_bound Q) - r <= 0 by XREAL_1:47; then A23: - s < - ((lower_bound Q) - r) by A19, XREAL_1:24; reconsider rm = r as Point of RealSpace by METRIC_1:def_13; r - (lower_bound Q) < s by A22, XREAL_1:19; then abs (r - (lower_bound Q)) < s by A23, SEQ_2:1; then the distance of RealSpace . (rm,m) < s by METRIC_1:def_12, METRIC_1: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) < s } ; then rm in Ball (m,s) by METRIC_1:17; hence contradiction by A20, A21, XBOOLE_0:def_5; ::_thesis: verum end; then lower_bound Q in [.0,1.] by BORSUK_1:40; then lower_bound Q in { u where u is Real : ( 0 <= u & u <= 1 ) } by RCOMP_1:def_1; then A24: ex u0 being Real st ( u0 = lower_bound Q & 0 <= u0 & u0 <= 1 ) ; now__::_thesis:_for_x_being_set_st_x_in__{__w_where_w_is_Real_:_(_0_<=_w_&_w_<_lower_bound_Q_)__}__holds_ x_in_P let x be set ; ::_thesis: ( x in { w where w is Real : ( 0 <= w & w < lower_bound Q ) } implies x in P ) assume x in { w where w is Real : ( 0 <= w & w < lower_bound Q ) } ; ::_thesis: x in P then consider w0 being Real such that A25: w0 = x and A26: 0 <= w0 and A27: w0 < lower_bound Q ; w0 <= 1 by A24, A27, XXREAL_0:2; then w0 in { u where u is Real : ( 0 <= u & u <= 1 ) } by A26; then w0 in P \/ Q by A1, BORSUK_1:40, RCOMP_1:def_1; then ( w0 in P or w0 in Q ) by XBOOLE_0:def_3; hence x in P by A11, A25, A27, SEQ_4:def_2; ::_thesis: verum end; then A28: { w where w is Real : ( 0 <= w & w < lower_bound Q ) } c= P by TARSKI:def_3; then reconsider D = { w where w is Real : ( 0 <= w & w < lower_bound Q ) } as Subset of R^1 by A9, METRIC_1:def_13, TOPMETR:def_6, XBOOLE_1:1; A29: not 0 in Q by A6, A16, XBOOLE_0:3; now__::_thesis:_for_G_being_Subset_of_R^1_st_G_is_open_&_t_in_G_holds_ D_meets_G let G be Subset of R^1; ::_thesis: ( G is open & t in G implies D meets G ) assume A30: G is open ; ::_thesis: ( t in G implies D meets G ) assume t in G ; ::_thesis: D meets G then consider e being real number such that A31: e > 0 and A32: Ball (m,e) c= G by A30, TOPMETR:15, TOPMETR:def_6; reconsider e = e as Element of REAL by XREAL_0:def_1; set e0 = max (0,((lower_bound Q) - (e / 2))); reconsider e1 = max (0,((lower_bound Q) - (e / 2))) as Point of RealSpace by METRIC_1:def_13; A33: e * (1 / 2) < e * 1 by A31, XREAL_1:68; now__::_thesis:_abs_((lower_bound_Q)_-_(max_(0,((lower_bound_Q)_-_(e_/_2)))))_<_e percases ( max (0,((lower_bound Q) - (e / 2))) = 0 or max (0,((lower_bound Q) - (e / 2))) = (lower_bound Q) - (e / 2) ) by XXREAL_0:16; supposeA34: max (0,((lower_bound Q) - (e / 2))) = 0 ; ::_thesis: abs ((lower_bound Q) - (max (0,((lower_bound Q) - (e / 2))))) < e then lower_bound Q <= e / 2 by XREAL_1:50, XXREAL_0:25; then lower_bound Q < e by A33, XXREAL_0:2; hence abs ((lower_bound Q) - (max (0,((lower_bound Q) - (e / 2))))) < e by A24, A34, ABSVALUE:def_1; ::_thesis: verum end; suppose max (0,((lower_bound Q) - (e / 2))) = (lower_bound Q) - (e / 2) ; ::_thesis: abs ((lower_bound Q) - (max (0,((lower_bound Q) - (e / 2))))) < e hence abs ((lower_bound Q) - (max (0,((lower_bound Q) - (e / 2))))) < e by A31, A33, ABSVALUE:def_1; ::_thesis: verum end; end; end; then the distance of RealSpace . (m,e1) < e by METRIC_1:def_12, METRIC_1: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) < e } ; then A35: e1 in Ball (m,e) by METRIC_1:17; ( max (0,((lower_bound Q) - (e / 2))) = 0 or max (0,((lower_bound Q) - (e / 2))) = (lower_bound Q) - (e / 2) ) by XXREAL_0:16; then ( 0 <= max (0,((lower_bound Q) - (e / 2))) & max (0,((lower_bound Q) - (e / 2))) < lower_bound Q ) by A29, A17, A24, A31, XREAL_1:44, XREAL_1:139, XXREAL_0:25; then max (0,((lower_bound Q) - (e / 2))) in { w where w is Real : ( 0 <= w & w < lower_bound Q ) } ; hence D meets G by A32, A35, XBOOLE_0:3; ::_thesis: verum end; then A36: t in Cl D by PRE_TOPC:24; A37: Cl A0 = A0 by A13, PRE_TOPC:22; Cl D c= Cl A0 by A28, PRE_TOPC:19; hence contradiction by A6, A17, A36, A37, XBOOLE_0:3; ::_thesis: verum end; supposeA38: 0 in Q ; ::_thesis: contradiction reconsider A00 = A0 ` as Subset of R^1 ; set l = lower_bound P; reconsider m = lower_bound P as Point of RealSpace by METRIC_1:def_13; reconsider t = m as Point of R^1 by TOPMETR:12, TOPMETR:def_6; set W = { w where w is Real : ( 0 <= w & w < lower_bound P ) } ; A39: lower_bound P in P proof assume not lower_bound P in P ; ::_thesis: contradiction then A40: t in A00 by SUBSET_1:29; A00 is open by A13, TOPS_1:3; then consider s being real number such that A41: s > 0 and A42: Ball (m,s) c= A0 ` by A40, TOPMETR:15, TOPMETR:def_6; consider r being real number such that A43: r in P and A44: r < (lower_bound P) + s by A7, A10, A41, SEQ_4:def_2; reconsider r = r as Real by XREAL_0:def_1; lower_bound P <= r by A10, A43, SEQ_4:def_2; then (lower_bound P) - r <= 0 by XREAL_1:47; then A45: - s < - ((lower_bound P) - r) by A41, XREAL_1:24; reconsider rm = r as Point of RealSpace by METRIC_1:def_13; r - (lower_bound P) < s by A44, XREAL_1:19; then abs (r - (lower_bound P)) < s by A45, SEQ_2:1; then real_dist . (r,(lower_bound P)) < s by METRIC_1:def_12; then dist (rm,m) < s by METRIC_1:def_1, METRIC_1:def_13; then rm in { q where q is Element of RealSpace : dist (m,q) < s } ; then rm in Ball (m,s) by METRIC_1:17; hence contradiction by A42, A43, XBOOLE_0:def_5; ::_thesis: verum end; then lower_bound P in [.0,1.] by BORSUK_1:40; then lower_bound P in { u where u is Real : ( 0 <= u & u <= 1 ) } by RCOMP_1:def_1; then A46: ex u0 being Real st ( u0 = lower_bound P & 0 <= u0 & u0 <= 1 ) ; now__::_thesis:_for_x_being_set_st_x_in__{__w_where_w_is_Real_:_(_0_<=_w_&_w_<_lower_bound_P_)__}__holds_ x_in_Q let x be set ; ::_thesis: ( x in { w where w is Real : ( 0 <= w & w < lower_bound P ) } implies x in Q ) assume x in { w where w is Real : ( 0 <= w & w < lower_bound P ) } ; ::_thesis: x in Q then consider w0 being Real such that A47: w0 = x and A48: 0 <= w0 and A49: w0 < lower_bound P ; w0 <= 1 by A46, A49, XXREAL_0:2; then w0 in { u where u is Real : ( 0 <= u & u <= 1 ) } by A48; then w0 in P \/ Q by A1, BORSUK_1:40, RCOMP_1:def_1; then ( w0 in P or w0 in Q ) by XBOOLE_0:def_3; hence x in Q by A10, A47, A49, SEQ_4:def_2; ::_thesis: verum end; then A50: { w where w is Real : ( 0 <= w & w < lower_bound P ) } c= Q by TARSKI:def_3; then reconsider D = { w where w is Real : ( 0 <= w & w < lower_bound P ) } as Subset of R^1 by A9, METRIC_1:def_13, TOPMETR:def_6, XBOOLE_1:1; A51: not 0 in P by A6, A38, XBOOLE_0:3; now__::_thesis:_for_G_being_Subset_of_R^1_st_G_is_open_&_t_in_G_holds_ D_meets_G let G be Subset of R^1; ::_thesis: ( G is open & t in G implies D meets G ) assume A52: G is open ; ::_thesis: ( t in G implies D meets G ) assume t in G ; ::_thesis: D meets G then consider e being real number such that A53: e > 0 and A54: Ball (m,e) c= G by A52, TOPMETR:15, TOPMETR:def_6; reconsider e = e as Real by XREAL_0:def_1; set e0 = max (0,((lower_bound P) - (e / 2))); reconsider e1 = max (0,((lower_bound P) - (e / 2))) as Point of RealSpace by METRIC_1:def_13; A55: e * (1 / 2) < e * 1 by A53, XREAL_1:68; now__::_thesis:_abs_((lower_bound_P)_-_(max_(0,((lower_bound_P)_-_(e_/_2)))))_<_e percases ( max (0,((lower_bound P) - (e / 2))) = 0 or max (0,((lower_bound P) - (e / 2))) = (lower_bound P) - (e / 2) ) by XXREAL_0:16; supposeA56: max (0,((lower_bound P) - (e / 2))) = 0 ; ::_thesis: abs ((lower_bound P) - (max (0,((lower_bound P) - (e / 2))))) < e then lower_bound P <= e / 2 by XREAL_1:50, XXREAL_0:25; then lower_bound P < e by A55, XXREAL_0:2; hence abs ((lower_bound P) - (max (0,((lower_bound P) - (e / 2))))) < e by A46, A56, ABSVALUE:def_1; ::_thesis: verum end; suppose max (0,((lower_bound P) - (e / 2))) = (lower_bound P) - (e / 2) ; ::_thesis: abs ((lower_bound P) - (max (0,((lower_bound P) - (e / 2))))) < e hence abs ((lower_bound P) - (max (0,((lower_bound P) - (e / 2))))) < e by A53, A55, ABSVALUE:def_1; ::_thesis: verum end; end; end; then real_dist . ((lower_bound P),(max (0,((lower_bound P) - (e / 2))))) < e by METRIC_1:def_12; then dist (m,e1) < e by METRIC_1:def_1, METRIC_1:def_13; then e1 in { z where z is Element of RealSpace : dist (m,z) < e } ; then A57: e1 in Ball (m,e) by METRIC_1:17; ( max (0,((lower_bound P) - (e / 2))) = 0 or max (0,((lower_bound P) - (e / 2))) = (lower_bound P) - (e / 2) ) by XXREAL_0:16; then ( 0 <= max (0,((lower_bound P) - (e / 2))) & max (0,((lower_bound P) - (e / 2))) < lower_bound P ) by A51, A39, A46, A53, XREAL_1:44, XREAL_1:139, XXREAL_0:25; then max (0,((lower_bound P) - (e / 2))) in { w where w is Real : ( 0 <= w & w < lower_bound P ) } ; hence D meets G by A54, A57, XBOOLE_0:3; ::_thesis: verum end; then A58: t in Cl D by PRE_TOPC:24; A59: Cl B0 = B0 by A14, PRE_TOPC:22; Cl D c= Cl B0 by A50, PRE_TOPC:19; hence contradiction by A6, A39, A58, A59, XBOOLE_0:3; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; hence I[01] is connected by CONNSP_1:10; ::_thesis: verum end; theorem :: TREAL_1:20 for a, b being real number st a <= b holds Closed-Interval-TSpace (a,b) is connected proof let a, b be real number ; ::_thesis: ( a <= b implies Closed-Interval-TSpace (a,b) is connected ) assume A1: a <= b ; ::_thesis: Closed-Interval-TSpace (a,b) is connected now__::_thesis:_Closed-Interval-TSpace_(a,b)_is_connected percases ( a < b or a = b ) by A1, XXREAL_0:1; suppose a < b ; ::_thesis: Closed-Interval-TSpace (a,b) is connected then L[01] (((#) (a,b)),((a,b) (#))) is being_homeomorphism by Th17; then A2: ( rng (L[01] (((#) (a,b)),((a,b) (#)))) = [#] (Closed-Interval-TSpace (a,b)) & L[01] (((#) (a,b)),((a,b) (#))) is continuous ) by TOPS_2:def_5; set A = the carrier of (Closed-Interval-TSpace (0,1)); ( the carrier of (Closed-Interval-TSpace (0,1)) = [#] (Closed-Interval-TSpace (0,1)) & (L[01] (((#) (a,b)),((a,b) (#)))) .: the carrier of (Closed-Interval-TSpace (0,1)) = rng (L[01] (((#) (a,b)),((a,b) (#)))) ) by RELSET_1:22; hence Closed-Interval-TSpace (a,b) is connected by A2, Th19, CONNSP_1:14, TOPMETR:20; ::_thesis: verum end; supposeA3: a = b ; ::_thesis: Closed-Interval-TSpace (a,b) is connected then ( [.a,b.] = {a} & a = (#) (a,b) ) by Def1, XXREAL_1:17; then [#] (Closed-Interval-TSpace (a,b)) = {((#) (a,b))} by A3, TOPMETR:18; hence Closed-Interval-TSpace (a,b) is connected by CONNSP_1:27; ::_thesis: verum end; end; end; hence Closed-Interval-TSpace (a,b) is connected ; ::_thesis: verum end; theorem Th21: :: TREAL_1:21 for f being continuous Function of I[01],I[01] ex x being Point of I[01] st f . x = x proof let f be continuous Function of I[01],I[01]; ::_thesis: ex x being Point of I[01] st f . x = x reconsider F = f as Function of [.0,1.],[.0,1.] by BORSUK_1:40; set A = { a where a is Real : ( a in [.0,1.] & F . a in [.0,a.] ) } ; set B = { b where b is Real : ( b in [.0,1.] & F . b in [.b,1.] ) } ; { a where a is Real : ( a in [.0,1.] & F . a in [.0,a.] ) } c= REAL proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { a where a is Real : ( a in [.0,1.] & F . a in [.0,a.] ) } or x in REAL ) assume x in { a where a is Real : ( a in [.0,1.] & F . a in [.0,a.] ) } ; ::_thesis: x in REAL then ex a being Real st ( a = x & a in [.0,1.] & F . a in [.0,a.] ) ; hence x in REAL ; ::_thesis: verum end; then reconsider A = { a where a is Real : ( a in [.0,1.] & F . a in [.0,a.] ) } as Subset of REAL ; A1: Closed-Interval-TSpace (0,1) = TopSpaceMetr (Closed-Interval-MSpace (0,1)) by TOPMETR:def_7; A2: A c= [.0,1.] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in [.0,1.] ) assume A3: x in A ; ::_thesis: x in [.0,1.] then reconsider x = x as Real ; ex a0 being Real st ( a0 = x & a0 in [.0,1.] & F . a0 in [.0,a0.] ) by A3; hence x in [.0,1.] ; ::_thesis: verum end; { b where b is Real : ( b in [.0,1.] & F . b in [.b,1.] ) } c= REAL proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { b where b is Real : ( b in [.0,1.] & F . b in [.b,1.] ) } or x in REAL ) assume x in { b where b is Real : ( b in [.0,1.] & F . b in [.b,1.] ) } ; ::_thesis: x in REAL then ex b being Real st ( b = x & b in [.0,1.] & F . b in [.b,1.] ) ; hence x in REAL ; ::_thesis: verum end; then reconsider B = { b where b is Real : ( b in [.0,1.] & F . b in [.b,1.] ) } as Subset of REAL ; A4: the carrier of (Closed-Interval-MSpace (0,1)) = [.0,1.] by TOPMETR:10; 0 in { w where w is Real : ( 0 <= w & w <= 1 ) } ; then A5: 0 in [.0,1.] by RCOMP_1:def_1; A6: [.0,1.] <> {} 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [.0,1.] or x in A \/ B ) assume A10: x in [.0,1.] ; ::_thesis: x in A \/ B 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__::_thesis:_y_in_A_\/_B percases ( F . y in [.0,y.] or F . y in [.y,1.] ) by A11, A12, XBOOLE_0:def_3; supposeA13: F . y in [.0,y.] ; ::_thesis: y in A \/ B A14: A c= A \/ B by XBOOLE_1:7; y in A by A10, A13; hence y in A \/ B by A14; ::_thesis: verum end; supposeA15: F . y in [.y,1.] ; ::_thesis: y in A \/ B A16: B c= A \/ B by XBOOLE_1:7; y in B by A10, A15; hence y in A \/ B by A16; ::_thesis: verum end; end; end; hence x in A \/ B ; ::_thesis: verum 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in [.0,1.] ) assume A19: x in B ; ::_thesis: x in [.0,1.] then reconsider x = x as Real ; ex b0 being Real st ( b0 = x & b0 in [.0,1.] & F . b0 in [.b0,1.] ) by A19; hence x in [.0,1.] ; ::_thesis: verum end; assume A20: for x being Point of I[01] holds f . x <> x ; ::_thesis: contradiction A21: A /\ B = {} proof set x = the Element of A /\ B; assume A22: A /\ B <> {} ; ::_thesis: contradiction then A23: the Element of A /\ B in A by XBOOLE_0:def_4; then A24: ex z being Real st ( z = the Element of A /\ B & z in [.0,1.] & F . z in [.0,z.] ) ; reconsider x = the Element of A /\ B as Real by A23; 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 A25: F . x in [.0,x.] /\ [.x,1.] by A24, XBOOLE_0:def_4; x in { q where q is Real : ( 0 <= q & q <= 1 ) } by A24, RCOMP_1:def_1; then ex u being Real st ( u = x & 0 <= u & u <= 1 ) ; then F . x in {x} by A25, XXREAL_1:418; then F . x = x by TARSKI:def_1; hence contradiction by A20, A24, BORSUK_1:40; ::_thesis: verum end; then A26: 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 A27: 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 ; ::_thesis: ex 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 ) take Q ; ::_thesis: ( [#] I[01] = P \/ Q & P <> {} I[01] & Q <> {} I[01] & P is closed & Q is closed & P misses Q ) thus A28: [#] I[01] = P \/ Q by A9, BORSUK_1:40, XBOOLE_0:def_10; ::_thesis: ( P <> {} I[01] & Q <> {} I[01] & P is closed & Q is closed & P misses Q ) thus ( P <> {} I[01] & Q <> {} I[01] ) by A27, A7; ::_thesis: ( P is closed & Q is closed & P misses Q ) thus P is closed ::_thesis: ( Q is closed & P misses Q ) proof set z = the Element of (Cl P) /\ Q; assume not P is closed ; ::_thesis: contradiction then A29: Cl P <> P by PRE_TOPC:22; A30: (Cl P) /\ Q <> {} proof assume (Cl P) /\ Q = {} ; ::_thesis: contradiction then Cl P misses Q by XBOOLE_0:def_7; then A31: Cl P c= Q ` by SUBSET_1:23; ( P c= Cl P & P = Q ` ) by A26, A28, PRE_TOPC:5, PRE_TOPC:18; hence contradiction by A29, A31, XBOOLE_0:def_10; ::_thesis: verum end; then A32: the Element of (Cl P) /\ Q in Cl P by XBOOLE_0:def_4; A33: the Element of (Cl P) /\ Q in Q by A30, XBOOLE_0:def_4; reconsider z = the Element of (Cl P) /\ Q as Point of I[01] by A32; reconsider t0 = z as Real by A33; A34: ex c being Real st ( c = t0 & c in [.0,1.] & F . c in [.c,1.] ) by A33; then reconsider s0 = F . t0 as Real ; t0 <= s0 by A34, XXREAL_1:1; then A35: 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,((s0 - t0) * (2 "))) as Subset of I[01] by BORSUK_1:40, TOPMETR:10; A36: ( W is open & f is_continuous_at z ) by A1, TMAP_1:50, TOPMETR:14, TOPMETR:20; A37: s0 - t0 <> 0 by A20; then A38: 0 / 2 < (s0 - t0) / 2 by A35, XREAL_1:74; then f . z in W by TBSP_1:11; then consider V being Subset of I[01] such that A39: ( V is open & z in V ) and A40: f .: V c= W by A36, TMAP_1:43; consider s being real number such that A41: s > 0 and A42: Ball (m,s) c= V by A1, A39, TOPMETR:15, TOPMETR:20; reconsider s = s as Real by XREAL_0:def_1; set r0 = min (s,((s0 - t0) * (2 "))); reconsider W0 = Ball (m,(min (s,((s0 - t0) * (2 "))))) as Subset of I[01] by BORSUK_1:40, TOPMETR:10; min (s,((s0 - t0) * (2 "))) > 0 by A38, A41, XXREAL_0:15; then A43: z in W0 by TBSP_1:11; set w = the Element of P /\ W0; W0 is open by A1, TOPMETR:14, TOPMETR:20; then P meets W0 by A32, A43, PRE_TOPC:24; then A44: P /\ W0 <> {} I[01] by XBOOLE_0:def_7; then A45: the Element of P /\ W0 in P by XBOOLE_0:def_4; A46: the Element of P /\ W0 in W0 by A44, XBOOLE_0:def_4; then reconsider w = the Element of P /\ W0 as Point of (Closed-Interval-MSpace (0,1)) ; reconsider w1 = w as Point of I[01] by A45; reconsider d = w1 as Real by A45; A47: d in A by A44, XBOOLE_0:def_4; Ball (m,(min (s,((s0 - t0) * (2 "))))) = { q where q is Element of (Closed-Interval-MSpace (0,1)) : dist (m,q) < min (s,((s0 - t0) * (2 "))) } by METRIC_1:17; then ( min (s,((s0 - t0) * (2 "))) <= (s0 - t0) * (2 ") & ex p being Element of (Closed-Interval-MSpace (0,1)) st ( p = w & dist (m,p) < min (s,((s0 - t0) * (2 "))) ) ) by A46, XXREAL_0:17; then dist (w,m) < (s0 - t0) * (2 ") by XXREAL_0:2; then A48: abs (d - t0) < (s0 - t0) * (2 ") by HEINE:1; d - t0 <= abs (d - t0) by ABSVALUE:4; then ( t0 + ((s0 - t0) * (2 ")) = s0 - ((s0 - t0) * (2 ")) & d - t0 < (s0 - t0) * (2 ") ) by A48, XXREAL_0:2; then A49: d < s0 - ((s0 - t0) * (2 ")) by XREAL_1:19; A50: (s0 - t0) * (2 ") < (s0 - t0) * 1 by A35, A37, XREAL_1:68; A51: Ball (n,((s0 - t0) * (2 "))) c= [.t0,1.] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Ball (n,((s0 - t0) * (2 "))) or x in [.t0,1.] ) assume A52: x in Ball (n,((s0 - t0) * (2 "))) ; ::_thesis: x in [.t0,1.] then reconsider u = x as Point of (Closed-Interval-MSpace (0,1)) ; x in [.0,1.] by A4, A52; then reconsider t = x as Real ; Ball (n,((s0 - t0) * (2 "))) = { q where q is Element of (Closed-Interval-MSpace (0,1)) : dist (n,q) < (s0 - t0) * (2 ") } by METRIC_1:17; then ex p being Element of (Closed-Interval-MSpace (0,1)) st ( p = u & dist (n,p) < (s0 - t0) * (2 ") ) by A52; then abs (s0 - t) < (s0 - t0) * (2 ") by HEINE:1; then A53: abs (s0 - t) < s0 - t0 by A50, XXREAL_0:2; s0 - t <= abs (s0 - t) by ABSVALUE:4; then s0 - t < s0 - t0 by A53, XXREAL_0:2; then A54: t0 <= t by XREAL_1:10; t <= 1 by A4, A52, XXREAL_1:1; then t in { q where q is Real : ( t0 <= q & q <= 1 ) } by A54; hence x in [.t0,1.] by RCOMP_1:def_1; ::_thesis: verum end; A55: Ball (n,((s0 - t0) * (2 "))) c= [.d,1.] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Ball (n,((s0 - t0) * (2 "))) or x in [.d,1.] ) assume A56: x in Ball (n,((s0 - t0) * (2 "))) ; ::_thesis: x in [.d,1.] then reconsider v = x as Point of (Closed-Interval-MSpace (0,1)) ; x in [.0,1.] by A4, A56; then reconsider t = x as Real ; Ball (n,((s0 - t0) * (2 "))) = { q where q is Element of (Closed-Interval-MSpace (0,1)) : dist (n,q) < (s0 - t0) * (2 ") } by METRIC_1:17; then ex p being Element of (Closed-Interval-MSpace (0,1)) st ( p = v & dist (n,p) < (s0 - t0) * (2 ") ) by A56; then A57: abs (s0 - t) < (s0 - t0) * (2 ") by HEINE:1; A58: now__::_thesis:_d_<_t percases ( t <= s0 or s0 < t ) ; suppose t <= s0 ; ::_thesis: d < t then 0 <= s0 - t by XREAL_1:48; then s0 - t < (s0 - t0) * (2 ") by A57, ABSVALUE:def_1; then s0 < ((s0 - t0) * (2 ")) + t by XREAL_1:19; then s0 - ((s0 - t0) * (2 ")) < t by XREAL_1:19; hence d < t by A49, XXREAL_0:2; ::_thesis: verum end; supposeA59: s0 < t ; ::_thesis: d < t s0 - ((s0 - t0) * (2 ")) < s0 by A38, XREAL_1:44; then d < s0 by A49, XXREAL_0:2; hence d < t by A59, XXREAL_0:2; ::_thesis: verum end; end; end; t <= 1 by A51, A56, XXREAL_1:1; then t in { w0 where w0 is Real : ( d <= w0 & w0 <= 1 ) } by A58; hence x in [.d,1.] by RCOMP_1:def_1; ::_thesis: verum end; Ball (m,(min (s,((s0 - t0) * (2 "))))) c= Ball (m,s) by PCOMPS_1:1, XXREAL_0:17; then W0 c= V by A42, XBOOLE_1:1; then f . w1 in f .: V by A46, FUNCT_2:35; then f . w1 in W by A40; then d in B by A55, BORSUK_1:40; hence contradiction by A26, A47, XBOOLE_0:3; ::_thesis: verum end; thus Q is closed ::_thesis: P misses Q proof set z = the Element of (Cl Q) /\ P; assume not Q is closed ; ::_thesis: contradiction then A60: Cl Q <> Q by PRE_TOPC:22; A61: (Cl Q) /\ P <> {} proof assume (Cl Q) /\ P = {} ; ::_thesis: contradiction then Cl Q misses P by XBOOLE_0:def_7; then A62: Cl Q c= P ` by SUBSET_1:23; ( Q c= Cl Q & Q = P ` ) by A26, A28, PRE_TOPC:5, PRE_TOPC:18; hence contradiction by A60, A62, XBOOLE_0:def_10; ::_thesis: verum end; then A63: the Element of (Cl Q) /\ P in Cl Q by XBOOLE_0:def_4; A64: the Element of (Cl Q) /\ P in P by A61, XBOOLE_0:def_4; reconsider z = the Element of (Cl Q) /\ P as Point of I[01] by A63; reconsider t0 = z as Real by A64; A65: ex c being Real st ( c = t0 & c in [.0,1.] & F . c in [.0,c.] ) by A64; then reconsider s0 = F . t0 as Real ; s0 <= t0 by A65, XXREAL_1:1; then A66: 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,((t0 - s0) * (2 "))) as Subset of I[01] by BORSUK_1:40, TOPMETR:10; A67: ( W is open & f is_continuous_at z ) by A1, TMAP_1:50, TOPMETR:14, TOPMETR:20; A68: t0 - s0 <> 0 by A20; then A69: 0 / 2 < (t0 - s0) / 2 by A66, XREAL_1:74; then f . z in W by TBSP_1:11; then consider V being Subset of I[01] such that A70: ( V is open & z in V ) and A71: f .: V c= W by A67, TMAP_1:43; consider s being real number such that A72: s > 0 and A73: Ball (m,s) c= V by A1, A70, TOPMETR:15, TOPMETR:20; reconsider s = s as Real by XREAL_0:def_1; set r0 = min (s,((t0 - s0) * (2 "))); reconsider W0 = Ball (m,(min (s,((t0 - s0) * (2 "))))) as Subset of I[01] by BORSUK_1:40, TOPMETR:10; min (s,((t0 - s0) * (2 "))) > 0 by A69, A72, XXREAL_0:15; then A74: z in W0 by TBSP_1:11; set w = the Element of Q /\ W0; W0 is open by A1, TOPMETR:14, TOPMETR:20; then Q meets W0 by A63, A74, PRE_TOPC:24; then A75: Q /\ W0 <> {} I[01] by XBOOLE_0:def_7; then A76: the Element of Q /\ W0 in Q by XBOOLE_0:def_4; A77: the Element of Q /\ W0 in W0 by A75, XBOOLE_0:def_4; then reconsider w = the Element of Q /\ W0 as Point of (Closed-Interval-MSpace (0,1)) ; reconsider w1 = w as Point of I[01] by A76; reconsider d = w1 as Real by A76; A78: d in B by A75, XBOOLE_0:def_4; Ball (m,(min (s,((t0 - s0) * (2 "))))) = { q where q is Element of (Closed-Interval-MSpace (0,1)) : dist (m,q) < min (s,((t0 - s0) * (2 "))) } by METRIC_1:17; then ( min (s,((t0 - s0) * (2 "))) <= (t0 - s0) * (2 ") & ex p being Element of (Closed-Interval-MSpace (0,1)) st ( p = w & dist (m,p) < min (s,((t0 - s0) * (2 "))) ) ) by A77, XXREAL_0:17; then dist (m,w) < (t0 - s0) * (2 ") by XXREAL_0:2; then A79: abs (t0 - d) < (t0 - s0) * (2 ") by HEINE:1; t0 - d <= abs (t0 - d) by ABSVALUE:4; then t0 + (- d) < (t0 - s0) * (2 ") by A79, XXREAL_0:2; then t0 < ((t0 - s0) * (2 ")) - (- d) by XREAL_1:20; then ( s0 + ((t0 - s0) * (2 ")) = t0 - ((t0 - s0) * (2 ")) & t0 < ((t0 - s0) * (2 ")) + (- (- d)) ) ; then A80: s0 + ((t0 - s0) * (2 ")) < d by XREAL_1:19; A81: (t0 - s0) * (2 ") < (t0 - s0) * 1 by A66, A68, XREAL_1:68; A82: Ball (n,((t0 - s0) * (2 "))) c= [.0,t0.] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Ball (n,((t0 - s0) * (2 "))) or x in [.0,t0.] ) assume A83: x in Ball (n,((t0 - s0) * (2 "))) ; ::_thesis: x in [.0,t0.] then reconsider u = x as Point of (Closed-Interval-MSpace (0,1)) ; x in [.0,1.] by A4, A83; then reconsider t = x as Real ; Ball (n,((t0 - s0) * (2 "))) = { q where q is Element of (Closed-Interval-MSpace (0,1)) : dist (n,q) < (t0 - s0) * (2 ") } by METRIC_1:17; then ex p being Element of (Closed-Interval-MSpace (0,1)) st ( p = u & dist (n,p) < (t0 - s0) * (2 ") ) by A83; then abs (t - s0) < (t0 - s0) * (2 ") by HEINE:1; then A84: abs (t - s0) < t0 - s0 by A81, XXREAL_0:2; t - s0 <= abs (t - s0) by ABSVALUE:4; then t - s0 < t0 - s0 by A84, XXREAL_0:2; then A85: t <= t0 by XREAL_1:9; 0 <= t by A4, A83, XXREAL_1:1; then t in { q where q is Real : ( 0 <= q & q <= t0 ) } by A85; hence x in [.0,t0.] by RCOMP_1:def_1; ::_thesis: verum end; A86: Ball (n,((t0 - s0) * (2 "))) c= [.0,d.] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Ball (n,((t0 - s0) * (2 "))) or x in [.0,d.] ) assume A87: x in Ball (n,((t0 - s0) * (2 "))) ; ::_thesis: x in [.0,d.] then reconsider v = x as Point of (Closed-Interval-MSpace (0,1)) ; x in [.0,1.] by A4, A87; then reconsider t = x as Real ; Ball (n,((t0 - s0) * (2 "))) = { q where q is Element of (Closed-Interval-MSpace (0,1)) : dist (n,q) < (t0 - s0) * (2 ") } by METRIC_1:17; then ex p being Element of (Closed-Interval-MSpace (0,1)) st ( p = v & dist (n,p) < (t0 - s0) * (2 ") ) by A87; then A88: abs (t - s0) < (t0 - s0) * (2 ") by HEINE:1; A89: now__::_thesis:_t_<_d percases ( s0 <= t or t < s0 ) ; suppose s0 <= t ; ::_thesis: t < d then 0 <= t - s0 by XREAL_1:48; then t - s0 < (t0 - s0) * (2 ") by A88, ABSVALUE:def_1; then t < s0 + ((t0 - s0) * (2 ")) by XREAL_1:19; hence t < d by A80, XXREAL_0:2; ::_thesis: verum end; supposeA90: t < s0 ; ::_thesis: t < d s0 < s0 + ((t0 - s0) * (2 ")) by A69, XREAL_1:29; then s0 < d by A80, XXREAL_0:2; hence t < d by A90, XXREAL_0:2; ::_thesis: verum end; end; end; 0 <= t by A82, A87, XXREAL_1:1; then t in { w0 where w0 is Real : ( 0 <= w0 & w0 <= d ) } by A89; hence x in [.0,d.] by RCOMP_1:def_1; ::_thesis: verum end; Ball (m,(min (s,((t0 - s0) * (2 "))))) c= Ball (m,s) by PCOMPS_1:1, XXREAL_0:17; then W0 c= V by A73, XBOOLE_1:1; then f . w1 in f .: V by A77, FUNCT_2:35; then f . w1 in W by A71; then d in A by A86, BORSUK_1:40; hence contradiction by A26, A78, XBOOLE_0:3; ::_thesis: verum end; thus P misses Q by A21, XBOOLE_0:def_7; ::_thesis: verum end; hence contradiction by Th19, CONNSP_1:10; ::_thesis: verum end; theorem Th22: :: TREAL_1:22 for a, b being real number st a <= b holds for f being continuous Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (a,b)) ex x being Point of (Closed-Interval-TSpace (a,b)) st f . x = x proof let a, b be real number ; ::_thesis: ( a <= b implies for f being continuous Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (a,b)) ex x being Point of (Closed-Interval-TSpace (a,b)) st f . x = x ) assume A1: a <= b ; ::_thesis: for f being continuous Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (a,b)) ex x being Point of (Closed-Interval-TSpace (a,b)) st f . x = x let f be continuous Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (a,b)); ::_thesis: ex x being Point of (Closed-Interval-TSpace (a,b)) st f . x = x now__::_thesis:_ex_x_being_Point_of_(Closed-Interval-TSpace_(a,b))_st_f_._x_=_x percases ( a < b or a = b ) by A1, XXREAL_0:1; supposeA2: a < b ; ::_thesis: ex x being Point of (Closed-Interval-TSpace (a,b)) st f . x = x set L = L[01] (((#) (a,b)),((a,b) (#))); set P = P[01] (a,b,((#) (0,1)),((0,1) (#))); A3: P[01] (a,b,((#) (0,1)),((0,1) (#))) is continuous Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (0,1)) by A2, Th12; set g = ((P[01] (a,b,((#) (0,1)),((0,1) (#)))) * f) * (L[01] (((#) (a,b)),((a,b) (#)))); A4: id (Closed-Interval-TSpace (a,b)) = (L[01] (((#) (a,b)),((a,b) (#)))) * (P[01] (a,b,((#) (0,1)),((0,1) (#)))) by A2, Th15; then A5: f = ((L[01] (((#) (a,b)),((a,b) (#)))) * (P[01] (a,b,((#) (0,1)),((0,1) (#))))) * f by FUNCT_2:17 .= (L[01] (((#) (a,b)),((a,b) (#)))) * ((P[01] (a,b,((#) (0,1)),((0,1) (#)))) * f) by RELAT_1:36 .= (L[01] (((#) (a,b)),((a,b) (#)))) * (((P[01] (a,b,((#) (0,1)),((0,1) (#)))) * f) * ((L[01] (((#) (a,b)),((a,b) (#)))) * (P[01] (a,b,((#) (0,1)),((0,1) (#)))))) by A4, FUNCT_2:17 .= (L[01] (((#) (a,b)),((a,b) (#)))) * ((((P[01] (a,b,((#) (0,1)),((0,1) (#)))) * f) * (L[01] (((#) (a,b)),((a,b) (#))))) * (P[01] (a,b,((#) (0,1)),((0,1) (#))))) by RELAT_1:36 .= ((L[01] (((#) (a,b)),((a,b) (#)))) * (((P[01] (a,b,((#) (0,1)),((0,1) (#)))) * f) * (L[01] (((#) (a,b)),((a,b) (#)))))) * (P[01] (a,b,((#) (0,1)),((0,1) (#)))) by RELAT_1:36 ; L[01] (((#) (a,b)),((a,b) (#))) is continuous Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (a,b)) by A1, Th8; then consider y being Point of (Closed-Interval-TSpace (0,1)) such that A6: (((P[01] (a,b,((#) (0,1)),((0,1) (#)))) * f) * (L[01] (((#) (a,b)),((a,b) (#))))) . y = y by A3, Th21, TOPMETR:20; A7: id (Closed-Interval-TSpace (0,1)) = (P[01] (a,b,((#) (0,1)),((0,1) (#)))) * (L[01] (((#) (a,b)),((a,b) (#)))) by A2, Th15; now__::_thesis:_ex_x_being_Element_of_the_carrier_of_(Closed-Interval-TSpace_(a,b))_st_f_._x_=_x take x = (L[01] (((#) (a,b)),((a,b) (#)))) . y; ::_thesis: f . x = x thus f . x = ((((L[01] (((#) (a,b)),((a,b) (#)))) * (((P[01] (a,b,((#) (0,1)),((0,1) (#)))) * f) * (L[01] (((#) (a,b)),((a,b) (#)))))) * (P[01] (a,b,((#) (0,1)),((0,1) (#))))) * (L[01] (((#) (a,b)),((a,b) (#))))) . y by A5, FUNCT_2:15 .= (((L[01] (((#) (a,b)),((a,b) (#)))) * (((P[01] (a,b,((#) (0,1)),((0,1) (#)))) * f) * (L[01] (((#) (a,b)),((a,b) (#)))))) * (id (Closed-Interval-TSpace (0,1)))) . y by A7, RELAT_1:36 .= ((L[01] (((#) (a,b)),((a,b) (#)))) * (((P[01] (a,b,((#) (0,1)),((0,1) (#)))) * f) * (L[01] (((#) (a,b)),((a,b) (#)))))) . y by FUNCT_2:17 .= x by A6, FUNCT_2:15 ; ::_thesis: verum end; hence ex x being Point of (Closed-Interval-TSpace (a,b)) st f . x = x ; ::_thesis: verum end; supposeA8: a = b ; ::_thesis: ex x being Point of (Closed-Interval-TSpace (a,b)) st f . x = x then ( [.a,b.] = {a} & a = (#) (a,b) ) by Def1, XXREAL_1:17; then A9: the carrier of (Closed-Interval-TSpace (a,b)) = {((#) (a,b))} by A8, TOPMETR:18; now__::_thesis:_ex_x_being_Point_of_(Closed-Interval-TSpace_(a,b))_st_f_._x_=_x take x = (#) (a,b); ::_thesis: f . x = x thus f . x = x by A9, TARSKI:def_1; ::_thesis: verum end; hence ex x being Point of (Closed-Interval-TSpace (a,b)) st f . x = x ; ::_thesis: verum end; end; end; hence ex x being Point of (Closed-Interval-TSpace (a,b)) st f . x = x ; ::_thesis: verum end; theorem Th23: :: TREAL_1:23 for X, Y being non empty SubSpace of R^1 for f being continuous Function of X,Y st ex a, b being Real st ( a <= b & [.a,b.] c= the carrier of X & [.a,b.] c= the carrier of Y & f .: [.a,b.] c= [.a,b.] ) holds ex x being Point of X st f . x = x proof let X, Y be non empty SubSpace of R^1 ; ::_thesis: for f being continuous Function of X,Y st ex a, b being Real st ( a <= b & [.a,b.] c= the carrier of X & [.a,b.] c= the carrier of Y & f .: [.a,b.] c= [.a,b.] ) holds ex x being Point of X st f . x = x let f be continuous Function of X,Y; ::_thesis: ( ex a, b being Real st ( a <= b & [.a,b.] c= the carrier of X & [.a,b.] c= the carrier of Y & f .: [.a,b.] c= [.a,b.] ) implies ex x being Point of X st f . x = x ) given a, b being Real such that A1: a <= b and A2: [.a,b.] c= the carrier of X and A3: [.a,b.] c= the carrier of Y and A4: f .: [.a,b.] c= [.a,b.] ; ::_thesis: ex x being Point of X st f . x = x reconsider A = [.a,b.] as non empty Subset of X by A1, A2, XXREAL_1:1; A5: dom (f | A) = (dom f) /\ A by RELAT_1:61; ( A = the carrier of X /\ A & dom f = the carrier of X ) by FUNCT_2:def_1, XBOOLE_1:28; then A6: dom (f | A) = the carrier of (Closed-Interval-TSpace (a,b)) by A1, A5, TOPMETR:18; A7: A = the carrier of (Closed-Interval-TSpace (a,b)) by A1, TOPMETR:18; then reconsider Z = Closed-Interval-TSpace (a,b) as SubSpace of X by TSEP_1:4; rng (f | A) c= the carrier of (Closed-Interval-TSpace (a,b)) by A4, A7, RELAT_1:115; then reconsider g = f | A as Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (a,b)) by A6, FUNCT_2:def_1, RELSET_1:4; A8: Z is SubSpace of Y by A3, A7, TSEP_1:4; for s being Point of (Closed-Interval-TSpace (a,b)) holds g is_continuous_at s proof let s be Point of (Closed-Interval-TSpace (a,b)); ::_thesis: g is_continuous_at s reconsider w = s as Point of X by A7, TARSKI:def_3; for G being Subset of (Closed-Interval-TSpace (a,b)) st G is open & g . s in G holds ex H being Subset of Z st ( H is open & s in H & g .: H c= G ) proof let G be Subset of (Closed-Interval-TSpace (a,b)); ::_thesis: ( G is open & g . s in G implies ex H being Subset of Z st ( H is open & s in H & g .: H c= G ) ) A9: f is_continuous_at w by TMAP_1:44; assume G is open ; ::_thesis: ( not g . s in G or ex H being Subset of Z st ( H is open & s in H & g .: H c= G ) ) then consider G0 being Subset of Y such that A10: G0 is open and A11: G0 /\ ([#] (Closed-Interval-TSpace (a,b))) = G by A8, TOPS_2:24; assume g . s in G ; ::_thesis: ex H being Subset of Z st ( H is open & s in H & g .: H c= G ) then f . w in G by A7, FUNCT_1:49; then f . w in G0 by A11, XBOOLE_0:def_4; then consider H0 being Subset of X such that A12: H0 is open and A13: w in H0 and A14: f .: H0 c= G0 by A10, A9, TMAP_1:43; now__::_thesis:_ex_H_being_Subset_of_Z_st_ (_H_is_open_&_s_in_H_&_g_.:_H_c=_G_) reconsider H = H0 /\ ([#] (Closed-Interval-TSpace (a,b))) as Subset of Z ; take H = H; ::_thesis: ( H is open & s in H & g .: H c= G ) thus H is open by A12, TOPS_2:24; ::_thesis: ( s in H & g .: H c= G ) thus s in H by A13, XBOOLE_0:def_4; ::_thesis: g .: H c= G thus g .: H c= G ::_thesis: verum proof let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in g .: H or t in G ) assume t in g .: H ; ::_thesis: t in G then consider r being set such that r in dom g and A15: r in H and A16: t = g . r by FUNCT_1:def_6; A17: r in the carrier of Z by A15; reconsider r = r as Point of (Closed-Interval-TSpace (a,b)) by A15; r in dom g by A17, FUNCT_2:def_1; then A18: t in g .: the carrier of Z by A16, FUNCT_1:def_6; reconsider p = r as Point of X by A7, TARSKI:def_3; p in [#] X ; then A19: p in dom f by FUNCT_2:def_1; ( t = f . p & p in H0 ) by A7, A15, A16, FUNCT_1:49, XBOOLE_0:def_4; then t in f .: H0 by A19, FUNCT_1:def_6; hence t in G by A11, A14, A18, XBOOLE_0:def_4; ::_thesis: verum end; end; hence ex H being Subset of Z st ( H is open & s in H & g .: H c= G ) ; ::_thesis: verum end; hence g is_continuous_at s by TMAP_1:43; ::_thesis: verum end; then reconsider h = g as continuous Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (a,b)) by TMAP_1:44; now__::_thesis:_ex_x_being_Point_of_X_st_f_._x_=_x consider y being Point of (Closed-Interval-TSpace (a,b)) such that A20: h . y = y by A1, Th22; reconsider x = y as Point of X by A7, TARSKI:def_3; take x = x; ::_thesis: f . x = x thus f . x = x by A7, A20, FUNCT_1:49; ::_thesis: verum end; hence ex x being Point of X st f . x = x ; ::_thesis: verum end; theorem :: TREAL_1:24 for X, Y being non empty SubSpace of R^1 for f being continuous Function of X,Y st ex a, b being Real st ( a <= b & [.a,b.] c= the carrier of X & f .: [.a,b.] c= [.a,b.] ) holds ex x being Point of X st f . x = x proof let X, Y be non empty SubSpace of R^1 ; ::_thesis: for f being continuous Function of X,Y st ex a, b being Real st ( a <= b & [.a,b.] c= the carrier of X & f .: [.a,b.] c= [.a,b.] ) holds ex x being Point of X st f . x = x let f be continuous Function of X,Y; ::_thesis: ( ex a, b being Real st ( a <= b & [.a,b.] c= the carrier of X & f .: [.a,b.] c= [.a,b.] ) implies ex x being Point of X st f . x = x ) given a, b being Real such that A1: a <= b and A2: [.a,b.] c= the carrier of X and A3: f .: [.a,b.] c= [.a,b.] ; ::_thesis: ex x being Point of X st f . x = x set g = (Y incl R^1) * f; the carrier of Y c= the carrier of R^1 by BORSUK_1:1; then reconsider B = f .: [.a,b.] as Subset of R^1 by XBOOLE_1:1; ((Y incl R^1) * f) .: [.a,b.] = (Y incl R^1) .: (f .: [.a,b.]) by RELAT_1:126; then ((Y incl R^1) * f) .: [.a,b.] = ((id R^1) | Y) .: B by TMAP_1:def_6; then ((Y incl R^1) * f) .: [.a,b.] = (id R^1) .: B by TMAP_1:55; then A4: ((Y incl R^1) * f) .: [.a,b.] c= [.a,b.] by A3, FUNCT_1:92; A5: ( Y incl R^1 is continuous Function of Y,R^1 & R^1 is SubSpace of R^1 ) by TMAP_1:87, TSEP_1:2; the carrier of X c= the carrier of R^1 by BORSUK_1:1; then A6: [.a,b.] c= the carrier of R^1 by A2, XBOOLE_1:1; now__::_thesis:_ex_x_being_Point_of_X_st_f_._x_=_x consider x being Point of X such that A7: ((Y incl R^1) * f) . x = x by A1, A2, A5, A6, A4, Th23; the carrier of Y c= the carrier of R^1 by BORSUK_1:1; then reconsider y = f . x as Point of R^1 by TARSKI:def_3; take x = x; ::_thesis: f . x = x thus f . x = (Y incl R^1) . y by TMAP_1:84 .= x by A7, FUNCT_2:15 ; ::_thesis: verum end; hence ex x being Point of X st f . x = x ; ::_thesis: verum end;