:: Continuity of Mappings over the Union of Subspaces
::  by Zbigniew Karno
::
:: Received May 22, 1992
:: Copyright (c) 1992-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies XBOOLE_0, PRE_TOPC, TARSKI, SUBSET_1, FUNCT_1, RELAT_1, FUNCT_4,
      STRUCT_0, RCOMP_1, SETFAM_1, CONNSP_2, ORDINAL2, FUNCOP_1, FUNCT_3,
      ZFMISC_1, TSEP_1, CONNSP_1, TMAP_1, PARTFUN1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1,
      PARTFUN1, FUNCT_2, FUNCT_4, FUNCOP_1, DOMAIN_1, STRUCT_0, PRE_TOPC,
      CONNSP_1, CONNSP_2, BORSUK_1, TSEP_1;
 constructors SETFAM_1, FUNCT_4, CONNSP_1, BORSUK_1, TSEP_1, FUNCOP_1;
 registrations XBOOLE_0, SUBSET_1, FUNCT_1, FUNCT_2, STRUCT_0, PRE_TOPC,
      BORSUK_1, TSEP_1, RELSET_1, RELAT_1, PARTFUN1, TOPS_1;
 requirements BOOLE, SUBSET;
 definitions PRE_TOPC, BORSUK_1, XBOOLE_0, STRUCT_0, RELAT_1;
 theorems TARSKI, SUBSET_1, FUNCT_1, FUNCT_2, FUNCT_4, ZFMISC_1, PRE_TOPC,
      CONNSP_2, TOPS_2, BORSUK_1, TSEP_1, RELAT_1, RELSET_1, XBOOLE_0,
      XBOOLE_1, CONNSP_1;

begin :: 1. Set-Theoretic Preliminaries.

registration
  let X be non empty TopSpace;
  let X1, X2 be non empty SubSpace of X;
  cluster X1 union X2 -> TopSpace-like;
  coherence;
end;

definition
  let A,B be non empty set;
  let A1,A2 be non empty Subset of A;
  let f1 be Function of A1,B, f2 be Function of A2,B;
  assume
A1: f1|(A1 /\ A2) = f2|(A1 /\ A2);
  func f1 union f2 -> Function of A1 \/ A2,B means
  :Def1:
  it|A1 = f1 & it|A2 = f2;
  existence
  proof
    reconsider A0 = A1 \/ A2 as non empty Subset of A;
    set G = f2 +*f1;
    set H = f1 +* f2;
    rng H c= rng f1 \/ rng f2 by FUNCT_4:17;
    then
A2: rng H c= B by XBOOLE_1:1;
    rng G c= rng f2 \/ rng f1 by FUNCT_4:17;
    then
A3: rng G c= B by XBOOLE_1:1;
A4: dom f1 = A1 & dom f2 = A2 by FUNCT_2:def 1;
    then dom H = A1 \/ A2 by FUNCT_4:def 1;
    then reconsider F0 = H as Function of A1 \/ A2,B by A2,FUNCT_2:def 1
,RELSET_1:4;
    dom G = A1 \/ A2 by A4,FUNCT_4:def 1;
    then reconsider F1 = G as Function of A1 \/ A2,B by A3,FUNCT_2:def 1
,RELSET_1:4;
    take F0;
A5: now
      let a be Element of A0;
      thus a in A2 implies H.a = f2.a by A4,FUNCT_4:def 1;
      thus a in A1 \ A2 implies H.a = f1.a
      proof
        assume a in A1 \ A2;
        then not a in A2 by XBOOLE_0:def 5;
        hence thesis by A4,FUNCT_4:def 1;
      end;
    end;
A6: now
      let a be Element of A0;
      thus a in A1 implies G.a = f1.a by A4,FUNCT_4:def 1;
      thus a in A2 \ A1 implies G.a = f2.a
      proof
        assume a in A2 \ A1;
        then not a in A1 by XBOOLE_0:def 5;
        hence thesis by A4,FUNCT_4:def 1;
      end;
    end;
A7: now
      let a be Element of A0;
A8:   now
        assume
A9:     a in A1 /\ A2;
        then
A10:    a in A1 by XBOOLE_0:def 4;
        a in A2 by A9,XBOOLE_0:def 4;
        then
A11:    F0.a = f2.a by A5;
        f1.a = (f2|(A1 /\ A2)).a by A1,A9,FUNCT_1:49
          .= f2.a by A9,FUNCT_1:49;
        hence F0.a = F1.a by A6,A10,A11;
      end;
A12:  now
A13:    now
          assume
A14:      a in A2 \ A1;
          A2 \ A1 c= A2 by XBOOLE_1:36;
          hence F0.a = f2.a by A5,A14
            .= F1.a by A6,A14;
        end;
A15:    now
A16:      A1 \ A2 c= A1 by XBOOLE_1:36;
          assume
A17:      a in A1 \ A2;
          hence F0.a = f1.a by A5
            .= F1.a by A6,A17,A16;
        end;
        assume a in A1 \+\ A2;
        hence F0.a = F1.a by A15,A13,XBOOLE_0:def 3;
      end;
      A0 = (A1 \+\ A2) \/ (A1 /\ A2) by XBOOLE_1:93;
      hence F0.a = F1.a by A12,A8,XBOOLE_0:def 3;
    end;
    now
      thus A1 is non empty Subset of A0 by XBOOLE_1:7;
      let a be Element of A0 such that
A18:  a in A1;
      thus F0.a = F1.a by A7
        .= f1.a by A6,A18;
    end;
    hence F0|A1 = f1 by FUNCT_2:96;
    A2 is non empty Subset of A0 by XBOOLE_1:7;
    hence thesis by A5,FUNCT_2:96;
  end;
  uniqueness
  proof
    reconsider A0 = A1 \/ A2 as non empty Subset of A;
    let F, G be Function of A1 \/ A2,B such that
A19: F|A1 = f1 and
A20: F|A2 = f2 and
A21: G|A1 = f1 and
A22: G|A2 = f2;
    now
      let a be Element of A0;
A23:  now
        assume
A24:    a in A2;
        hence F.a = (G|A2).a by A20,A22,FUNCT_1:49
          .= G.a by A24,FUNCT_1:49;
      end;
      now
        assume
A25:    a in A1;
        hence F.a = (G|A1).a by A19,A21,FUNCT_1:49
          .= G.a by A25,FUNCT_1:49;
      end;
      hence F.a = G.a by A23,XBOOLE_0:def 3;
    end;
    hence thesis by FUNCT_2:63;
  end;
end;

theorem Th1:
  for A, B be non empty set, A1, A2 being non empty Subset of A st
A1 misses A2 for f1 being Function of A1,B, f2 being Function of A2,B holds f1|
  (A1 /\ A2) = f2|(A1 /\ A2) & (f1 union f2)|A1 = f1 & (f1 union f2)|A2 = f2
proof
  let A, B be non empty set, A1, A2 be non empty Subset of A;
  assume A1 misses A2;
  then
A1: A1 /\ A2 = {} by XBOOLE_0:def 7;
  let f1 be Function of A1,B, f2 be Function of A2,B;
  A1 /\ A2 c= A2 by XBOOLE_1:17;
  then reconsider g2 = f2|(A1 /\ A2) as Function of {},B by A1,FUNCT_2:32;
  A1 /\ A2 c= A1 by XBOOLE_1:17;
  then reconsider g1 = f1|(A1 /\ A2) as Function of {},B by A1,FUNCT_2:32;
  g1 = g2;
  hence thesis by Def1;
end;

reserve A, B for non empty set,
  A1, A2, A3 for non empty Subset of A;

theorem Th2:
  for g being Function of A1 \/ A2,B, g1 being Function of A1,B, g2
  being Function of A2,B st g|A1 = g1 & g|A2 = g2 holds g = g1 union g2
proof
  let g be Function of A1 \/ A2,B, g1 be Function of A1,B, g2 be Function of
  A2,B;
  assume
A1: g|A1 = g1 & g|A2 = g2;
  A2 c= A1 \/ A2 by XBOOLE_1:7;
  then reconsider f2 = g|A2 as Function of A2,B by FUNCT_2:32;
  A1 c= A1 \/ A2 by XBOOLE_1:7;
  then reconsider f1 = g|A1 as Function of A1,B by FUNCT_2:32;
A2: A1 /\ A2 c= A2 by XBOOLE_1:17;
  A1 /\ A2 c= A1 by XBOOLE_1:17;
  then f1|(A1 /\ A2) = g|(A1 /\ A2) by FUNCT_1:51
    .= f2|(A1 /\ A2) by A2,FUNCT_1:51;
  hence thesis by A1,Def1;
end;

theorem
  for f1 being Function of A1,B, f2 being Function of A2,B st f1|(A1 /\
  A2) = f2|(A1 /\ A2) holds f1 union f2 = f2 union f1
proof
  let f1 be Function of A1,B, f2 be Function of A2,B;
  assume f1|(A1 /\ A2) = f2|(A1 /\ A2);
  then (f1 union f2)|A1 = f1 & (f1 union f2)|A2 = f2 by Def1;
  hence thesis by Th2;
end;

theorem
  for A12, A23 being non empty Subset of A st A12 = A1 \/ A2 & A23 = A2
  \/ A3 for f1 being Function of A1,B, f2 being Function of A2,B, f3 being
  Function of A3,B st f1|(A1 /\ A2) = f2|(A1 /\ A2) & f2|(A2 /\ A3) = f3|(A2 /\
A3) & f1|(A1 /\ A3) = f3|(A1 /\ A3) for f12 being Function of A12,B, f23 being
Function of A23,B st f12 = f1 union f2 & f23 = f2 union f3 holds f12 union f3 =
  f1 union f23
proof
  let A12, A23 be non empty Subset of A such that
A1: A12 = A1 \/ A2 and
A2: A23 = A2 \/ A3;
  let f1 be Function of A1,B, f2 be Function of A2,B, f3 be Function of A3,B
  such that
A3: f1|(A1 /\ A2) = f2|(A1 /\ A2) and
A4: f2|(A2 /\ A3) = f3|(A2 /\ A3) and
A5: f1|(A1 /\ A3) = f3|(A1 /\ A3);
  let f12 be Function of A12,B, f23 be Function of A23,B such that
A6: f12 = f1 union f2 and
A7: f23 = f2 union f3;
A8: (f12|A2)|(A2 /\ A3) = f2|(A2 /\ A3) by A3,A6,Def1;
  A1 \/ A23 = A12 \/ A3 by A1,A2,XBOOLE_1:4;
  then reconsider f = f12 union f3 as Function of A1 \/ A23,B;
  A12 /\ A3 c= A12 by XBOOLE_1:17;
  then reconsider F = f12|(A12 /\ A3) as Function of A12 /\ A3,B by FUNCT_2:32;
A9: A2 /\ A3 c= A2 by XBOOLE_1:17;
A10: f12|A2 = f2 by A3,A6,Def1;
  A23 c= A1 \/ A23 by XBOOLE_1:7;
  then reconsider H = f|A23 as Function of A23,B by FUNCT_2:32;
A11: A2 c= A12 by A1,XBOOLE_1:7;
  A12 /\ A3 c= A3 by XBOOLE_1:17;
  then reconsider G = f3|(A12 /\ A3) as Function of A12 /\ A3,B by FUNCT_2:32;
A12: A1 /\ A3 c= A1 by XBOOLE_1:17;
A13: (f12|A1)|(A1 /\ A3) = f1|(A1 /\ A3) by A3,A6,Def1;
  now
    let x be set;
    assume
A14: x in A12 /\ A3;
A15: A1 /\ A3 c= A12 /\ A3 by A1,XBOOLE_1:7,26;
A16: now
      assume
A17:  x in A1 /\ A3;
      hence F.x = (F|(A1 /\ A3)).x by FUNCT_1:49
        .= (f12|(A1 /\ A3)).x by A15,FUNCT_1:51
        .= (f3|(A1 /\ A3)).x by A5,A13,A12,FUNCT_1:51
        .= (G|(A1 /\ A3)).x by A15,FUNCT_1:51
        .= G.x by A17,FUNCT_1:49;
    end;
A18: A2 /\ A3 c= A12 /\ A3 by A1,XBOOLE_1:7,26;
A19: now
      assume
A20:  x in A2 /\ A3;
      hence F.x = (F|(A2 /\ A3)).x by FUNCT_1:49
        .= (f12|(A2 /\ A3)).x by A18,FUNCT_1:51
        .= (f3|(A2 /\ A3)).x by A4,A8,A9,FUNCT_1:51
        .= (G|(A2 /\ A3)).x by A18,FUNCT_1:51
        .= G.x by A20,FUNCT_1:49;
    end;
    A12 /\ A3 = (A1 /\ A3) \/ (A2 /\ A3) by A1,XBOOLE_1:23;
    hence F.x = G.x by A14,A16,A19,XBOOLE_0:def 3;
  end;
  then
A21: f12|(A12 /\ A3) = f3|(A12 /\ A3) by FUNCT_2:12;
  then
A22: (f|A12)|A1 = f12|A1 by Def1;
  (f|A12)|A2 = f12|A2 by A21,Def1;
  then
A23: f|A2 = f2 by A10,A11,FUNCT_1:51;
  now
    let x be set;
    assume
A24: x in A23;
A25: now
      assume
A26:  x in A2;
      thus H.x = f.x by A24,FUNCT_1:49
        .= f2.x by A23,A26,FUNCT_1:49
        .= (f23|A2).x by A4,A7,Def1
        .= f23.x by A26,FUNCT_1:49;
    end;
    now
      assume
A27:  x in A3;
      thus H.x = f.x by A24,FUNCT_1:49
        .= (f|A3).x by A27,FUNCT_1:49
        .= f3.x by A21,Def1
        .= (f23|A3).x by A4,A7,Def1
        .= f23.x by A27,FUNCT_1:49;
    end;
    hence H.x = f23.x by A2,A24,A25,XBOOLE_0:def 3;
  end;
  then
A28: f|A23 = f23 by FUNCT_2:12;
A29: A1 c= A12 by A1,XBOOLE_1:7;
  f12|A1 = f1 by A3,A6,Def1;
  then f|A1 = f1 by A22,A29,FUNCT_1:51;
  hence thesis by A28,Th2;
end;

theorem
  for f1 being Function of A1,B, f2 being Function of A2,B st f1|(A1 /\
  A2) = f2|(A1 /\ A2) holds (A1 is Subset of A2 iff f1 union f2 = f2) & (A2 is
  Subset of A1 iff f1 union f2 = f1)
proof
  let f1 be Function of A1,B, f2 be Function of A2,B such that
A1: f1|(A1 /\ A2) = f2|(A1 /\ A2);
A2: now
    assume A1 is Subset of A2;
    then A2 = A1 \/ A2 by XBOOLE_1:12;
    then (f1 union f2)|(A1 \/ A2) = f2 by A1,Def1;
    then (f1 union f2)*(id (A1 \/ A2)) = f2 by RELAT_1:65;
    hence f1 union f2 = f2 by FUNCT_2:17;
  end;
  now
A3: dom (f1 union f2) = A1 \/ A2 & dom f2 = A2 by FUNCT_2:def 1;
    assume f1 union f2 = f2;
    hence A1 is Subset of A2 by A3,XBOOLE_1:7;
  end;
  hence A1 is Subset of A2 iff f1 union f2 = f2 by A2;
A4: now
    assume A2 is Subset of A1;
    then A1 = A1 \/ A2 by XBOOLE_1:12;
    then (f1 union f2)|(A1 \/ A2) = f1 by A1,Def1;
    then (f1 union f2)*(id (A1 \/ A2)) = f1 by RELAT_1:65;
    hence f1 union f2 = f1 by FUNCT_2:17;
  end;
  now
A5: dom (f1 union f2) = A1 \/ A2 & dom f1 = A1 by FUNCT_2:def 1;
    assume f1 union f2 = f1;
    hence A2 is Subset of A1 by A5,XBOOLE_1:7;
  end;
  hence A2 is Subset of A1 iff f1 union f2 = f1 by A4;
end;

begin :: 2. Selected Properties of Subspaces of Topological Spaces.

reserve X for TopSpace;

theorem Th6:
  for X being TopStruct, X0 being SubSpace of X holds the
  TopStruct of X0 is strict SubSpace of X
proof
  let X be TopStruct, X0 be SubSpace of X;
  reconsider S = the TopStruct of X0 as TopStruct;
  S is SubSpace of X
  proof
A1: [#] (X0) = the carrier of X0;
    hence [#](S) c= [#](X) by PRE_TOPC:def 4;
    let P be Subset of S;
    thus P in the topology of S implies ex Q being Subset of X st Q in the
    topology of X & P = Q /\ [#](S) by A1,PRE_TOPC:def 4;
    given Q being Subset of X such that
A2: Q in the topology of X & P = Q /\ [#](S);
    thus thesis by A1,A2,PRE_TOPC:def 4;
  end;
  hence thesis;
end;

theorem Th7:
  for X being TopStruct for X1,X2 being TopSpace st X1 = the
  TopStruct of X2 holds X1 is SubSpace of X iff X2 is SubSpace of X
proof
  let X be TopStruct;
  let X1,X2 be TopSpace such that
A1: X1 = the TopStruct of X2;
  thus X1 is SubSpace of X implies X2 is SubSpace of X
  proof
A2: [#] (X1) = the carrier of X1;
    assume
A3: X1 is SubSpace of X;
    hence [#](X2) c= [#](X) by A1,A2,PRE_TOPC:def 4;
    let P be Subset of X2;
    thus P in the topology of X2 implies ex Q being Subset of X st Q in the
    topology of X & P = Q /\ [#](X2) by A1,A3,A2,PRE_TOPC:def 4;
    given Q being Subset of X such that
A4: Q in the topology of X & P = Q /\ [#](X2);
    thus thesis by A1,A3,A2,A4,PRE_TOPC:def 4;
  end;
  thus thesis by A1,Th6;
end;

theorem Th8:
  for X1,X2 being TopSpace st X2 = the TopStruct of X1 holds X1 is
  closed SubSpace of X iff X2 is closed SubSpace of X
proof
  let X1,X2 be TopSpace;
  assume
A1: X2 = the TopStruct of X1;
  thus X1 is closed SubSpace of X implies X2 is closed SubSpace of X
  proof
    assume
A2: X1 is closed SubSpace of X;
    then reconsider Y2 = X2 as SubSpace of X by A1,Th7;
    reconsider A2 = the carrier of Y2 as Subset of X by TSEP_1:1;
    A2 is closed by A1,A2,TSEP_1:11;
    hence thesis by TSEP_1:11;
  end;
  assume
A3: X2 is closed SubSpace of X;
  then reconsider Y1 = X1 as SubSpace of X by A1,Th7;
  reconsider A1 = the carrier of Y1 as Subset of X by TSEP_1:1;
  A1 is closed by A1,A3,TSEP_1:11;
  hence thesis by TSEP_1:11;
end;

theorem Th9:
  for X1,X2 being TopSpace st X2 = the TopStruct of X1 holds X1 is
  open SubSpace of X iff X2 is open SubSpace of X
proof
  let X1,X2 be TopSpace;
  assume
A1: X2 = the TopStruct of X1;
  thus X1 is open SubSpace of X implies X2 is open SubSpace of X
  proof
    assume
A2: X1 is open SubSpace of X;
    then reconsider Y2 = X2 as SubSpace of X by A1,Th7;
    reconsider A2 = the carrier of Y2 as Subset of X by TSEP_1:1;
    A2 is open by A1,A2,TSEP_1:16;
    hence thesis by TSEP_1:16;
  end;
  assume
A3: X2 is open SubSpace of X;
  then reconsider Y1 = X1 as SubSpace of X by A1,Th7;
  reconsider A1 = the carrier of Y1 as Subset of X by TSEP_1:1;
  A1 is open by A1,A3,TSEP_1:16;
  hence thesis by TSEP_1:16;
end;

reserve X for non empty TopSpace;
reserve X1, X2 for non empty SubSpace of X;

theorem Th10:
  X1 is SubSpace of X2 implies for x1 being Point of X1 ex x2
  being Point of X2 st x2 = x1
proof
  assume X1 is SubSpace of X2;
  then
A1: the carrier of X1 c= the carrier of X2 by TSEP_1:4;
  let x1 be Point of X1;
  x1 in the carrier of X1;
  then reconsider x2 = x1 as Point of X2 by A1;
  take x2;
  thus thesis;
end;

theorem Th11:
  for x being Point of X1 union X2 holds (ex x1 being Point of X1
  st x1 = x) or ex x2 being Point of X2 st x2 = x
proof
  let x be Point of X1 union X2;
  reconsider A0 = the carrier of X1 union X2 as Subset of X by TSEP_1:1;
  reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;
  reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;
  assume
A1: not ex x1 being Point of X1 st x1 = x;
  ex x2 being Point of X2 st x2 = x
  proof
    A0 = A1 \/ A2 & not x in A1 by A1,TSEP_1:def 2;
    then reconsider x2 = x as Point of X2 by XBOOLE_0:def 3;
    take x2;
    thus thesis;
  end;
  hence thesis;
end;

theorem Th12:
  X1 meets X2 implies for x being Point of X1 meet X2 holds (ex x1
  being Point of X1 st x1 = x) & ex x2 being Point of X2 st x2 = x
proof
  assume
A1: X1 meets X2;
  reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;
  reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;
  reconsider A0 = the carrier of X1 meet X2 as Subset of X by TSEP_1:1;
  let x be Point of X1 meet X2;
  A0 = A1 /\ A2 by A1,TSEP_1:def 4;
  then x in A1 & x in A2 by XBOOLE_0:def 4;
  hence thesis;
end;

theorem
  for x being Point of X1 union X2 for F1 being Subset of X1, F2 being
  Subset of X2 st F1 is closed & x in F1 & F2 is closed & x in F2 ex H being
  Subset of X1 union X2 st H is closed & x in H & H c= F1 \/ F2
proof
  let x be Point of X1 union X2;
  let F1 be Subset of X1, F2 be Subset of X2 such that
A1: F1 is closed and
A2: x in F1 and
A3: F2 is closed and
A4: x in F2;
A5: X1 is SubSpace of X1 union X2 by TSEP_1:22;
  then reconsider C1 = the carrier of X1 as Subset of X1 union X2 by TSEP_1:1;
  consider H1 being Subset of X1 union X2 such that
A6: H1 is closed and
A7: H1 /\ [#]X1 = F1 by A1,A5,PRE_TOPC:13;
A8: x in H1 by A2,A7,XBOOLE_0:def 4;
A9: X2 is SubSpace of X1 union X2 by TSEP_1:22;
  then reconsider C2 = the carrier of X2 as Subset of X1 union X2 by TSEP_1:1;
  consider H2 being Subset of X1 union X2 such that
A10: H2 is closed and
A11: H2 /\ [#]X2 = F2 by A3,A9,PRE_TOPC:13;
A12: x in H2 by A4,A11,XBOOLE_0:def 4;
  take H = H1 /\ H2;
A13: H /\ C1 c= H1 /\ C1 & H /\ C2 c= H2 /\ C2 by XBOOLE_1:17,26;
  the carrier of X1 union X2 = C1 \/ C2 by TSEP_1:def 2;
  then H = H /\ (C1 \/ C2) by XBOOLE_1:28
    .= (H /\ C1) \/ (H /\ C2) by XBOOLE_1:23;
  hence thesis by A6,A7,A10,A11,A13,A8,A12,XBOOLE_0:def 4,XBOOLE_1:13;
end;

theorem Th14:
  for x being Point of X1 union X2 for U1 being Subset of X1, U2
  being Subset of X2 st U1 is open & x in U1 & U2 is open & x in U2 ex V being
  Subset of X1 union X2 st V is open & x in V & V c= U1 \/ U2
proof
  let x be Point of X1 union X2;
  let U1 be Subset of X1, U2 be Subset of X2 such that
A1: U1 is open and
A2: x in U1 and
A3: U2 is open and
A4: x in U2;
A5: X1 is SubSpace of X1 union X2 by TSEP_1:22;
  then reconsider C1 = the carrier of X1 as Subset of X1 union X2 by TSEP_1:1;
  consider V1 being Subset of X1 union X2 such that
A6: V1 is open and
A7: V1 /\ [#]X1 = U1 by A1,A5,TOPS_2:24;
A8: x in V1 by A2,A7,XBOOLE_0:def 4;
A9: X2 is SubSpace of X1 union X2 by TSEP_1:22;
  then reconsider C2 = the carrier of X2 as Subset of X1 union X2 by TSEP_1:1;
  consider V2 being Subset of X1 union X2 such that
A10: V2 is open and
A11: V2 /\ [#]X2 = U2 by A3,A9,TOPS_2:24;
A12: x in V2 by A4,A11,XBOOLE_0:def 4;
  take V = V1 /\ V2;
A13: V /\ C1 c= V1 /\ C1 & V /\ C2 c= V2 /\ C2 by XBOOLE_1:17,26;
  the carrier of X1 union X2 = C1 \/ C2 by TSEP_1:def 2;
  then V = V /\ (C1 \/ C2) by XBOOLE_1:28
    .= (V /\ C1) \/ (V /\ C2) by XBOOLE_1:23;
  hence thesis by A6,A7,A10,A11,A13,A8,A12,XBOOLE_0:def 4,XBOOLE_1:13;
end;

theorem Th15:
  for x being Point of X1 union X2 for x1 being Point of X1, x2
  being Point of X2 st x1 = x & x2 = x for A1 being a_neighborhood of x1, A2
being a_neighborhood of x2 ex V being Subset of X1 union X2 st V is open & x in
  V & V c= A1 \/ A2
proof
  let x be Point of X1 union X2;
  let x1 be Point of X1, x2 be Point of X2 such that
A1: x1 = x & x2 = x;
  let A1 be a_neighborhood of x1, A2 be a_neighborhood of x2;
  consider U1 being Subset of X1 such that
A2: U1 is open and
A3: U1 c= A1 and
A4: x1 in U1 by CONNSP_2:6;
  consider U2 being Subset of X2 such that
A5: U2 is open and
A6: U2 c= A2 and
A7: x2 in U2 by CONNSP_2:6;
  consider V being Subset of X1 union X2 such that
A8: V is open & x in V & V c= U1 \/ U2 by A1,A2,A4,A5,A7,Th14;
  take V;
  U1 \/ U2 c= A1 \/ A2 by A3,A6,XBOOLE_1:13;
  hence thesis by A8,XBOOLE_1:1;
end;

theorem Th16:
  for x being Point of X1 union X2 for x1 being Point of X1, x2
  being Point of X2 st x1 = x & x2 = x for A1 being a_neighborhood of x1, A2
  being a_neighborhood of x2 ex A being a_neighborhood of x st A c= A1 \/ A2
proof
  let x be Point of X1 union X2;
  let x1 be Point of X1, x2 be Point of X2 such that
A1: x1 = x & x2 = x;
  let A1 be a_neighborhood of x1, A2 be a_neighborhood of x2;
  consider V being Subset of X1 union X2 such that
A2: V is open & x in V and
A3: V c= A1 \/ A2 by A1,Th15;
  reconsider W = V as a_neighborhood of x by A2,CONNSP_2:3;
  take W;
  thus thesis by A3;
end;

reserve X0, X1, X2, Y1, Y2 for non empty SubSpace of X;

theorem Th17:
  X0 is SubSpace of X1 implies X0 meets X1 & X1 meets X0
proof
  assume X0 is SubSpace of X1;
  then the carrier of X0 c= the carrier of X1 by TSEP_1:4;
  then the carrier of X0 = (the carrier of X0) /\ (the carrier of X1) by
XBOOLE_1:28;
  then
A1: (the carrier of X0) meets (the carrier of X1) by XBOOLE_0:def 7;
  hence X0 meets X1 by TSEP_1:def 3;
  thus thesis by A1,TSEP_1:def 3;
end;

theorem Th18:
  X0 is SubSpace of X1 & (X0 meets X2 or X2 meets X0) implies X1
  meets X2 & X2 meets X1
proof
  reconsider A0 = the carrier of X0, A1 = the carrier of X1, A2 = the carrier
  of X2 as Subset of X by TSEP_1:1;
  assume X0 is SubSpace of X1;
  then
A1: A0 c= A1 by TSEP_1:4;
A2: now
    assume X0 meets X2;
    then A2 meets A0 by TSEP_1:def 3;
    then A2 meets A1 by A1,XBOOLE_1:63;
    hence thesis by TSEP_1:def 3;
  end;
  assume X0 meets X2 or X2 meets X0;
  hence thesis by A2;
end;

theorem Th19:
  X0 is SubSpace of X1 & (X1 misses X2 or X2 misses X1) implies X0
  misses X2 & X2 misses X0
proof
  reconsider A0 = the carrier of X0, A1 = the carrier of X1, A2 = the carrier
  of X2 as Subset of X by TSEP_1:1;
  assume X0 is SubSpace of X1;
  then
A1: A0 c= A1 by TSEP_1:4;
A2: now
    assume X1 misses X2;
    then A2 misses A1 by TSEP_1:def 3;
    then A2 misses A0 by A1,XBOOLE_1:63;
    hence thesis by TSEP_1:def 3;
  end;
  assume X1 misses X2 or X2 misses X1;
  hence thesis by A2;
end;

theorem
  X0 union X0 = the TopStruct of X0
proof
  X0 is SubSpace of X0 by TSEP_1:2;
  hence thesis by TSEP_1:23;
end;

theorem
  X0 meet X0 = the TopStruct of X0
proof
A1: X0 is SubSpace of X0 by TSEP_1:2;
  then X0 meets X0 by Th17;
  hence thesis by A1,TSEP_1:28;
end;

theorem Th22:
  Y1 is SubSpace of X1 & Y2 is SubSpace of X2 implies Y1 union Y2
  is SubSpace of X1 union X2
proof
  assume Y1 is SubSpace of X1 & Y2 is SubSpace of X2;
  then the carrier of Y1 c= the carrier of X1 & the carrier of Y2 c= the
  carrier of X2 by TSEP_1:4;
  then (the carrier of Y1) \/ (the carrier of Y2) c= (the carrier of X1) \/ (
  the carrier of X2) by XBOOLE_1:13;
  then the carrier of (Y1 union Y2) c= (the carrier of X1) \/ (the carrier of
  X2) by TSEP_1:def 2;
  then the carrier of (Y1 union Y2) c= the carrier of (X1 union X2) by
TSEP_1:def 2;
  hence thesis by TSEP_1:4;
end;

theorem
  Y1 meets Y2 & Y1 is SubSpace of X1 & Y2 is SubSpace of X2 implies Y1
  meet Y2 is SubSpace of X1 meet X2
proof
  assume
A1: Y1 meets Y2;
  assume Y1 is SubSpace of X1 & Y2 is SubSpace of X2;
  then
A2: the carrier of Y1 c= the carrier of X1 & the carrier of Y2 c= the
  carrier of X2 by TSEP_1:4;
  (the carrier of Y1) meets (the carrier of Y2) by A1,TSEP_1:def 3;
  then (the carrier of Y1) /\ (the carrier of Y2) <> {} by XBOOLE_0:def 7;
  then (the carrier of X1) /\ (the carrier of X2) <> {} by A2,XBOOLE_1:3,27;
  then (the carrier of X1) meets (the carrier of X2) by XBOOLE_0:def 7;
  then
A3: X1 meets X2 by TSEP_1:def 3;
  (the carrier of Y1) /\ (the carrier of Y2) c= (the carrier of X1) /\ (
  the carrier of X2) by A2,XBOOLE_1:27;
  then (the carrier of Y1) /\ (the carrier of Y2) c= the carrier of (X1 meet
  X2) by A3,TSEP_1:def 4;
  then the carrier of (Y1 meet Y2) c= the carrier of (X1 meet X2) by A1,
TSEP_1:def 4;
  hence thesis by TSEP_1:4;
end;

theorem Th24:
  X1 is SubSpace of X0 & X2 is SubSpace of X0 implies X1 union X2
  is SubSpace of X0
proof
  assume X1 is SubSpace of X0 & X2 is SubSpace of X0;
  then the carrier of X1 c= the carrier of X0 & the carrier of X2 c= the
  carrier of X0 by TSEP_1:4;
  then (the carrier of X1) \/ (the carrier of X2) c= the carrier of X0 by
XBOOLE_1:8;
  then the carrier of (X1 union X2) c= the carrier of X0 by TSEP_1:def 2;
  hence thesis by TSEP_1:4;
end;

theorem
  X1 meets X2 & X1 is SubSpace of X0 & X2 is SubSpace of X0 implies X1
  meet X2 is SubSpace of X0
proof
  assume
A1: X1 meets X2;
  assume X1 is SubSpace of X0 & X2 is SubSpace of X0;
  then the carrier of X1 c= the carrier of X0 & the carrier of X2 c= the
  carrier of X0 by TSEP_1:4;
  then
A2: (the carrier of X1) \/ (the carrier of X2) c= the carrier of X0 by
XBOOLE_1:8;
  (the carrier of X1) /\ (the carrier of X2) c= (the carrier of X1) \/ (
  the carrier of X2) by XBOOLE_1:29;
  then (the carrier of X1) /\ (the carrier of X2) c= the carrier of X0 by A2,
XBOOLE_1:1;
  then the carrier of (X1 meet X2) c= the carrier of X0 by A1,TSEP_1:def 4;
  hence thesis by TSEP_1:4;
end;

theorem Th26:
  ((X1 misses X0 or X0 misses X1) & (X2 meets X0 or X0 meets X2)
implies (X1 union X2) meet X0 = X2 meet X0 & X0 meet (X1 union X2) = X0 meet X2
) & ((X1 meets X0 or X0 meets X1) & (X2 misses X0 or X0 misses X2) implies (X1
  union X2) meet X0 = X1 meet X0 & X0 meet (X1 union X2) = X0 meet X1)
proof
  reconsider A0 = the carrier of X0, A1 = the carrier of X1, A2 = the carrier
  of X2 as Subset of X by TSEP_1:1;
  thus (X1 misses X0 or X0 misses X1) & (X2 meets X0 or X0 meets X2) implies (
  X1 union X2) meet X0 = X2 meet X0 & X0 meet (X1 union X2) = X0 meet X2
  proof
    assume that
A1: X1 misses X0 or X0 misses X1 and
A2: X2 meets X0 or X0 meets X2;
A3: A1 misses A0 by A1,TSEP_1:def 3;
    X2 is SubSpace of X1 union X2 by TSEP_1:22;
    then
A4: (X1 union X2) meets X0 by A2,Th18;
    then
A5: the carrier of X0 meet (X1 union X2) = A0 /\ (the carrier of (X1 union
    X2)) by TSEP_1:def 4
      .= A0 /\ (A1 \/ A2) by TSEP_1:def 2
      .= (A0 /\ A1) \/ (A0 /\ A2) by XBOOLE_1:23
      .= {} \/ (A0 /\ A2) by A3,XBOOLE_0:def 7
      .= the carrier of (X0 meet X2) by A2,TSEP_1:def 4;
    the carrier of (X1 union X2) meet X0 = (the carrier of (X1 union X2))
    /\ A0 by A4,TSEP_1:def 4
      .= (A1 \/ A2) /\ A0 by TSEP_1:def 2
      .= (A1 /\ A0) \/ (A2 /\ A0) by XBOOLE_1:23
      .= {} \/ (A2 /\ A0) by A3,XBOOLE_0:def 7
      .= the carrier of (X2 meet X0) by A2,TSEP_1:def 4;
    hence thesis by A5,TSEP_1:5;
  end;
  thus (X1 meets X0 or X0 meets X1) & (X2 misses X0 or X0 misses X2) implies (
  X1 union X2) meet X0 = X1 meet X0 & X0 meet (X1 union X2) = X0 meet X1
  proof
    assume that
A6: X1 meets X0 or X0 meets X1 and
A7: X2 misses X0 or X0 misses X2;
A8: A2 misses A0 by A7,TSEP_1:def 3;
    X1 is SubSpace of X1 union X2 by TSEP_1:22;
    then
A9: (X1 union X2) meets X0 by A6,Th18;
    then
A10: the carrier of X0 meet (X1 union X2) = A0 /\ (the carrier of (X1
    union X2)) by TSEP_1:def 4
      .= A0 /\ (A1 \/ A2) by TSEP_1:def 2
      .= (A0 /\ A1) \/ (A0 /\ A2) by XBOOLE_1:23
      .= (A0 /\ A1) \/ {} by A8,XBOOLE_0:def 7
      .= the carrier of (X0 meet X1) by A6,TSEP_1:def 4;
    the carrier of (X1 union X2) meet X0 = (the carrier of (X1 union X2))
    /\ A0 by A9,TSEP_1:def 4
      .= (A1 \/ A2) /\ A0 by TSEP_1:def 2
      .= (A1 /\ A0) \/ (A2 /\ A0) by XBOOLE_1:23
      .= (A1 /\ A0) \/ {} by A8,XBOOLE_0:def 7
      .= the carrier of (X1 meet X0) by A6,TSEP_1:def 4;
    hence thesis by A10,TSEP_1:5;
  end;
end;

theorem Th27:
  X1 meets X2 implies (X1 is SubSpace of X0 implies X1 meet X2 is
SubSpace of X0 meet X2) & (X2 is SubSpace of X0 implies X1 meet X2 is SubSpace
  of X1 meet X0)
proof
  reconsider A0 = the carrier of X0, A1 = the carrier of X1, A2 = the carrier
  of X2 as Subset of X by TSEP_1:1;
  assume
A1: X1 meets X2;
  then
A2: the carrier of X1 meet X2 = A1 /\ A2 by TSEP_1:def 4;
A3: now
    assume
A4: X2 is SubSpace of X0;
    then A2 c= A0 by TSEP_1:4;
    then
A5: A1 /\ A2 c= A1 /\ A0 by XBOOLE_1:26;
    X1 meets X0 by A1,A4,Th18;
    then the carrier of X1 meet X0 = A1 /\ A0 by TSEP_1:def 4;
    hence X1 meet X2 is SubSpace of X1 meet X0 by A2,A5,TSEP_1:4;
  end;
  now
    assume
A6: X1 is SubSpace of X0;
    then A1 c= A0 by TSEP_1:4;
    then
A7: A1 /\ A2 c= A0 /\ A2 by XBOOLE_1:26;
    X0 meets X2 by A1,A6,Th18;
    then the carrier of X0 meet X2 = A0 /\ A2 by TSEP_1:def 4;
    hence X1 meet X2 is SubSpace of X0 meet X2 by A2,A7,TSEP_1:4;
  end;
  hence thesis by A3;
end;

theorem Th28:
  X1 is SubSpace of X0 & (X0 misses X2 or X2 misses X0) implies X0
  meet (X1 union X2) = the TopStruct of X1 & X0 meet (X2 union X1) = the
  TopStruct of X1
proof
  reconsider A0 = the carrier of X0, A1 = the carrier of X1, A2 = the carrier
  of X2 as Subset of X by TSEP_1:1;
A1: X1 is SubSpace of X1 union X2 by TSEP_1:22;
  assume
A2: X1 is SubSpace of X0;
  then
A3: A1 c= A0 by TSEP_1:4;
  assume X0 misses X2 or X2 misses X0;
  then
A4: A0 misses A2 by TSEP_1:def 3;
  X0 meets X1 by A2,Th17;
  then X0 meets X1 union X2 by A1,Th18;
  then
A5: the carrier of X0 meet (X1 union X2) = A0 /\ the carrier of X1 union X2
  by TSEP_1:def 4
    .= A0 /\ (A1 \/ A2) by TSEP_1:def 2
    .= (A0 /\ A1) \/ (A0 /\ A2) by XBOOLE_1:23
    .= (A0 /\ A1) \/ {} by A4,XBOOLE_0:def 7
    .= A1 by A3,XBOOLE_1:28;
  hence X0 meet (X1 union X2) = the TopStruct of X1 by TSEP_1:5;
  thus thesis by A5,TSEP_1:5;
end;

theorem Th29:
  X1 meets X2 implies (X1 is SubSpace of X0 implies (X0 meet X2)
meets X1 & (X2 meet X0) meets X1) & (X2 is SubSpace of X0 implies (X1 meet X0)
  meets X2 & (X0 meet X1) meets X2)
proof
  assume
A1: X1 meets X2;
A2: now
    X1 meet X2 is SubSpace of X2 by A1,TSEP_1:27;
    then
A3: (X1 meet X2) meets X2 by Th17;
    assume
A4: X2 is SubSpace of X0;
    then X1 meet X2 is SubSpace of X1 meet X0 by A1,Th27;
    hence
A5: (X1 meet X0) meets X2 by A3,Th18;
    X1 meets X0 by A1,A4,Th18;
    hence (X0 meet X1) meets X2 by A5,TSEP_1:26;
  end;
  now
    X1 meet X2 is SubSpace of X1 by A1,TSEP_1:27;
    then
A6: (X1 meet X2) meets X1 by Th17;
    assume
A7: X1 is SubSpace of X0;
    then X1 meet X2 is SubSpace of X0 meet X2 by A1,Th27;
    hence
A8: (X0 meet X2) meets X1 by A6,Th18;
    X0 meets X2 by A1,A7,Th18;
    hence (X2 meet X0) meets X1 by A8,TSEP_1:26;
  end;
  hence thesis by A2;
end;

theorem Th30:
  X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & (Y1 misses Y2 or
  Y1 meet Y2 misses X1 union X2) implies Y1 misses X2 & Y2 misses X1
proof
  assume that
A1: X1 is SubSpace of Y1 and
A2: X2 is SubSpace of Y2;
  assume
A3: Y1 misses Y2 or Y1 meet Y2 misses X1 union X2;
  now
    assume
A4: not Y1 misses Y2;
A5: now
      assume Y2 meets X1;
      then
A6:   (Y1 meet Y2) meets X1 by A1,Th29;
      X1 is SubSpace of X1 union X2 by TSEP_1:22;
      hence contradiction by A3,A4,A6,Th18;
    end;
    now
      assume Y1 meets X2;
      then
A7:   (Y1 meet Y2) meets X2 by A2,Th29;
      X2 is SubSpace of X1 union X2 by TSEP_1:22;
      hence contradiction by A3,A4,A7,Th18;
    end;
    hence thesis by A5;
  end;
  hence thesis by A1,A2,Th19;
end;

theorem Th31:
  X1 is not SubSpace of X2 & X2 is not SubSpace of X1 & X1 union
  X2 is SubSpace of Y1 union Y2 & Y1 meet (X1 union X2) is SubSpace of X1 & Y2
meet (X1 union X2) is SubSpace of X2 implies Y1 meets X1 union X2 & Y2 meets X1
  union X2
proof
  assume that
A1: X1 is not SubSpace of X2 and
A2: X2 is not SubSpace of X1;
  reconsider A1 = the carrier of X1, A2 = the carrier of X2, C1 = the carrier
  of Y1, C2 = the carrier of Y2 as Subset of X by TSEP_1:1;
  assume
A3: X1 union X2 is SubSpace of Y1 union Y2;
  assume that
A4: Y1 meet (X1 union X2) is SubSpace of X1 and
A5: Y2 meet (X1 union X2) is SubSpace of X2;
A6: the carrier of X1 union X2 = A1 \/ A2 by TSEP_1:def 2;
A7: the carrier of Y1 union Y2 = C1 \/ C2 by TSEP_1:def 2;
A8: now
    assume Y2 misses (X1 union X2);
    then
A9: C2 misses (A1 \/ A2) by A6,TSEP_1:def 3;
    A1 \/ A2 c= C1 \/ C2 by A3,A6,A7,TSEP_1:4;
    then
A10: A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by XBOOLE_1:28
      .= (C1 /\ (A1 \/ A2)) \/ (C2 /\ (A1 \/ A2)) by XBOOLE_1:23
      .= (C1 /\ (A1 \/ A2)) \/ {} by A9,XBOOLE_0:def 7
      .= C1 /\ (A1 \/ A2);
    then C1 meets (A1 \/ A2) by XBOOLE_0:def 7;
    then Y1 meets (X1 union X2) by A6,TSEP_1:def 3;
    then the carrier of Y1 meet (X1 union X2) = C1 /\ (A1 \/ A2) by A6,
TSEP_1:def 4;
    then
A11: A1 \/ A2 c= A1 by A4,A10,TSEP_1:4;
    A2 c= A1 \/ A2 by XBOOLE_1:7;
    then A2 c= A1 by A11,XBOOLE_1:1;
    hence contradiction by A2,TSEP_1:4;
  end;
  now
    assume Y1 misses (X1 union X2);
    then
A12: C1 misses (A1 \/ A2) by A6,TSEP_1:def 3;
    A1 \/ A2 c= C1 \/ C2 by A3,A6,A7,TSEP_1:4;
    then
A13: A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by XBOOLE_1:28
      .= (C1 /\ (A1 \/ A2)) \/ (C2 /\ (A1 \/ A2)) by XBOOLE_1:23
      .= {} \/ (C2 /\ (A1 \/ A2)) by A12,XBOOLE_0:def 7
      .= C2 /\ (A1 \/ A2);
    then C2 meets (A1 \/ A2) by XBOOLE_0:def 7;
    then Y2 meets (X1 union X2) by A6,TSEP_1:def 3;
    then the carrier of Y2 meet (X1 union X2) = C2 /\ (A1 \/ A2) by A6,
TSEP_1:def 4;
    then
A14: A1 \/ A2 c= A2 by A5,A13,TSEP_1:4;
    A1 c= A1 \/ A2 by XBOOLE_1:7;
    then A1 c= A2 by A14,XBOOLE_1:1;
    hence contradiction by A1,TSEP_1:4;
  end;
  hence thesis by A8;
end;

theorem Th32:
  X1 meets X2 & X1 is not SubSpace of X2 & X2 is not SubSpace of
  X1 & the TopStruct of X = (Y1 union Y2) union X0 & Y1 meet (X1 union X2) is
SubSpace of X1 & Y2 meet (X1 union X2) is SubSpace of X2 & X0 meet (X1 union X2
) is SubSpace of X1 meet X2 implies Y1 meets X1 union X2 & Y2 meets X1 union X2
proof
  assume
A1: X1 meets X2;
  reconsider C = the carrier of X0 as Subset of X by TSEP_1:1;
  reconsider C2 = the carrier of Y2 as Subset of X by TSEP_1:1;
  reconsider C1 = the carrier of Y1 as Subset of X by TSEP_1:1;
  reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;
  reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;
  assume that
A2: X1 is not SubSpace of X2 and
A3: X2 is not SubSpace of X1;
  assume
A4: the TopStruct of X = (Y1 union Y2) union X0;
  assume that
A5: Y1 meet (X1 union X2) is SubSpace of X1 and
A6: Y2 meet (X1 union X2) is SubSpace of X2;
  assume
A7: X0 meet (X1 union X2) is SubSpace of X1 meet X2;
A8: the carrier of X1 union X2 = A1 \/ A2 by TSEP_1:def 2;
A9: the carrier of Y1 union Y2 = C1 \/ C2 by TSEP_1:def 2;
A10: now
    assume Y2 misses (X1 union X2);
    then
A11: C2 misses (A1 \/ A2) by A8,TSEP_1:def 3;
    the carrier of X = (C1 \/ C2) \/ C by A4,A9,TSEP_1:def 2;
    then
A12: A1 \/ A2 = ((C2 \/ C1) \/ C) /\ (A1 \/ A2) by XBOOLE_1:28
      .= (C2 \/ (C1 \/ C)) /\ (A1 \/ A2) by XBOOLE_1:4
      .= (C2 /\ (A1 \/ A2)) \/ ((C1 \/ C) /\ (A1 \/ A2)) by XBOOLE_1:23
      .= {} \/ ((C1 \/ C) /\ (A1 \/ A2)) by A11,XBOOLE_0:def 7
      .= (C1 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23;
A13: now
      assume C1 /\ (A1 \/ A2) <> {};
      then C1 meets (A1 \/ A2) by XBOOLE_0:def 7;
      then Y1 meets (X1 union X2) by A8,TSEP_1:def 3;
      then
A14:  the carrier of Y1 meet (X1 union X2) = C1 /\ (A1 \/ A2) by A8,
TSEP_1:def 4;
      then
A15:  C1 /\ (A1 \/ A2) c= A1 by A5,TSEP_1:4;
      now
        per cases;
        suppose
          C /\ (A1 \/ A2) = {};
          hence A1 \/ A2 c= A1 by A5,A12,A14,TSEP_1:4;
        end;
        suppose
          C /\ (A1 \/ A2) <> {};
          then C meets (A1 \/ A2) by XBOOLE_0:def 7;
          then X0 meets (X1 union X2) by A8,TSEP_1:def 3;
          then
A16:      the carrier of X0 meet (X1 union X2) = C /\ (A1 \/ A2) by A8,
TSEP_1:def 4;
          the carrier of X1 meet X2 = A1 /\ A2 by A1,TSEP_1:def 4;
          then C /\ (A1 \/ A2) c= A1 /\ A2 by A7,A16,TSEP_1:4;
          then A1 \/ A2 c= A1 \/ A1 /\ A2 by A12,A15,XBOOLE_1:13;
          hence A1 \/ A2 c= A1 by XBOOLE_1:12,17;
        end;
      end;
      hence A1 \/ A2 c= A1;
    end;
A17: now
      assume C /\ (A1 \/ A2) <> {};
      then C meets (A1 \/ A2) by XBOOLE_0:def 7;
      then X0 meets (X1 union X2) by A8,TSEP_1:def 3;
      then
A18:  the carrier of X0 meet (X1 union X2) = C /\ (A1 \/ A2) by A8,TSEP_1:def 4
;
      the carrier of X1 meet X2 = A1 /\ A2 by A1,TSEP_1:def 4;
      then
A19:  C /\ (A1 \/ A2) c= A1 /\ A2 by A7,A18,TSEP_1:4;
A20:  A1 /\ A2 c= A1 by XBOOLE_1:17;
      then
A21:  C /\ (A1 \/ A2) c= A1 by A19,XBOOLE_1:1;
      now
        per cases;
        suppose
          C1 /\ (A1 \/ A2) = {};
          hence A1 \/ A2 c= A1 by A12,A19,A20,XBOOLE_1:1;
        end;
        suppose
          C1 /\ (A1 \/ A2) <> {};
          then C1 meets (A1 \/ A2) by XBOOLE_0:def 7;
          then Y1 meets (X1 union X2) by A8,TSEP_1:def 3;
          then the carrier of Y1 meet (X1 union X2) = C1 /\ (A1 \/ A2) by A8,
TSEP_1:def 4;
          then C1 /\ (A1 \/ A2) c= A1 by A5,TSEP_1:4;
          hence A1 \/ A2 c= A1 by A12,A21,XBOOLE_1:8;
        end;
      end;
      hence A1 \/ A2 c= A1;
    end;
    A2 c= A1 \/ A2 by XBOOLE_1:7;
    then A2 c= A1 by A12,A13,A17,XBOOLE_1:1;
    hence contradiction by A3,TSEP_1:4;
  end;
  now
    assume Y1 misses (X1 union X2);
    then
A22: C1 misses (A1 \/ A2) by A8,TSEP_1:def 3;
    the carrier of X = (C1 \/ C2) \/ C by A4,A9,TSEP_1:def 2;
    then
A23: A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by XBOOLE_1:28
      .= (C1 \/ (C2 \/ C)) /\ (A1 \/ A2) by XBOOLE_1:4
      .= (C1 /\ (A1 \/ A2)) \/ ((C2 \/ C) /\ (A1 \/ A2)) by XBOOLE_1:23
      .= {} \/ ((C2 \/ C) /\ (A1 \/ A2)) by A22,XBOOLE_0:def 7
      .= (C2 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23;
A24: now
      assume C2 /\ (A1 \/ A2) <> {};
      then C2 meets (A1 \/ A2) by XBOOLE_0:def 7;
      then Y2 meets (X1 union X2) by A8,TSEP_1:def 3;
      then
A25:  the carrier of Y2 meet (X1 union X2) = C2 /\ (A1 \/ A2) by A8,
TSEP_1:def 4;
      then
A26:  C2 /\ (A1 \/ A2) c= A2 by A6,TSEP_1:4;
      now
        per cases;
        suppose
          C /\ (A1 \/ A2) = {};
          hence A1 \/ A2 c= A2 by A6,A23,A25,TSEP_1:4;
        end;
        suppose
          C /\ (A1 \/ A2) <> {};
          then C meets (A1 \/ A2) by XBOOLE_0:def 7;
          then X0 meets (X1 union X2) by A8,TSEP_1:def 3;
          then
A27:      the carrier of X0 meet (X1 union X2) = C /\ (A1 \/ A2) by A8,
TSEP_1:def 4;
          the carrier of X1 meet X2 = A1 /\ A2 by A1,TSEP_1:def 4;
          then C /\ (A1 \/ A2) c= A1 /\ A2 by A7,A27,TSEP_1:4;
          then A1 \/ A2 c= A2 \/ A1 /\ A2 by A23,A26,XBOOLE_1:13;
          hence A1 \/ A2 c= A2 by XBOOLE_1:12,17;
        end;
      end;
      hence A1 \/ A2 c= A2;
    end;
A28: now
      assume C /\ (A1 \/ A2) <> {};
      then C meets (A1 \/ A2) by XBOOLE_0:def 7;
      then X0 meets (X1 union X2) by A8,TSEP_1:def 3;
      then
A29:  the carrier of X0 meet (X1 union X2) = C /\ (A1 \/ A2) by A8,TSEP_1:def 4
;
      the carrier of X1 meet X2 = A1 /\ A2 by A1,TSEP_1:def 4;
      then
A30:  C /\ (A1 \/ A2) c= A1 /\ A2 by A7,A29,TSEP_1:4;
A31:  A1 /\ A2 c= A2 by XBOOLE_1:17;
      then
A32:  C /\ (A1 \/ A2) c= A2 by A30,XBOOLE_1:1;
      now
        per cases;
        suppose
          C2 /\ (A1 \/ A2) = {};
          hence A1 \/ A2 c= A2 by A23,A30,A31,XBOOLE_1:1;
        end;
        suppose
          C2 /\ (A1 \/ A2) <> {};
          then C2 meets (A1 \/ A2) by XBOOLE_0:def 7;
          then Y2 meets (X1 union X2) by A8,TSEP_1:def 3;
          then the carrier of Y2 meet (X1 union X2) = C2 /\ (A1 \/ A2) by A8,
TSEP_1:def 4;
          then C2 /\ (A1 \/ A2) c= A2 by A6,TSEP_1:4;
          hence A1 \/ A2 c= A2 by A23,A32,XBOOLE_1:8;
        end;
      end;
      hence A1 \/ A2 c= A2;
    end;
    A1 c= A1 \/ A2 by XBOOLE_1:7;
    then A1 c= A2 by A23,A24,A28,XBOOLE_1:1;
    hence contradiction by A2,TSEP_1:4;
  end;
  hence thesis by A10;
end;

theorem Th33:
  X1 meets X2 & X1 is not SubSpace of X2 & X2 is not SubSpace of
  X1 & not X1 union X2 is SubSpace of Y1 union Y2 & the TopStruct of X = (Y1
  union Y2) union X0 & Y1 meet (X1 union X2) is SubSpace of X1 & Y2 meet (X1
  union X2) is SubSpace of X2 & X0 meet (X1 union X2) is SubSpace of X1 meet X2
  implies Y1 union Y2 meets X1 union X2 & X0 meets X1 union X2
proof
  assume
A1: X1 meets X2;
  assume
A2: X1 is not SubSpace of X2 & X2 is not SubSpace of X1;
  reconsider C = the carrier of X0 as Subset of X by TSEP_1:1;
  reconsider C2 = the carrier of Y2 as Subset of X by TSEP_1:1;
  reconsider C1 = the carrier of Y1 as Subset of X by TSEP_1:1;
  reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;
  reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;
A3: the carrier of Y1 union Y2 = C1 \/ C2 by TSEP_1:def 2;
A4: Y1 is SubSpace of Y1 union Y2 by TSEP_1:22;
  assume
A5: not X1 union X2 is SubSpace of Y1 union Y2;
  assume
A6: the TopStruct of X = (Y1 union Y2) union X0;
  assume
A7: Y1 meet (X1 union X2) is SubSpace of X1 & Y2 meet (X1 union X2) is
  SubSpace of X2;
  assume X0 meet (X1 union X2) is SubSpace of X1 meet X2;
  then Y1 meets X1 union X2 by A1,A2,A6,A7,Th32;
  hence Y1 union Y2 meets X1 union X2 by A4,Th18;
A8: the carrier of X1 union X2 = A1 \/ A2 by TSEP_1:def 2;
  then
A9: not A1 \/ A2 c= C1 \/ C2 by A5,A3,TSEP_1:4;
  now
    assume X0 misses (X1 union X2);
    then
A10: C misses (A1 \/ A2) by A8,TSEP_1:def 3;
    the carrier of X = (C1 \/ C2) \/ C by A6,A3,TSEP_1:def 2;
    then A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by XBOOLE_1:28
      .= ((C1 \/ C2) /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23
      .= ((C1 \/ C2) /\ (A1 \/ A2)) \/ {} by A10,XBOOLE_0:def 7
      .= (C1 \/ C2) /\ (A1 \/ A2);
    hence contradiction by A9,XBOOLE_1:17;
  end;
  hence thesis;
end;

theorem Th34:
  ((X1 union X2) meets X0 iff X1 meets X0 or X2 meets X0) & (X0
  meets (X1 union X2) iff X0 meets X1 or X0 meets X2)
proof
  reconsider A0 = the carrier of X0 as Subset of X by TSEP_1:1;
  reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;
  reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;
A1: X1 meets X0 or X2 meets X0 implies (X1 union X2) meets X0
  proof
    assume X1 meets X0 or X2 meets X0;
    then A1 meets A0 or A2 meets A0 by TSEP_1:def 3;
    then A1 /\ A0 <> {} or A2 /\ A0 <> {} by XBOOLE_0:def 7;
    then (A1 /\ A0) \/ (A2 /\ A0) <> {};
    then (A1 \/ A2) /\ A0 <> {} by XBOOLE_1:23;
    then (the carrier of (X1 union X2)) /\ A0 <> {} by TSEP_1:def 2;
    then (the carrier of (X1 union X2)) meets A0 by XBOOLE_0:def 7;
    hence thesis by TSEP_1:def 3;
  end;
A2: (X1 union X2) meets X0 implies X1 meets X0 or X2 meets X0
  proof
    assume (X1 union X2) meets X0;
    then (the carrier of (X1 union X2)) meets A0 by TSEP_1:def 3;
    then (the carrier of (X1 union X2)) /\ A0 <> {} by XBOOLE_0:def 7;
    then (A1 \/ A2) /\ A0 <> {} by TSEP_1:def 2;
    then (A1 /\ A0) \/ (A2 /\ A0) <> {} by XBOOLE_1:23;
    then A1 /\ A0 <> {} or A2 /\ A0 <> {};
    then A1 meets A0 or A2 meets A0 by XBOOLE_0:def 7;
    hence thesis by TSEP_1:def 3;
  end;
  hence (X1 union X2) meets X0 iff X1 meets X0 or X2 meets X0 by A1;
  thus thesis by A2,A1;
end;

theorem
  ((X1 union X2) misses X0 iff X1 misses X0 & X2 misses X0) & (X0 misses
  (X1 union X2) iff X0 misses X1 & X0 misses X2)
proof
  reconsider A0 = the carrier of X0 as Subset of X by TSEP_1:1;
  reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;
  reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;
A1: (X1 union X2) misses X0 implies X1 misses X0 & X2 misses X0
  proof
    assume (X1 union X2) misses X0;
    then (the carrier of (X1 union X2)) misses A0 by TSEP_1:def 3;
    then (the carrier of (X1 union X2)) /\ A0 = {} by XBOOLE_0:def 7;
    then (A1 \/ A2) /\ A0 = {} by TSEP_1:def 2;
    then
A2: (A1 /\ A0) \/ (A2 /\ A0) = {} by XBOOLE_1:23;
    then A2 /\ A0 = {};
    then
A3: A2 misses A0 by XBOOLE_0:def 7;
    A1 /\ A0 = {} by A2;
    then A1 misses A0 by XBOOLE_0:def 7;
    hence thesis by A3,TSEP_1:def 3;
  end;
A4: X1 misses X0 & X2 misses X0 implies (X1 union X2) misses X0
  proof
    assume that
A5: X1 misses X0 and
A6: X2 misses X0;
    A1 misses A0 by A5,TSEP_1:def 3;
    then
A7: A1 /\ A0 = {} by XBOOLE_0:def 7;
    A2 misses A0 by A6,TSEP_1:def 3;
    then (A1 /\ A0) \/ (A2 /\ A0) = {} by A7,XBOOLE_0:def 7;
    then (A1 \/ A2) /\ A0 = {} by XBOOLE_1:23;
    then (the carrier of (X1 union X2)) /\ A0 = {} by TSEP_1:def 2;
    then (the carrier of (X1 union X2)) misses A0 by XBOOLE_0:def 7;
    hence thesis by TSEP_1:def 3;
  end;
  hence (X1 union X2) misses X0 iff X1 misses X0 & X2 misses X0 by A1;
  thus thesis by A1,A4;
end;

theorem
  X1 meets X2 implies ((X1 meet X2) meets X0 implies X1 meets X0 & X2
  meets X0) & (X0 meets (X1 meet X2) implies X0 meets X1 & X0 meets X2)
proof
  reconsider A0 = the carrier of X0 as Subset of X by TSEP_1:1;
  reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;
  reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;
  assume
A1: X1 meets X2;
  thus (X1 meet X2) meets X0 implies X1 meets X0 & X2 meets X0
  proof
    assume (X1 meet X2) meets X0;
    then (the carrier of (X1 meet X2)) meets A0 by TSEP_1:def 3;
    then (the carrier of (X1 meet X2)) /\ A0 <> {} by XBOOLE_0:def 7;
    then (A1 /\ A2) /\ A0 <> {} by A1,TSEP_1:def 4;
    then
A2: A1 /\ (A2 /\ (A0 /\ A0)) <> {} by XBOOLE_1:16;
    then A1 /\ (A0 /\ (A2 /\ A0)) <> {} by XBOOLE_1:16;
    then (A1 /\ A0) /\ (A2 /\ A0) <> {} by XBOOLE_1:16;
    then A1 /\ A0 <> {};
    then
A3: A1 meets A0 by XBOOLE_0:def 7;
    A2 /\ A0 <> {} by A2;
    then A2 meets A0 by XBOOLE_0:def 7;
    hence thesis by A3,TSEP_1:def 3;
  end;
  hence thesis;
end;

theorem
  X1 meets X2 implies (X1 misses X0 or X2 misses X0 implies (X1 meet X2)
  misses X0) & (X0 misses X1 or X0 misses X2 implies X0 misses (X1 meet X2))
proof
  reconsider A0 = the carrier of X0 as Subset of X by TSEP_1:1;
  reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;
  reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;
  assume
A1: X1 meets X2;
  thus X1 misses X0 or X2 misses X0 implies (X1 meet X2) misses X0
  proof
    assume X1 misses X0 or X2 misses X0;
    then A1 misses A0 or A2 misses A0 by TSEP_1:def 3;
    then A1 /\ A0 = {} or A2 /\ A0 = {} by XBOOLE_0:def 7;
    then (A1 /\ A0) /\ (A2 /\ A0) = {};
    then A1 /\ ((A2 /\ A0) /\ A0) = {} by XBOOLE_1:16;
    then A1 /\ (A2 /\ (A0 /\ A0)) = {} by XBOOLE_1:16;
    then (A1 /\ A2) /\ A0 = {} by XBOOLE_1:16;
    then (the carrier of (X1 meet X2)) /\ A0 = {} by A1,TSEP_1:def 4;
    then (the carrier of (X1 meet X2)) misses A0 by XBOOLE_0:def 7;
    hence thesis by TSEP_1:def 3;
  end;
  hence thesis;
end;

theorem Th38:
  for X0 being closed non empty SubSpace of X holds X0 meets X1
  implies X0 meet X1 is closed SubSpace of X1
proof
  let X0 be closed non empty SubSpace of X;
  reconsider A0 = the carrier of X0 as Subset of X by TSEP_1:1;
  reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;
  reconsider B = A0 /\ A1 as Subset of X1 by XBOOLE_1:17;
  B = A0 /\ [#]X1 & A0 is closed by TSEP_1:11;
  then
A1: B is closed by PRE_TOPC:13;
  assume
A2: X0 meets X1;
  then B = the carrier of X0 meet X1 by TSEP_1:def 4;
  hence thesis by A2,A1,TSEP_1:11,27;
end;

theorem Th39:
  for X0 being open non empty SubSpace of X holds X0 meets X1
  implies X0 meet X1 is open SubSpace of X1
proof
  let X0 be open non empty SubSpace of X;
  reconsider A0 = the carrier of X0 as Subset of X by TSEP_1:1;
  reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;
  reconsider B = A0 /\ A1 as Subset of X1 by XBOOLE_1:17;
  B = A0 /\ [#]X1 & A0 is open by TSEP_1:16;
  then
A1: B is open by TOPS_2:24;
  assume
A2: X0 meets X1;
  then B = the carrier of X0 meet X1 by TSEP_1:def 4;
  hence thesis by A2,A1,TSEP_1:16,27;
end;

theorem
  for X0 being closed non empty SubSpace of X holds X1 is SubSpace of X0
  & X0 misses X2 implies X1 is closed SubSpace of X1 union X2 & X1 is closed
  SubSpace of X2 union X1
proof
A1: X1 is SubSpace of X1 union X2 by TSEP_1:22;
  reconsider S = the TopStruct of X1 as SubSpace of X by Th6;
  let X0 be closed non empty SubSpace of X;
  assume
A2: X1 is SubSpace of X0;
  assume X0 misses X2;
  then
A3: X0 meet (X1 union X2) = the TopStruct of X1 by A2,Th28;
  X0 meets X1 by A2,Th17;
  then X0 meets X1 union X2 by A1,Th18;
  then S is closed SubSpace of X1 union X2 by A3,Th38;
  hence thesis by Th8;
end;

theorem Th41:
  for X0 being open non empty SubSpace of X holds X1 is SubSpace
  of X0 & X0 misses X2 implies X1 is open SubSpace of X1 union X2 & X1 is open
  SubSpace of X2 union X1
proof
A1: X1 is SubSpace of X1 union X2 by TSEP_1:22;
  reconsider S = the TopStruct of X1 as SubSpace of X by Th6;
  let X0 be open non empty SubSpace of X;
  assume
A2: X1 is SubSpace of X0;
  assume X0 misses X2;
  then
A3: X0 meet (X1 union X2) = the TopStruct of X1 by A2,Th28;
  X0 meets X1 by A2,Th17;
  then X0 meets X1 union X2 by A1,Th18;
  then S is open SubSpace of X1 union X2 by A3,Th39;
  hence thesis by Th9;
end;

begin :: 3. Continuity of Mappings.

definition
  let X, Y be non empty TopSpace, f be Function of X,Y, x be Point of X;
  pred f is_continuous_at x means
  :Def2:
  for G being a_neighborhood of f.x ex
  H being a_neighborhood of x st f.:H c= G;
end;

notation
  let X, Y be non empty TopSpace, f be Function of X,Y, x be Point of X;
  antonym f is_not_continuous_at x for f is_continuous_at x;
end;

reserve X, Y for non empty TopSpace;
reserve f for Function of X,Y;

theorem Th42:
  for x being Point of X holds f is_continuous_at x iff for G
  being a_neighborhood of f.x holds f"G is a_neighborhood of x
proof
  let x be Point of X;
  thus f is_continuous_at x implies for G being a_neighborhood of f.x holds f"
  G is a_neighborhood of x
  proof
    assume
A1: f is_continuous_at x;
    let G be a_neighborhood of f.x;
    consider H being a_neighborhood of x such that
A2: f.:H c= G by A1,Def2;
    ex V being Subset of X st V is open & V c= f"G & x in V
    proof
      consider V being Subset of X such that
A3:   V is open & V c= H & x in V by CONNSP_2:6;
      take V;
      H c= f"G by A2,FUNCT_2:95;
      hence thesis by A3,XBOOLE_1:1;
    end;
    hence thesis by CONNSP_2:6;
  end;
  assume
A4: for G being a_neighborhood of f.x holds f"G is a_neighborhood of x;
  let G be a_neighborhood of f.x;
  reconsider H = f"G as a_neighborhood of x by A4;
  take H;
  thus thesis by FUNCT_1:75;
end;

theorem Th43:
  for x being Point of X holds f is_continuous_at x iff for G
being Subset of Y st G is open & f.x in G ex H being Subset of X st H is open &
  x in H & f.:H c= G
proof
  let x be Point of X;
  thus f is_continuous_at x implies for G being Subset of Y st G is open & f.x
  in G ex H being Subset of X st H is open & x in H & f.:H c= G
  proof
    assume
A1: f is_continuous_at x;
    let G be Subset of Y;
    assume G is open & f.x in G;
    then reconsider G0 = G as a_neighborhood of f.x by CONNSP_2:3;
    consider H0 being a_neighborhood of x such that
A2: f.:H0 c= G0 by A1,Def2;
    consider H being Subset of X such that
A3: H is open and
A4: H c= H0 and
A5: x in H by CONNSP_2:6;
    take H;
    f.:H c= f.:H0 by A4,RELAT_1:123;
    hence thesis by A2,A3,A5,XBOOLE_1:1;
  end;
  assume
A6: for G being Subset of Y st G is open & f.x in G ex H being Subset of
  X st H is open & x in H & f.:H c= G;
  let G0 be a_neighborhood of f.x;
  consider G being Subset of Y such that
A7: G is open and
A8: G c= G0 and
A9: f.x in G by CONNSP_2:6;
  consider H being Subset of X such that
A10: H is open & x in H and
A11: f.:H c= G by A6,A7,A9;
  reconsider H0 = H as a_neighborhood of x by A10,CONNSP_2:3;
  take H0;
  thus thesis by A8,A11,XBOOLE_1:1;
end;

theorem Th44:
  f is continuous iff for x being Point of X holds f is_continuous_at x
proof
  thus f is continuous implies for x being Point of X holds f is_continuous_at
  x
  proof
    assume
A1: f is continuous;
    let x be Point of X;
    for G being a_neighborhood of f.x ex H being a_neighborhood of x st f
    .:H c= G by A1,BORSUK_1:def 1;
    hence thesis by Def2;
  end;
  assume
A2: for x being Point of X holds f is_continuous_at x;
  thus f is continuous
  proof
    let x be Point of X, G be a_neighborhood of f.x;
    f is_continuous_at x by A2;
    hence thesis by Def2;
  end;
end;

theorem Th45:
  for X,Y,Z being non empty TopSpace st the carrier of Y = the
carrier of Z & the topology of Z c= the topology of Y for f being Function of X
  ,Y, g being Function of X,Z st f = g holds for x being Point of X holds f
  is_continuous_at x implies g is_continuous_at x
proof
  let X,Y,Z be non empty TopSpace;
  assume that
A1: the carrier of Y = the carrier of Z and
A2: the topology of Z c= the topology of Y;
  let f be Function of X,Y,g be Function of X,Z;
  assume
A3: f = g;
  let x be Point of X;
  assume
A4: f is_continuous_at x;
  for G being Subset of Z st G is open & g.x in G ex H being Subset of X
  st H is open & x in H & g.:H c= G
  proof
    let G be Subset of Z;
    reconsider F = G as Subset of Y by A1;
    assume that
A5: G is open and
A6: g.x in G;
    G in the topology of Z by A5,PRE_TOPC:def 2;
    then F is open by A2,PRE_TOPC:def 2;
    then consider H being Subset of X such that
A7: H is open & x in H & f.:H c= F by A3,A4,A6,Th43;
    take H;
    thus thesis by A3,A7;
  end;
  hence thesis by Th43;
end;

theorem Th46:
  for X,Y,Z being non empty TopSpace st the carrier of X = the
carrier of Y & the topology of Y c= the topology of X for f being Function of X
  ,Z, g being Function of Y,Z st f = g holds for x being Point of X, y being
  Point of Y st x = y holds g is_continuous_at y implies f is_continuous_at x
proof
  let X,Y,Z be non empty TopSpace;
  assume that
A1: the carrier of X = the carrier of Y and
A2: the topology of Y c= the topology of X;
  let f be Function of X,Z, g be Function of Y,Z;
  assume
A3: f = g;
  let x be Point of X, y be Point of Y;
  assume
A4: x = y;
  assume
A5: g is_continuous_at y;
  for G being Subset of Z st G is open & f.x in G ex H being Subset of X
  st H is open & x in H & f.:H c= G
  proof
    let G be Subset of Z;
    assume G is open & f.x in G;
    then consider H being Subset of Y such that
A6: H is open and
A7: y in H & g.:H c= G by A3,A4,A5,Th43;
    reconsider F = H as Subset of X by A1;
    take F;
    H in the topology of Y by A6,PRE_TOPC:def 2;
    hence thesis by A2,A3,A4,A7,PRE_TOPC:def 2;
  end;
  hence thesis by Th43;
end;

reserve X,Y,Z for non empty TopSpace;
reserve f for Function of X,Y,
  g for Function of Y,Z;

theorem Th47:
  for x being Point of X, y being Point of Y st y = f.x holds f
  is_continuous_at x & g is_continuous_at y implies g*f is_continuous_at x
proof
  let x be Point of X, y be Point of Y such that
A1: y = f.x;
  assume that
A2: f is_continuous_at x and
A3: g is_continuous_at y;
  for G being a_neighborhood of (g*f).x holds (g*f)"G is a_neighborhood of x
  proof
    let G be a_neighborhood of (g*f).x;
    (g*f).x = g.y by A1,FUNCT_2:15;
    then g"G is a_neighborhood of f.x by A1,A3,Th42;
    then f"(g"G) is a_neighborhood of x by A2,Th42;
    hence thesis by RELAT_1:146;
  end;
  hence thesis by Th42;
end;

theorem
  for y being Point of Y holds f is continuous & g is_continuous_at y
  implies for x being Point of X st x in f"{y} holds g*f is_continuous_at x
proof
  let y be Point of Y;
  assume
A1: f is continuous;
  assume
A2: g is_continuous_at y;
  let x be Point of X;
  assume x in f"{y};
  then {x} is Subset of f"{y} by SUBSET_1:41;
  then dom f = [#]X & Im(f,x) c= {y} by FUNCT_2:95,def 1;
  then
A3: {f.x} c= {y} by FUNCT_1:59;
  f.x in {f.x} by TARSKI:def 1;
  then
A4: f.x = y by A3,TARSKI:def 1;
  f is_continuous_at x by A1,Th44;
  hence thesis by A2,A4,Th47;
end;

theorem
  for x being Point of X holds f is_continuous_at x & g is continuous
  implies g*f is_continuous_at x
proof
  let x be Point of X;
  assume
A1: f is_continuous_at x;
  assume g is continuous;
  then g is_continuous_at (f.x) by Th44;
  hence thesis by A1,Th47;
end;

theorem
  f is continuous Function of X,Y iff for x being Point of X holds f
  is_continuous_at x by Th44;

theorem Th51:
  for X,Y,Z being non empty TopSpace st the carrier of Y = the
  carrier of Z & the topology of Z c= the topology of Y for f being continuous
  Function of X,Y holds f is continuous Function of X,Z
proof
  let X,Y,Z be non empty TopSpace;
  assume that
A1: the carrier of Y = the carrier of Z and
A2: the topology of Z c= the topology of Y;
  let f be continuous Function of X,Y;
  reconsider g = f as Function of X,Z by A1;
  for x being Point of X holds g is_continuous_at x
  proof
    let x be Point of X;
    f is_continuous_at x by Th44;
    hence thesis by A1,A2,Th45;
  end;
  hence thesis by Th44;
end;

theorem
  for X,Y,Z being non empty TopSpace st the carrier of X = the carrier
  of Y & the topology of Y c= the topology of X for f being continuous Function
  of Y,Z holds f is continuous Function of X,Z
proof
  let X,Y,Z be non empty TopSpace;
  assume that
A1: the carrier of X = the carrier of Y and
A2: the topology of Y c= the topology of X;
  let f be continuous Function of Y,Z;
  reconsider g = f as Function of X,Z by A1;
  for x being Point of X holds g is_continuous_at x
  proof
    let x be Point of X;
    reconsider y = x as Point of Y by A1;
    f is_continuous_at y by Th44;
    hence thesis by A1,A2,Th46;
  end;
  hence thesis by Th44;
end;

::(Definition of the restriction mapping - general case.)

Lm1:
  for A being set holds {} is Function of A,{}
proof
  let A be set;
  per cases;
  suppose
A1: A = {};
    reconsider f = {} as PartFunc of A,{} by RELSET_1:12;
    f is total by A1;
    hence thesis;
  end;
  suppose A <> {};
    thus thesis by FUNCT_2:def 1,RELSET_1:12;
  end;
end;

definition
  let S,T be 1-sorted;
  let f be Function of S,T;
  let R be 1-sorted such that
A1: the carrier of R c= the carrier of S;
  func f|R -> Function of R,T equals
:Def3:
  f | the carrier of R;
  coherence
  proof
    per cases;
    suppose the carrier of T = {} implies the carrier of S = {};
      hence thesis by A1,FUNCT_2:32;
    end;
    suppose
A1:   the carrier of T = {} & the carrier of S <> {};
      then f|the carrier of R = {};
      hence thesis by A1,Lm1;
    end;
  end;
end;

definition
  let X, Y be non empty TopSpace, f be Function of X,Y;
  let X0 be SubSpace of X;
  redefine func f | X0 equals
  f | the carrier of X0;
  compatibility
  proof
    [#]X0 c= [#]X by PRE_TOPC:def 4;
    hence thesis by Def3;
  end;
end;

reserve X, Y for non empty TopSpace,
  X0 for non empty SubSpace of X;
reserve f for Function of X,Y;

theorem Th53:
  for f0 being Function of X0,Y st for x being Point of X st x in
  the carrier of X0 holds f.x = f0.x holds f|X0 = f0
proof
  let f0 be Function of X0,Y;
  the carrier of X0 is Subset of X by TSEP_1:1;
  hence thesis by FUNCT_2:96;
end;

theorem Th54:
  the TopStruct of X0 = the TopStruct of X implies f = f|X0
proof
  assume the TopStruct of X0 = the TopStruct of X;
  hence f|X0 = f*(id the carrier of X) by RELAT_1:65
    .= f by FUNCT_2:17;
end;

theorem
  for A being Subset of X st A c= the carrier of X0 holds f.:A = (f|X0)
  .:A by FUNCT_2:97;

theorem
  for B being Subset of Y st f"B c= the carrier of X0 holds f"B = (f|X0)
  "B by FUNCT_2:98;

theorem Th57:
  for g being Function of X0,Y ex h being Function of X,Y st h|X0 = g
proof
  let g be Function of X0,Y;
  now
    per cases;
    suppose
A1:   the TopStruct of X = the TopStruct of X0;
      then reconsider h = g as Function of X,Y;
      take h;
      thus h|X0 = g by A1,Th54;
    end;
    suppose
A2:   the TopStruct of X <> the TopStruct of X0;
      Y is SubSpace of Y by TSEP_1:2;
      then reconsider B = the carrier of Y as non empty Subset of Y by TSEP_1:1
;
      set y = the Element of B;
      reconsider A0 = the carrier of X0 as Subset of X by TSEP_1:1;
A3:   X is SubSpace of X by TSEP_1:2;
      then reconsider A = the carrier of X as non empty Subset of X by TSEP_1:1
;
      reconsider A1 = A \ A0 as Subset of X;
A4:   A0 misses A1 by XBOOLE_1:79;
      A0 <> A by A2,A3,TSEP_1:5;
      then not A c= A0 by XBOOLE_0:def 10;
      then reconsider A1 as non empty Subset of A by XBOOLE_1:37;
      reconsider g1 = A1 --> y as Function of A1,B;
      reconsider A0 as non empty Subset of A;
      reconsider g0 = g as Function of A0,B;
      set G = g0 union g1;
      the carrier of X = A1 \/ A0 by XBOOLE_1:45;
      then reconsider h = G as Function of X,Y;
      take h;
      thus h|X0 = g by A4,Th1;
    end;
  end;
  hence thesis;
end;

reserve f for Function of X,Y,
  X0 for non empty SubSpace of X;

theorem Th58:
  for x being Point of X, x0 being Point of X0 st x = x0 holds f
  is_continuous_at x implies f|X0 is_continuous_at x0
proof
  let x be Point of X, x0 be Point of X0 such that
A1: x = x0;
  assume
A2: f is_continuous_at x;
  for G being Subset of Y st G is open & (f|X0).x0 in G ex H0 being Subset
  of X0 st H0 is open & x0 in H0 & (f|X0).:H0 c= G
  proof
    reconsider C = the carrier of X0 as Subset of X by TSEP_1:1;
    let G be Subset of Y such that
A3: G is open and
A4: (f|X0).x0 in G;
    f.x in G by A1,A4,FUNCT_1:49;
    then consider H being Subset of X such that
A5: H is open & x in H and
A6: f.:H c= G by A2,A3,Th43;
    reconsider H0 = H /\ C as Subset of X0 by XBOOLE_1:17;
    f.:H0 c= f.:H /\ f.:C & f.:H /\ f.:C c= f.:H by RELAT_1:121,XBOOLE_1:17;
    then f.:H0 c= f.:H by XBOOLE_1:1;
    then
A7: f.:H0 c= G by A6,XBOOLE_1:1;
    take H0;
    H0 = H /\ [#]X0 & (f|X0).:H0 c= f.:H0 by RELAT_1:128;
    hence thesis by A1,A5,A7,TOPS_2:24,XBOOLE_0:def 4,XBOOLE_1:1;
  end;
  hence thesis by Th43;
end;

::Characterizations of Continuity at the Point by Local one.

theorem Th59:
  for A being Subset of X, x being Point of X, x0 being Point of
  X0 st A c= the carrier of X0 & A is a_neighborhood of x & x = x0 holds f
  is_continuous_at x iff f|X0 is_continuous_at x0
proof
  let A be Subset of X, x be Point of X, x0 be Point of X0 such that
A1: A c= the carrier of X0 and
A2: A is a_neighborhood of x and
A3: x = x0;
  thus f is_continuous_at x implies f|X0 is_continuous_at x0 by A3,Th58;
  thus f|X0 is_continuous_at x0 implies f is_continuous_at x
  proof
    assume
A4: f|X0 is_continuous_at x0;
    for G being Subset of Y st G is open & f.x in G ex H being Subset of X
    st H is open & x in H & f.:H c= G
    proof
      let G be Subset of Y such that
A5:   G is open and
A6:   f.x in G;
      (f|X0).x0 in G by A3,A6,FUNCT_1:49;
      then consider H0 being Subset of X0 such that
A7:   H0 is open and
A8:   x0 in H0 and
A9:   (f|X0).:H0 c= G by A4,A5,Th43;
      consider V being Subset of X such that
A10:  V is open and
A11:  V c= A and
A12:  x in V by A2,CONNSP_2:6;
      reconsider V0 = V as Subset of X0 by A1,A11,XBOOLE_1:1;
A13:  H0 /\ V0 c= V by XBOOLE_1:17;
      then reconsider H = H0 /\ V0 as Subset of X by XBOOLE_1:1;
A14:  for z being Point of Y holds z in f.:H implies z in G
      proof
        set g = f|X0;
        let z be Point of Y;
        assume z in f.:H;
        then consider y being Point of X such that
A15:    y in H and
A16:    z = f.y by FUNCT_2:65;
        y in V by A13,A15;
        then y in A by A11;
        then
A17:    z = g.y by A1,A16,FUNCT_1:49;
        H0 /\ V0 c= H0 by XBOOLE_1:17;
        then z in g.:H0 by A15,A17,FUNCT_2:35;
        hence thesis by A9;
      end;
      take H;
      V0 is open by A10,TOPS_2:25;
      then H0 /\ V0 is open by A7;
      hence thesis by A3,A8,A10,A12,A13,A14,SUBSET_1:2,TSEP_1:9,XBOOLE_0:def 4;
    end;
    hence thesis by Th43;
  end;
end;

theorem Th60:
  for A being Subset of X, x being Point of X, x0 being Point of
  X0 st A is open & x in A & A c= the carrier of X0 & x = x0 holds f
  is_continuous_at x iff f|X0 is_continuous_at x0
proof
  let A be Subset of X, x be Point of X, x0 be Point of X0 such that
A1: A is open & x in A and
A2: A c= the carrier of X0 and
A3: x = x0;
  thus f is_continuous_at x implies f|X0 is_continuous_at x0 by A3,Th58;
  thus f|X0 is_continuous_at x0 implies f is_continuous_at x
  proof
    assume
A4: f|X0 is_continuous_at x0;
    A is a_neighborhood of x by A1,CONNSP_2:3;
    hence thesis by A2,A3,A4,Th59;
  end;
end;

theorem
  for X0 being open non empty SubSpace of X, x being Point of X, x0
  being Point of X0 st x = x0 holds f is_continuous_at x iff f|X0
  is_continuous_at x0
proof
  let X0 be open non empty SubSpace of X, x be Point of X, x0 be Point of X0;
  assume
A1: x = x0;
  hence f is_continuous_at x implies f|X0 is_continuous_at x0 by Th58;
  thus f|X0 is_continuous_at x0 implies f is_continuous_at x
  proof
    reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
    assume
A2: f|X0 is_continuous_at x0;
    A is open by TSEP_1:16;
    hence thesis by A1,A2,Th60;
  end;
end;

registration let X,Y;
  let f be continuous Function of X,Y, X0 be non empty SubSpace of X;
  cluster f|X0 -> continuous;
  coherence
proof
  for x0 being Point of X0 holds f|X0 is_continuous_at x0
  proof
    let x0 be Point of X0;
    the carrier of X0 c= the carrier of X & x0 in the carrier of X0 by
BORSUK_1:1;
    then reconsider x = x0 as Point of X;
    f is_continuous_at x by Th44;
    hence thesis by Th58;
  end;
  hence thesis by Th44;
end;
end;

theorem Th62:
  for X,Y,Z being non empty TopSpace, X0 being non empty SubSpace
of X, f being Function of X,Y, g being Function of Y,Z holds (g*f)|X0 = g*(f|X0
  )
proof
  let X,Y,Z be non empty TopSpace, X0 be non empty SubSpace of X, f be
  Function of X,Y, g be Function of Y,Z;
  set h = g*f;
  h|X0 = h|the carrier of X0;
  then reconsider G = h|the carrier of X0 as Function of X0,Z;
  f|X0 = f|the carrier of X0;
  then reconsider F0 = f|the carrier of X0 as Function of X0,Y;
  set F = g*F0;
  for x being Point of X0 holds G.x = F.x
  proof
    let x be Point of X0;
    the carrier of X0 c= the carrier of X by BORSUK_1:1;
    then reconsider y = x as Element of X by TARSKI:def 3;
    thus G.x = (g*f).y by FUNCT_1:49
      .= g.(f.y) by FUNCT_2:15
      .= g.(F0.x) by FUNCT_1:49
      .= F.x by FUNCT_2:15;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th63:
  for X,Y,Z being non empty TopSpace, X0 being non empty SubSpace
of X, g being Function of Y,Z, f being Function of X,Y st g is continuous & f|
  X0 is continuous holds (g*f)|X0 is continuous
proof
  let X,Y,Z be non empty TopSpace, X0 be non empty SubSpace of X, g be
  Function of Y,Z, f be Function of X,Y such that
A1: g is continuous & f|X0 is continuous;
  (g*f)|X0 = g*(f|X0) by Th62;
  hence thesis by A1;
end;

theorem
  for X,Y,Z being non empty TopSpace, X0 being non empty SubSpace of X,
  g being continuous Function of Y,Z, f being Function of X,Y st f|X0 is
  continuous Function of X0,Y holds (g*f)|X0 is continuous Function of X0,Z by
Th63;

::(Definition of the restriction mapping - special case.)

definition
  let X,Y be non empty TopSpace, X0, X1 be SubSpace of X, g be Function of X0,
  Y;
  assume
A1: X1 is SubSpace of X0;
  func g|X1 -> Function of X1,Y equals
  :Def5:
  g | the carrier of X1;
  coherence
  proof
    the carrier of X1 c= the carrier of X0 by A1,TSEP_1:4;
    hence thesis by FUNCT_2:32;
  end;
end;

reserve X, Y for non empty TopSpace,
  X0, X1 for non empty SubSpace of X;
reserve f for Function of X,Y,
  g for Function of X0,Y;

theorem Th65:
  X1 is SubSpace of X0 implies for x0 being Point of X0 st x0 in
  the carrier of X1 holds g.x0 = (g|X1).x0
proof
  assume
A1: X1 is SubSpace of X0;
  let x0 be Point of X0;
  assume x0 in the carrier of X1;
  hence g.x0 = (g|(the carrier of X1)).x0 by FUNCT_1:49
    .= (g|X1).x0 by A1,Def5;
end;

theorem
  X1 is SubSpace of X0 implies for g1 being Function of X1,Y st for x0
being Point of X0 st x0 in the carrier of X1 holds g.x0 = g1.x0 holds g|X1 = g1
proof
  assume
A1: X1 is SubSpace of X0;
  then
A2: the carrier of X1 is Subset of X0 by TSEP_1:1;
  let g1 be Function of X1,Y;
  assume
  for x0 being Point of X0 st x0 in the carrier of X1 holds g.x0 = g1. x0;
  then g|(the carrier of X1) = g1 by A2,FUNCT_2:96;
  hence thesis by A1,Def5;
end;

theorem Th67:
  g = g|X0
proof
  X0 is SubSpace of X0 by TSEP_1:2;
  hence g|X0 = g|(the carrier of X0) by Def5
    .= g*(id the carrier of X0) by RELAT_1:65
    .= g by FUNCT_2:17;
end;

theorem Th68:
  X1 is SubSpace of X0 implies for A being Subset of X0 st A c=
  the carrier of X1 holds g.:A = (g|X1).:A
proof
  assume
A1: X1 is SubSpace of X0;
  let A be Subset of X0;
  assume A c= the carrier of X1;
  hence g.:A = (g|(the carrier of X1)).:A by FUNCT_2:97
    .= (g|X1).:A by A1,Def5;
end;

theorem
  X1 is SubSpace of X0 implies for B being Subset of Y st g"B c= the
  carrier of X1 holds g"B = (g|X1)"B
proof
  assume
A1: X1 is SubSpace of X0;
  let B be Subset of Y;
  assume g"B c= the carrier of X1;
  hence g"B = (g|(the carrier of X1))"B by FUNCT_2:98
    .= (g|X1)"B by A1,Def5;
end;

theorem Th70:
  for g being Function of X0,Y st g = f|X0 holds X1 is SubSpace of
  X0 implies g|X1 = f|X1
proof
  let g be Function of X0,Y;
  assume
A1: g = f|X0;
  assume
A2: X1 is SubSpace of X0;
  then
A3: the carrier of X1 c= the carrier of X0 by TSEP_1:4;
  thus g|X1 = g|(the carrier of X1) by A2,Def5
    .= f|X1 by A1,A3,FUNCT_1:51;
end;

theorem Th71:
  X1 is SubSpace of X0 implies (f|X0)|X1 = f|X1
proof
  assume
A1: X1 is SubSpace of X0;
  then
A2: the carrier of X1 c= the carrier of X0 by TSEP_1:4;
  f|X0 = f|(the carrier of X0);
  then reconsider h = f|(the carrier of X0) as Function of X0,Y;
  thus (f|X0)|X1 = h|(the carrier of X1) by A1,Def5
    .= f|X1 by A2,FUNCT_1:51;
end;

theorem Th72:
  for X0, X1, X2 being non empty SubSpace of X st X1 is SubSpace
of X0 & X2 is SubSpace of X1 for g being Function of X0,Y holds (g|X1)|X2 = g|
  X2
proof
  let X0, X1, X2 be non empty SubSpace of X such that
A1: X1 is SubSpace of X0 and
A2: X2 is SubSpace of X1;
A3: X2 is SubSpace of X0 by A1,A2,TSEP_1:7;
  let g be Function of X0,Y;
  set h = g|X1;
A4: h = g|(the carrier of X1) & the carrier of X2 c= the carrier of X1 by A1,A2
,Def5,TSEP_1:4;
  thus h|X2 = h|(the carrier of X2) by A2,Def5
    .= g|(the carrier of X2) by A4,FUNCT_1:51
    .= g|X2 by A3,Def5;
end;

theorem
  for f being Function of X,Y, f0 being Function of X1,Y, g being
Function of X0,Y holds X0 = X & f = g implies (g|X1 = f0 iff f|X1 = f0) by Def5
;

reserve X0, X1, X2 for non empty SubSpace of X;
reserve f for Function of X,Y,
  g for Function of X0,Y;

theorem Th74:
  for x0 being Point of X0, x1 being Point of X1 st x0 = x1 holds
  X1 is SubSpace of X0 & g is_continuous_at x0 implies g|X1 is_continuous_at x1
proof
  let x0 be Point of X0, x1 be Point of X1 such that
A1: x0 = x1;
  assume
A2: X1 is SubSpace of X0;
  assume
A3: g is_continuous_at x0;
  for G being Subset of Y st G is open & (g|X1).x1 in G ex H0 being Subset
  of X1 st H0 is open & x1 in H0 & (g|X1).:H0 c= G
  proof
    reconsider C = the carrier of X1 as Subset of X0 by A2,TSEP_1:1;
    let G be Subset of Y such that
A4: G is open and
A5: (g|X1).x1 in G;
    g.x0 in G by A1,A2,A5,Th65;
    then consider H being Subset of X0 such that
A6: H is open & x0 in H and
A7: g.:H c= G by A3,A4,Th43;
    reconsider H0 = H /\ C as Subset of X1 by XBOOLE_1:17;
    g.:H0 c= g.:H /\ g.:C & g.:H /\ g.:C c= g.:H by RELAT_1:121,XBOOLE_1:17;
    then g.:H0 c= g.:H by XBOOLE_1:1;
    then
A8: g.:H0 c= G by A7,XBOOLE_1:1;
    take H0;
    g|X1 = g|C by A2,Def5;
    then H0 = H /\ [#]X1 & (g|X1).:H0 c= g.:H0 by RELAT_1:128;
    hence thesis by A1,A2,A6,A8,TOPS_2:24,XBOOLE_0:def 4,XBOOLE_1:1;
  end;
  hence thesis by Th43;
end;

theorem Th75:
  X1 is SubSpace of X0 implies for x0 being Point of X0, x1 being
  Point of X1 st x0 = x1 holds f|X0 is_continuous_at x0 implies f|X1
  is_continuous_at x1
proof
  assume
A1: X1 is SubSpace of X0;
  let x0 be Point of X0, x1 be Point of X1;
  assume
A2: x0 = x1;
  assume f|X0 is_continuous_at x0;
  then (f|X0)|X1 is_continuous_at x1 by A1,A2,Th74;
  hence thesis by A1,Th71;
end;

::Characterizations of Continuity at the Point by Local one.

theorem Th76:
  X1 is SubSpace of X0 implies for A being Subset of X0, x0 being
  Point of X0, x1 being Point of X1 st A c= the carrier of X1 & A is
  a_neighborhood of x0 & x0 = x1 holds g is_continuous_at x0 iff g|X1
  is_continuous_at x1
proof
  assume
A1: X1 is SubSpace of X0;
  let A be Subset of X0, x0 be Point of X0, x1 be Point of X1 such that
A2: A c= the carrier of X1 and
A3: A is a_neighborhood of x0 and
A4: x0 = x1;
  thus g is_continuous_at x0 implies g|X1 is_continuous_at x1 by A1,A4,Th74;
  thus g|X1 is_continuous_at x1 implies g is_continuous_at x0
  proof
    assume
A5: g|X1 is_continuous_at x1;
    for G being Subset of Y st G is open & g.x0 in G ex H being Subset of
    X0 st H is open & x0 in H & g.:H c= G
    proof
      let G be Subset of Y such that
A6:   G is open and
A7:   g.x0 in G;
      (g|X1).x1 in G by A1,A4,A7,Th65;
      then consider H1 being Subset of X1 such that
A8:   H1 is open and
A9:   x1 in H1 and
A10:  (g|X1).:H1 c= G by A5,A6,Th43;
      consider V being Subset of X0 such that
A11:  V is open and
A12:  V c= A and
A13:  x0 in V by A3,CONNSP_2:6;
      reconsider V1 = V as Subset of X1 by A2,A12,XBOOLE_1:1;
A14:  H1 /\ V1 c= V by XBOOLE_1:17;
      then reconsider H = H1 /\ V1 as Subset of X0 by XBOOLE_1:1;
A15:  for z being Point of Y holds z in g.:H implies z in G
      proof
        set f = g|X1;
        let z be Point of Y;
        assume z in g.:H;
        then consider y being Point of X0 such that
A16:    y in H and
A17:    z = g.y by FUNCT_2:65;
        y in V by A14,A16;
        then y in A by A12;
        then
A18:    z = f.y by A1,A2,A17,Th65;
        H1 /\ V1 c= H1 by XBOOLE_1:17;
        then z in f.:H1 by A16,A18,FUNCT_2:35;
        hence thesis by A10;
      end;
      take H;
      V1 is open by A1,A11,TOPS_2:25;
      then H1 /\ V1 is open by A8;
      hence thesis by A1,A4,A9,A11,A13,A14,A15,SUBSET_1:2,TSEP_1:9
,XBOOLE_0:def 4;
    end;
    hence thesis by Th43;
  end;
end;

theorem Th77:
  X1 is SubSpace of X0 implies for A being Subset of X0, x0 being
Point of X0, x1 being Point of X1 st A is open & x0 in A & A c= the carrier of
  X1 & x0 = x1 holds g is_continuous_at x0 iff g|X1 is_continuous_at x1
proof
  assume
A1: X1 is SubSpace of X0;
  let A be Subset of X0, x0 be Point of X0, x1 be Point of X1 such that
A2: A is open & x0 in A and
A3: A c= the carrier of X1 and
A4: x0 = x1;
  thus g is_continuous_at x0 implies g|X1 is_continuous_at x1 by A1,A4,Th74;
  thus g|X1 is_continuous_at x1 implies g is_continuous_at x0
  proof
    assume
A5: g|X1 is_continuous_at x1;
    A is a_neighborhood of x0 by A2,CONNSP_2:3;
    hence thesis by A1,A3,A4,A5,Th76;
  end;
end;

theorem
  X1 is SubSpace of X0 implies for A being Subset of X, x0 being Point
  of X0, x1 being Point of X1 st A is open & x0 in A & A c= the carrier of X1 &
  x0 = x1 holds g is_continuous_at x0 iff g|X1 is_continuous_at x1
proof
  assume
A1: X1 is SubSpace of X0;
  let A be Subset of X, x0 be Point of X0, x1 be Point of X1 such that
A2: A is open and
A3: x0 in A and
A4: A c= the carrier of X1 and
A5: x0 = x1;
  thus g is_continuous_at x0 implies g|X1 is_continuous_at x1 by A1,A5,Th74;
  thus g|X1 is_continuous_at x1 implies g is_continuous_at x0
  proof
    the carrier of X1 c= the carrier of X0 by A1,TSEP_1:4;
    then reconsider B = A as Subset of X0 by A4,XBOOLE_1:1;
    assume
A6: g|X1 is_continuous_at x1;
    B is open by A2,TOPS_2:25;
    hence thesis by A1,A3,A4,A5,A6,Th77;
  end;
end;

theorem Th79:
  X1 is open SubSpace of X0 implies for x0 being Point of X0, x1
  being Point of X1 st x0 = x1 holds g is_continuous_at x0 iff g|X1
  is_continuous_at x1
proof
  assume
A1: X1 is open SubSpace of X0;
  let x0 be Point of X0, x1 be Point of X1;
  assume
A2: x0 = x1;
  hence g is_continuous_at x0 implies g|X1 is_continuous_at x1 by A1,Th74;
  thus g|X1 is_continuous_at x1 implies g is_continuous_at x0
  proof
    reconsider A = the carrier of X1 as Subset of X0 by A1,TSEP_1:1;
    assume
A3: g|X1 is_continuous_at x1;
    A is open by A1,TSEP_1:16;
    hence thesis by A1,A2,A3,Th77;
  end;
end;

theorem
  X1 is open SubSpace of X & X1 is SubSpace of X0 implies for x0 being
Point of X0, x1 being Point of X1 st x0 = x1 holds g is_continuous_at x0 iff g|
  X1 is_continuous_at x1
proof
  assume
A1: X1 is open SubSpace of X;
  assume
A2: X1 is SubSpace of X0;
  let x0 be Point of X0, x1 be Point of X1;
  assume
A3: x0 = x1;
  hence g is_continuous_at x0 implies g|X1 is_continuous_at x1 by A2,Th74;
  thus g|X1 is_continuous_at x1 implies g is_continuous_at x0
  proof
    the carrier of X1 c= the carrier of X0 by A2,TSEP_1:4;
    then
A4: X1 is open SubSpace of X0 by A1,TSEP_1:19;
    assume g|X1 is_continuous_at x1;
    hence thesis by A3,A4,Th79;
  end;
end;

theorem Th81:
  the TopStruct of X1 = X0 implies for x0 being Point of X0, x1
  being Point of X1 st x0 = x1 holds g|X1 is_continuous_at x1 implies g
  is_continuous_at x0
proof
  reconsider Y1 = the TopStruct of X1 as TopSpace;
  assume
A1: the TopStruct of X1 = X0;
  then the carrier of X1 c= the carrier of X0;
  then reconsider A = the carrier of X1 as Subset of X0;
  A = [#]X0 by A1;
  then
A2: A is open;
  Y1 is SubSpace of X0 by A1,TSEP_1:2;
  then
A3: X1 is open SubSpace of X0 by A2,Th7,TSEP_1:16;
  let x0 be Point of X0, x1 be Point of X1 such that
A4: x0 = x1;
  assume g|X1 is_continuous_at x1;
  hence thesis by A4,A3,Th79;
end;

theorem Th82:
  for g being continuous Function of X0,Y holds X1 is SubSpace of
  X0 implies g|X1 is continuous Function of X1,Y
proof
  let g be continuous Function of X0,Y;
  assume
A1: X1 is SubSpace of X0;
  for x1 being Point of X1 holds g|X1 is_continuous_at x1
  proof
    let x1 be Point of X1;
    consider x0 being Point of X0 such that
A2: x0 = x1 by A1,Th10;
    g is_continuous_at x0 by Th44;
    hence thesis by A1,A2,Th74;
  end;
  hence thesis by Th44;
end;

theorem Th83:
  X1 is SubSpace of X0 & X2 is SubSpace of X1 implies for g being
  Function of X0,Y holds g|X1 is continuous Function of X1,Y implies g|X2 is
  continuous Function of X2,Y
proof
  assume
A1: X1 is SubSpace of X0;
  assume
A2: X2 is SubSpace of X1;
  let g be Function of X0,Y;
  assume g|X1 is continuous Function of X1,Y;
  then (g|X1)|X2 is continuous Function of X2,Y by A2,Th82;
  hence thesis by A1,A2,Th72;
end;

registration let X;
 cluster id X -> continuous;
 coherence
proof
  [#]X <> {} & for V being Subset of X st V is open holds (id X)"V is open
  by FUNCT_2:94;
  hence thesis by TOPS_2:43;
end;
end;

::(Definition of the inclusion mapping.)

definition
  let X be non empty TopSpace, X0 be SubSpace of X;

  func incl X0 -> Function of X0,X equals
  (id X)|X0;
  coherence;
  correctness;
end;

notation
  let X be non empty TopSpace, X0 be SubSpace of X;
  synonym X0 incl X for incl X0;
end;

theorem
  for X0 being non empty SubSpace of X, x being Point of X st x in the
  carrier of X0 holds (incl X0).x = x
proof
  let X0 be non empty SubSpace of X, x be Point of X;
  assume x in the carrier of X0;
  hence (incl X0).x = (id X).x by FUNCT_1:49
    .= x by FUNCT_1:18;
end;

theorem
  for X0 being non empty SubSpace of X, f0 being Function of X0,X st for
x being Point of X st x in the carrier of X0 holds x = f0.x holds incl X0 = f0
proof
  let X0 be non empty SubSpace of X, f0 be Function of X0,X;
  assume
A1: for x being Point of X st x in the carrier of X0 holds x = f0.x;
  now
    let x be Point of X such that
A2: x in the carrier of X0;
    (id X).x = x by FUNCT_1:18;
    hence (id X).x = f0.x by A1,A2;
  end;
  hence thesis by Th53;
end;

theorem
  for X0 being non empty SubSpace of X, f being Function of X,Y holds f|
  X0 = f*(incl X0)
proof
  let X0 be non empty SubSpace of X, f be Function of X,Y;
  thus f|X0 = (f*(id X))|X0 by FUNCT_2:17
    .= f*(incl X0) by Th62;
end;

theorem
  for X0 being non empty SubSpace of X holds incl X0 is continuous
  Function of X0,X;

begin :: 4. A Modification of the Topology of Topological Spaces.

reserve X for non empty TopSpace,
  H, G for Subset of X;

definition
  let X;
  let A be Subset of X;
  func A-extension_of_the_topology_of X -> Subset-Family of X equals
  {H \/ (G
  /\ A) : H in the topology of X & G in the topology of X};
  coherence
  proof
    set FF = {H \/ (G /\ A) : H in the topology of X & G in the topology of X};
    now
      let C be set;
      assume C in FF;
      then ex P, S being Subset of X st C = P \/ (S /\ A) & P in the topology
      of X & S in the topology of X;
      hence C in bool the carrier of X;
    end;
    hence thesis by TARSKI:def 3;
  end;
end;

theorem Th88:
  for A being Subset of X holds the topology of X c= A
  -extension_of_the_topology_of X
proof
  let A be Subset of X;
  now
    {}X = ({});
    then reconsider G = {} as Subset of X;
    let W be set;
    assume
A1: W in the topology of X;
    then reconsider H = W as Subset of X;
    H = H \/ (G /\ A) & G in the topology of X by PRE_TOPC:1;
    hence W in A-extension_of_the_topology_of X by A1;
  end;
  hence thesis by TARSKI:def 3;
end;

theorem Th89:
  for A being Subset of X holds {G /\ A where G is Subset of X :
  G in the topology of X} c= A-extension_of_the_topology_of X
proof
  let A be Subset of X;
  now
    {}X = ({});
    then reconsider H = {} as Subset of X;
    let W be set;
    assume W in {G /\ A where G is Subset of X : G in the topology of X};
    then consider G being Subset of X such that
A1: W = G /\ A & G in the topology of X;
    G /\ A = H \/ (G /\ A) & H in the topology of X by PRE_TOPC:1;
    hence W in A-extension_of_the_topology_of X by A1;
  end;
  hence thesis by TARSKI:def 3;
end;

theorem Th90:
  for A being Subset of X holds for C, D being Subset of X st C
in the topology of X & D in {G /\ A where G is Subset of X : G in the topology
  of X} holds C \/ D in A-extension_of_the_topology_of X & C /\ D in A
  -extension_of_the_topology_of X
proof
  let A be Subset of X;
  let C, D be Subset of X;
  assume
A1: C in the topology of X;
  assume D in {G /\ A where G is Subset of X : G in the topology of X};
  then consider G being Subset of X such that
A2: D = G /\ A and
A3: G in the topology of X;
  thus C \/ D in A-extension_of_the_topology_of X by A1,A2,A3;
  thus C /\ D in A-extension_of_the_topology_of X
  proof
    {}X = ({});
    then reconsider H = {} as Subset of X;
A4: C /\ D = H \/ ((C /\ G) /\ A) & H in the topology of X by A2,PRE_TOPC:1
,XBOOLE_1:16;
    C /\ G in the topology of X by A1,A3,PRE_TOPC:def 1;
    hence thesis by A4;
  end;
end;

theorem Th91:
  for A being Subset of X holds A in A -extension_of_the_topology_of X
proof
  let A be Subset of X;
  X is SubSpace of X by TSEP_1:2;
  then reconsider G = the carrier of X as Subset of X by TSEP_1:1;
A1: G in the topology of X by PRE_TOPC:def 1;
  {}X = ({});
  then reconsider H = {} as Subset of X;
  A = H \/ (G /\ A) & H in the topology of X by PRE_TOPC:1,XBOOLE_1:28;
  hence thesis by A1;
end;

theorem Th92:
  for A being Subset of X holds A in the topology of X iff the
  topology of X = A-extension_of_the_topology_of X
proof
  let A be Subset of X;
  thus A in the topology of X implies the topology of X = A
  -extension_of_the_topology_of X
  proof
    assume
A1: A in the topology of X;
    now
      let W be set;
      assume W in A-extension_of_the_topology_of X;
      then consider H, G being Subset of X such that
A2:   W = H \/ (G /\ A) and
A3:   H in the topology of X and
A4:   G in the topology of X;
      reconsider H1 = H as Subset of X;
      G /\ A in the topology of X by A1,A4,PRE_TOPC:def 1;
      then
A5:   G /\ A is open by PRE_TOPC:def 2;
      H1 is open by A3,PRE_TOPC:def 2;
      then H1 \/ (G /\ A) is open by A5;
      hence W in the topology of X by A2,PRE_TOPC:def 2;
    end;
    then
A6: A-extension_of_the_topology_of X c= the topology of X by TARSKI:def 3;
    the topology of X c= A-extension_of_the_topology_of X by Th88;
    hence thesis by A6,XBOOLE_0:def 10;
  end;
  thus thesis by Th91;
end;

definition
  let X be non empty TopSpace, A be Subset of X;
  func X modified_with_respect_to A -> strict TopSpace equals
  TopStruct(#the
    carrier of X, A-extension_of_the_topology_of X#);
  coherence
  proof
    set Y = TopStruct(#the carrier of X, A-extension_of_the_topology_of X#);
A1: for C,D being Subset of Y st C in the topology of Y & D in the
    topology of Y holds C /\ D in the topology of Y
    proof
      let C,D be Subset of Y;
      assume that
A2:   C in the topology of Y and
A3:   D in the topology of Y;
      consider H1, G1 being Subset of X such that
A4:   C = H1 \/ (G1 /\ A) and
A5:   H1 in the topology of X and
A6:   G1 in the topology of X by A2;
      consider H2, G2 being Subset of X such that
A7:   D = H2 \/ (G2 /\ A) and
A8:   H2 in the topology of X and
A9:   G2 in the topology of X by A3;
A10:  C /\ D = H1 /\ (H2 \/ (G2 /\ A)) \/ (G1 /\ A) /\ (H2 \/ ( G2 /\ A)
      ) by A4,A7,XBOOLE_1:23
        .= (H1 /\ H2 \/ H1 /\ (G2 /\ A)) \/ (G1 /\ A) /\ (H2 \/ (G2 /\ A))
      by XBOOLE_1:23
        .= (H1 /\ H2 \/ H1 /\ (G2 /\ A)) \/ ((G1 /\ A) /\ H2 \/ ((G1 /\ A)
      /\ (G2 /\ A))) by XBOOLE_1:23
        .= (H1 /\ H2 \/ ((H1 /\ G2) /\ A)) \/ ((G1 /\ A) /\ H2 \/ ((G1 /\ A)
      /\ (G2 /\ A))) by XBOOLE_1:16
        .= (H1 /\ H2 \/ ((H1 /\ G2) /\ A)) \/ ((G1 /\ A) /\ H2 \/ G1 /\ ((G2
      /\ A) /\ A)) by XBOOLE_1:16
        .= (H1 /\ H2 \/ ((H1 /\ G2) /\ A)) \/ ((G1 /\ A) /\ H2 \/ G1 /\ (G2
      /\ (A /\ A))) by XBOOLE_1:16
        .= (H1 /\ H2 \/ ((H1 /\ G2) /\ A)) \/ (H2 /\ (G1 /\ A) \/ (G1 /\ G2)
      /\ A) by XBOOLE_1:16
        .= (H1 /\ H2 \/ ((H1 /\ G2) /\ A)) \/ ((H2 /\ G1) /\ A \/ (G1 /\ G2)
      /\ A) by XBOOLE_1:16
        .= (H1 /\ H2 \/ ((H1 /\ G2) /\ A)) \/ ((H2 /\ G1 \/ G1 /\ G2) /\ A)
      by XBOOLE_1:23
        .= H1 /\ H2 \/ (((H1 /\ G2) /\ A) \/ ((H2 /\ G1 \/ G1 /\ G2) /\ A))
      by XBOOLE_1:4
        .= H1 /\ H2 \/ ((H1 /\ G2 \/ (H2 /\ G1 \/ G1 /\ G2)) /\ A) by
XBOOLE_1:23
        .= H1 /\ H2 \/ ((H1 /\ G2 \/ H2 /\ G1 \/ G1 /\ G2) /\ A) by XBOOLE_1:4;
      G1 /\ G2 in the topology of X by A6,A9,PRE_TOPC:def 1;
      then
A11:  G1 /\ G2 is open by PRE_TOPC:def 2;
      H2 /\ G1 in the topology of X by A6,A8,PRE_TOPC:def 1;
      then
A12:  H2 /\ G1 is open by PRE_TOPC:def 2;
      H1 /\ G2 in the topology of X by A5,A9,PRE_TOPC:def 1;
      then H1 /\ G2 is open by PRE_TOPC:def 2;
      then (H1 /\ G2) \/ (H2 /\ G1) is open by A12;
      then (H1 /\ G2) \/ (H2 /\ G1) \/ (G1 /\ G2) is open by A11;
      then
A13:  (H1 /\ G2) \/ (H2 /\ G1) \/ (G1 /\ G2) in the topology of X by
PRE_TOPC:def 2;
      H1 /\ H2 in the topology of X by A5,A8,PRE_TOPC:def 1;
      hence thesis by A13,A10;
    end;
A14: for FF being Subset-Family of Y st FF c= the topology of Y holds union
    FF in the topology of Y
    proof
      set SAA = {G /\ A where G is Subset of X : G in the topology of X};
      SAA c= A-extension_of_the_topology_of X by Th89;
      then reconsider SAA as Subset-Family of X by TOPS_2:2;
      let FF be Subset-Family of Y;
      set AA = {P \/ (S /\ A) where P is Subset of X, S is Subset of X : P in
      the topology of X & S in the topology of X};
      set FF1 = {H where H is Subset of X : H in the topology of X & ex G
      being Subset of X st G in the topology of X & H \/ (G /\ A) in FF};
      set FF2 = {G /\ A where G is Subset of X : G in the topology of X & ex H
      being Subset of X st H in the topology of X & H \/ (G /\ A) in FF};
      now
        let W be set;
        assume W in FF1;
        then ex H being Subset of X st W = H & H in the topology of X & ex G
        being Subset of X st G in the topology of X & H \/ (G /\ A) in FF;
        hence W in the topology of X;
      end;
      then
A15:  FF1 c= the topology of X by TARSKI:def 3;
      now
        let W be set;
        assume W in FF2;
        then ex G being Subset of X st W = G /\ A & G in the topology of X &
        ex H being Subset of X st H in the topology of X & H \/ (G /\ A) in FF;
        hence W in SAA;
      end;
      then
A16:  FF2 c= SAA by TARSKI:def 3;
      then reconsider FF2 as Subset-Family of X by TOPS_2:2;
A17:  union FF2 in SAA
      proof
        now
          per cases;
          suppose
A18:        A = {};
            now
              let W be set;
              assume W in {{}};
              then
A19:          W = {} /\ A by TARSKI:def 1;
              {} in the topology of X by PRE_TOPC:1;
              hence W in SAA by A19;
            end;
            then
A20:        {{}} c= SAA by TARSKI:def 3;
            now
              let W be set;
              assume W in SAA;
              then
              ex G being Subset of X st W = G /\ A & G in the topology of X;
              hence W in {{}} by A18,TARSKI:def 1;
            end;
            then SAA c= {{}} by TARSKI:def 3;
            then
A21:        SAA = {{}} by A20,XBOOLE_0:def 10;
            now
              per cases by A16,A21,ZFMISC_1:33;
              suppose
                FF2 = {{}};
                hence union FF2 = {} by ZFMISC_1:25;
              end;
              suppose
                FF2 = {};
                hence union FF2 = {} by ZFMISC_1:2;
              end;
            end;
            hence thesis by A21,TARSKI:def 1;
          end;
          suppose
            A <> {};
            then consider Y being strict non empty SubSpace of X such that
A22:        A = the carrier of Y by TSEP_1:10;
            now
              let W be set;
              assume W in SAA;
              then consider G being Subset of X such that
A23:          W = G /\ A and
A24:          G in the topology of X;
              reconsider C = G /\ [#] Y as Subset of Y;
              C in the topology of Y by A24,PRE_TOPC:def 4;
              hence W in the topology of Y by A22,A23;
            end;
            then
A25:        SAA c= the topology of Y by TARSKI:def 3;
A26:        now
              let W be set;
              assume
A27:          W in the topology of Y;
              then reconsider C = W as Subset of Y;
              ex G being Subset of X st G in the topology of X & C = G /\
              [#]Y by A27,PRE_TOPC:def 4;
              hence W in SAA by A22;
            end;
            then the topology of Y c= SAA by TARSKI:def 3;
            then
A28:        the topology of Y = SAA by A25,XBOOLE_0:def 10;
            then reconsider SS = FF2 as Subset-Family of Y by A16,TOPS_2:2;
            union SS in the topology of Y by A16,A28,PRE_TOPC:def 1;
            hence thesis by A26;
          end;
        end;
        hence thesis;
      end;
      reconsider FF1 as Subset-Family of X by A15,TOPS_2:2;
A29:  union FF1 in the topology of X by A15,PRE_TOPC:def 1;
      now
        let x be set such that
A30:    x in union FF1 \/ union FF2;
        now
          per cases by A30,XBOOLE_0:def 3;
          suppose
            x in union FF1;
            then consider W being set such that
A31:        x in W and
A32:        W in FF1 by TARSKI:def 4;
            consider H being Subset of X such that
A33:        W = H and
            H in the topology of X and
A34:        ex G being Subset of X st G in the topology of X & H \/ (
            G /\ A) in FF by A32;
            consider G being Subset of X such that
A35:        H \/ (G /\ A) in FF by A34;
A36:        H c= H \/ (G /\ A) by XBOOLE_1:7;
            H \/ (G /\ A) c= union FF by A35,ZFMISC_1:74;
            then H c= union FF by A36,XBOOLE_1:1;
            hence x in union FF by A31,A33;
          end;
          suppose
            x in union FF2;
            then consider W being set such that
A37:        x in W and
A38:        W in FF2 by TARSKI:def 4;
            consider G being Subset of X such that
A39:        W = G /\ A and
            G in the topology of X and
A40:        ex H being Subset of X st H in the topology of X & H \/ (
            G /\ A) in FF by A38;
            consider H being Subset of X such that
A41:        H \/ (G /\ A) in FF by A40;
A42:        G /\ A c= H \/ (G /\ A) by XBOOLE_1:7;
            H \/ (G /\ A) c= union FF by A41,ZFMISC_1:74;
            then G /\ A c= union FF by A42,XBOOLE_1:1;
            hence x in union FF by A37,A39;
          end;
        end;
        hence x in union FF;
      end;
      then
A43:  union FF1 \/ union FF2 c= union FF by TARSKI:def 3;
      assume
A44:  FF c= the topology of Y;
      now
        let x be set;
A45:    union FF1 c= union FF1 \/ union FF2 by XBOOLE_1:7;
A46:    union FF2 c= union FF1 \/ union FF2 by XBOOLE_1:7;
        assume x in union FF;
        then consider W being set such that
A47:    x in W and
A48:    W in FF by TARSKI:def 4;
        W in AA by A44,A48;
        then consider H, G being Subset of X such that
A49:    W = H \/ (G /\ A) and
A50:    H in the topology of X & G in the topology of X;
        G /\ A in FF2 by A48,A49,A50;
        then G /\ A c= union FF2 by ZFMISC_1:74;
        then
A51:    G /\ A c= union FF1 \/ union FF2 by A46,XBOOLE_1:1;
        H in FF1 by A48,A49,A50;
        then H c= union FF1 by ZFMISC_1:74;
        then H c= union FF1 \/ union FF2 by A45,XBOOLE_1:1;
        then H \/ (G /\ A) c= union FF1 \/ union FF2 by A51,XBOOLE_1:8;
        hence x in union FF1 \/ union FF2 by A47,A49;
      end;
      then union FF c= union FF1 \/ union FF2 by TARSKI:def 3;
      then union FF = union FF1 \/ union FF2 by A43,XBOOLE_0:def 10;
      hence thesis by A29,A17,Th90;
    end;
    the topology of X c= A-extension_of_the_topology_of X & the carrier of
    X in the topology of X by Th88,PRE_TOPC:def 1;
    hence thesis by A14,A1,PRE_TOPC:def 1;
  end;
end;

registration
  let X be non empty TopSpace, A be Subset of X;
  cluster X modified_with_respect_to A -> non empty;
  coherence;
end;

reserve A for Subset of X;

theorem
  the carrier of (X modified_with_respect_to A) = the carrier of X & the
topology of (X modified_with_respect_to A) = A-extension_of_the_topology_of X;

theorem Th94:
  for B being Subset of X modified_with_respect_to A st B = A holds B is open
proof
  let B be Subset of X modified_with_respect_to A;
  assume B = A;
  then B in A-extension_of_the_topology_of X by Th91;
  hence thesis by PRE_TOPC:def 2;
end;

theorem Th95:
  for A being Subset of X holds A is open iff the TopStruct of X
  = X modified_with_respect_to A
proof
  let A be Subset of X;
  thus A is open implies the TopStruct of X = X modified_with_respect_to A
  proof
    assume A is open;
    then A in the topology of X by PRE_TOPC:def 2;
    hence thesis by Th92;
  end;
  thus the TopStruct of X = X modified_with_respect_to A implies A is open
  proof
    assume the TopStruct of X = X modified_with_respect_to A;
    then A in the topology of X by Th92;
    hence thesis by PRE_TOPC:def 2;
  end;
end;

definition
  let X be non empty TopSpace, A be Subset of X;
  func modid(X,A) -> Function of X,X modified_with_respect_to A equals
  id (the
  carrier of X);
  coherence;
end;

theorem Th96:
  for x being Point of X st not x in A holds modid(X,A) is_continuous_at x
proof
  let x be Point of X;
  assume
A1: not x in A;
  now
    let W be Subset of X modified_with_respect_to A;
    assume that
A2: W is open and
A3: (modid(X,A)).x in W;
    W in A-extension_of_the_topology_of X by A2,PRE_TOPC:def 2;
    then consider H, G being Subset of X such that
A4: W = H \/ (G /\ A) and
A5: H in the topology of X and
    G in the topology of X;
A6: G /\ A c= A by XBOOLE_1:17;
    (modid(X,A)).x = x by FUNCT_1:18;
    then
A7: x in H or x in G /\ A by A3,A4,XBOOLE_0:def 3;
    thus ex V being Subset of X st V is open & x in V & (modid(X,A)).:V c= W
    proof
      reconsider H as Subset of X;
      take H;
      (modid(X,A)).:H = H by FUNCT_1:92;
      hence thesis by A1,A4,A5,A7,A6,PRE_TOPC:def 2,XBOOLE_1:7;
    end;
  end;
  hence thesis by Th43;
end;

theorem Th97:
  for X0 being non empty SubSpace of X st the carrier of X0
  misses A for x0 being Point of X0 holds (modid(X,A))|X0 is_continuous_at x0
proof
  let X0 be non empty SubSpace of X;
  assume
A1: (the carrier of X0) /\ A = {};
  let x0 be Point of X0;
  x0 in the carrier of X0 & the carrier of X0 c= the carrier of X by BORSUK_1:1
;
  then reconsider x = x0 as Point of X;
  not x in A by A1,XBOOLE_0:def 4;
  hence thesis by Th58,Th96;
end;

theorem Th98:
  for X0 being non empty SubSpace of X st the carrier of X0 = A
  for x0 being Point of X0 holds (modid(X,A))|X0 is_continuous_at x0
proof
  let X0 be non empty SubSpace of X;
  assume
A1: the carrier of X0 = A;
  let x0 be Point of X0;
  now
    x0 in the carrier of X0 & the carrier of X0 c= the carrier of X by
BORSUK_1:1;
    then reconsider x = x0 as Point of X;
    let W be Subset of X modified_with_respect_to A;
    assume that
A2: W is open and
A3: (modid(X,A)|X0).x0 in W;
    W in A-extension_of_the_topology_of X by A2,PRE_TOPC:def 2;
    then consider H, G being Subset of X such that
A4: W = H \/ (G /\ A) and
A5: H in the topology of X & G in the topology of X;
    reconsider H, G as Subset of X;
A6: (H /\ A) \/ (G /\ A) c= W by A4,XBOOLE_1:9,17;
    (modid(X,A)|X0).x0 = (id (the carrier of X)).x by FUNCT_1:49
      .= x by FUNCT_1:18;
    then x in H or x in G /\ A by A3,A4,XBOOLE_0:def 3;
    then x in H /\ A or x in G /\ A by A1,XBOOLE_0:def 4;
    then
A7: x in (H /\ A) \/ (G /\ A) by XBOOLE_0:def 3;
A8: (modid(X,A)|X0).:((H \/ G) /\ A) = (id (the carrier of X)).:((H \/ G)
    /\ A) by A1,FUNCT_2:97,XBOOLE_1:17
      .= (H \/ G) /\ A by FUNCT_1:92;
    thus ex V being Subset of X0 st V is open & x0 in V & (modid(X,A)|X0).: V
    c= W
    proof
      reconsider V = (H \/ G) /\ A as Subset of X0 by A1,XBOOLE_1:17;
      take V;
      H is open & G is open by A5,PRE_TOPC:def 2;
      then
A9:   H \/ G is open;
      V = (H \/ G) /\ [#]X0 by A1;
      hence thesis by A7,A8,A6,A9,TOPS_2:24,XBOOLE_1:23;
    end;
  end;
  hence thesis by Th43;
end;

theorem Th99:
  for X0 being non empty SubSpace of X st the carrier of X0
  misses A holds (modid(X,A))|X0 is continuous Function of X0,X
  modified_with_respect_to A
proof
  let X0 be non empty SubSpace of X;
  assume (the carrier of X0) misses A;
  then
  for x0 being Point of X0 holds ((modid(X,A))|X0) is_continuous_at x0 by Th97
;
  hence thesis by Th44;
end;

theorem Th100:
  for X0 being non empty SubSpace of X st the carrier of X0 = A
holds (modid(X,A))|X0 is continuous Function of X0,X modified_with_respect_to A
proof
  let X0 be non empty SubSpace of X;
  assume the carrier of X0 = A;
  then
  for x0 being Point of X0 holds ((modid(X,A))|X0) is_continuous_at x0 by Th98
;
  hence thesis by Th44;
end;

theorem Th101:
  for A being Subset of X holds A is open iff modid(X,A) is
  continuous Function of X,X modified_with_respect_to A
proof
  let A be Subset of X;
  thus A is open implies modid(X,A) is continuous Function of X,X
  modified_with_respect_to A
  proof
    reconsider f = modid(X,A) as Function of X,X;
A1: f = id X;
    assume A is open;
    then the TopStruct of X = X modified_with_respect_to A by Th95;
    hence thesis by A1,Th51;
  end;
A2: [#](X modified_with_respect_to A) <> {};
  thus modid(X,A) is continuous Function of X,X modified_with_respect_to A
  implies A is open
  proof
    set B = (modid(X,A)).:A;
    assume
A3: modid(X,A) is continuous Function of X,X modified_with_respect_to A;
    B = A by FUNCT_1:92;
    then
A4: (modid(X,A))"B = A by FUNCT_2:94;
    B is open by Th94,FUNCT_1:92;
    hence thesis by A2,A3,A4,TOPS_2:43;
  end;
end;

definition
  let X be non empty TopSpace, X0 be SubSpace of X;
  func X modified_with_respect_to X0 -> strict TopSpace means
  :Def10:
  for A being Subset of X st A = the carrier of X0 holds it = X
  modified_with_respect_to A;
  existence
  proof
    reconsider B = the carrier of X0 as Subset of X by TSEP_1:1;
    take X modified_with_respect_to B;
    thus thesis;
  end;
  uniqueness
  proof
    reconsider C = the carrier of X0 as Subset of X by TSEP_1:1;
    let Y1, Y2 be strict TopSpace such that
A1: for A being Subset of X st A = the carrier of X0 holds Y1 = X
    modified_with_respect_to A and
A2: for A being Subset of X st A = the carrier of X0 holds Y2 = X
    modified_with_respect_to A;
    Y1 = X modified_with_respect_to C by A1;
    hence thesis by A2;
  end;
end;

registration
  let X be non empty TopSpace, X0 be SubSpace of X;
  cluster X modified_with_respect_to X0 -> non empty;
  coherence
  proof
    [#]X0 c= [#]X by PRE_TOPC:def 4;
    then reconsider O = [#] X0 as Subset of X;
    X modified_with_respect_to X0 = X modified_with_respect_to O by Def10;
    hence thesis;
  end;
end;

reserve X0 for non empty SubSpace of X;

theorem Th102:
  the carrier of (X modified_with_respect_to X0) = the carrier of
  X & for A being Subset of X st A = the carrier of X0 holds the topology of (X
  modified_with_respect_to X0) = A-extension_of_the_topology_of X
proof
  set Y = X modified_with_respect_to X0;
  reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
A1: Y = X modified_with_respect_to A by Def10;
  hence the carrier of (X modified_with_respect_to X0) = the carrier of X;
  thus thesis by A1;
end;

theorem
  for Y0 being SubSpace of X modified_with_respect_to X0 st the carrier
  of Y0 = the carrier of X0 holds Y0 is open SubSpace of X
  modified_with_respect_to X0
proof
  let Y0 be SubSpace of X modified_with_respect_to X0;
  assume
A1: the carrier of Y0 = the carrier of X0;
  reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
  set Y = X modified_with_respect_to X0;
  reconsider B = the carrier of Y0 as Subset of Y by TSEP_1:1;
  Y = X modified_with_respect_to A by Def10;
  then B is open by A1,Th94;
  hence thesis by TSEP_1:16;
end;

theorem
  X0 is open SubSpace of X iff the TopStruct of X = X
  modified_with_respect_to X0
proof
  thus X0 is open SubSpace of X implies the TopStruct of X = X
  modified_with_respect_to X0
  proof
    reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
    assume X0 is open SubSpace of X;
    then A is open by TSEP_1:def 1;
    then the TopStruct of X = X modified_with_respect_to A by Th95;
    hence thesis by Def10;
  end;
  thus the TopStruct of X = X modified_with_respect_to X0 implies X0 is open
  SubSpace of X
  proof
    assume
A1: the TopStruct of X = X modified_with_respect_to X0;
    now
      let A be Subset of X;
      assume A = the carrier of X0;
      then the TopStruct of X = X modified_with_respect_to A by A1,Def10;
      hence A is open by Th95;
    end;
    hence thesis by TSEP_1:def 1;
  end;
end;

definition
  let X be non empty TopSpace, X0 be SubSpace of X;
  func modid(X,X0) -> Function of X,X modified_with_respect_to X0 means
  :Def11
  :
  for A being Subset of X st A = the carrier of X0 holds it = modid(X,A);
  existence
  proof
    reconsider B = the carrier of X0 as Subset of X by TSEP_1:1;
    reconsider F = modid(X,B) as Function of X,X modified_with_respect_to X0
    by Def10;
    take F;
    thus thesis;
  end;
  uniqueness
  proof
    reconsider C = the carrier of X0 as Subset of X by TSEP_1:1;
    let F1, F2 be Function of X,X modified_with_respect_to X0 such that
A1: for A being Subset of X st A = the carrier of X0 holds F1 = modid( X,A) and
A2: for A being Subset of X st A = the carrier of X0 holds F2 = modid( X,A);
    F1 = modid(X,C) by A1;
    hence thesis by A2;
  end;
end;

theorem
  modid(X,X0) = id X
proof
  reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
  modid(X,A) = modid(X,X0) by Def11;
  hence thesis;
end;

theorem Th106:
  for X0, X1 being non empty SubSpace of X st X0 misses X1 for x1
  being Point of X1 holds (modid(X,X0))|X1 is_continuous_at x1
proof
  let X0, X1 be non empty SubSpace of X;
  reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
  reconsider f = (modid(X,A))|X1 as Function of X1,X modified_with_respect_to
  X0 by Def10;
  assume
A1: X0 misses X1;
  let x1 be Point of X1;
  (the carrier of X1) misses A by A1,TSEP_1:def 3;
  then
A2: (modid(X,A))|X1 is_continuous_at x1 by Th97;
  now
    let W be Subset of X modified_with_respect_to X0;
    reconsider W0 = W as Subset of (X modified_with_respect_to A) by Th102;
    assume that
A3: W is open and
A4: f.x1 in W;
    W in the topology of (X modified_with_respect_to X0) by A3,PRE_TOPC:def 2;
    then W in A-extension_of_the_topology_of X by Th102;
    then
A5: W0 is open by PRE_TOPC:def 2;
    thus ex V being Subset of X1 st V is open & x1 in V & f.:V c= W
    proof
      consider V being Subset of X1 such that
A6:   V is open & x1 in V & ((modid(X,A))|X1).:V c= W0 by A2,A4,A5,Th43;
      take V;
      thus thesis by A6;
    end;
  end;
  then f is_continuous_at x1 by Th43;
  hence thesis by Def11;
end;

theorem Th107:
  for X0 being non empty SubSpace of X for x0 being Point of X0
  holds (modid(X,X0))|X0 is_continuous_at x0
proof
  let X0 be non empty SubSpace of X;
  reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
  reconsider f = (modid(X,A))|X0 as Function of X0,X modified_with_respect_to
  X0 by Def10;
  let x0 be Point of X0;
A1: (modid(X,A))|X0 is_continuous_at x0 by Th98;
  now
    let W be Subset of X modified_with_respect_to X0;
    reconsider W0 = W as Subset of (X modified_with_respect_to A) by Th102;
    assume that
A2: W is open and
A3: f.x0 in W;
    W in the topology of (X modified_with_respect_to X0) by A2,PRE_TOPC:def 2;
    then W in A-extension_of_the_topology_of X by Th102;
    then
A4: W0 is open by PRE_TOPC:def 2;
    thus ex V being Subset of X0 st V is open & x0 in V & f.:V c= W
    proof
      consider V being Subset of X0 such that
A5:   V is open & x0 in V & ((modid(X,A))|X0).:V c= W0 by A1,A3,A4,Th43;
      take V;
      thus thesis by A5;
    end;
  end;
  then f is_continuous_at x0 by Th43;
  hence thesis by Def11;
end;

theorem
  for X0, X1 being non empty SubSpace of X st X0 misses X1 holds (modid(
  X,X0))|X1 is continuous Function of X1,X modified_with_respect_to X0
proof
  let X0, X1 be non empty SubSpace of X;
  assume X0 misses X1;
  then
  for x1 being Point of X1 holds ((modid(X,X0))|X1) is_continuous_at x1 by
Th106;
  hence thesis by Th44;
end;

theorem
  for X0 being non empty SubSpace of X holds (modid(X,X0))|X0 is
  continuous Function of X0,X modified_with_respect_to X0
proof
  let X0 be non empty SubSpace of X;
  for x0 being Point of X0 holds ((modid(X,X0))|X0) is_continuous_at x0 by
Th107;
  hence thesis by Th44;
end;

theorem
  for X0 being SubSpace of X holds X0 is open SubSpace of X iff modid(X,
  X0) is continuous Function of X,X modified_with_respect_to X0
proof
  let X0 be SubSpace of X;
  reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
  thus X0 is open SubSpace of X implies modid(X,X0) is continuous Function of
  X,X modified_with_respect_to X0
  proof
    assume X0 is open SubSpace of X;
    then
A1: A is open by TSEP_1:16;
    X modified_with_respect_to X0 = X modified_with_respect_to A & modid(X
    ,X0) = modid(X,A) by Def10,Def11;
    hence thesis by A1,Th101;
  end;
  thus modid(X,X0) is continuous Function of X,X modified_with_respect_to X0
  implies X0 is open SubSpace of X
  proof
    assume
A2: modid(X,X0) is continuous Function of X,X modified_with_respect_to X0;
    X modified_with_respect_to X0 = X modified_with_respect_to A & modid(X
    ,X0) = modid(X,A) by Def10,Def11;
    then A is open by A2,Th101;
    hence thesis by TSEP_1:16;
  end;
end;

begin :: 5. Continuity of Mappings over the Union of Subspaces.

reserve X, Y for non empty TopSpace;

::Continuity at the Point of Mappings over the Union of Subspaces.

theorem Th111:
  for X1, X2 being non empty SubSpace of X, g being Function of
X1 union X2,Y for x1 being Point of X1, x2 being Point of X2, x being Point of
  X1 union X2 st x = x1 & x = x2 holds g is_continuous_at x iff g|X1
  is_continuous_at x1 & g|X2 is_continuous_at x2
proof
  let X1, X2 be non empty SubSpace of X, g be Function of X1 union X2,Y;
  let x1 be Point of X1, x2 be Point of X2, x be Point of X1 union X2 such
  that
A1: x = x1 and
A2: x = x2;
A3: X2 is SubSpace of X1 union X2 by TSEP_1:22;
A4: X1 is SubSpace of X1 union X2 by TSEP_1:22;
  hence g is_continuous_at x implies g|X1 is_continuous_at x1 & g|X2
  is_continuous_at x2 by A1,A2,A3,Th74;
  thus g|X1 is_continuous_at x1 & g|X2 is_continuous_at x2 implies g
  is_continuous_at x
  proof
    assume that
A5: g|X1 is_continuous_at x1 and
A6: g|X2 is_continuous_at x2;
    for G being a_neighborhood of g.x ex H being a_neighborhood of x st g
    .:H c= G
    proof
      let G be a_neighborhood of g.x;
      g.x = (g|X1).x1 by A1,A4,Th65;
      then consider H1 being a_neighborhood of x1 such that
A7:   (g|X1).:H1 c= G by A5,Def2;
      g.x = (g|X2).x2 by A2,A3,Th65;
      then consider H2 being a_neighborhood of x2 such that
A8:   (g|X2).:H2 c= G by A6,Def2;
      the carrier of X2 c= the carrier of X1 union X2 by A3,TSEP_1:4;
      then reconsider S2 = H2 as Subset of X1 union X2 by XBOOLE_1:1;
      g.:S2 c= G by A3,A8,Th68;
      then
A9:   S2 c= g"G by FUNCT_2:95;
      the carrier of X1 c= the carrier of X1 union X2 by A4,TSEP_1:4;
      then reconsider S1 = H1 as Subset of X1 union X2 by XBOOLE_1:1;
      consider H being a_neighborhood of x such that
A10:  H c= H1 \/ H2 by A1,A2,Th16;
      take H;
      g.:S1 c= G by A4,A7,Th68;
      then S1 c= g"G by FUNCT_2:95;
      then S1 \/ S2 c= g"G by A9,XBOOLE_1:8;
      then H c= g"G by A10,XBOOLE_1:1;
      hence thesis by FUNCT_2:95;
    end;
    hence thesis by Def2;
  end;
end;

theorem
  for f being Function of X,Y, X1, X2 being non empty SubSpace of X for
x being Point of X1 union X2, x1 being Point of X1, x2 being Point of X2 st x =
x1 & x = x2 holds f|(X1 union X2) is_continuous_at x iff f|X1 is_continuous_at
  x1 & f|X2 is_continuous_at x2
proof
  let f be Function of X,Y, X1, X2 be non empty SubSpace of X;
A1: X1 is SubSpace of X1 union X2 & X2 is SubSpace of X1 union X2 by TSEP_1:22;
  let x be Point of X1 union X2, x1 be Point of X1, x2 be Point of X2 such
  that
A2: x = x1 & x = x2;
  thus f|(X1 union X2) is_continuous_at x implies f|X1 is_continuous_at x1 & f
  |X2 is_continuous_at x2 by A2,A1,Th75;
  thus f|X1 is_continuous_at x1 & f|X2 is_continuous_at x2 implies f|(X1 union
  X2) is_continuous_at x
  proof
    set g = f|(X1 union X2);
    assume
A3: f|X1 is_continuous_at x1 & f|X2 is_continuous_at x2;
    g|X1 = f|X1 & g|X2 = f|X2 by A1,Th70;
    hence thesis by A2,A3,Th111;
  end;
end;

theorem
  for f being Function of X,Y, X1, X2 being non empty SubSpace of X st X
  = X1 union X2 for x being Point of X, x1 being Point of X1, x2 being Point of
X2 st x = x1 & x = x2 holds f is_continuous_at x iff f|X1 is_continuous_at x1 &
  f|X2 is_continuous_at x2
proof
  let f be Function of X,Y, X1, X2 be non empty SubSpace of X such that
A1: X = X1 union X2;
  let x be Point of X, x1 be Point of X1, x2 be Point of X2;
  assume that
A2: x = x1 and
A3: x = x2;
  thus f is_continuous_at x implies f|X1 is_continuous_at x1 & f|X2
  is_continuous_at x2 by A2,A3,Th58;
  thus f|X1 is_continuous_at x1 & f|X2 is_continuous_at x2 implies f
  is_continuous_at x
  proof
    assume that
A4: f|X1 is_continuous_at x1 and
A5: f|X2 is_continuous_at x2;
    for G being a_neighborhood of f.x ex H being a_neighborhood of x st f
    .:H c= G
    proof
      let G be a_neighborhood of f.x;
      f.x = (f|X1).x1 by A2,FUNCT_1:49;
      then consider H1 being a_neighborhood of x1 such that
A6:   (f|X1).:H1 c= G by A4,Def2;
      the carrier of X1 c= the carrier of X by BORSUK_1:1;
      then reconsider S1 = H1 as Subset of X by XBOOLE_1:1;
      f.x = (f|X2).x2 by A3,FUNCT_1:49;
      then consider H2 being a_neighborhood of x2 such that
A7:   (f|X2).:H2 c= G by A5,Def2;
      the carrier of X2 c= the carrier of X by BORSUK_1:1;
      then reconsider S2 = H2 as Subset of X by XBOOLE_1:1;
      f.:S2 c= G by A7,FUNCT_2:97;
      then
A8:   S2 c= f"G by FUNCT_2:95;
      consider H being a_neighborhood of x such that
A9:   H c= H1 \/ H2 by A1,A2,A3,Th16;
      take H;
      f.:S1 c= G by A6,FUNCT_2:97;
      then S1 c= f"G by FUNCT_2:95;
      then S1 \/ S2 c= f"G by A8,XBOOLE_1:8;
      then H c= f"G by A9,XBOOLE_1:1;
      hence thesis by FUNCT_2:95;
    end;
    hence thesis by Def2;
  end;
end;

reserve X1, X2 for non empty SubSpace of X;

::Continuity of Mappings over the Union of Subspaces.

theorem Th114:
  X1,X2 are_weakly_separated implies for g being Function of X1
  union X2,Y holds g is continuous Function of X1 union X2,Y iff g|X1 is
  continuous Function of X1,Y & g|X2 is continuous Function of X2,Y
proof
  assume
A1: X1,X2 are_weakly_separated;
  let g be Function of X1 union X2,Y;
A2: X2 is SubSpace of X1 union X2 by TSEP_1:22;
A3: X1 is SubSpace of X1 union X2 by TSEP_1:22;
  hence g is continuous Function of X1 union X2,Y implies g|X1 is continuous
  Function of X1,Y & g|X2 is continuous Function of X2,Y by A2,Th82;
  thus g|X1 is continuous Function of X1,Y & g|X2 is continuous Function of X2
  ,Y implies g is continuous Function of X1 union X2,Y
  proof
    assume that
A4: g|X1 is continuous Function of X1,Y and
A5: g|X2 is continuous Function of X2,Y;
    for x being Point of X1 union X2 holds g is_continuous_at x
    proof
      set X0 = X1 union X2;
      let x be Point of X1 union X2;
A6:   X1 meets X2 implies g is_continuous_at x
      proof
        assume
A7:     X1 meets X2;
A8:     now
          assume
A9:       ( not X1 is SubSpace of X2)& not X2 is SubSpace of X1;
          then consider Y1, Y2 being open non empty SubSpace of X such that
A10:      Y1 meet X0 is SubSpace of X1 and
A11:      Y2 meet X0 is SubSpace of X2 and
A12:      X0 is SubSpace of Y1 union Y2 or ex Z being closed non
empty SubSpace of X st the TopStruct of X = (Y1 union Y2) union Z & Z meet X0
          is SubSpace of X1 meet X2 by A1,A7,TSEP_1:89;
A13:      Y2 meets X0 implies Y2 meet X0 is open SubSpace of X0 by Th39;
A14:      Y1 meets X0 implies Y1 meet X0 is open SubSpace of X0 by Th39;
A15:      now
            X is SubSpace of X by TSEP_1:2;
            then reconsider X12 = the TopStruct of X as SubSpace of X by Th6;
            assume
A16:        not X0 is SubSpace of Y1 union Y2;
            then consider Z being closed non empty SubSpace of X such that
A17:        the TopStruct of X = (Y1 union Y2) union Z and
A18:        Z meet X0 is SubSpace of X1 meet X2 by A12;
            the carrier of X0 c= the carrier of X12 by BORSUK_1:1;
            then
A19:        X0 is SubSpace of X12 by TSEP_1:4;
            then X12 meets X0 by Th17;
            then
A20:        ((Y1 union Y2) union Z) meet X0 = the TopStruct of X0 by A17,A19,
TSEP_1:28;
A21:        Y1 meets X0 & Y2 meets X0 by A7,A9,A10,A11,A17,A18,Th32;
A22:        now
A23:          now
                given x2 being Point of Y2 meet X0 such that
A24:            x2 = x;
                g|(Y2 meet X0) is continuous by A2,A5,A11,Th83;
                then g|(Y2 meet X0) is_continuous_at x2 by Th44;
                hence thesis by A7,A9,A10,A11,A13,A17,A18,A24,Th32,Th79;
              end;
A25:          now
                given x1 being Point of Y1 meet X0 such that
A26:            x1 = x;
                g|(Y1 meet X0) is continuous by A3,A4,A10,Th83;
                then g|(Y1 meet X0) is_continuous_at x1 by Th44;
                hence thesis by A7,A9,A10,A11,A14,A17,A18,A26,Th32,Th79;
              end;
              assume
A27:          ex x12 being Point of (Y1 union Y2) meet X0 st x12 = x;
              (Y1 union Y2) meet X0 = (Y1 meet X0) union (Y2 meet X0) by A21,
TSEP_1:32;
              hence thesis by A27,A25,A23,Th11;
            end;
A28:        now
              given x0 being Point of Z meet X0 such that
A29:          x0 = x;
              consider x00 being Point of X1 meet X2 such that
A30:          x00 = x0 by A18,Th10;
              consider x1 being Point of X1 such that
A31:          x1 = x00 by A7,Th12;
              consider x2 being Point of X2 such that
A32:          x2 = x00 by A7,Th12;
              g|X1 is_continuous_at x1 & g|X2 is_continuous_at x2 by A4,A5,Th44
;
              hence thesis by A29,A30,A31,A32,Th111;
            end;
            (Y1 union Y2) meets X0 & Z meets X0 by A7,A9,A10,A11,A16,A17,A18
,Th33;
            then ((Y1 union Y2) meet X0) union (Z meet X0) = the TopStruct of
            X0 by A20,TSEP_1:32;
            hence thesis by A22,A28,Th11;
          end;
          now
            assume
A33:        X0 is SubSpace of Y1 union Y2;
            then
A34:        Y1 meets X0 by A9,A10,A11,Th31;
A35:        now
              given x2 being Point of Y2 meet X0 such that
A36:          x2 = x;
              g|(Y2 meet X0) is continuous by A2,A5,A11,Th83;
              then g|(Y2 meet X0) is_continuous_at x2 by Th44;
              hence thesis by A9,A10,A11,A13,A33,A36,Th31,Th79;
            end;
A37:        now
              given x1 being Point of Y1 meet X0 such that
A38:          x1 = x;
              g|(Y1 meet X0) is continuous by A3,A4,A10,Th83;
              then g|(Y1 meet X0) is_continuous_at x1 by Th44;
              hence thesis by A9,A10,A11,A14,A33,A38,Th31,Th79;
            end;
            Y1 is SubSpace of Y1 union Y2 by TSEP_1:22;
            then Y1 union Y2 meets X0 by A34,Th18;
            then
A39:        (Y1 union Y2) meet X0 = X0 by A33,TSEP_1:28;
            Y2 meets X0 by A9,A10,A11,A33,Th31;
            then (Y1 meet X0) union (Y2 meet X0) = X0 by A34,A39,TSEP_1:32;
            hence thesis by A37,A35,Th11;
          end;
          hence thesis by A15;
        end;
        now
A40:      now
            assume X2 is SubSpace of X1;
            then
A41:        the TopStruct of X1 = X0 by TSEP_1:23;
            then reconsider x1 = x as Point of X1;
            g|X1 is_continuous_at x1 by A4,Th44;
            hence thesis by A41,Th81;
          end;
A42:      now
            assume X1 is SubSpace of X2;
            then
A43:        the TopStruct of X2 = X0 by TSEP_1:23;
            then reconsider x2 = x as Point of X2;
            g|X2 is_continuous_at x2 by A5,Th44;
            hence thesis by A43,Th81;
          end;
          assume X1 is SubSpace of X2 or X2 is SubSpace of X1;
          hence thesis by A42,A40;
        end;
        hence thesis by A8;
      end;
      X1 misses X2 implies g is_continuous_at x
      proof
        assume X1 misses X2;
        then X1,X2 are_separated by A1,TSEP_1:78;
        then consider Y1, Y2 being open non empty SubSpace of X such that
A44:    X1 is SubSpace of Y1 and
A45:    X2 is SubSpace of Y2 and
A46:    Y1 misses Y2 or Y1 meet Y2 misses X0 by TSEP_1:77;
        Y2 misses X1 by A44,A45,A46,Th30;
        then
A47:    X2 is open SubSpace of X0 by A45,Th41;
A48:    now
          given x2 being Point of X2 such that
A49:      x2 = x;
          g|X2 is_continuous_at x2 by A5,Th44;
          hence thesis by A47,A49,Th79;
        end;
        Y1 misses X2 by A44,A45,A46,Th30;
        then
A50:    X1 is open SubSpace of X0 by A44,Th41;
        now
          given x1 being Point of X1 such that
A51:      x1 = x;
          g|X1 is_continuous_at x1 by A4,Th44;
          hence thesis by A50,A51,Th79;
        end;
        hence thesis by A48,Th11;
      end;
      hence thesis by A6;
    end;
    hence thesis by Th44;
  end;
end;

theorem Th115:
  for X1, X2 being closed non empty SubSpace of X for g being
Function of X1 union X2,Y holds g is continuous Function of X1 union X2,Y iff g
  |X1 is continuous Function of X1,Y & g|X2 is continuous Function of X2,Y
proof
  let X1, X2 be closed non empty SubSpace of X;
  let g be Function of X1 union X2,Y;
  X1,X2 are_weakly_separated by TSEP_1:80;
  hence thesis by Th114;
end;

theorem Th116:
  for X1, X2 being open non empty SubSpace of X for g being
Function of X1 union X2,Y holds g is continuous Function of X1 union X2,Y iff g
  |X1 is continuous Function of X1,Y & g|X2 is continuous Function of X2,Y
proof
  let X1, X2 be open non empty SubSpace of X;
  let g be Function of X1 union X2,Y;
  X1,X2 are_weakly_separated by TSEP_1:81;
  hence thesis by Th114;
end;

theorem Th117:
  X1,X2 are_weakly_separated implies for f being Function of X,Y
  holds f|(X1 union X2) is continuous Function of X1 union X2,Y iff f|X1 is
  continuous Function of X1,Y & f|X2 is continuous Function of X2,Y
proof
  assume
A1: X1,X2 are_weakly_separated;
  let f be Function of X,Y;
A2: X2 is SubSpace of X1 union X2 by TSEP_1:22;
  then
A3: f|(X1 union X2)|X2 = f|X2 by Th71;
A4: X1 is SubSpace of X1 union X2 by TSEP_1:22;
  then
A5: f|(X1 union X2)|X1 = f|X1 by Th71;
  hence
  f|(X1 union X2) is continuous Function of X1 union X2,Y implies f|X1 is
  continuous Function of X1,Y & f|X2 is continuous Function of X2,Y by A4,A2,A3
,Th82;
  thus thesis by A1,A5,A3,Th114;
end;

theorem
  for f being Function of X,Y, X1, X2 being closed non empty SubSpace of
  X holds f|(X1 union X2) is continuous Function of X1 union X2,Y iff f|X1 is
  continuous Function of X1,Y & f|X2 is continuous Function of X2,Y
proof
  let f be Function of X,Y, X1, X2 be closed non empty SubSpace of X;
  X1,X2 are_weakly_separated by TSEP_1:80;
  hence thesis by Th117;
end;

theorem
  for f being Function of X,Y, X1, X2 being open non empty SubSpace of X
  holds f|(X1 union X2) is continuous Function of X1 union X2,Y iff f|X1 is
  continuous Function of X1,Y & f|X2 is continuous Function of X2,Y
proof
  let f be Function of X,Y, X1, X2 be open non empty SubSpace of X;
  X1,X2 are_weakly_separated by TSEP_1:81;
  hence thesis by Th117;
end;

theorem Th120:
  for f being Function of X,Y, X1, X2 being non empty SubSpace of
  X st X = X1 union X2 & X1,X2 are_weakly_separated holds f is continuous
  Function of X,Y iff f|X1 is continuous Function of X1,Y & f|X2 is continuous
  Function of X2,Y
proof
  let f be Function of X,Y, X1, X2 be non empty SubSpace of X such that
A1: X = X1 union X2 and
A2: X1,X2 are_weakly_separated;
  thus f is continuous Function of X,Y implies f|X1 is continuous Function of
  X1,Y & f|X2 is continuous Function of X2,Y;
  assume
  f|X1 is continuous Function of X1,Y & f|X2 is continuous Function of X2,Y;
  then f|(X1 union X2) is continuous Function of X1 union X2,Y by A2,Th117;
  hence thesis by A1,Th54;
end;

theorem Th121:
  for f being Function of X,Y, X1, X2 being closed non empty
SubSpace of X st X = X1 union X2 holds f is continuous Function of X,Y iff f|X1
  is continuous Function of X1,Y & f|X2 is continuous Function of X2,Y
proof
  let f be Function of X,Y, X1, X2 be closed non empty SubSpace of X such that
A1: X = X1 union X2;
  X1,X2 are_weakly_separated by TSEP_1:80;
  hence thesis by A1,Th120;
end;

theorem Th122:
  for f being Function of X,Y, X1, X2 being open non empty
SubSpace of X st X = X1 union X2 holds f is continuous Function of X,Y iff f|X1
  is continuous Function of X1,Y & f|X2 is continuous Function of X2,Y
proof
  let f be Function of X,Y, X1, X2 be open non empty SubSpace of X such that
A1: X = X1 union X2;
  X1,X2 are_weakly_separated by TSEP_1:81;
  hence thesis by A1,Th120;
end;

::Some Characterizations of Separated Subspaces of Topological Spaces.

theorem Th123:
  X1,X2 are_separated iff X1 misses X2 & for Y being non empty
  TopSpace, g being Function of X1 union X2,Y st g|X1 is continuous Function of
X1,Y & g|X2 is continuous Function of X2,Y holds g is continuous Function of X1
  union X2,Y
proof
  thus X1,X2 are_separated implies X1 misses X2 & for Y being non empty
  TopSpace, g being Function of X1 union X2,Y st g|X1 is continuous Function of
X1,Y & g|X2 is continuous Function of X2,Y holds g is continuous Function of X1
  union X2,Y
  proof
    assume
A1: X1,X2 are_separated;
    hence X1 misses X2 by TSEP_1:63;
    X1,X2 are_weakly_separated by A1,TSEP_1:78;
    hence thesis by Th114;
  end;
  thus X1 misses X2 & (for Y being non empty TopSpace, g being Function of X1
union X2,Y st g|X1 is continuous Function of X1,Y & g|X2 is continuous Function
  of X2,Y holds g is continuous Function of X1 union X2,Y) implies X1,X2
  are_separated
  proof
    reconsider Y1 = X1, Y2 = X2 as SubSpace of X1 union X2 by TSEP_1:22;
    reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;
    reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;
A2: the carrier of X1 union X2 = A1 \/ A2 by TSEP_1:def 2;
    then reconsider C1 = A1 as Subset of X1 union X2 by XBOOLE_1:7;
    reconsider C2 = A2 as Subset of X1 union X2 by A2,XBOOLE_1:7;
A3: Cl C1 = (Cl A1) /\ [#](X1 union X2) by PRE_TOPC:17;
A4: Cl C2 = (Cl A2) /\ [#](X1 union X2) by PRE_TOPC:17;
    assume X1 misses X2;
    then
A5: C1 misses C2 by TSEP_1:def 3;
    assume
A6: for Y being non empty TopSpace, g being Function of X1 union X2,Y
st g|X1 is continuous Function of X1,Y & g|X2 is continuous Function of X2,Y
    holds g is continuous Function of X1 union X2,Y;
    assume X1,X2 are_not_separated;
    then
A7: ex A10, A20 being Subset of X st A10 = the carrier of X1 & A20 = the
    carrier of X2 & A10,A20 are_not_separated by TSEP_1:def 6;
A8: now
      assume
A9:   C1,C2 are_separated;
      then ((Cl A1) /\ [#](X1 union X2)) misses A2 by A3,CONNSP_1:def 1;
      then ((Cl A1) /\ [#](X1 union X2)) /\ A2 = {} by XBOOLE_0:def 7;
      then
A10:  (Cl A1 /\ A2) /\ [#](X1 union X2) = {} by XBOOLE_1:16;
      A1 misses ((Cl A2) /\ [#](X1 union X2)) by A4,A9,CONNSP_1:def 1;
      then A1 /\ ((Cl A2) /\ [#](X1 union X2)) = {} by XBOOLE_0:def 7;
      then
A11:  (A1 /\ Cl A2) /\ [#](X1 union X2) = {} by XBOOLE_1:16;
      C1 c= [#](X1 union X2) & A1 /\ Cl A2 c= A1 by XBOOLE_1:17;
      then A1 /\ Cl A2 = {} by A11,XBOOLE_1:1,28;
      then
A12:  A1 misses Cl A2 by XBOOLE_0:def 7;
      C2 c= [#](X1 union X2) & Cl A1 /\ A2 c= A2 by XBOOLE_1:17;
      then Cl A1 /\ A2 = {} by A10,XBOOLE_1:1,28;
      then Cl A1 misses A2 by XBOOLE_0:def 7;
      hence contradiction by A7,A12,CONNSP_1:def 1;
    end;
    now
      per cases by A8,A5,TSEP_1:37;
      suppose
A13:    not C1 is open;
        set g = modid(X1 union X2,C1);
        set Y = (X1 union X2) modified_with_respect_to C1;
        g|Y1 = g|X1 by Def5;
        then
A14:    g|X1 is continuous Function of X1,Y by Th100;
        g|Y2 = g|X2 by Def5;
        then
A15:    g|X2 is continuous Function of X2,Y by A5,Th99;
        not g is continuous Function of X1 union X2,Y by A13,Th101;
        hence contradiction by A6,A14,A15;
      end;
      suppose
A16:    not C2 is open;
        set g = modid(X1 union X2,C2);
        set Y = (X1 union X2) modified_with_respect_to C2;
        g|Y2 = g|X2 by Def5;
        then
A17:    g|X2 is continuous Function of X2,Y by Th100;
        g|Y1 = g|X1 by Def5;
        then
A18:    g|X1 is continuous Function of X1,Y by A5,Th99;
        not g is continuous Function of X1 union X2,Y by A16,Th101;
        hence contradiction by A6,A18,A17;
      end;
    end;
    hence contradiction;
  end;
end;

theorem Th124:
  X1,X2 are_separated iff X1 misses X2 & for Y being non empty
TopSpace, f being Function of X,Y st f|X1 is continuous Function of X1,Y & f|X2
is continuous Function of X2,Y holds f|(X1 union X2) is continuous Function of
  X1 union X2,Y
proof
  thus X1,X2 are_separated implies X1 misses X2 & for Y being non empty
TopSpace, f being Function of X,Y st f|X1 is continuous Function of X1,Y & f|X2
is continuous Function of X2,Y holds f|(X1 union X2) is continuous Function of
  X1 union X2,Y
  proof
    assume
A1: X1,X2 are_separated;
    hence X1 misses X2 by TSEP_1:63;
    X1,X2 are_weakly_separated by A1,TSEP_1:78;
    hence thesis by Th117;
  end;
  thus X1 misses X2 & (for Y being non empty TopSpace, f being Function of X,Y
  st f|X1 is continuous Function of X1,Y & f|X2 is continuous Function of X2,Y
  holds f|(X1 union X2) is continuous Function of X1 union X2,Y) implies X1,X2
  are_separated
  proof
    assume
A2: X1 misses X2;
    assume
A3: for Y being non empty TopSpace, f being Function of X,Y st f|X1 is
continuous Function of X1,Y & f|X2 is continuous Function of X2,Y holds f|(X1
    union X2) is continuous Function of X1 union X2,Y;
    for Y being non empty TopSpace, g being Function of X1 union X2,Y st g
|X1 is continuous Function of X1,Y & g|X2 is continuous Function of X2,Y holds
    g is continuous Function of X1 union X2,Y
    proof
      let Y be non empty TopSpace, g be Function of X1 union X2,Y such that
A4:   g|X1 is continuous Function of X1,Y and
A5:   g|X2 is continuous Function of X2,Y;
      consider h being Function of X,Y such that
A6:   h|(X1 union X2) = g by Th57;
      X2 is SubSpace of X1 union X2 by TSEP_1:22;
      then
A7:   h|X2 is continuous Function of X2,Y by A5,A6,Th70;
      X1 is SubSpace of X1 union X2 by TSEP_1:22;
      then h|X1 is continuous Function of X1,Y by A4,A6,Th70;
      hence thesis by A3,A6,A7;
    end;
    hence thesis by A2,Th123;
  end;
end;

theorem
  for X1, X2 being non empty SubSpace of X st X = X1 union X2 holds X1,
  X2 are_separated iff X1 misses X2 & for Y being non empty TopSpace, f being
  Function of X,Y st f|X1 is continuous Function of X1,Y & f|X2 is continuous
  Function of X2,Y holds f is continuous Function of X,Y
proof
  let X1, X2 be non empty SubSpace of X such that
A1: X = X1 union X2;
  thus X1,X2 are_separated implies X1 misses X2 & for Y being non empty
TopSpace, f being Function of X,Y st f|X1 is continuous Function of X1,Y & f|X2
  is continuous Function of X2,Y holds f is continuous Function of X,Y
  proof
    assume
A2: X1,X2 are_separated;
    hence X1 misses X2 by TSEP_1:63;
    X1,X2 are_weakly_separated by A2,TSEP_1:78;
    hence thesis by A1,Th120;
  end;
  thus X1 misses X2 & (for Y being non empty TopSpace, f being Function of X,Y
  st f|X1 is continuous Function of X1,Y & f|X2 is continuous Function of X2,Y
  holds f is continuous Function of X,Y) implies X1,X2 are_separated
  proof
    assume
A3: X1 misses X2;
    assume
A4: for Y being non empty TopSpace, f being Function of X,Y st f|X1 is
continuous Function of X1,Y & f|X2 is continuous Function of X2,Y holds f is
    continuous Function of X,Y;
    for Y being non empty TopSpace, f being Function of X,Y st f|X1 is
continuous Function of X1,Y & f|X2 is continuous Function of X2,Y holds f|(X1
    union X2) is continuous Function of X1 union X2,Y
    proof
      let Y be non empty TopSpace, f be Function of X,Y;
      assume f|X1 is continuous Function of X1,Y & f|X2 is continuous
      Function of X2,Y;
      then f is continuous Function of X,Y by A4;
      hence thesis;
    end;
    hence thesis by A3,Th124;
  end;
end;

begin :: 6. The Union of Continuous Mappings.

definition
  let X,Y be non empty TopSpace, X1, X2 be non empty SubSpace of X;
  let f1 be Function of X1,Y, f2 be Function of X2,Y;
  assume
A1: X1 misses X2 or f1|(X1 meet X2) = f2|(X1 meet X2);
  func f1 union f2 -> Function of X1 union X2,Y means
  :Def12:
  it|X1 = f1 & it| X2 = f2;
  existence
  proof
    set B = the carrier of Y;
    set A = the carrier of X1 union X2;
    set A2 = the carrier of X2;
    set A1 = the carrier of X1;
A2: X1 is SubSpace of X1 union X2 & X2 is SubSpace of X1 union X2 by TSEP_1:22;
A3: A = A1 \/ A2 by TSEP_1:def 2;
A4: A1 meets A2 implies f1|(A1 /\ A2) = f2|(A1 /\ A2)
    proof
      assume
A5:   A1 meets A2;
      then
A6:   X1 meets X2 by TSEP_1:def 3;
      then
A7:   X1 meet X2 is SubSpace of X1 by TSEP_1:27;
A8:   X1 meet X2 is SubSpace of X2 by A6,TSEP_1:27;
      thus f1|(A1 /\ A2) = f1|(the carrier of X1 meet X2) by A6,TSEP_1:def 4
        .= f2|(X1 meet X2) by A1,A5,A7,Def5,TSEP_1:def 3
        .= f2|(the carrier of X1 meet X2) by A8,Def5
        .= f2|(A1 /\ A2) by A6,TSEP_1:def 4;
    end;
    reconsider A1, A2 as non empty Subset of A by A3,XBOOLE_1:7;
    reconsider g1 = f1 as Function of A1,B;
    reconsider g2 = f2 as Function of A2,B;
    set G = g1 union g2;
    the carrier of X1 union X2 = (the carrier of X1) \/ (the carrier of
    X2 ) by TSEP_1:def 2;
    then reconsider F = G as Function of X1 union X2,Y;
    take F;
    G|A1 = f1 & G|A2 = f2 by A4,Def1,Th1;
    hence thesis by A2,Def5;
  end;
  uniqueness
  proof
    set A = the carrier of X1 union X2;
A9: X2 is SubSpace of X1 union X2 by TSEP_1:22;
    set A2 = the carrier of X2;
A10: X1 is SubSpace of X1 union X2 by TSEP_1:22;
    set A1 = the carrier of X1;
    let F be Function of X1 union X2,Y, G be Function of X1 union X2,Y such
    that
A11: F|X1 = f1 and
A12: F|X2 = f2 and
A13: G|X1 = f1 and
A14: G|X2 = f2;
A15: A = A1 \/ A2 by TSEP_1:def 2;
    now
      let a be Element of A;
A16:  now
        assume
A17:    a in A2;
        hence F.a = (F|A2).a by FUNCT_1:49
          .= f2.a by A12,A9,Def5
          .= (G|A2).a by A14,A9,Def5
          .= G.a by A17,FUNCT_1:49;
      end;
      now
        assume
A18:    a in A1;
        hence F.a = (F|A1).a by FUNCT_1:49
          .= f1.a by A11,A10,Def5
          .= (G|A1).a by A13,A10,Def5
          .= G.a by A18,FUNCT_1:49;
      end;
      hence F.a = G.a by A15,A16,XBOOLE_0:def 3;
    end;
    hence thesis by FUNCT_2:63;
  end;
end;

reserve X, Y for non empty TopSpace;

theorem Th126:
  for X1, X2 being non empty SubSpace of X for g being Function
  of X1 union X2,Y holds g = (g|X1) union (g|X2)
proof
  let X1, X2 be non empty SubSpace of X;
  let g be Function of X1 union X2,Y;
  now
    assume
A1: X1 meets X2;
    then
A2: X1 meet X2 is SubSpace of X2 by TSEP_1:27;
A3: X2 is SubSpace of X1 union X2 by TSEP_1:22;
A4: X1 is SubSpace of X1 union X2 by TSEP_1:22;
    X1 meet X2 is SubSpace of X1 by A1,TSEP_1:27;
    hence (g|X1)|(X1 meet X2) = g|(X1 meet X2) by A4,Th72
      .= (g|X2)|(X1 meet X2) by A2,A3,Th72;
  end;
  hence thesis by Def12;
end;

theorem
  for X1, X2 being non empty SubSpace of X st X = X1 union X2 for g
  being Function of X,Y holds g = (g|X1) union (g|X2)
proof
  let X1, X2 be non empty SubSpace of X such that
A1: X = X1 union X2;
  let g be Function of X,Y;
  reconsider h = g as Function of X1 union X2,Y by A1;
  X2 is SubSpace of X1 union X2 by TSEP_1:22;
  then
A2: h|X2 = g|X2 by Def5;
  X1 is SubSpace of X1 union X2 by TSEP_1:22;
  then h|X1 = g|X1 by Def5;
  hence thesis by A2,Th126;
end;

theorem Th128:
  for X1, X2 being non empty SubSpace of X st X1 meets X2 for f1
being Function of X1,Y, f2 being Function of X2,Y holds (f1 union f2)|X1 = f1 &
  (f1 union f2)|X2 = f2 iff f1|(X1 meet X2) = f2|(X1 meet X2)
proof
  let X1, X2 be non empty SubSpace of X such that
A1: X1 meets X2;
  let f1 be Function of X1,Y, f2 be Function of X2,Y;
  thus (f1 union f2)|X1 = f1 & (f1 union f2)|X2 = f2 implies f1|(X1 meet X2) =
  f2|(X1 meet X2)
  proof
A2: X1 meet X2 is SubSpace of X2 & X2 is SubSpace of X1 union X2 by A1,
TSEP_1:22,27;
    assume that
A3: (f1 union f2)|X1 = f1 and
A4: (f1 union f2)|X2 = f2;
    X1 meet X2 is SubSpace of X1 & X1 is SubSpace of X1 union X2 by A1,
TSEP_1:22,27;
    then (f1 union f2)|(X1 meet X2) = f1|(X1 meet X2) by A3,Th72;
    hence thesis by A2,A4,Th72;
  end;
  thus thesis by Def12;
end;

theorem
  for X1, X2 being non empty SubSpace of X, f1 being Function of X1,Y,
  f2 being Function of X2,Y st f1|(X1 meet X2) = f2|(X1 meet X2) holds (X1 is
SubSpace of X2 iff f1 union f2 = f2) & (X2 is SubSpace of X1 iff f1 union f2 =
  f1)
proof
  let X1, X2 be non empty SubSpace of X, f1 be Function of X1,Y, f2 be
  Function of X2,Y;
  reconsider Y1 = X1, Y2 = X2, Y3 = X1 union X2 as SubSpace of X1 union X2 by
TSEP_1:2,22;
  assume
A1: f1|(X1 meet X2) = f2|(X1 meet X2);
A2: now
    assume X1 is SubSpace of X2;
    then
A3: the TopStruct of X2 = X1 union X2 by TSEP_1:23;
    (f1 union f2)|X2 = f2 by A1,Def12;
    then (f1 union f2)|the carrier of Y2 = f2 by Def5;
    then (f1 union f2)|the carrier of Y3 = f2 by A3;
    then (f1 union f2)|(X1 union X2) = f2 by Def5;
    hence f1 union f2 = f2 by Th67;
  end;
A4: now
    assume X2 is SubSpace of X1;
    then
A5: the TopStruct of X1 = X1 union X2 by TSEP_1:23;
    (f1 union f2)|X1 = f1 by A1,Def12;
    then (f1 union f2)|the carrier of Y1 = f1 by Def5;
    then (f1 union f2)|the carrier of Y3 = f1 by A5;
    then (f1 union f2)|(X1 union X2) = f1 by Def5;
    hence f1 union f2 = f1 by Th67;
  end;
  now
A6: dom (f1 union f2) = the carrier of X1 union X2 & dom f2 = the carrier
    of X2 by FUNCT_2:def 1;
    assume f1 union f2 = f2;
    then X1 union X2 = the TopStruct of X2 by A6,TSEP_1:5;
    hence X1 is SubSpace of X2 by TSEP_1:23;
  end;
  hence X1 is SubSpace of X2 iff f1 union f2 = f2 by A2;
  now
A7: dom (f1 union f2) = the carrier of X1 union X2 & dom f1 = the carrier
    of X1 by FUNCT_2:def 1;
    assume f1 union f2 = f1;
    then X1 union X2 = the TopStruct of X1 by A7,TSEP_1:5;
    hence X2 is SubSpace of X1 by TSEP_1:23;
  end;
  hence X2 is SubSpace of X1 iff f1 union f2 = f1 by A4;
end;

theorem
  for X1, X2 being non empty SubSpace of X, f1 being Function of X1,Y,
f2 being Function of X2,Y st X1 misses X2 or f1|(X1 meet X2) = f2|(X1 meet X2)
  holds f1 union f2 = f2 union f1
proof
  let X1, X2 be non empty SubSpace of X, f1 be Function of X1,Y, f2 be
  Function of X2,Y;
  assume X1 misses X2 or f1|(X1 meet X2) = f2|(X1 meet X2);
  then (f1 union f2)|X1 = f1 & (f1 union f2)|X2 = f2 by Def12;
  hence thesis by Th126;
end;

theorem
  for X1, X2, X3 being non empty SubSpace of X, f1 being Function of X1,
Y, f2 being Function of X2,Y, f3 being Function of X3,Y st (X1 misses X2 or f1|
  (X1 meet X2) = f2|(X1 meet X2)) & (X1 misses X3 or f1|(X1 meet X3) = f3|(X1
meet X3)) & (X2 misses X3 or f2|(X2 meet X3) = f3|(X2 meet X3)) holds (f1 union
  f2) union f3 = f1 union (f2 union f3)
proof
  let X1, X2, X3 be non empty SubSpace of X, f1 be Function of X1,Y, f2 be
  Function of X2,Y, f3 be Function of X3,Y such that
A1: X1 misses X2 or f1|(X1 meet X2) = f2|(X1 meet X2) and
A2: X1 misses X3 or f1|(X1 meet X3) = f3|(X1 meet X3) and
A3: X2 misses X3 or f2|(X2 meet X3) = f3|(X2 meet X3);
  set g = (f1 union f2) union f3;
A4: (X1 union X2) union X3 = X1 union (X2 union X3) by TSEP_1:21;
  then reconsider f = g as Function of X1 union (X2 union X3),Y;
A5: X1 union X2 is SubSpace of X1 union (X2 union X3) by A4,TSEP_1:22;
A6: now
    assume
A7: (X1 union X2) meets X3;
    now
      per cases by A7,Th34;
      suppose
A8:     X1 meets X3 & not X2 meets X3;
        then
A9:     (X1 union X2) meet X3 = X1 meet X3 by Th26;
A10:    X1 is SubSpace of X1 union X2 by TSEP_1:22;
        X1 meet X3 is SubSpace of X1 by A8,TSEP_1:27;
        then (f1 union f2)|(X1 meet X3) = ((f1 union f2)|X1)|(X1 meet X3) by
A10,Th72
          .= f1|(X1 meet X3) by A1,Def12;
        hence
        (f1 union f2)|((X1 union X2) meet X3) = f3|((X1 union X2) meet X3
        ) by A2,A8,A9;
      end;
      suppose
A11:    not X1 meets X3 & X2 meets X3;
        then
A12:    (X1 union X2) meet X3 = X2 meet X3 by Th26;
A13:    X2 is SubSpace of X1 union X2 by TSEP_1:22;
        X2 meet X3 is SubSpace of X2 by A11,TSEP_1:27;
        then (f1 union f2)|(X2 meet X3) = ((f1 union f2)|X2)|(X2 meet X3) by
A13,Th72
          .= f2|(X2 meet X3) by A1,Def12;
        hence
        (f1 union f2)|((X1 union X2) meet X3) = f3|((X1 union X2) meet X3
        ) by A3,A11,A12;
      end;
      suppose
A14:    X1 meets X3 & X2 meets X3;
        then X1 meet X3 is SubSpace of X3 & X2 meet X3 is SubSpace of X3 by
TSEP_1:27;
        then
A15:    (X1 meet X3) union (X2 meet X3) is SubSpace of X3 by Th24;
A16:    X2 meet X3 is SubSpace of X2 by A14,TSEP_1:27;
A17:    X1 meet X3 is SubSpace of (X1 meet X3) union (X2 meet X3) by TSEP_1:22;
        then
A18:    (f3|((X1 meet X3) union (X2 meet X3)))|(X1 meet X3) = f3|(X1 meet
        X3) by A15,Th72;
A19:    X1 meet X3 is SubSpace of X1 by A14,TSEP_1:27;
        then
A20:    (X1 meet X3) union (X2 meet X3) is SubSpace of X1 union X2 by A16,Th22;
        then
A21:    ((f1 union f2)|((X1 meet X3) union (X2 meet X3)))|(X1 meet X3) =
        (f1 union f2)|(X1 meet X3) by A17,Th72;
        X2 is SubSpace of X1 union X2 by TSEP_1:22;
        then
A22:    (f1 union f2)|(X2 meet X3) = ((f1 union f2)|X2)|(X2 meet X3) by A16
,Th72
          .= f2|(X2 meet X3) by A1,Def12;
        set v = f3|((X1 meet X3) union (X2 meet X3));
A23:    X2 meet X3 is SubSpace of (X1 meet X3) union (X2 meet X3) by TSEP_1:22;
        then
A24:    (f3|((X1 meet X3) union (X2 meet X3)))|(X2 meet X3) = f3|(X2 meet
        X3) by A15,Th72;
        X1 is SubSpace of X1 union X2 by TSEP_1:22;
        then
A25:    (f1 union f2)|(X1 meet X3) = ((f1 union f2)|X1)|(X1 meet X3) by A19
,Th72
          .= f1|(X1 meet X3) by A1,Def12;
A26:    ((f1 union f2)|((X1 meet X3) union (X2 meet X3)))|(X2 meet X3) =
        (f1 union f2)|(X2 meet X3) by A20,A23,Th72;
        (f1 union f2)|((X1 union X2) meet X3) = ((f1 union f2)|((X1 meet
        X3) union (X2 meet X3))) by A14,TSEP_1:32
          .= (v|(X1 meet X3)) union (v|(X2 meet X3)) by A2,A3,A14,A25,A22,A21
,A26,A18,A24,Th126
          .= v by Th126;
        hence
        (f1 union f2)|((X1 union X2) meet X3) = f3|((X1 union X2) meet X3
        ) by A14,TSEP_1:32;
      end;
    end;
    hence (f1 union f2)|((X1 union X2) meet X3) = f3|((X1 union X2) meet X3);
  end;
  then X1 union X2 is SubSpace of (X1 union X2) union X3 & g|(X1 union X2) =
  f1 union f2 by Def12,TSEP_1:22;
  then
A27: f|(the carrier of (X1 union X2)) = f1 union f2 by Def5;
A28: X3 is SubSpace of X1 union (X2 union X3) by A4,TSEP_1:22;
A29: X2 union X3 is SubSpace of X1 union (X2 union X3) by TSEP_1:22;
  X3 is SubSpace of (X1 union X2) union X3 & g|X3 = f3 by A6,Def12,TSEP_1:22;
  then
A30: f|(the carrier of X3) = f3 by Def5;
A31: X1 union X2 is SubSpace of X1 union (X2 union X3) by A4,TSEP_1:22;
  X3 is SubSpace of X2 union X3 by TSEP_1:22;
  then
A32: (f|(X2 union X3))|X3 = f|X3 by A29,Th72
    .= f3 by A28,A30,Def5;
  X2 is SubSpace of X1 union X2 by TSEP_1:22;
  then
A33: f|X2 = (f|(X1 union X2))|X2 by A31,Th72
    .= (f1 union f2)|X2 by A5,A27,Def5;
  X2 is SubSpace of X2 union X3 by TSEP_1:22;
  then (f|(X2 union X3))|X2 = f|X2 by A29,Th72
    .= f2 by A1,A33,Def12;
  then
A34: f|(X2 union X3) = f2 union f3 by A32,Th126;
  X1 is SubSpace of X1 union X2 by TSEP_1:22;
  then f|X1 = (f|(X1 union X2))|X1 by A31,Th72
    .= (f1 union f2)|X1 by A5,A27,Def5;
  then f|X1 = f1 by A1,Def12;
  hence thesis by A34,Th126;
end;

::Continuity of the Union of Continuous Mappings.
::(Theorems presented below are suitable also in the case X = X1 union X2.)

theorem
  for X1, X2 being non empty SubSpace of X st X1 meets X2 for f1 being
  continuous Function of X1,Y, f2 being continuous Function of X2,Y st f1|(X1
meet X2) = f2|(X1 meet X2) holds X1,X2 are_weakly_separated implies f1 union f2
  is continuous Function of X1 union X2,Y
proof
  let X1, X2 be non empty SubSpace of X such that
A1: X1 meets X2;
  let f1 be continuous Function of X1,Y, f2 be continuous Function of X2,Y;
  assume f1|(X1 meet X2) = f2|(X1 meet X2);
  then
A2: (f1 union f2)|X1 = f1 & (f1 union f2)|X2 = f2 by A1,Th128;
  assume X1,X2 are_weakly_separated;
  hence thesis by A2,Th114;
end;

theorem Th133:
  for X1, X2 being non empty SubSpace of X st X1 misses X2 for f1
  being continuous Function of X1,Y, f2 being continuous Function of X2,Y holds
  X1,X2 are_weakly_separated implies f1 union f2 is continuous Function of X1
  union X2,Y
proof
  let X1, X2 be non empty SubSpace of X such that
A1: X1 misses X2;
  let f1 be continuous Function of X1,Y, f2 be continuous Function of X2,Y;
  assume
A2: X1,X2 are_weakly_separated;
  (f1 union f2)|X1 = f1 & (f1 union f2)|X2 = f2 by A1,Def12;
  hence thesis by A2,Th114;
end;

theorem
  for X1, X2 being closed non empty SubSpace of X st X1 meets X2 for f1
being continuous Function of X1,Y, f2 being continuous Function of X2,Y st f1|(
  X1 meet X2) = f2|(X1 meet X2) holds f1 union f2 is continuous Function of X1
  union X2,Y
proof
  let X1, X2 be closed non empty SubSpace of X such that
A1: X1 meets X2;
  let f1 be continuous Function of X1,Y, f2 be continuous Function of X2,Y;
  assume f1|(X1 meet X2) = f2|(X1 meet X2);
  then (f1 union f2)|X1 = f1 & (f1 union f2)|X2 = f2 by A1,Th128;
  hence thesis by Th115;
end;

theorem
  for X1, X2 being open non empty SubSpace of X st X1 meets X2 for f1
being continuous Function of X1,Y, f2 being continuous Function of X2,Y st f1|(
  X1 meet X2) = f2|(X1 meet X2) holds f1 union f2 is continuous Function of X1
  union X2,Y
proof
  let X1, X2 be open non empty SubSpace of X such that
A1: X1 meets X2;
  let f1 be continuous Function of X1,Y, f2 be continuous Function of X2,Y;
  assume f1|(X1 meet X2) = f2|(X1 meet X2);
  then (f1 union f2)|X1 = f1 & (f1 union f2)|X2 = f2 by A1,Th128;
  hence thesis by Th116;
end;

theorem
  for X1, X2 being closed non empty SubSpace of X st X1 misses X2 for f1
  being continuous Function of X1,Y, f2 being continuous Function of X2,Y holds
  f1 union f2 is continuous Function of X1 union X2,Y
proof
  let X1, X2 be closed non empty SubSpace of X such that
A1: X1 misses X2;
  let f1 be continuous Function of X1,Y, f2 be continuous Function of X2,Y;
  (f1 union f2)|X1 = f1 & (f1 union f2)|X2 = f2 by A1,Def12;
  hence thesis by Th115;
end;

theorem
  for X1, X2 being open non empty SubSpace of X st X1 misses X2 for f1
  being continuous Function of X1,Y, f2 being continuous Function of X2,Y holds
  f1 union f2 is continuous Function of X1 union X2,Y
proof
  let X1, X2 be open non empty SubSpace of X such that
A1: X1 misses X2;
  let f1 be continuous Function of X1,Y, f2 be continuous Function of X2,Y;
  (f1 union f2)|X1 = f1 & (f1 union f2)|X2 = f2 by A1,Def12;
  hence thesis by Th116;
end;

::A Characterization of Separated Subspaces by means of Continuity of the Union
::of Continuous continuous mappings defined on the Subspaces.

theorem
  for X1, X2 being non empty SubSpace of X holds X1,X2 are_separated iff
X1 misses X2 & for Y being non empty TopSpace, f1 being continuous Function of
  X1,Y, f2 being continuous Function of X2,Y holds f1 union f2 is continuous
  Function of X1 union X2,Y
proof
  let X1, X2 be non empty SubSpace of X;
  thus X1,X2 are_separated implies X1 misses X2 & for Y being non empty
TopSpace, f1 being continuous Function of X1,Y, f2 being continuous Function of
  X2,Y holds f1 union f2 is continuous Function of X1 union X2,Y
  proof
    assume
A1: X1,X2 are_separated;
    hence X1 misses X2 by TSEP_1:63;
    X1,X2 are_weakly_separated by A1,TSEP_1:78;
    hence thesis by A1,Th133,TSEP_1:63;
  end;
  thus X1 misses X2 & (for Y being non empty TopSpace, f1 being continuous
  Function of X1,Y, f2 being continuous Function of X2,Y holds f1 union f2 is
  continuous Function of X1 union X2,Y) implies X1,X2 are_separated
  proof
    assume
A2: X1 misses X2;
    assume
A3: for Y being non empty TopSpace, f1 being continuous Function of X1
    ,Y, f2 being continuous Function of X2,Y holds f1 union f2 is continuous
    Function of X1 union X2,Y;
    now
      let Y be non empty TopSpace, g be Function of X1 union X2,Y;
      assume that
A4:   g|X1 is continuous Function of X1,Y and
A5:   g|X2 is continuous Function of X2,Y;
      reconsider f2 = g|X2 as continuous Function of X2,Y by A5;
      reconsider f1 = g|X1 as continuous Function of X1,Y by A4;
      g = f1 union f2 by Th126;
      hence g is continuous Function of X1 union X2,Y by A3;
    end;
    hence thesis by A2,Th123;
  end;
end;

::Continuity of the Union of Continuous Mappings (a special case).

theorem
  for X1, X2 being non empty SubSpace of X st X = X1 union X2 for f1
being continuous Function of X1,Y, f2 being continuous Function of X2,Y st (f1
  union f2)|X1 = f1 & (f1 union f2)|X2 = f2 holds X1,X2 are_weakly_separated
  implies f1 union f2 is continuous Function of X,Y
proof
  let X1, X2 be non empty SubSpace of X such that
A1: X = X1 union X2;
  let f1 be continuous Function of X1,Y, f2 be continuous Function of X2,Y
  such that
A2: (f1 union f2)|X1 = f1 & (f1 union f2)|X2 = f2;
  reconsider g = f1 union f2 as Function of X,Y by A1;
  assume
A3: X1,X2 are_weakly_separated;
  g|X1 = f1 & g|X2 = f2 by A1,A2,Def5;
  hence thesis by A1,A3,Th120;
end;

theorem
  for X1, X2 being closed non empty SubSpace of X, f1 being continuous
Function of X1,Y, f2 being continuous Function of X2,Y st X = X1 union X2 & (f1
  union f2)|X1 = f1 & (f1 union f2)|X2 = f2 holds f1 union f2 is continuous
  Function of X,Y
proof
  let X1, X2 be closed non empty SubSpace of X, f1 be continuous Function of
  X1,Y, f2 be continuous Function of X2,Y such that
A1: X = X1 union X2 and
A2: (f1 union f2)|X1 = f1 & (f1 union f2)|X2 = f2;
  reconsider g = f1 union f2 as Function of X,Y by A1;
  g|X1 = f1 & g|X2 = f2 by A1,A2,Def5;
  hence thesis by A1,Th121;
end;

theorem
  for X1, X2 being open non empty SubSpace of X, f1 being continuous
Function of X1,Y, f2 being continuous Function of X2,Y st X = X1 union X2 & (f1
  union f2)|X1 = f1 & (f1 union f2)|X2 = f2 holds f1 union f2 is continuous
  Function of X,Y
proof
  let X1, X2 be open non empty SubSpace of X, f1 be continuous Function of X1,
  Y, f2 be continuous Function of X2,Y such that
A1: X = X1 union X2 and
A2: (f1 union f2)|X1 = f1 & (f1 union f2)|X2 = f2;
  reconsider g = f1 union f2 as Function of X,Y by A1;
  g|X1 = f1 & g|X2 = f2 by A1,A2,Def5;
  hence thesis by A1,Th122;
end;