The Mizar article:

The Brouwer Fixed Point Theorem for Intervals

by
Toshihiko Watanabe

Received August 17, 1992

Copyright (c) 1992 Association of Mizar Users

MML identifier: TREAL_1
[ MML identifier index ]


environ

 vocabulary ARYTM, RCOMP_1, BOOLE, PRE_TOPC, TOPMETR, PCOMPS_1, METRIC_1,
      SUBSET_1, ARYTM_1, FUNCT_1, ABSVALUE, TARSKI, SETFAM_1, SEQ_1, BORSUK_1,
      TMAP_1, RELAT_1, ORDINAL2, ARYTM_3, TOPS_2, RELAT_2, SEQ_2, SEQ_4,
      SQUARE_1, FUNCT_3, TREAL_1;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      RELAT_1, FUNCT_1, FUNCT_2, ABSVALUE, REAL_1, SQUARE_1, SEQ_4, RCOMP_1,
      PRE_TOPC, TOPS_2, CONNSP_1, METRIC_1, GRCAT_1, STRUCT_0, PCOMPS_1,
      TOPMETR, TSEP_1, TMAP_1, BORSUK_1;
 constructors ABSVALUE, REAL_1, SQUARE_1, SEQ_4, RCOMP_1, TOPS_2, CONNSP_1,
      GRCAT_1, TOPMETR, TMAP_1, PARTFUN1, MEMBERED;
 clusters SUBSET_1, FUNCT_1, PRE_TOPC, TOPMETR, BORSUK_1, STRUCT_0, XREAL_0,
      METRIC_1, RELSET_1, MEMBERED, ZFMISC_1;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
 definitions TARSKI;
 theorems TARSKI, AXIOMS, SUBSET_1, FUNCT_1, FUNCT_2, REAL_1, REAL_2, SQUARE_1,
      ABSVALUE, RCOMP_1, SEQ_2, SEQ_4, METRIC_1, PRE_TOPC, TOPS_1, TOPS_2,
      CONNSP_1, PCOMPS_1, BORSUK_1, TOPMETR, TOPMETR2, HEINE, TSEP_1, TMAP_1,
      RELAT_1, GRCAT_1, TBSP_1, RELSET_1, XREAL_0, XBOOLE_0, XBOOLE_1,
      XCMPLX_0, XCMPLX_1;
 schemes FUNCT_2;

begin
:: 1. Properties of Topological Intervals.

reserve a,b,c,d for real number;

theorem Th1:
 a <= c & d <= b implies [.c,d.] c= [.a,b.]
 proof
A1: c is Real by XREAL_0:def 1;
A2: d is Real by XREAL_0:def 1;
  assume A3: a <= c & d <= b;
  per cases;
  suppose c > d;
   then [.c,d.] = {} by RCOMP_1:13;
   hence thesis by XBOOLE_1:2;
  suppose c <= d;
   then A4: a <= d & c <= b by A3,AXIOMS:22;
   then A5: c in {r where r is Real : a <= r & r <= b} by A1,A3;
      d in {r where r is Real : a <= r & r <= b} by A2,A3,A4;
    then c in [.a,b.] & d in [.a,b.] by A5,RCOMP_1:def 1;
   hence thesis by RCOMP_1:16;
 end;

theorem Th2:
 a <= c & b <= d & c <= b implies [.a,b.] \/ [.c,d.] = [.a,d.]
 proof
  assume A1: a <= c & b <= d & c <= b;
  then A2: a <= b & c <= d by AXIOMS:22;
 A3: [.a,d.] c= [.a,b.] \/ [.c,d.]
  proof
     for r being set st r in [.a,d.] holds r in [. a,b .] \/ [. c,d .]
    proof
     let r be set;
     assume A4: r in [.a,d.];
     then reconsider s = r as Real;
         [.a,d.] = {q where q is Real : a<=q & q<=d } by RCOMP_1:def 1;
     then A5: ex p being Real st p = s & a<=p & p<=d by A4;

     A6: [.a,b.] = {u where u is Real : a<=u & u<=b } by RCOMP_1:def 1;
     A7: [.c,d.] = {v where v is Real : c <=v & v<=d } by RCOMP_1:def 1;
       now per cases;
      suppose s<=b;
       then s in [.a,b.] & [.a,b.] c= [.a,b.] \/ [.c,d.]
            by A5,A6,XBOOLE_1:7;
      hence s in [.a,b.] \/ [.c,d.];
      suppose not s<=b;
        then c <=s by A1,AXIOMS:22;
       then s in [.c,d.] & [.c,d.] c= [.a,b.] \/ [.c,d.]
            by A5,A7,XBOOLE_1:7;
       hence s in [.a,b.] \/ [.c,d.];
     end;
     hence thesis;
    end;
    hence thesis by TARSKI:def 3;
  end;
A8: b is Real by XREAL_0:def 1;
A9: c is Real by XREAL_0:def 1;
   [.a,b.] \/ [.c,d.] c= [.a,d.]
   proof
    A10: [.a,b.] c= [.a,d.]
     proof
        a<=d & b in {q where q is Real : a<=q & q<=d } by A1,A2,A8,AXIOMS:22;
      then a in [.a,d.] & b in [.a,d.] by RCOMP_1:15,def 1;
      hence thesis by RCOMP_1:16;
     end;
      [.c,d.] c= [.a,d.]
     proof
        a<=d & c in {q where q is Real : a<=q & q<=d } by A1,A2,A9,AXIOMS:22;
      then d in [.a,d.] & c in [.a,d.] by RCOMP_1:15,def 1;
      hence thesis by RCOMP_1:16;
     end;
    hence thesis by A10,XBOOLE_1:8;
   end;
  hence thesis by A3,XBOOLE_0:def 10;
end;

theorem Th3:
 a <= c & b <= d & c <= b implies [.a,b.] /\ [.c,d.] = [.c,b.]
 proof
  assume A1: a <= c & b <= d & c <= b;
   then A2: a <= b & c <= d by AXIOMS:22;
 A3: [.c,b.] c= [.a,b.] /\ [.c,d.]
  proof
    A4: [.c,b.] c= [.a,b.]
     proof
         c is Real by XREAL_0:def 1;
       then c in {q where q is Real : a<=q & q<=b } by A1;
      then c in [.a,b.] & b in [.a,b.] by A2,RCOMP_1:15,def 1;
      hence thesis by RCOMP_1:16;
     end;
      [.c,b.] c= [.c,d.]
     proof
         b is Real by XREAL_0:def 1;
       then b in {q where q is Real : c <=q & q<=d } by A1;
      then c in [.c,d.] & b in [.c,d.] by A2,RCOMP_1:15,def 1;
      hence thesis by RCOMP_1:16;
     end;
    hence thesis by A4,XBOOLE_1:19;
  end;
   [.a,b.] /\ [.c,d.] c= [.c,b.]
   proof
     for r being set st r in [.a,b.] /\ [.c,d.] holds r in [.c,b.]
    proof
     let r be set;
     assume A5: r in [.a,b.] /\ [.c,d.];
     then A6: r in [.a,b.] & r in [.c,d.] by XBOOLE_0:def 3;
     reconsider s = r as Real by A5;
         [.a,b.] = {u where u is Real : a<=u & u<=b } &
       [.c,d.] = {v where v is Real : c <=v & v<=d } by RCOMP_1:def 1;
     then (ex p being Real st p = s & a<=p & p<=b) &
          (ex q being Real st q = s & c <=q & q<=d) by A6;
     then s in {w where w is Real : c <=w & w<=b};
     hence thesis by RCOMP_1:def 1;
    end;
    hence thesis by TARSKI:def 3;
   end;
  hence thesis by A3,XBOOLE_0:def 10;
 end;

Lm1: for x being set st x in [.a,b.] holds x is Real;

Lm2: for v being real number, x being set st x in [.a,b.] & a <= b & v = x
holds a <= v & v <= b
 proof
  let v be real number, x be set;
  assume A1: x in [.a,b.] & a <= b & v = x;
  then x in {q where q is Real : a<=q & q<=b } by RCOMP_1:def 1;
  then ex p being Real st p = x & a<=p & p<=b;
  hence a<=v & v<=b by A1;
 end;

Lm3: for x being Point of Closed-Interval-TSpace(a,b) st a <= b
 holds x is 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:25;
   hence thesis by Lm1;
 end;

theorem Th4:
 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 a, b as Real by XREAL_0:def 1;
    reconsider B = A` as Subset of TopSpaceMetr(RealSpace)
      by TOPMETR:def 7;
       A2: the carrier of RealSpace = the carrier of TopSpaceMetr(RealSpace)
                                                               by TOPMETR:16;
     reconsider D = B as Subset of RealSpace by TOPMETR:16;
       set C = D`;
       for c being Point of RealSpace st c in B
       ex r being real number st r > 0 & Ball(c,r) c= B
      proof
        let c be Point of RealSpace;
       assume A3: c in B;
        reconsider n = c as Real by METRIC_1:def 14;
           not n in [.a,b.] by A1,A3,SUBSET_1:54;
        then A4: not n in {p where p is Real : a <= p & p <=
 b} by RCOMP_1:def 1;
       thus ex r being real number st r > 0 & Ball(c,r) c= B
         proof
            now per cases by A4;
           suppose A5: not a <= n;
             take r = a - n;
                now let x be set;
               assume A6: x in Ball(c,r);
                then reconsider t = x as Real by METRIC_1:def 14;
                reconsider u = x as Point of RealSpace by A6;
                   Ball(c,r) = {q where q is Element of
RealSpace
                                :dist(c,q)<r} by METRIC_1:18;
                 then ex v being Element of RealSpace st
                                                   v = u & dist(c,v)<r by A6;
                 then (real_dist).(t,n) < r by METRIC_1:def 1,def 14;
                 then abs(t - n) < r & t - n <= abs(t - n)
                                          by ABSVALUE:11,METRIC_1:def 13;
                 then t - n < a - n by AXIOMS:22;
                 then not ex q being Real st q = t & a <= q & q <= b
                         by REAL_1:49;
                 then not t in {p where p is Real : a <= p & p <= b};
                 then not u in C & the carrier of RealSpace <> {}
                                                  by A1,A2,RCOMP_1:def 1,
TOPMETR:def 7;
               hence x in B by SUBSET_1:50;
              end;
            hence r > 0 & Ball(c,r) c= B by A5,SQUARE_1:11,TARSKI:def 3;
           suppose A7: not n <= b;
             take r = n - b;
                now let x be set;
               assume A8: x in Ball(c,r);
                then reconsider t = x as Real by METRIC_1:def 14;
                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:18;
                 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,def 14;
                 then abs(n - t) < r & n - t <= abs(n - t)
                                          by ABSVALUE:11,METRIC_1:def 13;
                 then n - t < n - b by AXIOMS:22;
                 then not ex q being Real st q = t & a <= q & q <= b by REAL_2:
106;
                 then not t in {p where p is Real : a <= p & p <= b};
                 then not u in C & the carrier of RealSpace <> {}
                                                  by A1,A2,RCOMP_1:def 1,
TOPMETR:def 7;
               hence x in B by SUBSET_1:50;
              end;
             hence r > 0 & Ball(c,r) c= B by A7,SQUARE_1:11,TARSKI:def 3;
          end;
          hence thesis;
         end;
      end;
     then A` is open by TOPMETR:22,def 7;
    hence thesis by TOPS_1:29;
 end;

theorem Th5:
 a <= b implies Closed-Interval-TSpace(a,b) is closed SubSpace of R^1
 proof
  assume a <= b;
   then the carrier of Closed-Interval-TSpace(a,b) = [.a,b.] by TOPMETR:25;
    then for A be Subset of R^1 holds
 A = the carrier of Closed-Interval-TSpace(a,b) implies A is closed by Th4;
  hence thesis by BORSUK_1:def 14;
 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 A1: a <= c & d <= b & c <= d;
   then a <= d by AXIOMS:22;
   then A2: a <= b by A1,AXIOMS:22;
      [.c,d.] c= [.a,b.] by A1,Th1;
   then the carrier of Closed-Interval-TSpace(c,d) c= [.a,b.] by A1,TOPMETR:25
;
   then A3: the carrier of Closed-Interval-TSpace(c,d) c=
             the carrier of Closed-Interval-TSpace(a,b) by A2,TOPMETR:25;
      Closed-Interval-TSpace(c,d) is closed SubSpace of R^1 by A1,Th5;
  hence thesis by A3,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 A1: a <= c & b <= d & c <= b;
   then A2: a <= b & c <= d by AXIOMS:22;
   then A3: a <= d by A1,AXIOMS:22;
    A4: the carrier of Closed-Interval-TSpace(a,b) = [.a,b.] &
        the carrier of Closed-Interval-TSpace(c,d) = [.c,d.] by A2,TOPMETR:25;
    A5: the carrier of Closed-Interval-TSpace(a,d) = [.a,d.] by A3,TOPMETR:25;
     [.a,b.] \/ [.c,d.] = [.a,d.] by A1,Th2;
  hence Closed-Interval-TSpace(a,d) =
         Closed-Interval-TSpace(a,b) union Closed-Interval-TSpace(c,d)
                                               by A4,A5,TSEP_1:def 2;
    A6: the carrier of Closed-Interval-TSpace(c,b) = [.c,b.] by A1,TOPMETR:25;
    A7: [.a,b.] /\ [.c,d.] = [.c,b.] by A1,Th3;
   then (the carrier of Closed-Interval-TSpace(a,b)) /\
    (the carrier of Closed-Interval-TSpace(c,d)) <> {} by A1,A4,RCOMP_1:15;
   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 5;
 end;

definition let a,b be real number;
 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,RCOMP_1:15;
   hence thesis by A1,TOPMETR:25;
  end;
 correctness;
 func (a,b)(#) -> Point of Closed-Interval-TSpace(a,b) equals
:Def2:  b;
 coherence
  proof
      b in [.a,b.] by A1,RCOMP_1:15;
   hence thesis by A1,TOPMETR:25;
  end;
 correctness;
end;

theorem
   0[01] = (#)(0,1) & 1[01] = (0,1)(#)
 proof
  thus 0[01] = (#)(0,1) by Def1,BORSUK_1:def 17;
  thus 1[01] = (0,1)(#) by Def2,BORSUK_1:def 18;
 end;

theorem
   a <= b & b <= c implies (#)(a,b) = (#)(a,c) & (b,c)(#) = (a,c)(#)
 proof
   assume A1: a <= b & b <= c;
    then A2: a <= c by AXIOMS:22;
    thus (#)(a,b) = a by A1,Def1
               .= (#)(a,c) by A2,Def1;
    thus (b,c)(#) = c by A1,Def2
               .= (a,c)(#) by A2,Def2;
 end;

begin
:: 2. Continuous Mappings Between Topological Intervals.

definition let a,b be real number such that A1: a <= b;
  let t1,t2 be Point of Closed-Interval-TSpace(a,b);
 func L[01](t1,t2) -> map of
  Closed-Interval-TSpace(0,1),Closed-Interval-TSpace(a,b) means
:Def3: for s being Point of Closed-Interval-TSpace(0,1),
   r,r1,r2 being real number st
   s=r & r1=t1 & r2=t2 holds it.s = (1-r)*r1 + r*r2;
 existence
  proof
   reconsider r1 = t1, r2 = t2 as Real by A1,Lm3;
   deffunc U(Element of REAL) = (1-$1)*r1 + $1*r2;
   consider LI being Function of REAL,REAL such that
    A2: for r being Real holds LI.r= U(r) from LambdaD;

     A3: dom(LI|[.0,1.]) = the carrier of Closed-Interval-TSpace(0,1)
          proof
           A4: [.0,1.] = REAL /\ [.0,1.] by XBOOLE_1:28;
              dom LI = REAL & dom(LI|[.0,1.]) = (dom LI) /\ [.0,1.]
                                               by FUNCT_2:def 1,RELAT_1:90;
           hence thesis by A4,TOPMETR:25;
          end;
     A5: [.a,b.] = the carrier of Closed-Interval-TSpace(a,b)
                                                        by A1,TOPMETR:25;
      rng(LI|[.0,1.]) c= the carrier of Closed-Interval-TSpace(a,b)
     proof
          now let y be set;
         assume A6: y in rng(LI|[.0,1.]);
          then y in LI.:[.0,1.] by RELAT_1:148;
          then consider x being set such that
               x in dom LI and A7: x in [.0,1.] and A8: y = LI.x by FUNCT_1:def
12;
          reconsider c = x as Real by A7;
              c in { p where p is Real : 0 <= p & p <= 1} by A7,RCOMP_1:def 1;
          then A9: ex u being Real st u = c & 0 <= u & u <= 1;

             r1 in [.a,b.] & r2 in [.a,b.] by A5;
          then r1 in { p where p is Real : a <= p & p <= b} &
               r2 in { p where p is Real : a <= p & p <= b} by RCOMP_1:def 1;
          then A10: (ex v1 being Real st v1 = r1 & a <= v1 & v1 <= b) &
               (ex v2 being Real st v2 = r2 & a <= v2 & v2 <= b);

             rng(LI|[.0,1.]) c= rng LI & rng LI c= REAL
           by FUNCT_1:76,RELSET_1:12;
          then rng(LI|[.0,1.]) c= REAL by XBOOLE_1:1;
          then reconsider d = y as Real by A6;
            A11: d = (1 - c)*r1 + c*r2 by A2,A8;
           A12: 0 <= 1 - c & 1 - c <= 1 by A9,REAL_2:173,SQUARE_1:12;
          then (1 - c)*a <= (1 - c)*r1 & c*a <= c*r2 by A9,A10,AXIOMS:25;
          then (1 - c)*a + c*a <= d by A11,REAL_1:55;
          then ((1 - c) + c)*a <= d by XCMPLX_1:8;
          then ((1 + - c) + c)*a <= d by XCMPLX_0:def 8;
          then (1 + (- c + c))*a <= d by XCMPLX_1:1;
          then A13: (1 + 0)*a <= d by XCMPLX_0:def 6;
             (1 - c)*r1 <= (1 - c)*b & c*r2 <= c*b by A9,A10,A12,AXIOMS:25;
          then d <= (1 - c)*b + c*b by A11,REAL_1:55;
          then d <= ((1 - c) + c)*b by XCMPLX_1:8;
          then d <= ((1 + - c) + c)*b by XCMPLX_0:def 8;
          then d <= (1 + (- c + c))*b by XCMPLX_1:1;
          then d <= (1 + 0)*b by XCMPLX_0:def 6;
          then y in { q where q is Real : a <= q & q <= b} by A13;
         hence y in [.a,b.] by RCOMP_1:def 1;
        end;
      hence thesis by A5,TARSKI:def 3;
     end;
   then LI|[.0,1.] is Function
     of the carrier of Closed-Interval-TSpace(0,1),
        the carrier of Closed-Interval-TSpace(a,b)
   by A3,FUNCT_2:def 1,RELSET_1:11;
   then reconsider F = LI|[.0,1.] as map
     of Closed-Interval-TSpace(0,1),Closed-Interval-TSpace(a,b);
   take F;
   let s be Point of Closed-Interval-TSpace(0,1), r,r1,r2 be real number
   such that
       A14: s=r & r1=t1 & r2=t2;
A15: r is Real by XREAL_0:def 1;
       s in the carrier of Closed-Interval-TSpace(0,1) &
      the carrier of Closed-Interval-TSpace(0,1) = [.0,1.] by TOPMETR:25;
   hence F.s = LI.r by A14,FUNCT_1:72
      .= (1-r)*r1 + r*r2 by A2,A14,A15;
 end;
 uniqueness
  proof
    let F1, F2 be map of
       Closed-Interval-TSpace(0,1),Closed-Interval-TSpace(a,b);
   assume
    A16: for s being Point of Closed-Interval-TSpace(0,1),
   r,r1,r2 being real number st
         s=r & r1=t1 & r2=t2 holds F1.s = (1-r)*r1 + r*r2;
   assume
    A17: for s being Point of Closed-Interval-TSpace(0,1),
   r,r1,r2 being real number st
         s=r & r1=t1 & r2=t2 holds F2.s = (1-r)*r1 + r*r2;
      for s being Point of Closed-Interval-TSpace(0,1) holds F1.s = F2.s
     proof
      let s be Point of Closed-Interval-TSpace(0,1);
      reconsider r = s as Real by Lm3;
           reconsider r1 = t1, r2 = t2 as Real by A1,Lm3;
      thus F1.s = (1-r)*r1 + r*r2 by A16
                .= F2.s by A17;
     end;
   hence F1 = F2 by FUNCT_2:113;
  end;
 end;

theorem Th10:
 a <= b implies
  for t1,t2 being Point of Closed-Interval-TSpace(a,b) holds
   for s being Point of Closed-Interval-TSpace(0,1),
    r,r1,r2 being real number st
   s=r & r1=t1 & r2=t2 holds L[01](t1,t2).s = (r2 - r1)*r + r1
 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), r,r1,r2 be real number;
  assume s=r & r1=t1 & r2=t2;
  hence L[01](t1,t2).s = (1-r)*r1 + r*r2 by A1,Def3
     .= (1*r1 - r*r1) + r*r2 by XCMPLX_1:40
     .= (1*r1 + - r*r1) + r*r2 by XCMPLX_0:def 8
     .= (- r*r1 + r*r2) + r1 by XCMPLX_1:1
     .= (r*(- r1) + r*r2) + r1 by XCMPLX_1:175
     .= r*(r2 + - r1) + r1 by XCMPLX_1:8
     .= (r2 - r1)*r + r1 by XCMPLX_0:def 8;
 end;

theorem Th11:
 a <= b implies
  for t1,t2 being Point of Closed-Interval-TSpace(a,b) holds
   L[01](t1,t2) is continuous map of
     Closed-Interval-TSpace(0,1),Closed-Interval-TSpace(a,b)
 proof
  assume A1: a <= b;
  let t1,t2 be Point of Closed-Interval-TSpace(a,b);
   reconsider r1 = t1, r2 = t2 as Real by A1,Lm3;
   deffunc U(Element of REAL) = (r2 - r1)*$1 + r1;
    consider L being Function of REAL,REAL such that
        A2: for r being Real holds L.r= U(r) from LambdaD;
   reconsider f = L as map of R^1, R^1 by TOPMETR:24;
A3:    f is continuous by A2,TOPMETR:28;
      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 by Lm3;
            assume A5: s = w;
            thus L[01](t1,t2).s = (r2 - r1)*r + r1 by A1,Th10
                               .= f.w by A2,A5;
           end;
  A6: [.0,1.] = the carrier of Closed-Interval-TSpace(0,1) by TOPMETR:25;
      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:24;
        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
           A7: G0 is open and A8: G0 /\ [#] Closed-Interval-TSpace(a,b) = G
                                                              by TOPS_2:32;
        assume L[01](t1,t2).s in G;
         then f.w in G by A4;
         then f.w in G0 & f is_continuous_at w by A3,A8,TMAP_1:49,XBOOLE_0:def
3;
        then consider H0 being Subset of R^1 such that
          A9: H0 is open and A10: w in H0 and A11: f.:H0 c= G0 by A7,TMAP_1:48;
           now
             A12: [#] Closed-Interval-TSpace(0,1) =
            the carrier of Closed-Interval-TSpace(0,1) by PRE_TOPC:12;
          then H0 /\ [#] Closed-Interval-TSpace(0,1) is Subset of the carrier
of
              Closed-Interval-TSpace(0,1) by XBOOLE_1:17;
           then reconsider H = H0 /\ [#] Closed-Interval-TSpace(0,1)
           as Subset of Closed-Interval-TSpace(0,1);
          take H;
          thus H is open by A9,TOPS_2:32;
          thus s in H by A10,A12,XBOOLE_0:def 3;
          thus L[01](t1,t2).:H c= G
                proof
                  let t be set;
                 assume t in L[01](t1,t2).:H;
                  then consider r be 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 12;
                  A15: r in the carrier of Closed-Interval-TSpace(0,1)
                                                  by A13;
                 reconsider r as Point of Closed-Interval-TSpace(0,1) by A13;
                  reconsider p = r as Point of R^1 by A6,TARSKI:def 3,TOPMETR:
24;
                     p in the carrier of R^1;
                  then p in [#] R^1 by PRE_TOPC:12;
                  then t=f.p & p in H0 & p in dom f
                                           by A4,A13,A14,TOPS_2:51,XBOOLE_0:def
3;
                  then A16: t in f.:H0 by FUNCT_1:def 12;
                   A17:  rng L[01](t1,t2) c= [#] Closed-Interval-TSpace(a,b)
                                                           by TOPS_2:51;
                     r in dom L[01](t1,t2) by A12,A15,TOPS_2:51;
                  then t in
                   L[01](t1,t2).:(the carrier of Closed-Interval-TSpace(0,1))
                                                        by A14,FUNCT_1:def 12;
                  then t in rng L[01](t1,t2) by FUNCT_2:45;
                  hence thesis by A8,A11,A16,A17,XBOOLE_0:def 3;
                end;
         end;
        hence thesis;
       end;
      hence thesis by TMAP_1:48;
     end;
   hence thesis by TMAP_1:49;
 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 by A1,Lm3; 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 by Lm3;
        (#)(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 TMAP_1:92;
 end;

definition let a,b be real number such that A1: a < b;
  let t1,t2 be Point of Closed-Interval-TSpace(0,1);
 func P[01](a,b,t1,t2) -> map of
  Closed-Interval-TSpace(a,b),Closed-Interval-TSpace(0,1) means
:Def4: for s being Point of Closed-Interval-TSpace(a,b),
    r,r1,r2 being real number st
    s=r & r1=t1 & r2=t2 holds it.s = ((b-r)*r1 + (r-a)*r2)/(b-a);
 existence
  proof
    reconsider r1 = t1, r2 = t2 as Real by Lm3;
    reconsider a1 = a, b1 = b as Real by XREAL_0:def 1;
   deffunc U(Element of REAL) = ((b1-$1)*r1 + ($1-a1)*r2)/(b1-a1);
  consider PI being Function of REAL,REAL such that
   A2: for r being Real holds PI.r= U(r) from LambdaD;
    A3: dom(PI|[.a,b.]) =
        the carrier of Closed-Interval-TSpace(a,b)
       proof
        A4: [.a,b.] = REAL /\ [.a,b.] by XBOOLE_1:28;
           dom PI = REAL & dom(PI|[.a,b.]) = (dom PI) /\ [.a,b.]
                                           by FUNCT_2:def 1,RELAT_1:90;
        hence thesis by A1,A4,TOPMETR:25;
       end;
     A5: [.0,1.] = the carrier of Closed-Interval-TSpace(0,1)
                                                        by TOPMETR:25;
      rng(PI|[.a,b.]) c= the carrier of Closed-Interval-TSpace(0,1)
     proof
          now let y be set;
         assume A6: y in rng(PI|[.a,b.]);
          then y in PI.:[.a,b.] by RELAT_1:148;
          then consider x being set such that
               x in dom PI and A7: x in [.a,b.] and A8: y = PI.x by FUNCT_1:def
12;
          reconsider c = x as Real by A7;
              c in { p where p is Real : a <= p & p <= b} by A7,RCOMP_1:def 1;
          then A9: ex u being Real st u = c & a <= u & u <= b;

             r1 in [.0,1.] & r2 in [.0,1.] by A5;
          then r1 in { p where p is Real : 0 <= p & p <= 1} &
               r2 in { p where p is Real : 0 <= p & p <= 1} by RCOMP_1:def 1;
          then A10: (ex v1 being Real st v1 = r1 & 0 <= v1 & v1 <= 1) &
               (ex v2 being Real st v2 = r2 & 0 <= v2 & v2 <= 1);

             rng(PI|[.a,b.]) c= rng PI & rng PI c= REAL by FUNCT_1:76,RELSET_1:
12
;
          then rng(PI|[.a,b.]) c= REAL by XBOOLE_1:1;
          then reconsider d = y as Real by A6;
           A11: 0 < b - a by A1,SQUARE_1:11;
            A12: d = ((b - c)*r1 + (c - a)*r2)/(b-a) by A2,A8;
           A13: 0 <= b - c & 0 <= c - a by A9,SQUARE_1:12;
          then 0 <= (b - c)*r1 & 0 <= (c - a)*r2 by A10,REAL_2:121;
          then 0 + 0 <= (b - c)*r1 + (c - a)*r2 by REAL_1:55;
          then A14: 0 <= d by A11,A12,REAL_2:125;
             (b - c)*r1 <= b - c & (c - a)*r2 <= c - a by A10,A13,REAL_2:147;
          then (b - c)*r1 + (c - a)*r2 <= (b - c) + (c - a) by REAL_1:55;
          then (b - c)*r1 + (c - a)*r2 <= (b + - c) + (c - a) by XCMPLX_0:def 8
;
          then (b - c)*r1 + (c - a)*r2 <= b + (- c + (c - a)) by XCMPLX_1:1;
          then (b - c)*r1 + (c - a)*r2 <= b + (- c + (c + - a)) by XCMPLX_0:def
8
;
          then (b - c)*r1 + (c - a)*r2 <= b + ((- c + c) + - a) by XCMPLX_1:1;
          then (b - c)*r1 + (c - a)*r2 <= b + (0 + - a) by XCMPLX_0:def 6;
          then (b - c)*r1 + (c - a)*r2 <= b - a by XCMPLX_0:def 8;
          then d <= (b - a)/(b - a) & b - a <> 0 by A11,A12,REAL_1:73;
          then d <= 1 by XCMPLX_1:60;
          then y in { q where q is Real : 0 <= q & q <= 1} by A14;
         hence y in [.0,1.] by RCOMP_1:def 1;
        end;
      hence thesis by A5,TARSKI:def 3;
     end;
    then PI|[.a,b.] is Function
     of the carrier of Closed-Interval-TSpace(a,b),
        the carrier of Closed-Interval-TSpace(0,1)
        by A3,FUNCT_2:def 1,RELSET_1:11;
    then reconsider F = PI|[.a,b.] as map
     of Closed-Interval-TSpace(a,b),Closed-Interval-TSpace(0,1);
   take F;
   let s be Point of Closed-Interval-TSpace(a,b), r,r1,r2 be real number
   such that
      A15: s=r & r1=t1 & r2=t2;
A16: r is Real by XREAL_0:def 1;
       s in the carrier of Closed-Interval-TSpace(a,b) &
      the carrier of Closed-Interval-TSpace(a,b) = [.a,b.] by A1,TOPMETR:25;
   hence F.s = PI.r by A15,FUNCT_1:72
            .= ((b-r)*r1 + (r-a)*r2)/(b-a) by A2,A15,A16;
  end;
 uniqueness
  proof
   let F1, F2 be map of
       Closed-Interval-TSpace(a,b),Closed-Interval-TSpace(0,1);
   assume
    A17: for s being Point of Closed-Interval-TSpace(a,b),
       r,r1,r2 being real number st
         s=r & r1=t1 & r2=t2 holds F1.s = ((b-r)*r1 + (r-a)*r2)/(b-a);
   assume
    A18: for s being Point of Closed-Interval-TSpace(a,b),
  r,r1,r2 being real number st
         s=r & r1=t1 & r2=t2 holds F2.s = ((b-r)*r1 + (r-a)*r2)/(b-a);
      for s being Point of Closed-Interval-TSpace(a,b) holds F1.s = F2.s
     proof
      let s be Point of Closed-Interval-TSpace(a,b);
      reconsider r = s as Real by A1,Lm3;
      reconsider r1 = t1, r2 = t2 as Real by Lm3;
      thus F1.s = ((b-r)*r1 + (r-a)*r2)/(b-a) by A17
                .= F2.s by A18;
     end;
   hence F1 = F2 by FUNCT_2:113;
  end;
end;

theorem Th14:
 a < b implies
  for t1,t2 being Point of Closed-Interval-TSpace(0,1)
   for s being Point of Closed-Interval-TSpace(a,b), r,r1,r2 being Real st
    s=r & r1=t1 & r2=t2 holds
  P[01](a,b,t1,t2).s = ((r2 - r1)/(b-a))*r + (b*r1 -a*r2)/(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), r,r1,r2 be Real;
  assume s=r & r1=t1 & r2=t2;
  hence P[01](a,b,t1,t2).s = ((b-r)*r1 + (r-a)*r2)/(b-a) by A1,Def4
                  .= ((b*r1 - r*r1) + (r -a)*r2)/(b-a) by XCMPLX_1:40
                  .= ((b*r1 - r*r1) + (r*r2 -a*r2))/(b-a) by XCMPLX_1:40
                  .= ((b*r1 + - r*r1) + (r*r2 -a*r2))/(b-a) by XCMPLX_0:def 8
                  .= (b*r1 + (- r*r1 + (r*r2 -a*r2)))/(b-a) by XCMPLX_1:1
                  .= (b*r1 + (- r*r1 + (r*r2 + -a*r2)))/(b-a) by XCMPLX_0:def 8
                  .= (b*r1 + ((r*r2 + -r*r1) + -a*r2))/(b-a) by XCMPLX_1:1
                  .= (b*r1 + ((r*r2 - r*r1) + -a*r2))/(b-a) by XCMPLX_0:def 8
                  .= (b*r1 + (-a*r2 + r*(r2 - r1)))/(b-a) by XCMPLX_1:40
                  .= (r*(r2 - r1) + (b*r1 + -a*r2))/(b-a) by XCMPLX_1:1
                  .= (r*(r2 - r1) + (b*r1 -a*r2))/(b-a) by XCMPLX_0:def 8
                  .= (r*(r2 - r1))/(b-a) + (b*r1 -a*r2)/(b-a) by XCMPLX_1:63

               .= (r*(r2 - r1))* (1/(b-a)) + (b*r1 -a*r2)/(b-a) by XCMPLX_1:100
              .= ((r2 - r1)* (1/(b-a)))*r + (b*r1 -a*r2)/(b-a) by XCMPLX_1:4
              .= ((r2 - r1)/(b-a))*r + (b*r1 -a*r2)/(b-a) by XCMPLX_1:100;
 end;

theorem Th15:
 a < b implies
  for t1,t2 being Point of Closed-Interval-TSpace(0,1) holds
   P[01](a,b,t1,t2) is continuous map of
     Closed-Interval-TSpace(a,b),Closed-Interval-TSpace(0,1)
 proof
   assume A1: a < b;
  let t1,t2 be Point of Closed-Interval-TSpace(0,1);
   reconsider r1 = t1, r2 = t2 as Real by Lm3;
   reconsider a, b as Real by XREAL_0:def 1;
   deffunc U(Element of REAL) =
        ((r2 - r1)/(b-a))*$1 + (b*r1 -a*r2)/(b-a);
    consider P being Function of REAL,REAL such that
    A2: for r being Real holds P.r=  U(r) from LambdaD;
   reconsider f = P as map of R^1, R^1 by TOPMETR:24;
A3:    f is continuous by A2,TOPMETR:28;
      A4: 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 by A1,Lm3;
            assume A5: s = w;
            thus P[01](a,b,t1,t2).s
                  = ((r2 - r1)/(b-a))*r + (b*r1 -a*r2)/(b-a) by A1,Th14
                                   .= f.w by A2,A5;
           end;
    A6: [.a,b.] = the carrier of Closed-Interval-TSpace(a,b) by A1,TOPMETR:25;
      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 A6,TARSKI:def 3,TOPMETR:24;
        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
           A7: G0 is open and A8: G0 /\ [#] Closed-Interval-TSpace(0,1) = G
                                                              by TOPS_2:32;
        assume P[01](a,b,t1,t2).s in G;
         then f.w in G by A4;
         then f.w in G0 & f is_continuous_at w by A3,A8,TMAP_1:49,XBOOLE_0:def
3;
        then consider H0 being Subset of R^1 such that
          A9: H0 is open and A10: w in H0 and A11: f.:
H0 c= G0 by A7,TMAP_1:48;
           now
             A12: [#] Closed-Interval-TSpace(a,b) =
            the carrier of Closed-Interval-TSpace(a,b) by PRE_TOPC:12;
           then H0 /\ [#] Closed-Interval-TSpace(a,b)
    is Subset of Closed-Interval-TSpace(a,b) by XBOOLE_1:17;
           then reconsider H = H0 /\ [#] Closed-Interval-TSpace(a,b)
            as Subset of Closed-Interval-TSpace(a,b);
          take H;
          thus H is open by A9,TOPS_2:32;
          thus s in H by A10,A12,XBOOLE_0:def 3;
          thus P[01](a,b,t1,t2).:H c= G
                proof
                  let t be set;
                 assume t in P[01](a,b,t1,t2).:H;
                  then consider r be 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 12;
                  A15: r in the carrier of Closed-Interval-TSpace(a,b)
                                                  by A13;
                 reconsider r as Point of Closed-Interval-TSpace(a,b) by A13;
                  reconsider p = r as Point of R^1 by A6,TARSKI:def 3,TOPMETR:
24;
                     p in the carrier of R^1;
                  then p in [#] R^1 by PRE_TOPC:12;
                  then t=f.p & p in H0 & p in dom f
                                      by A4,A13,A14,TOPS_2:51,XBOOLE_0:def 3;
                  then A16: t in f.:H0 by FUNCT_1:def 12;
                   A17:  rng P[01](a,b,t1,t2) c= [#]
 Closed-Interval-TSpace(0,1) by TOPS_2:51;
                     r in dom P[01](a,b,t1,t2) by A12,A15,TOPS_2:51;
                  then t in P[01](a,b,t1,t2).:
(the carrier of Closed-Interval-TSpace(a,b))
                                                        by A14,FUNCT_1:def 12;
                  then t in rng P[01](a,b,t1,t2) by FUNCT_2:45;
                  hence thesis by A8,A11,A16,A17,XBOOLE_0:def 3;
                end;
         end;
        hence thesis;
       end;
      hence thesis by TMAP_1:48;
     end;
   hence thesis by TMAP_1:49;
 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;
  let t1,t2 be Point of Closed-Interval-TSpace(0,1);
   A2: a = (#)(a,b) by A1,Def1;
 reconsider r1 = t1, r2 = t2 as Real by Lm3;
   A3: b - a <> 0 by A1,SQUARE_1:11;
  thus P[01](a,b,t1,t2).(#)(a,b) = ((b-a)*r1 + (a-a)*r2)/(b-a) by A1,A2,Def4
                         .= ((b-a)*r1 + 0*r2)/(b-a) by XCMPLX_1:14
                         .= t1 by A3,XCMPLX_1:90;
      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
                      .= (0*r1 + (b-a)*r2)/(b-a) by XCMPLX_1:14
                      .= t2 by A3,XCMPLX_1:90;
 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 by Lm3;
       (#)(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 TMAP_1:92;
 end;

theorem Th18:
 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
  assume A1: a < b;
    then A2: b - a <> 0 by SQUARE_1:11;
  set L = L[01]((#)(a,b),(a,b)(#)), P = P[01](a,b,(#)(0,1),(0,1)(#));
   A3: 0 = (#)(0,1) & 1 = (0,1)(#) by Def1,Def2;
   A4: a = (#)(a,b) & b = (a,b)(#) by A1,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 by A1,Lm3;
      A5: P.c = ((b-r)*0 + (r-a)*1)/(b-a) by A1,A3,Def4
               .= (r-a)/(b-a);
     thus (L*P).c = L.(P.c) by FUNCT_2:21
            .= (1-((r-a)/(b-a)))*a + ((r-a)/(b-a))*b by A1,A4,A5,Def3
            .= ((1*(b-a)-(r-a))/(b-a))*a + ((r-a)/(b-a))*b by A2,XCMPLX_1:128
            .= ((b-r)/(b-a))*(a/1) + ((r-a)/(b-a))*b by XCMPLX_1:22
            .= ((b-r)*a)/(1*(b-a)) + ((r-a)/(b-a))*b by XCMPLX_1:77
            .= ((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:77
            .= ((b-r)*a + (r-a)*b)/(b-a) by XCMPLX_1:63
            .= ((a*b-a*r) + (r-a)*b)/(b-a) by XCMPLX_1:40
            .= ((b*r-a*b) + (a*b-a*r))/(b-a) by XCMPLX_1:40
            .= (b*r-a*r)/(b-a) by XCMPLX_1:39
            .= ((b-a)*r)/(b-a) by XCMPLX_1:40
            .= c by A2,XCMPLX_1:90;
    end;
  hence id Closed-Interval-TSpace(a,b) = L*P by TMAP_1:92;
     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 by Lm3;
      A6: L.c = (1-r)*a + r*b by A1,A4,Def3
              .= (1*a-r*a) + r*b by XCMPLX_1:40
              .= (r*b-r*a) + a by XCMPLX_1:30
              .= r*(b-a) + a by XCMPLX_1:40;
     thus (P*L).c = P.(L.c) by FUNCT_2:21
      .= ((b-(r*(b-a) + a))*0 + ((r*(b-a) + a)-a)*1)/(b-a) by A1,A3,A6,Def4
      .= (r*(b-a))/(b-a) by XCMPLX_1:26
      .= c by A2,XCMPLX_1:90;
    end;
  hence thesis by TMAP_1:92;
 end;

theorem Th19:
 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
  assume A1: a < b;
    then A2: b - a <> 0 by SQUARE_1:11;
  set L = L[01]((a,b)(#),(#)(a,b)), P = P[01](a,b,(0,1)(#),(#)(0,1));
   A3: 0 = (#)(0,1) & 1 = (0,1)(#) by Def1,Def2;
   A4: a = (#)(a,b) & b = (a,b)(#) by A1,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 by A1,Lm3;
      A5: P.c = ((b-r)*1 + (r-a)*0)/(b-a) by A1,A3,Def4
               .= (b-r)/(b-a);
     thus (L*P).c = L.(P.c) by FUNCT_2:21
            .= (1-((b-r)/(b-a)))*b + ((b-r)/(b-a))*a by A1,A4,A5,Def3
            .= ((1*(b-a)-(b-r))/(b-a))*b + ((b-r)/(b-a))*a by A2,XCMPLX_1:128
            .= (((r-b)+(b-a))/(b-a))*b + ((b-r)/(b-a))*a by XCMPLX_1:38
            .= ((r-a)/(b-a))*(b/1) + ((b-r)/(b-a))*a by XCMPLX_1:39
            .= ((r-a)*b)/(1*(b-a)) + ((b-r)/(b-a))*a by XCMPLX_1:77
            .= ((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:77
            .= ((r-a)*b + (b-r)*a)/(b-a) by XCMPLX_1:63
            .= ((b*r-b*a) + (b-r)*a)/(b-a) by XCMPLX_1:40
            .= ((b*r-a*b) + (a*b-a*r))/(b-a) by XCMPLX_1:40
            .= (b*r-a*r)/(b-a) by XCMPLX_1:39
            .= ((b-a)*r)/(b-a) by XCMPLX_1:40
            .= c by A2,XCMPLX_1:90;
    end;
  hence id Closed-Interval-TSpace(a,b) = L*P by TMAP_1:92;
     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 by Lm3;
      A6: L.c = (1-r)*b + r*a by A1,A4,Def3
              .= (1*b-r*b) + r*a by XCMPLX_1:40
              .= (r*a-r*b) + b by XCMPLX_1:30
              .= r*(a-b) + b by XCMPLX_1:40;
     thus (P*L).c = P.(L.c) by FUNCT_2:21
      .= ((b-(r*(a-b) + b))*1 + ((r*(a-b) + b)-a)*0)/(b-a) by A1,A3,A6,Def4
      .= (-(r*(a-b) + b) + b)/(b-a) by XCMPLX_0:def 8
      .= ((-(r*(a-b)) - b) + b)/(b-a) by XCMPLX_1:161
      .= (-(r*(a-b)))/(b-a) by XCMPLX_1:27
      .= (r*(-(a-b)))/(b-a) by XCMPLX_1:175
      .= (r*(b-a))/(b-a) by XCMPLX_1:143
      .= c by A2,XCMPLX_1:90;
    end;
  hence thesis by TMAP_1:92;
 end;

theorem Th20:
 a < b implies
   L[01]((#)(a,b),(a,b)(#)) is_homeomorphism &
      L[01]((#)(a,b),(a,b)(#))" = P[01](a,b,(#)(0,1),(0,1)(#)) &
   P[01](a,b,(#)(0,1),(0,1)(#)) is_homeomorphism &
      P[01](a,b,(#)(0,1),(0,1)(#))" = L[01]((#)(a,b),(a,b)(#))
 proof
  assume A1: a < b;
   reconsider A = the carrier of Closed-Interval-TSpace(a,b),
              B = the carrier of Closed-Interval-TSpace(0,1) as set;
   set L = L[01]((#)(a,b),(a,b)(#)),
       P = P[01](a,b,(#)(0,1),(0,1)(#));
  reconsider L0 = L as Function of B,A;
  reconsider P0 = P as Function of A,B;
   A2: id (the carrier of Closed-Interval-TSpace(0,1)) =
              id Closed-Interval-TSpace(0,1) by GRCAT_1:def 11
           .= P * L by A1,Th18;
  then A3: L is one-to-one &
    rng P = the carrier of Closed-Interval-TSpace(0,1) by FUNCT_2:29;
  then A4: rng P = [#](Closed-Interval-TSpace(0,1)) by PRE_TOPC:12;
   A5: id (the carrier of Closed-Interval-TSpace(a,b)) =
              id Closed-Interval-TSpace(a,b) by GRCAT_1:def 11
           .= L * P by A1,Th18;
  then A6: P is one-to-one &
      rng L = the carrier of Closed-Interval-TSpace(a,b) by FUNCT_2:29;
  then A7: rng L = [#](Closed-Interval-TSpace(a,b)) by PRE_TOPC:12;
    dom L = the carrier of Closed-Interval-TSpace(0,1) by FUNCT_2:def 1;
then A8: dom L = [#]Closed-Interval-TSpace(0,1) by PRE_TOPC:12;
  A9: L0" = L" by A3,A7,TOPS_2:def 4;
    dom P = the carrier of Closed-Interval-TSpace(a,b) by FUNCT_2:def 1;
then A10: dom P = [#]Closed-Interval-TSpace(a,b) by PRE_TOPC:12;
  A11: P0" = P" by A4,A6,TOPS_2:def 4;
  A12: P = L" by A2,A3,A6,A9,FUNCT_2:36;
  A13: L = P" by A3,A5,A6,A11,FUNCT_2:36;
    A14: L is continuous map of
      Closed-Interval-TSpace(0,1),Closed-Interval-TSpace(a,b) by A1,Th11;
   A15: L is continuous by A1,Th11;
    A16: P is continuous map of
      Closed-Interval-TSpace(a,b),Closed-Interval-TSpace(0,1) by A1,Th15;
   A17: P is continuous by A1,Th15;
  thus L[01]((#)(a,b),(a,b)(#)) is_homeomorphism
            by A3,A7,A8,A12,A15,A16,TOPS_2:def 5;
  thus L[01]((#)(a,b),(a,b)(#))" = P[01](a,b,(#)(0,1),(0,1)(#)
) by A2,A3,A6,A9,FUNCT_2:36;
  thus P[01](a,b,(#)(0,1),(0,1)(#)) is_homeomorphism
            by A4,A6,A10,A13,A14,A17,TOPS_2:def 5;
  thus P[01](a,b,(#)(0,1),(0,1)(#))" = L[01]((#)(a,b),(a,b)(#)
) by A3,A5,A6,A11,FUNCT_2:36;
 end;

theorem
   a < b implies
   L[01]((a,b)(#),(#)(a,b)) is_homeomorphism &
      L[01]((a,b)(#),(#)(a,b))" = P[01](a,b,(0,1)(#),(#)(0,1)) &
   P[01](a,b,(0,1)(#),(#)(0,1)) is_homeomorphism &
      P[01](a,b,(0,1)(#),(#)(0,1))" = L[01]((a,b)(#),(#)(a,b))
 proof
  assume A1: a < b;
   reconsider A = the carrier of Closed-Interval-TSpace(a,b),
              B = the carrier of Closed-Interval-TSpace(0,1) as set;
   set L = L[01]((a,b)(#),(#)(a,b)),
       P = P[01](a,b,(0,1)(#),(#)(0,1));
  reconsider L0 = L as Function of B,A;
  reconsider P0 = P as Function of A,B;
   A2: id (the carrier of Closed-Interval-TSpace(0,1)) =
              id Closed-Interval-TSpace(0,1) by GRCAT_1:def 11
           .= P * L by A1,Th19;
  then A3: L is one-to-one &
    rng P = the carrier of Closed-Interval-TSpace(0,1) by FUNCT_2:29;
  then A4: rng P = [#](Closed-Interval-TSpace(0,1)) by PRE_TOPC:12;
   A5: id (the carrier of Closed-Interval-TSpace(a,b)) =
              id Closed-Interval-TSpace(a,b) by GRCAT_1:def 11
           .= L * P by A1,Th19;
  then A6: P is one-to-one &
      rng L = the carrier of Closed-Interval-TSpace(a,b) by FUNCT_2:29;
  then A7: rng L = [#](Closed-Interval-TSpace(a,b)) by PRE_TOPC:12;
    dom L = the carrier of Closed-Interval-TSpace(0,1) by FUNCT_2:def 1;
then A8: dom L = [#]Closed-Interval-TSpace(0,1) by PRE_TOPC:12;
  A9: L0" = L" by A3,A7,TOPS_2:def 4;
    dom P = the carrier of Closed-Interval-TSpace(a,b) by FUNCT_2:def 1;
then A10: dom P = [#]Closed-Interval-TSpace(a,b) by PRE_TOPC:12;
   A11: P0" = P" by A4,A6,TOPS_2:def 4;
  A12: P = L" by A2,A3,A6,A9,FUNCT_2:36;
  A13: L = P" by A3,A5,A6,A11,FUNCT_2:36;
    A14: L is continuous map of
      Closed-Interval-TSpace(0,1),Closed-Interval-TSpace(a,b) by A1,Th11;
   A15: L is continuous by A1,Th11;
    A16: P is continuous map of
      Closed-Interval-TSpace(a,b),Closed-Interval-TSpace(0,1) by A1,Th15;
   A17: P is continuous by A1,Th15;
  thus L[01]((a,b)(#),(#)(a,b)) is_homeomorphism
                      by A3,A7,A8,A12,A15,A16,TOPS_2:def 5;
  thus L[01]((a,b)(#),(#)(a,b))" = P[01](a,b,(0,1)(#),(#)
(0,1)) by A2,A3,A6,A9,FUNCT_2:36;
  thus P[01](a,b,(0,1)(#),(#)(0,1)) is_homeomorphism
                      by A4,A6,A10,A13,A14,A17,TOPS_2:def 5;
  thus P[01](a,b,(0,1)(#),(#)(0,1))" = L[01]((a,b)(#),(#)
(a,b)) by A3,A5,A6,A11,FUNCT_2:36;
 end;

begin
:: 3. Connectedness of Intervals and Brouwer Fixed Point Theorem for Intervals.

theorem Th22:
 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] & B <> {}I[01] and
                 A3: A is closed and A4: B is closed;
    assume A5: A misses B;
     A6: [#]I[01] = [.0,1.] by BORSUK_1:83,PRE_TOPC:12;
     A7: I[01] is closed SubSpace of R^1 by Th5,TOPMETR:27;
     reconsider P = A, Q = B as Subset of REAL by BORSUK_1:83,XBOOLE_1:1;
       A8: the carrier of RealSpace = the carrier of TopSpaceMetr(RealSpace)
                                                               by TOPMETR:16;
     then reconsider A0 = P, B0 = Q as Subset of R^1 by METRIC_1:def 14,TOPMETR
:def 7;
       A9: A0 is closed & B0 is closed by A3,A4,A7,TSEP_1:12;
     consider x being Element of P;
     reconsider x as Real by A2,TARSKI:def 3;
         A10: now
               take x;
               thus x in P by A2;
              end;
     consider x being Element of Q;
     reconsider x as Real by A2,TARSKI:def 3;
A11: now
       take x;
       thus x in Q by A2;
      end;
        0 in {w where w is Real : 0<=w & w<=1};
      then A12: 0 in [.0,1.] by RCOMP_1:def 1;
        A13: P is bounded_below
              proof
                 now
                take p = 0;
                 let r be real number;
                assume r in P;
                 then r in [.0,1.] by BORSUK_1:83;
                 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 p <= r;
               end;
               hence thesis by SEQ_4:def 2;
              end;
        A14: Q is bounded_below
              proof
                 now
                take p = 0;
                 let r be real number;
                assume r in Q;
                 then r in [.0,1.] by BORSUK_1:83;
                 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 p <= r;
               end;
               hence thesis by SEQ_4:def 2;
              end;
      now per cases by A1,A6,A12,XBOOLE_0:def 2;
     suppose 0 in P;
      then A15: not 0 in Q by A5,XBOOLE_0:3;
       set l = lower_bound Q;
       reconsider m = l as Point of RealSpace by METRIC_1:def 14;
       reconsider t = m as Point of R^1 by TOPMETR:16,def 7;
       reconsider B00 = B0` as Subset of R^1;
         A16: l in Q
              proof
               assume not l in Q;
                then t in B00 & B00 is open by A9,SUBSET_1:50,TOPS_1:29;
                then consider s being real number such that
                  A17: s > 0 and A18: Ball(m,s) c= B0` by TOPMETR:22,def 7;
               consider r being real number such that
                  A19: r in Q and A20: r < l+s by A11,A14,A17,SEQ_4:def 5;
               reconsider r as Real by XREAL_0:def 1;
                reconsider rm = r as Point of RealSpace by METRIC_1:def 14;
                   l <= r by A14,A19,SEQ_4:def 5;
                then l - r <= 0 by REAL_2:106;
                then -s < -(l - r) by A17,REAL_1:50;
                then -s < r - l & r - l < s by A20,REAL_1:84,XCMPLX_1:143;
                then abs(r - l) < s by SEQ_2:9;
                then (the distance of RealSpace).(rm,m) < s
                             by METRIC_1:def 13,def 14;
                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:18;
                hence contradiction by A18,A19,SUBSET_1:54;
              end;
           then l in [.0,1.] by BORSUK_1:83;
           then l in {u where u is Real : 0<=u & u<=1} by RCOMP_1:def 1;
           then A21:ex u0 being Real st u0 = l & 0<=u0 & u0<=1;
      set W = {w where w is Real : 0<=w & w<l};
          now let x be set;
         assume x in W;
          then consider w0 being Real such that A22: w0 = x & 0<=w0 & w0<l;
             w0 <= 1 by A21,A22,AXIOMS:22;
           then w0 in {u where u is Real : 0<=u & u<=1} by A22;
           then w0 in P \/ Q by A1,A6,RCOMP_1:def 1;
           then w0 in P or w0 in Q by XBOOLE_0:def 2;
         hence x in P by A14,A22,SEQ_4:def 5;
        end;
       then A23: W c= P by TARSKI:def 3;
       then reconsider D = W as Subset of R^1 by A8,METRIC_1:def
14,TOPMETR:def 7,XBOOLE_1:1;
        A24: t in Cl D
              proof
                 now let G be Subset of R^1;
                assume A25: G is open;
                assume t in G;
                 then consider e being real number such that
                   A26: e > 0 and A27: Ball(m,e) c= G by A25,TOPMETR:22,def 7;
                   reconsider e as Element of REAL by XREAL_0:def 1;
                   A28: e*(1/2) < e*1 by A26,REAL_1:70;
                   then A29: (e*1)/2 < e by XCMPLX_1:75;
                  set e0 = max(0,l - (e/2));
                   A30: 0 <= e0 by SQUARE_1:46;
                   A31: e0 = 0 or e0 = l - (e/2) by SQUARE_1:49;
                          now assume A32: e0 >= l;
                         then e0 <> 0 & e/2 > 0
                         by A15,A16,A21,A26,REAL_1:def 5,REAL_2:127;
                         hence contradiction by A31,A32,SQUARE_1:29;
                        end;
                   then A33: e0 in W by A30;
                    reconsider e1 = e0 as Point of RealSpace
                      by METRIC_1:def 14;
                      now per cases by SQUARE_1:49;
                     suppose A34: e0 = 0;
                      then l - (e/2) <= 0 by SQUARE_1:46;
                      then l <= e/2 by SQUARE_1:11;
                      then l < e & abs l = l by A21,A29,ABSVALUE:def 1,AXIOMS:
22;
                      hence abs(l - e0) < e by A34;
                     suppose e0 = l - (e/2);
                       then l - e0 = e/2 & 2 > 0 by XCMPLX_1:18;
                       then l - e0 < e & l - e0 > 0 by A26,A28,REAL_2:127,
XCMPLX_1:75;
                      hence abs(l - e0) < e by ABSVALUE:def 1;
                    end;
                   then (the distance of RealSpace).(m,e1) < e
                                                  by METRIC_1:def 13,def 14;
                   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 e1 in Ball(m,e) by METRIC_1:18;
                   hence D meets G by A27,A33,XBOOLE_0:3;
               end;
               hence thesis by PRE_TOPC:54;
              end;
           Cl D c= Cl A0 & Cl A0 = A0 by A9,A23,PRE_TOPC:49,52;
       hence contradiction by A5,A16,A24,XBOOLE_0:3;
     suppose 0 in Q;
      then A35: not 0 in P by A5,XBOOLE_0:3;
       set l = lower_bound P;
       reconsider m = l as Point of RealSpace by METRIC_1:def 14;
       reconsider t = m as Point of R^1 by TOPMETR:16,def 7;
       reconsider A00 = A0` as Subset of R^1;
         A36: l in P
              proof
               assume not l in P;
                then t in A00 & A00 is open by A9,SUBSET_1:50,TOPS_1:29;
                then consider s being real number such that
                  A37: s > 0 and A38: Ball(m,s) c= A0` by TOPMETR:22,def 7;
               consider r being real number such that
                  A39: r in P and A40: r < l+s by A10,A13,A37,SEQ_4:def 5;
               reconsider r as Real by XREAL_0:def 1;
               reconsider rm = r as Point of RealSpace by METRIC_1:def 14;
                   l <= r by A13,A39,SEQ_4:def 5;
                then l - r <= 0 by REAL_2:106;
                then -s < -(l - r) by A37,REAL_1:50;
                then -s < r - l & r - l < s by A40,REAL_1:84,XCMPLX_1:143;
                then abs(r - l) < s by SEQ_2:9;
                 then (real_dist).(r,l) < s by METRIC_1:def 13;
                then dist(rm,m) < s by METRIC_1:def 1,def 14;
                then rm in {q where q is Element of RealSpace
                                                              : dist(m,q)<s};
                then rm in Ball(m,s) by METRIC_1:18;
                hence contradiction by A38,A39,SUBSET_1:54;
              end;
           then l in [.0,1.] by BORSUK_1:83;
           then l in {u where u is Real : 0<=u & u<=1} by RCOMP_1:def 1;
           then A41:ex u0 being Real st u0 = l & 0<=u0 & u0<=1;
      set W = {w where w is Real : 0<=w & w<l};
          now let x be set;
         assume x in W;
          then consider w0 being Real such that A42: w0 = x & 0<=w0 & w0<l;
             w0 <= 1 by A41,A42,AXIOMS:22;
           then w0 in {u where u is Real : 0<=u & u<=1} by A42;
           then w0 in P \/ Q by A1,A6,RCOMP_1:def 1;
           then w0 in P or w0 in Q by XBOOLE_0:def 2;
         hence x in Q by A13,A42,SEQ_4:def 5;
        end;
       then A43: W c= Q by TARSKI:def 3;
       then reconsider D = W as Subset of R^1 by A8,METRIC_1:def
14,TOPMETR:def 7,XBOOLE_1:1;
        A44: t in Cl D
              proof
                 now let G be Subset of R^1;
                assume A45: G is open;
                assume t in G;
                 then consider e being real number such that
                   A46: e > 0 and A47: Ball(m,e) c= G by A45,TOPMETR:22,def 7;
                   reconsider e as Real by XREAL_0:def 1;
                   A48: e*(1/2) < e*1 by A46,REAL_1:70;
                   then A49: (e*1)/2 < e by XCMPLX_1:75;
                  set e0 = max(0,l - (e/2));
                   A50: 0 <= e0 by SQUARE_1:46;
                   A51: e0 = 0 or e0 = l - (e/2) by SQUARE_1:49;
                          now assume A52: e0 >= l;
                         then e0 <> 0 & e/2 > 0 by A35,A36,A41,A46,REAL_1:def 5
,REAL_2:127;
                         hence contradiction by A51,A52,SQUARE_1:29;
                        end;
                   then A53: e0 in W by A50;
                   reconsider e1 = e0 as Point of RealSpace by METRIC_1:def 14;
                      now per cases by SQUARE_1:49;
                     suppose A54: e0 = 0;
                      then l - (e/2) <= 0 by SQUARE_1:46;
                      then l <= e/2 by SQUARE_1:11;
                      then l < e & abs l = l by A41,A49,ABSVALUE:def 1,AXIOMS:
22;
                      hence abs(l - e0) < e by A54;
                     suppose e0 = l - (e/2);
                       then l - e0 = e/2 & 2 > 0 by XCMPLX_1:18;
                       then l - e0 < e & l - e0 > 0 by A46,A48,REAL_2:127,
XCMPLX_1:75;
                      hence abs(l - e0) < e by ABSVALUE:def 1;
                    end;
                   then (real_dist).(l,e0) < e by METRIC_1:def 13;
                   then dist(m,e1) < e by METRIC_1:def 1,def 14;
                   then e1 in {z where z is Element of
                                                 RealSpace : dist(m,z)<e};
                   then e1 in Ball(m,e) by METRIC_1:18;
                   hence D meets G by A47,A53,XBOOLE_0:3;
               end;
               hence thesis by PRE_TOPC:54;
              end;
           Cl D c= Cl B0 & Cl B0 = B0 by A9,A43,PRE_TOPC:49,52;
       hence contradiction by A5,A36,A44,XBOOLE_0:3;
    end;
    hence contradiction;
   end;
  hence thesis by CONNSP_1:11;
end;

theorem
   a <= b implies Closed-Interval-TSpace(a,b) is connected
 proof
  assume A1: a <= b;
     now per cases by A1,REAL_1:def 5;
    suppose A2: a < b;
     set A = the carrier of Closed-Interval-TSpace(0,1);
        A3: A = [#](Closed-Interval-TSpace(0,1)) by PRE_TOPC:12;
         L[01]((#)(a,b),(a,b)(#)) is_homeomorphism by A2,Th20;
      then A4: 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;
           L[01]((#)(a,b),(a,b)(#)).:(A) = rng L[01]((#)(a,b),(a,b)(#)
) by FUNCT_2:45;
     hence Closed-Interval-TSpace(a,b) is connected by A3,A4,Th22,CONNSP_1:15,
TOPMETR:27;
    suppose A5: a = b;
     then [.a,b.] = {a} & a = (#)(a,b) by Def1,RCOMP_1:14;
     then the carrier of Closed-Interval-TSpace(a,b) = {(#)
(a,b)} by A5,TOPMETR:25;
     then [#] Closed-Interval-TSpace(a,b) = {(#)(a,b)} &
                      {(#)(a,b)} is connected by CONNSP_1:29,PRE_TOPC:12;
     hence Closed-Interval-TSpace(a,b) is connected by CONNSP_1:28;
   end;
  hence thesis;
 end;

theorem Th24:
 for f being continuous map of I[01],I[01]
  ex x being Point of I[01] st f.x = x
 proof
   let f be continuous map of I[01],I[01];
    assume A1: for x being Point of I[01] holds f.x <> x;
    A2: Closed-Interval-TSpace(0,1) =
               TopSpaceMetr(Closed-Interval-MSpace(0,1)) by TOPMETR:def 8;
        A3: the carrier of Closed-Interval-MSpace(0,1) = [.0,1.]
                                                         by TOPMETR:14;
    reconsider F = f as Function of [.0,1.], [.0,1.] by BORSUK_1:83;
     A4: [.0,1.] = {q where q is Real : 0<=q & q<=1 } by RCOMP_1:def 1;
    set A = {a where a is Real : a in [.0,1.] & F.a in [.0,a.]},
        B = {b where b is Real : b in [.0,1.] & F.b in [.b,1.]};
        A c= REAL
      proof
         let x be set;
         assume x in A;
         then ex a being Real st a = x & a in [.0,1.] & F.a in [.0,a.];
         hence x in REAL;
      end;
    then reconsider A as Subset of REAL;
        B c= REAL
      proof
         let x be set;
         assume x in B;
         then ex b being Real st b = x & b in [.0,1.] & F.b in [.b,1.];
         hence x in REAL;
      end;
    then reconsider B as Subset of REAL;
    A5: A c= [.0,1.]
     proof
        let x be set;
        assume A6: x in A;
        then reconsider x as Real;
          ex a0 being Real st a0 = x & a0 in [.0,1.] & F.a0 in [.0,a0.] by A6;
        hence thesis;
     end;
    A7: B c= [.0,1.]
     proof
        let x be set;
        assume A8: 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 A8;
        hence thesis;
     end;
    A9: [.0,1.] <> {} by RCOMP_1:15;
    A10: A \/ B = [.0,1.]
     proof
       A11: A \/ B c= [.0,1.] by A5,A7,XBOOLE_1:8;
        [.0,1.] c= A \/ B
       proof
          let x be set;
          assume A12: x in [.0,1.];
          then reconsider y = x as Real;
             ex p being Real st p = y & 0<=p & p<=1 by A4,A12;
          then A13: [.0,1.] = [.0,y.] \/ [.y,1.] by Th2;
          A14: [.0,1.] = dom F & rng F c= [.0,1.]
          by A9,FUNCT_2:def 1,RELSET_1:12;
          then A15: F.y in rng F by A12,FUNCT_1:def 5;
            now per cases by A13,A14,A15,XBOOLE_0:def 2;
           suppose F.y in [.0,y.];
            then y in A & A c= A \/ B by A12,XBOOLE_1:7;
            hence y in A \/ B;
           suppose F.y in [.y,1.];
            then y in B & B c= A \/ B by A12,XBOOLE_1:7;
            hence y in A \/ B;
          end;
          hence thesis;
       end;
      hence thesis by A11,XBOOLE_0:def 10;
     end;
A16:    1 in A
     proof
        1 in {w where w is Real : 0<=w & w<=1};
      then A17: 1 in [.0,1.] by RCOMP_1:def 1;
      A18: [.0,1.] = dom F & rng F c= [.0,1.] by A9,FUNCT_2:def 1,RELSET_1:12;
      then F.1 in rng F by A17,FUNCT_1:def 5;
      hence thesis by A17,A18;
     end;
A19:    0 in B
     proof
        0 in {w where w is Real : 0<=w & w<=1};
      then A20: 0 in [.0,1.] by RCOMP_1:def 1;
      A21: [.0,1.] = dom F & rng F c= [.0,1.] by A9,FUNCT_2:def 1,RELSET_1:12;
      then F.0 in rng F by A20,FUNCT_1:def 5;
      hence thesis by A20,A21;
     end;
    A22: A /\ B = {}
     proof
      assume A23: A /\ B <> {};
      consider x being Element of A /\ B;
      A24: x in A by A23,XBOOLE_0:def 3;
      then A25: ex z being Real st z = x & z in [.0,1.] & F.z in [.0,z.];
      reconsider x as Real by A24;
        x in B by A23,XBOOLE_0:def 3;
      then ex b0 being Real st b0 = x & b0 in [.0,1.] & F.b0 in [.b0,1.];
      then A26: F.x in [.0,x.] /\ [.x,1.] by A25,XBOOLE_0:def 3;
        x in {q where q is Real : 0<=q & q<=1 } by A25,RCOMP_1:def 1;
      then ex u being Real st u = x & 0<=u & u<=1;
      then F.x in {x} by A26,TOPMETR2:1;
      then F.x = x by TARSKI:def 1;
      hence contradiction by A1,A25,BORSUK_1:83;
     end;
then A27: A misses B by XBOOLE_0:def 7;
      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 A5,A7,BORSUK_1:83;
     take P,Q;
     thus A28: [#]I[01] = P \/ Q by A10,BORSUK_1:83,PRE_TOPC:12;
     thus P <> {}I[01] & Q <> {}I[01] by A16,A19;
     thus P is closed
      proof
       assume not P is closed;
       then A29: Cl P <> P by PRE_TOPC:52;
       A30: (Cl P) /\ Q <> {}
          proof
           assume (Cl P) /\ Q = {}; then (Cl P) misses Q by XBOOLE_0:def 7;
            then A31: Cl P c= Q` & P c= Cl P by PRE_TOPC:21,48;
              P = [#]I[01] \ Q by A27,A28,PRE_TOPC:25
                  .= Q` by PRE_TOPC:17;
           hence contradiction by A29,A31,XBOOLE_0:def 10;
          end;
        consider z being Element of (Cl P) /\ Q;
          A32: z in Cl P & z in Q by A30,XBOOLE_0:def 3;
        then reconsider z as Point of I[01];
        reconsider t0 = z as Real by A32;
A33:    ex c being Real st c = t0 & c in [.0,1.] & F.c in [.c,1.] by A32;
        then A34: 0 <= t0 & t0 <= 1 by Lm2;
        reconsider s0 = F.t0 as Real by A33;
            t0 <= s0 by A33,A34,Lm2;
        then A35: 0 <= s0 - t0 by SQUARE_1:12;
        reconsider m = z, n = f.z as Point of Closed-Interval-MSpace(0,1)
           by BORSUK_1:83,TOPMETR:14;
       set r = (s0 - t0) * 2";
          s0 <> t0 by A1;
        then A36: s0 - t0 <> 0 by XCMPLX_1:15;
        then 0 / 2 < (s0 - t0) / 2 & 0 <> 2 by A35,REAL_1:73;
        then A37: 0 * 2" < r by XCMPLX_0:def 9;
        A38: r < (s0 - t0) * 1 by A35,A36,REAL_1:70;
             A39: (s0 - t0) = (s0 - t0) * (2" * 2)
                           .= 2 * r by XCMPLX_1:4
                           .= r + r by XCMPLX_1:11;
            A40: t0 + r = - (0 + - t0) + r
                        .= - ((- s0 + s0) + - t0) + r by XCMPLX_0:def 6
                        .= - (- s0 + (s0 + - t0)) + r by XCMPLX_1:1
                        .= - (- s0 + (r + r)) + r by A39,XCMPLX_0:def 8
                        .= (- (- s0) + (- (r + r))) + r by XCMPLX_1:140
                        .= (s0 + (- r + (- r))) + r by XCMPLX_1:140
                        .= ((s0 + (- r)) + (- r)) + r by XCMPLX_1:1
                        .= (s0 + - r) + ((- r) + r) by XCMPLX_1:1
                        .= (s0 + - r) + 0 by XCMPLX_0:def 6
                        .= s0 - r by XCMPLX_0:def 8;
          Ball(n,r) is Subset of I[01] by BORSUK_1:83,TOPMETR:14
;
        then reconsider W = Ball(n,r) as Subset of I[01]
          ;
        A41: Ball(n,r) c= [.t0,1.]
          proof
           let x be set;
           assume A42: x in Ball(n,r);
            then x in [.0,1.] by A3;
            then reconsider t = x as Real;
            reconsider u = x as Point of Closed-Interval-MSpace(0,1)
                   by A42;
               Ball(n,r)=
               {q where q is Element of
                   Closed-Interval-MSpace(0,1):dist(n,q)<r} by METRIC_1:18;
            then ex p being Element of
                   Closed-Interval-MSpace(0,1) st
                          p = u & dist(n,p)<r by A42;
            then abs(s0 - t) < r by HEINE:1;
            then abs(s0 - t) < s0 - t0 & s0 - t <= abs(s0 - t)
                                         by A38,ABSVALUE:11,AXIOMS:22;
            then s0 - t < s0 - t0 by AXIOMS:22;
            then A43: t0 <= t by REAL_2:106;
               t <= 1 by A3,A42,Lm2;
            then t in {q where q is Real : t0<=q & q<=1 } by A43;
           hence x in [.t0,1.] by RCOMP_1:def 1;
          end;
          A44: f.z in W by A37,TBSP_1:16;
           W is open & f is_continuous_at z by A2,TMAP_1:55,TOPMETR:21,27;
        then consider V being Subset of I[01] such that
          A45: V is open and A46: z in V and A47: f.:V c= W by A44,TMAP_1:48;
       consider s being real number such that A48: s > 0 and
       A49: Ball(m,s) c= V by A2,A45,A46,TOPMETR:22,27;
       reconsider s as Real by XREAL_0:def 1;
       set r0 = min(s,r);
              A50: r0 > 0 by A37,A48,SQUARE_1:38;
              A51: r0 <= r by SQUARE_1:35;
              A52: r0 <= s by SQUARE_1:35;
          Ball(m,r0) is Subset of I[01]
          by BORSUK_1:83,TOPMETR:14;
        then reconsider W0 = Ball(m,r0) as Subset of I[01];
          A53: W0 is open by A2,TOPMETR:21,27;
          A54: z in W0 by A50,TBSP_1:16;
           Ball(m,r0) c= Ball(m,s) by A52,PCOMPS_1:1;
        then A55: W0 c= V by A49,XBOOLE_1:1;
          P meets W0 by A32,A53,A54,PRE_TOPC:54;
        then A56: P /\ W0 <> {}I[01] by XBOOLE_0:def 7;
        consider w being Element of P /\ W0;
          A57: w in P & w in W0 by A56,XBOOLE_0:def 3;
        then reconsider w as Point of
         Closed-Interval-MSpace(0,1);
       reconsider w1 = w as Point of I[01] by A57;
       reconsider d = w1 as Real by A57;
           Ball(m,r0) =
           {q where q is Element of
              Closed-Interval-MSpace(0,1):dist(m,q)<r0} by METRIC_1:18;
        then ex p being Element of
            Closed-Interval-MSpace(0,1) st p = w & dist(m,p)<r0 by A57;
        then dist(w,m) < r by A51,AXIOMS:22;
        then abs(d - t0) < r & d - t0 <= abs(d - t0) by ABSVALUE:11,HEINE:1;
        then d - t0 < r by AXIOMS:22;
        then A58: d < s0 - r by A40,REAL_1:84;
      A59: Ball(n,r) c= [.d,1.]
       proof
        let x be set;
        assume A60: x in Ball(n,r);
         then A61: x in [.0,1.] by A3;
        reconsider v = x as Point of Closed-Interval-MSpace(0,1)
                                                           by A60;
             reconsider t = x as Real by A61;
         A62: t0 <= t & t <= 1 by A34,A41,A60,Lm2;
            Ball(n,r)=
            {q where q is Element of
                 Closed-Interval-MSpace(0,1):dist(n,q)<r} by METRIC_1:18;
         then ex p being Element of
               Closed-Interval-MSpace(0,1) st p = v & dist(n,p)<r by A60;
         then A63: abs(s0 - t) < r by HEINE:1;
          now per cases;
         suppose t <= s0;
          then 0 <= s0 - t by SQUARE_1:12;
          then s0 - t < r by A63,ABSVALUE:def 1;
          then s0 < r + t by REAL_1:84;
          then s0 - r < t by REAL_1:84;
          hence d < t by A58,AXIOMS:22;
         suppose A64: s0 < t;
              s0 - r < s0 by A37,REAL_2:174;
           then d < s0 by A58,AXIOMS:22;
          hence d < t by A64,AXIOMS:22;
        end;
         then t in {w0 where w0 is Real : d<=w0 & w0<=1} by A62;
        hence thesis by RCOMP_1:def 1;
       end;
         F.d in [.d,1.]
       proof
           f.w1 in f.:V by A55,A57,FUNCT_2:43;
         then f.w1 in W by A47;
         hence thesis by A59;
       end;
        then d in A & d in B by A56,BORSUK_1:83,XBOOLE_0:def 3;
       hence contradiction by A27,XBOOLE_0:3;
      end;
     thus Q is closed
      proof
       assume not Q is closed;
       then A65: Cl Q <> Q by PRE_TOPC:52;
       A66: (Cl Q) /\ P <> {}
          proof
           assume (Cl Q) /\ P = {}; then (Cl Q) misses P by XBOOLE_0:def 7;
            then A67: Cl Q c= P` & Q c= Cl Q by PRE_TOPC:21,48;
              Q = [#]I[01] \ P by A27,A28,PRE_TOPC:25
                  .= P` by PRE_TOPC:17;
           hence contradiction by A65,A67,XBOOLE_0:def 10;
          end;
        consider z being Element of (Cl Q) /\ P;
          A68: z in Cl Q & z in P by A66,XBOOLE_0:def 3;
        then reconsider z as Point of I[01];
       reconsider t0 = z as Real by A68;
A69:    ex c being Real st c = t0 & c in [.0,1.] & F.c in [.0,c.] by A68;
        then A70: 0 <= t0 & t0 <= 1 by Lm2;
        reconsider s0 = F.t0 as Real by A69;
           s0 <= t0 by A69,A70,Lm2;
        then A71: 0 <= t0 - s0 by SQUARE_1:12;
        reconsider m = z, n = f.z as Point of Closed-Interval-MSpace(0,1)
           by BORSUK_1:83,TOPMETR:14;
       set r = (t0 - s0) * 2";
           t0 <> s0 by A1;
        then A72: t0 - s0 <> 0 by XCMPLX_1:15;
        then 0 / 2 < (t0 - s0) / 2 & 0 <> 2 by A71,REAL_1:73;
        then A73: 0 * 2" < r by XCMPLX_0:def 9;
        A74: r < (t0 - s0) * 1 by A71,A72,REAL_1:70;
             A75: (t0 - s0) = (t0 - s0) * (2" * 2)
                           .= 2 * r by XCMPLX_1:4
                           .= r + r by XCMPLX_1:11;
            A76: s0 + r = - (0 + - s0) + r
                        .= - ((- t0 + t0) + - s0) + r by XCMPLX_0:def 6
                        .= - (- t0 + (t0 + - s0)) + r by XCMPLX_1:1
                        .= - (- t0 + (r + r)) + r by A75,XCMPLX_0:def 8
                        .= (- (- t0) + (- (r + r))) + r by XCMPLX_1:140
                        .= (t0 + (- r + (- r))) + r by XCMPLX_1:140
                        .= ((t0 + (- r)) + (- r)) + r by XCMPLX_1:1
                        .= (t0 + - r) + ((- r) + r) by XCMPLX_1:1
                        .= (t0 + - r) + 0 by XCMPLX_0:def 6
                        .= t0 - r by XCMPLX_0:def 8;
          Ball(n,r) is Subset of I[01]
        by BORSUK_1:83,TOPMETR:14;
        then reconsider W = Ball(n,r) as Subset of I[01];
         A77: Ball(n,r) c= [.0,t0.]
          proof
           let x be set;
           assume A78: x in Ball(n,r);
            then x in [.0,1.] by A3;
            then reconsider t = x as Real;
            reconsider u = x as Point of Closed-Interval-MSpace(0,1)
                   by A78;
               Ball(n,r)={q where q is Element of
                   Closed-Interval-MSpace(0,1):dist(n,q)<r} by METRIC_1:18;
            then ex p being Element of
                   Closed-Interval-MSpace(0,1) st
                          p = u & dist(n,p)<r by A78;
            then abs(t - s0) < r by HEINE:1;
            then abs(t - s0) < t0 - s0 & t - s0 <= abs(t - s0)
                                         by A74,ABSVALUE:11,AXIOMS:22;
            then t - s0 < t0 - s0 by AXIOMS:22;
            then A79: t <= t0 by REAL_1:49;
               0 <= t & t <= 1 by A3,A78,Lm2;
            then t in {q where q is Real : 0<=q & q<=t0 } by A79;
           hence x in [.0,t0.] by RCOMP_1:def 1;
          end;
          A80: f.z in W by A73,TBSP_1:16;
           W is open & f is_continuous_at z by A2,TMAP_1:55,TOPMETR:21,27;
        then consider V being Subset of I[01] such that
          A81: V is open and A82: z in V and A83: f.:V c= W by A80,TMAP_1:48;
       consider s being real number such that
       A84: s > 0 and A85: Ball(m,s) c= V by A2,A81,A82,TOPMETR:22,27;
       reconsider s as Real by XREAL_0:def 1;
       set r0 = min(s,r);
              A86: r0 > 0 by A73,A84,SQUARE_1:38;
              A87: r0 <= r by SQUARE_1:35;
              A88: r0 <= s by SQUARE_1:35;
          Ball(m,r0) is Subset of I[01]
              by BORSUK_1:83,TOPMETR:14;
        then reconsider W0 = Ball(m,r0) as Subset of I[01];
          A89: W0 is open by A2,TOPMETR:21,27;
          A90: z in W0 by A86,TBSP_1:16;
           Ball(m,r0) c= Ball(m,s) by A88,PCOMPS_1:1;
        then A91: W0 c= V by A85,XBOOLE_1:1;
          Q meets W0 by A68,A89,A90,PRE_TOPC:54;
        then A92: Q /\ W0 <> {}I[01] by XBOOLE_0:def 7;
        consider w being Element of Q /\ W0;
          A93: w in Q & w in W0 by A92,XBOOLE_0:def 3;
        then reconsider w as Point of
         Closed-Interval-MSpace(0,1);
       reconsider w1 = w as Point of I[01] by A93;
       reconsider d = w1 as Real by A93;
           Ball(m,r0) =
           {q where q is Element of
              Closed-Interval-MSpace(0,1):dist(m,q)<r0} by METRIC_1:18;
        then ex p being Element of
            Closed-Interval-MSpace(0,1) st p = w & dist(m,p)<r0 by A93;
        then dist(m,w) < r by A87,AXIOMS:22;
        then abs(t0 - d) < r & t0 - d <= abs(t0 - d) by ABSVALUE:11,HEINE:1;
        then t0 - d < r by AXIOMS:22;
        then t0 + - d < r by XCMPLX_0:def 8;
        then t0 < r - (-d) by REAL_1:86;
        then t0 < r + - (-d) by XCMPLX_0:def 8;
        then A94: s0 + r < d by A76,REAL_1:84;
     A95: Ball(n,r) c= [.0,d.]
       proof let x be set;
        assume A96: x in Ball(n,r);
         then A97: x in [.0,1.] by A3;
        reconsider v = x as Point of Closed-Interval-MSpace(0,1)
                                                           by A96;
             reconsider t = x as Real by A97;
         A98: 0 <= t & t <= t0 by A70,A77,A96,Lm2;
            Ball(n,r)=
            {q where q is Element of
                 Closed-Interval-MSpace(0,1):dist(n,q)<r} by METRIC_1:18;
         then ex p being Element of
               Closed-Interval-MSpace(0,1) st p = v & dist(n,p)<r by A96;
         then A99: abs(t - s0) < r by HEINE:1;
          now per cases;
         suppose s0 <= t;
          then 0 <= t - s0 by SQUARE_1:12;
          then t - s0 < r by A99,ABSVALUE:def 1;
          then t < s0 + r by REAL_1:84;
          hence t < d by A94,AXIOMS:22;
         suppose A100: t < s0;
              s0 < s0 + r by A73,REAL_2:174;
           then s0 < d by A94,AXIOMS:22;
          hence t < d by A100,AXIOMS:22;
        end;
         then t in {w0 where w0 is Real : 0<=w0 & w0<=d} by A98;
        hence thesis by RCOMP_1:def 1;
       end;
               F.d in [.0,d.]
               proof
                   f.w1 in f.:V by A91,A93,FUNCT_2:43;
                then f.w1 in W by A83;
                hence thesis by A95;
               end;
        then d in A & d in B by A92,BORSUK_1:83,XBOOLE_0:def 3;
       hence contradiction by A27,XBOOLE_0:3;
      end;
      thus P misses Q by A22,XBOOLE_0:def 7;
    end;
    hence contradiction by Th22,CONNSP_1:11;
 end;

theorem Th25:
 a <= b implies
  for f being continuous map
         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
  assume A1: a <= b;
   let f be continuous map
         of Closed-Interval-TSpace(a,b), Closed-Interval-TSpace(a,b);
     now per cases by A1,REAL_1:def 5;
    suppose A2: a < b;
     set L = L[01]((#)(a,b),(a,b)(#)), P = P[01](a,b,(#)(0,1),(0,1)(#));
     set g = (P * f) * L;
      A3: id Closed-Interval-TSpace(a,b) = L * P by A2,Th18;
      A4: id Closed-Interval-TSpace(0,1) = P * L by A2,Th18;
      A5: f = (L * P) * f by A3,TMAP_1:93
            .= L * (P * f) by RELAT_1:55
            .= L * ((P * f) * (L * P)) by A3,TMAP_1:93
            .= L * (g * P) by RELAT_1:55
            .= (L * g) * P by RELAT_1:55;
       A6: L is continuous map
        of Closed-Interval-TSpace(0,1), Closed-Interval-TSpace(a,b)
                                                     by A1,Th11;
         P is continuous map
        of Closed-Interval-TSpace(a,b), Closed-Interval-TSpace(0,1)
                                                     by A2,Th15;
       then P * f is continuous by TOPS_2:58;
       then g is continuous by A6,TOPS_2:58;
      then consider y be Point of Closed-Interval-TSpace(0,1)
        such that A7: g.y = y by Th24,TOPMETR:27;
        now
       take x = L.y;
        thus f.x = (((L * g) * P) * L).y by A5,FUNCT_2:21
         .= ((L * g) *(id Closed-Interval-TSpace(0,1))).y by A4,RELAT_1:55
                .= (L * g).y by TMAP_1:93
                .= x by A7,FUNCT_2:21;
      end;
     hence ex x being Point of Closed-Interval-TSpace(a,b) st f.x = x;
    suppose A8: a = b;
     then [.a,b.] = {a} & a = (#)(a,b) by Def1,RCOMP_1:14;
     then A9: the carrier of Closed-Interval-TSpace(a,b) = {(#)(a,b)} by A8,
TOPMETR:25;
        now
       take x = (#)(a,b);
       thus f.x = x by A9,TARSKI:def 1;
      end;
     hence ex x being Point of Closed-Interval-TSpace(a,b) st f.x = x;
   end;
  hence thesis;
 end;

theorem Th26:
 for X, Y being non empty SubSpace of R^1, f being continuous map of X,Y
 holds
  (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
 proof
   let X, Y be non empty SubSpace of R^1, f be continuous map of X,Y;
  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.];
  reconsider A = [.a,b.] as non empty Subset of X
  by A1,A2,RCOMP_1:15;
   A5: A = the carrier of Closed-Interval-TSpace(a,b) by A1,TOPMETR:25;
     A6: dom(f|A) = the carrier of Closed-Interval-TSpace(a,b)
          proof
            A7: A = (the carrier of X) /\ A by XBOOLE_1:28;
               dom f = [#]X by TOPS_2:51;
           then dom f = the carrier of X & dom(f|A) = (dom f) /\ A
                                                    by PRE_TOPC:12,RELAT_1:90;
           hence thesis by A1,A7,TOPMETR:25;
          end;
    rng(f|A) c= the carrier of Closed-Interval-TSpace(a,b) by A4,A5,RELAT_1:148
;
   then f|A is Function
     of the carrier of Closed-Interval-TSpace(a,b),
        the carrier of Closed-Interval-TSpace(a,b)
   by A6,FUNCT_2:def 1,RELSET_1:11;
   then reconsider g = f|A as map
     of Closed-Interval-TSpace(a,b),Closed-Interval-TSpace(a,b);
     reconsider Z = Closed-Interval-TSpace(a,b) as SubSpace of X
                                                              by A5,TSEP_1:4;
     A8: Z is SubSpace of Y by A3,A5,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);
        reconsider w = s as Point of X by A5,TARSKI:def 3;
        for G being Subset of Closed-Interval-TSpace(a,b)
         st G is open & g.s in G
        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);
        assume G is open;
         then consider G0 being Subset of Y such that
           A9: G0 is open and A10: G0 /\ [#] Closed-Interval-TSpace(a,b) = G
                                                           by A8,TOPS_2:32;
        assume g.s in G;
         then f.w in G by A5,FUNCT_1:72;
         then f.w in G0 & f is_continuous_at w by A10,TMAP_1:49,XBOOLE_0:def 3
;
        then consider H0 being Subset of X such that
          A11: H0 is open and A12: w in
 H0 and A13: f.:H0 c= G0 by A9,TMAP_1:48;
           now
             A14: [#] Closed-Interval-TSpace(a,b) =
            the carrier of Closed-Interval-TSpace(a,b) by PRE_TOPC:12;
           then H0 /\ [#] Closed-Interval-TSpace(a,b) is Subset of the carrier
of Z
              by XBOOLE_1:17;
           then reconsider H = H0 /\ [#] Closed-Interval-TSpace(a,b)
               as Subset of Z;
          take H;
          thus H is open by A11,TOPS_2:32;
          thus s in H by A12,A14,XBOOLE_0:def 3;
          thus g.:H c= G
                proof
                  let t be set;
                 assume t in g.:H;
                  then consider r be set such that
                     r in dom g and A15: r in H and
                   A16: t = g.r by FUNCT_1:def 12;
                A17: r in the carrier of Z by A15;
                 reconsider r as Point of Closed-Interval-TSpace(a,b) by A15;
                  reconsider p = r as Point of X by A5,TARSKI:def 3;
                     p in the carrier of X;
                  then p in [#] X by PRE_TOPC:12;
                  then t=f.p & p in H0 & p in dom f
                            by A5,A15,A16,FUNCT_1:72,TOPS_2:51,XBOOLE_0:def 3;
                  then A18: t in f.:H0 by FUNCT_1:def 12;
                   A19:  rng g c= [#] Z by TOPS_2:51;
                     r in dom g by A14,A17,TOPS_2:51;
                  then t in g.:(the carrier of Z) by A16,FUNCT_1:def 12;
                  then t in rng g by FUNCT_2:45;
                  hence thesis by A10,A13,A18,A19,XBOOLE_0:def 3;
                end;
         end;
        hence thesis;
       end;
      hence thesis by TMAP_1:48;
     end;
    then reconsider h = g as continuous map
             of Closed-Interval-TSpace(a,b),Closed-Interval-TSpace(a,b) by
TMAP_1:49;
      now
     consider y being Point of Closed-Interval-TSpace(a,b) such that
        A20: h.y = y by A1,Th25;
      reconsider x = y as Point of X by A5,TARSKI:def 3;
     take x;
     thus f.x = x by A5,A20,FUNCT_1:72;
    end;
  hence thesis;
 end;

theorem
   for X, Y being non empty SubSpace of R^1,
     f being continuous map of X,Y holds
  (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
 proof
   let X, Y be non empty SubSpace of R^1,
       f be continuous map of X,Y;
  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.];
  set g = (Y incl R^1) * f;
      (Y incl R^1) is continuous map of Y,R^1 by TMAP_1:98;
   then A4: g is continuous by TOPS_2:58;
      A5: R^1 is SubSpace of R^1 by TSEP_1:2;
      the carrier of X c= the carrier of R^1 by BORSUK_1:35;
   then A6: [.a,b.] c= the carrier of R^1 by A2,XBOOLE_1:1;
       f.:[.a,b.] c= the carrier of Y &
       the carrier of Y c= the carrier of R^1 by BORSUK_1:35;
   then reconsider B = f.:[.a,b.] as Subset of R^1 by XBOOLE_1:1
;
       g.:[.a,b.] = (Y incl R^1).:(f.:[.a,b.]) by RELAT_1:159;
   then g.:[.a,b.] = ((id R^1)|Y).:B by TMAP_1:def 6;
   then g.:[.a,b.] = (id R^1).:B by TMAP_1:61;
   then g.:[.a,b.] = (id the carrier of R^1).:B by GRCAT_1:def 11;
   then A7: g.:[.a,b.] c= [.a,b.] by A3,BORSUK_1:3;
      now
     consider x being Point of X such that
        A8: g.x = x by A1,A2,A4,A5,A6,A7,Th26;
     take x;
         the carrier of Y c= the carrier of R^1 by BORSUK_1:35;
      then reconsider y = f.x as Point of R^1 by TARSKI:def 3;
     thus f.x = (Y incl R^1).y by TMAP_1:95
             .= x by A8,FUNCT_2:21;
    end;
  hence thesis;
 end;

Back to top