:: Some Properties of Isomorphism between Relational Structures. On
:: the Product of Topological Spaces
::  by Jaros{\l}aw Gryko and Artur Korni{\l}owicz
::
:: Received June 22, 1999
:: Copyright (c) 1999-2019 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 ZFMISC_1, CARD_1, SUBSET_1, RELAT_1, FUNCT_1, XBOOLE_0, STRUCT_0,
      RELAT_2, ORDERS_2, WAYBEL_0, FUNCOP_1, MONOID_0, YELLOW_6, XXREAL_0,
      SEQM_3, PRE_TOPC, WAYBEL_9, WAYBEL24, CAT_1, YELLOW_0, NEWTON, CARD_3,
      FUNCT_2, VALUED_1, WELLORD1, LATTICE3, XXREAL_2, LATTICES, TARSKI,
      T_0TOPSP, TOPS_2, ORDINAL2, WAYBEL11, RCOMP_1, CARD_FIL, YELLOW_8,
      SETFAM_1, FINSET_1, WAYBEL_3, TOPS_1, WAYBEL18, PBOOLE, RLVECT_2,
      FUNCT_4, CANTOR_1, WAYBEL_1, FUNCT_3, GROUP_6;
 notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FINSET_1, TOPS_2, FUNCT_1,
      PBOOLE, RELSET_1, PARTFUN1, FUNCT_4, FUNCOP_1, ORDINAL1, NUMBERS,
      FUNCT_7, CARD_3, MONOID_0, SETFAM_1, FUNCT_2, DOMAIN_1, STRUCT_0,
      PRALG_1, PRE_TOPC, TOPS_1, COMPTS_1, T_0TOPSP, CANTOR_1, TMAP_1,
      ORDERS_2, LATTICE3, WAYBEL18, YELLOW_0, WAYBEL_0, WAYBEL_1, YELLOW_1,
      YELLOW_2, WAYBEL_3, YELLOW_6, YELLOW_8, WAYBEL_9, WAYBEL11, WAYBEL24;
 constructors FINSUB_1, REALSET1, FUNCT_7, TOPS_1, TOPS_2, LATTICE3, TMAP_1,
      T_0TOPSP, CANTOR_1, MONOID_0, ORDERS_3, WAYBEL_1, YELLOW_8, WAYBEL11,
      WAYBEL18, WAYBEL24, COMPTS_1, RELSET_1;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1,
      STRUCT_0, PRE_TOPC, TOPS_1, YELLOW_0, TEX_4, MONOID_0, WAYBEL_0,
      YELLOW_1, YELLOW_6, YELLOW_8, WAYBEL18, WAYBEL19, TOPGRP_1, BORSUK_3,
      WAYBEL24, RELSET_1, FINSET_1;
 requirements SUBSET, BOOLE;
 definitions TARSKI, MONOID_0, STRUCT_0, PRE_TOPC, TOPS_2, COMPTS_1, T_0TOPSP,
      LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_1, WAYBEL_3, YELLOW_8, FUNCT_2,
      XBOOLE_0, FUNCOP_1;
 equalities ORDINAL1, STRUCT_0, FUNCOP_1;
 expansions TARSKI, PRE_TOPC, TOPS_2, T_0TOPSP, WAYBEL_0, FUNCT_2, XBOOLE_0;
 theorems TARSKI, PRE_TOPC, ZFMISC_1, FUNCT_1, FUNCT_2, FUNCT_7, PRALG_1,
      FUNCOP_1, CARD_3, BORSUK_1, TOPS_2, TOPS_3, YELLOW_0, YELLOW_1, YELLOW_2,
      YELLOW_9, YELLOW12, WAYBEL_0, WAYBEL_1, WAYBEL_9, WAYBEL11, WAYBEL10,
      WAYBEL13, WAYBEL18, WAYBEL24, YELLOW_8, TMAP_1, TSP_1, FUNCT_4, URYSOHN1,
      XBOOLE_0, XBOOLE_1, SETFAM_1, CARD_1, PARTFUN1, RELSET_1;

begin  :: Preliminaries

theorem
  bool {0} = {0,1} by CARD_1:49,ZFMISC_1:24;

theorem Th2:
  for X being set, Y being Subset of X holds rng ((id X)|Y) = Y
proof
  let X be set, Y be Subset of X;
  set f = id X;
A1: f|Y is Function of Y,X by FUNCT_2:32;
  hereby
    let y be object;
    assume y in rng (f|Y);
    then consider x being object such that
A2: x in dom (f|Y) and
A3: y = (f|Y).x by FUNCT_1:def 3;
    (f|Y).x = f.x by A2,FUNCT_1:47
      .= x by A2,FUNCT_1:17;
    hence y in Y by A1,A2,A3,FUNCT_2:def 1;
  end;
  let y be object;
  X = {} implies Y = {};
  then
A4: dom (f|Y) = Y by A1,FUNCT_2:def 1;
  assume
A5: y in Y;
  then (f|Y).y = f.y by FUNCT_1:49
    .= y by A5,FUNCT_1:18;
  hence thesis by A4,A5,FUNCT_1:def 3;
end;

theorem
  for S being empty 1-sorted, T being 1-sorted, f being Function of S, T
  st rng f = [#]T holds T is empty;

theorem
  for S being 1-sorted, T being empty 1-sorted, f being Function of S, T
  st dom f = [#]S holds S is empty;

theorem
  for S being non empty 1-sorted, T being 1-sorted, f being Function of
  S, T st dom f = [#]S holds T is non empty;

theorem
  for S being 1-sorted, T being non empty 1-sorted, f being Function of
  S, T st rng f = [#]T holds S is non empty;

definition
  let S be non empty reflexive RelStr, T be non empty RelStr, f be Function of
  S, T;
  redefine attr f is directed-sups-preserving means
  for X being non empty directed Subset of S holds f preserves_sup_of X;
  compatibility;
end;

definition
  let R be 1-sorted, N be NetStr over R;
  attr N is Function-yielding means
  :Def2:
  the mapping of N is Function-yielding;
end;

registration
  cluster non empty constituted-Functions for 1-sorted;
  existence
  proof
    take A = 1-sorted (#{{}}#);
    thus the carrier of A is non empty;
    let a be Element of A;
    thus thesis;
  end;
end;

registration
  cluster strict non empty constituted-Functions for RelStr;
  existence
  proof
    take A = RelStr (#{{}}, id {{}}#);
    thus A is strict non empty;
    let a be Element of A;
    thus thesis;
  end;
end;

registration
  let R be constituted-Functions 1-sorted;
  cluster -> Function-yielding for NetStr over R;
  coherence
  proof
    let N be NetStr over R;
    let x be object;
    assume x in dom the mapping of N;
    then (the mapping of N).x in rng the mapping of N by FUNCT_1:def 3;
    hence thesis;
  end;
end;

registration
  let R be constituted-Functions 1-sorted;
  cluster strict Function-yielding for NetStr over R;
  existence
  proof
    take A = NetStr (#the carrier of R, id the carrier of R, id the carrier of
      R#);
    thus A is strict;
    let x be object;
    assume x in dom the mapping of A;
    hence thesis by FUNCT_1:18;
  end;
end;

registration
  let R be non empty constituted-Functions 1-sorted;
  cluster strict non empty Function-yielding for NetStr over R;
  existence
  proof
    take A = NetStr (#the carrier of R, id the carrier of R, id the carrier of
      R#);
    thus A is strict non empty;
    let x be object;
    assume x in dom the mapping of A;
    hence thesis by FUNCT_1:18;
  end;
end;

registration
  let R be constituted-Functions 1-sorted, N be Function-yielding NetStr over
  R;
  cluster the mapping of N -> Function-yielding;
  coherence by Def2;
end;

registration
  let R be non empty constituted-Functions 1-sorted;
  cluster strict Function-yielding for net of R;
  existence
  proof
    set p = the Element of R;
    set N = the net of R;
    take ConstantNet(N,p);
    thus thesis;
  end;
end;

registration
  let S be non empty 1-sorted, N be non empty NetStr over S;
  cluster rng the mapping of N -> non empty;
  coherence;
end;

registration
  let S be non empty 1-sorted, N be non empty NetStr over S;
  cluster rng netmap (N,S) -> non empty;
  coherence;
end;

theorem
  for A, B, C being non empty RelStr, f being Function of B, C, g, h
  being Function of A, B st g <= h & f is monotone holds f * g <= f * h
proof
  let A, B, C be non empty RelStr, f be Function of B, C, g, h be Function of
  A, B such that
A1: g <= h and
A2: for x, y being Element of B st x <= y holds f.x <= f.y;
  for x being Element of A holds (f*g).x <= (f*h).x
  proof
    let x be Element of A;
A3: (f*g).x = f.(g.x) & (f*h).x = f.(h.x) by FUNCT_2:15;
    g.x <= h.x by A1,YELLOW_2:9;
    hence thesis by A2,A3;
  end;
  hence thesis by YELLOW_2:9;
end;

theorem
  for S being non empty TopSpace, T being non empty TopSpace-like
TopRelStr, f, g being Function of S, T, x, y being Element of ContMaps(S,T) st
  x = f & y = g holds x <= y iff f <= g
proof
  let S be non empty TopSpace, T be non empty TopSpace-like TopRelStr, f, g be
  Function of S, T, x, y be Element of ContMaps(S,T) such that
A1: x = f & y = g;
A2: ContMaps(S,T) is full SubRelStr of T |^ the carrier of S by WAYBEL24:def 3;
  then reconsider x1 = x, y1 = y as Element of T |^ the carrier of S by
YELLOW_0:58;
  hereby
    assume x <= y;
    then x1 <= y1 by A2,YELLOW_0:59;
    hence f <= g by A1,WAYBEL10:11;
  end;
  assume f <= g;
  then x1 <= y1 by A1,WAYBEL10:11;
  hence thesis by A2,YELLOW_0:60;
end;

definition
  let I be non empty set, R be non empty RelStr, f be Element of R |^ I, i be
  Element of I;
  redefine func f.i -> Element of R;
  coherence
  proof
    reconsider g = f as Element of product (I --> R) by YELLOW_1:def 5;
    g.i is Element of (I --> R).i;
    hence thesis;
  end;
end;

begin  :: Some properties of isomorphism between relational structures

theorem Th9:
  for S, T being RelStr, f being Function of S, T st f is
  isomorphic holds f is onto
proof
  let S, T be RelStr, f be Function of S, T such that
A1: f is isomorphic;
  per cases;
  suppose
    S is non empty & T is non empty;
    hence rng f = the carrier of T by A1,WAYBEL_0:66;
  end;
  suppose
    S is empty or T is empty;
    then T is empty by A1,WAYBEL_0:def 38;
    then the carrier of T = {};
    hence rng f = the carrier of T;
  end;
end;

registration
  let S, T be RelStr;
  cluster isomorphic -> onto for Function of S, T;
  coherence by Th9;
end;

theorem Th10:
  for S, T being non empty RelStr, f being Function of S, T st f
  is isomorphic holds f/" is isomorphic
proof
  let S, T be non empty RelStr, f be Function of S, T;
  assume
A1: f is isomorphic;
  then (ex g being Function of T, S st g = f qua Function" & g is monotone )&
  rng f = the carrier of T by WAYBEL_0:66,def 38;
  hence thesis by A1,TOPS_2:def 4,WAYBEL_0:68;
end;

theorem
  for S, T being non empty RelStr st S, T are_isomorphic & S is
  with_infima holds T is with_infima
proof
  let S, T be non empty RelStr;
  given f being Function of S, T such that
A1: f is isomorphic;
  assume
A2: for a, b being Element of S ex c being Element of S st c <= a & c <=
  b & for c9 being Element of S st c9 <= a & c9 <= b holds c9 <= c;
  let x, y be Element of T;
  consider c being Element of S such that
A3: c <= f/".x & c <= f/".y and
A4: for c9 being Element of S st c9 <= f/".x & c9 <= f/".y holds c9 <= c by A2;
  take f.c;
A5: ex g being Function of T, S st g = f qua Function" & g is monotone by A1,
WAYBEL_0:def 38;
A6: rng f = the carrier of T by A1,WAYBEL_0:66;
A7: f/" = (f qua Function)" by A1,TOPS_2:def 4;
  f.c <= f.(f/".x) & f.c <= f.(f/".y) by A1,A3,WAYBEL_0:66;
  hence f.c <= x & f.c <= y by A1,A6,A7,FUNCT_1:35;
  let z9 be Element of T;
  assume z9 <= x & z9 <= y;
  then f/".z9 <= f/".x & f/".z9 <= f/".y by A7,A5,WAYBEL_1:def 2;
  then f/".z9 <= c by A4;
  then f.(f/".z9) <= f.c by A1,WAYBEL_0:66;
  hence thesis by A1,A6,A7,FUNCT_1:35;
end;

theorem
  for S, T being non empty RelStr st S, T are_isomorphic & S is
  with_suprema holds T is with_suprema
proof
  let S, T be non empty RelStr;
  given f being Function of S, T such that
A1: f is isomorphic;
  assume
A2: for a, b being Element of S ex c being Element of S st a <= c & b <=
  c & for c9 being Element of S st a <= c9 & b <= c9 holds c <= c9;
  let x, y be Element of T;
  consider c being Element of S such that
A3: f/".x <= c & f/".y <= c and
A4: for c9 being Element of S st f/".x <= c9 & f/".y <= c9 holds c <= c9 by A2;
  take f.c;
A5: ex g being Function of T, S st g = f qua Function" & g is monotone by A1,
WAYBEL_0:def 38;
A6: rng f = the carrier of T by A1,WAYBEL_0:66;
A7: f/" = (f qua Function)" by A1,TOPS_2:def 4;
  f.(f/".x) <= f.c & f.(f/".y) <= f.c by A1,A3,WAYBEL_0:66;
  hence x <= f.c & y <= f.c by A1,A6,A7,FUNCT_1:35;
  let z9 be Element of T;
  assume x <= z9 & y <= z9;
  then f/".x <= f/".z9 & f/".y <= f/".z9 by A7,A5,WAYBEL_1:def 2;
  then c <= f/".z9 by A4;
  then f.c <= f.(f/".z9) by A1,WAYBEL_0:66;
  hence thesis by A1,A6,A7,FUNCT_1:35;
end;

theorem Th13:
  for L being RelStr st L is empty holds L is bounded
proof
  let L be RelStr such that
A1: L is empty;
  set x = the Element of L;
  thus L is lower-bounded
  proof
    take x;
    let a be Element of L;
    assume a in the carrier of L;
    hence thesis by A1;
  end;
  take x;
  let a be Element of L;
  assume a in the carrier of L;
  hence thesis by A1;
end;

registration
  cluster empty -> bounded for RelStr;
  coherence by Th13;
end;

theorem
  for S, T being RelStr st S, T are_isomorphic & S is lower-bounded
  holds T is lower-bounded
proof
  let S, T be RelStr;
  given f being Function of S, T such that
A1: f is isomorphic;
  per cases;
  suppose
    S is non empty & T is non empty;
    then reconsider s = S, t = T as non empty RelStr;
    given X being Element of S such that
A2: X is_<=_than the carrier of S;
    reconsider x = X as Element of s;
    reconsider g = f as Function of s, t;
    reconsider y = g.x as Element of T;
    take y;
    y is_<=_than g.:[#]S by A1,A2,YELLOW_2:13;
    then y is_<=_than rng g by RELSET_1:22;
    hence thesis by A1,WAYBEL_0:66;
  end;
  suppose
    S is empty or T is empty;
    then T is empty by A1,WAYBEL_0:def 38;
    then reconsider T as bounded RelStr;
    T is lower-bounded;
    hence thesis;
  end;
end;

theorem
  for S, T being RelStr st S, T are_isomorphic & S is upper-bounded
  holds T is upper-bounded
proof
  let S, T be RelStr;
  given f being Function of S, T such that
A1: f is isomorphic;
  per cases;
  suppose
    S is non empty & T is non empty;
    then reconsider s = S, t = T as non empty RelStr;
    given X being Element of S such that
A2: X is_>=_than the carrier of S;
    reconsider x = X as Element of s;
    reconsider g = f as Function of s, t;
    reconsider y = g.x as Element of T;
    take y;
    y is_>=_than g.:[#]S by A1,A2,YELLOW_2:14;
    then y is_>=_than rng g by RELSET_1:22;
    hence thesis by A1,WAYBEL_0:66;
  end;
  suppose
    S is empty or T is empty;
    then T is empty by A1,WAYBEL_0:def 38;
    then reconsider T as bounded RelStr;
    T is lower-bounded;
    hence thesis;
  end;
end;

theorem
  for S, T being non empty RelStr, A being Subset of S, f being Function
  of S, T st f is isomorphic & ex_sup_of A, S holds ex_sup_of f.:A, T
proof
  let S, T be non empty RelStr, A be Subset of S, f be Function of S, T such
  that
A1: f is isomorphic;
A2: f"(f.:A) c= A by A1,FUNCT_1:82;
A3: rng f = [#]T by A1,WAYBEL_0:66;
A4: f/" = f qua Function " by A1,TOPS_2:def 4;
  given a being Element of S such that
A5: A is_<=_than a and
A6: for b being Element of S st A is_<=_than b holds b >= a and
A7: for c being Element of S st A is_<=_than c & for b being Element of
  S st A is_<=_than b holds b >= c holds c = a;
  take f.a;
  thus f.:A is_<=_than f.a by A1,A5,WAYBEL13:19;
A8: f/" is isomorphic by A1,Th10;
A9: dom f = the carrier of S by FUNCT_2:def 1;
  then A c= f"(f.:A) by FUNCT_1:76;
  then
A10: f"(f.:A) = A by A2;
  hereby
    let b be Element of T;
    assume f.:A is_<=_than b;
    then f/".:(f.:A) is_<=_than f/".b by A8,WAYBEL13:19;
    then f"(f.:A) is_<=_than f/".b by A1,A3,TOPS_2:55;
    then f/".b >= a by A6,A10;
    then f.(f/".b) >= f.a by A1,WAYBEL_0:66;
    hence b >= f.a by A1,A3,A4,FUNCT_1:35;
  end;
  let c be Element of T;
  assume
A11: f.:A is_<=_than c;
  assume
A12: for b being Element of T st f.:A is_<=_than b holds b >= c;
A13: for b being Element of S st A is_<=_than b holds b >= f/".c
  proof
    let b be Element of S;
    assume A is_<=_than b;
    then f.:A is_<=_than f.b by A1,WAYBEL13:19;
    then f.b >= c by A12;
    then f/".(f.b) >= f/".c by A8,WAYBEL_0:66;
    hence thesis by A1,A4,A9,FUNCT_1:34;
  end;
  f/".:(f.:A) is_<=_than f/".c by A8,A11,WAYBEL13:19;
  then A is_<=_than f/".c by A1,A3,A10,TOPS_2:55;
  then f/".c = a by A7,A13;
  hence thesis by A1,A3,A4,FUNCT_1:35;
end;

theorem
  for S, T being non empty RelStr, A being Subset of S, f being Function
  of S, T st f is isomorphic & ex_inf_of A, S holds ex_inf_of f.:A, T
proof
  let S, T be non empty RelStr, A be Subset of S, f be Function of S, T such
  that
A1: f is isomorphic;
A2: f"(f.:A) c= A by A1,FUNCT_1:82;
A3: rng f = [#]T by A1,WAYBEL_0:66;
A4: f/" = f qua Function " by A1,TOPS_2:def 4;
  given a being Element of S such that
A5: A is_>=_than a and
A6: for b being Element of S st A is_>=_than b holds b <= a and
A7: for c being Element of S st A is_>=_than c & for b being Element of
  S st A is_>=_than b holds b <= c holds c = a;
  take f.a;
  thus f.:A is_>=_than f.a by A1,A5,WAYBEL13:18;
A8: f/" is isomorphic by A1,Th10;
A9: dom f = the carrier of S by FUNCT_2:def 1;
  then A c= f"(f.:A) by FUNCT_1:76;
  then
A10: f"(f.:A) = A by A2;
  hereby
    let b be Element of T;
    assume f.:A is_>=_than b;
    then f/".:(f.:A) is_>=_than f/".b by A8,WAYBEL13:18;
    then f"(f.:A) is_>=_than f/".b by A1,A3,TOPS_2:55;
    then f/".b <= a by A6,A10;
    then f.(f/".b) <= f.a by A1,WAYBEL_0:66;
    hence b <= f.a by A1,A3,A4,FUNCT_1:35;
  end;
  let c be Element of T;
  assume
A11: f.:A is_>=_than c;
  assume
A12: for b being Element of T st f.:A is_>=_than b holds b <= c;
A13: for b being Element of S st A is_>=_than b holds b <= f/".c
  proof
    let b be Element of S;
    assume A is_>=_than b;
    then f.:A is_>=_than f.b by A1,WAYBEL13:18;
    then f.b <= c by A12;
    then f/".(f.b) <= f/".c by A8,WAYBEL_0:66;
    hence thesis by A1,A4,A9,FUNCT_1:34;
  end;
  f/".:(f.:A) is_>=_than f/".c by A8,A11,WAYBEL13:18;
  then A is_>=_than f/".c by A1,A3,A10,TOPS_2:55;
  then f/".c = a by A7,A13;
  hence thesis by A1,A3,A4,FUNCT_1:35;
end;

begin  :: On the product of topological spaces

theorem
  for S, T being TopStruct st (S,T are_homeomorphic or ex f being
Function of S,T st dom f = [#]S & rng f = [#]T) holds S is empty iff T is empty
proof
  let S, T be TopStruct;
  assume
A1: S,T are_homeomorphic or ex f being Function of S,T st dom f = [#]S &
  rng f = [#]T;
  per cases by A1;
  suppose
    S,T are_homeomorphic;
    then consider f being Function of S, T such that
A2: f is being_homeomorphism;
    rng f = [#]T & dom f = [#]S by A2;
    hence thesis;
  end;
  suppose
    ex f being Function of S,T st dom f = [#]S & rng f = [#]T;
    hence thesis;
  end;
end;

theorem
  for T being non empty TopSpace holds T, the TopStruct of T are_homeomorphic
proof
  let T be non empty TopSpace;
  reconsider f = id T as Function of T, the TopStruct of T;
  take f;
  thus dom f = [#]T;
  thus rng f = [#]T
    .= [#]the TopStruct of T;
  thus f is one-to-one;
  thus f is continuous by YELLOW12:36;
  thus thesis by YELLOW12:36;
end;

registration
  let T be Scott reflexive non empty TopRelStr;
  cluster open -> inaccessible upper for Subset of T;
  coherence by WAYBEL11:def 4;
  cluster inaccessible upper -> open for Subset of T;
  coherence by WAYBEL11:def 4;
end;

theorem
  for T being TopStruct, x, y being Point of T, X, Y being Subset of T
  st X = {x} & Cl X c= Cl Y holds x in Cl Y
proof
  let T be TopStruct, x, y be Point of T, X, Y be Subset of T such that
A1: X = {x} and
A2: Cl X c= Cl Y;
  X c= Cl X by PRE_TOPC:18;
  then
A3: X c= Cl Y by A2;
  x in X by A1,TARSKI:def 1;
  hence thesis by A3;
end;

theorem
  for T being TopStruct, x, y being Point of T, Y, V being Subset of T
  st Y = {y} & x in Cl Y & V is open & x in V holds y in V
proof
  let T be TopStruct, x, y be Point of T, Y, V be Subset of T such that
A1: Y = {y};
  assume x in Cl Y & V is open & x in V;
  then Y meets V by PRE_TOPC:def 7;
  hence thesis by A1,ZFMISC_1:50;
end;

theorem
  for T being TopStruct, x, y being Point of T, X, Y being Subset of T
st X = {x} & Y = {y} holds (for V being Subset of T st V is open holds (x in V
  implies y in V)) implies Cl X c= Cl Y
proof
  let T be TopStruct, x, y be Point of T, X, Y be Subset of T;
  assume that
A1: X = {x} and
A2: Y = {y} & for V being Subset of T st V is open holds x in V implies y in V;
  let z be object;
  assume
A3: z in Cl X;
  for V being Subset of T st V is open holds z in V implies Y meets V
  proof
    let V be Subset of T;
    assume that
A4: V is open and
A5: z in V;
    X meets V by A3,A4,A5,PRE_TOPC:def 7;
    then x in V by A1,ZFMISC_1:50;
    hence thesis by A2,A4,ZFMISC_1:48;
  end;
  hence thesis by A3,PRE_TOPC:def 7;
end;

theorem Th23:
  for S, T being non empty TopSpace, A being irreducible Subset of
S, B being Subset of T st A = B & the TopStruct of S = the TopStruct of T holds
  B is irreducible
proof
  let S, T be non empty TopSpace, A be irreducible Subset of S, B be Subset of
  T such that
A1: A = B and
A2: the TopStruct of S = the TopStruct of T;
  A is non empty closed by YELLOW_8:def 3;
  hence B is non empty closed by A1,A2,TOPS_3:79;
  let B1, B2 be Subset of T such that
A3: B1 is closed & B2 is closed and
A4: B = B1 \/ B2;
  reconsider A1 = B1, A2 = B2 as Subset of S by A2;
  A1 is closed & A2 is closed by A2,A3,TOPS_3:79;
  hence thesis by A1,A4,YELLOW_8:def 3;
end;

theorem Th24:
  for S, T being non empty TopSpace, a being Point of S, b being
  Point of T, A being Subset of S, B being Subset of T st a = b & A = B & the
  TopStruct of S = the TopStruct of T & a is_dense_point_of A holds b
  is_dense_point_of B
proof
  let S, T be non empty TopSpace, a be Point of S, b be Point of T, A be
  Subset of S, B be Subset of T;
  assume a = b & A = B & the TopStruct of S = the TopStruct of T & a in A & A
  c= Cl{a};
  hence b in B & B c= Cl{b} by TOPS_3:80;
end;

theorem Th25:
  for S, T being TopStruct, A being Subset of S, B being Subset of
T st A = B & the TopStruct of S = the TopStruct of T & A is compact holds B is
  compact
proof
  let S, T be TopStruct, A be Subset of S, B be Subset of T such that
A1: A = B and
A2: the TopStruct of S = the TopStruct of T and
A3: for F being Subset-Family of S st F is Cover of A & F is open ex G
  being Subset-Family of S st G c= F & G is Cover of A & G is finite;
  let F be Subset-Family of T such that
A4: F is Cover of B & F is open;
  reconsider K = F as Subset-Family of S by A2;
  consider L being Subset-Family of S such that
A5: L c= K & L is Cover of A & L is finite by A1,A2,A3,A4,WAYBEL_9:19;
  reconsider G = L as Subset-Family of T by A2;
  take G;
  thus thesis by A1,A5;
end;

theorem
  for S, T being non empty TopSpace st the TopStruct of S = the
  TopStruct of T & S is sober holds T is sober
proof
  let S, T be non empty TopSpace such that
A1: the TopStruct of S = the TopStruct of T and
A2: for A be irreducible Subset of S ex a being Point of S st a
is_dense_point_of A & for b being Point of S st b is_dense_point_of A holds a =
  b;
  let B be irreducible Subset of T;
  reconsider A = B as irreducible Subset of S by A1,Th23;
  consider a being Point of S such that
A3: a is_dense_point_of A and
A4: for b being Point of S st b is_dense_point_of A holds a = b by A2;
  reconsider p = a as Point of T by A1;
  take p;
  thus p is_dense_point_of B by A1,A3,Th24;
  let q be Point of T;
  reconsider b = q as Point of S by A1;
  assume q is_dense_point_of B;
  then b is_dense_point_of A by A1,Th24;
  hence thesis by A4;
end;

theorem
  for S, T being non empty TopSpace st the TopStruct of S = the
  TopStruct of T & S is locally-compact holds T is locally-compact
proof
  let S, T be non empty TopSpace such that
A1: the TopStruct of S = the TopStruct of T and
A2: for x being Point of S, X being Subset of S st x in X & X is open ex
  Y being Subset of S st x in Int Y & Y c= X & Y is compact;
  let x be Point of T, X be Subset of T such that
A3: x in X & X is open;
  reconsider A = X as Subset of S by A1;
  consider B being Subset of S such that
A4: x in Int B & B c= A & B is compact by A1,A2,A3,TOPS_3:76;
  reconsider Y = B as Subset of T by A1;
  take Y;
  thus thesis by A1,A4,Th25,TOPS_3:77;
end;

theorem
  for S, T being TopStruct st the TopStruct of S = the TopStruct of T &
  S is compact holds T is compact
proof
  let S, T be TopStruct such that
A1: the TopStruct of S = the TopStruct of T and
A2: for F being Subset-Family of S st F is Cover of S & F is open ex G
  being Subset-Family of S st G c= F & G is Cover of S & G is finite;
  let F be Subset-Family of T such that
A3: F is Cover of T & F is open;
  reconsider K = F as Subset-Family of S by A1;
  consider L being Subset-Family of S such that
A4: L c= K & L is Cover of S & L is finite by A1,A2,A3,WAYBEL_9:19;
  reconsider G = L as Subset-Family of T by A1;
  take G;
  thus thesis by A1,A4;
end;

definition
  let I be non empty set, T be non empty TopSpace, x be Point of product (I
  --> T), i be Element of I;
  redefine func x.i -> Element of T;
  coherence
  proof
    x.i is Point of T;
    hence thesis;
  end;
end;

theorem Th29:
  for M being non empty set, J being TopStruct-yielding non-Empty
  ManySortedSet of M, x, y being Point of product J holds x in Cl {y} iff for i
  being Element of M holds x.i in Cl {y.i}
proof
  let M be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of M,
  x, y be Point of product J;
  hereby
    assume
A1: x in Cl {y};
    let i be Element of M;
    x in the carrier of product J;
    then x in product Carrier J by WAYBEL18:def 3;
    then consider f being Function such that
A2: x = f and
A3: dom f = dom Carrier J and
A4: for z being object st z in dom Carrier J holds f.z in (Carrier J).z
    by CARD_3:def 5;
A5: i in M;
    for G being Subset of J.i st G is open holds x.i in G implies {y.i} meets G
    proof
      let G be Subset of J.i;
      assume that
A6:   G is open and
A7:   x.i in G;
      reconsider G9 = G as Subset of J.i;
      [#](J.i) <> {} & proj(J,i) is continuous by WAYBEL18:5;
      then
A8:   proj(J,i)"G9 is open by A6,TOPS_2:43;
A9:   for z being object st z in dom ((Carrier J)+*(i,G)) holds f.z in ((
      Carrier J)+*(i,G)).z
      proof
        let z be object;
        assume z in dom ((Carrier J)+*(i,G));
        then
A10:    z in dom Carrier J by FUNCT_7:30;
        per cases;
        suppose
          z = i;
          hence thesis by A2,A7,A10,FUNCT_7:31;
        end;
        suppose
          z <> i;
          then ((Carrier J)+*(i,G)).z = (Carrier J).z by FUNCT_7:32;
          hence thesis by A4,A10;
        end;
      end;
A11:  product ((Carrier J) +* (i,G9)) = proj(J,i)"G9 by WAYBEL18:4;
      dom f = dom ((Carrier J) +* (i,G)) by A3,FUNCT_7:30;
      then x in product ((Carrier J) +* (i,G)) by A2,A9,CARD_3:def 5;
      then {y} meets proj(J,i)"G9 by A1,A8,A11,PRE_TOPC:def 7;
      then y in product ((Carrier J) +* (i,G)) by A11,ZFMISC_1:50;
      then consider g being Function such that
A12:  y = g and
      dom g = dom ((Carrier J) +* (i,G)) and
A13:  for z being object st z in dom ((Carrier J) +* (i,G)) holds g.z in
      ((Carrier J) +* (i,G)).z by CARD_3:def 5;
A14:  i in dom Carrier J by A5,PARTFUN1:def 2;
      then i in dom ((Carrier J) +* (i,G)) by FUNCT_7:30;
      then g.i in ((Carrier J) +* (i,G)).i by A13;
      then g.i in G by A14,FUNCT_7:31;
      hence thesis by A12,ZFMISC_1:48;
    end;
    hence x.i in Cl {y.i} by PRE_TOPC:def 7;
  end;
  reconsider K = product_prebasis J as prebasis of product J by WAYBEL18:def 3;
  assume
A15: for i being Element of M holds x.i in Cl {y.i};
  for Z being finite Subset-Family of product J st Z c= K & x in
  Intersect Z holds Intersect Z meets {y}
  proof
    let Z be finite Subset-Family of product J;
    assume that
A16: Z c= K and
A17: x in Intersect Z;
    for Y being set st Y in Z holds y in Y
    proof
      let Y be set;
      y in the carrier of product J;
      then y in product Carrier J by WAYBEL18:def 3;
      then consider g being Function such that
A18:  y = g and
A19:  dom g = dom Carrier J and
A20:  for z being object st z in dom Carrier J holds g.z in (Carrier J).
      z by CARD_3:def 5;
      assume
A21:  Y in Z;
      then Y in K by A16;
      then consider
      i being set, W being TopStruct, V being Subset of W such that
A22:  i in M and
A23:  V is open and
A24:  W = J.i and
A25:  Y = product ((Carrier J)+*(i,V)) by WAYBEL18:def 2;
      reconsider i as Element of M by A22;
      reconsider V as Subset of (J.i) by A24;
      x in Y by A17,A21,SETFAM_1:43;
      then
A26:  ex f being Function st x = f & dom f = dom ((Carrier J)+* (i,V)) &
for z being object st z in dom ((Carrier J)+*(i,V))
holds f.z in (( Carrier J)+*(i
      ,V)).z by A25,CARD_3:def 5;
      x.i in Cl {y.i} by A15;
      then
A27:  x.i in V implies {y.i} meets V by A23,A24,PRE_TOPC:def 7;
A28:  for z being object st z in dom ((Carrier J)+*(i,V)) holds g.z in ((
      Carrier J)+*(i,V)).z
      proof
        let z be object;
        assume
A29:    z in dom ((Carrier J)+*(i,V));
        then
A30:    z in dom Carrier J by FUNCT_7:30;
        per cases;
        suppose
A31:      z = i;
          then ((Carrier J)+*(i,V)).z = V by A30,FUNCT_7:31;
          hence thesis by A27,A26,A18,A29,A31,ZFMISC_1:50;
        end;
        suppose
          z <> i;
          then ((Carrier J)+*(i,V)).z = (Carrier J).z by FUNCT_7:32;
          hence thesis by A20,A30;
        end;
      end;
      dom g = dom ((Carrier J)+*(i,V)) by A19,FUNCT_7:30;
      hence thesis by A25,A18,A28,CARD_3:def 5;
    end;
    then y in {y} & y in Intersect Z by SETFAM_1:43,TARSKI:def 1;
    hence thesis by XBOOLE_0:3;
  end;
  hence thesis by YELLOW_9:38;
end;

theorem
  for M being non empty set, T being non empty TopSpace, x, y being
Point of product (M --> T) holds x in Cl {y} iff for i being Element of M holds
  x.i in Cl {y.i}
proof
  let M be non empty set, T be non empty TopSpace, x, y be Point of product (M
  --> T);
  reconsider J = M --> T as TopStruct-yielding non-Empty ManySortedSet of M;
  reconsider x9 = x, y9 = y as Point of product J;
  thus x in Cl {y} implies for i being Element of M holds x.i in Cl {y.i}
  proof
    assume
A1: x in Cl {y};
    let i be Element of M;
    x9.i in Cl {y9.i} by A1,Th29;
    hence thesis;
  end;
  assume
A2: for i being Element of M holds x.i in Cl {y.i};
  for i being Element of M holds x9.i in Cl {y9.i}
  proof
    let i be Element of M;
    x.i in Cl {y.i} by A2;
    hence thesis;
  end;
  hence thesis by Th29;
end;

theorem Th31:
  for M being non empty set, i being Element of M, J being
  TopStruct-yielding non-Empty ManySortedSet of M, x being Point of product J
  holds pi(Cl {x}, i) = Cl {x.i}
proof
  let M be non empty set, i be Element of M, J be TopStruct-yielding non-Empty
  ManySortedSet of M, x be Point of product J;
  consider f being object such that
A1: f in Cl {x} by XBOOLE_0:def 1;
A2: f in the carrier of product J by A1;
  thus pi(Cl {x}, i) c= Cl {x.i}
  proof
    let a be object;
    assume a in pi(Cl {x}, i);
    then ex f being Function st f in Cl {x} & a = f.i by CARD_3:def 6;
    hence thesis by Th29;
  end;
  reconsider f as Element of product J by A1;
  let a be object;
  set y = f +* (i .--> a);
A3: dom Carrier J = M by PARTFUN1:def 2;
A4: f in product Carrier J by A2,WAYBEL18:def 3;
  then
A5: dom f = M by A3,CARD_3:9;
  assume
A7: a in Cl {x.i};
A8: for m being object st m in dom Carrier J holds y.m in (Carrier J).m
  proof
    let m be object;
    assume
A9: m in dom Carrier J;
    then
A10: ex R being 1-sorted st R = J.m & Carrier J.m = the carrier of R by
PRALG_1:def 13;
    per cases;
    suppose
A11:  m = i;
      then y.m = a by FUNCT_7:94;
      hence thesis by A7,A10,A11;
    end;
    suppose
      m <> i;
      then not m in dom (i .--> a) by TARSKI:def 1;
      then y.m = f.m by FUNCT_4:11;
      hence thesis by A4,A9,CARD_3:9;
    end;
  end;
  dom y = dom f \/ dom (i .--> a) by FUNCT_4:def 1
    .= M \/ {i} by A5
    .= M by ZFMISC_1:40;
  then y in product Carrier J by A3,A8,CARD_3:9;
  then reconsider y = f +* (i .--> a) as Element of product J by WAYBEL18:def 3
;
  for m being Element of M holds y.m in Cl {x.m}
  proof
    let m be Element of M;
    per cases;
    suppose
      m = i;
      hence thesis by A7,FUNCT_7:94;
    end;
    suppose
      m <> i;
      then not m in dom (i .--> a) by TARSKI:def 1;
      then y.m = f.m by FUNCT_4:11;
      hence thesis by A1,Th29;
    end;
  end;
  then
A12: f +* (i .--> a) in Cl {x} by Th29;
  (f +* (i .--> a)).i = a by FUNCT_7:94;
  hence thesis by A12,CARD_3:def 6;
end;

theorem
  for M being non empty set, i being Element of M, T being non empty
  TopSpace, x being Point of product (M --> T) holds pi(Cl {x}, i) = Cl {x.i}
proof
  let M be non empty set, i be Element of M, T be non empty TopSpace, x be
  Point of product (M --> T);
  (M --> T).i = T;
  hence thesis by Th31;
end;

theorem
  for X, Y being non empty TopStruct, f being Function of X, Y, g being
  Function of Y, X st f = id X & g = id X & f is continuous & g is continuous
  holds the TopStruct of X = the TopStruct of Y
proof
  let X, Y be non empty TopStruct, f be Function of X, Y, g be Function of Y,
  X such that
A1: f = id X and
A2: g = id X and
A3: f is continuous and
A4: g is continuous;
A5: the carrier of X = dom f by FUNCT_2:def 1
    .= the carrier of Y by A2,FUNCT_2:def 1;
A6: [#]Y <> {};
A7: [#]X <> {};
  the topology of X = the topology of Y
  proof
    hereby
      let A be object;
      assume
A8:   A in the topology of X;
      then reconsider B = A as Subset of X;
      B is open by A8;
      then
A9:   g"B is open by A4,A7,TOPS_2:43;
      g"B = B by A2,FUNCT_2:94;
      hence A in the topology of Y by A9;
    end;
    let A be object;
    assume
A10: A in the topology of Y;
    then reconsider B = A as Subset of Y;
    B is open by A10;
    then
A11: f"B is open by A3,A6,TOPS_2:43;
    f"B = B by A1,A5,FUNCT_2:94;
    hence thesis by A11;
  end;
  hence thesis by A5;
end;

theorem
  for X, Y being non empty TopSpace, f being Function of X, Y st corestr
  f is continuous holds f is continuous
proof
  let X, Y be non empty TopSpace, f be Function of X, Y such that
A1: corestr f is continuous;
  corestr f = f by WAYBEL18:def 7;
  hence thesis by A1,PRE_TOPC:26;
end;

registration
  let X be non empty TopSpace, Y be non empty SubSpace of X;
  cluster incl Y -> continuous;
  coherence by TMAP_1:87;
end;

theorem
  for T being non empty TopSpace, f being Function of T, T st f*f = f
  holds corestr f * incl Image f = id Image f
proof
  let T be non empty TopSpace, f be Function of T, T such that
A1: f*f = f;
  set cf = corestr f, i = incl Image f;
  for x being object st x in the carrier of Image f holds (cf*i).x = (id
  Image f).x
  proof
A2: the carrier of Image f c= the carrier of T by BORSUK_1:1;
    let x be object;
    assume
A3: x in the carrier of Image f;
    the carrier of Image f = rng f by WAYBEL18:9;
    then
A4: ex y being object st y in dom f & f.y = x by A3,FUNCT_1:def 3;
    thus (cf*i).x = cf.(i.x) by A3,FUNCT_2:15
      .= cf.x by A3,A2,TMAP_1:84
      .= f.x by WAYBEL18:def 7
      .= x by A1,A4,FUNCT_2:15
      .= (id Image f).x by A3,FUNCT_1:18;
  end;
  hence thesis;
end;

theorem
  for Y being non empty TopSpace, W being non empty SubSpace of Y holds
  corestr incl W is being_homeomorphism
proof
  let Y be non empty TopSpace, W be non empty SubSpace of Y;
  set ci = corestr incl W;
  thus dom ci = [#]W by FUNCT_2:def 1;
  thus
A1: rng ci = [#]Image incl W by FUNCT_2:def 3;
A2: ci = incl W by WAYBEL18:def 7
    .= (id Y)|W by TMAP_1:def 6
    .= (id the carrier of Y)|the carrier of W by TMAP_1:def 4;
  hence
A3: ci is one-to-one by FUNCT_1:52;
A4: for P being Subset of W st P is open holds ci/""P is open
  proof
    let P be Subset of W;
    assume P in the topology of W;
    then
A5: ex Q being Subset of Y st Q in the topology of Y & P = Q /\ [#]W by
PRE_TOPC:def 4;
A6: the carrier of W is non empty Subset of Y by BORSUK_1:1;
    then
A7: P is Subset of Y by XBOOLE_1:1;
A8: [#]W = rng ((id the carrier of Y)|the carrier of W) by A6,Th2
      .= rng ((id Y)|W) by TMAP_1:def 4
      .= rng incl W by TMAP_1:def 6
      .= [#]Image incl W by WAYBEL18:9;
    ci/""P = ((id the carrier of Y)|the carrier of W).:P by A1,A2,A3,TOPS_2:54
      .= (id the carrier of Y).:P by FUNCT_2:97
      .= P by A7,FUNCT_1:92;
    hence ci/""P in the topology of Image incl W by A5,A8,PRE_TOPC:def 4;
  end;
  thus ci is continuous by WAYBEL18:10;
  [#]W <> {};
  hence thesis by A4,TOPS_2:43;
end;

theorem Th37:
  for M being non empty set, J being TopStruct-yielding non-Empty
ManySortedSet of M st for i being Element of M holds J.i is T_0 TopSpace holds
  product J is T_0
proof
  let M be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of M
  such that
A1: for i be Element of M holds J.i is T_0 TopSpace;
  for x, y being Point of product J st x <> y holds Cl {x} <> Cl {y}
  proof
    let x, y be Point of product J such that
A2: x <> y and
A3: Cl {x} = Cl {y};
    y in the carrier of product J;
    then y in product Carrier J by WAYBEL18:def 3;
    then dom y = dom Carrier J by CARD_3:9;
    then
A4: dom y = M by PARTFUN1:def 2;
    x in the carrier of product J;
    then x in product Carrier J by WAYBEL18:def 3;
    then dom x = dom Carrier J by CARD_3:9;
    then dom x = M by PARTFUN1:def 2;
    then consider i being object such that
A5: i in M and
A6: x.i <> y.i by A2,A4,FUNCT_1:2;
    reconsider i as Element of M by A5;
A7: pi(Cl {y}, i) = Cl {y.i} by Th31;
    J.i is T_0 TopSpace & pi(Cl {x}, i) = Cl {x.i} by A1,Th31;
    hence contradiction by A3,A6,A7,TSP_1:def 5;
  end;
  hence thesis by TSP_1:def 5;
end;

registration
  let I be non empty set, T be non empty T_0 TopSpace;
  cluster product (I --> T) -> T_0;
  coherence
  proof
    for i being Element of I holds (I --> T).i is T_0 TopSpace;
    hence thesis by Th37;
  end;
end;

theorem Th38:
  for M being non empty set, J being TopStruct-yielding non-Empty
  ManySortedSet of M st for i being Element of M holds J.i is T_1 TopSpace-like
  holds product J is T_1
proof
  let M be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of M
  such that
A1: for i be Element of M holds J.i is T_1 TopSpace-like;
  for p being Point of product J holds {p} is closed
  proof
    let p be Point of product J;
    {p} = Cl {p}
    proof
      thus {p} c= Cl {p} by PRE_TOPC:18;
      let a be object;
      assume
A2:   a in Cl {p};
      then reconsider a, p as Element of product J;
A3:   for i being object st i in M holds a.i = p.i
      proof
        let i be object;
        assume i in M;
        then reconsider i as Element of M;
        J.i is TopSpace & J.i is T_1 by A1;
        then
A4:     {p.i} is closed by URYSOHN1:19;
        a.i in Cl {p.i} by A2,Th29;
        then a.i in {p.i} by A4,PRE_TOPC:22;
        hence thesis by TARSKI:def 1;
      end;
      p in the carrier of product J;
      then p in product Carrier J by WAYBEL18:def 3;
      then dom p = dom Carrier J by CARD_3:9;
      then
A5:   dom p = M by PARTFUN1:def 2;
      a in the carrier of product J;
      then a in product Carrier J by WAYBEL18:def 3;
      then dom a = dom Carrier J by CARD_3:9;
      then dom a = M by PARTFUN1:def 2;
      then a = p by A5,A3,FUNCT_1:2;
      hence thesis by TARSKI:def 1;
    end;
    hence thesis;
  end;
  hence thesis by URYSOHN1:19;
end;

registration
  let I be non empty set, T be non empty T_1 TopSpace;
  cluster product (I --> T) -> T_1;
  coherence
  proof
    for i being Element of I holds (I --> T).i is T_1 TopSpace-like;
    hence thesis by Th38;
  end;
end;