:: Injective Spaces
::  by Jaros{\l}aw Gryko
::
:: Received April 17, 1998
:: Copyright (c) 1998-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 SETFAM_1, XBOOLE_0, CANTOR_1, TARSKI, PRE_TOPC, RLVECT_3,
      RELAT_1, PRALG_1, FUNCT_1, PBOOLE, FUNCOP_1, WAYBEL_3, STRUCT_0,
      SUBSET_1, CARD_3, RLVECT_2, RCOMP_1, FUNCT_4, MONOID_0, ORDINAL2,
      FUNCTOR0, PARTFUN1, FUNCT_6, BORSUK_1, FUNCT_3, GROUP_6, WAYBEL_1,
      FUNCT_2, T_0TOPSP, TOPS_2, CARD_1, ZFMISC_1, RELAT_2, ORDERS_2, WAYBEL11,
      YELLOW_9, YELLOW_1, LATTICE3, FILTER_1, XXREAL_0, WAYBEL_0, CARD_FIL,
      FINSET_1, REWRITE1, WAYBEL_8, LATTICES, CAT_1, WAYBEL_9, WAYBEL18;
 notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, SETFAM_1, RELAT_1, PBOOLE,
      FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, DOMAIN_1, ORDINAL1, NUMBERS,
      STRUCT_0, PRE_TOPC, T_0TOPSP, FUNCT_3, FUNCT_6, FUNCT_7, CARD_3,
      FUNCOP_1, MONOID_0, PRALG_1, ORDERS_2, LATTICE3, YELLOW_1, CANTOR_1,
      FINSET_1, TOPS_2, BORSUK_1, TMAP_1, YELLOW_0, YELLOW_9, WAYBEL_0,
      WAYBEL_3, WAYBEL_8, WAYBEL_9, WAYBEL11;
 constructors FUNCT_3, FUNCT_7, TOPS_2, BORSUK_1, LATTICE3, TMAP_1, T_0TOPSP,
      CANTOR_1, MONOID_0, PRALG_1, WAYBEL_3, WAYBEL_5, WAYBEL_8, WAYBEL11,
      YELLOW_9, BINOP_1;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, FUNCOP_1, CARD_3,
      STRUCT_0, PRE_TOPC, BORSUK_1, LATTICE3, YELLOW_0, MONOID_0, WAYBEL_0,
      YELLOW_1, WAYBEL_3, WAYBEL_8, WAYBEL11, YELLOW_9, WAYBEL17, RELAT_1,
      CARD_1;
 requirements SUBSET, BOOLE, NUMERALS;
 definitions TARSKI, PRE_TOPC, FUNCOP_1, WAYBEL_1, WAYBEL_3, XBOOLE_0, PRALG_1;
 equalities STRUCT_0, ORDINAL1;
 expansions TARSKI, PRE_TOPC, WAYBEL_1, XBOOLE_0;
 theorems TARSKI, PRE_TOPC, ENUMSET1, ZFMISC_1, T_0TOPSP, TOPS_1, TOPS_2,
      FINSET_1, FUNCT_2, FUNCT_3, RELAT_1, FUNCT_1, BORSUK_1, FUNCOP_1,
      CANTOR_1, LATTICE3, ORDERS_2, MSSUBFAM, PRALG_1, CARD_3, WAYBEL_3,
      FUNCT_6, FUNCT_7, TMAP_1, YELLOW_9, YELLOW_0, YELLOW_1, WAYBEL_0,
      WAYBEL_7, WAYBEL_8, WAYBEL11, WAYBEL13, WAYBEL14, RELSET_1, SETFAM_1,
      XBOOLE_0, XBOOLE_1, ORDERS_1, MONOID_0, CARD_1, PARTFUN1;
 schemes SUBSET_1, CLASSES1, FUNCT_1, FRAENKEL;

begin :: Preliminaries

theorem Th1:
  for X being set, A,B being Subset-Family of X st B = A \ {{}} or
  A = B \/ {{}} holds UniCl A = UniCl B
proof
  let X be set;
  let A,B be Subset-Family of X;
  assume
A1: B = A \ {{}} or A = B \/ {{}};
A2: UniCl A c= UniCl B
  proof
    let x be object;
    assume x in UniCl A;
    then consider Y being Subset-Family of X such that
A3: Y c= A and
A4: x = union Y by CANTOR_1:def 1;
A5: Y \ {{}} c= B
    proof
      let w be object;
      assume
A6:   w in Y \ {{}};
      per cases by A1;
      suppose
A7:     B = A \ {{}};
        w in Y & not w in {{}} by A6,XBOOLE_0:def 5;
        hence thesis by A3,A7,XBOOLE_0:def 5;
      end;
      suppose
A8:     A = B \/ {{}};
        w in Y & not w in {{}} by A6,XBOOLE_0:def 5;
        hence thesis by A3,A8,XBOOLE_0:def 3;
      end;
    end;
    reconsider Z = Y \ {{}} as Subset-Family of X;
    Z \/ {{}} = Y \/ {{}} by XBOOLE_1:39;
    then union (Z \/ {{}}) = union Y \/ union {{}} by ZFMISC_1:78
      .= union Y \/ {} by ZFMISC_1:25
      .= union Y;
    then x = union Z \/ union {{}} by A4,ZFMISC_1:78
      .= union Z \/ {} by ZFMISC_1:25
      .= union Z;
    hence thesis by A5,CANTOR_1:def 1;
  end;
  UniCl B c= UniCl A by A1,CANTOR_1:9,XBOOLE_1:7,36;
  hence thesis by A2;
end;

theorem Th2:
  for T being TopSpace, K being Subset-Family of T holds K is Basis
  of T iff K \ {{}} is Basis of T
proof
  let T be TopSpace, K be Subset-Family of T;
  reconsider K9 = K \ {{}} as Subset-Family of T;
A1: UniCl K9 c= UniCl K by CANTOR_1:9,XBOOLE_1:36;
A2: K \ {{}} c= K by XBOOLE_1:36;
  hereby
    assume
A3: K is Basis of T;
    then the topology of T c= UniCl K by CANTOR_1:def 2;
    then
A4: the topology of T c= UniCl K9 by Th1;
    K c= the topology of T by A3,TOPS_2:64;
    then K \ {{}} c= the topology of T by A2;
    hence K \ {{}} is Basis of T by A4,CANTOR_1:def 2,TOPS_2:64;
  end;
  assume
A5: K \ {{}} is Basis of T;
  then
A6: K9 c= the topology of T by TOPS_2:64;
A7: K c= the topology of T
  proof
    let x be object;
    assume
A8: x in K;
    per cases;
    suppose
      x = {};
      hence thesis by PRE_TOPC:1;
    end;
    suppose
      x <> {};
      then not x in {{}} by TARSKI:def 1;
      then x in K9 by A8,XBOOLE_0:def 5;
      hence thesis by A6;
    end;
  end;
  the topology of T c= UniCl K9 by A5,CANTOR_1:def 2;
  then the topology of T c= UniCl K by A1;
  hence thesis by A7,CANTOR_1:def 2,TOPS_2:64;
end;

definition
  let F be Relation;
  attr F is TopStruct-yielding means
  :Def1:
  for x being object st x in rng F holds x is TopStruct;
end;

registration
  cluster TopStruct-yielding -> 1-sorted-yielding for Function;
  coherence
  proof
    let F be Function such that
A1: F is TopStruct-yielding;
    let x be object;
    assume x in dom F;
    then F.x in rng F by FUNCT_1:def 3;
    hence thesis by A1;
  end;
end;

registration
  let I be set;
  cluster TopStruct-yielding for ManySortedSet of I;
  existence
  proof
    take f = I --> the TopSpace;
    let v be object;
    assume v in rng(f);
    hence thesis by TARSKI:def 1;
  end;
end;

registration
  let I be set;
  cluster TopStruct-yielding non-Empty for ManySortedSet of I;
  existence
  proof
    set R = the non empty TopSpace;
    take J = I --> R;
    thus J is TopStruct-yielding
    proof
      let x be object;
      assume x in rng J;
      hence thesis by TARSKI:def 1;
    end;
    thus J is non-Empty
    proof
      let S be 1-sorted;
      assume S in rng J;
      hence thesis by TARSKI:def 1;
    end;
  end;
end;

definition
  let J be non empty set;
  let A be TopStruct-yielding ManySortedSet of J;
  let j be Element of J;
  redefine func A.j -> TopStruct;
  coherence
  proof
    dom A = J by PARTFUN1:def 2;
    then A.j in rng A by FUNCT_1:def 3;
    hence thesis by Def1;
  end;
end;

definition
  let I be set;
  let J be TopStruct-yielding ManySortedSet of I;
  func product_prebasis J -> Subset-Family of product Carrier J means
  :Def2:
  for x being Subset of product Carrier J holds x in it iff ex i being set, T
  being TopStruct, V being Subset of T st i in I & V is open & T = J.i & x =
  product ((Carrier J) +* (i,V));
  existence
  proof
    defpred P[Subset of product Carrier J] means ex i being set, T being
TopStruct, V being Subset of T st i in I & V is open & T = J.i & $1 = product (
    (Carrier J) +* (i,V));
    thus ex F being Subset-Family of product Carrier J st for x being Subset
    of product Carrier J holds x in F iff P[x] from SUBSET_1:sch 3;
  end;
  uniqueness
  proof
    let P1,P2 be Subset-Family of product Carrier J such that
A1: for x being Subset of product Carrier J holds x in P1 iff ex i
being set, T being TopStruct, V being Subset of T st i in I & V is open & T = J
    .i & x = product ((Carrier J) +* (i,V)) and
A2: for x being Subset of product Carrier J holds x in P2 iff ex i
being set, T being TopStruct, V being Subset of T st i in I & V is open & T = J
    .i & x = product ((Carrier J) +* (i,V));
A3: P2 c= P1
    proof
      let x be object;
      assume
A4:   x in P2;
      then reconsider x9 = x as Subset of product Carrier J;
      ex i being set, T being TopStruct, V being Subset of T st i in I & V
      is open & T = J.i & x9 = product ((Carrier J) +* (i,V)) by A2,A4;
      hence thesis by A1;
    end;
    P1 c= P2
    proof
      let x be object;
      assume
A5:   x in P1;
      then reconsider x9 = x as Subset of product Carrier J;
      ex i being set, T being TopStruct, V being Subset of T st i in I & V
      is open & T = J.i & x9 = product ((Carrier J) +* (i,V)) by A1,A5;
      hence thesis by A2;
    end;
    hence thesis by A3;
  end;
end;

theorem Th3:
  for X be set, A be Subset-Family of X holds TopStruct (#X,UniCl
    FinMeetCl A#) is TopSpace-like
proof
  let X be set;
  let A be Subset-Family of X;
  per cases;
  suppose
A1: X = {};
    set T = TopStruct (#X, UniCl FinMeetCl A#);
    the carrier of T in FinMeetCl A & FinMeetCl A c= UniCl FinMeetCl A by
CANTOR_1:1,8;
    hence the carrier of T in the topology of T;
    hence for a being Subset-Family of T st a c= the topology of T holds union
    a in the topology of T by A1;
    thus thesis by A1;
  end;
  suppose
    X <> {};
    hence thesis by CANTOR_1:15;
  end;
end;

definition
  let I be set;
  let J be TopStruct-yielding non-Empty ManySortedSet of I;
  func product J -> strict TopSpace means
  :Def3:
  the carrier of it = product Carrier J & product_prebasis J is prebasis of it;
  existence
  proof
    set X = product Carrier J;
    reconsider A = product_prebasis J as Subset-Family of X;
    consider T being strict TopStruct such that
A1: T = TopStruct (# X, UniCl FinMeetCl A #);
    reconsider T as strict TopSpace by A1,Th3;
    take T;
    thus the carrier of T = product Carrier J by A1;
    now
      assume {} in rng Carrier J;
      then consider i being object such that
A2:   i in dom Carrier J and
A3:   {} = (Carrier J).i by FUNCT_1:def 3;
      consider R being 1-sorted such that
A4:   R = J.i and
A5:   {} = the carrier of R by A2,A3,PRALG_1:def 13;
      dom J = I by PARTFUN1:def 2;
      then R in rng J by A2,A4,FUNCT_1:def 3;
      then reconsider R as non empty 1-sorted by WAYBEL_3:def 7;
      the carrier of R = {} by A5;
      hence contradiction;
    end;
    then X is non empty by CARD_3:26;
    hence thesis by A1,CANTOR_1:18;
  end;
  uniqueness
  proof
    let T1,T2 be strict TopSpace such that
A6: the carrier of T1 = product Carrier J and
A7: product_prebasis J is prebasis of T1 and
A8: the carrier of T2 = product Carrier J and
A9: product_prebasis J is prebasis of T2;
    now
      assume {} in rng Carrier J;
      then consider i being object such that
A10:  i in dom Carrier J and
A11:  {} = (Carrier J).i by FUNCT_1:def 3;
      consider R being 1-sorted such that
A12:  R = J.i and
A13:  {} = the carrier of R by A10,A11,PRALG_1:def 13;
      dom J = I by PARTFUN1:def 2;
      then R in rng J by A10,A12,FUNCT_1:def 3;
      then reconsider R as non empty 1-sorted by WAYBEL_3:def 7;
      the carrier of R = {} by A13;
      hence contradiction;
    end;
    then product Carrier J <> {} by CARD_3:26;
    then reconsider t1 = T1, t2 = T2 as non empty TopSpace by A6,A8;
    t1 = t2 by A6,A7,A8,A9,CANTOR_1:17;
    hence thesis;
  end;
end;

registration
  let I be set;
  let J be TopStruct-yielding non-Empty ManySortedSet of I;
  cluster product J -> non empty;
  coherence
  proof
A1: now
      assume {} in rng Carrier J;
      then consider i being object such that
A2:   i in dom Carrier J and
A3:   {} = (Carrier J).i by FUNCT_1:def 3;
      consider R being 1-sorted such that
A4:   R = J.i and
A5:   {} = the carrier of R by A2,A3,PRALG_1:def 13;
      dom J = I by PARTFUN1:def 2;
      then R in rng J by A2,A4,FUNCT_1:def 3;
      then reconsider R as non empty 1-sorted by WAYBEL_3:def 7;
      the carrier of R = {} by A5;
      hence contradiction;
    end;
    the carrier of product J = product Carrier J by Def3;
    then the carrier of product J <> {} by A1,CARD_3:26;
    hence thesis;
  end;
end;

definition
  let I be non empty set;
  let J be TopStruct-yielding non-Empty ManySortedSet of I;
  let i be Element of I;
  redefine func J.i -> non empty TopStruct;
  coherence
  proof
    dom J = I by PARTFUN1:def 2;
    then J.i in rng J by FUNCT_1:def 3;
    hence thesis by WAYBEL_3:def 7;
  end;
end;

registration
  let I be set;
  let J be TopStruct-yielding non-Empty ManySortedSet of I;
  cluster product J -> constituted-Functions;
  coherence
  proof
    the carrier of product J = product Carrier J by Def3;
    hence thesis by MONOID_0:80;
  end;
end;

definition
  let I be non empty set;
  let J be TopStruct-yielding non-Empty ManySortedSet of I;
  let x be Element of product J;
  let i be Element of I;
  redefine func x.i -> Element of J.i;
  coherence
  proof
A1: dom Carrier J = I by PARTFUN1:def 2;
    ( ex R being 1-sorted st R = J.i & (Carrier J).i = the carrier of R)&
    the carrier of product J = product Carrier J by Def3,PRALG_1:def 13;
    hence thesis by A1,CARD_3:9;
  end;
end;

definition
  let I be non empty set;
  let J be TopStruct-yielding non-Empty ManySortedSet of I;
  let i be Element of I;
  func proj(J,i) -> Function of product J, J.i equals
  proj(Carrier J,i);
  coherence
  proof
    consider f being Function such that
A1: f = proj (Carrier J,i);
A2: dom f = product Carrier J by A1,CARD_3:def 16
      .= the carrier of product J by Def3;
    rng f c= the carrier of J.i
    proof
      let y be object;
      assume y in rng f;
      then consider x be object such that
A3:   x in dom f and
A4:   y = f.x by FUNCT_1:def 3;
      reconsider x as Element of product J by A2,A3;
      f.x = x.i by A1,A3,CARD_3:def 16;
      hence thesis by A4;
    end;
    hence thesis by A1,A2,FUNCT_2:def 1,RELSET_1:4;
  end;
end;

theorem Th4:
  for I being non empty set, J being TopStruct-yielding non-Empty
ManySortedSet of I, i being Element of I, P being Subset of J.i holds proj(J,i)
  "P = product ((Carrier J) +* (i,P))
proof
  let I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I,
  i be Element of I, P be Subset of J.i;
  set f = (Carrier J) +* (i,P);
A1: dom Carrier J = I by PARTFUN1:def 2;
A2: dom f = dom Carrier J by FUNCT_7:30
    .= I by PARTFUN1:def 2;
A3: product f c= proj(J,i)"P
  proof
    let x be object;
    assume x in product f;
    then consider g being Function such that
A4: x = g and
A5: dom g = dom f and
A6: for y being object st y in dom f holds g.y in f.y by CARD_3:def 5;
A7: for j being object st j in dom Carrier J holds g.j in (Carrier J).j
    proof
      let j be object;
      assume j in dom Carrier J;
      then
A8:   j in I;
      then
A9:   ex R being 1-sorted st R = J.j & (Carrier J).j = the carrier of R by
PRALG_1:def 13;
      per cases;
      suppose
A10:    j = i;
        f.i = P by A1,FUNCT_7:31;
        then g.j in P by A2,A6,A10;
        hence thesis by A9,A10;
      end;
      suppose
        j <> i;
        then f.j = (Carrier J).j by FUNCT_7:32;
        hence thesis by A2,A6,A8;
      end;
    end;
    dom g = dom Carrier J by A5,FUNCT_7:30;
    then
A11: g in product Carrier J by A7,CARD_3:9;
    then
A12: g in dom proj(Carrier J,i) by CARD_3:def 16;
    f.i = P by A1,FUNCT_7:31;
    then g.i in P by A2,A6;
    then
A13: proj(Carrier J,i).g in P by A12,CARD_3:def 16;
    g in dom proj(J,i) by A11,CARD_3:def 16;
    hence thesis by A4,A13,FUNCT_1:def 7;
  end;
  proj(J,i)"P c= product f
  proof
    let x be object;
    assume
A14: x in proj(J,i)"P;
    then
A15: x in dom proj(Carrier J,i) by FUNCT_1:def 7;
    then x in product Carrier J;
    then consider g being Function such that
A16: x = g and
A17: dom g = dom Carrier J and
A18: for y being object st y in dom Carrier J holds g.y in (Carrier J).y
    by CARD_3:def 5;
A19: dom g = dom f by A17,FUNCT_7:30;
    for j being object st j in dom f holds g.j in f.j
    proof
      let j be object;
      assume j in dom f;
      then
A20:  g.j in (Carrier J).j by A17,A18,A19;
      per cases;
      suppose
A21:    i = j;
        proj(Carrier J,i).x = g.i by A15,A16,CARD_3:def 16;
        then g.i in P by A14,FUNCT_1:def 7;
        hence thesis by A1,A21,FUNCT_7:31;
      end;
      suppose
        i <> j;
        hence thesis by A20,FUNCT_7:32;
      end;
    end;
    hence thesis by A16,A19,CARD_3:def 5;
  end;
  hence thesis by A3;
end;

theorem Th5:
  for I being non empty set, J being TopStruct-yielding non-Empty
  ManySortedSet of I, i being Element of I holds proj(J,i) is continuous
proof
  let I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I,
  i be Element of I;
A1: for P being Subset of J.i st P is open holds proj(J,i)"P is open
  proof
    let P be Subset of J.i;
    assume
A2: P is open;
    proj(J,i)"P c= product Carrier J
    proof
      let x be object;
      assume x in proj(J,i)"P;
      then x in dom proj(Carrier J,i) by FUNCT_1:def 7;
      hence thesis;
    end;
    then reconsider x = proj(J,i)"P as Subset of product Carrier J;
    product_prebasis J is prebasis of product J by Def3;
    then
A3: product_prebasis J c= the topology of product J by TOPS_2:64;
    x = product ((Carrier J) +* (i,P)) by Th4;
    then proj(J,i)"P in product_prebasis J by A2,Def2;
    hence thesis by A3;
  end;
  [#](J.i) <> {};
  hence thesis by A1,TOPS_2:43;
end;

theorem Th6:
  for X being non empty TopSpace, I being non empty set, J being
TopStruct-yielding non-Empty ManySortedSet of I, f being Function of X, product
  J holds f is continuous iff for i being Element of I holds proj(J,i)*f is
  continuous
proof
  let X be non empty TopSpace, I be non empty set, J be TopStruct-yielding
  non-Empty ManySortedSet of I, f be Function of X, product J;
  set B = product_prebasis J;
  hereby
    assume
A1: f is continuous;
    let i be Element of I;
    proj(J,i) is continuous by Th5;
    hence proj(J,i)*f is continuous by A1,TOPS_2:46;
  end;
  assume
A2: for i being Element of I holds proj(J,i)*f is continuous;
A3: for P being Subset of product J st P in B holds f"P is open
  proof
    let P be Subset of product J;
    reconsider p = P as Subset of product Carrier J by Def3;
    assume P in B;
    then consider
    i being set, T being TopStruct, V being Subset of T such that
A4: i in I and
A5: V is open and
A6: T = J.i and
A7: p = product ((Carrier J) +* (i,V)) by Def2;
    reconsider j = i as Element of I by A4;
    reconsider V as Subset of J.j by A6;
    proj(J,j)*f is continuous & [#](J.j) <> {} by A2;
    then
A8: (proj(J,j)*f)"V is open by A5,A6,TOPS_2:43;
    proj(J,j)"V = p by A7,Th4;
    hence thesis by A8,RELAT_1:146;
  end;
  B is prebasis of product J by Def3;
  hence thesis by A3,YELLOW_9:36;
end;

begin :: Main Part

definition
  let Z be TopStruct;
  attr Z is injective means ::p.121 definition 3.1.

  for X being non empty TopSpace for f being
  Function of X, Z st f is continuous holds for Y being non empty TopSpace st X
is SubSpace of Y ex g being Function of Y,Z st g is continuous & g|(the carrier
  of X) = f;
end;

theorem Th7: ::p.121 lemma 3.2.(i)
  for I being non empty set, J being TopStruct-yielding non-Empty
  ManySortedSet of I st for i being Element of I holds J.i is injective holds
  product J is injective
proof
  let I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I;
  assume
A1: for i being Element of I holds J.i is injective;
  set B = product_prebasis J;
  let X be non empty TopSpace;
  let f be Function of X, product J;
  assume
A2: f is continuous;
  let Y be non empty TopSpace;
  defpred P[object,object] means
   ex i1 being Element of I st i1 = $1 & ex g being
Function of Y, J.i1 st g is continuous & g|(the carrier of X) = proj(J,i1)*f &
  $2 = g;
  assume
A3: X is SubSpace of Y;
A4: for i being object st i in I ex u being object st P[i,u]
  proof
    let i be object;
    assume i in I;
    then reconsider i1 = i as Element of I;
    J.i1 is injective & proj(J,i1)*f is continuous by A1,A2,Th6;
    then consider g being Function of Y, J.i1 such that
A5: g is continuous & g|(the carrier of X) = proj(J,i1)*f by A3;
    take g, i1;
    thus thesis by A5;
  end;
  consider G being Function such that
A6: dom G = I and
A7: for i being object st i in I holds P[i,G.i] from CLASSES1:sch 1(A4);
 G is Function-yielding
  proof
    let j be object;
    assume j in dom G;
    then ex i being Element of I st i = j & ex g being Function of Y, J.i st g
    is continuous & g|(the carrier of X) = proj(J,i)*f & G.j = g by A6,A7;
    hence thesis;
  end;
  then reconsider G as Function-yielding Function;
A8: the carrier of Y c= dom <:G:>
  proof
    let x be object;
    consider i being object such that
A9: i in I by XBOOLE_0:def 1;
    assume
A10: x in the carrier of Y;
A11: for f9 being Function st f9 in rng G holds x in dom f9
    proof
      let f9 be Function;
      assume f9 in rng G;
      then consider k being object such that
A12:  k in dom G and
A13:  f9 = G.k by FUNCT_1:def 3;
      ex i1 being Element of I st i1 = k & ex ff being Function of Y, J.i1
st ff is continuous & ff|(the carrier of X) = proj(J,i1)*f & G.k = ff by A6,A7
,A12;
      hence thesis by A10,A13,FUNCT_2:def 1;
    end;
    consider j being Element of I such that
    j = i and
A14: ex g being Function of Y, J.j st g is continuous & g|(the carrier
    of X) = proj(J,j)*f & G.i = g by A7,A9;
    consider g being Function of Y, J.j such that
    g is continuous and
    g|(the carrier of X) = proj(J,j)*f and
A15: G.i = g by A14;
    g in rng G by A6,A9,A15,FUNCT_1:def 3;
    hence thesis by A11,FUNCT_6:33;
  end;
A16: product rngs G c= product Carrier J
  proof
    let y be object;
    assume y in product rngs G;
    then consider h being Function such that
A17: y = h and
A18: dom h = dom rngs G and
A19: for x being object st x in dom rngs G holds h.x in (rngs G).x
by CARD_3:def 5;
A20: dom h = I by A6,A18,FUNCT_6:60
      .= dom Carrier J by PARTFUN1:def 2;
    for x being object st x in dom Carrier J holds h.x in (Carrier J).x
    proof
      let x be object;
      assume
A21:  x in dom Carrier J;
      then
A22:  x in I;
      then consider i being Element of I such that
A23:  i = x and
A24:  ex g being Function of Y, J.i st g is continuous & g|(the
      carrier of X) = proj(J,i)*f & G.x = g by A7;
A25:  ex R being 1-sorted st R = J.x & (Carrier J).x = the carrier of R by A22,
PRALG_1:def 13;
      consider g being Function of Y, J.i such that
      g is continuous and
      g|(the carrier of X) = proj(J,i)*f and
A26:  G.x = g by A24;
      x in dom G by A6,A21;
      then
A27:  (rngs G).x = rng g by A26,FUNCT_6:22;
      h.x in (rngs G).x by A18,A19,A20,A21;
      hence thesis by A23,A27,A25;
    end;
    hence thesis by A17,A20,CARD_3:def 5;
  end;
  dom <:G:> c= the carrier of Y
  proof
    let x be object;
    assume
A28: x in dom <:G:>;
    consider j being object such that
A29: j in I by XBOOLE_0:def 1;
    consider i being Element of I such that
    i = j and
A30: ex g being Function of Y, J.i st g is continuous & g|(the carrier
    of X) = proj(J,i)*f & G.j = g by A7,A29;
    consider g being Function of Y, J.i such that
    g is continuous and
    g|(the carrier of X) = proj(J,i)*f and
A31: G.j = g by A30;
    g in rng G by A6,A29,A31,FUNCT_1:def 3;
    then x in dom g by A28,FUNCT_6:32;
    hence thesis;
  end;
  then
A32: dom <:G:> = the carrier of Y by A8;
  rng <:G:> c= product rngs G by FUNCT_6:29;
  then
A33: rng <:G:> c= product Carrier J by A16;
  then rng <:G:> c= the carrier of product J by Def3;
  then reconsider
  h = <:G:> as Function of the carrier of Y, the carrier of product
  J by A32,FUNCT_2:def 1,RELSET_1:4;
A34: dom (h|(the carrier of X)) = dom h /\ the carrier of X by RELAT_1:61
    .= (the carrier of Y) /\ the carrier of X by FUNCT_2:def 1
    .= the carrier of X by A3,BORSUK_1:1,XBOOLE_1:28
    .= dom f by FUNCT_2:def 1;
A35: for x being object st x in dom (h|(the carrier of X)) holds (h|(the
  carrier of X)).x = f.x
  proof
    let x be object;
    assume
A36: x in dom (h|(the carrier of X));
    then
A37: x in dom h by RELAT_1:57;
    (h|(the carrier of X)).x in rng (h|(the carrier of X)) by A36,FUNCT_1:def 3
;
    then (h|(the carrier of X)).x in the carrier of product J;
    then (h|(the carrier of X)).x in product Carrier J by Def3;
    then consider z being Function such that
A38: (h|(the carrier of X)).x = z and
A39: dom z = dom Carrier J and
    for i being object st i in dom Carrier J holds z.i in (Carrier J).i by
CARD_3:def 5;
    f.x in rng f by A34,A36,FUNCT_1:def 3;
    then f.x in the carrier of product J;
    then
A40: f.x in product Carrier J by Def3;
    then consider y being Function such that
A41: f.x = y and
A42: dom y = dom Carrier J and
    for i being object st i in dom Carrier J holds y.i in (Carrier J).i by
CARD_3:def 5;
A43: x in the carrier of Y by A37;
    for j being object st j in dom y holds y.j = z.j
    proof
      let j be object;
      assume j in dom y;
      then
A44:  j in I by A42;
      then consider i being Element of I such that
A45:  i = j and
A46:  ex g being Function of Y, J.i st g is continuous & g|(the
      carrier of X) = proj(J,i)*f & G.j = g by A7;
A47:  y in dom proj(Carrier J,i) by A40,A41,CARD_3:def 16;
      consider g being Function of Y, J.i such that
      g is continuous and
A48:  g|(the carrier of X) = proj(J,i)*f and
A49:  G.j = g by A46;
      x in dom h & z = <:G:>.x by A36,A43,A38,FUNCT_1:49,FUNCT_2:def 1;
      hence z.j = g.x by A6,A44,A49,FUNCT_6:34
        .= (proj(J,i)*f).x by A36,A48,FUNCT_1:49
        .= proj(Carrier J,i).y by A36,A41,FUNCT_2:15
        .= y.j by A45,A47,CARD_3:def 16;
    end;
    hence thesis by A41,A42,A38,A39,FUNCT_1:2;
  end;
  reconsider h as Function of Y, product J;
A50: for P being Subset of product J st P in B holds h"P is open
  proof
    let P be Subset of product J;
    reconsider p = P as Subset of product Carrier J by Def3;
    assume P in B;
    then consider
    i being set, T being TopStruct, V being Subset of T such that
A51: i in I and
A52: V is open and
A53: T = J.i and
A54: p = product ((Carrier J) +* (i,V)) by Def2;
    consider j being Element of I such that
A55: j = i and
A56: ex g being Function of Y, J.j st g is continuous & g|(the carrier
    of X) = proj(J,j)*f & G.i = g by A7,A51;
    reconsider V as Subset of J.j by A53,A55;
A57: dom proj(J,j) = product Carrier J by CARD_3:def 16;
    consider g being Function of Y, J.j such that
A58: g is continuous and
    g|(the carrier of X) = proj(J,j)*f and
A59: G.i = g by A56;
A60: dom g = the carrier of Y by FUNCT_2:def 1
      .= dom h by FUNCT_2:def 1;
A61: proj(J,j)"V = p by A54,A55,Th4;
A62: h"P c= g"V
    proof
      let x be object;
      assume
A63:  x in h"P;
      then
A64:  h.x in proj(J,j)"V by A61,FUNCT_1:def 7;
      then h.x in product Carrier J by A57,FUNCT_1:def 7;
      then consider y being Function such that
A65:  h.x = y and
      dom y = dom Carrier J and
      for i being object st i in dom Carrier J holds y.i in (Carrier J).i by
CARD_3:def 5;
      h.x in dom proj(J,j) by A64,FUNCT_1:def 7;
      then proj(J,j).(h.x) = y.j by A65,CARD_3:def 16;
      then
A66:  y.j in V by A64,FUNCT_1:def 7;
      x in dom h by A63,FUNCT_1:def 7;
      then
A67:  g.x = y.j by A6,A55,A59,A65,FUNCT_6:34;
      x in dom g by A60,A63,FUNCT_1:def 7;
      hence thesis by A66,A67,FUNCT_1:def 7;
    end;
A68: g"V c= h"P
    proof
      let x be object;
      assume
A69:  x in g"V;
      then
A70:  x in dom h by A60,FUNCT_1:def 7;
      then
A71:  h.x in rng h by FUNCT_1:def 3;
      then consider y being Function such that
A72:  h.x = y and
      dom y = dom Carrier J and
      for i being object st i in dom Carrier J holds y.i in (Carrier J).i
by A33,
CARD_3:def 5;
      h.x in product Carrier J by A33,A71;
      then y in dom proj(Carrier J,j) by A72,CARD_3:def 16;
      then
A73:  proj(J,j).(h.x) = y.j by A72,CARD_3:def 16;
      g.x = y.j by A6,A55,A59,A70,A72,FUNCT_6:34;
      then proj(J,j).(h.x) in V by A69,A73,FUNCT_1:def 7;
      then h.x in proj(J,j)"V by A33,A57,A71,FUNCT_1:def 7;
      hence thesis by A61,A70,FUNCT_1:def 7;
    end;
    [#](J.j) <> {};
    then g"V is open by A52,A53,A55,A58,TOPS_2:43;
    hence thesis by A62,A68,XBOOLE_0:def 10;
  end;
  take h;
  B is prebasis of product J by Def3;
  hence h is continuous by A50,YELLOW_9:36;
  thus thesis by A34,A35,FUNCT_1:2;
end;

theorem ::p.121 lemma 3.2.(ii)
  for T being non empty TopSpace st T is injective for S being non empty
  SubSpace of T st S is_a_retract_of T holds S is injective
proof
  let T be non empty TopSpace;
  assume
A1: T is injective;
  let S be non empty SubSpace of T;
  set p = incl S;
  assume S is_a_retract_of T;
  then consider r being continuous Function of T,S such that
A2: r is being_a_retraction by BORSUK_1:def 17;
  let X be non empty TopSpace, F be Function of X, S;
  assume
A3: F is continuous;
  reconsider f = p*F as Function of X,T;
  let Y be non empty TopSpace;
  assume
A4: X is SubSpace of Y;
  p is continuous by TMAP_1:87;
  then consider g be Function of Y,T such that
A5: g is continuous and
A6: g|(the carrier of X) = f by A1,A3,A4;
  take G = r*g;
A7: the carrier of S c= the carrier of T by BORSUK_1:1;
A8: the carrier of X c= the carrier of Y by A4,BORSUK_1:1;
A9: for x being object st x in dom F holds F.x = G.x
  proof
    let x be object;
    assume
A10: x in dom F;
    then
A11: x in the carrier of X & g.x = f.x by A6,FUNCT_1:49;
A12: F.x in rng F by A10,FUNCT_1:def 3;
    then F.x in the carrier of S;
    then reconsider y = F.x as Point of T by A7;
A13: f.x = p.y by A10,FUNCT_2:15
      .= F.x by A12,TMAP_1:84;
    F.x = r.y by A2,A12,BORSUK_1:def 16;
    hence thesis by A8,A13,A11,FUNCT_2:15;
  end;
  thus G is continuous by A5;
A14: dom F = the carrier of X by FUNCT_2:def 1;
  dom G /\ the carrier of X = (the carrier of Y) /\ the carrier of X by
FUNCT_2:def 1
    .= the carrier of X by A4,BORSUK_1:1,XBOOLE_1:28;
  hence thesis by A14,A9,FUNCT_1:46;
end;

definition
  let X be 1-sorted, Y be TopStruct, f be Function of X,Y;
  func Image f -> SubSpace of Y equals
  Y|(rng f);
  coherence;
end;

registration
  let X be non empty 1-sorted, Y be non empty TopStruct, f be Function of X,Y;
  cluster Image f -> non empty;
  coherence;
end;

theorem Th9:
  for X being 1-sorted, Y being TopStruct, f being Function of X,Y
  holds the carrier of Image f = rng f
proof
  let X be 1-sorted,Y be TopStruct, f be Function of X,Y;
  thus the carrier of Image f = [#](Y|(rng f)) .= rng f by PRE_TOPC:def 5;
end;

definition
  let X be 1-sorted, Y be non empty TopStruct, f be Function of X,Y;
  func corestr(f) -> Function of X,Image f equals
  f;
  coherence
  proof
    the carrier of Image f = rng f & the carrier of X = dom f by Th9,
FUNCT_2:def 1;
    hence thesis by FUNCT_2:1;
  end;
end;

theorem Th10:
  for X, Y being non empty TopSpace, f being Function of X,Y st f
  is continuous holds corestr f is continuous
proof
  let X, Y be non empty TopSpace;
  let f be Function of X,Y;
A1: f is Function of dom f,rng f by FUNCT_2:1;
A2: [#]Y <> {};
  assume
A3: f is continuous;
A4: for R being Subset of Image f st R is open holds (corestr f)"R is open
  proof
    [#](Image f) = rng f by Th9;
    then
A5: f"([#](Image f)) = dom f by A1,FUNCT_2:40
      .= the carrier of X by FUNCT_2:def 1;
    the carrier of X in the topology of X by PRE_TOPC:def 1;
    then
A6: f"([#](Image f)) is open by A5;
    let R be Subset of Image f;
    assume R is open;
    then R in the topology of Image f;
    then consider Q being Subset of Y such that
A7: Q in the topology of Y and
A8: R = Q /\ [#](Image f) by PRE_TOPC:def 4;
    reconsider Q as Subset of Y;
    Q is open by A7;
    then
A9: f"Q is open by A3,A2,TOPS_2:43;
    f"Q /\ f"([#](Image f)) = f"(Q /\ [#](Image f)) by FUNCT_1:68;
    hence thesis by A8,A9,A6,TOPS_1:11;
  end;
  [#]Image f <> {};
  hence thesis by A4,TOPS_2:43;
end;

registration
  let X be 1-sorted,Y be non empty TopStruct;
  let f be Function of X,Y;
  cluster corestr f -> onto;
  coherence
  proof
    the carrier of Image f = rng corestr f by Th9;
    hence thesis by FUNCT_2:def 3;
  end;
end;

definition
  let X,Y be TopStruct;
  pred X is_Retract_of Y means
  ex f being Function of Y,Y st f is continuous &
  f*f = f & Image f, X are_homeomorphic;
end;

theorem Th11: ::p.121 lemma 3.2.(iii)
  for T,S being non empty TopSpace st T is injective for f being
  Function of T,S st corestr(f) is being_homeomorphism holds T is_Retract_of S
proof
  let T,S be non empty TopSpace;
  assume
A1: T is injective;
  let f be Function of T,S;
  consider g being Function of Image f, T such that
A2: g = (corestr f)";
  assume
A3: corestr(f) is being_homeomorphism;
  then g is continuous by A2,TOPS_2:def 5;
  then consider h being Function of S,T such that
A4: h is continuous and
A5: h|(the carrier of Image f) = g by A1;
  g is being_homeomorphism by A3,A2,TOPS_2:56;
  then
A6: g is one-to-one by TOPS_2:def 5;
A7: the carrier of Image f = rng f by Th9;
A8: for x being object st x in the carrier of T holds (h*f).x = x
  proof
    let x be object;
    assume
A9: x in the carrier of T;
    then
A10: x in dom (corestr f) by FUNCT_2:def 1;
A11: x in dom f by A9,FUNCT_2:def 1;
    then
A12: f.x in rng f by FUNCT_1:def 3;
A13: corestr f is one-to-one by A3,TOPS_2:def 5;
    thus (h*f).x = h.(f.x) by A11,FUNCT_1:13
      .= ((corestr f)").((corestr f).x) by A2,A5,A7,A12,FUNCT_1:49
      .= ((corestr f qua Function)").((corestr f).x) by A13,TOPS_2:def 4
      .= x by A10,A13,FUNCT_1:34;
  end;
  dom (h*f) = the carrier of T by FUNCT_2:def 1;
  then
A14: h*f = id (the carrier of T) by A8,FUNCT_1:17;
  take F = f*h;
  set H = h*(incl Image F);
A15: dom H = [#](Image F) by FUNCT_2:def 1;
  rng h c= the carrier of T;
  then
A16: rng h c= dom f by FUNCT_2:def 1;
A17: rng F c= rng f
  proof
    let y be object;
    assume y in rng F;
    then consider x being object such that
A18: x in dom F and
A19: y = F.x by FUNCT_1:def 3;
    x in the carrier of S by A18;
    then
A20: x in dom h by FUNCT_2:def 1;
    then
A21: h.x in rng h by FUNCT_1:def 3;
    f.(h.x) = y by A19,A20,FUNCT_1:13;
    hence thesis by A16,A21,FUNCT_1:def 3;
  end;
A22: H is one-to-one
  proof
    let x,y be Element of Image F;
    assume
A23: H.x = H.y;
A24: x in the carrier of Image F;
    then
A25: x in dom (incl Image F) by FUNCT_2:def 1;
A26: y in the carrier of Image F;
    then
A27: y in dom (incl Image F) by FUNCT_2:def 1;
A28: y in rng F by A26,Th9;
A29: x in rng F by A24,Th9;
    then reconsider a = x, b = y as Point of S by A28;
    reconsider x9 = x, y9 = y as Element of Image f by A17,A29,A28,Th9;
    g.x9 = h.x by A5,FUNCT_1:49
      .= h.((incl Image F).a) by TMAP_1:84
      .= (h*(incl Image F)).b by A23,A25,FUNCT_1:13
      .= h.((incl Image F).b) by A27,FUNCT_1:13
      .= h.y by TMAP_1:84
      .= g.y9 by A5,FUNCT_1:49;
    hence thesis by A6;
  end;
A30: dom incl Image F = the carrier of Image F by FUNCT_2:def 1;
A31: rng H = [#]T
  proof
    thus rng H c= [#](T);
    let y be object;
    assume
A32: y in [#](T);
    then
A33: y in dom f by FUNCT_2:def 1;
    then
A34: F.(f.y) = ((f*h)*f).y by FUNCT_1:13
      .= (f*id T).y by A14,RELAT_1:36
      .= f.y by FUNCT_2:17;
A35: f.y in rng f by A33,FUNCT_1:def 3;
    then reconsider pp = f.y as Point of S;
    f.y in the carrier of S by A35;
    then
A36: f.y in dom F by FUNCT_2:def 1;
    then F.(f.y) in rng F by FUNCT_1:def 3;
    then
A37: f.y in the carrier of Image F by A34,Th9;
    then
A38: y in dom((incl Image F)*f) by A30,A33,FUNCT_1:11;
    dom H = rng F by A15,Th9;
    then
A39: f.y in dom H by A36,A34,FUNCT_1:def 3;
    H.(f.y) = ((h*(incl Image F))*f).y by A33,FUNCT_1:13
      .= (h*((incl Image F)*f)).y by RELAT_1:36
      .= h.(((incl Image F)*f).y) by A38,FUNCT_1:13
      .= h.((incl Image F).pp) by A33,FUNCT_1:13
      .= h.(f.y) by A37,TMAP_1:84
      .= (id T).y by A14,A33,FUNCT_1:13
      .= y by A32,FUNCT_1:18;
    hence thesis by A39,FUNCT_1:def 3;
  end;
  reconsider p = incl(Image f) as Function of Image f,S;
A40: [#]S <> {};
A41: dom (p*(corestr f)) = the carrier of T by FUNCT_2:def 1
    .= dom f by FUNCT_2:def 1;
A42: for P being Subset of S holds f"P = (p*(corestr f))"P
  proof
    let P be Subset of S;
    hereby
      let x be object;
      assume
A43:  x in f"P;
      then
A44:  x in dom f by FUNCT_1:def 7;
      then f.x in rng f by FUNCT_1:def 3;
      then
A45:  f.x in the carrier of Image f by Th9;
A46:  f.x in P by A43,FUNCT_1:def 7;
      then reconsider y = f.x as Point of S;
      (p*(corestr f)).x = p.(f.x) by A44,FUNCT_1:13
        .= y by A45,TMAP_1:84;
      hence x in (p*(corestr f))"P by A41,A44,A46,FUNCT_1:def 7;
    end;
    let x be object;
    assume
A47: x in (p*(corestr f))"P;
    then
A48: x in dom(p*(corestr f)) by FUNCT_1:def 7;
    then
A49: f.x in rng f by A41,FUNCT_1:def 3;
    then reconsider y = f.x as Point of S;
A50: (p*(corestr f)).x in P by A47,FUNCT_1:def 7;
A51: f.x in the carrier of Image f by A49,Th9;
    (p*(corestr f)).x = p.(f.x) by A41,A48,FUNCT_1:13
      .= y by A51,TMAP_1:84;
    hence thesis by A41,A48,A50,FUNCT_1:def 7;
  end;
A52: corestr(f) is continuous by A3,TOPS_2:def 5;
A53: for P being Subset of Image F st P is open holds (H")"P is open
  proof
    let P be Subset of Image F;
A54: p is continuous by TMAP_1:87;
    (incl Image F).:P = P
    proof
      hereby
        let y be object;
        assume y in (incl Image F).:P;
        then consider x being object such that
A55:    x in dom (incl Image F) and
A56:    x in P & y = (incl Image F).x by FUNCT_1:def 6;
        x in the carrier of Image F by A55;
        then x in rng F by Th9;
        then reconsider xx = x as Point of S;
        (incl Image F).xx = x by A55,TMAP_1:84;
        hence y in P by A56;
      end;
      let y be object;
      assume
A57:  y in P;
      then
A58:  y in the carrier of Image F;
      then y in rng F by Th9;
      then reconsider yy = y as Point of S;
A59:  yy = (incl Image F).y by A57,TMAP_1:84;
      y in dom (incl Image F) by A58,FUNCT_2:def 1;
      hence thesis by A57,A59,FUNCT_1:def 6;
    end;
    then
A60: H.:P = h.:P by RELAT_1:126;
    assume P is open;
    then P in the topology of Image F;
    then consider Q being Subset of S such that
A61: Q in the topology of S and
A62: P = Q /\ [#](Image F) by PRE_TOPC:def 4;
    reconsider Q as Subset of S;
A63: f"Q = h.:P
    proof
      hereby
        let x be object;
        assume
A64:    x in f"Q;
        then
A65:    x in dom f by FUNCT_1:def 7;
        then
A66:    h.(f.x) = (id T).x by A14,FUNCT_1:13
          .= x by A64,FUNCT_1:18;
        f.x in rng f by A65,FUNCT_1:def 3;
        then
A67:    f.x in the carrier of S;
        then
A68:    f.x in dom h by FUNCT_2:def 1;
A69:    f.x in dom F by A67,FUNCT_2:def 1;
        F.(f.x) = f.(h.(f.x)) by A68,FUNCT_1:13
          .= f.((id T).x) by A14,A65,FUNCT_1:13
          .= f.x by A64,FUNCT_1:18;
        then f.x in rng F by A69,FUNCT_1:def 3;
        then
A70:    f.x in the carrier of Image F by Th9;
        f.x in Q by A64,FUNCT_1:def 7;
        then f.x in P by A62,A70,XBOOLE_0:def 4;
        hence x in h.:P by A68,A66,FUNCT_1:def 6;
      end;
      let x be object;
      assume x in h.:P;
      then consider y being object such that
A71:  y in dom h and
A72:  y in P and
A73:  x = h.y by FUNCT_1:def 6;
A74:  y in Q by A62,A72,XBOOLE_0:def 4;
      y in the carrier of Image F by A72;
      then
A75:  y in rng F by Th9;
A76:  x in rng h by A71,A73,FUNCT_1:def 3;
      then f.x in rng f by A16,FUNCT_1:def 3;
      then reconsider a = f.x, b = y as Element of Image f by A17,A75,Th9;
      g.a = h.(f.x) by A5,FUNCT_1:49
        .= (id T).x by A16,A14,A76,FUNCT_1:13
        .= h.y by A73,A76,FUNCT_1:18
        .= g .b by A5,FUNCT_1:49;
      then f.x in Q by A6,A74;
      hence thesis by A16,A76,FUNCT_1:def 7;
    end;
    Q is open by A61;
    then (p*(corestr f))"Q is open by A40,A52,A54,TOPS_2:43;
    then f"Q is open by A42;
    hence thesis by A31,A22,A63,A60,TOPS_2:54;
  end;
A77: p is continuous by TMAP_1:87;
A78: [#]T <> {};
  for P being Subset of S st P is open holds F"P is open
  proof
    let P be Subset of S;
    assume P is open;
    then (p*(corestr f))"P is open by A40,A52,A77,TOPS_2:43;
    then f"P is open by A42;
    then h"(f"P) is open by A78,A4,TOPS_2:43;
    hence thesis by RELAT_1:146;
  end;
  hence F is continuous by A40,TOPS_2:43;
  thus F*F = (f*h*f)*h by RELAT_1:36
    .= f*(id T)*h by A14,RELAT_1:36
    .= F by FUNCT_2:17;
  [#]Image F <> {};
  then incl Image F is continuous & H" is continuous by A53,TMAP_1:87,TOPS_2:43
;
  then H is being_homeomorphism by A4,A15,A31,A22,TOPS_2:def 5;
  hence thesis by T_0TOPSP:def 1;
end;

definition
  func Sierpinski_Space -> strict TopStruct means
  :Def9:
  the carrier of it = {0,1} & the topology of it = {{}, {1}, {0,1}};
  existence
  proof
    set c = {0,1}, t = {{}, {1}, {0,1} };
    t c= bool c
    proof
      let x be object;
      reconsider xx=x as set by TARSKI:1;
      assume
A1:   x in t;
      per cases by A1,ENUMSET1:def 1;
      suppose
A2:     x = {};
        {} c= c;
        hence thesis by A2;
      end;
      suppose
        x = {1};
        then xx c= c by ZFMISC_1:7;
        hence thesis;
      end;
      suppose
        x = {0,1};
        then xx c= c;
        hence thesis;
      end;
    end;
    then reconsider t as Subset-Family of c;
    take s = TopStruct (# c, t #);
    thus the carrier of s = {0,1};
    thus thesis;
  end;
  uniqueness;
end;

registration
  cluster Sierpinski_Space -> non empty TopSpace-like;
  coherence
  proof
    set IT = Sierpinski_Space;
    thus IT is non empty by Def9;
    {0,1} in {{}, {1}, {0,1} } by ENUMSET1:def 1;
    then the carrier of IT in {{}, {1}, {0,1} } by Def9;
    hence the carrier of IT in the topology of IT by Def9;
    thus for a being Subset-Family of IT st a c= the topology of IT holds
    union a in the topology of IT
    proof
      let a be Subset-Family of IT;
      assume a c= the topology of IT;
      then
A1:   a c= {{}, {1}, {0,1} } by Def9;
      per cases by A1,ZFMISC_1:118;
      suppose
        a = {};
        then union a in {{}, {1}, {0,1} } by ENUMSET1:def 1,ZFMISC_1:2;
        hence thesis by Def9;
      end;
      suppose
        a = {{}};
        then union a = {} by ZFMISC_1:25;
        then union a in {{}, {1}, {0,1} } by ENUMSET1:def 1;
        hence thesis by Def9;
      end;
      suppose
        a = {{1}};
        then union a = {1} by ZFMISC_1:25;
        then union a in {{}, {1}, {0,1} } by ENUMSET1:def 1;
        hence thesis by Def9;
      end;
      suppose
        a = {{0,1}};
        then union a = {0,1} by ZFMISC_1:25;
        then union a in {{}, {1}, {0,1} } by ENUMSET1:def 1;
        hence thesis by Def9;
      end;
      suppose
        a = {{},{1}};
        then union a = {} \/ {1} by ZFMISC_1:75;
        then union a in {{}, {1}, {0,1} } by ENUMSET1:def 1;
        hence thesis by Def9;
      end;
      suppose
        a = {{1},{0,1}};
        then union a = {1} \/ {0,1} by ZFMISC_1:75
          .= {0,1} by ZFMISC_1:9;
        then union a in {{} , {1}, {0,1}} by ENUMSET1:def 1;
        hence thesis by Def9;
      end;
      suppose
        a = {{},{0,1}};
        then union a = {} \/ {0,1} by ZFMISC_1:75;
        then union a in {{}, {1}, {0,1} } by ENUMSET1:def 1;
        hence thesis by Def9;
      end;
      suppose
        a = {{},{1},{0,1}};
        then a = {{} } \/ {{1},{0,1}} by ENUMSET1:2;
        then union a = union {{}} \/ union {{1},{0,1}} by ZFMISC_1:78
          .= {} \/ union {{1},{0,1}} by ZFMISC_1:25
          .= {1} \/ {0,1} by ZFMISC_1:75
          .= {0,1} by ZFMISC_1:9;
        then union a in {{}, {1}, {0,1} } by ENUMSET1:def 1;
        hence thesis by Def9;
      end;
    end;
    let a,b be Subset of IT;
    assume a in the topology of IT & b in the topology of IT;
    then
A2: a in {{}, {1}, {0,1} } & b in {{}, {1}, {0,1} } by Def9;
    per cases by A2,ENUMSET1:def 1;
    suppose
      a = {} & b = {};
      then a /\ b in {{}, {1}, {0,1} } by ENUMSET1:def 1;
      hence thesis by Def9;
    end;
    suppose
      a = {} & b = {1};
      then a /\ b in {{}, {1}, {0,1} } by ENUMSET1:def 1;
      hence thesis by Def9;
    end;
    suppose
      a = {} & b = {0,1};
      then a /\ b in {{}, {1}, {0,1} } by ENUMSET1:def 1;
      hence thesis by Def9;
    end;
    suppose
      a = {1} & b = {};
      then a /\ b in {{}, {1}, {0,1} } by ENUMSET1:def 1;
      hence thesis by Def9;
    end;
    suppose
      a = {1} & b = {1};
      then a /\ b in {{}, {1}, {0,1} } by ENUMSET1:def 1;
      hence thesis by Def9;
    end;
    suppose
      a = {1} & b = {0,1};
      then a /\ b = {1} by ZFMISC_1:13;
      then a /\ b in {{}, {1}, {0,1} } by ENUMSET1:def 1;
      hence thesis by Def9;
    end;
    suppose
      a = {0,1} & b = {};
      then a /\ b in {{}, {1}, {0,1} } by ENUMSET1:def 1;
      hence thesis by Def9;
    end;
    suppose
      a = {0,1} & b = {1};
      then a /\ b = {1} by ZFMISC_1:13;
      then a /\ b in {{}, {1}, {0,1} } by ENUMSET1:def 1;
      hence thesis by Def9;
    end;
    suppose
      a = {0,1} & b = {0,1};
      then a /\ b in {{}, {1}, {0,1} } by ENUMSET1:def 1;
      hence thesis by Def9;
    end;
  end;
end;

Lm1: Sierpinski_Space is T_0
proof
  set S = Sierpinski_Space;
  for x,y being Point of S st x <> y holds ex V being Subset of S st V is
  open & ( x in V & not y in V or y in V & not x in V )
  proof
    set V = {1};
    let x,y be Point of S;
    y in the carrier of S;
    then
A1: y in {0,1} by Def9;
    {1} c= {0,1} by ZFMISC_1:7;
    then reconsider V as Subset of S by Def9;
    x in the carrier of S;
    then x in {0,1} by Def9;
    then
A2: x = 0 or x = 1 by TARSKI:def 2;
    {1} in {{}, {1}, {0,1} } by ENUMSET1:def 1;
    then {1} in the topology of S by Def9;
    then
A3: V is open;
    assume
A4: x <> y;
    per cases by A4,A1,A2,TARSKI:def 2;
    suppose
      x = 0 & y = 1;
      then x in V & not y in V or y in V & not x in V by TARSKI:def 1;
      hence thesis by A3;
    end;
    suppose
      x = 1 & y = 0;
      then x in V & not y in V or y in V & not x in V by TARSKI:def 1;
      hence thesis by A3;
    end;
  end;
  hence thesis;
end;

registration
  cluster Sierpinski_Space -> T_0;
  coherence by Lm1;
end;

registration ::p.122 lemma 3.3.
  cluster Sierpinski_Space -> injective;
  coherence
  proof
    let X be non empty TopSpace;
    set S = Sierpinski_Space;
    let f be Function of X, S;
A1: [#]S <> {};
    {1} c= {0,1} by ZFMISC_1:7;
    then reconsider u = {1} as Subset of S by Def9;
    u in {{}, {1}, {0,1}} by ENUMSET1:def 1;
    then u in the topology of S by Def9;
    then
A2: u is open;
    assume f is continuous;
    then f"u is open by A1,A2,TOPS_2:43;
    then
A3: f"u in the topology of X;
    let Y be non empty TopSpace;
    assume
A4: X is SubSpace of Y;
    then consider V being Subset of Y such that
A5: V in the topology of Y and
A6: f"u = V /\ [#](X) by A3,PRE_TOPC:def 4;
    reconsider V as Subset of Y;
    set g = chi(V,the carrier of Y);
A7: dom g = the carrier of Y by FUNCT_3:def 3;
    reconsider g as Function of Y,S by Def9;
A8: the carrier of X c= the carrier of Y by A4,BORSUK_1:1;
A9: for x being object st x in dom f holds f.x = g.x
    proof
      let x be object;
      assume
A10:  x in dom f;
      then
A11:  x in the carrier of X;
      per cases;
      suppose
A12:    x in V;
        then x in f"u by A6,A10,XBOOLE_0:def 4;
        then
A13:    f.x in {1} by FUNCT_1:def 7;
        g.x = 1 by A12,FUNCT_3:def 3;
        hence thesis by A13,TARSKI:def 1;
      end;
      suppose
A14:    not x in V;
        f.x in rng f by A10,FUNCT_1:def 3;
        then f.x in the carrier of S;
        then f.x in {0,1} by Def9;
        then
A15:    f.x = 0 or f.x = 1 by TARSKI:def 2;
        not x in f"{1} by A6,A14,XBOOLE_0:def 4;
        then not x in dom f or not f.x in {1} by FUNCT_1:def 7;
        hence thesis by A8,A10,A11,A14,A15,FUNCT_3:def 3,TARSKI:def 1;
      end;
    end;
    take g;
A16: V is open by A5;
    for P being Subset of S st P is open holds g"P is open
    proof
      let P be Subset of S;
      assume P is open;
      then P in the topology of S;
      then
A17:  P in {{}, {1}, {0,1} } by Def9;
      per cases by A17,ENUMSET1:def 1;
      suppose
        P = {};
        then g"P = {};
        then g"P in the topology of Y by PRE_TOPC:1;
        hence thesis;
      end;
      suppose
A18:    P = {1};
A19:    g"P c= V
        proof
          let x be object;
          assume
A20:      x in g"P;
          then g.x in {1} by A18,FUNCT_1:def 7;
          then g.x = 1 by TARSKI:def 1;
          hence thesis by A20,FUNCT_3:def 3;
        end;
        V c= g"P
        proof
          let x be object;
          assume
A21:      x in V;
          then g.x = 1 by FUNCT_3:def 3;
          then g.x in {1} by TARSKI:def 1;
          hence thesis by A7,A18,A21,FUNCT_1:def 7;
        end;
        hence thesis by A16,A19,XBOOLE_0:def 10;
      end;
      suppose
        P = {0,1};
        then g"P = the carrier of Y by FUNCT_2:40;
        then g"P in the topology of Y by PRE_TOPC:def 1;
        hence thesis;
      end;
    end;
    hence g is continuous by A1,TOPS_2:43;
    dom g /\ (the carrier of X) = (the carrier of Y) /\ (the carrier of X
    ) by FUNCT_3:def 3
      .= the carrier of X by A4,BORSUK_1:1,XBOOLE_1:28
      .= dom f by FUNCT_2:def 1;
    hence thesis by A9,FUNCT_1:46;
  end;
end;

registration
  let I be set;
  let S be non empty 1-sorted;
  cluster I --> S -> non-Empty;
  coherence
  proof
    let s be 1-sorted;
    assume s in rng (I --> S);
    hence thesis by TARSKI:def 1;
  end;
end;

registration
  let I be set;
  let T be TopStruct;
  cluster I --> T -> TopStruct-yielding;
  coherence
  proof
    let x be object;
    assume x in rng (I --> T);
    hence thesis by TARSKI:def 1;
  end;
end;

registration
  let I be non empty set;
  let L be non empty antisymmetric RelStr;
  cluster product (I --> L) -> antisymmetric;
  coherence
  proof
    for i being Element of I holds (I --> L).i is antisymmetric;
    hence thesis by WAYBEL_3:30;
  end;
end;

registration
  let I be non empty set;
  let L be non empty transitive RelStr;
  cluster product (I --> L) -> transitive;
  coherence
  proof
    for i being Element of I holds (I --> L).i is transitive;
    hence thesis by WAYBEL_3:29;
  end;
end;

theorem
  for T being Scott TopAugmentation of BoolePoset {0} holds the topology
  of T = the topology of Sierpinski_Space
proof
  let T be Scott TopAugmentation of BoolePoset {0};
A1: LattPOSet BooleLatt {0} =
     RelStr(#the carrier of BooleLatt {0}, LattRel( BooleLatt {0})#)
     by LATTICE3:def 2;
A2: the RelStr of T = BoolePoset {0} by YELLOW_9:def 4;
  then
A3: the carrier of T = the carrier of LattPOSet BooleLatt {0}
            by YELLOW_1:def 2
    .= bool {0} by A1,LATTICE3:def 1
    .= {0,1} by CARD_1:49,ZFMISC_1:24;
  then reconsider j = {0}, z = 0 as Element of BoolePoset {0}
              by A2,TARSKI:def 2,CARD_1:49;
A4: now
    let x be object;
    assume x in the topology of Sierpinski_Space;
    then
A5: x in {{}, {{0}}, {0,{0}} } by Def9,CARD_1:49;
    per cases by A5,ENUMSET1:def 1,CARD_1:49;
    suppose
      x = {};
      hence x in the topology of T by PRE_TOPC:1;
    end;
    suppose
A6:   x = {{0}};
      then reconsider x9 = x as Subset of T by A3,ZFMISC_1:7,CARD_1:49;
      for a,b being Element of T st a in x9 & a <= b holds b in x9
      proof
        let a,b be Element of T;
        assume that
A7:     a in x9 and
A8:     a <= b;
A9:     a = {0} by A6,A7,TARSKI:def 1;
A10:    b <> 0
        proof
          assume
A11:      b = 0;
          [a, b] in the InternalRel of T by A8,ORDERS_2:def 5;
          then j <= z by A2,A9,A11,ORDERS_2:def 5;
          then {0} c= {} by YELLOW_1:2;
          hence thesis;
        end;
        b = 0 or b = 1 by A3,TARSKI:def 2;
        hence thesis by A6,A10,TARSKI:def 1,CARD_1:49;
      end;
      then
A12:  x9 is upper by WAYBEL_0:def 20;
      for D being non empty directed Subset of T st sup D in x9 holds D
      meets x9
      proof
        let D be non empty directed Subset of T;
        assume
A13:    sup D in x9;
        D <> {0}
        proof
          assume D = {0};
          then sup D = sup {z} by A2,YELLOW_0:17,26
            .= 0 by YELLOW_0:39;
          hence thesis by A6,A13,TARSKI:def 1;
        end;
        then D = {1} or D = {0,1} by A3,ZFMISC_1:36;
        then
A14:    1 in D by TARSKI:def 1,def 2;
        1 in x9 by A6,TARSKI:def 1,CARD_1:49;
        hence thesis by A14,XBOOLE_0:3;
      end;
      then x9 is inaccessible by WAYBEL11:def 1;
      then x9 is open by A12,WAYBEL11:def 4;
      hence x in the topology of T;
    end;
    suppose
      x = {0,1};
      hence x in the topology of T by A3,PRE_TOPC:def 1;
    end;
  end;
  reconsider c = {z} as Subset of T by A2;
  now
    set a = 0, b = {0};
    let y be object;
A15: not b in {z};
    a c= b & a in {z} by TARSKI:def 1;
    then not {z} is upper by A15,WAYBEL_7:7;
    then not c is upper by A2,WAYBEL_0:25;
    then
A16: not c is open by WAYBEL11:def 4;
    assume
A17: y in the topology of T;
    then reconsider x = y as Subset of T;
    x = {} or x = {0} or x = {1} or x = {0,1} by A3,ZFMISC_1:36;
    then y in {{}, {1}, {0,1} } by A17,A16,ENUMSET1:def 1;
    hence y in the topology of Sierpinski_Space by Def9;
  end;
  hence thesis by A4,TARSKI:2;
end;

theorem Th13:
  for I being non empty set holds the set of all product ((Carrier (I -->
  Sierpinski_Space))+*(i,{1})) where i is Element of I is
  prebasis of product (I --> Sierpinski_Space)
proof
  let I be non empty set;
  set IS = I --> Sierpinski_Space, pB = the set of all
 product ((Carrier IS)+*(i,{1})) where i is Element of I;
  set P = product_prebasis IS;
A1: P is prebasis of product IS by Def3;
  then
A2: P c= the topology of product IS by TOPS_2:64;
  pB c= bool the carrier of product IS
  proof
    let x be object;
    reconsider xx=x as set by TARSKI:1;
    assume x in pB;
    then consider i being Element of I such that
A3: x = product ((Carrier IS)+*(i,{1}));
    product ((Carrier IS)+*(i,{1})) c= product Carrier IS
    proof
      let y be object;
      assume y in product ((Carrier IS)+*(i,{1}));
      then consider g being Function such that
A4:   y = g and
A5:   dom g = dom ((Carrier IS)+*(i,{1})) and
A6:   for z being object st z in dom ((Carrier IS)+*(i,{1})) holds g.z in
      ((Carrier IS)+*(i,{1})).z by CARD_3:def 5;
A7:   for z being object st z in dom Carrier IS
holds g.z in ( Carrier IS ) . z
      proof
        let z be object;
        assume
A8:     z in dom (Carrier IS);
        then
A9:     z in I;
        then consider R being 1-sorted such that
A10:    R = IS.z and
A11:    (Carrier IS).z = the carrier of R by PRALG_1:def 13;
A12:    the carrier of R = the carrier of Sierpinski_Space by A9,A10,FUNCOP_1:7
          .= {0,1} by Def9;
        z in dom ((Carrier IS)+*(i,{1})) by A8,FUNCT_7:30;
        then
A13:    g.z in ((Carrier IS)+*(i,{1})).z by A6;
        per cases;
        suppose
          z = i;
          then ((Carrier IS)+*(i,{1})).z = {1} by A8,FUNCT_7:31;
          then g.z = 1 by A13,TARSKI:def 1;
          hence thesis by A11,A12,TARSKI:def 2;
        end;
        suppose
          z <> i;
          hence thesis by A13,FUNCT_7:32;
        end;
      end;
      dom g = dom Carrier IS by A5,FUNCT_7:30;
      hence thesis by A4,A7,CARD_3:def 5;
    end;
    then xx c= the carrier of product IS by A3,Def3;
    hence thesis;
  end;
  then reconsider B = pB as Subset-Family of product IS;
  reconsider B as Subset-Family of product IS;
A14: B c= P
  proof
    {1} c= {0,1} by ZFMISC_1:7;
    then reconsider V = {1} as Subset of Sierpinski_Space by Def9;
    let x be object;
    assume
A15: x in B;
    then consider i being Element of I such that
A16: x = product ((Carrier IS)+*(i,{1}));
    reconsider y = x as Subset of product Carrier IS by A15,Def3;
    {1} in {{}, {1}, {0,1} } by ENUMSET1:def 1;
    then {1} in the topology of Sierpinski_Space by Def9;
    then
A17: V is open;
    Sierpinski_Space = IS.i & y = product ((Carrier IS) +* (i,V)) by A16;
    hence thesis by A17,Def2;
  end;
  reconsider P as Subset-Family of product IS by Def3;
  reconsider P as Subset-Family of product IS;
  FinMeetCl P is Basis of product IS by A1,YELLOW_9:23;
  then reconsider F = (FinMeetCl P) \ {{}} as Basis of product IS by Th2;
A18: F c= FinMeetCl B
  proof
    let x be object;
    assume
A19: x in F;
    then reconsider y = x as Subset of product IS;
    x in FinMeetCl P by A19,XBOOLE_0:def 5;
    then consider Y1 being Subset-Family of product IS such that
A20: Y1 c= P and
A21: Y1 is finite and
A22: y = Intersect Y1 by CANTOR_1:def 3;
    reconsider Y2 = Y1 /\ B as Subset-Family of product IS;
A23: Y2 c= B & Y2 is finite by A21,FINSET_1:1,XBOOLE_1:17;
A24: the carrier of product IS = product Carrier IS by Def3;
A25: not x in {{}} by A19,XBOOLE_0:def 5;
A26: Intersect Y2 c= Intersect Y1
    proof
      let z be object;
      assume
A27:  z in Intersect Y2;
      then
A28:  z in product Carrier IS by A24;
      for Y being set st Y in Y1 holds z in Y
      proof
        let Y be set;
        assume
A29:    Y in Y1;
        then reconsider Y9 = Y as Subset of product Carrier IS by Def3;
        consider i being set, S being TopStruct, V being Subset of S such that
A30:    i in I and
A31:    V is open and
A32:    S = IS.i and
A33:    Y9 = product ((Carrier IS) +* (i,V)) by A20,A29,Def2;
        reconsider V9 = V as Subset of Sierpinski_Space by A30,A32,FUNCOP_1:7;
        V in the topology of S by A31;
        then V9 in the topology of Sierpinski_Space by A30,A32,FUNCOP_1:7;
        then
A34:    V9 in {{}, {1}, {0,1} } by Def9;
A35:    i in dom (Carrier IS) by A30,PARTFUN1:def 2;
A36:    V9 <> {}
        proof
          ((Carrier IS)+*(i,{})).i = {} & i in dom ((Carrier IS)+*(i,{}))
          by A35,FUNCT_7:30,31;
          then
A37:      {} in rng ((Carrier IS)+*(i,{})) by FUNCT_1:def 3;
          assume V9 = {};
          then Y9 = {} by A33,A37,CARD_3:26;
          then y = {} by A22,A29,MSSUBFAM:3;
          hence thesis by A25,TARSKI:def 1;
        end;
        reconsider i9 = i as Element of I by A30;
A38:    ex RR being 1-sorted st RR = IS.i & (Carrier IS).i = the carrier
        of RR by A30,PRALG_1:def 13;
        per cases by A34,A36,ENUMSET1:def 1;
        suppose
          V9 = {1};
          then Y9 = product ((Carrier IS)+*(i9,{1})) by A33;
          then Y in B;
          then Y in Y2 by A29,XBOOLE_0:def 4;
          hence thesis by A27,SETFAM_1:43;
        end;
        suppose
          V9 = {0,1};
          then V9 = the carrier of Sierpinski_Space by Def9
            .= (Carrier IS).i by A30,A38,FUNCOP_1:7;
          hence thesis by A28,A33,FUNCT_7:35;
        end;
      end;
      hence thesis by A27,SETFAM_1:43;
    end;
    Intersect Y1 c= Intersect Y2 by SETFAM_1:44,XBOOLE_1:17;
    then y = Intersect Y2 by A22,A26;
    hence thesis by A23,CANTOR_1:def 3;
  end;
  pB c= the topology of product IS by A14,A2;
  hence thesis by A18,CANTOR_1:def 4,TOPS_2:64;
end;

registration
  let I be non empty set;
  let L be complete LATTICE;
  cluster product (I --> L) -> with_suprema complete;
  coherence
  proof
    reconsider IB = I --> L as RelStr-yielding non-Empty reflexive-yielding
    ManySortedSet of I;
    for i being Element of I holds IB.i is complete LATTICE;
    hence thesis by WAYBEL_3:31;
  end;
end;

registration
  let I be non empty set;
  let X be algebraic lower-bounded LATTICE;
  cluster product (I --> X) -> algebraic;
  coherence
  proof
    set IB = I --> X;
    for i being Element of I holds IB.i is algebraic lower-bounded LATTICE;
    hence thesis by WAYBEL13:25;
  end;
end;

theorem Th14:
  for X being non empty set ex f being Function of BoolePoset X,
product (X --> BoolePoset {0}) st f is isomorphic & for Y being Subset of X
   holds
  f.Y = chi(Y,X)
proof
  let X be non empty set;
  set XB = X --> BoolePoset {0};
  deffunc F(set) = chi($1,X);
  consider f being Function such that
A1: dom f = bool X and
A2: for Y being set st Y in bool X holds f.Y = F(Y) from FUNCT_1:sch 5;
  LattPOSet BooleLatt {0} = RelStr(#the carrier of BooleLatt {0}, LattRel(
    BooleLatt {0})#) by LATTICE3:def 2;
  then
A3: the carrier of BoolePoset{0} = the carrier of BooleLatt{0}
            by YELLOW_1:def 2
    .= bool {{}} by LATTICE3:def 1
    .= {0,1} by CARD_1:49,ZFMISC_1:24;
A4: rng f c= product Carrier XB
  proof
    let y be object;
    assume y in rng f;
    then consider x being object such that
A5: x in dom f & y = f.x by FUNCT_1:def 3;
    reconsider x as set by TARSKI:1;
A6: dom chi(x,X) = X by FUNCT_3:def 3
      .= dom (Carrier XB) by PARTFUN1:def 2;
A7: for z being object st z in dom Carrier XB
holds chi(x,X).z in (Carrier XB).z
    proof
      let z be object;
      assume z in dom (Carrier XB);
      then
A8:   z in X;
      then ex R being 1-sorted st R = XB.z & (Carrier XB).z = the carrier of R
      by PRALG_1:def 13;
      then
A9:   (Carrier XB).z = {0,1} by A3,A8,FUNCOP_1:7;
      per cases;
      suppose
        z in x;
        then chi(x,X).z = 1 by A8,FUNCT_3:def 3;
        hence thesis by A9,TARSKI:def 2;
      end;
      suppose
        not z in x;
        then chi(x,X).z = 0 by A8,FUNCT_3:def 3;
        hence thesis by A9,TARSKI:def 2;
      end;
    end;
    chi(x,X) = y by A1,A2,A5;
    hence thesis by A6,A7,CARD_3:def 5;
  end;
  LattPOSet BooleLatt X = RelStr(#the carrier of BooleLatt X, LattRel(
    BooleLatt X)#) by LATTICE3:def 2;
  then
A10: the carrier of BoolePoset X = the carrier of BooleLatt X by YELLOW_1:def 2
    .= bool X by LATTICE3:def 1;
A11: the carrier of product XB = product Carrier XB by YELLOW_1:def 4;
  then reconsider
  f as Function of BoolePoset X, product (X --> BoolePoset {0}) by A10,A1,A4,
FUNCT_2:def 1,RELSET_1:4;
A12: for A,B being Element of BoolePoset X holds A <= B iff f.A <= f.B
  proof
    let A,B be Element of BoolePoset X;
A13: f.A = chi(A,X) & f.B = chi(B,X) by A10,A2;
    hereby
      assume A <= B;
      then
A14:  A c= B by YELLOW_1:2;
      for i being object st i in X ex R being RelStr, xi,yi being Element of
      R st R = XB.i & xi = chi(A,X).i & yi = chi(B,X).i & xi <= yi
      proof
        let i be object;
        assume
A15:    i in X;
        take R = BoolePoset {0};
        per cases;
        suppose
A16:      i in A;
          reconsider xi = 1, yi = 1 as Element of R by A3,TARSKI:def 2;
          take xi,yi;
          thus R = XB.i by A15,FUNCOP_1:7;
          thus xi = chi(A,X).i by A15,A16,FUNCT_3:def 3;
          thus yi = chi(B,X).i by A14,A15,A16,FUNCT_3:def 3;
          thus xi <= yi;
        end;
        suppose
A17:      not i in A;
          thus thesis
          proof
            per cases;
            suppose
A18:          i in B;
              reconsider xi = 0, yi = 1 as Element of R by A3,TARSKI:def 2;
              take xi,yi;
              thus R = XB.i by A15,FUNCOP_1:7;
              thus xi = chi(A,X).i by A15,A17,FUNCT_3:def 3;
              thus yi = chi(B,X).i by A15,A18,FUNCT_3:def 3;
              xi c= yi;
              hence xi <= yi by YELLOW_1:2;
            end;
            suppose
A19:          not i in B;
              reconsider xi = 0, yi = 0 as Element of R by A3,TARSKI:def 2;
              take xi,yi;
              thus R = XB.i by A15,FUNCOP_1:7;
              thus xi = chi(A,X).i by A15,A17,FUNCT_3:def 3;
              thus yi = chi(B,X).i by A15,A19,FUNCT_3:def 3;
              thus xi <= yi;
            end;
          end;
        end;
      end;
      hence f.A <= f.B by A11,A13,YELLOW_1:def 4;
    end;
    assume f.A <= f.B;
    then consider h1,h2 being Function such that
A20: h1 = f.A and
A21: h2 = f.B and
A22: for i be object st i in X ex R being RelStr, xi,yi being Element of
    R st R = XB.i & xi = h1.i & yi = h2.i & xi <= yi by A11,YELLOW_1:def 4;
    A c= B
    proof
      let i be object;
      assume
A23:  i in A;
      then consider R being RelStr, xi,yi being Element of R such that
A24:  R = XB.i and
A25:  xi = h1.i and
A26:  yi = h2.i and
A27:  xi <= yi by A10,A22;
      reconsider a = xi, b = yi as Element of BoolePoset {0} by A10,A23,A24,
FUNCOP_1:7;
A28:  a <= b by A10,A23,A24,A27,FUNCOP_1:7;
A29:  xi = chi(A,X).i by A10,A2,A20,A25
        .= 1 by A10,A23,FUNCT_3:def 3;
A30:  yi <> 0
      proof
        assume yi = 0;
        then {0} c= 0 by A29,A28,YELLOW_1:2,CARD_1:49;
        hence thesis;
      end;
A31:  R = BoolePoset {0} by A10,A23,A24,FUNCOP_1:7;
      chi(B,X).i = h2.i by A10,A2,A21
        .= 1 by A3,A26,A31,A30,TARSKI:def 2;
      hence thesis by FUNCT_3:36;
    end;
    hence thesis by YELLOW_1:2;
  end;
  product Carrier XB c= rng f
  proof
    let z be object;
    assume z in product Carrier XB;
    then consider g being Function such that
A32: z = g and
A33: dom g = dom (Carrier XB) and
A34: for y being object st y in dom (Carrier XB) holds g.y in (Carrier XB
    ).y by CARD_3:def 5;
    set A = g"{1};
A35: A c= X
    proof
      let a be object;
      assume a in A;
      then a in dom g by FUNCT_1:def 7;
      hence thesis by A33;
    end;
A36: dom chi(A,X) = X by FUNCT_3:def 3
      .= dom g by A33,PARTFUN1:def 2;
    for a being object st a in dom chi(A,X) holds chi(A,X).a = g.a
    proof
      let a be object;
      assume
A37:  a in dom chi(A,X);
      then a in X;
      then a in dom (Carrier XB) by PARTFUN1:def 2;
      then
A38:  g.a in (Carrier XB).a by A34;
      ex R being 1-sorted st R = XB.a & (Carrier XB).a = the carrier of R
      by A37,PRALG_1:def 13;
      then (Carrier XB).a = {0,1} by A3,A37,FUNCOP_1:7;
      then
A39:  g.a = 0 or g.a = 1 by A38,TARSKI:def 2;
      per cases;
      suppose
        a in A;
        then chi(A,X).a = 1 & g.a in {1} by A37,FUNCT_1:def 7,FUNCT_3:def 3;
        hence thesis by TARSKI:def 1;
      end;
      suppose
A40:    not a in A;
        g.a <> 1
        proof
          assume g.a = 1;
          then g.a in {1} by TARSKI:def 1;
          hence thesis by A36,A37,A40,FUNCT_1:def 7;
        end;
        hence thesis by A37,A39,A40,FUNCT_3:def 3;
      end;
    end;
    then z = chi(A,X) by A32,A36,FUNCT_1:2
      .= f.A by A2,A35;
    hence thesis by A1,A35,FUNCT_1:def 3;
  end;
  then
A41: rng f = the carrier of product XB by A11;
  take f;
  for A,B being Element of BoolePoset X st f.A = f.B holds A = B
  proof
    let A, B be Element of BoolePoset X;
    assume
A42: f.A = f.B;
    f.A = chi(A,X) & f.B = chi(B,X) by A10,A2;
    hence thesis by A10,A42,FUNCT_3:38;
  end;
  then f is one-to-one;
  hence f is isomorphic by A41,A12,WAYBEL_0:66;
  thus thesis by A2;
end;

theorem Th15: ::p.122 lemma 3.4.(i)
  for I being non empty set for T being Scott TopAugmentation of
product (I --> BoolePoset {0})
   holds the topology of T = the topology of product
  (I --> Sierpinski_Space)
proof
  let I be non empty set;
  set IB = I --> BoolePoset {0}, IS = I --> Sierpinski_Space;
A1: the carrier of product IB = product Carrier IB by YELLOW_1:def 4;
  LattPOSet BooleLatt{0} = RelStr(#the carrier of BooleLatt{0}, LattRel(
    BooleLatt{0})#) by LATTICE3:def 2;
  then
A2: the carrier of BoolePoset{0} = the carrier of BooleLatt{0}
              by YELLOW_1:def 2
    .= bool {{}} by LATTICE3:def 1
    .= {0,1} by CARD_1:49,ZFMISC_1:24;
A3: for i being object st i in dom Carrier IB holds (Carrier IB).i = (Carrier
  IS).i
  proof
    let i be object;
    assume i in dom Carrier IB;
    then
A4: i in I;
    then consider R1 being 1-sorted such that
A5: R1 = IB.i and
A6: (Carrier IB).i = the carrier of R1 by PRALG_1:def 13;
    consider R2 being 1-sorted such that
A7: R2 = IS.i and
A8: (Carrier IS).i = the carrier of R2 by A4,PRALG_1:def 13;
    the carrier of R1 = {0,1} by A2,A4,A5,FUNCOP_1:7
      .= the carrier of Sierpinski_Space by Def9
      .= the carrier of R2 by A4,A7,FUNCOP_1:7;
    hence thesis by A6,A8;
  end;
  reconsider P = the set of all
product ((Carrier IS)+*(ii,{1})) where ii is Element of I
 as prebasis of product (I --> Sierpinski_Space) by Th13;
  let T be Scott TopAugmentation of product (I --> BoolePoset {0});
A9: dom Carrier IB = I by PARTFUN1:def 2
    .= dom Carrier IS by PARTFUN1:def 2;
  reconsider T9 = T as complete Scott TopLattice;
A10: the RelStr of T = product (I --> BoolePoset {0}) by YELLOW_9:def 4;
  then T9 is algebraic by WAYBEL_8:17;
  then consider R being Basis of T9 such that
A11: R = {uparrow yy where yy is Element of T9 : yy in the carrier of
  CompactSublatt T9} by WAYBEL14:42;
A12: the carrier of T = product Carrier (I --> BoolePoset {0}) by A10,
YELLOW_1:def 4
    .= product Carrier (I --> Sierpinski_Space) by A9,A3,FUNCT_1:2
    .= the carrier of product (I --> Sierpinski_Space) by Def3;
  then reconsider P9 = P as Subset-Family of T;
  consider f being Function of BoolePoset I, product IB such that
A13: f is isomorphic and
A14: for Y being Subset of I holds f.Y = chi(Y,I) by Th14;
A15: Carrier IB = Carrier IS by A9,A3,FUNCT_1:2;
A16: FinMeetCl P c= R
  proof
    deffunc F(object) = product ((Carrier IS)+*($1,{1}));
    let X be object;
    consider F being Function such that
A17: dom F = I and
A18: for e being object st e in I holds F.e = F(e) from FUNCT_1:sch 3;
    assume
A19: X in FinMeetCl P;
    then reconsider X9 = X as Subset of product IS;
    consider ZZ being Subset-Family of product IS such that
A20: ZZ c= P and
A21: ZZ is finite and
A22: X = Intersect ZZ by A19,CANTOR_1:def 3;
    P c= rng F
    proof
      let w be object;
      assume w in P;
      then consider e being Element of I such that
A23:  w = product ((Carrier IS)+*(e,{1}));
      w = F.e by A18,A23;
      hence thesis by A17,FUNCT_1:def 3;
    end;
    then ZZ c= rng F by A20;
    then consider x9 being set such that
A24: x9 c= dom F and
A25: x9 is finite and
A26: F.:x9 = ZZ by A21,ORDERS_1:85;
    reconsider x9 as Subset of I by A17,A24;
    reconsider x = x9 as Element of BoolePoset I by WAYBEL_8:26;
    reconsider y = f.x as Element of product IB;
    set PP = {product ((Carrier IS)+*(i,{1})) where i is Element of I: i in x9
    };
A27: ZZ c= PP
    proof
      let w be object;
      assume w in ZZ;
      then consider e being object such that
A28:  e in dom F and
A29:  e in x9 and
A30:  w = F.e by A26,FUNCT_1:def 6;
      reconsider e as Element of I by A17,A28;
      w = product ((Carrier IS)+*(e,{1})) by A18,A30;
      hence thesis by A29;
    end;
    PP c= ZZ
    proof
      let w be object;
      assume w in PP;
      then consider e being Element of I such that
A31:  w = product ((Carrier IS)+*(e,{1})) and
A32:  e in x9;
      w = F.e by A18,A31;
      hence thesis by A17,A26,A32,FUNCT_1:def 6;
    end;
    then
A33: ZZ = PP by A27;
A34: uparrow y c= X9
    proof
      let z be object;
      assume
A35:  z in uparrow y;
      then reconsider z9 = z as Element of product IB;
      y <= z9 by A35,WAYBEL_0:18;
      then consider h1,h2 being Function such that
A36:  h1 = y and
A37:  h2 = z9 and
A38:  for i be object st i in I ex R being RelStr, xi,yi being Element
      of R st R = IB.i & xi = h1.i & yi = h2.i & xi <= yi by A1,YELLOW_1:def 4;
      z in the carrier of product IB by A35;
      then z in product Carrier IB by YELLOW_1:def 4;
      then
A39:  ex gg being Function st z = gg & dom gg = dom (Carrier IB) & for w
being object st w in dom (Carrier IB) holds gg.w in (Carrier IB).w
by CARD_3:def 5;
A40:  h1 = chi(x,I) by A14,A36;
      for Z being set st Z in ZZ holds z in Z
      proof
        let Z be set;
        assume Z in ZZ;
        then consider j being Element of I such that
A41:    Z = product ((Carrier IS)+*(j,{1})) and
A42:    j in x by A33;
        consider RS being RelStr, xj,yj being Element of RS such that
A43:    RS = IB.j and
A44:    xj = h1.j and
A45:    yj = h2.j and
A46:    xj <= yj by A38;
A47:    RS = BoolePoset {0} by A43;
A48:    xj = 1 by A40,A42,A44,FUNCT_3:def 3;
A49:    yj <> 0
        proof
          assume yj = 0;
          then {0} c= 0 by A46,A48,A47,YELLOW_1:2,CARD_1:49;
          hence thesis;
        end;
        reconsider b = yj as Element of BoolePoset {0} by A43;
A50:    dom ((Carrier IS)+*(j,{1})) = dom (Carrier IS) by FUNCT_7:30
          .= I by PARTFUN1:def 2;
A51:    b in the carrier of BoolePoset {0};
A52:    for w being object st w in dom ((Carrier IS)+*(j,{1})) holds h2.w
        in ((Carrier IS)+*(j,{1})).w
        proof
          let w be object;
          assume w in dom ((Carrier IS)+*(j,{1}));
          then
A53:      w in dom Carrier IS by A50,PARTFUN1:def 2;
          per cases;
          suppose
            w = j;
            then ((Carrier IS)+*(j,{1})).w = {1} & h2.w = 1 by A2,A45,A51,A49
,A53,FUNCT_7:31,TARSKI:def 2;
            hence thesis by TARSKI:def 1;
          end;
          suppose
            w <> j;
            then ((Carrier IS)+*(j,{1})).w =(Carrier IS).w by FUNCT_7:32;
            hence thesis by A15,A39,A37,A53;
          end;
        end;
        dom h2 = dom ((Carrier IS)+*(j,{1})) by A39,A37,A50,PARTFUN1:def 2;
        hence thesis by A37,A41,A52,CARD_3:def 5;
      end;
      hence thesis by A10,A12,A22,A35,SETFAM_1:43;
    end;
A54: X9 c= uparrow y
    proof
      set h1 = chi(x,I);
      let z be object;
      assume
A55:  z in X9;
      then reconsider z9 = z as Element of product IB by A10,A12;
      z in the carrier of product IB by A10,A12,A55;
      then z in product Carrier IB by YELLOW_1:def 4;
      then consider h2 being Function such that
A56:  z = h2 and
      dom h2 = dom (Carrier IB) and
A57:  for w being object st w in dom (Carrier IB) holds h2.w in (
      Carrier IB).w by CARD_3:def 5;
A58:  for i be object st i in I ex R being RelStr, xi,yi being Element of R
      st R = IB.i & xi = h1.i & yi = h2.i & xi <= yi
      proof
        let i be object;
        assume
A59:    i in I;
        then reconsider i9 = i as Element of I;
        ex RB being 1-sorted st RB = IB.i & (Carrier IB).i = the carrier
        of RB by A59,PRALG_1:def 13;
        then
A60:    (Carrier IB).i = {0,1} by A2,A59,FUNCOP_1:7;
        take RS = BoolePoset {0};
A61:    i in dom (Carrier IB) by A59,PARTFUN1:def 2;
        then
A62:    h2.i in (Carrier IB).i by A57;
        per cases;
        suppose
A63:      i in x;
          reconsider xi = 1, yi = 1 as Element of RS by A2,TARSKI:def 2;
          take xi,yi;
          thus RS = IB.i by A59,FUNCOP_1:7;
          thus xi = h1.i by A63,FUNCT_3:def 3;
A64:      ((Carrier IS)+*(i9,{1})).i9 = {1} by A9,A61,FUNCT_7:31;
          product ((Carrier IS)+*(i9,{1})) in ZZ by A33,A63;
          then z in product ((Carrier IS)+*(i9,{1})) by A22,A55,SETFAM_1:43;
          then consider h29 being Function such that
A65:      z = h29 and
          dom h29 = dom ((Carrier IS)+*(i9,{1})) and
A66:      for w being object st w in dom ((Carrier IS)+*(i9,{1})) holds
          h29.w in ((Carrier IS)+*(i9,{1})).w by CARD_3:def 5;
          i9 in dom ((Carrier IS)+*(i9,{1})) by A9,A61,FUNCT_7:30;
          then h29.i9 in ((Carrier IS)+*(i9,{1})).i9 by A66;
          hence yi = h2.i by A56,A65,A64,TARSKI:def 1;
          thus xi <= yi;
        end;
        suppose
A67:      not i in x;
          thus thesis
          proof
            per cases by A60,A62,TARSKI:def 2;
            suppose
A68:          h2.i = 0;
              reconsider xi = 0, yi = 0 as Element of RS by A2,TARSKI:def 2;
              take xi,yi;
              thus RS = IB.i by A59,FUNCOP_1:7;
              thus xi = h1.i by A59,A67,FUNCT_3:def 3;
              thus yi = h2.i by A68;
              thus xi <= yi;
            end;
            suppose
A69:          h2.i = 1;
              reconsider xi = 0, yi = 1 as Element of RS by A2,TARSKI:def 2;
              take xi,yi;
              thus RS = IB.i by A59,FUNCOP_1:7;
              thus xi = h1.i by A59,A67,FUNCT_3:def 3;
              thus yi = h2.i by A69;
              xi c= yi;
              hence xi <= yi by YELLOW_1:2;
            end;
          end;
        end;
      end;
      h1 = y by A14;
      then y <= z9 by A1,A56,A58,YELLOW_1:def 4;
      hence thesis by WAYBEL_0:18;
    end;
    reconsider Y = y as Element of T9 by A10;
    x is compact by A25,WAYBEL_8:28;
    then y is compact by A13,WAYBEL13:28;
    then Y is compact by A10,WAYBEL_8:9;
    then
A70: Y in the carrier of CompactSublatt T9 by WAYBEL_8:def 1;
    uparrow Y = uparrow {Y} by WAYBEL_0:def 18
      .= uparrow {y} by A10,WAYBEL_0:13
      .= uparrow y by WAYBEL_0:def 18;
    then X = uparrow Y by A54,A34,XBOOLE_0:def 10;
    hence thesis by A11,A70;
  end;
A71: rng f = the carrier of product IB by A13,WAYBEL_0:66;
  R c= FinMeetCl P
  proof
    deffunc F(Element of I) = product ((Carrier IS)+*($1,{1}));
    let X be object;
    assume
A72: X in R;
    then consider Y being Element of T9 such that
A73: X = uparrow Y and
A74: Y in the carrier of CompactSublatt T9 by A11;
    reconsider X9 = X as Subset of product IS by A12,A72;
    reconsider y = Y as Element of product IB by A10;
    consider x being object such that
A75: x in dom f and
A76: y = f.x by A71,FUNCT_1:def 3;
    reconsider x as Element of BoolePoset I by A75;
    Y is compact by A74,WAYBEL_8:def 1;
    then y is compact by A10,WAYBEL_8:9;
    then x is compact by A13,A76,WAYBEL13:28;
    then
A77: x is finite by WAYBEL_8:28;
A78: {F(jj) where jj is Element of I: jj in x} is finite from FRAENKEL:sch
    21(A77);
    set ZZ = {product ((Carrier IS)+*(jj,{1})) where jj is Element of I: jj in
    x };
    reconsider x9 = x as Subset of I by WAYBEL_8:26;
A79: ZZ c= P
    proof
      let z be object;
      assume z in ZZ;
      then ex j being Element of I st z = product ((Carrier IS)+*(j, {1})) & j
      in x9;
      hence thesis;
    end;
    then reconsider ZZ as Subset-Family of product IS by XBOOLE_1:1;
A80: uparrow Y = uparrow {Y} by WAYBEL_0:def 18
      .= uparrow {y} by A10,WAYBEL_0:13
      .= uparrow y by WAYBEL_0:def 18;
A81: Intersect ZZ c= X9
    proof
      set h1 = chi(x,I);
      let z be object;
      assume
A82:  z in Intersect ZZ;
      then reconsider z9 = z as Element of product IB by A10,A12;
      z in the carrier of product IB by A10,A12,A82;
      then z in product Carrier IB by YELLOW_1:def 4;
      then consider h2 being Function such that
A83:  z = h2 and
      dom h2 = dom (Carrier IB) and
A84:  for w being object st w in dom (Carrier IB) holds h2.w in (Carrier
      IB).w by CARD_3:def 5;
A85:  for i be object st i in I ex R being RelStr, xi,yi being Element of R
      st R = IB.i & xi = h1.i & yi = h2.i & xi <= yi
      proof
        let i be object;
        assume
A86:    i in I;
        then reconsider i9 = i as Element of I;
        ex RB being 1-sorted st RB = IB.i & (Carrier IB).i = the carrier
        of RB by A86,PRALG_1:def 13;
        then
A87:    (Carrier IB).i = {0,1} by A2,A86,FUNCOP_1:7;
        take RS = BoolePoset {0};
A88:    i in dom (Carrier IB) by A86,PARTFUN1:def 2;
        then
A89:    h2.i in (Carrier IB).i by A84;
        per cases;
        suppose
A90:      i in x;
          reconsider xi = 1, yi = 1 as Element of RS by A2,TARSKI:def 2;
          take xi,yi;
          thus RS = IB.i by A86,FUNCOP_1:7;
          thus xi = h1.i by A86,A90,FUNCT_3:def 3;
A91:      ((Carrier IS)+*(i9,{1})).i9 = {1} by A9,A88,FUNCT_7:31;
          product ((Carrier IS)+*(i9,{1})) in ZZ by A90;
          then z in product ((Carrier IS)+*(i9,{1})) by A82,SETFAM_1:43;
          then consider h29 being Function such that
A92:      z = h29 and
          dom h29 = dom ((Carrier IS)+*(i9,{1})) and
A93:      for w being object st w in dom ((Carrier IS)+*(i9,{1})) holds
          h29.w in ((Carrier IS)+*(i9,{1})).w by CARD_3:def 5;
          i9 in dom ((Carrier IS)+*(i9,{1})) by A9,A88,FUNCT_7:30;
          then h29.i9 in ((Carrier IS)+*(i9,{1})).i9 by A93;
          hence yi = h2.i by A83,A92,A91,TARSKI:def 1;
          thus xi <= yi;
        end;
        suppose
A94:      not i in x;
          thus thesis
          proof
            per cases by A87,A89,TARSKI:def 2;
            suppose
A95:          h2.i = 0;
              reconsider xi = 0, yi = 0 as Element of RS by A2,TARSKI:def 2;
              take xi,yi;
              thus RS = IB.i by A86,FUNCOP_1:7;
              thus xi = h1.i by A86,A94,FUNCT_3:def 3;
              thus yi = h2.i by A95;
              thus xi <= yi;
            end;
            suppose
A96:          h2.i = 1;
              reconsider xi = 0, yi = 1 as Element of RS by A2,TARSKI:def 2;
              take xi,yi;
              thus RS = IB.i by A86,FUNCOP_1:7;
              thus xi = h1.i by A86,A94,FUNCT_3:def 3;
              thus yi = h2.i by A96;
              xi c= yi;
              hence xi <= yi by YELLOW_1:2;
            end;
          end;
        end;
      end;
      h1 = f.x9 by A14
        .= y by A76;
      then y <= z9 by A1,A83,A85,YELLOW_1:def 4;
      hence thesis by A73,A80,WAYBEL_0:18;
    end;
    X9 c= Intersect ZZ
    proof
      let z be object;
      assume
A97:  z in X9;
      then reconsider z9 = z as Element of product IB by A10,A12;
      y <= z9 by A73,A80,A97,WAYBEL_0:18;
      then consider h1,h2 being Function such that
A98:  h1 = y and
A99:  h2 = z9 and
A100: for i be object st i in I ex R being RelStr, xi,yi being Element
      of R st R = IB.i & xi = h1.i & yi = h2.i & xi <= yi by A1,YELLOW_1:def 4;
      z in the carrier of product IB by A10,A12,A97;
      then z in product Carrier IB by YELLOW_1:def 4;
      then
A101: ex gg being Function st z = gg & dom gg = dom (Carrier IB) & for w
being object st w in dom (Carrier IB) holds gg.w in (Carrier IB).w
by CARD_3:def 5;
A102: h1 = f.x9 by A76,A98
        .= chi(x,I) by A14;
      for Z being set st Z in ZZ holds z in Z
      proof
        let Z be set;
        assume Z in ZZ;
        then consider j being Element of I such that
A103:   Z = product ((Carrier IS)+*(j,{1})) and
A104:   j in x;
        consider RS being RelStr, xj,yj being Element of RS such that
A105:   RS = IB.j and
A106:   xj = h1.j and
A107:   yj = h2.j and
A108:   xj <= yj by A100;
        reconsider a = xj, b = yj as Element of BoolePoset{0}
       by A105;
A109:   a <= b by A105,A108;
A110:   xj = 1 by A102,A104,A106,FUNCT_3:def 3;
A111:   yj <> 0
        proof
          assume yj = 0;
          then {0} c= 0 by A110,A109,YELLOW_1:2,CARD_1:49;
          hence thesis;
        end;
A112:   dom ((Carrier IS)+*(j,{1})) = dom (Carrier IS) by FUNCT_7:30
          .= I by PARTFUN1:def 2;
A113:   b in the carrier of BoolePoset{0};
A114:   for w being object st w in dom ((Carrier IS)+*(j,{1})) holds h2.w in
        ((Carrier IS)+*(j,{1})).w
        proof
          let w be object;
          assume w in dom ((Carrier IS)+*(j,{1}));
          then
A115:     w in dom Carrier IS by A112,PARTFUN1:def 2;
          per cases;
          suppose
            w = j;
            then
            ((Carrier IS)+*(j,{1})).w = {1} & h2.w = 1 by A2,A107,A113,A111
,A115,FUNCT_7:31,TARSKI:def 2;
            hence thesis by TARSKI:def 1;
          end;
          suppose
            w <> j;
            then ((Carrier IS)+*(j,{1})).w =(Carrier IS).w by FUNCT_7:32;
            hence thesis by A15,A101,A99,A115;
          end;
        end;
        dom h2 = dom ((Carrier IS)+*(j,{1})) by A101,A99,A112,PARTFUN1:def 2;
        hence thesis by A99,A103,A114,CARD_3:def 5;
      end;
      hence thesis by A97,SETFAM_1:43;
    end;
    then X9 = Intersect ZZ by A81;
    hence thesis by A79,A78,CANTOR_1:def 3;
  end;
  then R = FinMeetCl P by A16;
  then P9 is prebasis of T by A12,YELLOW_9:23;
  hence thesis by A12,YELLOW_9:26;
end;

theorem Th16:
  for T,S being non empty TopSpace st the carrier of T = the
  carrier of S & the topology of T = the topology of S & T is injective holds S
  is injective
proof
  let T,S be non empty TopSpace;
  assume that
A1: the carrier of T = the carrier of S and
A2: the topology of T = the topology of S and
A3: T is injective;
  let X be non empty TopSpace;
  let f be Function of X,S;
  reconsider f9 = f as Function of X,T by A1;
A4: [#]S <> {};
  assume
A5: f is continuous;
A6: for P being Subset of T st P is open holds (f9)"P is open
  proof
    let P be Subset of T;
    reconsider P9 = P as Subset of S by A1;
    assume P is open;
    then P9 in the topology of S by A2;
    then P9 is open;
    hence thesis by A4,A5,TOPS_2:43;
  end;
  let Y be non empty TopSpace;
  assume
A7: X is SubSpace of Y;
A8: [#]T <> {};
  then f9 is continuous by A6,TOPS_2:43;
  then consider h being Function of Y,T such that
A9: h is continuous and
A10: h|(the carrier of X) = f9 by A3,A7;
  reconsider g = h as Function of Y,S by A1;
  take g;
  for P being Subset of S st P is open holds g"P is open
  proof
    let P be Subset of S;
    reconsider P9 = P as Subset of T by A1;
    assume P is open;
    then P9 in the topology of T by A2;
    then P9 is open;
    hence thesis by A8,A9,TOPS_2:43;
  end;
  hence g is continuous by A4,TOPS_2:43;
  thus thesis by A10;
end;

theorem ::p.122 lemma 3.4.(i) part II
  for I being non empty set for T being Scott TopAugmentation of product
  (I --> BoolePoset{0}) holds T is injective
proof
  let I be non empty set, T be Scott TopAugmentation of product (I -->
  BoolePoset{0});
  set IB = I --> BoolePoset{0}, IS = I --> Sierpinski_Space;
A1: dom Carrier IB = I by PARTFUN1:def 2
    .= dom Carrier IS by PARTFUN1:def 2;
A2: the topology of T = the topology of product (I --> Sierpinski_Space) by
Th15;
  LattPOSet BooleLatt{0} = RelStr(#the carrier of BooleLatt{0}, LattRel(
    BooleLatt{0})#) by LATTICE3:def 2;
  then
A3: the carrier of BoolePoset{0} = the carrier of BooleLatt{0}
                  by YELLOW_1:def 2
    .= bool {{}} by LATTICE3:def 1
    .= {0,1} by CARD_1:49,ZFMISC_1:24;
A4: for i being object st i in dom Carrier IB holds (Carrier IB).i = (Carrier
  IS).i
  proof
    let i be object;
    assume i in dom Carrier IB;
    then
A5: i in I;
    then consider R1 being 1-sorted such that
A6: R1 = IB.i and
A7: (Carrier IB).i = the carrier of R1 by PRALG_1:def 13;
    consider R2 being 1-sorted such that
A8: R2 = IS.i and
A9: (Carrier IS).i = the carrier of R2 by A5,PRALG_1:def 13;
    the carrier of R1 = {0,1} by A3,A5,A6,FUNCOP_1:7
      .= the carrier of Sierpinski_Space by Def9
      .= the carrier of R2 by A5,A8,FUNCOP_1:7;
    hence thesis by A7,A9;
  end;
  for i being Element of I holds (I --> Sierpinski_Space).i is injective;
  then
A10: product (I --> Sierpinski_Space) is injective by Th7;
  the RelStr of T = product (I --> BoolePoset{0}) by YELLOW_9:def 4;
  then the carrier of T = product Carrier (I --> BoolePoset{0}) by
YELLOW_1:def 4
    .= product Carrier (I --> Sierpinski_Space) by A1,A4,FUNCT_1:2
    .= the carrier of product (I --> Sierpinski_Space) by Def3;
  hence thesis by A2,A10,Th16;
end;

theorem Th18: ::p.122 lemma 3.4.(ii)
  for T being T_0-TopSpace ex M being non empty set, f being
  Function of T, product (M --> Sierpinski_Space) st corestr(f) is
  being_homeomorphism
proof
  let T be T_0-TopSpace;
  take M = the carrier of (InclPoset the topology of T);
  set J = M --> Sierpinski_Space;
  reconsider PP = the set of all
product((Carrier J)+*(m,{1})) where m is Element of M
 as prebasis of product J by Th13;
  deffunc F(object) =
  chi({u where u is Subset of T: $1 in u & u is open}, the topology of T);
  consider f being Function such that
A1: dom f = the carrier of T and
A2: for x being object st x in the carrier of T holds f.x = F(x) from
  FUNCT_1:sch 3;
  rng f c= the carrier of product J
  proof
    let y be object;
    assume y in rng f;
    then consider x being object such that
A3: x in dom f & y = f.x by FUNCT_1:def 3;
    set ch = chi({u where u is Subset of T: x in u & u is open}, the topology
    of T);
A4: dom ch = the topology of T by FUNCT_3:def 3
      .= M by YELLOW_1:1
      .= dom (Carrier J) by PARTFUN1:def 2;
A5: for z being object st z in dom (Carrier J) holds ch.z in (Carrier J).z
    proof
      let z be object;
      assume z in dom (Carrier J);
      then
A6:   z in M;
      then z in the topology of T by YELLOW_1:1;
      then z in dom ch by FUNCT_3:def 3;
      then
A7:   ch.z in rng ch by FUNCT_1:def 3;
      ex R being 1-sorted st R = J.z & (Carrier J).z = the carrier of R by A6,
PRALG_1:def 13;
      then (Carrier J).z = the carrier of Sierpinski_Space by A6,FUNCOP_1:7
        .= {0,1} by Def9;
      hence thesis by A7;
    end;
    y = ch by A1,A2,A3;
    then y in product Carrier J by A4,A5,CARD_3:def 5;
    hence thesis by Def3;
  end;
  then reconsider f as Function of T, product J by A1,FUNCT_2:def 1,RELSET_1:4;
  take f;
A8: rng (corestr f) = [#](Image f) by FUNCT_2:def 3;
  for A being Subset of product J st A in PP holds f"A is open
  proof
    {1} c= {0,1} by ZFMISC_1:7;
    then reconsider V = {1} as Subset of Sierpinski_Space by Def9;
    let A be Subset of product J;
    reconsider a = A as Subset of product Carrier J by Def3;
    assume A in PP;
    then consider i being Element of M such that
A9: a = product ((Carrier J) +* (i,{1}));
A10: i in M;
    then
A11: i in the topology of T by YELLOW_1:1;
    then reconsider i9 = i as Subset of T;
A12: i in dom (Carrier J) by A10,PARTFUN1:def 2;
A13: i c= f"A
    proof
      let z be object;
      assume
A14:  z in i;
      set W = {u where u is Subset of T: z in u & u is open};
      i9 is open by A11;
      then
A15:  i in W by A14;
A16:  for w being object st w in dom ((Carrier J) +* (i,V)) holds chi(W,the
      topology of T).w in ((Carrier J) +* (i,V)).w
      proof
        let w be object;
        assume w in dom ((Carrier J) +* (i,V));
        then w in dom (Carrier J) by FUNCT_7:30;
        then
A17:    w in M;
        then w in the topology of T by YELLOW_1:1;
        then
A18:    w in dom chi(W,the topology of T) by FUNCT_3:def 3;
        per cases;
        suppose
          w = i;
          then
          ((Carrier J) +* (i,V)).w = {1} & chi(W,the topology of T).w = 1
          by A11,A12,A15,FUNCT_3:def 3,FUNCT_7:31;
          hence thesis by TARSKI:def 1;
        end;
        suppose
A19:      w <> i;
A20:      chi(W,the topology of T).w in rng chi(W,the topology of T ) by A18,
FUNCT_1:def 3;
          ex r being 1-sorted st r = J.w & (Carrier J).w = the carrier of
          r by A17,PRALG_1:def 13;
          then
A21:      (Carrier J).w = the carrier of Sierpinski_Space by A17,FUNCOP_1:7
            .= {0,1} by Def9;
          ((Carrier J) +* (i,V)).w = (Carrier J).w by A19,FUNCT_7:32;
          hence thesis by A21,A20;
        end;
      end;
A22:  dom chi(W,the topology of T) = the topology of T by FUNCT_3:def 3
        .= M by YELLOW_1:1
        .= dom (Carrier J) by PARTFUN1:def 2
        .= dom ((Carrier J) +* (i,V)) by FUNCT_7:30;
A23:  z in i9 by A14;
      then f.z = chi(W,the topology of T) by A2;
      then f.z in A by A9,A22,A16,CARD_3:def 5;
      hence thesis by A1,A23,FUNCT_1:def 7;
    end;
A24: ((Carrier J)+*(i,V)).i = {1} by A12,FUNCT_7:31;
    f"A c= i
    proof
      let z be object;
      set W = {u where u is Subset of T: z in u & u is open};
      assume z in f"A;
      then f.z in a & f.z = chi(W,the topology of T) by A2,FUNCT_1:def 7;
      then consider g being Function such that
A25:  chi(W,the topology of T) = g and
      dom g = dom ((Carrier J) +* (i,V)) and
A26:  for w being object st w in dom ((Carrier J) +* (i,V)) holds g.w in
      ((Carrier J) +* (i,V)).w by A9,CARD_3:def 5;
      i in dom ((Carrier J) +* (i,V)) by A12,FUNCT_7:30;
      then g.i in ((Carrier J) +* (i,V)).i by A26;
      then chi(W,the topology of T).i = 1 by A24,A25,TARSKI:def 1;
      then i in W by FUNCT_3:36;
      then ex uu being Subset of T st i = uu & z in uu & uu is open;
      hence thesis;
    end;
    then f"A = i by A13;
    hence thesis by A11;
  end;
  then f is continuous by YELLOW_9:36;
  then
A27: dom (corestr f) = [#]T & corestr f is continuous by Th10,FUNCT_2:def 1;
A28: corestr f is one-to-one
  proof
    let x,y be Element of T;
    set U1 = {u where u is Subset of T: x in u & u is open};
    set U2 = {u where u is Subset of T: y in u & u is open};
    assume
A29: (corestr f).x = (corestr f).y;
    thus x = y
    proof
A30:  f.x = chi(U1,the topology of T) & f.y = chi(U2,the topology of T) by A2;
      assume not thesis;
      then consider V being Subset of T such that
A31:  V is open and
A32:  x in V & not y in V or y in V & not x in V by T_0TOPSP:def 7;
A33:  V in the topology of T by A31;
      per cases by A32;
      suppose
A34:    x in V & not y in V;
        reconsider v = V as Subset of T;
A35:    not v in U2
        proof
          assume not thesis;
          then ex u being Subset of T st u = v & y in u & u is open;
          hence thesis by A34;
        end;
        v in U1 by A31,A34;
        then chi(U1,the topology of T).v = 1 by A33,FUNCT_3:def 3;
        hence thesis by A29,A30,A33,A35,FUNCT_3:def 3;
      end;
      suppose
A36:    y in V & not x in V;
        reconsider v = V as Subset of T;
A37:    not v in U1
        proof
          assume not thesis;
          then ex u being Subset of T st u = v & x in u & u is open;
          hence thesis by A36;
        end;
        v in U2 by A31,A36;
        then chi(U2,the topology of T).v = 1 by A33,FUNCT_3:def 3;
        hence thesis by A29,A30,A33,A37,FUNCT_3:def 3;
      end;
    end;
  end;
A38: for V being Subset of T st V is open holds f.:V = product ((Carrier J)
  +* (V,{1})) /\ the carrier of Image f
  proof
    let V be Subset of T;
    assume
A39: V is open;
    hereby
      let y be object;
      assume y in f.:V;
      then consider x being object such that
A40:  x in dom f and
A41:  x in V and
A42:  y = f.x by FUNCT_1:def 6;
      y in rng f by A40,A42,FUNCT_1:def 3;
      then
A43:  y in the carrier of Image f by Th9;
      set Q = {u where u is Subset of T: x in u & u is open};
A44:  V in Q by A39,A41;
A45:  for W being object st W in dom ((Carrier J) +* (V,{1})) holds chi(Q,
      the topology of T).W in ((Carrier J) +* (V,{1})).W
      proof
        let W be object;
        assume W in dom ((Carrier J) +* (V,{1}));
        then
A46:    W in dom (Carrier J) by FUNCT_7:30;
        then
A47:    W in M;
        then
A48:    W in the topology of T by YELLOW_1:1;
        then
A49:    W in dom chi(Q,the topology of T) by FUNCT_3:def 3;
        per cases;
        suppose
          W = V;
          then
          ((Carrier J) +* (V,{1})).W = {1} & chi(Q,the topology of T).W =
          1 by A44,A46,A48,FUNCT_3:def 3,FUNCT_7:31;
          hence thesis by TARSKI:def 1;
        end;
        suppose
A50:      W <> V;
A51:      chi(Q,the topology of T).W in rng chi(Q,the topology of T) by A49,
FUNCT_1:def 3;
          ex r being 1-sorted st r = J.W & (Carrier J).W = the carrier of
          r by A47,PRALG_1:def 13;
          then
A52:      (Carrier J).W = the carrier of Sierpinski_Space by A47,FUNCOP_1:7
            .= {0,1} by Def9;
          ((Carrier J) +* (V,{1})).W = (Carrier J).W by A50,FUNCT_7:32;
          hence thesis by A52,A51;
        end;
      end;
A53:  dom chi(Q,the topology of T) = the topology of T by FUNCT_3:def 3
        .= M by YELLOW_1:1
        .= dom Carrier J by PARTFUN1:def 2
        .= dom ((Carrier J) +* (V,{1})) by FUNCT_7:30;
      y = chi(Q,the topology of T) by A2,A40,A42;
      then y in product ((Carrier J) +* (V,{1})) by A53,A45,CARD_3:def 5;
      hence y in product ((Carrier J) +* (V,{1})) /\ the carrier of Image f by
A43,XBOOLE_0:def 4;
    end;
    let y be object;
    assume
A54: y in product ((Carrier J) +* (V,{1})) /\ the carrier of Image f;
    then y in product ((Carrier J) +* (V,{1})) by XBOOLE_0:def 4;
    then consider g being Function such that
A55: y = g and
    dom g = dom ((Carrier J) +* (V,{1})) and
A56: for W being object st W in dom ((Carrier J) +* (V,{1})) holds g.W
    in ((Carrier J) +* (V,{1})).W by CARD_3:def 5;
    rng f = the carrier of Image f by Th9;
    then y in rng f by A54,XBOOLE_0:def 4;
    then consider x being object such that
A57: x in dom f & y = f.x by FUNCT_1:def 3;
    V in the topology of T by A39;
    then V in M by YELLOW_1:1;
    then
A58: V in dom (Carrier J) by PARTFUN1:def 2;
    then V in dom ((Carrier J) +* (V,{1})) by FUNCT_7:30;
    then g.V in ((Carrier J) +* (V,{1})).V by A56;
    then
A59: g.V in {1} by A58,FUNCT_7:31;
    set Q = {u where u is Subset of T: x in u & u is open};
    y = chi(Q,the topology of T) by A2,A57;
    then chi(Q,the topology of T).V = 1 by A55,A59,TARSKI:def 1;
    then V in Q by FUNCT_3:36;
    then ex u being Subset of T st u = V & x in u & u is open;
    hence thesis by A57,FUNCT_1:def 6;
  end;
A60: for V being Subset of T st V is open holds ((corestr f)")"V is open
  proof
    let V be Subset of T;
A61: PP c= the topology of product J by TOPS_2:64;
    assume
A62: V is open;
    then V in the topology of T;
    then reconsider W = V as Element of M by YELLOW_1:1;
A63: product((Carrier J)+*(W,{1})) in PP;
    then reconsider Q = product((Carrier J)+*(V,{1})) as Subset of product J;
    (corestr f).:V = Q /\ [#](Image f) by A38,A62;
    then (corestr f).: V in the topology of Image f by A63,A61,PRE_TOPC:def 4;
    then (corestr f).:V is open;
    hence thesis by A8,A28,TOPS_2:54;
  end;
  [#]T <> {};
  then (corestr f)" is continuous by A60,TOPS_2:43;
  hence thesis by A8,A28,A27,TOPS_2:def 5;
end;

theorem ::p.122 lemma 3.4.(iii)
  for T being T_0-TopSpace st T is injective ex M being non empty set st
  T is_Retract_of product (M --> Sierpinski_Space)
proof
  let T be T_0-TopSpace;
  assume
A1: T is injective;
  ex M being non empty set, f being Function of T, product (M -->
  Sierpinski_Space) st corestr(f) is being_homeomorphism by Th18;
  hence thesis by A1,Th11;
end;