:: Algebraic Properties of Homotopies
::  by Adam Grabowski and Artur Korni{\l}owicz
::
:: Received March 18, 2004
:: Copyright (c) 2004 Association of Mizar Users

environ

 vocabularies PRE_TOPC, FUNCT_1, RELAT_1, SUBSET_1, BOOLE, COMPTS_1, ORDINAL2,
      FUNCT_4, FUNCOP_1, TOPS_2, BORSUK_1, GRAPH_1, RCOMP_1, ARYTM_3, ARYTM_1,
      TREAL_1, SEQ_1, TOPMETR, SEQM_3, EUCLID, MCART_1, BORSUK_2, BORSUK_6,
      ARYTM, FUNCT_3, MEMBERED, FINSEQ_1, JGRAPH_2, SGRAPH1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
      XXREAL_0, XREAL_0, REAL_1, MEMBERED, MCART_1, FINSEQ_1, RELAT_1, FUNCT_1,
      RELSET_1, PARTFUN1, FUNCT_3, FUNCT_2, FUNCOP_1, STRUCT_0, PRE_TOPC,
      EUCLID, TOPS_2, RCOMP_1, COMPTS_1, JGRAPH_2, TREAL_1, FUNCT_4, BORSUK_1,
      TOPMETR, BINOP_1, BORSUK_2, BORSUK_4;
 constructors REAL_1, RCOMP_1, FINSEQ_4, CONNSP_1, TOPS_2, COMPTS_1, GRCAT_1,
      T_0TOPSP, MONOID_0, TREAL_1, BORSUK_2, JGRAPH_2, BORSUK_4, SEQ_1;
 registrations XBOOLE_0, RELSET_1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0,
      MEMBERED, STRUCT_0, PRE_TOPC, BORSUK_1, MONOID_0, EUCLID, TOPMETR,
      BORSUK_2, BORSUK_3, JGRAPH_2, BORSUK_4;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions XBOOLE_0, BORSUK_2, MEMBERED, BINOP_1, EUCLID, STRUCT_0, PCOMPS_1,
      TARSKI;
 theorems BORSUK_1, FUNCOP_1, TOPS_2, TREAL_1, FUNCT_2, FUNCT_1, PRE_TOPC,
      RCOMP_1, TARSKI, RELAT_1, REAL_1, TOPS_1, REAL_2, TOPMETR, FUNCT_4,
      TOPMETR2, MCART_1, ZFMISC_1, FUNCT_3, COMPTS_1, XBOOLE_0, XBOOLE_1,
      XCMPLX_1, BORSUK_2, TMAP_1, BORSUK_3, BORSUK_4, XREAL_0, YELLOW12,
      JORDAN6, JGRAPH_2, TSEP_1, JGRAPH_1, JORDAN5B, MEMBERED, TOPREAL6,
      EUCLID, FINSEQ_1, CATALG_1, JORDAN1K, XREAL_1, XXREAL_0, FINSEQ_2,
      XXREAL_1;
 schemes RECDEF_2, DOMAIN_1, XBOOLE_0, JGRAPH_2, PARTFUN1, BINOP_1;

begin :: Preliminaries

scheme ExFunc3CondD { C() -> non empty set, P,Q,R[set], F,G,H(set) -> set }:
  ex f being Function st dom f = C() &
  for c being Element of C() holds (P[c] implies f.c = F(c)) &
  (Q[c] implies f.c = G(c)) & (R[c] implies f.c = H(c))
provided
A1: for c being Element of C() holds (P[c] implies not Q[c]) &
(P[c] implies not R[c]) & (Q[c] implies not R[c])
and
A2: for c being Element of C() holds P[c] or Q[c] or R[c]
proof
A3: for c being set st c in C() holds (P[c] implies not Q[c]) &
  (P[c] implies not R[c]) & (Q[c] implies not R[c]) by A1;
A4: for c being set st c in C() holds P[c] or Q[c] or R[c] by A2;
  ex f being Function st dom f = C() &
  for c being set st c in C() holds (P[c] implies f.c = F(c)) &
  (Q[c] implies f.c = G(c)) & (R[c] implies f.c = H(c)) from
  RECDEF_2:sch 1(A3,A4);
  then consider f being Function such that
A5: dom f = C() and
A6: for c being set st c in C() holds (P[c] implies f.c = F(c)) &
  (Q[c] implies f.c = G(c)) & (R[c] implies f.c = H(c));
  take f;
  thus dom f = C() by A5;
  let c be Element of C();
  thus thesis by A6;
end;

theorem Th1:
  the carrier of [:I[01],I[01]:] = [:[.0,1.], [.0,1.]:] by BORSUK_1:83,def 5;

canceled 3;

theorem Th5:
  for a, b, x being real number st a <= x & x <= b holds
  (x - a) / (b - a) in the carrier of Closed-Interval-TSpace (0,1)
proof
  let a, b, x be real number;
  assume
A1: a <= x & x <= b;
  then
A2: x - a <= b - a by XREAL_1:11;
A3: a <= b by A1,XXREAL_0:2;
  then
A4: b - a >= 0 by XREAL_1:50;
A5: (x - a) / (b - a) <= 1
  proof
    per cases by A3,XREAL_1:50;
    suppose b - a = 0;
      hence thesis by XCMPLX_1:49;
    end;
    suppose b - a > 0;
      hence thesis by A2,REAL_2:117;
    end;
  end;
  x - a >= 0 by A1,XREAL_1:50;
  then (x - a) / (b - a) >= 0 by A4;
  then (x - a) / (b - a) in [.0,1.] by A5,XXREAL_1:1;
  hence thesis by TOPMETR:25;
end;

theorem Th6:
  for x being Point of I[01] st x <= 1/2 holds 2 * x is Point of I[01]
proof
  let x be Point of I[01];
  assume x <= 1/2;
  then
A1: 2 * x <= 2 * (1/2) by XREAL_1:66;
  0 <= x by BORSUK_1:86;
  then 2 * 0 <= 2 * x;
  hence thesis by A1,BORSUK_1:86;
end;

theorem Th7:
  for x being Point of I[01] st x >= 1/2 holds 2 * x - 1 is Point of I[01]
proof
  let x be Point of I[01];
  assume x >= 1/2;
  then 2 * x >= 2 * (1/2) by XREAL_1:66;
  then
A1: 2 * x - 1 >= 1 - 1 by XREAL_1:11;
  x <= 1 by BORSUK_1:86;
  then 2 * x <= 2 * 1 by XREAL_1:66;
  then 2 * x - 1 <= 2 - 1 by XREAL_1:11;
  hence thesis by A1,BORSUK_1:86;
end;

theorem Th8:
  for p, q being Point of I[01] holds p * q is Point of I[01]
proof
  let p, q be Point of I[01];
A1: 0 <= p & p <= 1 & 0 <= q & q <= 1 by BORSUK_1:86;
  then
A2: 0 <= p * q;
  p * q <= 1 by A1,REAL_2:140;
  hence thesis by A2,BORSUK_1:86;
end;

theorem Th9:
  for x being Point of I[01] holds 1/2 * x is Point of I[01]
proof
  let x be Point of I[01];
  x >= 0 by BORSUK_1:86;
  then
A1: 1/2 * x >= 1/2 * 0;
  x <= 1 by BORSUK_1:86;
  then 1/2 * x <= 1/2 * 1 by XREAL_1:66;
  then 1/2 * x <= 1 by XXREAL_0:2;
  hence thesis by A1,BORSUK_1:86;
end;

theorem Th10:
  for x being Point of I[01] st x >= 1/2 holds x - 1/4 is Point of I[01]
proof
  let x be Point of I[01];
  assume x >= 1/2;
  then x >= 1/4 + 0 by XXREAL_0:2;
  then
A1: x - 1/4 >= 0 by XREAL_1:21;
  x <= 1 by BORSUK_1:86;
  then x <= 1 + 1/4 by XXREAL_0:2;
  then x - 1/4 <= 1 by XREAL_1:22;
  hence thesis by A1,BORSUK_1:86;
end;

canceled;

theorem Th12:
  id I[01] is Path of 0[01], 1[01]
proof
  set f = id I[01];
  f.0 = 0[01] & f.1 = 1[01] by BORSUK_1:def 17,def 18,TMAP_1:91;
  hence thesis by BORSUK_2:def 4;
end;

theorem Th13:
  for a, b, c, d being Point of I[01] st a <= b & c <= d holds
  [:[.a,b.], [.c,d.]:] is compact non empty Subset of [:I[01], I[01]:]
proof
  let a, b, c, d be Point of I[01];
  assume that
A1: a <= b and
A2: c <= d;
A3: [.a,b.] is Subset of I[01] by BORSUK_4:43;
  [.c,d.] is Subset of I[01] by BORSUK_4:43;
  then
A4: [:[.a,b.], [.c,d.]:] c=
  [:the carrier of I[01], the carrier of I[01]:] by A3,ZFMISC_1:119;
A5: a in [.a,b.] by A1,XXREAL_1:1;
  c in [.c,d.] by A2,XXREAL_1:1;
  then reconsider Ewa = [:[.a,b.], [.c,d.]:] as
  non empty Subset of [:I[01], I[01]:] by A4,A5,BORSUK_1:def 5,ZFMISC_1:106;
  [.a,b.] is compact Subset of I[01] &
  [.c,d.] is compact Subset of I[01] by A1,A2,BORSUK_4:49;
  then Ewa is compact Subset of [:I[01], I[01]:] by BORSUK_3:27;
  hence thesis;
end;

begin :: Affine Maps

theorem Th14:
  for S, T being Subset of TOP-REAL 2 st
  S = {p where p is Point of TOP-REAL 2 : p`2 <= 2 * p`1 - 1 } &
  T = {p where p is Point of TOP-REAL 2 : p`2 <= p`1 } holds
  AffineMap (1, 0, 1/2, 1/2) .: S = T
proof
  let S, T be Subset of TOP-REAL 2;
  assume
A1: S = {p where p is Point of TOP-REAL 2 : p`2 <= 2 * p`1 - 1 } &
  T = {p where p is Point of TOP-REAL 2 : p`2 <= p`1 };
  set A = 1, B = 0, C = 1/2, D = 1/2;
  set f = AffineMap (1,0,1/2,1/2);
  f .: S = T
  proof
    thus f .: S c= T
    proof
      let x be set;
      assume x in f .: S;
      then consider y being set such that
A2:   y in dom f & y in S & x = f.y by FUNCT_1:def 12;
      consider p being Point of TOP-REAL 2 such that
A3:   y = p & p`2 <= 2 * p`1 - 1 by A1,A2;
      set b = f.p;
A4:   f.p = |[A*(p`1)+B,C*(p`2)+D]| by JGRAPH_2:def 2;
      then
A5:   b`1 = A * (p`1) + B by EUCLID:56;
A6:   b`2 = C * (p`2) + D by A4,EUCLID:56;
      C * p`2 <= C * (2 * p`1 - 1) by A3,XREAL_1:66;
      then C * p`2 + D <= p`1 - C + D by XREAL_1:8;
      hence thesis by A1,A2,A3,A5,A6;
    end;
    let x be set;
    assume x in T;
    then consider p being Point of TOP-REAL 2 such that
A7: x = p & p`2 <= p`1 by A1;
    f is onto by JORDAN1K:36;
    then rng f = the carrier of TOP-REAL 2 by FUNCT_2:def 3;
    then consider y being set such that
A8: y in dom f & x = f.y by A7,FUNCT_1:def 5;
    reconsider y as Point of TOP-REAL 2 by A8;
    set b = f.y;
A9: f.y = |[A*(y`1)+B,C*(y`2)+D]| by JGRAPH_2:def 2;
    then
A10: b`1 = y`1 by EUCLID:56;
A11: b`2 = C * (y`2) + D by A9,EUCLID:56;
    2 * b`2 <= 2 * y`1 by A7,A8,A10,XREAL_1:66;
    then 2 * b`2 - 1 <= 2 * y`1 - 1 by XREAL_1:11;
    then y in S by A1,A11;
    hence thesis by A8,FUNCT_1:def 12;
  end;
  hence thesis;
end;

theorem Th15:
  for S, T being Subset of TOP-REAL 2 st
  S = {p where p is Point of TOP-REAL 2 : p`2 >= 2 * p`1 - 1 } &
  T = {p where p is Point of TOP-REAL 2 : p`2 >= p`1 } holds
  AffineMap (1, 0, 1/2, 1/2) .: S = T
proof
  let S, T be Subset of TOP-REAL 2;
  assume
A1: S = {p where p is Point of TOP-REAL 2 : p`2 >= 2 * p`1 - 1 } &
  T = {p where p is Point of TOP-REAL 2 : p`2 >= p`1 };
  set A = 1, B = 0, C = 1/2, D = 1/2;
  set f = AffineMap (1,0,1/2,1/2);
  f .: S = T
  proof
    thus f .: S c= T
    proof
      let x be set;
      assume x in f .: S;
      then consider y being set such that
A2:   y in dom f & y in S & x = f.y by FUNCT_1:def 12;
      consider p being Point of TOP-REAL 2 such that
A3:   y = p & p`2 >= 2 * p`1 - 1 by A1,A2;
      set b = f.p;
A4:   f.p = |[A*(p`1)+B,C*(p`2)+D]| by JGRAPH_2:def 2;
      then
A5:   b`1 = A * (p`1) + B by EUCLID:56;
A6:   b`2 = C * (p`2) + D by A4,EUCLID:56;
      C * p`2 >= C * (2 * p`1 - 1) by A3,XREAL_1:66;
      then b`2 >= p`1 - C + D by A6,XREAL_1:8;
      hence thesis by A1,A2,A3,A5;
    end;
    let x be set;
    assume x in T;
    then consider p being Point of TOP-REAL 2 such that
A7: x = p & p`2 >= p`1 by A1;
    f is onto by JORDAN1K:36;
    then rng f = the carrier of TOP-REAL 2 by FUNCT_2:def 3;
    then consider y being set such that
A8: y in dom f & x = f.y by A7,FUNCT_1:def 5;
    reconsider y as Point of TOP-REAL 2 by A8;
    set b = f.y;
A9: f.y = |[A*(y`1)+B,C*(y`2)+D]| by JGRAPH_2:def 2;
    then
A10: b`1 = y`1 by EUCLID:56;
A11: b`2 = C * (y`2) + D by A9,EUCLID:56;
    2 * b`2 >= 2 * y`1 by A7,A8,A10,XREAL_1:66;
    then 2 * b`2 - 1 >= 2 * y`1 - 1 by XREAL_1:11;
    then y in S by A1,A11;
    hence thesis by A8,FUNCT_1:def 12;
  end;
  hence thesis;
end;

theorem Th16:
  for S, T being Subset of TOP-REAL 2 st
  S = {p where p is Point of TOP-REAL 2 : p`2 >= 1 - 2 * p`1 } &
  T = {p where p is Point of TOP-REAL 2 : p`2 >= - p`1 } holds
  AffineMap (1, 0, 1/2, -1/2) .: S = T
proof
  let S, T be Subset of TOP-REAL 2;
  assume
A1: S = {p where p is Point of TOP-REAL 2 : p`2 >= 1 - 2 * p`1 } &
  T = {p where p is Point of TOP-REAL 2 : p`2 >= - p`1 };
  set A = 1, B = 0, C = 1/2, D = -1/2;
  set f = AffineMap (1,0,1/2,-1/2);
  f .: S = T
  proof
    thus f .: S c= T
    proof
      let x be set;
      assume x in f .: S;
      then consider y being set such that
A2:   y in dom f & y in S & x = f.y by FUNCT_1:def 12;
      consider p being Point of TOP-REAL 2 such that
A3:   y = p & p`2 >= 1 - 2 * p`1 by A1,A2;
      set b = f.p;
A4:   f.p = |[A*(p`1)+B,C*(p`2)+D]| by JGRAPH_2:def 2;
      then
A5:   b`1 = A * (p`1) + B by EUCLID:56;
      C * p`2 >= C * (1 - 2 * p`1) by A3,XREAL_1:66;
      then C * p`2 + D >= C - p`1 + D by XREAL_1:8;
      then b`2 >= - b`1 by A4,A5,EUCLID:56;
      hence thesis by A1,A2,A3;
    end;
    let x be set;
    assume x in T;
    then consider p being Point of TOP-REAL 2 such that
A6: x = p & p`2 >= - p`1 by A1;
    f is onto by JORDAN1K:36;
    then rng f = the carrier of TOP-REAL 2 by FUNCT_2:def 3;
    then consider y being set such that
A7: y in dom f & x = f.y by A6,FUNCT_1:def 5;
    reconsider y as Point of TOP-REAL 2 by A7;
    set b = f.y;
A8: f.y = |[A*(y`1)+B,C*(y`2)+D]| by JGRAPH_2:def 2;
    then
A9: b`1 = y`1 by EUCLID:56;
A10: b`2 = C * (y`2) + D by A8,EUCLID:56;
    2 * b`2 >= 2 * (- y`1) by A6,A7,A9,XREAL_1:66;
    then 2 * b`2 + 1 >= 2 * (- y`1) + 1 by XREAL_1:8;
    then y`2 >= 1 - 2 * y`1 by A10;
    then y in S by A1;
    hence thesis by A7,FUNCT_1:def 12;
  end;
  hence thesis;
end;

theorem Th17:
  for S, T being Subset of TOP-REAL 2 st
  S = {p where p is Point of TOP-REAL 2 : p`2 <= 1 - 2 * p`1 } &
  T = {p where p is Point of TOP-REAL 2 : p`2 <= - p`1 } holds
  AffineMap (1, 0, 1/2, -1/2) .: S = T
proof
  let S, T be Subset of TOP-REAL 2;
  assume
A1: S = {p where p is Point of TOP-REAL 2 : p`2 <= 1 - 2 * p`1 } &
  T = {p where p is Point of TOP-REAL 2 : p`2 <= - p`1 };
  set A = 1, B = 0, C = 1/2, D = -1/2;
  set f = AffineMap (1,0,1/2,-1/2);
  f .: S = T
  proof
    thus f .: S c= T
    proof
      let x be set;
      assume x in f .: S;
      then consider y being set such that
A2:   y in dom f & y in S & x = f.y by FUNCT_1:def 12;
      consider p being Point of TOP-REAL 2 such that
A3:   y = p & p`2 <= 1 - 2 * p`1 by A1,A2;
      set b = f.p;
A4:   f.p = |[A*(p`1)+B,C*(p`2)+D]| by JGRAPH_2:def 2;
      then
A5:   b`1 = A * (p`1) + B by EUCLID:56;
      C * p`2 <= C * (1 - 2 * p`1) by A3,XREAL_1:66;
      then C * p`2 + D <= C - p`1 + D by XREAL_1:8;
      then b`2 <= - b`1 by A4,A5,EUCLID:56;
      hence thesis by A1,A2,A3;
    end;
    let x be set;
    assume x in T;
    then consider p being Point of TOP-REAL 2 such that
A6: x = p & p`2 <= - p`1 by A1;
    f is onto by JORDAN1K:36;
    then rng f = the carrier of TOP-REAL 2 by FUNCT_2:def 3;
    then consider y being set such that
A7: y in dom f & x = f.y by A6,FUNCT_1:def 5;
    reconsider y as Point of TOP-REAL 2 by A7;
    set b = f.y;
A8: f.y = |[A*(y`1)+B,C*(y`2)+D]| by JGRAPH_2:def 2;
    then
A9: b`1 = y`1 by EUCLID:56;
A10: b`2 = C * (y`2) + D by A8,EUCLID:56;
    2 * b`2 <= 2 * (- y`1) by A6,A7,A9,XREAL_1:66;
    then 2 * b`2 + 1 <= 2 * (- y`1) + 1 by XREAL_1:8;
    then y`2 <= 1 - 2 * y`1 by A10;
    then y in S by A1;
    hence thesis by A7,FUNCT_1:def 12;
  end;
  hence thesis;
end;

begin :: Real-membered Structures

theorem Th18:
  for T being non empty 1-sorted holds T is real-membered iff
  for x being Element of T holds x is real
proof
  let T be non empty 1-sorted;
  thus T is real-membered implies
   for x being Element of T holds x is real;
  assume for x being Element of T holds x is real;
  then for x being set st x in the carrier of T holds x is real;
  then the carrier of T is real-membered by MEMBERED:def 3;
  hence thesis by BORSUK_4:def 2;
end;

registration
  cluster non empty real-membered 1-sorted;
  existence
  proof
    take I[01];
    thus thesis;
  end;
  cluster non empty real-membered TopSpace;
  existence
  proof
    take I[01];
    thus thesis;
  end;
end;

registration
  let T be real-membered 1-sorted;
  cluster -> real Element of T;
  coherence;
end;

registration
  let T be real-membered TopStruct;
  cluster -> real-membered SubSpace of T;
  coherence
  proof
    let R be SubSpace of T;
    the carrier of R is real-membered
    proof
      let x be set;
      assume
A1:   x in the carrier of R;
      the carrier of R c= the carrier of T by BORSUK_1:35;
      then x is Element of T by A1;
      hence thesis;
    end;
    hence thesis by BORSUK_4:def 2;
  end;
end;

registration
  let S, T be real-membered non empty TopSpace, p be Element of [:S, T:];
  cluster p`1 -> real;
  coherence
  proof
    p in the carrier of [:S, T:];
    then p in [:the carrier of S, the carrier of T:] by BORSUK_1:def 5;
    then p`1 in the carrier of S by MCART_1:10;
    hence thesis;
  end;
  cluster p`2 -> real;
  coherence
  proof
    p in the carrier of [:S, T:];
    then p in [:the carrier of S, the carrier of T:] by BORSUK_1:def 5;
    then p`2 in the carrier of T by MCART_1:10;
    hence thesis;
  end;
end;

registration
  let T be non empty SubSpace of [:I[01], I[01]:], x be Point of T;
  cluster x`1 -> real;
  coherence
  proof
A1: the carrier of T c= the carrier of [:I[01], I[01]:] by BORSUK_1:35;
    x in the carrier of T;
    then reconsider x' = x as Point of [:I[01], I[01]:] by A1;
    x'`1 is real;
    hence thesis;
  end;
  cluster x`2 -> real;
  coherence
  proof
A2: the carrier of T c= the carrier of [:I[01], I[01]:] by BORSUK_1:35;
    x in the carrier of T;
    then reconsider x' = x as Point of [:I[01], I[01]:] by A2;
    x'`2 is real;
    hence thesis;
  end;
end;

registration
  cluster R^1 -> real-membered;
  coherence
  proof
    for x being Element of R^1 holds x is real by TOPMETR:24;
    hence thesis by Th18;
  end;
end;

begin :: Closed Subsets of TOP-REAL 2

theorem Th19:
  {p where p is Point of TOP-REAL 2 : p`2 <= 2 * p`1 - 1 }
  is closed Subset of TOP-REAL 2
proof
  defpred P[Point of TOP-REAL 2] means $1`2 <= 2 * $1`1 - 1;
  {p where p is Point of TOP-REAL 2 : P[p] }
  is Subset of TOP-REAL 2 from JGRAPH_2:sch 1;
  then reconsider K = {p where p is Point of TOP-REAL 2 : p`2 <= 2 * p`1 - 1 }
  as Subset of TOP-REAL 2;
  set f = AffineMap (1,0,1/2,1/2);
  reconsider L = {p where p is Point of TOP-REAL 2 : p`2 <= p`1 }
  as closed Subset of TOP-REAL 2 by JGRAPH_2:56;
  K c= the carrier of TOP-REAL 2;
  then
A1: K c= dom f by FUNCT_2:def 1;
A2: f is one-to-one by JGRAPH_2:54;
A3: f .: K = L by Th14;
  K = f " (f .: K) by A1,A2,FUNCT_1:164;
  hence thesis by A3,PRE_TOPC:def 12;
end;

theorem Th20:
  {p where p is Point of TOP-REAL 2 : p`2 >= 2 * p`1 - 1 }
  is closed Subset of TOP-REAL 2
proof
  defpred P[Point of TOP-REAL 2] means $1`2 >= 2 * $1`1 - 1;
  {p where p is Point of TOP-REAL 2 : P[p] }
  is Subset of TOP-REAL 2 from JGRAPH_2:sch 1;
  then reconsider K = {p where p is Point of TOP-REAL 2 : p`2 >= 2 * p`1 - 1 }
  as Subset of TOP-REAL 2;
  set f = AffineMap (1,0,1/2,1/2);
  reconsider L = {p where p is Point of TOP-REAL 2 : p`2 >= p`1 }
  as closed Subset of TOP-REAL 2 by JGRAPH_2:56;
  K c= the carrier of TOP-REAL 2;
  then
A1: K c= dom f by FUNCT_2:def 1;
A2: f is one-to-one by JGRAPH_2:54;
A3: f .: K = L by Th15;
  K = f " (f .: K) by A1,A2,FUNCT_1:164;
  hence thesis by A3,PRE_TOPC:def 12;
end;

theorem Th21:
  {p where p is Point of TOP-REAL 2 : p`2 <= 1 - 2 * p`1 }
  is closed Subset of TOP-REAL 2
proof
  defpred P[Point of TOP-REAL 2] means $1`2 <= 1 - 2 * $1`1;
  {p where p is Point of TOP-REAL 2 : P[p] }
  is Subset of TOP-REAL 2 from JGRAPH_2:sch 1;
  then reconsider K = {p where p is Point of TOP-REAL 2 : p`2 <= 1 - 2 * p`1 }
  as Subset of TOP-REAL 2;
  set f = AffineMap (1,0,1/2,-1/2);
  reconsider L = {p where p is Point of TOP-REAL 2 : p`2 <= - p`1 }
  as closed Subset of TOP-REAL 2 by JGRAPH_2:57;
  K c= the carrier of TOP-REAL 2;
  then
A1: K c= dom f by FUNCT_2:def 1;
A2: f is one-to-one by JGRAPH_2:54;
A3: f .: K = L by Th17;
  K = f " (f .: K) by A1,A2,FUNCT_1:164;
  hence thesis by A3,PRE_TOPC:def 12;
end;

theorem Th22:
  {p where p is Point of TOP-REAL 2 : p`2 >= 1 - 2 * p`1 }
  is closed Subset of TOP-REAL 2
proof
  defpred P[Point of TOP-REAL 2] means $1`2 >= 1 - 2 * $1`1;
  {p where p is Point of TOP-REAL 2 : P[p] }
  is Subset of TOP-REAL 2 from JGRAPH_2:sch 1;
  then reconsider K = {p where p is Point of TOP-REAL 2 : p`2 >= 1 - 2 * p`1 }
  as Subset of TOP-REAL 2;
  set f = AffineMap (1,0,1/2,-1/2);
  reconsider L = {p where p is Point of TOP-REAL 2 : p`2 >= - p`1 }
  as closed Subset of TOP-REAL 2 by JGRAPH_2:57;
  K c= the carrier of TOP-REAL 2;
  then
A1: K c= dom f by FUNCT_2:def 1;
A2: f is one-to-one by JGRAPH_2:54;
A3: f .: K = L by Th16;
  K = f " (f .: K) by A1,A2,FUNCT_1:164;
  hence thesis by A3,PRE_TOPC:def 12;
end;

theorem Th23:
  {p where p is Point of TOP-REAL 2 : p`2 >= 1 - 2 * p`1 &
  p`2 >= 2 * p`1 - 1 } is closed Subset of TOP-REAL 2
proof
  defpred P[Point of TOP-REAL 2] means $1`2 >= 1 - 2 * $1`1;
  defpred R[Point of TOP-REAL 2] means $1`2 >= 2 * $1`1 - 1;
  set T = {p where p is Point of TOP-REAL 2 : P[p] & R[p] };
  reconsider K = { p where p is Point of TOP-REAL 2 : P[p] }
  as closed Subset of TOP-REAL 2 by Th22;
  reconsider L = { p where p is Point of TOP-REAL 2 : R[p] }
  as closed Subset of TOP-REAL 2 by Th20;
  {p where p is Point of TOP-REAL 2 : P[p] & R[p] } =
  { p where p is Point of TOP-REAL 2 : P[p] } /\
  { p where p is Point of TOP-REAL 2 : R[p] } from DOMAIN_1:sch 10;
  then T = K /\ L;
  hence thesis by TOPS_1:35;
end;

theorem Th24:
  ex f being Function of [:R^1,R^1:], TOP-REAL 2 st
  for x, y being Real holds f. [x,y] = <*x,y*>
proof
  defpred P[Element of REAL,Element of REAL,set] means
  ex c being Element of REAL 2 st c = $3 & $3 = <*$1,$2*>;
A1: for x, y being Element of REAL ex u being Element of REAL 2 st P[x,y,u]
  proof
    let x, y be Element of REAL;
    take <*x,y*>;
    <*x,y*> is Element of REAL 2 by CATALG_1:10;
    hence thesis;
  end;
  consider f being Function of [:REAL,REAL:],REAL 2 such that
A2: for x, y being Element of REAL holds P[x,y,f.(x,y)]
  from BINOP_1:sch 3(A1);
  the carrier of [:R^1,R^1:] = [:the carrier of R^1,the carrier of R^1:] &
  the carrier of R^1 = REAL & the carrier of TOP-REAL 2 = REAL 2
  by BORSUK_1:def 5,TOPMETR:24;
  then reconsider f as Function of [:R^1,R^1:], TOP-REAL 2;
  take f;
  for x, y being Real holds f. [x,y] = <*x,y*>
  proof
    let x, y be Real;
    P[x,y,f.(x,y)] by A2;
    hence thesis;
  end;
  hence thesis;
end;

theorem Th25:
  { p where p is Point of [:R^1,R^1:] : p`2 <= 1 - 2 * (p`1) }
  is closed Subset of [:R^1,R^1:]
proof
  set GG = [:R^1,R^1:], SS = TOP-REAL 2;
  defpred P[Point of GG] means $1`2 <= 1 - 2 * ($1`1);
  defpred R[Point of SS] means $1`2 <= 1 - 2 * ($1`1);
  reconsider K = { p where p is Point of GG : P[p] } as Subset of GG
  from DOMAIN_1:sch 7;
  reconsider L = { p where p is Point of SS : R[p] } as Subset of SS
  from DOMAIN_1:sch 7;
  consider f being Function of GG, SS such that
A1: for x, y being Real holds f. [x,y] = <*x,y*> by Th24;
A2: f is_homeomorphism by A1,TOPREAL6:85;
  f .: K = L
  proof
    thus f .: K c= L
    proof
      let x be set;
      assume x in f .: K;
      then consider y being set such that
A3:   y in dom f & y in K & x = f.y by FUNCT_1:def 12;
      consider z being Point of GG such that
A4:   z = y & P[z] by A3;
      z in the carrier of GG;
      then z in [:the carrier of R^1, the carrier of R^1:] by BORSUK_1:def 5;
      then consider x1, y1 being set such that
A5:   x1 in the carrier of R^1 & y1 in the carrier of R^1 & z = [x1, y1]
      by ZFMISC_1:def 2;
      reconsider x1, y1 as Real by A5,TOPMETR:24;
A6:   x = |[ x1, y1 ]| by A1,A3,A4,A5;
      then reconsider x' = x as Point of SS;
A7:   x'`1 = x1 by A6,FINSEQ_1:61;
A8:   x'`2 = y1 by A6,FINSEQ_1:61;
      z`1 = x1 & z`2 = y1 by A5,MCART_1:7;
      hence thesis by A4,A7,A8;
    end;
    thus L c= f .: K
    proof
      let x be set;
      assume x in L;
      then consider z being Point of SS such that
A9:   z = x & R[z];
      consider x1, y1 being Real such that
A10:  z = <*x1, y1*> by FINSEQ_2:120;
      z`1 = x1 by A10,EUCLID:56;
      then
A11:  y1 <= 1 - 2 * x1 by A9,A10,EUCLID:56;
      set Y = [x1, y1];
A12:  Y in [:REAL, REAL:] by ZFMISC_1:106;
      then
A13:  Y in the carrier of GG by BORSUK_1:def 5,TOPMETR:24;
      reconsider Y as Point of GG by A12,BORSUK_1:def 5,TOPMETR:24;
      Y`1 = x1 & Y`2 = y1 by MCART_1:7;
      then
A14:  Y in K by A11;
A15:  Y in dom f by A13,FUNCT_2:def 1;
      x = f.Y by A1,A9,A10;
      hence thesis by A14,A15,FUNCT_1:def 12;
    end;
  end;
  hence thesis by A2,Th21,TOPS_2:72;
end;

theorem Th26:
  { p where p is Point of [:R^1,R^1:] : p`2 <= 2 * (p`1) - 1 }
  is closed Subset of [:R^1,R^1:]
proof
  set GG = [:R^1,R^1:], SS = TOP-REAL 2;
  defpred P[Point of GG] means $1`2 <= 2 * ($1`1) - 1;
  defpred R[Point of SS] means $1`2 <= 2 * ($1`1) - 1;
  reconsider K = { p where p is Point of GG : P[p] } as Subset of GG
  from DOMAIN_1:sch 7;
  reconsider L = { p where p is Point of SS : R[p] } as Subset of SS
  from DOMAIN_1:sch 7;
  consider f being Function of GG, SS such that
A1: for x, y being Real holds f. [x,y] = <*x,y*> by Th24;
A2: f is_homeomorphism by A1,TOPREAL6:85;
  f .: K = L
  proof
    thus f .: K c= L
    proof
      let x be set;
      assume x in f .: K;
      then consider y being set such that
A3:   y in dom f & y in K & x = f.y by FUNCT_1:def 12;
      consider z being Point of GG such that
A4:   z = y & P[z] by A3;
      z in the carrier of GG;
      then z in [:the carrier of R^1, the carrier of R^1:] by BORSUK_1:def 5;
      then consider x1, y1 being set such that
A5:   x1 in the carrier of R^1 & y1 in the carrier of R^1 & z = [x1, y1]
      by ZFMISC_1:def 2;
      reconsider x1, y1 as Real by A5,TOPMETR:24;
A6:   x = |[ x1, y1 ]| by A1,A3,A4,A5;
      then reconsider x' = x as Point of SS;
A7:   x'`1 = x1 by A6,FINSEQ_1:61;
A8:   x'`2 = y1 by A6,FINSEQ_1:61;
      z`1 = x1 & z`2 = y1 by A5,MCART_1:7;
      hence thesis by A4,A7,A8;
    end;
    thus L c= f .: K
    proof
      let x be set;
      assume x in L;
      then consider z being Point of SS such that
A9:   z = x & R[z];
      consider x1, y1 being Real such that
A10:  z = <*x1, y1*> by FINSEQ_2:120;
      z`1 = x1 by A10,EUCLID:56;
      then
A11:  y1 <= 2 * x1 - 1 by A9,A10,EUCLID:56;
      set Y = [x1, y1];
A12:  Y in [:the carrier of R^1, the carrier of R^1:]
      by TOPMETR:24,ZFMISC_1:106;
      then
A13:  Y in the carrier of GG by BORSUK_1:def 5;
      reconsider Y as Point of GG by A12,BORSUK_1:def 5;
      Y`1 = x1 & Y`2 = y1 by MCART_1:7;
      then
A14:  Y in K by A11;
A15:  Y in dom f by A13,FUNCT_2:def 1;
      x = f.Y by A1,A9,A10;
      hence thesis by A14,A15,FUNCT_1:def 12;
    end;
  end;
  hence thesis by A2,Th19,TOPS_2:72;
end;

theorem Th27:
  { p where p is Point of [:R^1,R^1:] :
  p`2 >= 1 - 2 * (p`1) & p`2 >= 2 * (p`1) - 1 }
  is closed Subset of [:R^1,R^1:]
proof
  set GG = [:R^1,R^1:], SS = TOP-REAL 2;
  defpred P[Point of GG] means
  $1`2 >= 1 - 2 * ($1`1) & $1`2 >= 2 * ($1`1) - 1;
  defpred R[Point of SS] means
  $1`2 >= 1 - 2 * ($1`1) & $1`2 >= 2 * ($1`1) - 1;
  reconsider K = { p where p is Point of GG : P[p] } as Subset of GG
  from DOMAIN_1:sch 7;
  reconsider L = { p where p is Point of SS : R[p] } as Subset of SS
  from DOMAIN_1:sch 7;
  consider f being Function of GG, SS such that
A1: for x, y being Real holds f. [x,y] = <*x,y*> by Th24;
A2: f is_homeomorphism by A1,TOPREAL6:85;
  f .: K = L
  proof
    thus f .: K c= L
    proof
      let x be set;
      assume x in f .: K;
      then consider y being set such that
A3:   y in dom f & y in K & x = f.y by FUNCT_1:def 12;
      consider z being Point of GG such that
A4:   z = y & P[z] by A3;
      z in the carrier of GG;
      then z in [:the carrier of R^1, the carrier of R^1:] by BORSUK_1:def 5;
      then consider x1, y1 being set such that
A5:   x1 in the carrier of R^1 & y1 in the carrier of R^1 & z = [x1, y1]
      by ZFMISC_1:def 2;
      reconsider x1, y1 as Real by A5,TOPMETR:24;
A6:   x = |[ x1, y1 ]| by A1,A3,A4,A5;
      then reconsider x' = x as Point of SS;
A7:   x'`1 = x1 by A6,FINSEQ_1:61;
A8:   x'`2 = y1 by A6,FINSEQ_1:61;
      z`1 = x1 & z`2 = y1 by A5,MCART_1:7;
      hence thesis by A4,A7,A8;
    end;
    thus L c= f .: K
    proof
      let x be set;
      assume x in L;
      then consider z being Point of SS such that
A9:   z = x & R[z];
      consider x1, y1 being Real such that
A10:  z = <*x1, y1*> by FINSEQ_2:120;
      z`1 = x1 by A10,EUCLID:56;
      then
A11:  y1 >= 1 - 2 * x1 & y1 >= 2 * x1 - 1 by A9,A10,EUCLID:56;
      set Y = [x1, y1];
A12:  Y in [:the carrier of R^1, the carrier of R^1:]
      by TOPMETR:24,ZFMISC_1:106;
      then
A13:  Y in the carrier of GG by BORSUK_1:def 5;
      reconsider Y as Point of GG by A12,BORSUK_1:def 5;
      Y`1 = x1 & Y`2 = y1 by MCART_1:7;
      then
A14:  Y in K by A11;
A15:  Y in dom f by A13,FUNCT_2:def 1;
      x = f.Y by A1,A9,A10;
      hence thesis by A14,A15,FUNCT_1:def 12;
    end;
  end;
  hence thesis by A2,Th23,TOPS_2:72;
end;

theorem Th28:
  { p where p is Point of [:I[01],I[01]:] : p`2 <= 1 - 2 * (p`1) }
  is closed non empty Subset of [:I[01],I[01]:]
proof
  set GG = [:I[01],I[01]:], SS = [:R^1,R^1:];
  0 in the carrier of I[01] by BORSUK_1:86;
  then [0,0] in [:the carrier of I[01], the carrier of I[01]:]
  by ZFMISC_1:106;
  then reconsider x = [0,0] as Point of GG by BORSUK_1:def 5;
  x`1 = 0 & x`2 = 0 by MCART_1:7;
  then
A1: x`2 <= 1 - 2 * (x`1);
  set P0 = { p where p is Point of GG : p`2 <= 1 - 2 * (p`1) };
A2: x in P0 by A1;
  reconsider PA = { p where p is Point of SS : p`2 <= 1 - 2 * (p`1) }
  as closed Subset of SS by Th25;
A3: GG is SubSpace of SS by BORSUK_3:25;
  P0 = PA /\ [#] GG
  proof
    thus P0 c= PA /\ [#] GG
    proof
      let x be set;
      assume x in P0;
      then consider p being Point of GG such that
A4:   x = p & p`2 <= 1 - 2 * (p`1);
A5:   x in the carrier of GG by A4;
      the carrier of GG c= the carrier of SS by A3,BORSUK_1:35;
      then reconsider a = x as Point of SS by A5;
      a`2 <= 1 - 2 * (a`1) by A4;
      then x in PA;
      hence thesis by A4,XBOOLE_0:def 3;
    end;
    let x be set;
    assume
A6: x in PA /\ [#] GG;
    then x in PA & x in [#] GG by XBOOLE_0:def 3;
    then ex p being Point of SS st x = p & p`2 <= 1 - 2 * (p`1);
    hence thesis by A6;
  end;
  hence thesis by A2,A3,PRE_TOPC:43;
end;

theorem Th29:
  { p where p is Point of [:I[01],I[01]:] :
  p`2 >= 1 - 2 * (p`1) & p`2 >= 2 * (p`1) - 1 }
  is closed non empty Subset of [:I[01],I[01]:]
proof
  set GG = [:I[01],I[01]:], SS = [:R^1,R^1:];
  1 in the carrier of I[01] by BORSUK_1:86;
  then [1,1] in [:the carrier of I[01], the carrier of I[01]:]
  by ZFMISC_1:106;
  then reconsider x = [1,1] as Point of GG by BORSUK_1:def 5;
  x`1 = 1 & x`2 = 1 by MCART_1:7;
  then
A1: x`2 >= 1 - 2 * (x`1) & x`2 >= 2 * (x`1) - 1;
  set P0 = { p where p is Point of GG : p`2 >= 1 - 2 * (p`1) &
  p`2 >= 2 * (p`1) - 1 };
A2: x in P0 by A1;
  reconsider PA = { p where p is Point of SS :
  p`2 >= 1 - 2 * (p`1) & p`2 >= 2 * (p`1) - 1 }
  as closed Subset of SS by Th27;
A3: GG is SubSpace of SS by BORSUK_3:25;
  P0 = PA /\ [#] GG
  proof
    thus P0 c= PA /\ [#] GG
    proof
      let x be set;
      assume x in P0;
      then consider p being Point of GG such that
A4:   x = p & p`2 >= 1 - 2 * (p`1) & p`2 >= 2 * (p`1) - 1;
A5:   x in the carrier of GG by A4;
      the carrier of GG c= the carrier of SS by A3,BORSUK_1:35;
      then reconsider a = x as Point of SS by A5;
      a`2 >= 1 - 2 * (a`1) & a`2 >= 2 * (a`1) - 1 by A4;
      then x in PA;
      hence thesis by A4,XBOOLE_0:def 3;
    end;
    let x be set;
    assume
A6: x in PA /\ [#] GG;
    then x in PA & x in [#] GG by XBOOLE_0:def 3;
    then ex p being Point of SS st
    x = p & p`2 >= 1 - 2 * (p`1) & p`2 >= 2 * (p`1) - 1;
    hence thesis by A6;
  end;
  hence thesis by A2,A3,PRE_TOPC:43;
end;

theorem Th30:
  { p where p is Point of [:I[01],I[01]:] : p`2 <= 2 * (p`1) - 1 }
  is closed non empty Subset of [:I[01],I[01]:]
proof
  set GG = [:I[01],I[01]:], SS = [:R^1,R^1:];
  0 in the carrier of I[01] & 1 in the carrier of I[01] by BORSUK_1:86;
  then [1,0] in [:the carrier of I[01], the carrier of I[01]:]
  by ZFMISC_1:106;
  then reconsider x = [1,0] as Point of GG by BORSUK_1:def 5;
  x`1 = 1 & x`2 = 0 by MCART_1:7;
  then
A1: x`2 <= 2 * (x`1) - 1;
  set P0 = { p where p is Point of GG : p`2 <= 2 * (p`1) - 1 };
A2: x in P0 by A1;
  reconsider PA = { p where p is Point of SS : p`2 <= 2 * (p`1) - 1 }
  as closed Subset of SS by Th26;
A3: GG is SubSpace of SS by BORSUK_3:25;
  P0 = PA /\ [#] GG
  proof
    thus P0 c= PA /\ [#] GG
    proof
      let x be set;
      assume x in P0;
      then consider p being Point of GG such that
A4:   x = p & p`2 <= 2 * (p`1) - 1;
A5:   x in the carrier of GG by A4;
      the carrier of GG c= the carrier of SS by A3,BORSUK_1:35;
      then reconsider a = x as Point of SS by A5;
      a`2 <= 2 * (a`1) - 1 by A4;
      then x in PA;
      hence thesis by A4,XBOOLE_0:def 3;
    end;
    let x be set;
    assume
A6: x in PA /\ [#] GG;
    then x in PA & x in [#] GG by XBOOLE_0:def 3;
    then ex p being Point of SS st x = p & p`2 <= 2 * (p`1) - 1;
    hence thesis by A6;
  end;
  hence thesis by A2,A3,PRE_TOPC:43;
end;

theorem Th31:
  for S, T being non empty TopSpace, p being Point of [:S, T:] holds
  p`1 is Point of S & p`2 is Point of T
proof
  let S, T be non empty TopSpace, p be Point of [:S, T:];
  p in the carrier of [:S, T:];
  then p in [:the carrier of S, the carrier of T:] by BORSUK_1:def 5;
  hence thesis by MCART_1:10;
end;

theorem Th32:
  for A, B being Subset of [:I[01],I[01]:] st
  A = [:[.0,1/2.], [.0,1.]:] & B = [:[.1/2,1.], [.0,1.]:] holds
  [#] ([:I[01],I[01]:] | A) \/ [#] ([:I[01],I[01]:] | B) = [#] [:I[01],I[01]:]
proof
  let A, B be Subset of [:I[01],I[01]:];
  assume that
A1: A = [:[.0,1/2.], [.0,1.]:] and
A2: B = [:[.1/2,1.], [.0,1.]:];
  [#] ([:I[01],I[01]:] | A) \/ [#] ([:I[01],I[01]:] | B)
  = A \/ [#] ([:I[01],I[01]:] | B) by PRE_TOPC:def 10
    .= A \/ B by PRE_TOPC:def 10
    .= [:[.0,1/2.] \/ [.1/2,1.], [.0,1.]:]
  by A1,A2,ZFMISC_1:120
    .= [:[.0,1.], [.0,1.]:] by XXREAL_1:174
    .= [#] [:I[01],I[01]:] by BORSUK_1:83,def 5;
  hence thesis;
end;

theorem Th33:
  for A, B being Subset of [:I[01],I[01]:] st
  A = [:[.0,1/2.], [.0,1.]:] & B = [:[.1/2,1.], [.0,1.]:] holds
  [#] ([:I[01],I[01]:] | A) /\ [#] ([:I[01],I[01]:] | B) = [:{1/2}, [.0,1.] :]
proof
  let A, B be Subset of [:I[01],I[01]:];
  assume that
A1: A = [:[.0,1/2.], [.0,1.]:] and
A2: B = [:[.1/2,1.], [.0,1.]:];
  [#] ([:I[01],I[01]:] | A) /\ [#] ([:I[01],I[01]:] | B) =
  A /\ [#] ([:I[01],I[01]:] | B) by PRE_TOPC:def 10
    .= A /\ B by PRE_TOPC:def 10
    .= [:[.0,1/2.] /\ [.1/2,1.], [.0,1.]:] by A1,A2,ZFMISC_1:122
    .= [:{1/2}, [.0,1.]:] by TOPMETR2:1;
  hence thesis;
end;

begin :: Compact Spaces

registration
  let T be TopStruct;
  cluster {}T -> compact;
  coherence by COMPTS_1:9;
end;

registration
  let T be TopStruct;
  cluster empty compact Subset of T;
  existence
  proof
    take {}T;
    thus {}T is empty;
    thus {}T is compact;
    thus thesis;
  end;
end;

theorem Th34:
  for T being TopStruct holds {} is empty compact Subset of T
proof
  let T be TopStruct;
  {}T c= the carrier of T;
  hence thesis;
end;

theorem Th35:
  for T being TopStruct, a, b being real number st a > b holds
  [.a,b.] is empty compact Subset of T
proof
  let T be TopStruct, a, b be real number;
  assume a > b;
  then [.a,b.] = {}T by XXREAL_1:29;
  hence thesis;
end;

theorem
  for a, b, c, d being Point of I[01] holds
  [:[.a,b.], [.c,d.]:] is compact Subset of [:I[01], I[01]:]
proof
  let a, b, c, d be Point of I[01];
  per cases;
  suppose a <= b & c <= d;
    hence thesis by Th13;
  end;
  suppose a > b & c <= d;
    then reconsider A = [.a,b.] as empty Subset of I[01] by Th35;
    [:A, [.c,d.]:] = {};
    hence thesis by Th34;
  end;
  suppose a > b & c > d;
    then reconsider A = [.c,d.] as empty Subset of I[01] by Th35;
    [:[.a,b.], A:] = {};
    hence thesis by Th34;
  end;
  suppose a <= b & c > d;
    then reconsider A = [.c,d.] as empty Subset of I[01] by Th35;
    [:[.a,b.], A:] = {};
    hence thesis by Th34;
  end;
end;

begin :: Continuous Maps

definition
  let a, b, c, d be real number;
  canceled;
  func L[01](a,b,c,d) -> Function of
  Closed-Interval-TSpace(a,b),Closed-Interval-TSpace(c,d) equals
  L[01]((#)(c,d),(c,d)(#)) * P[01](a,b,(#)(0,1),(0,1)(#));
  correctness;
end;

theorem Th37:
  for a, b, c, d being real number st a < b & c < d holds
  L[01](a,b,c,d).a = c & L[01](a,b,c,d).b = d
proof
  let a, b, c, d be real number;
  assume
A1: a < b & c < d;
  then a in [.a,b.] by XXREAL_1:1;
  then a in the carrier of Closed-Interval-TSpace (a,b) by A1,TOPMETR:25;
  then a in dom P[01](a,b,(#)(0,1),(0,1)(#)) by FUNCT_2:def 1;
  hence L[01](a,b,c,d).a =
  L[01]((#)(c,d),(c,d)(#)).(P[01](a,b,(#)(0,1),(0,1)(#)).a) by FUNCT_1:23
    .= L[01]((#)(c,d),(c,d)(#)).(P[01](a,b,(#)(0,1),(0,1)(#)).(#)(a,b))
  by A1,TREAL_1:def 1
    .= L[01]((#)(c,d),(c,d)(#)).((#)(0,1)) by A1,TREAL_1:16
    .= (#)(c,d) by A1,TREAL_1:12
    .= c by A1,TREAL_1:def 1;
  b in [.a,b.] by A1,XXREAL_1:1;
  then b in the carrier of Closed-Interval-TSpace (a,b) by A1,TOPMETR:25;
  then b in dom P[01](a,b,(#)(0,1),(0,1)(#)) by FUNCT_2:def 1;
  hence L[01](a,b,c,d).b =
  L[01]((#)(c,d),(c,d)(#)).(P[01](a,b,(#)(0,1),(0,1)(#)).b) by FUNCT_1:23
    .= L[01]((#)(c,d),(c,d)(#)).(P[01](a,b,(#)(0,1),(0,1)(#)).(a,b)(#))
  by A1,TREAL_1:def 2
    .= L[01]((#)(c,d),(c,d)(#)).((0,1)(#)) by A1,TREAL_1:16
    .= (c,d)(#) by A1,TREAL_1:12
    .= d by A1,TREAL_1:def 2;
end;

theorem Th38:
  for a, b, c, d being real number st a < b & c <= d holds
  L[01](a,b,c,d) is continuous Function of
  Closed-Interval-TSpace(a,b), Closed-Interval-TSpace(c,d)
proof
  let a, b, c, d be real number;
  assume
A1: a < b & c <= d;
  then
A2: L[01]((#)(c,d),(c,d)(#)) is continuous Function of
  Closed-Interval-TSpace(0,1),Closed-Interval-TSpace(c,d) by TREAL_1:11;
  P[01](a,b,(#)(0,1),(0,1)(#)) is continuous Function of
  Closed-Interval-TSpace(a,b),Closed-Interval-TSpace(0,1) by A1,TREAL_1:15;
  hence thesis by A2;
end;

theorem Th39:
  for a, b, c, d being real number st a < b & c <= d
  for x being real number st a <= x & x <= b holds
  L[01](a,b,c,d).x = ((d - c)/(b - a)) * (x - a) + c
proof
  let a, b, c, d be real number;
  assume
A1: a < b;
  assume
A2: c <= d;
  let x be real number;
  assume
A3: a <= x;
  assume
A4: x <= b;
  set f = L[01](a,b,c,d);
  set F = L[01]((#)(c,d),(c,d)(#));
  set G = P[01](a,b,(#)(0,1),(0,1)(#));
A5: (#)(c,d) = c & (c,d)(#) = d by A2,TREAL_1:def 1,def 2;
  x in [.a,b.] by A3,A4,XXREAL_1:1;
  then
A6: x in the carrier of Closed-Interval-TSpace (a,b) by A1,TOPMETR:25;
  then
A7: x in dom G by FUNCT_2:def 1;
A8: 0 = (#)(0,1) & 1 = (0,1)(#) by TREAL_1:def 1,def 2;
  set X = (x-a)/(b-a);
A9: X in the carrier of Closed-Interval-TSpace (0,1) by A3,A4,Th5;
  f.x = F.(G.x) by A7,FUNCT_1:23
    .= F.(((b-x)*0 + (x-a)*1)/(b-a)) by A1,A6,A8,TREAL_1:def 4
    .= (1 - X)*c + X * d by A2,A5,A9,TREAL_1:def 3
    .= ((d - c)/(b - a)) * (x - a) + c by XCMPLX_1:236;
  hence L[01](a,b,c,d).x = ((d - c)/(b - a)) * (x - a) + c;
end;

theorem Th40:
  for f1,f2 being Function of [:I[01],I[01]:],I[01] st
  f1 is continuous & f2 is continuous &
  (for p being Point of [:I[01],I[01]:] holds
  f1.p * f2.p is Point of I[01]) holds
  ex g being Function of [:I[01],I[01]:],I[01] st
  (for p being Point of [:I[01],I[01]:],r1,r2 being real number st
  f1.p=r1 & f2.p=r2 holds g.p=r1*r2) & g is continuous
proof
  let f1,f2 be Function of [:I[01],I[01]:],I[01];
  assume
A1: f1 is continuous & f2 is continuous &
  (for p being Point of [:I[01],I[01]:] holds f1.p * f2.p is Point of I[01]);
  set X = [:I[01],I[01]:];
  reconsider f1' = f1, f2' = f2 as Function of X, R^1
  by BORSUK_1:83,FUNCT_2:9,TOPMETR:24;
  f1' is continuous & f2' is continuous by A1,TOPMETR:7;
  then consider g being Function of X,R^1 such that
A2: (for p being Point of X,r1,r2 being real number st
  f1'.p=r1 & f2'.p=r2 holds g.p=r1*r2) & g is continuous by JGRAPH_2:35;
  reconsider A = [.0,1.] as non empty Subset of R^1 by XXREAL_1:1,TOPMETR:24;
A3: [.0,1.] = the carrier of R^1|A by PRE_TOPC:29;
A4: rng g c= [.0,1.]
  proof
    let x be set;
    assume x in rng g;
    then consider y being set such that
A5: y in dom g & x = g.y by FUNCT_1:def 5;
    reconsider y as Point of X by A5;
    g.y = f1.y * f2.y by A2;
    then g.y is Point of I[01] by A1;
    hence thesis by A5,BORSUK_1:83;
  end;
  dom g = the carrier of X by FUNCT_2:def 1;
  then reconsider g as Function of X, R^1|A by A3,A4,FUNCT_2:4;
  R^1 | A = I[01] by BORSUK_1:def 16,TOPMETR:def 7;
  then reconsider g as continuous Function of X, I[01] by A2,JGRAPH_1:63;
  take g;
  thus thesis by A2;
end;

theorem Th41:
  for f1,f2 being Function of [:I[01],I[01]:],I[01] st
  f1 is continuous & f2 is continuous &
  (for p being Point of [:I[01],I[01]:] holds f1.p + f2.p is Point of I[01])
  holds ex g being Function of [:I[01],I[01]:],I[01] st
  (for p being Point of [:I[01],I[01]:],r1,r2 being real number st
  f1.p=r1 & f2.p=r2 holds g.p=r1+r2) & g is continuous
proof
  let f1,f2 be Function of [:I[01],I[01]:],I[01];
  assume
A1: f1 is continuous & f2 is continuous &
  (for p being Point of [:I[01],I[01]:] holds f1.p + f2.p is Point of I[01]);
  set X = [:I[01],I[01]:];
  reconsider f1' = f1, f2' = f2 as Function of X, R^1
  by BORSUK_1:83,FUNCT_2:9,TOPMETR:24;
  f1' is continuous & f2' is continuous by A1,TOPMETR:7;
  then consider g being Function of X,R^1 such that
A2: (for p being Point of X,r1,r2 being real number st
  f1'.p=r1 & f2'.p=r2 holds g.p=r1+r2) & g is continuous by JGRAPH_2:29;
  reconsider A = [.0,1.] as non empty Subset of R^1 by XXREAL_1:1,TOPMETR:24;
A3: [.0,1.] = the carrier of R^1|A by PRE_TOPC:29;
A4: rng g c= [.0,1.]
  proof
    let x be set;
    assume x in rng g;
    then consider y being set such that
A5: y in dom g & x = g.y by FUNCT_1:def 5;
    reconsider y as Point of X by A5;
    g.y = f1.y + f2.y by A2;
    then g.y is Point of I[01] by A1;
    hence thesis by A5,BORSUK_1:83;
  end;
  dom g = the carrier of X by FUNCT_2:def 1;
  then reconsider g as Function of X, R^1|A by A3,A4,FUNCT_2:4;
  R^1 | A = I[01] by BORSUK_1:def 16,TOPMETR:def 7;
  then reconsider g as continuous Function of X, I[01] by A2,JGRAPH_1:63;
  take g;
  thus thesis by A2;
end;

theorem
  for f1,f2 being Function of [:I[01],I[01]:],I[01] st
  f1 is continuous & f2 is continuous &
  (for p being Point of [:I[01],I[01]:] holds f1.p - f2.p is Point of I[01])
  holds ex g being Function of [:I[01],I[01]:],I[01] st
  (for p being Point of [:I[01],I[01]:],r1,r2 being real number st
  f1.p=r1 & f2.p=r2 holds g.p=r1-r2) & g is continuous
proof
  let f1,f2 be Function of [:I[01],I[01]:],I[01];
  assume
A1: f1 is continuous & f2 is continuous &
  (for p being Point of [:I[01],I[01]:] holds f1.p - f2.p is Point of I[01]);
  set X = [:I[01],I[01]:];
  reconsider f1' = f1, f2' = f2 as Function of X, R^1
  by BORSUK_1:83,FUNCT_2:9,TOPMETR:24;
  f1' is continuous & f2' is continuous by A1,TOPMETR:7;
  then consider g being Function of X,R^1 such that
A2: (for p being Point of X,r1,r2 being real number st
  f1'.p=r1 & f2'.p=r2 holds g.p=r1-r2) & g is continuous by JGRAPH_2:31;
  reconsider A = [.0,1.] as non empty Subset of R^1 by XXREAL_1:1,TOPMETR:24;
A3: [.0,1.] = the carrier of R^1|A by PRE_TOPC:29;
A4: rng g c= [.0,1.]
  proof
    let x be set;
    assume x in rng g;
    then consider y being set such that
A5: y in dom g & x = g.y by FUNCT_1:def 5;
    reconsider y as Point of X by A5;
    g.y = f1.y - f2.y by A2;
    then g.y is Point of I[01] by A1;
    hence thesis by A5,BORSUK_1:83;
  end;
  dom g = the carrier of X by FUNCT_2:def 1;
  then reconsider g as Function of X, R^1|A by A3,A4,FUNCT_2:4;
  R^1 | A = I[01] by BORSUK_1:def 16,TOPMETR:def 7;
  then reconsider g as continuous Function of X, I[01] by A2,JGRAPH_1:63;
  take g;
  thus thesis by A2;
end;

begin :: Paths

reserve T for non empty TopSpace,
  a, b, c, d for Point of T;

theorem Th43:
  for P being Path of a,b st P is continuous holds
  P * L[01]((0,1)(#),(#)(0,1)) is continuous Function of I[01], T
proof
  let P be Path of a,b such that
A1: P is continuous;
  reconsider g = L[01]((0,1)(#),(#)(0,1)) as Function of I[01], I[01]
  by TOPMETR:27;
  reconsider f = P * g as Function of I[01], T;
  g is continuous by TOPMETR:27,TREAL_1:11;
  then f is continuous by A1;
  hence P * L[01]((0,1)(#),(#)(0,1)) is continuous Function of I[01], T;
end;

theorem Th44:
  for X being non empty TopStruct, a, b being Point of X,
  P being Path of a,b st P.0 = a & P.1 = b holds
  (P * L[01]((0,1)(#),(#)(0,1))).0 = b & (P * L[01]((0,1)(#),(#)(0,1))).1 = a
proof
  let X be non empty TopStruct, a, b be Point of X;
  let P be Path of a,b such that
A1: P.0 = a and
A2: P.1 = b;
  set e = L[01]((0,1)(#),(#)(0,1));
A3: e.0 = e.(#)(0,1) by TREAL_1:def 1
    .= (0,1)(#) by TREAL_1:12
    .= 1 by TREAL_1:def 2;
A4: e.1 = e.(0,1)(#) by TREAL_1:def 2
    .= (#)(0,1) by TREAL_1:12
    .= 0 by TREAL_1:def 1;
A5: the carrier of Closed-Interval-TSpace(0,1) = [. 0,1 .] by TOPMETR:25;
  0 in [. 0,1 .] by XXREAL_1:1;
  hence (P * e).0 = b by A2,A3,A5,FUNCT_2:21;
  1 in [. 0,1 .] by XXREAL_1:1;
  hence (P * e).1 = a by A1,A4,A5,FUNCT_2:21;
end;

theorem Th45:
  for P being Path of a,b st P is continuous & P.0 = a & P.1 = b holds
  -P is continuous & (-P).0 = b & (-P).1 = a
proof
  let P be Path of a,b such that
A1: P is continuous and
A2: P.0 = a and
A3: P.1 = b;
  P * L[01]((0,1)(#),(#)(0,1)) is continuous Function of I[01], T &
  (P * L[01]((0,1)(#),(#)(0,1))).0 = b &
  (P * L[01]((0,1)(#),(#)(0,1))).1 = a by A1,A2,A3,Th43,Th44;
  then b,a are_connected by BORSUK_2:def 1;
  hence -P is continuous & (-P).0 = b & (-P).1 = a by BORSUK_2:def 2;
end;

definition
  let T be non empty TopSpace, a,b be Point of T;
  redefine pred a,b are_connected;
  reflexivity
  proof
    let a be Point of T;
    thus a,a are_connected;
  end;
  symmetry
  proof
    let a,b be Point of T;
    assume
A1: a,b are_connected;
    consider P being Path of a,b;
    take -P;
    P is continuous & P.0 = a & P.1 = b by A1,BORSUK_2:def 2;
    hence thesis by Th45;
  end;
end;

theorem Th46:
  a,b are_connected & b,c are_connected implies a,c are_connected
proof
  assume that
A1: a,b are_connected and
A2: b,c are_connected;
  consider P being Path of a,b, R being Path of b,c;
  take P+R;
  P is continuous & P.0 = a & P.1 = b &
  R is continuous & R.0 = b & R.1 = c by A1,A2,BORSUK_2:def 2;
  hence thesis by BORSUK_2:17;
end;

canceled 3;

theorem Th50:
  a,b are_connected implies for A being Path of a,b holds A = --A
proof
  assume
A1: a,b are_connected;
  let A be Path of a,b;
  set I = the carrier of I[01];
  for x being Element of I holds A.x = (--A).x
  proof
    let x be Element of I;
    reconsider z = 1-x as Point of I[01] by JORDAN5B:4;
    thus (--A).x = (-A).(1-x) by A1,BORSUK_2:def 6
      .= A.(1-z) by A1,BORSUK_2:def 6
      .= A.x;
  end;
  hence A = --A by FUNCT_2:113;
end;

theorem
  for T being non empty arcwise_connected TopSpace, a, b being Point of T
  for A being Path of a,b holds A = --A
proof
  let T be non empty arcwise_connected TopSpace, a, b be Point of T;
  a,b are_connected by BORSUK_2:def 3;
  hence thesis by Th50;
end;

begin :: Reexamination of a Path Concept

definition
  let T be non empty arcwise_connected TopSpace;
  let a, b, c be Point of T;
  let P be Path of a, b, Q be Path of b, c;
  redefine
  canceled;
  func P + Q means

  for t being Point of I[01] holds
  ( t <= 1/2 implies it.t = P.(2*t) ) & ( 1/2 <= t implies it.t = Q.(2*t-1) );
  compatibility
  proof
    let X be Path of a, c;
    a,b are_connected & b,c are_connected by BORSUK_2:def 3;
    hence thesis by BORSUK_2:def 5;
  end;
end;

definition
  let T be non empty arcwise_connected TopSpace;
  let a, b be Point of T;
  let P be Path of a, b;
  redefine func - P means
  :Def5:
  for t being Point of I[01] holds it.t = P.(1-t);
  compatibility
  proof
    let X be Path of b, a;
    b,a are_connected by BORSUK_2:def 3;
    hence thesis by BORSUK_2:def 6;
  end;
end;

begin :: Reparametrizations

definition
  let T be non empty TopSpace, a, b be Point of T;
  let P be Path of a, b;
  let f be continuous Function of I[01], I[01];
  assume
A1: f.0 = 0 & f.1 = 1 & a, b are_connected;
  func RePar (P, f) -> Path of a, b equals
  :Def6:
  P * f;
  coherence
  proof
    set PF = P * f;
    0 in the carrier of I[01] by BORSUK_1:86;
    then 0 in dom f by FUNCT_2:def 1;
    then
A2: PF.0 = P.(f.0) by FUNCT_1:23
      .= a by A1,BORSUK_2:def 2;
    1 in the carrier of I[01] by BORSUK_1:86;
    then 1 in dom f by FUNCT_2:def 1;
    then
A3: PF.1 = P.(f.1) by FUNCT_1:23
      .= b by A1,BORSUK_2:def 2;
    P is continuous by A1,BORSUK_2:def 2;
    then PF is continuous;
    hence thesis by A1,A2,A3,BORSUK_2:def 2;
  end;
end;

canceled;

theorem Th53:
  for P being Path of a, b, f being continuous Function of I[01], I[01] st
  f.0 = 0 & f.1 = 1 & a, b are_connected holds RePar (P, f), P are_homotopic
proof
  let P be Path of a, b, f be continuous Function of I[01], I[01];
  assume
A1: f.0 = 0 & f.1 = 1 & a,b are_connected;
  set Q = RePar (P,f);
A2: 0 is Point of I[01] & 1 is Point of I[01] by BORSUK_1:86;
  set X = [:I[01], I[01]:];
  reconsider ID = id I[01] as Path of 0[01], 1[01] by Th12;
  set G1 = -ID;
  reconsider G2 = pr2 (the carrier of I[01], the carrier of I[01])
  as continuous Function of X, I[01] by YELLOW12:40;
  reconsider f1 = G1 * G2 as continuous Function of X, I[01];
A3: for s, t being Point of I[01] holds f1. [s,t] = 1 - t
  proof
    let s, t be Point of I[01];
A4: 1 - t in the carrier of I[01] by JORDAN5B:4;
    [s,t] in [:the carrier of I[01],the carrier of I[01]:] by ZFMISC_1:106;
    then [s,t] in dom G2 by FUNCT_2:def 1;
    then f1. [s,t] = G1. (G2.(s,t)) by FUNCT_1:23
      .= G1. t by FUNCT_3:def 6
      .= ID.(1 - t) by Def5
      .= 1 - t by A4,TMAP_1:91;
    hence thesis;
  end;
  reconsider F2 = pr1 (the carrier of I[01], the carrier of I[01])
  as continuous Function of X, I[01] by YELLOW12:39;
  reconsider f2 = f * F2 as continuous Function of X, I[01];
A5: for s, t being Point of I[01] holds f2.(s,t) = f.s
  proof
    let s, t be Point of I[01];
    [s,t] in [:the carrier of I[01],the carrier of I[01]:] by ZFMISC_1:106;
    then [s,t] in dom F2 by FUNCT_2:def 1;
    hence f2.(s,t) = f.(F2.(s,t)) by FUNCT_1:23
      .= f.s by FUNCT_3:def 5;
  end;
  reconsider f3 = pr1 (the carrier of I[01], the carrier of I[01]) as
  continuous Function of X, I[01] by YELLOW12:39;
  reconsider f4 = pr2 (the carrier of I[01], the carrier of I[01]) as
  continuous Function of X, I[01] by YELLOW12:40;
A6: for p being Point of X holds f1.p * f2.p is Point of I[01] by Th8;
A7: for p being Point of X holds f3.p * f4.p is Point of I[01] by Th8;
  consider g1 being Function of X,I[01] such that
A8: (for p being Point of X,r1,r2 being real number st
  f1.p=r1 & f2.p=r2 holds g1.p=r1*r2) & g1 is continuous by A6,Th40;
A9: for t, s being Point of I[01] holds g1. [s,t] = (1 - t) * f.s
  proof
    let t,s be Point of I[01];
    f1.(s,t) = 1 - t & f2.(s,t) = f.s by A3,A5;
    hence thesis by A8;
  end;
  consider g2 being Function of X,I[01] such that
A10: (for p being Point of X,r1,r2 being real number st
  f3.p=r1 & f4.p=r2 holds g2.p=r1*r2) & g2 is continuous by A7,Th40;
A11: for t, s being Point of I[01] holds g2. [s,t] = t * s
  proof
    let t, s being Point of I[01];
    f3.(s,t) = s & f4.(s,t) = t by FUNCT_3:def 5,def 6;
    hence thesis by A10;
  end;
  for p being Point of X holds g1.p + g2.p is Point of I[01]
  proof
    let p be Point of X;
    p in the carrier of [:I[01],I[01]:];
    then p in [:the carrier of I[01], the carrier of I[01]:]
    by BORSUK_1:def 5;
    then consider s, t being set such that
A12: s in the carrier of I[01] & t in the carrier of I[01] & p = [s,t]
    by ZFMISC_1:def 2;
    reconsider s, t as Point of I[01] by A12;
    set a = f.s;
    per cases;
    suppose
A13:  f.s <= s;
      0 <= t & t <= 1 by BORSUK_1:83,XXREAL_1:1;
      then
A14:  a<=(1-t)*a+t*s & (1-t)*a+t*s<=s by A13,XREAL_1:174,175;
A15:  g1.p + g2.p = (1 - t) * f.s + g2.p by A9,A12
        .= (1 - t) * f.s + t * s by A11,A12;
A16:  0 <= a by BORSUK_1:83,XXREAL_1:1;
      s <= 1 by BORSUK_1:83,XXREAL_1:1;
      then (1-t)*a+t*s <= 1 by A14,XXREAL_0:2;
      hence thesis by A14,A15,A16,BORSUK_1:83,XXREAL_1:1;
    end;
    suppose
A17:  a > s;
      set j = 1 - t;
      j in the carrier of I[01] by JORDAN5B:4;
      then 0 <= j & j <= 1 by BORSUK_1:86;
      then
A18:  s <= (1 - j)*s + j * a & (1 - j)*s + j * a <= a by A17,XREAL_1:174,175;
A19:  g1.p + g2.p = (1 - t) * f.s + g2.p by A9,A12
        .= (1 - t) * f.s + t * s by A11,A12;
A20:  0 <= s by BORSUK_1:83,XXREAL_1:1;
      a <= 1 by BORSUK_1:83,XXREAL_1:1;
      then (1-t)*a+t*s <= 1 by A18,XXREAL_0:2;
      hence thesis by A18,A19,A20,BORSUK_1:83,XXREAL_1:1;
    end;
  end;
  then consider h being Function of X,I[01] such that
A21: (for p being Point of X,r1,r2 being real number st
  g1.p=r1 & g2.p=r2 holds h.p=r1+r2) & h is continuous by A8,A10,Th41;
A22: for t, s being Point of I[01] holds h. [s,t] = (1 - t) * f.s + t * s
  proof
    let t, s being Point of I[01];
    g1. [s,t] = (1 - t) * f.s & g2. [s,t] = t * s by A9,A11;
    hence thesis by A21;
  end;
A23: for s being Point of I[01] holds h. [s,0] = f.s
  proof
    let s be Point of I[01];
    thus h. [s,0] = (1 - 0) * f.s + 0 * s by A2,A22
      .= f.s;
  end;
A24: for s being Point of I[01] holds h. [s,1] = s
  proof
    let s be Point of I[01];
    thus h. [s,1] = (1 - 1) * f.s + 1 * s by A2,A22
      .= s;
  end;
A25: for t being Point of I[01] holds h. [0,t] = 0
  proof
    let t be Point of I[01];
    reconsider oo = 0 as Point of I[01] by BORSUK_1:86;
    thus h. [0,t] = (1 - t) * f.oo + t * 0 by A22
      .= 0 by A1;
  end;
A26: for t being Point of I[01] holds h. [1,t] = 1
  proof
    let t be Point of I[01];
    reconsider oo = 1 as Point of I[01] by BORSUK_1:86;
    thus h. [1,t] = (1 - t) * f.oo + t * 1 by A22
      .= 1 by A1;
  end;
A27: dom h = the carrier of [:I[01],I[01]:] by FUNCT_2:def 1
    .= [:the carrier of I[01],the carrier of I[01]:] by BORSUK_1:def 5;
  set H = P * h;
  P is continuous by A1,BORSUK_2:def 2;
  then
A28: H is continuous by A21;
A29: for s being Point of I[01] holds H.(s,0) = Q.s & H.(s,1) = P.s
  proof
    let s be Point of I[01];
    s in the carrier of I[01] & 0 in the carrier of I[01] by BORSUK_1:86;
    then
A30: [s,0] in dom h by A27,ZFMISC_1:106;
    1 in the carrier of I[01] by BORSUK_1:86;
    then
A31: [s,1] in dom h by A27,ZFMISC_1:106;
    s in the carrier of I[01];
    then
A32: s in dom f by FUNCT_2:def 1;
    thus H.(s,0) = P.(h. [s,0]) by A30,FUNCT_1:23
      .= P.(f.s) by A23
      .= (P * f).s by A32,FUNCT_1:23
      .= Q.s by A1,Def6;
    thus H.(s,1) = P. (h. [s,1]) by A31,FUNCT_1:23
      .= P.s by A24;
  end;
  for t being Point of I[01] holds H.(0,t) = a & H.(1,t) = b
  proof
    let t be Point of I[01];
    t in the carrier of I[01] & 0 in the carrier of I[01] by BORSUK_1:86;
    then
A33: [0,t] in dom h by A27,ZFMISC_1:106;
    1 in the carrier of I[01] by BORSUK_1:86;
    then
A34: [1,t] in dom h by A27,ZFMISC_1:106;
    thus H.(0,t) = P. (h. [0,t]) by A33,FUNCT_1:23
      .= P. 0 by A25
      .= a by A1,BORSUK_2:def 2;
    thus H.(1,t) = P. (h. [1,t]) by A34,FUNCT_1:23
      .= P. 1 by A26
      .= b by A1,BORSUK_2:def 2;
  end;
  hence thesis by A28,A29,BORSUK_2:def 7;
end;

theorem
  for T being non empty arcwise_connected TopSpace, a, b be Point of T,
  P being Path of a, b, f being continuous Function of I[01], I[01] st
  f.0 = 0 & f.1 = 1 holds RePar (P, f), P are_homotopic
proof
  let T be non empty arcwise_connected TopSpace, a, b be Point of T,
  P be Path of a, b, f be continuous Function of I[01], I[01];
  a, b are_connected by BORSUK_2:def 3;
  hence thesis by Th53;
end;

definition
  func 1RP -> Function of I[01], I[01] means
  :Def7:
  for t being Point of I[01] holds (t <= 1/2 implies it.t = 2 * t) &
  (t > 1/2 implies it.t = 1);
  existence
  proof
    defpred P[real number] means $1 <= 1/2;
    deffunc F(real number) = 2 * $1;
    deffunc G(set) = 1;
    consider f being Function such that
A1: dom f = the carrier of I[01] & for x being Element of I[01] holds
    (P[x] implies f.x = F(x)) &
    (not P[x] implies f.x = G(x)) from PARTFUN1:sch 4;
    for x being set st x in the carrier of I[01] holds
    f.x in the carrier of I[01]
    proof
      let x be set;
      assume x in the carrier of I[01];
      then reconsider x as Point of I[01];
      per cases;
      suppose
A2:     P[x];
        then f.x = 2 * x by A1;
        then f.x is Point of I[01] by A2,Th6;
        hence thesis;
      end;
      suppose not P[x];
        then f.x = G(x) by A1;
        hence thesis by BORSUK_1:86;
      end;
    end;
    then reconsider f as Function of I[01], I[01] by A1,FUNCT_2:5;
    for t being Point of I[01] holds (t <= 1/2 implies f.t = 2 * t) &
    (t > 1/2 implies f.t = 1) by A1;
    hence thesis;
  end;
  uniqueness
  proof
    let f1, f2 be Function of I[01], I[01];
    assume that
A3: for t being Point of I[01] holds (t <= 1/2 implies f1.t = 2 * t) &
    (t > 1/2 implies f1.t = 1) and
A4: for t being Point of I[01] holds (t <= 1/2 implies f2.t = 2 * t) &
    (t > 1/2 implies f2.t = 1);
    for t being Point of I[01] holds f1.t = f2.t
    proof
      let t be Point of I[01];
      per cases;
      suppose
A5:     t <= 1/2;
        then f1.t = 2 * t by A3
          .= f2.t by A4,A5;
        hence thesis;
      end;
      suppose
A6:     t > 1/2;
        then f1.t = 1 by A3
          .= f2.t by A4,A6;
        hence thesis;
      end;
    end;
    hence thesis by FUNCT_2:113;
  end;
end;

registration
  cluster 1RP -> continuous;
  coherence
  proof
A1: 0 is Point of I[01] & 1/2 is Point of I[01] & 1 is Point of I[01]
    by BORSUK_1:86;
    then reconsider A = [.0,1/2.] as non empty compact Subset of I[01]
    by BORSUK_4:49;
    reconsider B = [.1/2,1.] as non empty compact Subset of I[01]
    by A1,BORSUK_4:49;
    set T1 = I[01]|A, T2 = I[01]|B, T = I[01];
    T1 = Closed-Interval-TSpace (0,1/2) by TOPMETR:31;
    then reconsider f = L[01](0,1/2,0,1) as continuous Function of T1, I[01]
    by Th38,TOPMETR:27;
    reconsider g = T2 --> 1[01] as continuous Function of T2, I[01];
A2: g = (the carrier of T2) --> 1 by BORSUK_1:def 2,def 18;
A3: ([#] T1) \/ ([#] T2) = [.0,1/2.] \/ ([#] T2) by PRE_TOPC:def 10
      .= [.0,1/2.] \/ [.1/2,1.] by PRE_TOPC:def 10
      .= [#] T by BORSUK_1:83,XXREAL_1:174;
    for p be set st p in ([#] T1) /\ ([#] T2) holds f.p = g.p
    proof
      let p be set;
      assume p in ([#] T1) /\ ([#] T2);
      then p in [.0,1/2.] /\ ([#] T2) by PRE_TOPC:def 10;
      then p in [.0,1/2.] /\ [.1/2,1.] by PRE_TOPC:def 10;
      then p in {1/2} by TOPMETR2:1;
      then
A4:   p = 1/2 by TARSKI:def 1;
      then p in [.1/2,1.] by XXREAL_1:1;
      then
A5:   p in the carrier of T2 by PRE_TOPC:29;
      f.p = ((1 - 0)/(1/2 - 0)) * (1/2 - 0) + 0 by A4,Th39
        .= g.p by A2,A5,FUNCOP_1:13;
      hence thesis;
    end;
    then consider h being Function of I[01], I[01] such that
A6: h = f +* g & h is continuous by A3,BORSUK_2:1;
    1RP = h
    proof
      for x being Element of I[01] holds 1RP.x = (f +* g).x
      proof
        let x be Element of I[01];
A7:     dom g = the carrier of T2 by FUNCT_2:def 1
          .= [.1/2,1.] by PRE_TOPC:29;
        per cases by REAL_1:def 5;
        suppose
A8:       x < 1/2;
          then
A9:       not x in dom g by A7,XXREAL_1:1;
          0 <= x by BORSUK_1:86;
          then
A10:      f.x = ((1 - 0)/(1/2 - 0)) * (x - 0) + 0 by A8,Th39
            .= (1/(1/2)) * x;
          thus 1RP.x = 2 * x by A8,Def7
            .= (f +* g).x by A9,A10,FUNCT_4:12;
        end;
        suppose
A11:      x = 1/2;
          then
A12:      x in dom g by A7,XXREAL_1:1;
          thus 1RP.x = 2 * (1/2) by A11,Def7
            .= g.x by A2,A12,FUNCOP_1:13
            .= (f +* g).x by A12,FUNCT_4:14;
        end;
        suppose
A13:      x > 1/2;
          x <= 1 by BORSUK_1:86;
          then
A14:      x in dom g by A7,A13,XXREAL_1:1;
          thus 1RP.x = 1 by A13,Def7
            .= g.x by A2,A14,FUNCOP_1:13
            .= (f +* g).x by A14,FUNCT_4:14;
        end;
      end;
      hence thesis by A6,FUNCT_2:113;
    end;
    hence thesis by A6;
  end;
end;

theorem Th55:
  1RP.0 = 0 & 1RP.1 = 1
proof
  reconsider x = 0, y = 1 as Point of I[01] by BORSUK_1:86;
  thus 1RP.0 = 2*x by Def7
    .= 0;
  thus 1RP.1 = 1RP.y
    .= 1 by Def7;
end;

definition
  func 2RP -> Function of I[01], I[01] means
  :Def8:
  for t being Point of I[01] holds (t <= 1/2 implies it.t = 0) &
  (t > 1/2 implies it.t = 2 * t - 1);
  existence
  proof
    defpred P[real number] means $1 <= 1/2;
    deffunc G(real number) = 2 * $1 - 1;
    deffunc F(set) = 0;
    consider f being Function such that
A1: dom f = the carrier of I[01] & for x being Element of I[01] holds
    (P[x] implies f.x = F(x)) &
    (not P[x] implies f.x = G(x)) from PARTFUN1:sch 4;
    for x being set st x in the carrier of I[01] holds
    f.x in the carrier of I[01]
    proof
      let x be set;
      assume x in the carrier of I[01];
      then reconsider x as Point of I[01];
      per cases;
      suppose P[x];
        then f.x = 0 by A1;
        hence thesis by BORSUK_1:86;
      end;
      suppose
A2:     not P[x];
        then f.x = G(x) by A1;
        then f.x is Point of I[01] by A2,Th7;
        hence thesis;
      end;
    end;
    then reconsider f as Function of I[01], I[01] by A1,FUNCT_2:5;
    for t being Point of I[01] holds (t <= 1/2 implies f.t = 0) &
    (t > 1/2 implies f.t = 2 * t - 1) by A1;
    hence thesis;
  end;
  uniqueness
  proof
    let f1, f2 be Function of I[01], I[01];
    assume that
A3: for t being Point of I[01] holds (t <= 1/2 implies f1.t = 0) &
    (t > 1/2 implies f1.t = 2 * t - 1) and
A4: for t being Point of I[01] holds (t <= 1/2 implies f2.t = 0) &
    (t > 1/2 implies f2.t = 2 * t - 1);
    for t being Point of I[01] holds f1.t = f2.t
    proof
      let t be Point of I[01];
      per cases;
      suppose
A5:     t <= 1/2;
        then f1.t = 0 by A3
          .= f2.t by A4,A5;
        hence thesis;
      end;
      suppose
A6:     t > 1/2;
        then f1.t = 2 * t - 1 by A3
          .= f2.t by A4,A6;
        hence thesis;
      end;
    end;
    hence thesis by FUNCT_2:113;
  end;
end;

registration
  cluster 2RP -> continuous;
  coherence
  proof
A1: 0 is Point of I[01] & 1/2 is Point of I[01] & 1 is Point of I[01]
    by BORSUK_1:86;
    then reconsider A = [.0,1/2.] as non empty compact Subset of I[01]
    by BORSUK_4:49;
    reconsider B = [.1/2,1.] as non empty compact Subset of I[01]
    by A1,BORSUK_4:49;
    set T1 = I[01]|A, T2 = I[01]|B, T = I[01];
    T2 = Closed-Interval-TSpace (1/2,1) by TOPMETR:31;
    then reconsider f = L[01](1/2,1,0,1) as continuous Function of T2, I[01]
    by Th38,TOPMETR:27;
    reconsider g = T1 --> 0[01] as continuous Function of T1, I[01];
A2: g = (the carrier of T1) --> 0 by BORSUK_1:def 2,def 17;
A3: ([#] T2) \/ ([#] T1) = [.0,1/2.] \/ ([#] T2) by PRE_TOPC:def 10
      .= [.0,1/2.] \/ [.1/2,1.] by PRE_TOPC:def 10
      .= [#] T by BORSUK_1:83,XXREAL_1:174;
    for p be set st p in ([#] T2) /\ ([#] T1) holds f.p = g.p
    proof
      let p be set;
      assume p in ([#] T2) /\ ([#] T1);
      then p in [.0,1/2.] /\ ([#] T2) by PRE_TOPC:def 10;
      then p in [.0,1/2.] /\ [.1/2,1.] by PRE_TOPC:def 10;
      then p in {1/2} by TOPMETR2:1;
      then
A4:   p = 1/2 by TARSKI:def 1;
      then p in [.0,1/2.] by XXREAL_1:1;
      then
A5:   p in the carrier of T1 by PRE_TOPC:29;
      f.p = ((1 - 0)/(1 - 1/2)) * (1/2 - 1/2) + 0 by A4,Th39
        .= g.p by A2,A5,FUNCOP_1:13;
      hence thesis;
    end;
    then consider h being Function of I[01], I[01] such that
A6: h = g +* f & h is continuous by A3,BORSUK_2:1;
    2RP = h
    proof
      for x being Element of I[01] holds 2RP.x = (g +* f).x
      proof
        let x be Element of I[01];
A7:     dom f = the carrier of T2 by FUNCT_2:def 1
          .= [.1/2,1.] by PRE_TOPC:29;
        per cases by REAL_1:def 5;
        suppose
A8:       x > 1/2;
          x <= 1 by BORSUK_1:86;
          then
A9:       x in dom f by A7,A8,XXREAL_1:1;
          1 >= x by BORSUK_1:86;
          then
A10:      f.x = ((1 - 0)/(1 - 1/2)) * (x - 1/2) + 0 by A8,Th39
            .= 2 * x - 1;
          thus 2RP.x = 2 * x - 1 by A8,Def8
            .= (g +* f).x by A9,A10,FUNCT_4:14;
        end;
        suppose
A11:      x = 1/2;
          then
A12:      x in dom f by A7,XXREAL_1:1;
          thus 2RP.x = ((1 - 0)/(1 - 1/2)) * (1/2 - 1/2) + 0 by A11,Def8
            .= f.x by A11,Th39
            .= (g +* f).x by A12,FUNCT_4:14;
        end;
        suppose
A13:      x < 1/2;
          then
A14:      not x in dom f by A7,XXREAL_1:1;
          x >= 0 by BORSUK_1:86;
          then x in [.0,1/2.] by A13,XXREAL_1:1;
          then
A15:      x in the carrier of T1 by PRE_TOPC:29;
          thus 2RP.x = 0 by A13,Def8
            .= g.x by A2,A15,FUNCOP_1:13
            .= (g +* f).x by A14,FUNCT_4:12;
        end;
      end;
      hence thesis by A6,FUNCT_2:113;
    end;
    hence thesis by A6;
  end;
end;

theorem Th56:
  2RP.0 = 0 & 2RP.1 = 1
proof
  reconsider x = 0, y = 1 as Point of I[01] by BORSUK_1:86;
  thus 2RP.0 = 2RP.x
    .= 0 by Def8;
  thus 2RP.1 = 2 * y - 1 by Def8
    .= 1;
end;

definition
  func 3RP -> Function of I[01], I[01] means
  :Def9:
  for x being Point of I[01] holds (x <= 1/2 implies it.x = 1/2 * x) &
  (x > 1/2 & x <= 3/4 implies it.x = x - 1/4) &
  (x > 3/4 implies it.x = 2 * x - 1);
  existence
  proof
    defpred P[real number] means $1 <= 1/2;
    defpred Q[real number] means $1 > 1/2 & $1 <= 3/4;
    defpred R[real number] means $1 > 3/4;
    deffunc F(real number) = 1/2 * $1;
    deffunc G(real number) = $1 - 1/4;
    deffunc H(real number) = 2 * $1 - 1;
A1: for c being Element of I[01] holds (P[c] implies not Q[c]) &
    (P[c] implies not R[c]) & (Q[c] implies not R[c]) by XXREAL_0:2;
A2: for c being Element of I[01] holds P[c] or Q[c] or R[c];
    consider f being Function such that
A3: dom f = the carrier of I[01] & for c being Element of I[01] holds
    (P[c] implies f.c = F(c)) & (Q[c] implies f.c = G(c)) &
    (R[c] implies f.c = H(c)) from ExFunc3CondD(A1,A2);
    for x being set st x in the carrier of I[01] holds
    f.x in the carrier of I[01]
    proof
      let x be set;
      assume x in the carrier of I[01];
      then reconsider x as Point of I[01];
      per cases;
      suppose P[x];
        then f.x = 1/2 * x by A3;
        then f.x is Point of I[01] by Th9;
        hence thesis;
      end;
      suppose
A4:     Q[x];
        then f.x = G(x) by A3;
        then f.x is Point of I[01] by A4,Th10;
        hence thesis;
      end;
      suppose
A5:     R[x];
        then f.x = 2 * x - 1 by A3;
        then f.x is Point of I[01] by A5,Th7,XXREAL_0:2;
        hence thesis;
      end;
    end;
    then reconsider f as Function of I[01], I[01] by A3,FUNCT_2:5;
    for x being Point of I[01] holds (x <= 1/2 implies f.x = 1/2 * x) &
    (x > 1/2 & x <= 3/4 implies f.x = x - 1/4) &
    (x > 3/4 implies f.x = 2 * x - 1) by A3;
    hence thesis;
  end;
  uniqueness
  proof
    let f1, f2 be Function of I[01], I[01];
    assume that
A6: for x being Point of I[01] holds (x <= 1/2 implies f1.x = 1/2 * x) &
    (x > 1/2 & x <= 3/4 implies f1.x = x - 1/4) &
    (x > 3/4 implies f1.x = 2 * x - 1) and
A7: for x being Point of I[01] holds (x <= 1/2 implies f2.x = 1/2 * x) &
    (x > 1/2 & x <= 3/4 implies f2.x = x - 1/4) &
    (x > 3/4 implies f2.x = 2 * x - 1);
    for x being Point of I[01] holds f1.x = f2.x
    proof
      let x be Point of I[01];
      per cases;
      suppose
A8:     x <= 1/2;
        then f1.x = 1/2 * x by A6
          .= f2.x by A7,A8;
        hence thesis;
      end;
      suppose
A9:     x > 1/2 & x <= 3/4;
        then f1.x = x - 1/4 by A6
          .= f2.x by A7,A9;
        hence thesis;
      end;
      suppose
A10:    x > 3/4;
        then f1.x = 2 * x - 1 by A6
          .= f2.x by A7,A10;
        hence thesis;
      end;
    end;
    hence thesis by FUNCT_2:113;
  end;
end;

registration
  cluster 3RP -> continuous;
  coherence
  proof
A1: 0 is Point of I[01] & 1/2 is Point of I[01] & 1/4 is Point of I[01] &
    3/4 is Point of I[01] & 1 is Point of I[01] by BORSUK_1:86;
    then reconsider A = [.0,1/2.] as non empty compact Subset of I[01]
    by BORSUK_4:49;
    reconsider B = [.1/2,3/4.] as non empty compact Subset of I[01]
    by A1,BORSUK_4:49;
    reconsider C = [.3/4,1.] as non empty compact Subset of I[01]
    by A1,BORSUK_4:49;
    reconsider D = [.1/2,1.] as non empty compact Subset of I[01]
    by A1,BORSUK_4:49;
    reconsider E = [.1/4,1/2.] as non empty compact Subset of I[01]
    by A1,BORSUK_4:49;
    reconsider F = [.0,1/4.] as non empty compact Subset of I[01]
    by A1,BORSUK_4:49;
    set T = I[01];
    set T1 = T|A, T2 = T|B, T3 = T|C, T4 = T|D, T5 = T|E, T6 = T|F;
A2: Closed-Interval-TSpace (3/4,1) = T3 by TOPMETR:31;
A3: Closed-Interval-TSpace (1/2,1) = T4 by TOPMETR:31;
A4: Closed-Interval-TSpace (1/4,1/2) = T5 by TOPMETR:31;
A5: Closed-Interval-TSpace (1/2,3/4) = T2 by TOPMETR:31;
A6: Closed-Interval-TSpace (0,1/4) = T6 by TOPMETR:31;
A7: Closed-Interval-TSpace (0,1/2) = T1 by TOPMETR:31;
    set f = L[01](0,1/2,0,1/4);
    reconsider f as continuous Function of T1, T6 by A6,A7,Th38;
    reconsider f as continuous Function of T1, T by JORDAN6:4;
A8: for x being Point of T1 holds f.x = 1/2 * x
    proof
      let x be Point of T1;
      x in the carrier of T1;
      then x in A by PRE_TOPC:29;
      then 0 <= x & x <= 1/2 by XXREAL_1:1;
      then f.x = ((1/4 - 0)/(1/2 - 0)) * (x - 0) + 0 by Th39
        .= 1/2 * x;
      hence thesis;
    end;
    set g = L[01](1/2,3/4,1/4,1/2);
    reconsider g as continuous Function of T2, T5 by A4,A5,Th38;
    reconsider g as continuous Function of T2, T by JORDAN6:4;
A9: for x being Point of T2 holds g.x = x - 1/4
    proof
      let x be Point of T2;
      x in the carrier of T2;
      then x in B by PRE_TOPC:29;
      then 1/2 <= x & x <= 3/4 by XXREAL_1:1;
      then g.x = ((1/2 - 1/4)/(3/4 - 1/2)) * (x - 1/2) + 1/4 by Th39
        .= x - 1/4;
      hence thesis;
    end;
    set h = L[01](3/4,1,1/2,1);
    reconsider h as continuous Function of T3, T4 by A2,A3,Th38;
    reconsider h as continuous Function of T3, T by JORDAN6:4;
A10: for x being Point of T3 holds h.x = 2 * x - 1
    proof
      let x be Point of T3;
      x in the carrier of T3;
      then x in C by PRE_TOPC:29;
      then 3/4 <= x & x <= 1 by XXREAL_1:1;
      then h.x = ((1 - 1/2)/(1 - 3/4)) * (x - 3/4) + 1/2 by Th39
        .= 2 * x - 1;
      hence thesis;
    end;
    reconsider G = [.0,3/4.] as non empty compact Subset of I[01]
    by A1,BORSUK_4:49;
    reconsider TT1 = T1, TT2 = T2 as SubSpace of T|G by XXREAL_1:34,TOPMETR:29;
    set f1 = f, g1 = g;
A11: ([#] TT1) \/ ([#] TT2) = A \/ ([#] TT2) by PRE_TOPC:def 10
      .= A \/ B by PRE_TOPC:def 10
      .= [.0,3/4.] by XXREAL_1:174
      .= [#] (T|G) by PRE_TOPC:def 10;
A12: T|G is_T2 by TOPMETR:3;
A13: ([#] TT1) /\ ([#] TT2) = A /\ ([#] TT2) by PRE_TOPC:def 10
      .= A /\ B by PRE_TOPC:def 10
      .= {1/2} by TOPMETR2:1;
    for p be set st p in ([#] TT1) /\ ([#] TT2) holds f1.p = g1.p
    proof
      let p be set;
      assume p in ([#] TT1) /\ ([#] TT2);
      then
A14:  p = 1/2 by A13,TARSKI:def 1;
      then reconsider p as Point of I[01] by BORSUK_1:83,XXREAL_1:1;
      f1.p = ((1/4 - 0)/(1/2 - 0)) * (p - 0) + 0 by A14,Th39
        .= ((1/2 - 1/4)/(3/4 - 1/2)) * (p - 1/2) + 1/4 by A14
        .= g1.p by A14,Th39;
      hence thesis;
    end;
    then consider FF being Function of T|G, T such that
A15: FF = f1 +* g1 & FF is continuous by A11,A12,BORSUK_2:1;
A16: ([#] (T|G)) \/ ([#] T3) = G \/ ([#] T3) by PRE_TOPC:def 10
      .= G \/ C by PRE_TOPC:def 10
      .= [#] T by BORSUK_1:83,XXREAL_1:174;
A17: ([#] (T|G)) /\ ([#] T3) = G /\ ([#] T3) by PRE_TOPC:def 10
      .= G /\ C by PRE_TOPC:def 10
      .= {3/4} by TOPMETR2:1;
    for p be set st p in ([#] (T|G)) /\ ([#] T3) holds FF.p = h.p
    proof
      let p be set;
      assume p in ([#] (T|G)) /\ ([#] T3);
      then
A18:  p = 3/4 by A17,TARSKI:def 1;
      then reconsider p as Point of T by BORSUK_1:86;
      p in [.1/2,3/4.] by A18,XXREAL_1:1;
      then p in the carrier of T2 by PRE_TOPC:29;
      then p in dom g by FUNCT_2:def 1;
      then FF.p = g.p by A15,FUNCT_4:14
        .= 1/2 by A18,Th37
        .= h.p by A18,Th37;
      hence thesis;
    end;
    then consider HH being Function of T, T such that
A19: HH = FF +* h & HH is continuous by A15,A16,BORSUK_2:1;
    for x being Element of T holds HH.x = 3RP.x
    proof
      let x be Element of T;
A20:  0 <= x & x <= 1 by BORSUK_1:86;
      per cases by REAL_1:def 5;
      suppose
A21:    x < 1/2;
        then x in [.0,1/2.] by A20,XXREAL_1:1;
        then
A22:    x is Point of T1 by PRE_TOPC:29;
        not x in [.1/2,3/4.] by A21,XXREAL_1:1;
        then not x in the carrier of T2 by PRE_TOPC:29;
        then
A23:    not x in dom g;
        x < 3/4 by A21,XXREAL_0:2;
        then not x in [.3/4,1.] by XXREAL_1:1;
        then not x in the carrier of T3 by PRE_TOPC:29;
        then not x in dom h;
        then HH.x = FF.x by A19,FUNCT_4:12
          .= f.x by A15,A23,FUNCT_4:12
          .= 1/2 * x by A8,A22
          .= 3RP.x by A21,Def9;
        hence thesis;
      end;
      suppose
A24:    x = 1/2;
        then x in [.1/2,3/4.] by XXREAL_1:1;
        then x in the carrier of T2 by PRE_TOPC:29;
        then
A25:    x in dom g by FUNCT_2:def 1;
        not x in [.3/4,1.] by A24,XXREAL_1:1;
        then not x in the carrier of T3 by PRE_TOPC:29;
        then not x in dom h;
        then HH.x = FF.x by A19,FUNCT_4:12
          .= g.x by A15,A25,FUNCT_4:14
          .= 1/2 * x by A24,Th37
          .= 3RP.x by A24,Def9;
        hence thesis;
      end;
      suppose
A26:    x > 1/2 & x < 3/4;
        then x in [.1/2,3/4.] by XXREAL_1:1;
        then
A27:    x in the carrier of T2 by PRE_TOPC:29;
        then
A28:    x in dom g by FUNCT_2:def 1;
        not x in [.3/4,1.] by A26,XXREAL_1:1;
        then not x in the carrier of T3 by PRE_TOPC:29;
        then not x in dom h;
        then HH.x = FF.x by A19,FUNCT_4:12
          .= g.x by A15,A28,FUNCT_4:14
          .= x - 1/4 by A9,A27
          .= 3RP.x by A26,Def9;
        hence thesis;
      end;
      suppose
A29:    x = 3/4;
        then x in [.3/4,1.] by XXREAL_1:1;
        then x in the carrier of T3 by PRE_TOPC:29;
        then x in dom h by FUNCT_2:def 1;
        then HH.x = h.x by A19,FUNCT_4:14
          .= x - 1/4 by A29,Th37
          .= 3RP.x by A29,Def9;
        hence thesis;
      end;
      suppose
A30:    x > 3/4;
        then x in [.3/4,1.] by A20,XXREAL_1:1;
        then
A31:    x in the carrier of T3 by PRE_TOPC:29;
        then x in dom h by FUNCT_2:def 1;
        then HH.x = h.x by A19,FUNCT_4:14
          .= 2 * x - 1 by A10,A31
          .= 3RP.x by A30,Def9;
        hence thesis;
      end;
    end;
    hence thesis by A19,FUNCT_2:113;
  end;
end;

theorem Th57:
  3RP.0 = 0 & 3RP.1 = 1
proof
A1: 0 is Point of I[01] & 1 is Point of I[01] by BORSUK_1:86;
  hence 3RP.0 = 1/2 * 0 by Def9
    .= 0;
  thus 3RP.1 = 2 * 1 - 1 by A1,Def9
    .= 1;
end;

theorem Th58:
  for P being Path of a, b, Q being constant Path of b, b st
  a,b are_connected holds RePar (P, 1RP) = P + Q
proof
  let P be Path of a, b, Q be constant Path of b, b;
  set f = RePar (P, 1RP), g = P + Q;
  assume
A1: a, b are_connected;
A2: b, b are_connected;
  for p being Element of I[01] holds f.p = g.p
  proof
    let p be Element of I[01];
    p in the carrier of I[01];
    then
A3: p in dom 1RP by FUNCT_2:def 1;
    0 in the carrier of I[01] by BORSUK_1:86;
    then
A4: 0 in dom Q by FUNCT_2:def 1;
A5: f.p = (P * 1RP).p by A1,Def6,Th55
      .= P. (1RP.p) by A3,FUNCT_1:23;
    per cases;
    suppose
A6:   p <= 1/2;
      then f.p = P.(2*p) by A5,Def7
        .= g.p by A1,A6,BORSUK_2:def 5;
      hence thesis;
    end;
    suppose
A7:   p > 1/2;
      then 2*p - 1 is Point of I[01] by Th7;
      then 2*p - 1 in the carrier of I[01];
      then
A8:   2*p - 1 in dom Q by FUNCT_2:def 1;
      f.p = P.1 by A5,A7,Def7
        .= b by A1,BORSUK_2:def 2
        .= Q.0 by A2,BORSUK_2:def 2
        .= Q.(2*p - 1) by A4,A8,FUNCT_1:def 16
        .= g.p by A1,A7,BORSUK_2:def 5;
      hence thesis;
    end;
  end;
  hence thesis by FUNCT_2:113;
end;

theorem Th59:
  for P being Path of a, b,
  Q being constant Path of a, a st a,b are_connected holds
  RePar (P, 2RP) = Q + P
proof
  let P be Path of a, b, Q be constant Path of a, a;
  assume
A1: a,b are_connected;
A2: a,a are_connected;
  set f = RePar (P, 2RP), g = Q + P;
  for p being Element of I[01] holds f.p = g.p
  proof
    let p be Element of I[01];
    p in the carrier of I[01];
    then
A3: p in dom 2RP by FUNCT_2:def 1;
    0 in the carrier of I[01] by BORSUK_1:86;
    then
A4: 0 in dom Q by FUNCT_2:def 1;
A5: f.p = (P * 2RP).p by A1,Def6,Th56
      .= P. (2RP.p) by A3,FUNCT_1:23;
    per cases;
    suppose
A6:   p <= 1/2;
      then 2*p is Point of I[01] by Th6;
      then 2*p in the carrier of I[01];
      then
A7:   2*p in dom Q by FUNCT_2:def 1;
      f.p = P.0 by A5,A6,Def8
        .= a by A1,BORSUK_2:def 2
        .= Q.0 by A2,BORSUK_2:def 2
        .= Q.(2*p) by A4,A7,FUNCT_1:def 16
        .= g.p by A1,A6,BORSUK_2:def 5;
      hence thesis;
    end;
    suppose
A8:   p > 1/2;
      then f.p = P.(2*p - 1) by A5,Def8
        .= g.p by A1,A8,BORSUK_2:def 5;
      hence thesis;
    end;
  end;
  hence thesis by FUNCT_2:113;
end;

theorem Th60:
  for P being Path of a, b, Q being Path of b, c, R being Path of c, d st
  a,b are_connected & b,c are_connected & c,d are_connected holds
  RePar (P + Q + R, 3RP) = P + (Q + R)
proof
  let P be Path of a, b, Q be Path of b, c, R be Path of c, d;
  assume that
A1: a,b are_connected and
A2: b,c are_connected and
A3: c,d are_connected;
A4: a,c are_connected by A1,A2,Th46;
A5: b,d are_connected by A2,A3,Th46;
  set F = P + Q + R;
  set f = RePar (F, 3RP), g = P + (Q + R);
  for x being Point of I[01] holds f.x = g.x
  proof
    let x be Point of I[01];
    x in the carrier of I[01];
    then
A6: x in dom 3RP by FUNCT_2:def 1;
A7: f.x = (F*3RP).x by A3,A4,Def6,Th46,Th57
      .= F.(3RP.x) by A6,FUNCT_1:23;
    per cases;
    suppose
A8:   x <= 1/2;
      reconsider y = 1/2 * x as Point of I[01] by Th9;
      1/2 * x <= (1/2) * (1/2) by A8,XREAL_1:66;
      then
A9:   y <= 1/2 by XXREAL_0:2;
      reconsider z = 2 * y as Point of I[01];
      f.x = F.y by A7,A8,Def9
        .= (P + Q).z by A3,A4,A9,BORSUK_2:def 5
        .= P.(2 * x) by A1,A2,A8,BORSUK_2:def 5
        .= g.x by A1,A5,A8,BORSUK_2:def 5;
      hence thesis;
    end;
    suppose
A10:  x > 1/2 & x <= 3/4;
      then
A11:  x - 1/4 <= 3/4 - 1/4 by XREAL_1:11;
      then
A12:  x - 1/4 <= 1 by XXREAL_0:2;
A13:  1/2 - 1/4 <= x - 1/4 by A10,XREAL_1:11;
      then reconsider y = x - 1/4 as Point of I[01] by A12,BORSUK_1:86;
      reconsider z = 2 * y as Point of I[01] by A11,Th6;
A14:  2 * y >= 2 * (1/4) by A13,XREAL_1:66;
      reconsider w = 2 * x - 1 as Point of I[01] by A10,Th7;
      2 * x <= 2 * (3/4) by A10,XREAL_1:66;
      then
A15:  2 * x - 1 <= 3/2 - 1 by XREAL_1:11;
      f.x = F.y by A7,A10,Def9
        .= (P + Q).z by A3,A4,A11,BORSUK_2:def 5
        .= Q.(2 * z - 1) by A1,A2,A14,BORSUK_2:def 5
        .= Q.(2 * w)
        .= (Q + R).w by A2,A3,A15,BORSUK_2:def 5
        .= g.x by A1,A5,A10,BORSUK_2:def 5;
      hence thesis;
    end;
    suppose
A16:  x > 3/4;
      then
A17:  x > 1/2 by XXREAL_0:2;
      reconsider y = 2 * x - 1 as Point of I[01] by A16,Th7,XXREAL_0:2;
      2 * x > 2 * (3/4) by A16,XREAL_1:70;
      then
A18:  2 * x - 1 > 2 * (3/4) - 1 by REAL_1:92;
      reconsider w = 2 * x - 1 as Point of I[01] by A16,Th7,XXREAL_0:2;
      f.x = F.y by A7,A16,Def9
        .= R.(2 * y - 1) by A3,A4,A18,BORSUK_2:def 5
        .= (Q + R).w by A2,A3,A18,BORSUK_2:def 5
        .= g.x by A1,A5,A17,BORSUK_2:def 5;
      hence thesis;
    end;
  end;
  hence thesis by FUNCT_2:113;
end;

begin :: Decomposition of the Unit Square

definition
  func LowerLeftUnitTriangle -> Subset of [:I[01], I[01]:] means
  :Def10:
  for x being set holds x in it iff
  ex a, b being Point of I[01] st x = [a,b] & b <= 1 - 2 * a;
  existence
  proof
    defpred P[set] means
    ex a, b being Point of I[01] st $1 = [a,b] & b <= 1 - 2 * a;
    consider X being set such that
A1: for x being set holds x in X iff x in the carrier of [:I[01], I[01]:] &
    P[x] from XBOOLE_0:sch 1;
    X c= the carrier of [:I[01], I[01]:]
    proof
      let x be set;
      assume x in X;
      hence thesis by A1;
    end;
    then reconsider X as Subset of [:I[01], I[01]:];
    take X;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let X1, X2 be Subset of [:I[01], I[01]:] such that
A2: for x being set holds x in X1 iff
    ex a, b being Point of I[01] st x = [a,b] & b <= 1 - 2 * a and
A3: for x being set holds x in X2 iff
    ex a, b being Point of I[01] st x = [a,b] & b <= 1 - 2 * a;
    X1 = X2
    proof
      thus X1 c= X2
      proof
        let x be set;
        assume x in X1;
        then ex a, b being Point of I[01] st x = [a,b] & b <= 1 - 2 * a by A2;
        hence thesis by A3;
      end;
      let x be set;
      assume x in X2;
      then ex a, b being Point of I[01] st x = [a,b] & b <= 1 - 2 * a by A3;
      hence thesis by A2;
    end;
    hence thesis;
  end;
end;

notation
  synonym IAA for LowerLeftUnitTriangle;
end;

definition
  func UpperUnitTriangle -> Subset of [:I[01], I[01]:] means
  :Def11:
  for x being set holds x in it iff
  ex a, b being Point of I[01] st x = [a,b] & b >= 1 - 2 * a & b >= 2 * a - 1;
  existence
  proof
    defpred P[set] means ex a, b being Point of I[01] st $1 = [a,b] &
    b >= 1 - 2 * a & b >= 2 * a - 1;
    consider X being set such that
A1: for x being set holds x in X iff x in the carrier of [:I[01], I[01]:] &
    P[x] from XBOOLE_0:sch 1;
    X c= the carrier of [:I[01], I[01]:]
    proof
      let x be set;
      assume x in X;
      hence thesis by A1;
    end;
    then reconsider X as Subset of [:I[01], I[01]:];
    take X;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let X1, X2 be Subset of [:I[01], I[01]:] such that
A2: for x being set holds x in X1 iff
    ex a, b being Point of I[01] st x = [a,b] &
    b >= 1 - 2 * a & b >= 2 * a - 1 and
A3: for x being set holds x in X2 iff
    ex a, b being Point of I[01] st x = [a,b] &
    b >= 1 - 2 * a & b >= 2 * a - 1;
    X1 = X2
    proof
      thus X1 c= X2
      proof
        let x be set;
        assume x in X1;
        then ex a, b being Point of I[01] st x = [a,b] &
        b >= 1 - 2 * a & b >= 2 * a - 1 by A2;
        hence thesis by A3;
      end;
      let x be set;
      assume x in X2;
      then ex a, b being Point of I[01] st x = [a,b] &
      b >= 1 - 2 * a & b >= 2 * a - 1 by A3;
      hence thesis by A2;
    end;
    hence thesis;
  end;
end;

notation
  synonym IBB for UpperUnitTriangle;
end;

definition
  func LowerRightUnitTriangle -> Subset of [:I[01], I[01]:] means
  :Def12:
  for x being set holds x in it iff
  ex a, b being Point of I[01] st x = [a,b] & b <= 2 * a - 1;
  existence
  proof
    defpred P[set] means
    ex a, b being Point of I[01] st $1 = [a,b] & b <= 2 * a - 1;
    consider X being set such that
A1: for x being set holds x in X iff x in the carrier of [:I[01], I[01]:] &
    P[x] from XBOOLE_0:sch 1;
    X c= the carrier of [:I[01], I[01]:]
    proof
      let x be set;
      assume x in X;
      hence thesis by A1;
    end;
    then reconsider X as Subset of [:I[01], I[01]:];
    take X;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let X1, X2 be Subset of [:I[01], I[01]:] such that
A2: for x being set holds x in X1 iff
    ex a, b being Point of I[01] st x = [a,b] & b <= 2 * a - 1 and
A3: for x being set holds x in X2 iff
    ex a, b being Point of I[01] st x = [a,b] & b <= 2 * a - 1;
    X1 = X2
    proof
      thus X1 c= X2
      proof
        let x be set;
        assume x in X1;
        then ex a, b being Point of I[01] st x = [a,b] & b <= 2 * a - 1 by A2;
        hence thesis by A3;
      end;
      let x be set;
      assume x in X2;
      then ex a, b being Point of I[01] st x = [a,b] & b <= 2 * a - 1 by A3;
      hence thesis by A2;
    end;
    hence thesis;
  end;
end;

notation
  synonym ICC for LowerRightUnitTriangle;
end;

theorem Th61:
  IAA = { p where p is Point of [:I[01], I[01]:] : p`2 <= 1 - 2 * (p`1) }
proof
  set P = { p where p is Point of [:I[01], I[01]:] : p`2 <= 1 - 2 * (p`1) };
  thus IAA c= P
  proof
    let x be set;
    assume
A1: x in IAA;
    then consider a, b being Point of I[01] such that
A2: x = [a,b] & b <= 1 - 2 * a by Def10;
    reconsider x' = x as Point of [:I[01], I[01]:] by A1;
    x'`1 = a & x'`2 = b by A2,MCART_1:7;
    hence thesis by A2;
  end;
  let x be set;
  assume x in P;
  then consider p being Point of [:I[01], I[01]:] such that
A3: p = x & p`2 <= 1 - 2 * (p`1);
  x in the carrier of [:I[01], I[01]:] by A3;
  then x in [:the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def 5;
  then
A4: x = [x`1, x`2] by MCART_1:23;
A5: p`1 is Point of I[01] by Th31;
  p`2 is Point of I[01] by Th31;
  hence thesis by A3,A4,A5,Def10;
end;

theorem Th62:
  IBB = { p where p is Point of [:I[01], I[01]:] :
  p`2 >= 1 - 2 * (p`1) & p`2 >= 2 * (p`1) - 1 }
proof
  set P = { p where p is Point of [:I[01], I[01]:] :
  p`2 >= 1 - 2 * (p`1) & p`2 >= 2 * (p`1) - 1 };
  thus IBB c= P
  proof
    let x be set;
    assume
A1: x in IBB;
    then consider a, b being Point of I[01] such that
A2: x = [a,b] & b >= 1 - 2 * a & b >= 2 * a - 1 by Def11;
    reconsider x' = x as Point of [:I[01], I[01]:] by A1;
    x'`1 = a & x'`2 = b by A2,MCART_1:7;
    hence thesis by A2;
  end;
  let x be set;
  assume x in P;
  then consider p being Point of [:I[01], I[01]:] such that
A3: p = x & p`2 >= 1 - 2 * (p`1) & p`2 >= 2 * (p`1) - 1;
  x in the carrier of [:I[01], I[01]:] by A3;
  then x in [:the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def 5;
  then
A4: x = [x`1, x`2] by MCART_1:23;
A5: p`1 is Point of I[01] by Th31;
  p`2 is Point of I[01] by Th31;
  hence thesis by A3,A4,A5,Def11;
end;

theorem Th63:
  ICC = { p where p is Point of [:I[01], I[01]:] : p`2 <= 2 * (p`1) - 1 }
proof
  set P = { p where p is Point of [:I[01], I[01]:] : p`2 <= 2 * (p`1) - 1 };
  thus ICC c= P
  proof
    let x be set;
    assume
A1: x in ICC;
    then consider a, b being Point of I[01] such that
A2: x = [a,b] & b <= 2 * a - 1 by Def12;
    reconsider x' = x as Point of [:I[01], I[01]:] by A1;
    x'`1 = a & x'`2 = b by A2,MCART_1:7;
    hence thesis by A2;
  end;
  let x be set;
  assume x in P;
  then consider p being Point of [:I[01], I[01]:] such that
A3: p = x & p`2 <= 2 * (p`1) - 1;
  x in the carrier of [:I[01], I[01]:] by A3;
  then x in [:the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def 5;
  then
A4: x = [x`1, x`2] by MCART_1:23;
A5: p`1 is Point of I[01] by Th31;
  p`2 is Point of I[01] by Th31;
  hence thesis by A3,A4,A5,Def12;
end;

registration
  cluster IAA -> closed non empty;
  coherence by Th28,Th61;
  cluster IBB -> closed non empty;
  coherence by Th29,Th62;
  cluster ICC -> closed non empty;
  coherence by Th30,Th63;
end;

theorem Th64:
  IAA \/ IBB \/ ICC = [:[.0,1.], [.0,1.]:]
proof
  thus IAA \/ IBB \/ ICC c= [:[.0,1.], [.0,1.]:] by Th1;
  let x be set;
  assume
A1: x in [:[.0,1.], [.0,1.]:];
  then reconsider q = x`1, p = x`2 as Point of I[01] by BORSUK_1:83,MCART_1:10;
A2: x = [q,p] by A1,MCART_1:23;
  x in IAA or x in IBB or x in ICC
  proof
    per cases;
    suppose
A3:   p >= 1 - 2 * q;
      now per cases;
        suppose p >= 2 * q - 1;
          hence thesis by A2,A3,Def11;
        end;
        suppose p < 2 * q - 1;
          hence thesis by A2,Def12;
        end;
      end;
      hence thesis;
    end;
    suppose p < 1 - 2 * q;
      hence thesis by A2,Def10;
    end;
  end;
  then x in IAA \/ IBB or x in ICC by XBOOLE_0:def 2;
  hence thesis by XBOOLE_0:def 2;
end;

theorem Th65:
  IAA /\ IBB = { p where p is Point of [:I[01], I[01]:] :
  p`2 = 1 - 2 * (p`1) }
proof
  set KK = { p where p is Point of [:I[01], I[01]:] : p`2 = 1 - 2 * (p`1) };
  thus IAA /\ IBB c= KK
  proof
    let x be set;
    assume x in IAA /\ IBB;
    then
A1: x in IAA & x in IBB by XBOOLE_0:def 3;
    then consider p being Point of [:I[01], I[01]:] such that
A2: x = p & p`2 <= 1 - 2 * (p`1) by Th61;
    consider q being Point of [:I[01], I[01]:] such that
A3: x = q & q`2 >= 1 - 2 * (q`1) & q`2 >= 2 * (q`1) - 1 by A1,Th62;
    p`2 = 1 - 2 * (p`1) by A2,A3,XXREAL_0:1;
    hence thesis by A2;
  end;
  let x be set;
  assume x in KK;
  then consider p being Point of [:I[01], I[01]:] such that
A4: p = x & p`2 = 1 - 2 * (p`1);
  x in the carrier of [:I[01], I[01]:] by A4;
  then
A5: x in [:the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def 5;
  then
A6: x = [p`1,p`2] by A4,MCART_1:23;
A7: p`1 in the carrier of I[01] & p`2 in the carrier of I[01]
  by A4,A5,MCART_1:10;
  then
A8: x in IAA by A4,A6,Def10;
  1 - 2 * p`1 >= 0 by A4,A7,BORSUK_1:86;
  then 0 + 2 * p`1 <= 1 by XREAL_1:21;
  then (2 * p`1)/2 <= 1/2 by REAL_1:73;
  then 2 * p`1 - 1 <= 0 & 0 <= 1 - 2 * (p`1) by XREAL_1:219,220;
  then x in IBB by A4,A6,A7,Def11;
  hence thesis by A8,XBOOLE_0:def 3;
end;

theorem Th66:
  ICC /\ IBB = { p where p is Point of [:I[01], I[01]:] :
  p`2 = 2 * (p`1) - 1 }
proof
  set KK = { p where p is Point of [:I[01], I[01]:] : p`2 = 2 * (p`1) - 1 };
  thus ICC /\ IBB c= KK
  proof
    let x be set;
    assume x in ICC /\ IBB;
    then
A1: x in ICC & x in IBB by XBOOLE_0:def 3;
    then consider p being Point of [:I[01], I[01]:] such that
A2: x = p & p`2 <= 2 * (p`1) - 1 by Th63;
    consider q being Point of [:I[01], I[01]:] such that
A3: x = q & q`2 >= 1 - 2 * (q`1) & q`2 >= 2 * (q`1) - 1 by A1,Th62;
    p`2 = 2 * (p`1) - 1 by A2,A3,XXREAL_0:1;
    hence thesis by A2;
  end;
  let x be set;
  assume x in KK;
  then consider p being Point of [:I[01], I[01]:] such that
A4: p = x & p`2 = 2 * (p`1) - 1;
  x in the carrier of [:I[01], I[01]:] by A4;
  then
A5: x in [:the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def 5;
  then
A6: x = [p`1,p`2] by A4,MCART_1:23;
A7: p`1 in the carrier of I[01] & p`2 in the carrier of I[01]
  by A4,A5,MCART_1:10;
  then
A8: x in ICC by A4,A6,Def12;
  2 * p`1 - 1 >= 0 by A4,A7,BORSUK_1:86;
  then 2 * p`1 >= 0 + 1 by XREAL_1:21;
  then (2 * p`1)/2 >= 1/2 by REAL_1:73;
  then 2 * p`1 - 1 >= 0 & 0 >= 1 - 2 * (p`1) by XREAL_1:221,222;
  then x in IBB by A4,A6,A7,Def11;
  hence thesis by A8,XBOOLE_0:def 3;
end;

theorem Th67:
  for x being Point of [:I[01], I[01]:] st x in IAA holds x`1 <= 1/2
proof
  set GG = [:I[01], I[01]:];
  let x be Point of GG;
  assume x in IAA;
  then consider a, b being Point of I[01] such that
A1: x = [a,b] & b <= 1 - 2 * a by Def10;
  b >= 0 by BORSUK_1:86;
  then 1 >= 0 + 2 * a by A1,XREAL_1:21;
  then
A2: 1/2 >= (2 * a)/2 by REAL_1:73;
  x = [x`1, x`2] by A1,MCART_1:8;
  hence thesis by A1,A2,ZFMISC_1:33;
end;

theorem Th68:
  for x being Point of [:I[01], I[01]:] st x in ICC holds x`1 >= 1/2
proof
  set GG = [:I[01], I[01]:];
  let x be Point of GG;
  assume x in ICC;
  then consider a, b being Point of I[01] such that
A1: x = [a,b] & b <= 2 * a - 1 by Def12;
  b >= 0 by BORSUK_1:86;
  then 0 + 1 <= 2 * a by A1,XREAL_1:21;
  then
A2: 1/2 <= (2 * a)/2 by REAL_1:73;
  x = [x`1, x`2] by A1,MCART_1:8;
  hence thesis by A1,A2,ZFMISC_1:33;
end;

theorem Th69:
  for x being Point of I[01] holds [0,x] in IAA
proof
  let x be Point of I[01];
A1: 0 is Point of I[01] by BORSUK_1:86;
  x <= 1 - 2 * 0 by BORSUK_1:86;
  hence thesis by A1,Def10;
end;

theorem Th70:
  for s being set holds [0,s] in IBB implies s = 1
proof
  let s be set;
  assume [0,s] in IBB;
  then consider a, b being Point of I[01] such that
A1: [0,s] = [a,b] & b >= 1 - 2 * a & b >= 2 * a - 1 by Def11;
A2: b <= 1 by BORSUK_1:86;
  a = 0 & b = s by A1,ZFMISC_1:33;
  hence thesis by A1,A2,XXREAL_0:1;
end;

theorem Th71:
  for s being set holds [s,1] in ICC implies s = 1
proof
  let s be set;
  assume [s,1] in ICC;
  then consider a, b being Point of I[01] such that
A1: [s,1] = [a,b] & b <= 2 * a - 1 by Def12;
A2: a <= 1 by BORSUK_1:86;
A3: a = s & b = 1 by A1,ZFMISC_1:33;
  then 1 + 1 <= 2 * a by A1,XREAL_1:21;
  then 2/2 <= (2 * a)/2 by REAL_1:73;
  hence thesis by A2,A3,XXREAL_0:1;
end;

theorem Th72:
  [0,1] in IBB
proof
A1: 0 is Point of I[01] & 1 is Point of I[01] by BORSUK_1:86;
  1 >= 1 - 2 * 0 & 1 >= 2 * 0 - 1;
  hence thesis by A1,Def11;
end;

theorem Th73:
  for x being Point of I[01] holds [x,1] in IBB
proof
  let x be Point of I[01];
A1: 0 is Point of I[01] & 1 is Point of I[01] by BORSUK_1:86;
A2: x <= 1 & x >= 0 by BORSUK_1:86;
  then 2 * x <= 2 * 1 by XREAL_1:66;
  then
A3: 2 * x - 1 <= 2 * 1 - 1 by REAL_1:92;
  2 * x >= 2 * 0 by A2;
  then 1 - 2 * x <= 1 - 2 * 0 by REAL_1:92;
  hence thesis by A1,A3,Def11;
end;

theorem Th74:
  [1/2,0] in ICC & [1,1] in ICC
proof
A1: 1/2 is Point of I[01] & 0 is Point of I[01] & 1 is Point of I[01]
  by BORSUK_1:86;
  0 <= 2 * (1/2) - 1;
  hence [1/2,0] in ICC by A1,Def12;
  1 <= 2 * 1 - 1;
  hence thesis by A1,Def12;
end;

theorem Th75:
  [1/2,0] in IBB
proof
A1: 1/2 is Point of I[01] & 0 is Point of I[01] & 1 is Point of I[01]
  by BORSUK_1:86;
  0 <= 1 - 2 * (1/2);
  hence [1/2,0] in IBB by A1,Def11;
end;

theorem Th76:
  for x being Point of I[01] holds [1,x] in ICC
proof
  let x be Point of I[01];
A1: 1 is Point of I[01] by BORSUK_1:86;
  x <= 2 * 1 - 1 by BORSUK_1:86;
  hence thesis by A1,Def12;
end;

theorem Th77:
  for x being Point of I[01] st x >= 1/2 holds [x,0] in ICC
proof
  let x be Point of I[01];
  assume x >= 1/2;
  then 2 * x >= 2 * (1/2) by XREAL_1:66;
  then
A1: 2 * x - 1 >= 2 * (1/2) - 1 by REAL_1:92;
  0 is Point of I[01] by BORSUK_1:86;
  hence thesis by A1,Def12;
end;

theorem Th78:
  for x being Point of I[01] st x <= 1/2 holds [x,0] in IAA
proof
  let x be Point of I[01];
  assume x <= 1/2;
  then 2 * x <= 2 * (1/2) by XREAL_1:66;
  then
A1: 1 - 2 * x >= 1 - 2 * (1/2) by REAL_1:92;
  0 is Point of I[01] by BORSUK_1:86;
  hence [x,0] in IAA by A1,Def10;
end;

theorem Th79:
  for x being Point of I[01] st x < 1/2 holds
  not [x,0] in IBB & not [x,0] in ICC
proof
  let x be Point of I[01];
  assume
A1: x < 1/2;
  thus not [x,0] in IBB
  proof
    assume [x,0] in IBB;
    then consider a, b being Point of I[01] such that
A2: [x,0] = [a,b] & b >= 1 - 2 * a & b >= 2 * a - 1 by Def11;
    x = a & b = 0 by A2,ZFMISC_1:33;
    then 0 + 2 * x >= 1 by A2,XREAL_1:22;
    then (2 * x)/2 >= 1/2 by REAL_1:73;
    hence thesis by A1;
  end;
  not [x,0] in ICC
  proof
    assume [x,0] in ICC;
    then consider a, b being Point of I[01] such that
A3: [x,0] = [a,b] & b <= 2 * a - 1 by Def12;
    x = a & b = 0 by A3,ZFMISC_1:33;
    then 0 + 1 <= 2 * x by A3,XREAL_1:21;
    then 1/2 <= (2 * x)/2 by REAL_1:73;
    hence thesis by A1;
  end;
  hence thesis;
end;

theorem Th80:
  IAA /\ ICC = { [1/2,0] }
proof
  thus IAA /\ ICC c= { [1/2,0] }
  proof
    let x be set;
    assume
A1: x in IAA /\ ICC;
    then
A2: x in IAA & x in ICC by XBOOLE_0:def 3;
    reconsider y = x as Point of [:I[01], I[01]:] by A1;
    y in the carrier of [:I[01], I[01]:];
    then
A3: y in [:the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def 5;
A4: y`1 >= 1/2 by A2,Th68;
    y`1 <= 1/2 by A2,Th67;
    then
A5: y`1 = 1/2 by A4,XXREAL_0:1;
    consider q being Point of [:I[01], I[01]:] such that
A6: q = y & q`2 <= 2 * (q`1) - 1 by A2,Th63;
    y`2 is Point of I[01] by Th31;
    then y`2 = 0 by A5,A6,BORSUK_1:86;
    then y = [1/2,0] by A3,A5,MCART_1:23;
    hence thesis by TARSKI:def 1;
  end;
A7: 1/2 is Point of I[01] by BORSUK_1:86;
  then
A8: [1/2,0] in IAA by Th78;
  [1/2,0] in ICC by A7,Th77;
  then [1/2,0] in IAA /\ ICC by A8,XBOOLE_0:def 3;
  hence { [1/2,0] } c= IAA /\ ICC by ZFMISC_1:37;
end;

Lm1: for x, y being Point of I[01] holds
[x,y] in the carrier of [:I[01], I[01]:];

begin :: Properties of a Homotopy

reserve X for non empty arcwise_connected TopSpace,
  a1, b1, c1, d1 for Point of X;

theorem Th81:
  for P be Path of a, b, Q be Path of b, c, R be Path of c, d st
  a,b are_connected & b,c are_connected & c,d are_connected holds
  (P + Q) + R, P + (Q + R) are_homotopic
proof
  let P be Path of a, b, Q be Path of b, c, R be Path of c, d such that
A1: a,b are_connected and
A2: b,c are_connected and
A3: c,d are_connected;
A4: a,c are_connected by A1,A2,Th46;
  RePar (P + Q + R, 3RP) = P + (Q + R) by A1,A2,A3,Th60;
  hence thesis by A3,A4,Th46,Th53,Th57;
end;

theorem
  for P be Path of a1, b1, Q be Path of b1, c1, R be Path of c1, d1 holds
  (P + Q) + R, P + (Q + R) are_homotopic
proof
  let P be Path of a1, b1, Q be Path of b1, c1, R be Path of c1, d1;
  a1,b1 are_connected & b1,c1 are_connected & c1,d1 are_connected
  by BORSUK_2:def 3;
  hence thesis by Th81;
end;

theorem Th83:
  for P1, P2 being Path of a, b, Q1, Q2 being Path of b, c st
  a, b are_connected & b, c are_connected &
  P1, P2 are_homotopic & Q1, Q2 are_homotopic holds
  P1 + Q1, P2 + Q2 are_homotopic
proof
  let P1, P2 be Path of a, b, Q1, Q2 be Path of b, c;
  assume that
A1: a,b are_connected and
A2: b,c are_connected and
A3: P1,P2 are_homotopic and
A4: Q1,Q2 are_homotopic;
  consider f being Function of [:I[01],I[01]:], T such that
A5: f is continuous &
  for s being Point of I[01] holds f.(s,0) = P1.s & f.(s,1) = P2.s &
  for t being Point of I[01] holds f.(0,t) = a & f.(1,t) = b
  by A3,BORSUK_2:def 7;
  consider g being Function of [:I[01],I[01]:], T such that
A6: g is continuous &
  for s being Point of I[01] holds g.(s,0) = Q1.s & g.(s,1) = Q2.s &
  for t being Point of I[01] holds g.(0,t) = b & g.(1,t) = c
  by A4,BORSUK_2:def 7;
  reconsider R1 = L[01](0,1/2,0,1) as continuous Function of
  Closed-Interval-TSpace(0,1/2), I[01] by Th38,TOPMETR:27;
  reconsider R2 = L[01](1/2,1,0,1) as continuous Function of
  Closed-Interval-TSpace(1/2,1), I[01] by Th38,TOPMETR:27;
  set f1 = [:R1,id I[01]:], g1 = [:R2,id I[01]:];
  set BB = [:I[01],I[01]:];
A7: 0 is Point of I[01] & 1 is Point of I[01] & 1/2 is Point of I[01]
  by BORSUK_1:86;
  then reconsider N1 = [:[.0,1/2.], [.0,1.]:] as compact non empty Subset of
  BB by Th13;
  reconsider N2 = [:[.1/2,1.], [.0,1.]:] as compact non empty Subset of BB
  by A7,Th13;
  set T1 = BB | N1;
  set T2 = BB | N2;
  reconsider f1 as continuous Function of
  [:Closed-Interval-TSpace(0,1/2),I[01]:], [:I[01],I[01]:] by BORSUK_2:12;
  reconsider A01 = [.0,1.] as non empty Subset of I[01] by A7,BORSUK_4:49;
  reconsider B01 = [.0,1/2.] as non empty Subset of I[01] by A7,BORSUK_4:49;
  reconsider B02 = [.1/2,1.] as non empty Subset of I[01] by A7,BORSUK_4:49;
  A01 = [#] I[01] by BORSUK_1:83;
  then
A8: I[01] = I[01] | A01 by TSEP_1:100;
  Closed-Interval-TSpace (0,1/2) = I[01] | B01 by TOPMETR:31;
  then T1 = [:Closed-Interval-TSpace(0,1/2),I[01]:] by A8,BORSUK_3:26;
  then reconsider K1 = f * f1 as continuous Function of T1, T by A5;
  reconsider g1 as continuous Function of
  [:Closed-Interval-TSpace(1/2,1),I[01]:], [:I[01],I[01]:] by BORSUK_2:12;
  Closed-Interval-TSpace (1/2,1) = I[01] | B02 by TOPMETR:31;
  then T2 = [:Closed-Interval-TSpace(1/2,1),I[01]:] by A8,BORSUK_3:26;
  then reconsider K2 = g * g1 as continuous Function of T2, T by A6;
A9: ([#] T1) \/ ([#] T2) = [#] BB by Th32;
A10: dom K2 = the carrier of [:Closed-Interval-TSpace(1/2,1), I[01]:]
  by FUNCT_2:def 1
    .= [:the carrier of Closed-Interval-TSpace(1/2,1),
  the carrier of I[01]:] by BORSUK_1:def 5;
A11: dom f1 = the carrier of [:Closed-Interval-TSpace(0,1/2), I[01]:]
  by FUNCT_2:def 1
    .= [:the carrier of Closed-Interval-TSpace(0,1/2),
  the carrier of I[01]:] by BORSUK_1:def 5;
A12: dom g1 = the carrier of [:Closed-Interval-TSpace(1/2,1), I[01]:]
  by FUNCT_2:def 1
    .= [:the carrier of Closed-Interval-TSpace(1/2,1),
  the carrier of I[01]:] by BORSUK_1:def 5;
  for p be set st p in ([#] T1) /\ ([#] T2) holds K1.p = K2.p
  proof
    let p be set;
    assume p in ([#] T1) /\ ([#] T2);
    then p in [:{1/2}, [.0,1.] :] by Th33;
    then consider x, y being set such that
A13: x in {1/2} & y in [.0,1.] & p = [x,y] by ZFMISC_1:def 2;
A14: y in the carrier of I[01] by A13,TOPMETR:25,27;
    reconsider y as Point of I[01] by A13,TOPMETR:25,27;
A15: x = 1/2 by A13,TARSKI:def 1;
    then x in [.0,1/2.] by XXREAL_1:1;
    then
A16: x in the carrier of Closed-Interval-TSpace(0,1/2) by TOPMETR:25;
    then p in [:the carrier of Closed-Interval-TSpace(0,1/2),
    the carrier of I[01]:] by A13,A14,ZFMISC_1:106;
    then p in the carrier of [:Closed-Interval-TSpace(0,1/2),I[01]:]
    by BORSUK_1:def 5;
    then
A17: p in dom f1 by FUNCT_2:def 1;
    x in [.1/2,1.] by A15,XXREAL_1:1;
    then
A18: x in the carrier of Closed-Interval-TSpace(1/2,1) by TOPMETR:25;
    then p in [:the carrier of Closed-Interval-TSpace(1/2,1),
    the carrier of I[01]:] by A13,A14,ZFMISC_1:106;
    then p in the carrier of [:Closed-Interval-TSpace(1/2,1),I[01]:]
    by BORSUK_1:def 5;
    then
A19: p in dom g1 by FUNCT_2:def 1;
A20: x in dom R1 by A16,FUNCT_2:def 1;
A21: y in dom id I[01] by A14,FUNCT_2:def 1;
    then
A22: [x,y] in [:dom R1, dom id I[01]:] by A20,ZFMISC_1:106;
    x in dom R2 by A18,FUNCT_2:def 1;
    then
A23: [x,y] in [:dom R2, dom id I[01]:] by A21,ZFMISC_1:106;
A24: R1. (1/2) = 1 by Th37;
A25: R2. (1/2) = 0 by Th37;
    K1.p = f.(f1.(x,y)) by A13,A17,FUNCT_1:23
      .= f.(R1.x,(id I[01]).y) by A22,FUNCT_3:86
      .= b by A5,A15,A24
      .= g.(R2.x,(id I[01]).y) by A6,A15,A25
      .= g.(g1.(x,y)) by A23,FUNCT_3:86
      .= K2.p by A13,A19,FUNCT_1:23;
    hence thesis;
  end;
  then consider h being Function of [:I[01],I[01]:], T such that
A26: h = K1 +* K2 & h is continuous by A9,BORSUK_2:1;
  take h;
A27: for s being Point of I[01] holds h.(s,0) = (P1+Q1).s &
  h.(s,1) = (P2+Q2).s
  proof
    let s be Point of I[01];
A28: h.(s,0) = (P1+Q1).s
    proof
      per cases;
      suppose
A29:    s < 1/2;
A30:    s >= 0 by BORSUK_1:86;
        not s in [.1/2,1.] by A29,XXREAL_1:1;
        then not s in the carrier of Closed-Interval-TSpace(1/2,1)
        by TOPMETR:25;
        then
A31:    not [s,0] in dom K2 by A10,ZFMISC_1:106;
        s in [.0,1/2.] by A29,A30,XXREAL_1:1;
        then
A32:    s in the carrier of Closed-Interval-TSpace(0,1/2) &
        0 in the carrier of I[01] by BORSUK_1:86,TOPMETR:25;
        then
A33:    [s,0] in dom f1 by A11,ZFMISC_1:106;
A34:    s in dom R1 by A32,FUNCT_2:def 1;
        0 in dom id I[01] by A32,FUNCT_2:def 1;
        then
A35:    [s,0] in [:dom R1, dom id I[01]:] by A34,ZFMISC_1:106;
A36:    R1.s = ((1 - 0)/(1/2 - 0)) * (s - 0) + 0 by A29,A30,Th39
          .= 2 * s;
A37:    2 * s is Point of I[01] by A29,Th6;
        h.(s,0) = K1.(s,0) by A26,A31,FUNCT_4:12
          .= f.(f1.(s,0)) by A33,FUNCT_1:23
          .= f.(R1.s,(id I[01]).0) by A35,FUNCT_3:86
          .= f.(2*s,0) by A7,A36,TMAP_1:91
          .= P1.(2 * s) by A5,A37;
        hence thesis by A1,A2,A29,BORSUK_2:def 5;
      end;
      suppose
A38:    s >= 1/2;
A39:    s <= 1 by BORSUK_1:86;
        then s in [.1/2,1.] by A38,XXREAL_1:1;
        then
A40:    s in the carrier of Closed-Interval-TSpace(1/2,1) &
        0 in the carrier of I[01] by BORSUK_1:86,TOPMETR:25;
        then
A41:    [s,0] in dom K2 by A10,ZFMISC_1:106;
A42:    [s,0] in dom g1 by A12,A40,ZFMISC_1:106;
A43:    s in dom R2 by A40,FUNCT_2:def 1;
        0 in dom id I[01] by A40,FUNCT_2:def 1;
        then
A44:    [s,0] in [:dom R2, dom id I[01]:] by A43,ZFMISC_1:106;
A45:    R2.s = ((1 - 0)/(1 - 1/2)) * (s - 1/2) + 0 by A38,A39,Th39
          .= 2 * s - 1;
A46:    2 * s - 1 is Point of I[01] by A38,Th7;
        h.(s,0) = K2.(s,0) by A26,A41,FUNCT_4:14
          .= g.(g1.(s,0)) by A42,FUNCT_1:23
          .= g.(R2.s,(id I[01]).0) by A44,FUNCT_3:86
          .= g.(2*s-1,0) by A7,A45,TMAP_1:91
          .= Q1.(2 * s - 1) by A6,A46;
        hence thesis by A1,A2,A38,BORSUK_2:def 5;
      end;
    end;
    h.(s,1) = (P2+Q2).s
    proof
      per cases;
      suppose
A47:    s < 1/2;
A48:    s >= 0 by BORSUK_1:86;
        not s in [.1/2,1.] by A47,XXREAL_1:1;
        then not s in the carrier of Closed-Interval-TSpace(1/2,1)
        by TOPMETR:25;
        then
A49:    not [s,1] in dom K2 by A10,ZFMISC_1:106;
        s in [.0,1/2.] by A47,A48,XXREAL_1:1;
        then
A50:    s in the carrier of Closed-Interval-TSpace(0,1/2) &
        1 in the carrier of I[01] by BORSUK_1:86,TOPMETR:25;
        then
A51:    [s,1] in dom f1 by A11,ZFMISC_1:106;
A52:    s in dom R1 by A50,FUNCT_2:def 1;
        1 in dom id I[01] by A50,FUNCT_2:def 1;
        then
A53:    [s,1] in [:dom R1, dom id I[01]:] by A52,ZFMISC_1:106;
A54:    R1.s = ((1 - 0)/(1/2 - 0)) * (s - 0) + 0 by A47,A48,Th39
          .= 2 * s;
A55:    2 * s is Point of I[01] by A47,Th6;
        h.(s,1) = K1.(s,1) by A26,A49,FUNCT_4:12
          .= f.(f1.(s,1)) by A51,FUNCT_1:23
          .= f.(R1.s,(id I[01]).1) by A53,FUNCT_3:86
          .= f.(2*s,1) by A7,A54,TMAP_1:91
          .= P2.(2 * s) by A5,A55;
        hence thesis by A1,A2,A47,BORSUK_2:def 5;
      end;
      suppose
A56:    s >= 1/2;
A57:    s <= 1 by BORSUK_1:86;
        then s in [.1/2,1.] by A56,XXREAL_1:1;
        then
A58:    s in the carrier of Closed-Interval-TSpace(1/2,1) &
        1 in the carrier of I[01] by BORSUK_1:86,TOPMETR:25;
        then
A59:    [s,1] in dom K2 by A10,ZFMISC_1:106;
A60:    [s,1] in dom g1 by A12,A58,ZFMISC_1:106;
A61:    s in dom R2 by A58,FUNCT_2:def 1;
        1 in dom id I[01] by A58,FUNCT_2:def 1;
        then
A62:    [s,1] in [:dom R2, dom id I[01]:] by A61,ZFMISC_1:106;
A63:    R2.s = ((1 - 0)/(1 - 1/2)) * (s - 1/2) + 0 by A56,A57,Th39
          .= 2 * s - 1;
A64:    2 * s - 1 is Point of I[01] by A56,Th7;
        h.(s,1) = K2.(s,1) by A26,A59,FUNCT_4:14
          .= g.(g1.(s,1)) by A60,FUNCT_1:23
          .= g.(R2.s,(id I[01]).1) by A62,FUNCT_3:86
          .= g.(2*s-1,1) by A7,A63,TMAP_1:91
          .= Q2.(2 * s - 1) by A6,A64;
        hence thesis by A1,A2,A56,BORSUK_2:def 5;
      end;
    end;
    hence thesis by A28;
  end;
  for t being Point of I[01] holds h.(0,t) = a & h.(1,t) = c
  proof
    let t be Point of I[01];
A65: dom K2 = the carrier of [:Closed-Interval-TSpace(1/2,1), I[01]:]
    by FUNCT_2:def 1
      .= [:the carrier of Closed-Interval-TSpace(1/2,1),
    the carrier of I[01]:] by BORSUK_1:def 5;
    not 0 in [.1/2,1.] by XXREAL_1:1;
    then not 0 in the carrier of Closed-Interval-TSpace(1/2,1) by TOPMETR:25;
    then
A66: not [0,t] in dom K2 by A65,ZFMISC_1:106;
    1 in [.1/2,1.] by XXREAL_1:1;
    then
A67: 1 in the carrier of Closed-Interval-TSpace (1/2,1) by TOPMETR:25;
    then
A68: [1,t] in dom K2 by A65,ZFMISC_1:106;
    0 in [.0,1/2.] by XXREAL_1:1;
    then
A69: 0 in the carrier of Closed-Interval-TSpace (0,1/2) by TOPMETR:25;
    then
A70: 0 in dom R1 by FUNCT_2:def 1;
A71: t in the carrier of I[01];
A72: [0,t] in dom f1 by A11,A69,ZFMISC_1:106;
    1 in [.1/2,1.] by XXREAL_1:1;
    then 1 in the carrier of Closed-Interval-TSpace (1/2,1) by TOPMETR:25;
    then
A73: [1,t] in dom g1 by A12,ZFMISC_1:106;
    t in dom id I[01] by A71,FUNCT_2:def 1;
    then
A74: [0,t] in [:dom R1, dom id I[01]:] by A70,ZFMISC_1:106;
A75: 1 in dom R2 by A67,FUNCT_2:def 1;
    t in the carrier of I[01];
    then t in dom id I[01] by FUNCT_2:def 1;
    then
A76: [1,t] in [:dom R2, dom id I[01]:] by A75,ZFMISC_1:106;
    thus h.(0,t) = K1.(0,t) by A26,A66,FUNCT_4:12
      .= f.(f1.(0,t)) by A72,FUNCT_1:23
      .= f.(R1.0,(id I[01]).t) by A74,FUNCT_3:86
      .= f.(R1.0,t) by TMAP_1:91
      .= f.(0,t) by Th37
      .= a by A5;
    h.(1,t) = K2.(1,t) by A26,A68,FUNCT_4:14
      .= g.(g1.(1,t)) by A73,FUNCT_1:23
      .= g.(R2.1,(id I[01]).t) by A76,FUNCT_3:86
      .= g.(R2.1,t) by TMAP_1:91
      .= g.(1,t) by Th37
      .= c by A6;
    hence thesis;
  end;
  hence thesis by A26,A27;
end;

theorem
  for P1, P2 being Path of a1, b1, Q1, Q2 being Path of b1, c1 st
  P1, P2 are_homotopic & Q1, Q2 are_homotopic holds
  P1 + Q1, P2 + Q2 are_homotopic
proof
  let P1, P2 be Path of a1, b1, Q1, Q2 be Path of b1, c1;
  a1, b1 are_connected & b1, c1 are_connected by BORSUK_2:def 3;
  hence thesis by Th83;
end;

theorem Th85:
  for P, Q being Path of a, b st a, b are_connected &
  P, Q are_homotopic holds -P, -Q are_homotopic
proof
  let P, Q be Path of a, b;
  assume
A1: a,b are_connected;
  assume P, Q are_homotopic;
  then consider f being Function of [:I[01],I[01]:], T such that
A2: f is continuous &
  for s being Point of I[01] holds f.(s,0) = P.s & f.(s,1) = Q.s &
  for t being Point of I[01] holds f.(0,t) = a & f.(1,t) = b
  by BORSUK_2:def 7;
  reconsider fB = L[01]((0,1)(#),(#)(0,1)) as continuous Function
  of I[01], I[01] by TOPMETR:27,TREAL_1:11;
  reconsider fF = id I[01] as continuous Function of I[01], I[01];
  set F = [:fB, fF:];
A3: F is continuous by BORSUK_2:12;
A4: dom fB = the carrier of I[01] & dom fF = the carrier of I[01]
  by FUNCT_2:def 1;
A5: 0 is Point of I[01] by BORSUK_1:86;
  reconsider ff = f * F as Function of [:I[01],I[01]:], T;
  take ff;
  thus ff is continuous by A2,A3;
A6: for s being Point of I[01] holds ff.(s,0) = (-P).s & ff.(s,1) = (-Q).s
  proof
    let s be Point of I[01];
A7: for t being Point of I[01], t' being Real st t = t' holds fB.t = 1-t'
    proof
      let t be Point of I[01], t' be Real;
      assume
A8:   t = t';
      reconsider ee = t as Point of Closed-Interval-TSpace (0,1) by TOPMETR:27;
A9:   (0,1)(#) = 1 & (#)(0,1) = 0 by TREAL_1:def 1,def 2;
      fB.t = fB.ee
        .= ((0-1)*t' + 1) by A8,A9,TREAL_1:10
        .= (1 - 1*t');
      hence thesis;
    end;
A10: s in dom fB & 0 in dom fF & 1 in dom fF by A4,BORSUK_1:86;
A11: s is Point of I[01] & s is Real by XREAL_0:def 1;
A12: 1-s is Point of I[01] & 1-s is Real by JORDAN5B:4;
A13: fB.s = 1 - s by A7,A11;
A14: F.(s,0) = [fB.s,fF.0] by A10,FUNCT_3:def 9
      .= [1-s, 0] by A5,A13,TMAP_1:91;
A15: 1 is Point of I[01] by BORSUK_1:86;
A16: F.(s,1) = [fB.s,fF.1] by A10,FUNCT_3:def 9
      .= [1-s,1] by A13,A15,TMAP_1:91;
A17: dom F = [:dom fB, dom fF:] by FUNCT_3:def 9;
    then
A18: [s,1] in dom F by A10,ZFMISC_1:106;
    [s,0] in dom F by A10,A17,ZFMISC_1:106;
    then
A19: ff.(s,0) = f.(1-s,0) by A14,FUNCT_1:23
      .= P.(1-s) by A2,A12
      .= (-P).s by A1,BORSUK_2:def 6;
    ff.(s,1) = f.(1-s,1) by A16,A18,FUNCT_1:23
      .= Q.(1-s) by A2,A12
      .= (-Q).s by A1,BORSUK_2:def 6;
    hence thesis by A19;
  end;
  for t being Point of I[01] holds ff.(0,t) = b & ff.(1,t) = a
  proof
    let t be Point of I[01];
    t in the carrier of I[01];
    then reconsider tt = t as Real by BORSUK_1:83;
A20: for t being Point of I[01], t' being Real st t = t' holds fB.t = 1-t'
    proof
      let t be Point of I[01], t' be Real;
      assume
A21:  t = t';
      reconsider ee = t as Point of Closed-Interval-TSpace (0,1) by TOPMETR:27;
A22:  (0,1)(#) = 1 & (#)(0,1) = 0 by TREAL_1:def 1,def 2;
      fB.t = fB.ee
        .= ((0-1)*t' + 1) by A21,A22,TREAL_1:10
        .= (1 - 1*t');
      hence thesis;
    end;
    then
A23: fB.0 = 1 - 0 by A5
      .= 1;
    1 is Point of I[01] by BORSUK_1:86;
    then
A24: fB.1 = 1 - 1 by A20
      .= 0;
    dom fB = the carrier of I[01] &
    dom fF = the carrier of I[01] by FUNCT_2:def 1;
    then
A25: 0 in dom fB & 1 in dom fB & t in dom fF by BORSUK_1:86;
    then
A26: F.(0,t) = [fB.0,fF.t] by FUNCT_3:def 9
      .= [1,tt] by A23,TMAP_1:91;
A27: F.(1,t) = [fB.1,fF.t] by A25,FUNCT_3:def 9
      .= [0,tt] by A24,TMAP_1:91;
A28: dom F = [:dom fB, dom fF:] by FUNCT_3:def 9;
    then
A29: [1,t] in dom F by A25,ZFMISC_1:106;
    [0,t] in dom F by A25,A28,ZFMISC_1:106;
    then
A30: ff.(0,t) = f.(1,t) by A26,FUNCT_1:23
      .= b by A2;
    ff.(1,t) = f.(0,t) by A27,A29,FUNCT_1:23
      .= a by A2;
    hence thesis by A30;
  end;
  hence thesis by A6;
end;

theorem
  for P, Q being Path of a1, b1 st
  P, Q are_homotopic holds -P, -Q are_homotopic
proof
  let P, Q be Path of a1, b1;
  a1, b1 are_connected by BORSUK_2:def 3;
  hence thesis by Th85;
end;

theorem
  for P, Q, R be Path of a, b holds
  P, Q are_homotopic & Q, R are_homotopic implies P, R are_homotopic
proof
  let P, Q, R be Path of a, b;
  assume
A1: P, Q are_homotopic & Q, R are_homotopic;
  then consider f being Function of [:I[01],I[01]:], T such that
A2: f is continuous &
  for s being Point of I[01] holds f.(s,0) = P.s & f.(s,1) = Q.s &
  for t being Point of I[01] holds f.(0,t) = a & f.(1,t) = b
  by BORSUK_2:def 7;
  consider g being Function of [:I[01],I[01]:], T such that
A3: g is continuous &
  for s being Point of I[01] holds g.(s,0) = Q.s & g.(s,1) = R.s &
  for t being Point of I[01] holds g.(0,t) = a & g.(1,t) = b
  by A1,BORSUK_2:def 7;
  reconsider P1 = P[01](0, 1/2, (#)(0,1), (0,1)(#)) as
  continuous Function of Closed-Interval-TSpace(0,1/2), I[01]
  by TOPMETR:27,TREAL_1:15;
  reconsider P2 = P[01](1/2, 1, (#)(0,1), (0,1)(#)) as
  continuous Function of Closed-Interval-TSpace(1/2,1), I[01]
  by TOPMETR:27,TREAL_1:15;
  set e1 = [:id I[01], P1:], e2 = [:id I[01], P2:];
A4: dom id I[01] = the carrier of I[01] by FUNCT_2:def 1;
A5: dom P[01](1/2, 1, (#)(0,1), (0,1)(#)) =
  the carrier of Closed-Interval-TSpace(1/2, 1) by FUNCT_2:def 1;
A6: e1 is continuous Function of
  [:I[01],Closed-Interval-TSpace(0,1/2):], [:I[01],I[01]:] by BORSUK_2:12;
A7: e2 is continuous Function of
  [:I[01],Closed-Interval-TSpace(1/2,1):], [:I[01],I[01]:] by BORSUK_2:12;
  set f1 = f * e1, g1 = g * e2;
A8: rng e2 = [:rng id I[01], rng P[01](1/2, 1, (#)(0,1), (0,1)(#)):]
  by FUNCT_3:88;
  dom g = the carrier of [:I[01], I[01]:] by FUNCT_2:def 1
    .= [:the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def 5;
  then
A9: dom g1 = dom e2 by A8,RELAT_1:46,TOPMETR:27,ZFMISC_1:119
    .= [:the carrier of I[01], the carrier of
  Closed-Interval-TSpace(1/2,1):] by A4,A5,FUNCT_3:def 9;
A10: the carrier of Closed-Interval-TSpace(0,1/2) = [.0,1/2.] &
  the carrier of Closed-Interval-TSpace(1/2,1) = [.1/2,1.] by TOPMETR:25;
A11: [.0,1.] c= the carrier of I[01] by BORSUK_1:83;
  [.0,1/2.] c= the carrier of I[01] by BORSUK_1:83,XXREAL_1:34;
  then
A12: [:[.0,1.], [.0,1/2.]:] c= [:the carrier of I[01], the carrier of I[01]:]
  by BORSUK_1:83,ZFMISC_1:119;
A13: 1 in [.0,1.] by XXREAL_1:1;
  0 in [.0,1/2.] by XXREAL_1:1;
  then reconsider Ewa = [:[.0,1.], [.0,1/2.]:] as
  non empty Subset of [:I[01], I[01]:] by A12,A13,BORSUK_1:def 5,ZFMISC_1:106;
  [.1/2,1.] c= the carrier of I[01] by BORSUK_1:83,XXREAL_1:34;
  then
A14: [:[.0,1.], [.1/2,1.]:] c= [:the carrier of I[01], the carrier of I[01]:]
  by BORSUK_1:83,ZFMISC_1:119;
  1 in [.1/2,1.] by XXREAL_1:1;
  then reconsider Ewa1 = [:[.0,1.], [.1/2,1.]:] as
  non empty Subset of [:I[01], I[01]:] by A13,A14,BORSUK_1:def 5,ZFMISC_1:106;
  set T1 = [:I[01], I[01]:] | Ewa;
  set T2 = [:I[01], I[01]:] | Ewa1;
  reconsider A01 = [.0,1.] as non empty Subset of I[01] by A11,XXREAL_1:1;
  reconsider B01 = [.0,1/2.] as non empty Subset of I[01]
  by BORSUK_1:83,XXREAL_1:1,34;
  1/2 in [.0,1/2.] by XXREAL_1:1;
  then
A15: 1/2 in the carrier of Closed-Interval-TSpace(0,1/2) by TOPMETR:25;
  reconsider B02 = [.1/2,1.] as non empty Subset of I[01]
  by BORSUK_1:83,XXREAL_1:1,34;
  A01 = [#] I[01] by BORSUK_1:83;
  then
A16: I[01] = I[01] | A01 by TSEP_1:100;
  Closed-Interval-TSpace (0,1/2) = I[01] | B01 by TOPMETR:31;
  then
A17: T1 = [:I[01],Closed-Interval-TSpace(0,1/2):] by A16,BORSUK_3:26;
  Closed-Interval-TSpace (1/2,1) = I[01] | B02 by TOPMETR:31;
  then
A18: T2 = [:I[01],Closed-Interval-TSpace(1/2,1):] by A16,BORSUK_3:26;
A19: [#] T1 = Ewa & [#] T2 = Ewa1 by PRE_TOPC:def 10;
  then
A20: [#] T1 \/ [#] T2 = [:[.0,1.], [.0,1/2.] \/ [.1/2,1.]:] by ZFMISC_1:120
    .= [:the carrier of I[01], the carrier of I[01]:]
  by BORSUK_1:83,XXREAL_1:174
    .= [#] [:I[01],I[01]:] by BORSUK_1:def 5;
  reconsider f1 as continuous Function of T1, T by A2,A6,A17;
  reconsider g1 as continuous Function of T2,T by A3,A7,A18;
A21: 0 is Point of I[01] & 1 is Point of I[01] & 1/2 is Point of I[01]
  by BORSUK_1:86;
  then
A22: [.0,1.] is compact Subset of I[01] &
  [.0,1/2.] is compact Subset of I[01] by BORSUK_4:49;
  then Ewa is compact Subset of [:I[01], I[01]:] by BORSUK_3:27;
  then
A23: T1 is compact;
  [.1/2,1.] is compact Subset of I[01] by A21,BORSUK_4:49;
  then Ewa1 is compact Subset of [:I[01], I[01]:] by A22,BORSUK_3:27;
  then
A24: T2 is compact;
A25: [#] T1 /\ [#] T2
  = [:[.0,1.], [.0,1/2.] /\ [.1/2,1.]:] by A19,ZFMISC_1:122
    .= [:[.0,1.], {1/2} :] by TOPMETR2:1;
A26: dom e1 = the carrier of [:I[01], Closed-Interval-TSpace(0,1/2):]
  by FUNCT_2:def 1
    .= [:the carrier of I[01],
  the carrier of Closed-Interval-TSpace(0,1/2):] by BORSUK_1:def 5;
A27: dom e2 = the carrier of [:I[01], Closed-Interval-TSpace(1/2,1):]
  by FUNCT_2:def 1
    .= [:the carrier of I[01],
  the carrier of Closed-Interval-TSpace(1/2,1):] by BORSUK_1:def 5;
A28: dom e1 = [:dom id I[01], dom P1:] by FUNCT_3:def 9;
A29: dom e2 = [:dom id I[01], dom P2:] by FUNCT_3:def 9;
A30: 1/2 in [.1/2,1.] by XXREAL_1:1;
  then
A31: 1/2 in the carrier of Closed-Interval-TSpace(1/2,1) by TOPMETR:25;
  for p be set st p in [#] T1 /\ [#] T2 holds f1.p = g1.p
  proof
    let p be set;
    assume p in [#] T1 /\ [#] T2;
    then consider x, y be set such that
A32: x in [.0,1.] & y in {1/2} & p = [x,y] by A25,ZFMISC_1:def 2;
A33: y = 1/2 by A32,TARSKI:def 1;
    x in { r where r is Real : 0 <= r & r <= 1 } by A32,RCOMP_1:def 1;
    then consider r1 be Real such that
A34: r1 = x & 0 <= r1 & r1 <= 1;
    reconsider x' = x as Point of I[01] by A34,BORSUK_1:86;
    f1.p = g1.p
    proof
A35:  x in the carrier of I[01] by A34,BORSUK_1:86;
      1/2 in [.0,1/2.] by XXREAL_1:1;
      then reconsider y' = 1/2 as Point of Closed-Interval-TSpace(0,1/2)
      by TOPMETR:25;
      reconsider r1 = (#)(0,1), r2 = (0,1)(#) as Real
      by BORSUK_1:def 17,def 18,TREAL_1:8;
      set t' = 1/2;
A36:  P1.y' = ((r2 - r1)/(1/2 - 0))*t' + ((1/2)*r1 - 0 *r2)/(1/2 - 0)
      by TREAL_1:14
        .= ((1 - r1)/(1/2 - 0))*t' + ((1/2)*r1 - 0 *r2)/(1/2 - 0)
      by TREAL_1:def 2
        .= ((1 - 0)/(1/2 - 0))*t' + ((1/2)*r1 - 0 *r2)/(1/2 - 0)
      by TREAL_1:def 1
        .= ((1 - 0)/(1/2 - 0))*t' + ((1/2)*0 - 0 *1)/(1/2 - 0)
      by TREAL_1:def 1
        .= 1;
      reconsider y' = 1/2 as Point of Closed-Interval-TSpace(1/2,1)
      by A30,TOPMETR:25;
A37:  P2.y' = ((r2 - r1)/(1 - 1/2))*t' + (1*r1 - (1/2)*r2)/(1 - 1/2)
      by TREAL_1:14
        .= 0 by BORSUK_1:def 17,TREAL_1:8;
A38:  [x,y] in dom e1 by A15,A26,A33,A35,ZFMISC_1:106;
A39:  [x,y] in dom e2 by A27,A31,A33,A35,ZFMISC_1:106;
      f1.p = f.(e1.(x,y)) by A32,A38,FUNCT_1:23
        .= f.(id I[01].x, P1.y) by A28,A38,FUNCT_3:86
        .= f.(x',1) by A33,A36,TMAP_1:91
        .= Q.x' by A2
        .= g.(x',0) by A3
        .= g.(id I[01]. x', P2.y) by A33,A37,TMAP_1:91
        .= g.(e2.(x, y)) by A29,A39,FUNCT_3:86
        .= g1. p by A32,A39,FUNCT_1:23;
      hence thesis;
    end;
    hence thesis;
  end;
  then consider h being Function of [:I[01],I[01]:], T such that
A40: h = f1 +* g1 & h is continuous by A20,A23,A24,BORSUK_2:1;
A41: the carrier of Closed-Interval-TSpace(1/2,1) = [. 1/2,1 .] by TOPMETR:25;
A42: the carrier of Closed-Interval-TSpace(0,1/2) = [. 0,1/2 .] by TOPMETR:25;
A43: for s being Point of I[01] holds h.(s,0) = P.s & h.(s,1) = R.s
  proof
    let s be Point of I[01];
A44: the carrier of Closed-Interval-TSpace(1/2,1) = [. 1/2,1 .] by TOPMETR:25;
    then not 0 in the carrier of Closed-Interval-TSpace(1/2,1) by XXREAL_1:1;
    then
A45: not [s,0] in dom g1 by A9,ZFMISC_1:106;
A46: 0 in the carrier of Closed-Interval-TSpace(0,1/2) by A42,XXREAL_1:1;
    then
A47: [s,0] in dom e1 by A26,ZFMISC_1:106;
    reconsider r1 = (#)(0,1), r2 = (0,1)(#) as Real
    by BORSUK_1:def 17,def 18,TREAL_1:8;
A48: P1.0 = ((r2 - r1)/(1/2 - 0))*0 + ((1/2)*r1 - 0 *r2)/(1/2 - 0)
    by A46,TREAL_1:14
      .= ((1/2)*0 - 0 *r2)/(1/2 - 0)by TREAL_1:def 1;
A49: h.(s,0) = f1.(s,0) by A40,A45,FUNCT_4:12
      .= f.(e1.(s,0)) by A47,FUNCT_1:23
      .= f.(id I[01].s, P1.0) by A28,A47,FUNCT_3:86
      .= f.(s,0) by A48,TMAP_1:91
      .= P.s by A2;
A50: 1 in the carrier of Closed-Interval-TSpace(1/2,1) by A44,XXREAL_1:1;
    then
A51: [s,1] in dom g1 by A9,ZFMISC_1:106;
A52: [s,1] in dom e2 by A27,A50,ZFMISC_1:106;
    1/2 < 1 & 1 = (0,1)(#) & 1 = (1/2,1)(#) by TREAL_1:def 2;
    then
A53: P2.1 = 1 by TREAL_1:16;
    h.(s,1) = g1.(s,1) by A40,A51,FUNCT_4:14
      .= g.(e2.(s,1)) by A52,FUNCT_1:23
      .= g.(id I[01]. s, P2.1) by A29,A52,FUNCT_3:86
      .= g.(s,1) by A53,TMAP_1:91
      .= R.s by A3;
    hence thesis by A49;
  end;
A54: 1 in the carrier of I[01] by BORSUK_1:86;
  for t being Point of I[01] holds h.(0,t) = a & h.(1,t) = b
  proof
    let t be Point of I[01];
    per cases;
    suppose
A55:  t < 1/2;
A56:  0 <= t by BORSUK_1:86;
A57:  0 in the carrier of I[01] by BORSUK_1:86;
      not t in the carrier of Closed-Interval-TSpace(1/2,1)
      by A41,A55,XXREAL_1:1;
      then
A58:  not [0,t] in dom g1 by A9,ZFMISC_1:106;
A59:  t in the carrier of Closed-Interval-TSpace(0,1/2)
      by A42,A55,A56,XXREAL_1:1;
      then
A60:  [0,t] in dom e1 by A26,A57,ZFMISC_1:106;
      reconsider r1 = (#)(0,1), r2 = (0,1)(#) as Real
      by BORSUK_1:def 17,def 18,TREAL_1:8;
A61:  t is Real by XREAL_0:def 1;
      then P1.t = ((r2 - r1)/(1/2 - 0))*t + ((1/2)*r1 - 0 *r2)/(1/2 - 0)
      by A59,TREAL_1:14
        .= ((1 - r1)/(1/2))*t + ((1/2)*r1)/(1/2) by TREAL_1:def 2
        .= ((1 - 0)/(1/2))*t + ((1/2)*r1)/(1/2) by TREAL_1:def 1
        .= (1/(1/2))*t + ((1/2)*0)/(1/2) by TREAL_1:def 1
        .= 2*t;
      then
A62:  P1.t is Point of I[01] by A55,Th6;
      thus h.(0,t) = f1.(0,t) by A40,A58,FUNCT_4:12
        .= f.(e1.(0,t)) by A60,FUNCT_1:23
        .= f.(id I[01].0, P1.t) by A28,A60,FUNCT_3:86
        .= f.(0,P1.t) by A21,TMAP_1:91
        .= a by A2,A62;
      not t in the carrier of Closed-Interval-TSpace(1/2,1)
      by A10,A55,XXREAL_1:1;
      then
A63:  not [1,t] in dom g1 by A9,ZFMISC_1:106;
      t in the carrier of Closed-Interval-TSpace(0,1/2)
      by A10,A55,A56,XXREAL_1:1;
      then
A64:  [1,t] in dom e1 by A26,A54,ZFMISC_1:106;
      P1.t = ((r2 - r1)/(1/2 - 0))*t + ((1/2)*r1 - 0 *r2)/(1/2 - 0)
      by A59,A61,TREAL_1:14
        .= ((1 - r1)/(1/2))*t + ((1/2)*r1)/(1/2) by TREAL_1:def 2
        .= ((1 - 0)/(1/2))*t + ((1/2)*r1)/(1/2) by TREAL_1:def 1
        .= (1/(1/2))*t + ((1/2)*0)/(1/2) by TREAL_1:def 1
        .= 2*t;
      then
A65:  P1.t is Point of I[01] by A55,Th6;
      thus h.(1,t) = f1.(1,t) by A40,A63,FUNCT_4:12
        .= f.(e1.(1,t)) by A64,FUNCT_1:23
        .= f.(id I[01]. 1, P1.t) by A28,A64,FUNCT_3:86
        .= f.(1,P1.t) by A21,TMAP_1:91
        .= b by A2,A65;
    end;
    suppose
A66:  t >= 1/2;
A67:  0 in the carrier of I[01] by BORSUK_1:86;
      t <= 1 by BORSUK_1:86;
      then
A68:  t in the carrier of Closed-Interval-TSpace(1/2,1) by A41,A66,XXREAL_1:1;
      then
A69:  [0,t] in dom g1 by A9,A67,ZFMISC_1:106;
A70:  [0,t] in dom e2 by A27,A67,A68,ZFMISC_1:106;
      reconsider r1 = (#)(0,1), r2 = (0,1)(#) as Real
      by BORSUK_1:def 17,def 18,TREAL_1:8;
A71:  t is Real by XREAL_0:def 1;
      then P2.t = ((r2 - r1)/(1 - 1/2))*t + (1*r1 - (1/2) *r2)/(1 - 1/2)
      by A68,TREAL_1:14
        .= ((1 - r1)/(1/2))*t + (1*r1 - (1/2) *r2)/(1/2) by TREAL_1:def 2
        .= ((1 - 0)/(1/2))*t + (1*r1 - (1/2) *r2)/(1/2) by TREAL_1:def 1
        .= (1/(1/2))*t + (1*0 - (1/2) *r2)/(1/2) by TREAL_1:def 1
        .= (1/(1/2))*t + (1*0 - (1/2) *1)/(1/2) by TREAL_1:def 2
        .= 2*t - 1;
      then
A72:  P2.t is Point of I[01] by A66,Th7;
      thus h.(0,t) = g1.(0,t) by A40,A69,FUNCT_4:14
        .= g.(e2.(0,t)) by A70,FUNCT_1:23
        .= g.(id I[01]. 0, P2.t) by A29,A70,FUNCT_3:86
        .= g.(0,P2.t) by A21,TMAP_1:91
        .= a by A3,A72;
A73:  [1,t] in dom g1 by A9,A54,A68,ZFMISC_1:106;
A74:  [1,t] in dom e2 by A27,A54,A68,ZFMISC_1:106;
      P2.t = ((r2 - r1)/(1 - 1/2))*t + (1*r1 - (1/2) *r2)/(1 - 1/2)
      by A68,A71,TREAL_1:14
        .= ((1 - r1)/(1/2))*t + (1*r1 - (1/2) *r2)/(1/2) by TREAL_1:def 2
        .= ((1 - 0)/(1/2))*t + (1*r1 - (1/2) *r2)/(1/2) by TREAL_1:def 1
        .= 2*t + (1*0 - (1/2) *r2)/(1/2) by TREAL_1:def 1
        .= 2*t + (-(1/2) *r2)/(1/2)
        .= 2*t + (-(1/2) *1)/(1/2) by TREAL_1:def 2
        .= 2*t - 1;
      then
A75:  P2.t is Point of I[01] by A66,Th7;
      thus h.(1,t) = g1.(1,t) by A40,A73,FUNCT_4:14
        .= g.(e2.(1,t)) by A74,FUNCT_1:23
        .= g.(id I[01]. 1, P2.t) by A29,A74,FUNCT_3:86
        .= g.(1,P2.t) by A21,TMAP_1:91
        .= b by A3,A75;
    end;
  end;
  hence thesis by A40,A43,BORSUK_2:def 7;
end;

theorem Th88:
  for P be Path of a, b,
  Q be constant Path of b, b st a, b are_connected holds
  P + Q, P are_homotopic
proof
  let P be Path of a, b, Q be constant Path of b, b such that
A1: a,b are_connected;
  RePar (P, 1RP) = P + Q by A1,Th58;
  hence thesis by A1,Th53,Th55;
end;

theorem
  for P be Path of a1, b1, Q be constant Path of b1, b1 holds
  P + Q, P are_homotopic
proof
  let P be Path of a1, b1, Q be constant Path of b1, b1;
  a1,b1 are_connected by BORSUK_2:def 3;
  hence thesis by Th88;
end;

theorem Th90:
  for P be Path of a, b,
  Q be constant Path of a, a st a, b are_connected holds
  Q + P, P are_homotopic
proof
  let P be Path of a, b, Q be constant Path of a, a such that
A1: a,b are_connected;
  RePar (P, 2RP) = Q + P by A1,Th59;
  hence thesis by A1,Th53,Th56;
end;

theorem
  for P be Path of a1, b1, Q be constant Path of a1, a1 holds
  Q + P, P are_homotopic
proof
  let P be Path of a1, b1, Q be constant Path of a1, a1;
  a1,b1 are_connected by BORSUK_2:def 3;
  hence thesis by Th90;
end;

theorem Th92:
  for P being Path of a, b,
  Q being constant Path of a, a st a, b are_connected holds
  P + - P, Q are_homotopic
proof
  let P be Path of a, b, Q be constant Path of a, a such that
A1: a, b are_connected;
A2: -P is continuous by A1,BORSUK_2:def 2;
  set S = [:I[01],I[01]:];
  set S1 = S|IAA;
  set S2 = S|IBB;
  set S3 = S|ICC;
  reconsider e1 = pr1(the carrier of I[01], the carrier of I[01])
  as continuous Function of S, I[01] by YELLOW12:39;
  reconsider e2 = pr2(the carrier of I[01], the carrier of I[01])
  as continuous Function of S, I[01] by YELLOW12:40;
A3: a, a are_connected;
  then reconsider PP = P + -P as continuous Path of a,a by BORSUK_2:def 2;
  set ff = PP * e1;
  reconsider f = ff|IAA as Function of S1, T by PRE_TOPC:30;
  reconsider f as continuous Function of S1, T by TOPMETR:10;
A4: for x being Point of S1 holds f.x = P.(2 * x`1)
  proof
    let x be Point of S1;
    x in the carrier of S1;
    then
A5: x in IAA by PRE_TOPC:29;
    then
A6: x in the carrier of S;
    then
A7: x in [:the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def 5;
    then
A8: x = [x`1,x`2] by MCART_1:23;
    then
A9: x`1 in the carrier of I[01] & x`2 in the carrier of I[01]
    by A7,ZFMISC_1:106;
    then
A10: e1.(x`1,x`2) = x`1 by FUNCT_3:def 5;
A11: x in dom e1 by A6,FUNCT_2:def 1;
A12: x`1 <= 1/2 by A5,Th67;
    f.x = ff.x by A5,FUNCT_1:72
      .= (P + -P).(e1.x) by A11,FUNCT_1:23
      .= P.(2 * x`1) by A1,A8,A9,A10,A12,BORSUK_2:def 5;
    hence thesis;
  end;
  set gg = (-P) * e2;
  reconsider gg as continuous Function of S, T by A2;
  reconsider g = gg|IBB as Function of S2, T by PRE_TOPC:30;
  reconsider g as continuous Function of S2, T by TOPMETR:10;
A13: for x being Point of S2 holds g.x = P.(1 - x`2)
  proof
    let x be Point of S2;
    x in the carrier of S2;
    then
A14: x in IBB by PRE_TOPC:29;
    then
A15: x in the carrier of S;
    then
A16: x in [:the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def 5;
    then
A17: x = [x`1,x`2] by MCART_1:23;
    then
A18: x`1 in the carrier of I[01] & x`2 in the carrier of I[01]
    by A16,ZFMISC_1:106;
    then
A19: e2.(x`1,x`2) = x`2 by FUNCT_3:def 6;
A20: x in dom e2 by A15,FUNCT_2:def 1;
    g.x = gg.x by A14,FUNCT_1:72
      .= (-P).(e2.x) by A20,FUNCT_1:23
      .= P.(1 - x`2) by A1,A17,A18,A19,BORSUK_2:def 6;
    hence thesis;
  end;
  set hh = PP * e1;
  reconsider h = hh|ICC as Function of S3, T by PRE_TOPC:30;
  reconsider h as continuous Function of S3, T by TOPMETR:10;
A21: for x being Point of S3 holds h.x = (-P).(2 * x`1 - 1)
  proof
    let x be Point of S3;
    x in the carrier of S3;
    then
A22: x in ICC by PRE_TOPC:29;
    then
A23: x in the carrier of S;
    then
A24: x in [:the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def 5;
    then
A25: x = [x`1,x`2] by MCART_1:23;
    then
A26: x`1 in the carrier of I[01] & x`2 in the carrier of I[01]
    by A24,ZFMISC_1:106;
    then
A27: e1.(x`1,x`2) = x`1 by FUNCT_3:def 5;
A28: x in dom e1 by A23,FUNCT_2:def 1;
A29: x`1 >= 1/2 by A22,Th68;
    h.x = hh.x by A22,FUNCT_1:72
      .= (P + - P).(e1.x) by A28,FUNCT_1:23
      .= (-P).(2 * x`1 - 1) by A1,A25,A26,A27,A29,BORSUK_2:def 5;
    hence thesis;
  end;
  set S12 = S | (IAA \/ IBB);
  reconsider S12 as non empty SubSpace of S;
A30: the carrier of S12 = IAA \/ IBB by PRE_TOPC:29;
A31: [#]S1 = IAA by PRE_TOPC:def 10;
A32: [#]S2 = IBB by PRE_TOPC:def 10;

then reconsider s1 = [#]S1, s2 = [#]S2 as Subset of S12 by A30,A31,XBOOLE_1:7;
A33: ([#] S1) \/ ([#] S2) = [#] S12 by A30,A32,PRE_TOPC:def 10;
A34: for p be set st p in ([#] S1) /\ ([#] S2) holds f.p = g.p
  proof
    let p be set;
    assume p in ([#] S1) /\ ([#] S2);
    then p in ([#] S1) /\ IBB by PRE_TOPC:def 10;
    then
A35: p in IAA /\ IBB by PRE_TOPC:def 10;
    then consider r being Point of S such that
A36: r = p & r`2 = 1 - 2 * (r`1) by Th65;
A37: p in IAA & p in IBB by A35,XBOOLE_0:def 3;
    then reconsider pp = p as Point of S1 by PRE_TOPC:29;
A38: 2 * r`1 = 1 - r`2 by A36;
A39: pp is Point of S2 by A37,PRE_TOPC:29;
    f.p = P.(2 * pp`1) by A4
      .= g.p by A13,A36,A38,A39;
    hence thesis;
  end;
A40: S1 is SubSpace of S12 by TOPMETR:29,XBOOLE_1:7;
A41: S2 is SubSpace of S12 by TOPMETR:29,XBOOLE_1:7;
A42: s1 is closed by A31,TOPS_2:34;
  s2 is closed by A32,TOPS_2:34;
  then consider fg being Function of S12, T such that
A43: fg = f +* g & fg is continuous by A33,A34,A40,A41,A42,JGRAPH_2:9;
A44: [#]S3 = ICC by PRE_TOPC:def 10;
  reconsider s12 = [#]S12, s3 = [#]S3 as Subset of S by PRE_TOPC:def 10;
A45: ([#] S12) \/ ([#] S3) = (IAA \/ IBB) \/ ICC by A30,PRE_TOPC:def 10
    .= [#] S by Th64,BORSUK_1:83,def 5;
A46: for p be set st p in ([#] S12) /\ ([#] S3) holds fg.p = h.p
  proof
    let p be set;
    assume p in ([#] S12) /\ ([#] S3);
    then
A47: p in { [1/2,0] } \/ (IBB /\ ICC) by A30,A44,Th80,XBOOLE_1:23;
    [1/2,0] in IBB /\ ICC by Th74,Th75,XBOOLE_0:def 3;
    then { [1/2,0] } c= IBB /\ ICC by ZFMISC_1:37;
    then
A48: p in IBB /\ ICC by A47,XBOOLE_1:12;
    then consider q being Point of S such that
A49: q = p & q`2 = 2 * (q`1) - 1 by Th66;
A50: p in IBB & p in ICC by A48,XBOOLE_0:def 3;
    then reconsider pp = p as Point of S3 by PRE_TOPC:29;
A51: pp is Point of S2 by A50,PRE_TOPC:29;
A52: 2 * pp`1 - 1 is Point of I[01] by A49,Th31;
    p in the carrier of S2 by A50,PRE_TOPC:29;
    then p in dom g by FUNCT_2:def 1;
    then fg.p = g.p by A43,FUNCT_4:14
      .= P.(1 - pp`2) by A13,A51
      .= (-P).(2 * pp`1 - 1) by A1,A49,A52,BORSUK_2:def 6
      .= h.p by A21;
    hence thesis;
  end;
A53: s12 is closed by A30,TOPS_1:36;
  s3 = ICC by PRE_TOPC:def 10;
  then consider H being Function of S, T such that
A54: H = fg +* h & H is continuous by A43,A45,A46,A53,JGRAPH_2:9;
A55: for s being Point of I[01] holds H.(s,0) = (P+ -P).s & H.(s,1) = Q.s
  proof
    let s be Point of I[01];
    thus H.(s,0) = (P+ -P).s
    proof
A56:  [s,0]`1 = s by MCART_1:7;
      per cases by REAL_1:def 5;
      suppose
A57:    s < 1/2;
        then
A58:    [s,0] in IAA by Th78;
        not [s,0] in ICC by A57,Th79;
        then not [s,0] in the carrier of S3 by P