:: Some Remarks about Product Spaces
::  by Sebastian Koch
::
:: Received September 29, 2018
:: Copyright (c) 2018-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 STRUCT_0, SUBSET_1, PRE_TOPC, FUNCT_1, FUNCT_2, RELAT_1,
      XBOOLE_0, TARSKI, ZFMISC_1, ORDINAL2, TOPS_2, RCOMP_1, T_0TOPSP,
      SETFAM_1, RLVECT_3, CARD_1, EQREL_1, CARD_3, PARTFUN1, FUNCT_7, WAYBEL18,
      FUNCOP_1, TOPS_5, PBOOLE, RLVECT_2, WAYBEL_3, PRALG_1, FUNCT_4, CANTOR_1,
      FINSET_1, ALGSPEC1, SETLIM_2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ENUMSET1, SETFAM_1, PBOOLE,
      RELAT_1, FUNCT_1, FINSET_1, ORDINAL1, RELSET_1, PARTFUN1, TOPS_2,
      FUNCT_2, FUNCT_3, DOMAIN_1, CARD_1, CARD_3, FUNCOP_1, FUNCT_4, FUNCT_7,
      EQREL_1, STRUCT_0, PRALG_1, ALGSPEC1, PRE_TOPC, BORSUK_1, T_0TOPSP,
      CANTOR_1, BORSUK_2, BORSUK_3, WAYBEL_3, WAYBEL18;
 constructors TOPS_2, CANTOR_1, TOPALG_6, MONOID_0, WAYBEL18, FUNCT_4, FUNCT_7,
      ALGSPEC1, BORSUK_3;
 registrations SUBSET_1, FUNCT_1, FUNCT_2, STRUCT_0, PRE_TOPC, TOPS_1,
      BORSUK_1, RELSET_1, CARD_1, ORDINAL1, NAT_1, XBOOLE_0, MONOID_0,
      PRE_POLY, FUNCOP_1, CARD_3, FUNCT_4, FINSET_1, WAYBEL18, RELAT_1, PBOOLE,
      TOPGRP_1;
 requirements SUBSET, BOOLE, NUMERALS;
 definitions TARSKI;
 theorems TARSKI, SUBSET_1, XBOOLE_0, RELAT_1, FUNCT_1, FUNCT_2, EQREL_1,
      ORDERS_5, TOPS_2, T_0TOPSP, TOPREALA, STRUCT_0, PRE_TOPC, YELLOW12,
      BORSUK_1, XBOOLE_1, ENUMSET1, ZFMISC_1, WAYBEL18, WAYBEL_3, FUNCOP_1,
      PARTFUN1, CARD_1, CARD_3, PENCIL_3, CANTOR_1, SETFAM_1, FINSET_1,
      YELLOW_9, FUNCT_7, FUNCT_4, CARD_2, YELLOW_8, RELSET_2, FUNCT_3,
      YELLOW17, PRALG_1, NECKLACE, PBOOLE, ALGSPEC1, PUA2MSS1, XTUPLE_0,
      LATTICE2;
 schemes FUNCT_1, FUNCT_2, SUBSET_1, PBOOLE;

begin  :: Preliminaries

:: into FUNCT_1 ?
:: compare FUNCT_1:4
theorem Th1:
  for f being one-to-one Function, y being object st rng f = {y}
  holds dom f = {f".y}
proof
  let f be one-to-one Function, y be object;
  assume A1: rng f = {y};
  then y in rng f by TARSKI:def 1;
  then consider x0 being object such that
    A2: x0 in dom f & f.x0 = y by FUNCT_1:def 3;
  for x being object holds x in dom f iff x = f".y
  proof
    let x be object;
    hereby
      assume A3: x in dom f;
      then f.x in rng f by FUNCT_1:3;
      then f.x = y by A1, TARSKI:def 1;
      hence x = f".y by A3, FUNCT_1:34;
    end;
    assume x = f".y;
    hence thesis by A2, FUNCT_1:34;
  end;
  hence thesis by TARSKI:def 1;
end;

:: into FUNCT_1 ?
theorem Th2:
  for f being one-to-one Function, y1, y2 being object st rng f = {y1, y2}
  holds dom f = {f".y1, f".y2}
proof
  let f be one-to-one Function, y1, y2 be object;
  assume A1: rng f = {y1,y2};
  then A2: y1 in rng f & y2 in rng f by TARSKI:def 2;
  then consider x1 being object such that
    A3: x1 in dom f & f.x1 = y1 by FUNCT_1:def 3;
  consider x2 being object such that
    A4: x2 in dom f & f.x2 = y2 by A2, FUNCT_1:def 3;
  for x being object holds x in dom f iff x = f".y1 or x = f".y2
  proof
    let x be object;
    thus x in dom f implies x = f".y1 or x = f".y2
    proof
      assume A5: x in dom f;
      then f.x in rng f by FUNCT_1:3;
      then f.x = y1 or f.x = y2  by A1, TARSKI:def 2;
      hence thesis by A5, FUNCT_1:34;
    end;
    thus thesis by A3,A4, FUNCT_1:34;
  end;
  hence thesis by TARSKI:def 2;
end;

:: into PARTFUN1 ?
registration
  let X, Y be set;
  cluster empty X-defined Y-valued one-to-one for Function;
  existence
  proof
    take f = the empty one-to-one Function;
    dom f = {} & rng f = {};
    hence thesis by RELAT_1:def 18, RELAT_1:def 19, XBOOLE_1:2;
  end;
end;

:: into FINSET_1 ?
registration
  let T,S be set;
  let f be Function of T,S;
  let G be finite Subset-Family of T;
  cluster f.:G -> finite;
  coherence
  proof
    defpred P[object,object] means
      ex A being Subset of T st $1 = A & $2 = f.:A;
    A1: for x,y1,y2 be object st x in G & P[x,y1] & P[x,y2] holds y1 = y2;
    A2: for x being object st x in G ex y being object st P[x,y]
    proof
      let x be object;
      assume x in G;
      then reconsider A = x as Subset of T;
      take f.:A, A;
      thus thesis;
    end;
    consider g being Function such that
      A3: dom g = G & for x being object st x in G holds P[x,g.x]
      from FUNCT_1:sch 2(A1,A2);
    for y being object holds y in rng g iff y in f.:G
    proof
      let y be object;
      hereby
        assume y in rng g;
        then consider x being object such that
          A4: x in dom g & g.x = y by FUNCT_1:def 3;
        ex A being Subset of T st
           x = A & y = f.:A by A3, A4;
        hence y in f.:G by A3, A4, FUNCT_2:def 10;
      end;
      assume A6: y in f.:G;
      then reconsider B = y as Subset of S;
      consider A being Subset of T such that
        A7: A in G & B = f.:A by A6, FUNCT_2:def 10;
      ex A0 being Subset of T st
        A = A0 & g.A = f.:A0 by A3, A7;
      hence thesis by A3, A7, FUNCT_1:def 3;
    end;
    then rng g = f.:G by TARSKI:2;
    hence thesis by A3, FINSET_1:8;
  end;
end;

:: into RELSET_2 ?
theorem Th3:
  for A being set, F being Subset-Family of A, R be Relation holds
    R.: meet F c= meet {R.:X where X is Subset of A : X in F}
proof
  let A be set, F be Subset-Family of A, R be Relation;
  per cases;
  suppose meet F = {};
    then R.: meet F = {};
    hence thesis by XBOOLE_1:2;
  end;
  suppose meet F <> {};
    then consider X0 being object such that
      A1: X0 in F by SETFAM_1:1, XBOOLE_0:def 1;
    reconsider X0 as Subset of A by A1;
    A2: R.:X0 in {R.:X where X is Subset of A : X in F} by A1;
      let y be object;
      assume y in R.: meet F;
      then consider x being object such that
        A3: [x,y] in R & x in meet F by RELAT_1:def 13;
      now
        let Y be set;
        assume Y in {R.:X where X is Subset of A : X in F};
        then consider X being Subset of A such that
          A4: Y = R.:X & X in F;
        x in X by A3, A4, SETFAM_1:def 1;
        hence y in Y by A3, A4, RELAT_1:def 13;
      end;
      hence y in meet {R.:X where X is Subset of A : X in F}
        by A2, SETFAM_1:def 1;
  end;
end;

:: into RELSET_2 ?
theorem Th4:
  for A being set, F being Subset-Family of A, f be one-to-one Function holds
    f.: meet F = meet {f.:X where X is Subset of A : X in F}
proof
  let A be set, F be Subset-Family of A, f be one-to-one Function;
  set S = {f.:X where X is Subset of A : X in F};
  A7: meet S c= f.: meet F
  proof
    let y be object;
    assume A1: y in meet S;
    then consider z being object such that
      A2: z in S by XBOOLE_0:def 1, SETFAM_1:1;
    consider X0 being Subset of A such that
      A3: z = f.:X0 & X0 in F by A2;
    A4: y in f.:X0 by A1, A2, A3, SETFAM_1:def 1;
    ex x being object st x in dom f & x in meet F & y = f.x
    proof
      consider x0 being object such that
        A5: x0 in dom f & x0 in X0 & y = f.x0 by A4, FUNCT_1:def 6;
      take x0;
      for X being set st X in F holds x0 in X
      proof
        let X be set;
        assume X in F;
        then f.:X in S;
        then y in f.:X by A1, SETFAM_1:def 1;
        then consider x being object such that
          A6: x in dom f & x in X & y = f.x by FUNCT_1:def 6;
        thus thesis by A5, A6, FUNCT_1:def 4;
      end;
      hence thesis by A3, A5, SETFAM_1:def 1;
    end;
    hence thesis by FUNCT_1:def 6;
  end;
  f.: meet F c= meet S by Th3;
  hence thesis by A7, XBOOLE_0:def 10;
end;

:: into EQREL_1 ?
theorem Th5:
  for X being set, Y being non empty set, f being Function of X, Y
  holds {f"{y} where y is Element of Y : y in rng f} is a_partition of X
proof
  let X be set, Y be non empty set, f be Function of X, Y;
  set P = {f"{y} where y is Element of Y : y in rng f};
  for x being object holds x in X iff ex A being set st x in A & A in P
  proof
    let x be object;
    hereby
      assume A1: x in X;
      then A2: f.x in rng f & f.x in Y by FUNCT_2:4, FUNCT_2:5;
      reconsider A = f"{f.x} as set;
      take A;
      f.x in {f.x} by TARSKI:def 1;
      hence x in A by A1, FUNCT_2:38;
      thus A in P by A2;
    end;
    given A being set such that
      A3: x in A & A in P;
    consider y being Element of Y such that
      A4: f"{y} = A & y in rng f by A3;
    thus x in X by A3, A4;
  end;
  then A5: union P = X by TARSKI:def 4;
  A6: for A being Subset of X st A in P holds A <> {} &
    for B being Subset of X st B in P holds A = B or A misses B
  proof
    let A be Subset of X;
    assume A in P;
    then consider y1 being Element of Y such that
      A7: A = f"{y1} & y1 in rng f;
    consider x being object such that
      A8: x in X & y1 = f.x by A7, FUNCT_2:11;
    f.x in {y1} by A8, TARSKI:def 1;
    hence A <> {} by A7, A8, FUNCT_2:38;
    let B be Subset of X;
    assume B in P;
    then ex y2 being Element of Y st B = f"{y2} & y2 in rng f;
    hence thesis by A7, ZFMISC_1:11, FUNCT_1:71;
  end;
  P c= bool X
  proof
    let x be object;
    assume x in P;
    then ex y being Element of Y st f"{y} = x & y in rng f;
    hence thesis;
  end;
  hence thesis by A5, A6, EQREL_1:def 4;
end;

:: into FUNCOP_1 ?
theorem
  for X being non empty set, x,y being object st X --> x = X --> y holds x = y
proof
  let X be non empty set, x,y be object;
  assume A1: X --> x = X --> y;
  rng(X --> x) = {x} & rng(X --> y) = {y} by FUNCOP_1:8;
  hence thesis by A1, ZFMISC_1:3;
end;

:: into FUNCOP_1 ?
theorem Th7:
  for i being object, J being ManySortedSet of {i} holds J = {i} --> J.i
proof
  let i be object, J be ManySortedSet of {i};
  A1: dom J = {i} by PARTFUN1:def 2
    .= dom ({i} --> J.i);
  for x being object st x in dom J holds J.x = ({i} --> J.i).x
  proof
    let x be object;
    assume x in dom J;
    then A2: x = i by TARSKI:def 1;
    ({i} --> J.i).i = (i .--> J.i).i by FUNCOP_1:def 9 .= J.i by FUNCOP_1:72;
    hence thesis by A2;
  end;
  hence thesis by A1, FUNCT_1:2;
end;

:: into CARD_1 ?
theorem Th8:
  for I being 2-element set, i,j being Element of I st i <> j holds I = {i,j}
proof
  let I be 2-element set;
  let i,j be Element of I;
  assume A1: i <> j;
  for x being object holds x = i or x = j iff x in I
  proof
    let x be object;
    thus x = i or x = j implies x in I;
    assume A2: x in I;
    assume x <> i & x <> j;
    then A3: card {x,i,j} = 3 by A1, CARD_2:58;
    {x,i,j} c= I
    proof
      let z be object;
      assume z in {x,i,j};
      then z = x or z = i or z = j by ENUMSET1:def 1;
      hence thesis by A2;
    end;
    then card {x,i,j} c= card I by CARD_1:11;
    then A4: {0,1,2} c= 2 by A3, CARD_1:def 7, CARD_1:51;
    2 in {0,1,2} by ENUMSET1:def 1;
    then 2 in 2 by A4;
    hence contradiction;
  end;
  hence I = {i,j} by TARSKI:def 2;
end;

:: into FUNCT_4 ?
:: compare FUNCT_4:66
theorem Th9:
  for I being 2-element set, f being ManySortedSet of I
  for i,j being Element of I st i <> j holds f = (i,j) --> (f.i,f.j)
proof
  let I be 2-element set, f be ManySortedSet of I;
  let i,j be Element of I;
  assume A1: i <> j;
  dom f = I by PARTFUN1:def 2
    .= {i,j} by A1, Th8;
  hence thesis by FUNCT_4:66;
end;

:: into FUNCT_4 ?
theorem Th10:
  for a,b,c,d being object st a <> b holds (a,b) --> (c,d) = (b,a) --> (d,c)
proof
  let a,b,c,d be object;
  assume A1: a <> b;
  A2: dom (a,b) --> (c,d) = {a,b} by FUNCT_4:62;
  then A3: dom (a,b) --> (c,d) = dom (b,a) --> (d,c) by FUNCT_4:62;
  for x being object st x in dom (a,b) --> (c,d)
    holds ((a,b) --> (c,d)).x = ((b,a) --> (d,c)).x
  proof
    let x be object;
    assume x in dom (a,b) --> (c,d);
    then per cases by A2, TARSKI:def 2;
    suppose A4: x = a;
      hence ((a,b) --> (c,d)).x = c by A1, FUNCT_4:63
        .= ((b,a) --> (d,c)).x by A4, FUNCT_4:63;
    end;
    suppose A5: x = b;
      hence ((a,b) --> (c,d)).x = d by FUNCT_4:63
        .= ((b,a) --> (d,c)).x by A1, A5, FUNCT_4:63;
    end;
  end;
  hence thesis by A3, FUNCT_1:2;
end;

:: into FUNCT_4 ?
theorem Th11:
  for f being Function, i, j being object st i in dom f & j in dom f
  holds f = f +* (i,j) --> (f.i,f.j)
proof
  let f be Function, i, j be object;
  assume A1: i in dom f & j in dom f;
  thus f = f +* (j .--> f.j) by A1, FUNCT_4:7, LATTICE2:5
    .= (f +* (i .--> f.i)) +* (j .--> f.j) by A1, FUNCT_4:7, LATTICE2:5
    .= f +* ((i .--> f.i) +* (j .--> f.j)) by FUNCT_4:14
    .= f +* (i,j) --> (f.i,f.j) by FUNCT_4:def 4;
end;

:: into FUNCT_4 ?
:: compare FUNCT_7:15, FUNCT_4:114
theorem Th12:
  for x,y,z being object holds (x .--> y) +* (x .--> z) = x .--> z
proof
  let x,y,z be object;
  A1: dom (x .--> y) = dom ({x} --> y) by FUNCOP_1:def 9
    .= {x};
  dom (x .--> z) = dom ({x} --> z) by FUNCOP_1:def 9
    .= {x};
  hence thesis by A1, FUNCT_4:19;
end;

:: into PBOOLE ?
registration
  cluster non non-empty for Function;
  existence
  proof
    take the empty-yielding ManySortedSet of the non empty set;
    thus thesis;
  end;
end;

:: BEGIN into CARD_3 ?

theorem Th13:
  for X, Y being non empty set, y being Element of Y
  holds X --> y in product (X --> Y)
proof
  let X, Y be non empty set, y be Element of Y;
  set f = X --> y;
  A1: dom f = X
    .= dom (X --> Y);
  for x being object st x in dom (X --> Y) holds f.x in (X --> Y).x
  proof
    let x be object;
    assume A2: x in dom (X --> Y);
    then A3: (X --> Y).x = Y by FUNCOP_1:7;
    f.x = y by A2, FUNCOP_1:7;
    hence thesis by A3;
  end;
  hence thesis by A1, CARD_3:def 5;
end;

theorem Th14:
  for X being non empty set, Y being set, Z being Subset of Y
  holds product(X --> Z) c= product (X --> Y)
proof
  let X be non empty set, Y be set, Z be Subset of Y;
    let x be object;
    assume x in product(X --> Z);
    then consider g being Function such that
      A1: x = g & dom g = dom (X --> Z) and
      A2: for y being object st y in dom (X --> Z) holds g.y in (X --> Z).y
      by CARD_3:def 5;
    now
      let y be object;
      assume a4: y in dom (X --> Y);
      then A4: y in X;
      A5: (X --> Z).y = Z & (X --> Y).y = Y by a4,FUNCOP_1:7;
      y in dom (X --> Z) by A4;
      then g.y in (X --> Z).y by A2;
      hence g.y in (X --> Y).y  by A5;
    end;
    hence thesis by A1, CARD_3:def 5;
end;

theorem Th15:
  for X being non empty set, i being object holds
  product ({i} --> X) = {{i} --> x where x is Element of X : not contradiction}
proof
  let X be non empty set, i be object;
  set S = {{i} --> x where x is Element of X : not contradiction};
  for z being object holds z in product ({i} --> X) iff z in S
  proof
    let z be object;
    hereby
      assume z in product ({i} --> X);
      then consider f being Function such that
        A1: z = f & dom f = dom ({i} --> X) and
        A2: for y being object st y in dom ({i} --> X)
          holds f.y in ({i} --> X).y by CARD_3:def 5;
      A3: dom f = {i} by A1;
      for y being object st y in dom f holds f.y = f.i
        by  A1,TARSKI:def 1;
      then A4: f = {i} --> f.i by A3, FUNCOP_1:11;
      i in dom ({i} --> X) by  TARSKI:def 1;
      then f.i in ({i} --> X).i by A2;
      then f.i in (i .--> X). i by FUNCOP_1:def 9;
      then f.i in X by FUNCOP_1:72;
      hence z in S by A1, A4;
    end;
    assume z in S;
    then ex x being Element of X st
       z = {i} --> x;
    hence thesis by Th13;
  end;
  hence thesis by TARSKI:2;
end;

theorem Th16:
  for X being non empty set, i, f being object
  holds f in product({i} --> X) iff ex x being Element of X st f = {i} --> x
proof
  let X be non empty set, i,f be object;
  hereby
    assume f in product({i} --> X);
    then f in {{i} --> x where x is Element of X : not contradiction} by Th15;
    hence ex x being Element of X st f = {i} --> x;
  end;
  assume ex x being Element of X st f = {i} --> x;
  then f in {{i} --> x where x is Element of X : not contradiction};
  hence thesis by Th15;
end;

:: compare YELLOW17:8
theorem
  for X being non empty set, i being object, x being Element of X
  holds proj({i} --> X,i).({i} --> x) = x
proof
  let X be non empty set, i be object, x be Element of X;
  {i} --> x in product ({i} --> X) by Th13;
  then {i} --> x in dom proj({i} --> X,i) by CARD_3:def 16;
  hence proj({i} --> X,i).({i} --> x) = ({i} --> x).i by CARD_3:def 16
    .= (i .--> x).i by FUNCOP_1:def 9
    .= x by FUNCOP_1:72;
end;

:: corrolary from CARD_3:26
Lm1:
  for f being Function holds rng f = {{}} implies product f = {}
proof
  let f be Function;
  assume rng f = {{}};
  then {} in rng f by TARSKI:def 1;
  hence thesis by CARD_3:26;
end;

:: compare CARD_3:26
theorem
  for X, Y being set holds X <> {} & Y = {} iff product (X --> Y) = {}
proof
  let X, Y be set;
  hereby
    assume X <> {} & Y = {};
    then rng(X --> Y) = {{}} by FUNCOP_1:8;
    then {} in rng(X --> Y) by TARSKI:def 1;
    hence product(X --> Y) = {} by CARD_3:26;
  end;
  assume product (X --> Y) = {};
  hence thesis;
end;

registration
  let f be empty Function, x be object;
  cluster proj(f,x) -> trivial;
  coherence
  proof
    dom proj(f,x) = {{}} by CARD_3:10, CARD_3:def 16;
    hence thesis;
  end;
end;

theorem Th19:
  for f being trivial Function, x being object st x in dom f
  holds proj(f,x) is one-to-one
proof
  let f be trivial Function, x be object;
  assume A1: x in dom f;
  then consider t being object such that
    A2: dom f = {t} by ZFMISC_1:131;
  A3: dom f = {x} by A1, A2, TARSKI:def 1;
  set F = proj(f,x);
  for y, z being object st y in dom F & z in dom F & F.y = F.z holds y = z
  proof
    let y,z be object;
    assume A4: y in dom F & z in dom F & F.y = F.z;
    then consider g being Function such that
      A5: y = g & dom g = dom f and
      for s being object st s in dom f holds g.s in f.s
        by CARD_3:def 5;
    consider h being Function such that
      A6: z = h & dom h = dom f and
      for s being object st s in dom f holds h.s in f.s
        by A4, CARD_3:def 5;
    A7: g.x = F.z by A4, A5, CARD_3:def 16
      .= h.x by A4, A6, CARD_3:def 16;
    for s being object st s in dom g holds g.s = h.s
    proof
      let s be object;
      assume s in dom g;
      then s = x by A3, A5, TARSKI:def 1;
      hence thesis by A7;
    end;
    hence thesis by A5, A6, FUNCT_1:2;
  end;
  hence thesis by FUNCT_1:def 4;
end;

registration
  let x,y be object;
  cluster proj(x .--> y,x) -> one-to-one;
  coherence
  proof
    x in {x} by TARSKI:def 1;
    then x in dom({x} --> y);
    then A1: x in dom(x .--> y) by FUNCOP_1:def 9;
    x is set & y is set by TARSKI:1;
    hence thesis by A1, Th19;
  end;
end;

registration
  let I be 1-element set, J be ManySortedSet of I, i be Element of I;
  cluster proj(J,i) -> one-to-one;
  coherence
  proof
    dom J = I by PARTFUN1:def 2;
    then J is trivial & i in dom J;
    hence thesis by Th19;
  end;
end;

theorem
  for X being non empty set, Y being Subset of X, i being object
  holds proj({i} --> X,i).:product ({i} --> Y) = Y
proof
  let X be non empty set, Y be Subset of X, i be object;
  per cases;
  suppose A1: Y is empty;
    then rng ({i} --> Y) = {{}} by FUNCOP_1:8;
    then product ({i} --> Y) = {} by Lm1;
    hence thesis by A1;
  end;
  suppose A2: Y is non empty;
    for x being object holds x in proj({i} --> X,i).:product ({i} --> Y)
      iff x in Y
    proof
      let x be object;
      hereby
        assume x in proj({i} --> X,i).:product ({i} --> Y);
        then consider y being object such that
          A3: y in dom proj({i} --> X,i) & y in product ({i} --> Y) and
          A4: x = proj({i} --> X,i).y by FUNCT_1:def 6;
        consider z being Element of Y such that
          A5: y = {i} --> z by A2, A3, Th16;
        reconsider y as Function by A5;
        x = y.i by A3, A4, CARD_3:def 16
          .= (i .--> z).i by A5, FUNCOP_1:def 9
          .= z by FUNCOP_1:72;
        hence x in Y by A2;
      end;
      assume x in Y;
      then reconsider z = x as Element of Y;
      ex y being object st y in dom proj({i} --> X,i) &
        y in product ({i} --> Y) & x = proj({i} --> X,i).y
      proof
        set y = {i} --> z;
        take y;
        y in product ({i} --> Y) by A2, Th13;
        then y in product ({i} --> X) by Th14, TARSKI:def 3;
        hence A7: y in dom proj({i} --> X,i) &
            y in product ({i} --> Y) by A2,Th13,CARD_3:def 16;
        thus x = (i .--> z).i by FUNCOP_1:72
          .= y.i by FUNCOP_1:def 9
          .= proj({i} --> X,i).y by A7, CARD_3:def 16;
      end;
      hence thesis by FUNCT_1:def 6;
    end;
    hence thesis by TARSKI:2;
  end;
end;

theorem Th21:
  for f, g being non-empty Function, i, x being object
  st x in product f /\ product(f+*g) holds proj(f,i).x = proj(f+*g,i).x
proof
  let f, g be non-empty Function, i, x being object;
  assume A1: x in product f /\ product(f+*g);
  then x in product f by XBOOLE_0:def 4;
  then reconsider h = x as Function;
  x in product f & x in product(f+*g) by A1, XBOOLE_0:def 4;
  then A2: x in dom proj(f,i) & x in dom proj(f+*g,i) by CARD_3:def 16;
  hence proj(f,i).x = h.i by CARD_3:def 16
    .= proj(f+*g,i).x by A2, CARD_3:def 16;
end;

theorem Th22:
  for f, g being non-empty Function, i being object, A being set
  st A c= product f /\ product(f+*g) holds proj(f,i).:A = proj(f+*g,i).:A
proof
  let f, g be non-empty Function, i being object, A being set;
  assume A1: A c= product f /\ product(f+*g);
  for y being object holds y in proj(f,i).:A iff y in proj(f+*g,i).:A
  proof
    let y be object;
    hereby
      assume y in proj(f,i).:A;
      then consider x being object such that
      A2: x in dom proj(f,i) & x in A & y = proj(f,i).x by FUNCT_1:def 6;
      x in product(f+*g) by A1,A2,XBOOLE_0:def 4;
      then A4: x in dom proj(f+*g,i) by CARD_3:def 16;
      y = proj(f+*g,i).x by A2, A1, Th21;
      hence y in proj(f+*g,i).:A by A2, A4, FUNCT_1:def 6;
    end;
    assume y in proj(f+*g,i).:A;
    then consider x being object such that
    A5: x in dom proj(f+*g,i) & x in A & y = proj(f+*g,i).x by FUNCT_1:def 6;
    x in product f by A1,A5,XBOOLE_0:def 4;
    then A7: x in dom proj(f,i) by CARD_3:def 16;
    y = proj(f,i).x by A5, A1, Th21;
    hence y in proj(f,i).:A by A5, A7, FUNCT_1:def 6;
  end;
  hence thesis by TARSKI:2;
end;

theorem Th23:
  for f, g being non-empty Function
  st dom g c= dom f & for i being object st i in dom g holds g.i c= f.i
  holds product(f+*g) c= product f
proof
  let f, g be non-empty Function;
  assume that
    A1: dom g c= dom f and
    A2: for i being object st i in dom g holds g.i c= f.i;
  A3: dom(f+*g) = dom f \/ dom g by FUNCT_4:def 1
    .= dom f by A1, XBOOLE_1:12;
  now
    let x be object;
    assume x in dom (f+*g);
    thus (f+*g).x c= f.x
    proof
      let i be object;
      assume A4: i in (f+*g).x;
      per cases;
      suppose a5: x in dom g;
        then A5: i in g.x by A4, FUNCT_4:13;
        g.x c= f.x by a5,A2;
        hence i in f.x by A5;
      end;
      suppose not x in dom g;
        hence i in f.x by A4, FUNCT_4:11;
      end;
    end;
  end;
  hence product(f+*g) c= product f by A3, CARD_3:27;
end;

theorem Th24:
  for f, g being non-empty Function
  st dom g c= dom f & for i being object st i in dom g holds g.i c= f.i holds
    for i being object st i in dom f \ dom g
    holds proj(f,i).:product(f+*g) = f.i
proof
  let f, g be non-empty Function;
  assume that
    A1: dom g c= dom f and
    A2: for i being object st i in dom g holds g.i c= f.i;
  A3: dom(f+*g) = dom f \/ dom g by FUNCT_4:def 1
    .= dom f by A1, XBOOLE_1:12;
  A4: product(f+*g) = product f /\ product(f+*g) by A1, A2, Th23,XBOOLE_1:28;
  let i be object;
  assume a5: i in dom f \ dom g;
  then A5: i in dom f & not i in dom g by XBOOLE_0:def 5;
  thus proj(f,i).:product(f+*g) = proj(f+*g,i).:product(f+*g) by A4, Th22
    .= proj(f+*g,i).:dom proj(f+*g,i) by CARD_3:def 16
    .= rng proj(f+*g,i) by RELAT_1:113
    .= (f+*g).i by A3, a5, YELLOW17:3
    .= f.i by A5, FUNCT_4:11;
end;

theorem Th25:
  for f, g being non-empty Function
  st dom g c= dom f & for i being object st i in dom g holds g.i c= f.i
  holds for i being object st i in dom g holds proj(f,i).:product(f+*g) = g.i
proof
  let f, g be non-empty Function;
  assume that
    A1: dom g c= dom f and
    A2: for i being object st i in dom g holds g.i c= f.i;
  A3: dom(f+*g) = dom f \/ dom g by FUNCT_4:def 1
    .= dom f by A1, XBOOLE_1:12;
  A4: product(f+*g) = product f /\ product(f+*g) by A1, A2, Th23,XBOOLE_1:28;
  let i be object;
  assume A5: i in dom g;
  thus proj(f,i).:product(f+*g) = proj(f+*g,i).:product(f+*g) by A4, Th22
    .= proj(f+*g,i).:dom proj(f+*g,i) by CARD_3:def 16
    .= rng proj(f+*g,i) by RELAT_1:113
    .= (f+*g).i by A1, A3, A5, YELLOW17:3
    .= g.i by A5, FUNCT_4:13;
end;

theorem Th26:
  for f, g being non-empty Function
  st dom g = dom f & for i being object st i in dom g holds g.i c= f.i
  holds for i being object st i in dom g holds proj(f,i).:product g = g.i
proof
  let f, g be non-empty Function;
  assume that
    A1: dom g = dom f and
    A2: for i being object st i in dom g holds g.i c= f.i;
  let i be object;
  assume A3: i in dom g;
  thus proj(f,i).:product g = proj(f,i).:product(f +* g) by A1, FUNCT_4:19
    .= g.i by A1, A2, A3, Th25;
end;

theorem Th27:
  for f being Function, X, Y being set, i being object st X c= Y
  holds product(f +* (i .--> X)) c= product(f +* (i .--> Y))
proof
  let f be Function, X, Y be set, i be object;
  assume A1: X c= Y;
  dom (f +* (i .--> X)) = dom f \/ dom(i .--> X) by FUNCT_4:def 1
    .= dom f \/ dom({i} --> X) by FUNCOP_1:def 9
    .= dom f \/ {i};
  then A3: dom (f +* (i .--> X)) = dom f \/ dom({i} --> Y)
    .= dom f \/ dom(i .--> Y) by FUNCOP_1:def 9
    .= dom (f +* (i .--> Y)) by FUNCT_4:def 1;
  now
    let x be object;
    assume x in dom (f +* (i .--> X));
    per cases;
    suppose A4: x = i;
      then x in {i} by TARSKI:def 1;
      then x in dom({i} --> X) & x in dom({i} --> Y);
      then A5: x in dom(i .--> X) & x in dom(i .--> Y) by FUNCOP_1:def 9;
      then A6: (f +* (i .--> X)).x = (i .--> X).x by FUNCT_4:13
        .= X by A4, FUNCOP_1:72;
      (f +* (i .--> Y)).x = (i .--> Y).x by A5, FUNCT_4:13
        .= Y by A4, FUNCOP_1:72;
      hence (f +* (i .--> X)).x c= (f +* (i .--> Y)).x by A1, A6;
    end;
    suppose x <> i;
      then not x in dom(i .--> X) & not x in dom(i .--> Y) by TARSKI:def 1;
      then (f +* (i .--> X)).x = f.x & (f +* (i .--> Y)).x = f.x by FUNCT_4:11;
      hence (f +* (i .--> X)).x c= (f +* (i .--> Y)).x;
    end;
  end;
  hence thesis by A3, CARD_3:27;
end;

theorem Th28:
  for i,j being object, A, B, C, D being set st A c= C & B c= D
  holds product((i,j) --> (A,B)) c= product((i,j) --> (C,D))
proof
  let i,j be object, A,B,C,D be set;
  assume A1: A c= C & B c= D;
  per cases;
  suppose A2: i <> j;
      let x be object;
      assume x in product((i,j) --> (A,B));
      then consider g being Function such that
        A3: g = x & dom g = dom (i,j) --> (A,B) and
        A4: for y being object st y in dom (i,j) --> (A,B)
          holds g.y in ((i,j) --> (A,B)).y by CARD_3:def 5;
      A5: dom (i,j) --> (A,B) = {i,j} by FUNCT_4:62
        .= dom (i,j) --> (C,D) by FUNCT_4:62;
      for y being object st y in dom (i,j) --> (C,D) holds
        g.y in ((i,j) --> (C,D)).y
      proof
        let y be object;
        assume A6: y in dom (i,j) --> (C,D);
        then y in {i,j} by FUNCT_4:62;
        then per cases by TARSKI:def 2;
        suppose A7: y = i;
          then g.y in ((i,j) --> (A,B)).i by A4, A5, A6;
          then g.y in A by A2, FUNCT_4:63;
          then g.y in C by A1;
          hence thesis by A2, A7, FUNCT_4:63;
        end;
        suppose A8: y = j;
          then g.y in ((i,j) --> (A,B)).j by A4, A5, A6;
          then g.y in B by FUNCT_4:63;
          then g.y in D by A1;
          hence thesis by A8, FUNCT_4:63;
        end;
      end;
      hence thesis by A3, A5, CARD_3:def 5;
  end;
  suppose A9: i = j;
    then A10: (i,j) --> (A,B) = i .--> B by FUNCT_4:81
      .= {i} --> B by FUNCOP_1:def 9;
    (i,j) --> (C,D) = i .--> D by A9, FUNCT_4:81
      .= {i} --> D by FUNCOP_1:def 9;
    hence thesis by A1, A10, Th14;
  end;
end;

theorem Th29:
  for X, Y being set, f, i, j being object st i <> j
  holds f in product((i,j) --> (X,Y)) iff
    ex x,y being object st x in X & y in Y & f = (i,j) --> (x,y)
proof
  let X,Y be set, f, i, j be object;
  assume A1: i <> j;
  thus f in product((i,j) --> (X,Y)) implies
    ex x,y being object st x in X & y in Y & f = (i,j) --> (x,y)
  proof
    assume f in product((i,j) --> (X,Y));
    then consider g being Function such that
      A2: g = f & dom g = dom (i,j) --> (X,Y) and
      A3: for z being object st z in dom (i,j) --> (X,Y)
        holds g.z in ((i,j) --> (X,Y)).z by CARD_3:def 5;
    take g.i, g.j;
    A4: dom (i,j) --> (X,Y) = {i,j} by FUNCT_4:62;
    then i in dom (i,j) --> (X,Y) by TARSKI:def 2;
    then g.i in ((i,j) --> (X,Y)).i by A3;
    hence g.i in X by A1, FUNCT_4:63;
    j in dom (i,j) --> (X,Y) by A4, TARSKI:def 2;
    then g.j in ((i,j) --> (X,Y)).j by A3;
    hence thesis by A2, A4, FUNCT_4:66,FUNCT_4:63;
  end;
  given x,y being object such that
    A5: x in X & y in Y & f = (i,j) --> (x,y);
  reconsider g = f as Function by A5;
  A6: dom g = {i,j} by A5, FUNCT_4:62
    .= dom (i,j) --> (X,Y) by FUNCT_4:62;
  for z being object st z in dom (i,j) --> (X,Y)
    holds g.z in ((i,j) --> (X,Y)).z
  proof
    let z be object;
    assume z in dom (i,j) --> (X,Y);
    then z in {i,j} by FUNCT_4:62;
    then per cases by TARSKI:def 2;
    suppose A7: z = i;
      then g.z = x by A1, A5, FUNCT_4:63;
      hence thesis by A1, A5, A7, FUNCT_4:63;
    end;
    suppose A8: z = j;
      then g.z = y by A5, FUNCT_4:63;
      hence thesis by A5, A8, FUNCT_4:63;
    end;
  end;
  hence thesis by A6, CARD_3:9;
end;

theorem Th30:
  for f being non-empty Function, X, Y being set, i, j, x, y being object
  for g being Function
  st x in X & y in Y & i <> j & g in product f
  holds g +* (i,j) --> (x,y) in product(f +* (i,j) --> (X,Y))
proof
  let f be non-empty Function, X, Y be set;
  let i,j,x,y be object, g be Function;
  assume that
    A1: x in X & y in Y and
    A2: i <> j & g in product f;
  A3: dom(g +* (i,j) --> (x,y))
     = dom g \/ dom (i,j) --> (x,y) by FUNCT_4:def 1
    .= dom g \/ {i,j} by FUNCT_4:62
    .= dom f \/ {i,j} by A2, CARD_3:9
    .= dom f \/ dom (i,j) --> (X,Y) by FUNCT_4:62
    .= dom(f +* (i,j) --> (X,Y)) by FUNCT_4:def 1;
  for z being object st z in dom(f +* (i,j) --> (X,Y))
    holds (g +* (i,j) --> (x,y)).z in (f +* (i,j) --> (X,Y)).z
  proof
    let z be object;
    assume A4: z in dom(f +* (i,j) --> (X,Y));
    per cases;
    suppose A5: z in {i,j};
      then z in dom (i,j) --> (x,y) by FUNCT_4:62;
      then A6: (g +* (i,j) --> (x,y)).z = ((i,j) --> (x,y)).z by FUNCT_4:13;
      z in dom (i,j) --> (X,Y) by A5, FUNCT_4:62;
      then A7: (f +* (i,j) --> (X,Y)).z = ((i,j) --> (X,Y)).z by FUNCT_4:13;
      per cases by A5, TARSKI:def 2;
      suppose A8: z = i;
        then (g +* (i,j) --> (x,y)).z = x by A2, A6, FUNCT_4:63;
        hence thesis by A1, A2, A7, A8, FUNCT_4:63;
      end;
      suppose A9: z = j;
        then (g +* (i,j) --> (x,y)).z = y by A6, FUNCT_4:63;
        hence thesis by A1, A7, A9, FUNCT_4:63;
      end;
    end;
    suppose A10: not z in {i,j};
      then not z in dom (i,j) --> (x,y) by FUNCT_4:62;
      then A11: (g +* (i,j) --> (x,y)).z = g.z by FUNCT_4:11;
      not z in dom (i,j) --> (X,Y) by A10, FUNCT_4:62;
      then A12: (f +* (i,j) --> (X,Y)).z = f.z by FUNCT_4:11;
      z in dom f \/ dom (i,j) --> (X,Y) by A4, FUNCT_4:def 1;
      then z in dom f \/ {i,j} by FUNCT_4:62;
      then z in dom f by A10, XBOOLE_0:def 3;
      hence thesis by A2, A11, A12, CARD_3:9;
    end;
  end;
  hence thesis by A3, CARD_3:9;
end;

theorem Th31:
  for f being Function, A, B, C, D being set, i, j being object
  st A c= C & B c= D
  holds product(f +* (i,j) --> (A,B)) c= product(f +* (i,j) --> (C,D))
proof
  let f be Function, A,B,C,D be set, i,j be object;
  assume A1: A c= C & B c= D;
  per cases;
  suppose i = j;
    then (i,j) --> (A,B) = i .--> B & (i,j) --> (C,D) = i .--> D by FUNCT_4:81;
    hence thesis by A1, Th27;
  end;
  suppose A2: i <> j;
    dom(f +* (i,j) --> (A,B)) = dom f \/ dom (i,j) --> (A,B) by FUNCT_4:def 1
      .= dom f \/ {i,j} by FUNCT_4:62;
    then A3: dom(f +* (i,j) --> (A,B))
       = dom f \/ dom (i,j) --> (C,D) by FUNCT_4:62
      .=  dom(f +* (i,j) --> (C,D)) by FUNCT_4:def 1;
    for x being object st x in dom(f +* (i,j) --> (A,B))
      holds (f +* (i,j) --> (A,B)).x c= (f +* (i,j) --> (C,D)).x
    proof
      let x be object;
      assume x in dom(f +* (i,j) --> (A,B));
      per cases;
      suppose A4: x in {i,j};
        then x in dom (i,j) --> (A,B) by FUNCT_4:62;
        then A5: (f +* (i,j) --> (A,B)).x = ((i,j) --> (A,B)).x by FUNCT_4:13;
        x in dom (i,j) --> (C,D) by A4, FUNCT_4:62;
        then A6: (f +* (i,j) --> (C,D)).x = ((i,j) --> (C,D)).x by FUNCT_4:13;
        per cases by A4, TARSKI:def 2;
        suppose A7: x = i;
          then (f +* (i,j) --> (A,B)).x = A by A2, A5, FUNCT_4:63;
          hence thesis by A1, A2, A6, A7, FUNCT_4:63;
        end;
        suppose A9: x = j;
          then (f +* (i,j) --> (A,B)).x = B by A5, FUNCT_4:63;
          hence thesis by A1, A6, A9, FUNCT_4:63;
        end;
      end;
      suppose A11: not x in {i,j};
        then not x in dom (i,j) --> (A,B) by FUNCT_4:62;
        then A12: (f +* (i,j) --> (A,B)).x = f.x by FUNCT_4:11;
        not x in dom (i,j) --> (C,D) by A11, FUNCT_4:62;
        hence thesis by A12, FUNCT_4:11;
      end;
    end;
    hence thesis by A3, CARD_3:27;
  end;
end;

theorem
  for f being Function, A, B being set, i, j being object
  st i in dom f & j in dom f & A c= f.i & B c= f.j
  holds product(f +* (i,j) --> (A,B)) c= product f
proof
  let f be Function, A, B be set, i, j be object;
  assume A1: i in dom f & j in dom f & A c= f.i & B c= f.j;
  then product f = product(f +* (i,j) --> (f.i,f.j)) by Th11;
  hence thesis by A1, Th31;
end;

:: $\prod_{i\in I} A_i \cap \prod_{i\in I} B_i = \prod_{i\in I} (A_i \cap B_i)$
:: compare MSUALG_2:1
theorem Th33:
  for I being set, f, g being ManySortedSet of I
  holds product f /\ product g = product(f (/\) g)
proof
  let I be set, f, g be ManySortedSet of I;
  for x being object holds x in product f /\ product g iff
    ex h being Function st h = x & dom h = dom(f (/\) g) &
      for y being object st y in dom(f (/\) g)
      holds h.y in (f (/\) g).y
  proof
    let x be object;
    hereby
      assume x in product f /\ product g;
      then A1: x in product f & x in product g by XBOOLE_0:def 4;
      then consider h being Function such that
        A2: h = x & dom h = dom f and
        A3: for y being object st y in dom f holds h.y in f.y by CARD_3:def 5;
      take h;
      thus h = x by A2;
      thus dom h = I by A2, PARTFUN1:def 2
        .= dom(f (/\) g) by PARTFUN1:def 2;
      let y be object;
      assume a4: y in dom(f (/\) g);
      then A4: y in I;
      A5: y in dom f & y in dom g by A4, PARTFUN1:def 2;
      then A6: h.y in f.y by A3;
      h.y in g.y by A1, A2, A5, CARD_3:9;
      then h.y in f.y /\ g.y by A6, XBOOLE_0:def 4;
      hence h.y in (f (/\) g).y by a4, PBOOLE:def 5;
    end;
    given h being Function such that
      A7: h = x & dom h = dom(f (/\) g) and
      A8: for y being object st y in dom(f (/\) g)
        holds h.y in (f (/\) g).y;
    a9: dom h = I by A7, PARTFUN1:def 2;
    then A9: dom h = dom f & dom h = dom g by PARTFUN1:def 2;
    A10: now
      let y be object;
      assume A11: (y in dom f or y in dom g);
      h.y in (f (/\) g).y by A7, A8, a9, A11;
      then h.y in f.y /\ g.y by A11, PBOOLE:def 5;
      hence h.y in f.y & h.y in g.y by XBOOLE_0:def 4;
    end;
    for y being object st y in dom f holds h.y in f.y by A10;
    then A13: h in product f by A9, CARD_3:9;
    for y being object st y in dom g holds h.y in g.y by A10;
    then h in product g by A9, CARD_3:9;
    hence x in product f /\ product g by A7, A13, XBOOLE_0:def 4;
  end;
  hence thesis by CARD_3:def 5;
end;

:: END into CARD_3 ?
:: BEGIN into FUNCT_7 ?

Lm2:
  for I being 2-element set, f being ManySortedSet of I
  for i, j being Element of I, x being object st i <> j
  holds f +* (i,x) = (i,j) --> (x,f.j)
proof
  let I be 2-element set, f be ManySortedSet of I;
  let i,j be Element of I, x be object;
  assume A1: i <> j;
  then a2:I = {i,j} by Th8;
  then A2: dom f = {i,j} by PARTFUN1:def 2;
  A3: dom(f +* (i,x)) = dom f by FUNCT_7:30
    .= dom (i,j) --> (x,f.j) by A2, FUNCT_4:62;
  for z being object st z in dom(f +* (i,x))
    holds (f +* (i,x)).z = ((i,j) --> (x,f.j)).z
  proof
    let z be object;
    assume z in dom(f +* (i,x));
    then per cases by a2,TARSKI:def 2;
    suppose A5: z = i;
      hence (f +* (i,x)).z = x by A2, a2, FUNCT_7:31
        .= ((i,j) --> (x,f.j)).z by A1, A5, FUNCT_4:63;
    end;
    suppose A6: z = j;
      hence (f +* (i,x)).z = f.j by A1, FUNCT_7:32
        .= ((i,j) --> (x,f.j)).z by A6, FUNCT_4:63;
    end;
  end;
  hence thesis by A3, FUNCT_1:2;
end;

theorem Th34:
  for I being 2-element set, f being ManySortedSet of I
  for i, j being Element of I, x being object st i <> j
  holds f +* (i,x) = (i,j) --> (x,f.j) & f +* (j,x) = (i,j) --> (f.i,x)
proof
  let I be 2-element set, f be ManySortedSet of I;
  let i, j be Element of I, x be object;
  assume A1: i <> j;
  thus f +* (i,x) = (i,j) --> (x,f.j) by A1, Lm2;
  thus f +* (j,x) = (j,i) --> (x,f.i) by A1, Lm2
    .= (i,j) --> (f.i,x) by A1, Th10;
end;

theorem Th35:
  for f being non-empty Function, X being set, i being object st i in dom f
  holds f +* (i,X) is non-empty iff X is non empty
proof
  let f be non-empty Function, X be set, i be object;
  assume A1: i in dom f;
  hereby
    assume A2: f +* (i,X) is non-empty;
    i in dom(f +* (i,X)) by A1, FUNCT_7:30;
    then (f +* (i,X)).i <> {} by A2, FUNCT_1:def 9;
    hence X is non empty by A1, FUNCT_7:31;
  end;
  assume A3: X is non empty;
  for x being object st x in dom(f +* (i,X)) holds (f +* (i,X)).x is non empty
  proof
    let x be object;
    assume A4: x in dom(f +* (i,X));
    A5: x in dom f by A4, FUNCT_7:30;
    x <> i implies (f +* (i,X)).x = f.x by FUNCT_7:32;
    hence thesis by A5, FUNCT_1:def 9, A3, FUNCT_7:31;
  end;
  hence thesis by FUNCT_1:def 9;
end;

theorem Th36:
  for f being non-empty Function, X being set, i being object st i in dom f
  holds product(f +* (i,X)) = {} iff X is empty
proof
  let f be non-empty Function, X be set, i be object;
  assume A1: i in dom f;
  then A2: i in dom(f +* (i,X)) by FUNCT_7:30;
  hereby
    assume product(f +* (i,X)) = {};
    then f +* (i,X) is non non-empty;
    hence X is empty by A1, Th35;
  end;
  assume X is empty;
  then (f +* (i,X)).i = {} by A1, FUNCT_7:31;
  then {} in rng (f +* (i,X)) by A2, FUNCT_1:def 3;
  hence thesis by CARD_3:26;
end;

theorem Th37:
  for f being non-empty Function, X being set, i, x being object
  for g being Function st i in dom f & x in X & g in product f
  holds g +* (i,x) in product(f +* (i,X))
proof
  let f be non-empty Function, X be set, i,x be object;
  let g be Function;
  assume A1: i in dom f & x in X & g in product f;
  A2: dom(g +* (i,x)) = dom g by FUNCT_7:30
    .= dom f by A1, CARD_3:9
    .= dom(f +* (i,X)) by FUNCT_7:30;
  for y being object st y in dom(f+*(i,X)) holds (g+*(i,x)).y in (f+*(i,X)).y
  proof
    let y be object;
    assume A3: y in dom(f+*(i,X));
    then A4:y in dom f by FUNCT_7:30;
    per cases;
    suppose A5: i = y;
      y in dom f by A3, FUNCT_7:30;
      then y in dom g by A1, CARD_3:9;
      then (g+*(i,x)).y = x by A5, FUNCT_7:31;
      hence thesis by A1, A5, FUNCT_7:31;
    end;
    suppose i <> y;
      then (g+*(i,x)).y = g.y & (f+*(i,X)).y = f.y by FUNCT_7:32;
      hence thesis by A4,A1,CARD_3:9;
    end;
  end;
  hence thesis by A2, CARD_3:9;
end;

theorem Th38:
  for f being Function, X, Y being set, i being object st i in dom f & X c= Y
  holds product(f +* (i,X)) c= product(f +* (i,Y))
proof
  let f be Function, X, Y be set, i be object;
  assume A1: i in dom f & X c= Y;
  then f +* (i,X) = f +* (i .--> X) & f +* (i,Y) = f +* (i .--> Y)
    by FUNCT_7:def 3;
  hence thesis by A1, Th27;
end;

:: compare YELLOW17:2
theorem Th39:
  for f being Function, X being set, i being object st i in dom f & X c= f.i
  holds product(f +* (i,X)) c= product(f)
proof
let f be Function, X be set, i be object;
 I: i is set by TARSKI:1;
assume i in dom f & X c= f.i;
  then product(f +* (i,X)) c= product(f +* (i,f.i)) by Th38;
  hence thesis by I, FUNCT_7:35;
end;

theorem
  for f being non-empty Function, X, Y being non empty set, i, j being object
  st i in dom f & j in dom f & (not X c= f.i or not f.j c= Y) &
    product (f +* (i,X)) c= product (f +* (j,Y))
  holds i = j & X c= Y
proof
  let f be non-empty Function, X, Y be non empty set, i, j be object;
  assume that
    A1: i in dom f & j in dom f and
    A2: not X c= f.i or not f.j c= Y and
    A3: product (f +* (i,X)) c= product (f +* (j,Y));
  a4: f +* (i,X) is non-empty & f +* (j,Y) is non-empty by A1, Th35;
  thus A5: i = j
  proof
    assume A6: i <> j;
    A7: i in dom(f +* (i,X)) & j in dom(f +* (i,X)) by A1, FUNCT_7:30;
    (f +* (i,X)).i c= (f +* (j,Y)).i by a4, A7, A3, PUA2MSS1:1;
    then a8: X c= (f +* (j,Y)).i by A1, FUNCT_7:31;
    (f +* (i,X)).j c= (f +* (j,Y)).j by a4, A7, A3, PUA2MSS1:1;
    then (f +* (i,X)).j c= Y by A1, FUNCT_7:31;
    hence contradiction by A2, a8, A6, FUNCT_7:32;
  end;
    let x be object;
    assume A9: x in X;
    set g = the Element of product f;
    A10: g +* (i,x) in product(f +* (i,X)) by A1, A9, Th37;
    i in dom(f +* (j,Y)) by A1, FUNCT_7:30;
    then (g +* (i,x)).i in (f +* (j,Y)).i by A3, A10, CARD_3:9;
    then A11: (g +* (i,x)).i in Y by A1, A5, FUNCT_7:31;
    i in dom g by A1, CARD_3:9;
    hence thesis by A11, FUNCT_7:31;
end;

theorem
  for f being non-empty Function, X being set, i being object
  st i in dom f & product(f +* (i,X)) c= product f holds X c= f.i
proof
  let f be non-empty Function, X be set, i be object;
  assume A1: i in dom f & product(f +* (i,X)) c= product f;
    let x be object;
    assume A2: x in X;
    set g = the Element of product f;
    a3: g +* (i,x) in product(f +* (i,X)) by A1, A2, Th37;
    i in dom g by A1, CARD_3:9;
    then (g +* (i,x)).i = x by FUNCT_7:31;
    hence thesis by A1, a3, CARD_3:9;
end;

theorem Th42:
  for f being non-empty Function, X, Y being non empty set, i, j being object
  st i in dom f & j in dom f & (X <> f.i or Y <> f.j) &
    product (f +* (i,X)) = product (f +* (j,Y))
  holds i = j & X = Y
proof
  let f be non-empty Function, X, Y be non empty set, i, j be object;
  assume that
    A1: i in dom f & j in dom f and
    A2: X <> f.i or Y <> f.j and
    A3: product (f +* (i,X)) = product (f +* (j,Y));
  f +* (i,X) is non-empty & f +* (j,Y) is non-empty by A1, Th35;
  then A4: f +* (i,X) = f +* (j,Y) by A3, PUA2MSS1:2;
  thus A5: i = j
  proof
    assume A6: i <> j;
    A7: X = (f +* (i,X)).i by A1, FUNCT_7:31
      .= f.i by A4, A6, FUNCT_7:32;
    Y = (f +* (j,Y)).j by A1, FUNCT_7:31
      .= f.j by A4, A6, FUNCT_7:32;
    hence contradiction by A2, A7;
  end;
  thus X = (f +* (j,Y)).i by A1, A4, FUNCT_7:31
    .= Y by A1, A5, FUNCT_7:31;
end;

theorem Th43:
  for f being non-empty Function, X being set, i being object
  st i in dom f & X c= f.i holds proj(f,i).:product(f +* (i,X)) = X
proof
  let f be non-empty Function, X be set, i be object;
  assume A1: i in dom f & X c= f.i;
  then A2: f +* (i,X) = f +* (i .--> X) by FUNCT_7:def 3
    .= f +* ({i} --> X) by FUNCOP_1:def 9;
  A3: i in dom (f +* (i,X)) by A1, FUNCT_7:30;
  per cases;
  suppose A4: X is non empty;
    {i} c= dom f by A1, ZFMISC_1:31;
    then A5: dom ({i} --> X) c= dom f;
    A6: for j being object st j in dom ({i} --> X) holds ({i} --> X).j c= f.j
    proof
      let j be object;
      assume A7: j in dom ({i} --> X);
      then i = j by TARSKI:def 1;
      hence thesis by A1, A7, FUNCOP_1:7;
    end;
    A8: i in {i} by TARSKI:def 1;
    then i in dom ({i} --> X);
    then proj(f,i).:product(f +* ({i} --> X)) = ({i} --> X).i
      by A5, A6, A4, Th25;
    hence thesis by A2,A8, FUNCOP_1:7;
  end;
  suppose A9: X is empty;
    then (f +* (i,X)).i is empty by A1, FUNCT_7:31;
    then {} in rng (f +* (i,X)) by A3, FUNCT_1:3;
    then product(f +* (i,X)) = {} by CARD_3:26;
    hence thesis by A9;
  end;
end;

theorem Th44:
  for x,y,z being object holds (x .--> y) +* (x,z) = x .--> z
proof
  let x,y,z be object;
  dom (x .--> y) = dom ({x} --> y) by FUNCOP_1:def 9
    .= {x};
  then x in dom (x .--> y) by TARSKI:def 1;
  then (x .--> y) +* (x,z) = (x .--> y) +* (x .--> z) by FUNCT_7:def 3;
  hence thesis by Th12;
end;

:: END into FUNCT_7 ?

:: into PRALG_1 ?
registration
  let I being non empty set;
  let J being 1-sorted-yielding non-Empty ManySortedSet of I;
  cluster Carrier J -> non-empty;
  coherence
  proof
    assume Carrier J is non non-empty;
    then {} in rng Carrier J by RELAT_1:def 9;
    then consider i being object such that
      A1: i in dom Carrier J & (Carrier J).i = {} by FUNCT_1:def 3;
    reconsider i as set by TARSKI:1;
    consider R being 1-sorted such that
      A2: R = J.i & (Carrier J).i = the carrier of R by A1, PRALG_1:def 13;
    dom J = I by PARTFUN1:def 2;
    then R in rng J by A1, A2, FUNCT_1:3;
    then R is non empty by WAYBEL_3:def 7;
    hence contradiction by A1, A2;
  end;
end;

begin :: Remarks about Product Spaces

theorem Th45:
  for T,S being TopSpace, f being Function of T,S
  holds f is open iff
    ex B being Basis of T st
      for V being Subset of T st V in B holds f.:V is open
proof
  let T,S be TopSpace, f be Function of T,S;
  hereby
    assume A1: f is open;
    reconsider B = the Basis of T as Basis of T;
    take B;
    let V be Subset of T;
    assume V in B;
    hence f.:V is open by A1, TOPS_2:def 1, T_0TOPSP:def 2;
  end;
  given B being Basis of T such that
    A2: for V being Subset of T st V in B holds f.:V is open;
  now
    let A be Subset of T;
    set Y = { G where G is Subset of T : G in B & G c= A };
    Y c= bool the carrier of T
    proof
      let g be object;
      assume g in Y;
      then ex G being Subset of T st g = G & G in B & G c= A;
      hence thesis;
    end;
    then reconsider Y as Subset-Family of T;
    set Z = { f.:G where G is Subset of T : G in Y };
    Z c= bool the carrier of S
    proof
      let h be object;
      assume h in Z;
      then ex G being Subset of T st
        h = f.:G & G in Y;
      hence thesis;
    end;
    then reconsider Z as Subset-Family of S;
    A7: for P being Subset of S holds P in Z implies P is open
    proof
      let P be Subset of S;
      assume P in Z;
      then consider G1 being Subset of T such that
        A5: P = f.:G1 & G1 in Y;
      ex G2 being Subset of T st
        G1 = G2 & G2 in B & G2 c= A by A5;
      hence thesis by A2, A5;
    end;
    assume A is open;
    then A = union Y by YELLOW_8:9;
    then f.:A = union Z by RELSET_2:14; :: f(UY) = Uf(Y)
    hence f.:A is open by A7, TOPS_2:19,TOPS_2:def 1;
  end;
  hence thesis by T_0TOPSP:def 2;
end;

theorem
  for T1,T2,S1,S2 being non empty TopSpace
  for f being Function of T1, S1, g being Function of T2, S2
  st f is open & g is open holds [: f,g :] is open
proof
  let T1,T2,S1,S2 be non empty TopSpace;
  let f be Function of T1, S1, g be Function of T2, S2;
  assume A1: f is open & g is open;
  ex B being Basis of [: T1,T2 :] st
    for P being Subset of [: T1, T2 :] st P in B holds [: f,g :].:P is open
  proof
    set B1 = the Basis of T1;
    set B2 = the Basis of T2;
    set B = {[: V,W :] where V is Subset of T1, W is Subset of T2 :
      V in B1 & W in B2};
    reconsider B as Basis of [: T1, T2 :] by YELLOW_9:40;
    take B;
    let P be Subset of [: T1, T2 :];
    assume P in B;
    then consider V being Subset of T1, W being Subset of T2 such that
      A2: P = [: V,W :] & V in B1 & W in B2;
    A3: f.:V is open & g.:W is open by A1, T_0TOPSP:def 2,A2, TOPS_2:def 1;
    [: f,g :].:P = [: f.:V,g.:W :] by A2, FUNCT_3:72;
    hence thesis by A3, BORSUK_1:6;
  end;
  hence thesis by Th45;
end;

theorem Th47:
  for S,T being non empty TopSpace, f being Function of S,T
  st f is bijective &
    ex K being Basis of S, L being Basis of T st f.:K = L
  holds f is being_homeomorphism
proof
  let S, T be non empty TopSpace, f be Function of S,T;
  assume A1: f is bijective;
  given K being Basis of S, L being Basis of T such that
    A2: f.:K = L;
  for W being Subset of T st W in L holds f"W is open
  proof
    let W be Subset of T;
    assume W in L;
    then consider V being Subset of S such that
      A3: V in K & W = f.:V by A2, FUNCT_2:def 10;
    dom f = the carrier of S by FUNCT_2:def 1;
    then V = f"W by A1, A3, FUNCT_1:94;
    hence thesis by A3, TOPS_2:def 1;
  end;
  then A4: f is continuous by YELLOW_9:34;
  for V being Subset of S st V in K holds f.:V is open
  proof
    let V be Subset of S;
    assume V in K;
    then f.:V in f.:K by FUNCT_2:def 10;
    hence thesis by A2, TOPS_2:def 1;
  end;
  then f is open by Th45;
  then A5: f" is continuous by A1, TOPREALA:14;
  A6: rng f = the carrier of T by A1, FUNCT_2:def 3
    .= [#]T by STRUCT_0:def 3;
  dom f = the carrier of S by FUNCT_2:def 1
    .= [#]S by STRUCT_0:def 3;
  hence thesis by A1, A5, A4, A6, TOPS_2:def 5;
end;

theorem Th48:
  for S,T being non empty TopSpace, f being Function of S,T
  st f is bijective &
    ex K being prebasis of S, L being prebasis of T st f.:K = L
  holds f is being_homeomorphism
proof
  let S, T be non empty TopSpace, f be Function of S,T;
  assume A1: f is bijective;
  given K being prebasis of S, L being prebasis of T such that
    A2: f.:K = L;
  :: the basic idea is to take the canonical bases from the prebases and
  :: show the condition of the theorem above
  reconsider K0 = FinMeetCl K as Basis of S by YELLOW_9:23;
  reconsider L0 = FinMeetCl L as Basis of T by YELLOW_9:23;
  reconsider g = f" as Function of T, S;
  reconsider f0 = f as one-to-one Function by A1;
  a3:   f0" = g by A1, TOPS_2:def 4;
  for W being Subset of T holds W in L0 iff
    ex V being Subset of S st V in K0 & f.:V = W
  proof
    let W be Subset of T;
    thus W in L0 implies ex V being Subset of S st V in K0 & f.:V = W
    proof
      assume W in L0;
      then consider Y being Subset-Family of T such that
        A4: Y c= L & Y is finite & W = Intersect Y by CANTOR_1:def 3;
      per cases;
      suppose A5: Y <> {};
        then A6: W = meet Y by A4, SETFAM_1:def 9;
        reconsider X = g.:Y as Subset-Family of S;
        reconsider V = meet X as Subset of S;
        take V;
        :: we use V := meet f"Y, then f.:V = f.:meet f"Y = meet f.:f"Y = meet Y
        ex Z being Subset-Family of S st Z c= K & Z is finite & V = Intersect Z
        proof
          take X;
          for x being object st x in X holds x in K
          proof
            let x be object;
            assume x in X;
            then consider B being Subset of T such that
              A7: B in Y & x = g.:B by FUNCT_2:def 10;
            consider A being Subset of S such that
              A8: A in K & B = f.:A by A2, A4, A7, FUNCT_2:def 10;
            A9: dom f = the carrier of S by FUNCT_2:def 1;
            x = f"(f.:A) by a3,FUNCT_1:85, A7, A8
              .= A by A1, A9, FUNCT_1:94;
            hence thesis by A8;
          end;
          hence X c= K & X is finite by A4, TARSKI:def 3;
          consider B being object such that
            A10: B in Y by A5, XBOOLE_0:def 1;
          reconsider B as Subset of T by A10;
          g.:B in X by A10, FUNCT_2:def 10;
          hence thesis by SETFAM_1:def 9;
        end;
        hence V in K0 by CANTOR_1:def 3;
        set Z = { f.:A where A is Subset of S : A in X };
        for x being object holds x in Z iff x in Y
        proof
          let x be object;
          A11: rng f = the carrier of T by A1, FUNCT_2:def 3;
          hereby
            assume x in Z;
            then consider A being Subset of S such that
              A12: f.:A = x & A in X;
            consider B being Subset of T such that
              A13: B in Y & A = g.:B by A12, FUNCT_2:def 10;
            x = f.:(f"B) by a3,FUNCT_1:85, A12, A13
              .= B by A11, FUNCT_1:77;
            hence x in Y by A13;
          end;
          assume A14: x in Y;
          then reconsider B = x as Subset of T;
          A15: g.:B in X by A14, FUNCT_2:def 10;
          f.:(g.:B) = f.:(f"B) by a3,FUNCT_1:85
            .= B by A11, FUNCT_1:77;
          hence thesis by A15;
        end;
        then Z = Y by TARSKI:2;
        hence f.:V = W by A1, A6, Th4;
      end;
      suppose Y = {};
        then A16: W = the carrier of T by A4, SETFAM_1:def 9;
        set V = [#]S;
        take V;
        set Z = the empty Subset-Family of S;
        Intersect Z = the carrier of S by SETFAM_1:def 9;
        then Z c= K & Z is finite & V = Intersect Z
          by XBOOLE_1:2,STRUCT_0:def 3;
        hence V in K0 by CANTOR_1:def 3;
        thus f.:V = f.:the carrier of S by STRUCT_0:def 3
          .= f.:dom f by FUNCT_2:def 1
          .= rng f by RELAT_1:113
          .= W by A16, A1, FUNCT_2:def 3;
      end;
    end;
    given V being Subset of S such that
      A17: V in K0 & f.:V = W;
    consider X being Subset-Family of S such that
      A18: X c= K & X is finite & V = Intersect X by A17, CANTOR_1:def 3;
    per cases;
    suppose A19: X <> {};
      then A20: V = meet X by A18, SETFAM_1:def 9;
      ex Y being Subset-Family of T st Y c= L & Y is finite & W = Intersect Y
      proof
        reconsider Y = f.:X as Subset-Family of T;
        take Y;
        thus Y c= L
        proof
          let x be object;
          assume x in Y;
          then ex A being Subset of S st
            A in X & f.:A = x by FUNCT_2:def 10;
          hence thesis by A2, FUNCT_2:def 10, A18;
        end;
        thus Y is finite by A18;
        set Z = { f.:A where A is Subset of S : A in X };
        for x being object holds x in Y iff x in Z
        proof
          let x be object;
          hereby
            assume x in Y;
            then ex A being Subset of S st
              A in X & f.:A = x by FUNCT_2:def 10;
            hence x in Z;
          end;
          assume x in Z;
          then ex A being Subset of S st f.:A = x & A in X;
          hence thesis by FUNCT_2:def 10;
        end;
        then Y = Z by TARSKI:2;
        then A24: meet Y = W by A1, A17, A20, Th4;
        consider A being object such that
          A25: A in X by A19, XBOOLE_0:def 1;
        reconsider A as Subset of S by A25;
        f.:A in f.:X by A25, FUNCT_2:def 10;
        hence thesis by A24, SETFAM_1:def 9;
      end;
      hence thesis by CANTOR_1:def 3;
    end;
    suppose X = {};
      then A26: V = the carrier of S by A18, SETFAM_1:def 9;
      set Y = the empty Subset-Family of T;
      B1: Y c= L & Y is finite by XBOOLE_1:2;
      W = f.:dom f by A17, A26, FUNCT_2:def 1
          .= rng f by RELAT_1:113
          .= the carrier of T by A1, FUNCT_2:def 3
          .= Intersect Y by SETFAM_1:def 9;
      hence W in L0 by B1,CANTOR_1:def 3;
    end;
  end;
  then f.:K0 = L0 by FUNCT_2:def 10;
  hence thesis by A1, Th47;
end;

:: compare TOPGEN_5:71 (the converse)
theorem Th49:
  for S, T being TopSpace
  st ex K being Basis of S, L being Basis of T st K = INTERSECTION(L,{[#]S})
  holds S is SubSpace of T
proof
  let S, T be TopSpace;
  given K being Basis of S, L being Basis of T such that
    A1: K = INTERSECTION(L,{[#]S});
  A2: for A being Subset of S holds A in the topology of S iff
    ex B being Subset of T st B in the topology of T & A = B /\ [#]S
  proof
    let A be Subset of S;
    hereby
      assume A in the topology of S;
      then A in UniCl K by CANTOR_1:def 2, TARSKI:def 3;
      then consider X being Subset-Family of S such that
        A3: X c= K & A = union X by CANTOR_1:def 1;
      set Y = { D where D is Subset of T :
        D in L & ex C being Element of K st C in X & C = D /\ [#]S };
      Y c= bool the carrier of T
      proof
        let x be object;
        assume x in Y;
        then ex D being Subset of T st
          D = x & D in L &
          ex C being Element of K st C in X & C = D /\ [#]S;
        hence thesis;
      end;
      then reconsider Y as Subset-Family of T;
      set B = union Y;
      take B;
      for x being Subset of T holds x in Y implies x is open
      proof
        let x be Subset of T;
        assume x in Y;
        then ex D being Subset of T st
          D = x & D in L &
          ex C being Element of K st C in X & C = D /\ [#]S;
        hence thesis by TOPS_2:def 1;
      end;
      then Y is open by TOPS_2:def 1;
      hence B in the topology of T by TOPS_2:19, PRE_TOPC:def 2;
      for x being object holds x in A iff x in B /\ [#]S
      proof
        let x be object;
        hereby
          assume x in A;
          then consider C being set such that
            A6: x in C & C in X by A3, TARSKI:def 4;
          reconsider C as Element of K by A3, A6;
          consider D, S0 being set such that
            A7: D in L & S0 in {[#]S} & C = D /\ S0
            by A1, A3, A6, SETFAM_1:def 5;
          reconsider D as Subset of T by A7;
          C in X & C = D /\ [#]S by A6, A7, TARSKI:def 1;
          then A8: D in Y by A7;
          x in D by A6, A7, XBOOLE_0:def 4;
          then A9: x in B by A8, TARSKI:def 4;
          x in S0 by A6, A7, XBOOLE_0:def 4;
          then x in [#]S by A7, TARSKI:def 1;
          hence x in B /\ [#]S by A9, XBOOLE_0:def 4;
        end;
        assume A10: x in B /\ [#]S;
        then x in B by XBOOLE_0:def 4;
        then consider D0 being set such that
          A11: x in D0 & D0 in Y by TARSKI:def 4;
        consider D being Subset of T such that
          A12: D = D0 & D in L and
          A13: ex C being Element of K st C in X & C = D /\ [#]S by A11;
        consider C being Element of K such that
          A14: C in X & C = D /\ [#]S by A13;
        x in [#]S by A10, XBOOLE_0:def 4;
        then x in C by A11, A12, A14, XBOOLE_0:def 4;
        hence thesis by A3, A14, TARSKI:def 4;
      end;
      hence A = B /\ [#]S by TARSKI:2;
    end;
    given B being Subset of T such that
      A15: B in the topology of T & A = B /\ [#]S;
    B in UniCl L by A15, CANTOR_1:def 2, TARSKI:def 3;
    then consider Y being Subset-Family of T such that
      A16: Y c= L & B = union Y by CANTOR_1:def 1;
    set X = INTERSECTION(Y,{[#]S});
    X c= bool the carrier of S
    proof
      let x be object;
      reconsider x0 = x as set by TARSKI:1;
      assume x in X;
      then consider C, S0 being set such that
        A17: C in Y & S0 in {[#]S} & x0 = C /\ S0 by SETFAM_1:def 5;
      x0 c= S0 by A17, XBOOLE_1:17;
      then x0 c= [#]S by A17, TARSKI:def 1;
      then x0 c= the carrier of S by STRUCT_0:def 3;
      hence thesis;
    end;
    then reconsider X as Subset-Family of S;
    for x being Subset of S holds x in X implies x is open
    proof
      let x be Subset of S;
      assume x in X;
      then consider C, S0 being set such that
        A18: C in Y & S0 in {[#]S} & x = C /\ S0 by SETFAM_1:def 5;
      x in K by A1, A16, A18, SETFAM_1:def 5;
      hence thesis by TOPS_2:def 1;
    end;
    then A19: X is open by TOPS_2:def 1;
    A = union X by A15, A16, SETFAM_1:25;
    hence thesis by A19, TOPS_2:19, PRE_TOPC:def 2;
  end;
  :: since we are only dealing with unions here, [#]S c= [#]T can be derived
  the carrier of S in the topology of S by PRE_TOPC:def 1;
  then consider B being Subset of T such that
    A20: B in the topology of T & the carrier of S = B /\ [#]S
    by A2;
  [#]S = B /\ [#]S by A20, STRUCT_0:def 3;
  then [#]S c= B by XBOOLE_1:17;
  then [#]S c= the carrier of T by XBOOLE_1:1;
  then [#]S c= [#]T by STRUCT_0:def 3;
  hence thesis by A2, PRE_TOPC:def 4;
end;

theorem Th50:
  for S, T being TopSpace
  st [#]S c= [#]T & ex K being prebasis of S, L being prebasis of T
    st K = INTERSECTION(L,{[#]S})
  holds S is SubSpace of T
proof
  let S, T be TopSpace;
  assume A1: [#]S c= [#]T;
  given K being prebasis of S, L being prebasis of T such that
    A2: K = INTERSECTION(L,{[#]S});
  :: the basic idea is to take the canonical bases from the prebases and
  :: show the condition of the theorem above
  reconsider K0 = FinMeetCl K as Basis of S by YELLOW_9:23;
  reconsider L0 = FinMeetCl L as Basis of T by YELLOW_9:23;
  for x being object holds x in K0 iff x in INTERSECTION(L0,{[#]S})
  proof
    let x be object;
    hereby
      assume A3: x in K0;
      then reconsider A = x as Subset of S;
      consider X being Subset-Family of S such that
        A4: X c= K & X is finite & A = Intersect X by A3, CANTOR_1:def 3;
      per cases;
      suppose A5: X <> {};
        then A6: A = meet X by A4, SETFAM_1:def 9;
        defpred P[object,object] means ex D being Subset of T
          st $1 = D /\ [#]S & $2 = D;
        A7: for x being object st x in X ex y being object st y in L & P[x,y]
        proof
          let x be object;
          assume x in X;
          then consider D, S0 being set such that
            A8: D in L & S0 in {[#]S} & x = D /\ S0 by A2, A4, SETFAM_1:def 5;
          take D;
          thus D in L by A8;
          reconsider D0 = D as Subset of T by A8;
          take D0;
          thus thesis by A8, TARSKI:def 1;
        end;
        consider f being Function such that
          A9: dom f = X & rng f c= L and
          A10: for x being object st x in X holds P[x,f.x]
          from FUNCT_1:sch 6(A7);
        reconsider Y = rng f as Subset-Family of T by A9, XBOOLE_1:1;
        set B = meet Y;
        A11: Y is finite by A4, A9, FINSET_1:8;
A12:    f <> {} by A5, A9;
        then B = Intersect Y by SETFAM_1:def 9;
        then A13: B in L0 by A9, A11, CANTOR_1:def 3;
        for y being object holds y in A iff y in B /\ [#]S
        proof
          let y be object;
          hereby
            assume A14: y in A;
            for D being set st D in Y holds y in D
            proof
              let D be set;
              assume D in Y;
              then consider C being object such that
                A15: C in dom f & f.C = D by FUNCT_1:def 3;
              reconsider C as set by TARSKI:1;
              A16: ex D0 being Subset of T st
                C = D0 /\ [#]S & D = D0 by A9, A10, A15;
              y in C by A6, A9, A14, A15, SETFAM_1:def 1;
              hence thesis by A16, TARSKI:def 3, XBOOLE_1:17;
            end;
            then A17: y in B by A12, SETFAM_1:def 1;
            the carrier of S = [#]S by STRUCT_0:def 3;
            hence y in B /\ [#]S by A14, A17, XBOOLE_0:def 4;
          end;
          assume y in B /\ [#]S;
          then A18: y in B & y in [#]S by XBOOLE_0:def 4;
          for C being set st C in X holds y in C
          proof
            let C be set;
            assume A19: C in X;
            then consider D being Subset of T such that
              A20: C = D /\ [#]S & f.C = D by A10;
            D in Y by A9, A19, A20, FUNCT_1:def 3;
            then y in D by A18, SETFAM_1:def 1;
            hence thesis by A18, A20, XBOOLE_0:def 4;
          end;
          hence thesis by A5, A6, SETFAM_1:def 1;
        end;
        then A21: A = B /\ [#]S by TARSKI:2;
        [#]S in {[#]S} by TARSKI:def 1;
        hence x in INTERSECTION(L0,{[#]S}) by A13, A21, SETFAM_1:def 5;
      end;
      suppose X = {};
        then A22: A = the carrier of S by A4, SETFAM_1:def 9
          .= [#]S by STRUCT_0:def 3;
        ex B, S0 being set st B in L0 & S0 in {[#]S} & A = B /\ S0
        proof
          take [#]T, [#]S;
          set Y = the empty Subset-Family of T;
          A23: Y c= L & Y is finite by XBOOLE_1:2;
          Intersect Y = the carrier of T by SETFAM_1:def 9
            .= [#]T by STRUCT_0:def 3;
          hence thesis by A1, A22, XBOOLE_1:28,TARSKI:def 1,A23,CANTOR_1:def 3;
        end;
        hence x in INTERSECTION(L0,{[#]S}) by SETFAM_1:def 5;
      end;
    end;
    assume x in INTERSECTION(L0,{[#]S});
    then consider B, S0 being set such that
      A24: B in L0 & S0 in {[#]S} & x = B /\ S0 by SETFAM_1:def 5;
    consider Y being Subset-Family of T such that
      A25: Y c= L & Y is finite & B = Intersect Y by A24, CANTOR_1:def 3;
    per cases;
    suppose A26: Y <> {};
      defpred P[object,object] means ex D being Subset of T
        st $2 = D /\ [#]S & $1 = D;
      A27: for x being object st x in Y ex y being object st y in K & P[x,y]
      proof
        let x be object;
        assume A28: x in Y;
        then reconsider D = x as Subset of T;
        take D /\ [#]S;
        [#]S in {[#]S} by TARSKI:def 1;
        hence D /\ [#]S in K by A2, A25, A28, SETFAM_1:def 5;
        take D;
        thus thesis;
      end;
      consider f being Function such that
        A29: dom f = Y & rng f c= K and
        A30: for x being object st x in Y holds P[x,f.x]
        from FUNCT_1:sch 6(A27);
      reconsider X = rng f as Subset-Family of S by A29, XBOOLE_1:1;
      A31: X is finite by A25, A29, FINSET_1:8;
      a32:f <> {} by A26, A29;
      reconsider A = x as set by TARSKI:1;
      for y being object holds y in A iff
        for M being set st M in X holds y in M
      proof
        let y be object;
        hereby
          assume A33: y in A;
          let M be set;
          assume M in X;
          then consider D being object such that
            A34: D in dom f & f.D = M by FUNCT_1:def 3;
          consider D0 being Subset of T such that
            A35: M = D0 /\ [#]S & D = D0 by A29, A30, A34;
          y in B by A24, A33, XBOOLE_0:def 4;
          then y in meet Y by A25, A26, SETFAM_1:def 9;
          then A36: y in D0 by A29, A34, A35, SETFAM_1:def 1;
          y in S0 by A24, A33, XBOOLE_0:def 4;
          then y in [#]S by A24, TARSKI:def 1;
          hence y in M by A36, A35, XBOOLE_0:def 4;
        end;
        assume A37: for M being set st M in X holds y in M;
        for M being set st M in Y holds y in M
        proof
          let M be set;
          assume A38: M in Y;
          then consider D being Subset of T such that
            A39: f.M = D /\ [#]S & M = D by A30;
          M /\ [#]S in X by A29, A38, A39, FUNCT_1:3;
          then y in M /\ [#]S by A37;
          hence thesis by XBOOLE_1:17, TARSKI:def 3;
        end;
        then y in meet Y by A26, SETFAM_1:def 1;
        then A40: y in B by A25, A26, SETFAM_1:def 9;
        set M0 = the Element of Y;
        consider D0 being Subset of T such that
          A41: f.M0 = D0 /\ [#]S & M0 = D0 by A26, A30;
        M0 /\ [#]S in X by A29, A26, A41, FUNCT_1:3;
        then y in M0 /\ [#]S by A37;
        then y in [#]S by XBOOLE_1:17, TARSKI:def 3;
        then y in S0 by A24, TARSKI:def 1;
        hence thesis by A24, A40, XBOOLE_0:def 4;
      end;
      then A = meet X by a32, SETFAM_1:def 1;
      then x = Intersect X by a32, SETFAM_1:def 9;
      hence thesis by A29, A31, CANTOR_1:def 3;
    end;
    suppose Y = {};
      then A42: B = the carrier of T by A25, SETFAM_1:def 9
        .= [#]T by STRUCT_0:def 3;
      set X = the empty Subset-Family of S;
      [#]S = the carrier of S by STRUCT_0:def 3;
      then a43: X c= K & X is finite & [#]S = Intersect X
        by XBOOLE_1:2, SETFAM_1:def 9;
      x = B /\ [#]S by A24, TARSKI:def 1
        .= [#]S by A1, A42, XBOOLE_1:28;
      hence thesis by a43, CANTOR_1:def 3;
    end;
  end;
  hence thesis by TARSKI:2, Th49;
end;

theorem Th51:
  for S, T being TopSpace
  st ex K being prebasis of S, L being prebasis of T
    st [#]S in K & K = INTERSECTION(L,{[#]S})
  holds S is SubSpace of T
proof
  let S, T be TopSpace;
  given K being prebasis of S, L being prebasis of T such that
    A1: [#]S in K & K = INTERSECTION(L,{[#]S});
  consider B, S0 being set such that
    A2: B in L & S0 in {[#]S} & [#]S = B /\ S0 by A1, SETFAM_1:def 5;
  B c= the carrier of T by A2;
  then A3: B c= [#]T by STRUCT_0:def 3;
  [#]S c= B by A2, XBOOLE_1:17;
  hence thesis by A1, A3, Th50, XBOOLE_1:1;
end;

theorem Th52:
  for I being non empty set
  for J being TopStruct-yielding non-Empty ManySortedSet of I
  for i being Element of I holds rng proj(J,i) = the carrier of J.i
proof
  let I be non empty set;
  let J be TopStruct-yielding non-Empty ManySortedSet of I;
  let i be Element of I;
  A1: dom Carrier J = I by PARTFUN1:def 2;
  thus rng proj(J,i) = rng proj(Carrier J,i) by WAYBEL18:def 4
    .= (Carrier J).i by A1, YELLOW17:3
    .= [#](J.i) by PENCIL_3:7
    .= the carrier of J.i by STRUCT_0:def 3;
end;

registration
  let X be set, T be TopStruct;
  cluster X --> T -> TopStruct-yielding;
  coherence;
end;

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

registration
  cluster TopSpace-yielding -> TopStruct-yielding for Relation;
  coherence
  proof
    let F be Relation;
    assume F is TopSpace-yielding;
    then for x being object st x in rng F holds x is TopStruct;
    hence thesis by WAYBEL18:def 1;
  end;
end;

registration
  cluster TopSpace-yielding -> 1-sorted-yielding for Function;
  coherence;
end;

registration
  let X be set, T be TopSpace;
  cluster X --> T -> TopSpace-yielding;
  coherence
  proof
    for x being set st x in rng(X --> T) holds x is TopSpace by TARSKI:def 1;
    hence thesis;
  end;
end;

registration
  let I be set;
  cluster TopSpace-yielding non-Empty for ManySortedSet of I;
  existence
  proof
    take J = I --> the non empty TopSpace;
    thus thesis;
  end;
end;

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

definition
  let f be Function;
  func ProjMap f -> ManySortedFunction of dom f means
  :Def2:
  for x being object st x in dom f holds it.x = proj(f,x);
  existence
  proof
    deffunc F(object) = proj(f,$1);
    consider g being ManySortedSet of dom f such that
      A1: for x being object st x in dom f holds g.x = F(x) from PBOOLE:sch 4;
    now
      let x be object;
      assume x in dom g;
      then g.x = proj(f,x) by A1;
      hence g.x is Function;
    end;
    then reconsider g as ManySortedFunction of dom f by FUNCOP_1:def 6;
    take g;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let g1, g2 be ManySortedFunction of dom f;
    assume that
      A2: for x being object st x in dom f holds g1.x = proj(f,x) and
      A3: for x being object st x in dom f holds g2.x = proj(f,x);
    now
      let x be object;
      assume A4: x in dom f;
      hence g1.x = proj(f,x) by A2 .= g2.x by A3, A4;
    end;
    hence thesis by PBOOLE:3;
  end;
end;

registration
  let f be empty Function;
  cluster ProjMap f -> empty;
  coherence;
end;

registration
  let f be non-empty Function;
  cluster ProjMap f -> non-empty;
  coherence
  proof
    now
      let x be object;
      assume x in dom ProjMap f;
      then (ProjMap f).x = proj(f,x) by Def2;
      hence (ProjMap f).x is non empty;
    end;
    hence thesis by FUNCT_1:def 9;
  end;
end;

registration
  let f be non non-empty Function;
  cluster ProjMap f -> empty-yielding;
  coherence
  proof
    {} in rng f by RELAT_1:def 9;
    then A1: product f = {} by CARD_3:26;
    now
      let x be object;
      assume x in dom ProjMap f;
      then (ProjMap f).x = proj(f,x) by Def2;
      hence (ProjMap f).x is empty by A1;
    end;
    hence thesis by FUNCT_1:def 8;
  end;
end;

definition
  let I be non empty set;
  let J be TopStruct-yielding non-Empty ManySortedSet of I;
  func ProjMap J -> ManySortedSet of I equals
  ProjMap Carrier J;
  coherence
  proof
    dom Carrier J = I by PARTFUN1:def 2;
    hence thesis;
  end;
end;

registration
  let I be non empty set;
  let J be TopStruct-yielding non-Empty ManySortedSet of I;
  cluster ProjMap J -> Function-yielding non empty non-empty;
  coherence;
end;

theorem Th53:
  for I being non empty set
  for J being TopStruct-yielding non-Empty ManySortedSet of I
  for i being Element of I holds (ProjMap J).i = proj(J,i)
proof
  let I be non empty set;
  let J be TopStruct-yielding non-Empty ManySortedSet of I;
  let i be Element of I;
  dom Carrier J = I by PARTFUN1:def 2;
  hence (ProjMap J).i = proj(Carrier J,i) by Def2
    .= proj(J,i) by WAYBEL18:def 4;
end;

:: this functor will be used to express the notion of
:: "all but finitely many factors being the full factor space"
:: when considering the canonical base of the product topology
definition
  let I be non empty set;
  let J be TopStruct-yielding non-Empty ManySortedSet of I;
  let f be one-to-one I-valued Function;
  func product_basis_selector(J,f) -> ManySortedSet of rng f equals
  ((ProjMap J).:.:(I-indexing(f"))) | rng f;
  coherence
  proof
    dom (((ProjMap J).:.:(I-indexing(f"))) |rng f)
       = dom ((ProjMap J).:.:(I-indexing(f"))) /\ rng f by RELAT_1:61
      .= I /\ rng f by PARTFUN1:def 2
      .= rng f by XBOOLE_1:28;
    hence thesis by PARTFUN1:def 2;
  end;
end;

registration
  let I be non empty set;
  let J be TopStruct-yielding non-Empty ManySortedSet of I;
  let f be empty one-to-one I-valued Function;
  cluster product_basis_selector(J,f) -> empty;
  coherence;
end;

theorem Th54:
  for I being non empty set
  for J being TopStruct-yielding non-Empty ManySortedSet of I
  for f being one-to-one I-valued Function
  for i being Element of I st i in rng f
  holds product_basis_selector(J,f).i = proj(J,i).:(f".i)
proof
  let I be non empty set;
  let J be TopStruct-yielding non-Empty ManySortedSet of I;
  let f be one-to-one I-valued Function;
  let i be Element of I;
  assume A1: i in rng f;
  then A2: i in dom(f") by FUNCT_1:33;
  thus product_basis_selector(J,f).i
     = ((ProjMap J).:.:(I-indexing(f"))).i by A1, FUNCT_1:49
    .= ((ProjMap J).i).:((I-indexing(f")).i) by PBOOLE:def 20
    .= proj(J,i).:((I-indexing(f")).i) by Th53
    .= proj(J,i).:(f".i) by A2, ALGSPEC1:9;
end;

theorem Th55:
  for I being non empty set
  for J being TopStruct-yielding non-Empty ManySortedSet of I
  for f being one-to-one I-valued Function
  st f" is non-empty & dom f c= bool product Carrier J
  holds product_basis_selector(J,f) is non-empty
proof
  let I be non empty set;
  let J be TopStruct-yielding non-Empty ManySortedSet of I;
  let f be one-to-one I-valued Function;
  assume A1: f" is non-empty & dom f c= bool product Carrier J;
  assume product_basis_selector(J,f) is non non-empty;
  then consider x being object such that
    A2: x in dom product_basis_selector(J,f) and
    A3: product_basis_selector(J,f).x is empty by FUNCT_1:def 9;
  A4: x in rng f by A2;
  then reconsider i = x as Element of I;
  proj(J,i).:(f".i) is empty by A3, A2, Th54;
  then dom proj(J,i) misses f".i by RELAT_1:118;
  then dom proj(Carrier J,i) misses f".i by WAYBEL18:def 4;
  then A5: product Carrier J misses f".i by CARD_3:def 16;
  A6: rng(f") c= bool product Carrier J by A1, FUNCT_1:33;
  i in dom(f") by A4, FUNCT_1:33;
  then f".i in rng(f") by FUNCT_1:3;
  hence contradiction by A1,A5, A6, XBOOLE_1:67;
end;

theorem Th56:
  for I being non empty set
  for J being TopSpace-yielding non-Empty ManySortedSet of I
  holds {} in product_prebasis J
proof
  let I be non empty set;
  let J be TopSpace-yielding non-Empty ManySortedSet of I;
  set P = the empty 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 & P = product ((Carrier J) +* (i,V))
  proof
    set i = the Element of I;
    set V = the empty Subset of J.i;
    take i, J.i, V;
    dom Carrier J = I by PARTFUN1:def 2;
    hence thesis by Th36;
  end;
  hence thesis by WAYBEL18:def 2;
end;

:: compare YELLOW17:16
theorem Th57:
  for I being non empty set
  for J being TopStruct-yielding non-Empty ManySortedSet of I
  for P being non empty Subset of product Carrier J st P in product_prebasis J
  holds ex i being Element of I st proj(J,i).:P is open &
    for j being Element of I st j <> i holds proj(J,j).:P = [#](J.j)
proof
  let I being non empty set;
  let J being TopStruct-yielding non-Empty ManySortedSet of I;
  let P be non empty Subset of product Carrier J;
  assume P in product_prebasis J;
  then consider i being set, T being TopStruct, V being Subset of T such that
    A1: i in I & V is open & T = J.i and
    A2: P = product( (Carrier J) +* (i,V)) by WAYBEL18:def 2;
  reconsider i as Element of I by A1;
  reconsider V as Subset of J.i by A1;
  take i;
  A3: dom Carrier J = I by PARTFUN1:def 2;
  a4: rng proj(J,i) = the carrier of J.i by Th52;
  proj(J,i).:P = proj(J,i).:(proj(J,i)"V) by A2, WAYBEL18:4;
  hence proj(J,i).:P is open by A1, a4, FUNCT_1:77;
  let j be Element of I;
  assume A5: j <> i;
  for x being object holds x in proj(J,j).:P iff x in [#](J.j)
  proof
    let x be object;
    hereby
      assume x in proj(J,j).:P;
      then consider y being object such that
        A6: y in dom proj(J,j) & y in P & x = proj(J,j).y by FUNCT_1:def 6;
      consider g being Function such that
        A7: y = g & dom g = dom ((Carrier J) +* (i,V)) and
        A8: for z being object st z in dom ((Carrier J) +* (i,V))
          holds g.z in ((Carrier J) +* (i,V)).z by A2, A6, CARD_3:def 5;
      j in dom Carrier J by A3;
      then A9: j in dom ((Carrier J) +* (i,V)) by FUNCT_7:30;
      x = g.j by A6, A7, YELLOW17:8;
      then x in ((Carrier J) +* (i,V)).j by A8, A9;
      then x in (Carrier J).j by A5, FUNCT_7:32;
      hence x in [#](J.j) by PENCIL_3:7;
    end;
    assume x in [#](J.j);
    then x in (Carrier J).j by PENCIL_3:7;
    then A10: x in ((Carrier J) +* (i,V)).j by A5, FUNCT_7:32;
    set g0 = the Element of product( (Carrier J) +* (i,V));
    set g = g0 +* (j,x);
    a11:(Carrier J).i = [#](J.i) by PENCIL_3:7
      .= the carrier of J.i by STRUCT_0:def 3;
    consider g00 being Function such that
      A12: g0 = g00 & dom g00 = dom ((Carrier J) +* (i,V)) and
      A13: for z being object st z in dom ((Carrier J) +* (i,V))
        holds g00.z in ((Carrier J) +* (i,V)).z by A2, CARD_3:def 5;
    ex f being Function st g = f & dom f = dom ((Carrier J) +* (i,V)) &
      for z being object st z in dom ((Carrier J) +* (i,V))
        holds f.z in ((Carrier J) +* (i,V)).z
    proof
      take g;
      thus g=g & dom g = dom ((Carrier J) +* (i,V)) by A12, FUNCT_7:30;
      let z be object;
      assume A15: z in dom ((Carrier J) +* (i,V));
      z <> j implies g.z = g0.z by FUNCT_7:32;
      hence thesis by A10, A12,A13, A15, FUNCT_7:31;
    end;
    then A16: g in product( (Carrier J) +* (i,V)) by CARD_3:def 5;
    a17: product( (Carrier J) +* (i,V)) c= product Carrier J by A3, a11, Th39;
    then g in product Carrier J by A16;
    then g in dom proj(Carrier J,j) by CARD_3:def 16;
    then A18: g in dom proj(J,j) by WAYBEL18:def 4;
    A19: j in dom Carrier J by A3;
    A20: g is Element of product J by a17,A16, WAYBEL18:def 3;
    j in dom g0 by A12, A19, FUNCT_7:30;
    then x = g.j by FUNCT_7:31
      .= proj(J,j).g by A20, YELLOW17:8;
    hence thesis by A2, A16, A18, FUNCT_1:def 6;
  end;
  hence proj(J,j).:P = [#](J.j) by TARSKI:2;
end;

theorem Th58:
  for I being non empty set
  for J being TopSpace-yielding non-Empty ManySortedSet of I
  for P being non empty Subset of product Carrier J st P in product_prebasis J
  holds (for j being Element of I holds proj(J,j).:P is open) &
    ex i being Element of I
    st for j being Element of I st j <> i holds proj(J,j).:P = [#](J.j)
proof
  let I being non empty set;
  let J being TopSpace-yielding non-Empty ManySortedSet of I;
  let P be non empty Subset of product Carrier J;
  assume P in product_prebasis J;
  then consider i being Element of I such that
    A1: proj(J,i).:P is open and
    A2: for j being Element of I st j <> i holds proj(J,j).:P = [#](J.j)
    by Th57;
  hereby
    let j be Element of I;
    j<>i implies proj(J,j).:P = [#](J.j) by A2;
    hence proj(J,j).:P is open by A1;
  end;
  take i;
  thus thesis by A2;
end;

theorem Th59:
  for I being non empty set
  for J being TopStruct-yielding non-Empty ManySortedSet of I
  for f being one-to-one I-valued Function
  for X being Subset-Family of product Carrier J
  st X c= product_prebasis J & dom f = X & f" is non-empty &
    for A being Subset of product Carrier J st A in X
    holds proj(J,f/.A).:A is open
  holds for i being Element of I holds
    (not i in rng f implies
      proj(J,i).:product(Carrier J +* product_basis_selector(J,f)) = [#](J.i))
    & (i in rng f implies
      proj(J,i).:product(Carrier J +* product_basis_selector(J,f)) is open)
proof
  let I be non empty set;
  let J be TopStruct-yielding non-Empty ManySortedSet of I;
  let f be one-to-one I-valued Function;
  let X be Subset-Family of product Carrier J;
  set g = product_basis_selector(J,f);
  set P = product(Carrier J +* g);
  assume that
    A1: X c= product_prebasis J & dom f = X & f" is non-empty and
    A2: for A being Subset of product Carrier J st A in X
      holds proj(J,f/.A).:A is open;
  let i be Element of I;
  A3: dom Carrier J = I & dom g = rng f by PARTFUN1:def 2;
  A4: g is non-empty by A1, Th55;
  A6: now
    let j be object;
    assume a7: j in dom g;
    then  j in rng f;
    then reconsider k = j as Element of I;
    g.j = proj(J,k).:(f".k) by a7, Th54;
    then g.j c= the carrier of J.k;
    then g.j c= [#](J.k) by STRUCT_0:def 3;
    hence g.j c= (Carrier J).j by PENCIL_3:7;
  end;
  thus not i in rng f implies proj(J,i).:P = [#](J.i)
  proof
    assume not i in rng f;
    then A8: i in dom Carrier J \ dom g by A3, XBOOLE_0:def 5;
    thus proj(J,i).:P = proj(Carrier J,i).:P by WAYBEL18:def 4
      .= (Carrier J).i by A3, A4, A6, A8, Th24
      .= [#](J.i) by PENCIL_3:7;
  end;
  assume A9: i in rng f;
  A11: proj(J,i).:P = proj(Carrier J,i).:P by WAYBEL18:def 4
    .= g.i by A4, A3, A6, A9, Th25
    .= proj(J,i).:(f".i) by A9, Th54;
  A12: f.(f".i) = i by A9, FUNCT_1:35;
  i in dom(f") by A9, FUNCT_1:33;
  then a13: f".i in rng(f") by FUNCT_1:3;
  then A13: f".i in dom f by FUNCT_1:33;
  f".i in X by A1,a13,FUNCT_1:33;
  then reconsider A = f".i as Subset of product Carrier J;
  f/.A = i by A12, A13, PARTFUN1:def 6;
  hence thesis by A2, A11, A13,A1;
end;

theorem Th60:
  for I being non empty set
  for J being TopSpace-yielding non-Empty ManySortedSet of I
  for f being one-to-one I-valued Function
  for X being Subset-Family of product Carrier J
  st X c= product_prebasis J & dom f = X & f" is non-empty &
    for A being Subset of product Carrier J st A in X
    holds proj(J,f/.A).:A is open
  holds for i being Element of I holds
    proj(J,i).:product(Carrier J +* product_basis_selector(J,f)) is open &
    (not i in rng f implies
      proj(J,i).:product(Carrier J +* product_basis_selector(J,f)) = [#](J.i))
proof
  let I be non empty set;
  let J be TopSpace-yielding non-Empty ManySortedSet of I;
  let f be one-to-one I-valued Function;
  let X be Subset-Family of product Carrier J;
  set g = product_basis_selector(J,f);
  set P = product(Carrier J +* g);
  assume that
    A1: X c= product_prebasis J & dom f = X & f" is non-empty and
    A2: for A being Subset of product Carrier J st A in X
      holds proj(J,f/.A).:A is open;
  let i be Element of I;
  not i in rng f implies
      proj(J,i).:P = [#](J.i) by A1, A2, Th59;
  hence thesis by A1, A2, Th59;
end;

Lm3:
  for I being non empty set
  for J being TopSpace-yielding non-Empty ManySortedSet of I
  for P being Subset of product Carrier J
  holds P in FinMeetCl product_prebasis J implies
    ex X being Subset-Family of product Carrier J,
      f being one-to-one I-valued Function
    st X c= product_prebasis J & X is finite & P = Intersect X &
      dom f = X & P = product(Carrier J +* product_basis_selector(J,f))
proof
  let I be non empty set;
  let J be TopSpace-yielding non-Empty ManySortedSet of I;
  let P be Subset of product Carrier J;
  assume A1: P in FinMeetCl product_prebasis J;
  consider Y being Subset-Family of product Carrier J such that
    A2: Y c= product_prebasis J & Y is finite & P = Intersect Y
    by A1, CANTOR_1:def 3;
  :: the usual textbook Proof uses induction to prove this theorem.
  :: Here, we take a more direct approach.
  per cases;
  :: the special cases of P = {} and P = product J are handled at the end
  suppose A3: Y is non empty & meet Y <> {};
    then A4: P = meet Y by A2, SETFAM_1:def 9;
    :: P is an intersection of a set Y of prebasis elements (possibly infinite)
    :: g maps these prebasis elements to their corresponding coordinate
    defpred P[object,object] means
      ex i being Element of I, B being Subset of J.i
      st $2 = i & B is open & $1 = product(Carrier J +* (i,B));
    A5: for x being object st x in Y ex i being object st i in I & P[x,i]
    proof
      let x be object;
      assume x in Y;
      then consider i being set, T being TopStruct, V being Subset of T
        such that
        A6: i in I & V is open & T = J.i & x = product ((Carrier J) +* (i,V))
        by A2, WAYBEL18:def 2;
      take i;
      thus i in I by A6;
      reconsider j=i as Element of I by A6;
      reconsider V as Subset of J.j by A6;
      take j,V;
      thus thesis by A6;
    end;
    consider g being Function of Y, I such that
      A7: for x being object st x in Y holds P[x,g.x] from FUNCT_2:sch 1(A5);
    :: the set of all g"{i} partitions Y; taking the meet of each one
    :: we get a set X of prebasis elements of which two always have a
    :: different relevant coordinate (hence ensuring that f will be one-to-one)
    set X = {meet (g"{i}) where i is Element of I : g"{i} <> {}};
    X c= bool product Carrier J
    proof
      let x be object;
      assume x in X;
      then consider i being Element of I such that
        A8: x = meet(g"{i}) & g"{i} <> {};
      reconsider Z = g"{i} as Subset-Family of product Carrier J by XBOOLE_1:1;
      meet Z is Subset of product Carrier J;
      hence thesis by A8;
    end;
    then reconsider X as Subset-Family of product Carrier J;
    take X;
    :: f is designed to work like g: it maps the elements of X
    :: to their corresponding coordinate.
    defpred Q[object,object] means ex i being Element of I
      st $2 = i & $1 = meet (g"{i}) & g"{i} <> {};
    A9: for x being object st x in X ex i being object st i in I & Q[x,i]
    proof
      let x be object;
      assume x in X;
      then consider i being Element of I such that
        A10: x = meet(g"{i}) & g"{i} <> {};
      take i;
      thus i in I;
      take i;
      thus thesis by A10;
    end;
    consider f being Function of X, I such that
      A11: for x being object st x in X holds Q[x,f.x] from FUNCT_2:sch 1(A9);
    A12: dom f = X & rng f c= I by FUNCT_2:def 1;
    :: confirm the one-to-one property
    for x1,x2 being object st x1 in dom f & x2 in dom f & f.x1 = f.x2
      holds x1 = x2
    proof
      let x1, x2 being object;
      assume A13: x1 in dom f & x2 in dom f & f.x1 = f.x2;
      then consider i1 being Element of I such that
        A14: f.x1 = i1 & x1 = meet(g"{i1}) & g"{i1} <> {} by A11;
      ex i2 being Element of I st
        f.x2 = i2 & x2 = meet(g"{i2}) & g"{i2} <> {} by A11, A13;
      hence thesis by A13, A14;
    end;
    then reconsider f as one-to-one I-valued Function by FUNCT_1:def 4;
    take f;
    :: needed for technical reasons
    A16: for i being Element of I, S being non empty set
      st g"{i} <> {} & S in g"{i}
      ex V being non empty open Subset of J.i
        st S = product (Carrier J +* (i,V))
    proof
      let i be Element of I;
      let S be non empty set;
      assume a17: g"{i} <> {} & S in g"{i};
      then A17: S in Y & g.S in {i} by FUNCT_2:38;
      then consider j being set, T being TopStruct, V being Subset of T
        such that A18: j in I & V is open & T = J.j and
        A19: S = product (Carrier J +* (j,V)) by A2, WAYBEL18:def 2;
      a20:dom Carrier J = I by PARTFUN1:def 2;
      per cases;
      suppose A21: V <> (Carrier J).j;
        A22: V is non empty by A19, a20, Th36,A18;
        A23: i = j
        proof
          g.S = i by A17, TARSKI:def 1;
          then consider k being Element of I, B being Subset of J.k such that
            A24: i = k & B is open and
            A25: S = product(Carrier J +* (k,B)) by A7, a17;
          B is non empty by a20, A25, Th36;
          hence thesis by A19, A18,a20, A21, A22, A24, A25, Th42;
        end;
        then reconsider V as non empty open Subset of J.i
          by A19, a20, Th36, A18;
        take V;
        thus thesis by A19, A23;
      end;
      suppose V = (Carrier J).j;
        then A26: S = product Carrier J by A19, FUNCT_7:35
          .= product(Carrier J +* (i,(Carrier J).i)) by FUNCT_7:35;
        take [#](J.i);
        thus thesis by A26, PENCIL_3:7;
      end;
    end;
    A27: X is non empty
    proof
      A28: ex i being Element of I st g"{i} <> {}
      proof
        set A = the Element of Y;
        consider i being Element of I, B being Subset of J.i such that
          A29: g.A = i & B is open & A = product(Carrier J +* (i,B)) by A3, A7;
        take i;
        g.A in {i} by A29, TARSKI:def 1;
        hence g"{i} <> {} by A3, FUNCT_2:38;
      end;
      ex x being object st x in X
      proof
        consider i being Element of I such that
          A30: g"{i} <> {} by A28;
        meet(g"{i}) in X by A30;
        hence thesis;
      end;
      hence thesis;
    end;
    :: this Lemma is basically asserting that
    :: $\bigcap_{i\in g"\{k\}} \pi^{-1}_{k} (U_{i})
    ::   = \pi^{-1}_{k} (\bigcap_{i\in g"\{k\}} U_{i})$ holds for each $k$
    A31: for x being Element of X
      st x = meet (g"{f.x}) & g"{f.x} <> {} & x <> {}
      ex Z being Subset-Family of J.(In(f.x, I))
      st Z = {proj(J,In(f.x, I)).:V
          where V is Subset of product Carrier J : V in g"{f.x}} &
        Z is open & Z is finite & Z is non empty &
        x = product (Carrier J +* (f.x, meet Z))
    proof
      let x be Element of X;
      set i = In(f.x, I);
      a32: f.x in rng f by A12, A27, FUNCT_1:3;
      then A32: i = f.x by SUBSET_1:def 8;
      assume A33: x = meet (g"{f.x}) & g"{f.x} <> {} & x <> {};
      set Z = {proj(J,In(f.x, I)).:V
        where V is Subset of product Carrier J : V in g"{f.x}};
      Z c= bool the carrier of J.i
      proof
        let y be object;
        assume y in Z;
        then ex V being Subset of product Carrier J st
           y = proj(J,i).:V & V in g"{f.x};
        hence thesis;
      end;
      then reconsider Z as Subset-Family of J.i;
      take Z;
      thus Z = {proj(J,In(f.x, I)).:V
        where V is Subset of product Carrier J : V in g"{f.x}};
      for A being Subset of J.i holds A in Z implies A is open
      proof
        let A be Subset of J.i;
        assume A in Z;
        then consider V being Subset of product Carrier J such that
          A35: A = proj(J,i).:V & V in g"{f.x};
        V in Y & (V is empty or V is non empty) by A35;
        hence thesis by A2, A35, Th58;
      end;
      hence Z is open by TOPS_2:def 1;
      defpred R[object,object] means ex V being Subset of product Carrier J
        st $1 = V & $2 = proj(J,i).:V;
      A37: for y,z1,z2 being object st y in g"{i} & R[y,z1] & R[y,z2]
        holds z1 = z2;
      A38: for y being object st y in g"{i} ex z being object st R[y,z]
      proof
        let y be object;
        assume y in g"{i};
        then y in Y;
        then reconsider V = y as Subset of product Carrier J;
        take proj(J,i).:V,V;
        thus thesis;
      end;
      consider h being Function such that
        A39: dom h = g"{i} & for y being object st y in g"{i}
          holds R[y,h.y] from FUNCT_1:sch 2(A37,A38);
      a45: for y being object holds y in rng h iff y in Z
      proof
        let y be object;
        hereby
          assume y in rng h;
          then consider z being object such that
            A40: z in dom h & y = h.z by FUNCT_1:def 3;
          ex V being Subset of product Carrier J st
             z = V & h.z = proj(J,i).:V by A39, A40;
          hence y in Z by A32, A39, A40;
        end;
        assume y in Z;
        then consider V being Subset of product Carrier J such that
          A42: y = proj(J,i).:V & V in g"{f.x};
        A43: V in dom h by a32,SUBSET_1:def 8, A39, A42;
        ex V0 being Subset of product Carrier J st
           V = V0 & h.V = proj(J,i).:V0 by A32, A39, A42;
        hence thesis by A42, A43,  FUNCT_1:def 3;
      end;
      then rng h = Z by TARSKI:2;
      hence Z is finite by A2, A39, FINSET_1:8;
      h.the Element of g"{f.x} in rng h by A32, A33, A39, FUNCT_1:3;
      hence A46: Z is non empty by a45;
      a47: dom Carrier J = I by PARTFUN1:def 2;
      then A47: i in dom Carrier J;
      for y being object holds y in meet(g"{i}) iff
        y in product (Carrier J +* (i,meet Z))
      proof
        let y be object;
        hereby
          assume A49: y in meet(g"{i});
          set S0 = the Element of g"{i};
          S0 is non empty by A32, A33, A49, SETFAM_1:def 1;
          then consider V0 being non empty open Subset of J.i such that
            A50: S0 = product (Carrier J +* (i,V0)) by A16, A32, A33;
          y in product (Carrier J +* (i,V0))
            by A32, A33, A49, A50, SETFAM_1: def 1;
          then consider f0 being Function such that
            A51: y = f0 & dom f0 = dom (Carrier J +* (i,V0)) and
            A52: for z being object st z in dom (Carrier J +* (i,V0))
              holds f0.z in (Carrier J +* (i,V0)).z by CARD_3:def 5;
          now
            take f0;
            thus y = f0 by A51;
            thus dom f0 = dom Carrier J by A51, FUNCT_7:30
              .= dom (Carrier J +* (i,meet Z)) by FUNCT_7:30;
            let z be object;
            assume z in dom (Carrier J +* (i,meet Z));
            then A53: z in dom Carrier J by FUNCT_7:30;
            per cases;
            suppose A54: z <> i;
              then A55: (Carrier J +* (i,meet Z)).z
                 =(Carrier J).z by FUNCT_7:32
                .= (Carrier J +* (i,V0)).z by A54, FUNCT_7:32;
              z in dom (Carrier J +* (i,V0)) by A53, FUNCT_7:30;
              hence f0.z in (Carrier J +* (i,meet Z)).z by A52, A55;
            end;
            suppose A56: z = i;
              then A57: (Carrier J +* (i,meet Z)).z
                = meet Z by A53, FUNCT_7:31;
              for S being set st S in Z holds f0.z in S
              proof
                let S be set;
                assume S in Z;
                then consider S1 being Subset of product Carrier J
                  such that A58: S = proj(J,i).:S1 & S1 in g"{f.x};
                S1 is non empty by A32, A49, A58, SETFAM_1:def 1;
                then consider V1 being non empty open Subset of J.i
                  such that A59: S1 = product (Carrier J +* (i,V1))
                  by A16, A32, A58;
                V1 c= the carrier of J.i;
                then V1 c= [#](J.i) by STRUCT_0:def 3;
                then A60: V1 c= (Carrier J).i by PENCIL_3:7;
                proj(J,i) = proj(Carrier J,i) by WAYBEL18:def 4;
                then A61: S = V1 by A58, A59, A60, a47, Th43;
                y in S1 by A32, A49, A58, SETFAM_1:def 1;
                then consider f1 being Function such that
                  A62: y = f1 & dom f1 = dom (Carrier J +* (i,V1)) and
                  A63: for a being object st a in dom (Carrier J +* (i,V1))
                    holds f1.a in (Carrier J +* (i,V1)).a by A59, CARD_3:def 5;
                i in dom (Carrier J +* (i,V1)) by A47, FUNCT_7:30;
                then f1.i in (Carrier J +* (i,V1)).i by A63;
                hence f0.z in S by A51, A56, A61, A62, a47, FUNCT_7:31;
              end;
              hence f0.z in (Carrier J +* (i,meet Z)).z
                by A57,A46,SETFAM_1:def 1;
            end;
          end;
          hence y in product (Carrier J +* (i,meet Z)) by CARD_3:def 5;
        end;
        assume A64: y in product (Carrier J +* (i,meet Z));
        for S being set st S in g"{i} holds y in S
        proof
          let S be set;
          assume A65: S in g"{i};
          S is non empty by A32, A33, A65, SETFAM_1:4;
          then consider V being non empty open Subset of J.i such that
            A66: S = product (Carrier J +* (i,V)) by A16, A65;
          V c= the carrier of J.i;
          then V c= [#](J.i) by STRUCT_0:def 3;
          then A67: V c= (Carrier J).i by PENCIL_3:7;
          proj(J,i) = proj(Carrier J,i) by WAYBEL18:def 4;
          then A68: proj(J,i).:S = V by a47, A66, A67, Th43;
          S in Y by A65;
          then V in Z by A32, A65, A68;
          then product (Carrier J +* (i,meet Z))
            c= product (Carrier J +* (i,V)) by a47, Th38,SETFAM_1:3;
          hence y in S by A64, A66;
        end;
        hence y in meet(g"{i}) by A32, A33, SETFAM_1:def 1;
      end;
      hence x = product (Carrier J +* (f.x, meet Z)) by A32, A33, TARSKI:2;
    end;
    :: this is proven easily with the Lemma
    for x being object holds x in X implies x in product_prebasis J
    proof
      let x be object;
      assume A69: x in X;
      per cases;
      suppose A70: x <> {};
        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))
        proof
          consider i being Element of I such that
            A71: f.x = i & x = meet(g"{i}) & g"{i} <> {} by A11, A69;
          consider Z being Subset-Family of J.(In(f.x, I)) such that
            Z = {proj(J,In(f.x, I)).:V
              where V is Subset of product Carrier J : V in g"{f.x}} and
            A72: Z is open & Z is finite & Z is non empty and
            A73: x = product (Carrier J +* (f.x, meet Z))
            by A31, A69, A70, A71;
          set W = meet Z;
          take i, J.(In(f.x, I)), W;
          thus thesis by A71, A73,A72, TOPS_2:20;
        end;
        hence thesis by A69, WAYBEL18:def 2;
      end;
      suppose x = {};
        hence thesis by Th56;
      end;
    end;
    hence X c= product_prebasis J by TARSKI:def 3;
    :: we show that changing the order of intersections (as we grouped some
    :: with meet g"{i}) doesn't change the set
    for x being object holds x in meet X iff x in meet Y
    proof
      let x be object;
      hereby
        assume A74: x in meet X;
        for Sy being set st Sy in Y holds x in Sy
        proof
          let Sy be set;
          assume A75: Sy in Y;
          then consider i being Element of I, B being Subset of J.i such that
            A76: g.Sy = i & B is open & Sy = product(Carrier J +* (i,B)) by A7;
          g.Sy in {i} by A76, TARSKI:def 1;
          then A77: Sy in g"{i} by A75, FUNCT_2:38;
          then meet(g"{i}) in X;
          then A78: x in meet(g"{i}) by A74, SETFAM_1:def 1;
          meet(g"{i}) c= Sy by A77, SETFAM_1:3;
          hence x in Sy by A78;
        end;
        hence x in meet Y by A3, SETFAM_1:def 1;
      end;
      assume A79: x in meet Y;
      for Sx being set st Sx in X holds x in Sx
      proof
        let Sx be set;
        assume Sx in X;
        then consider i being Element of I such that
          A80: Sx = meet(g"{i}) & g"{i} <> {};
        for A being set st A in g"{i} holds x in A by A79, SETFAM_1:def 1;
        hence x in Sx by A80, SETFAM_1:def 1;
      end;
      hence x in meet X by A27, SETFAM_1:def 1;
    end;
    then A81: meet X = meet Y by TARSKI:2;
    :: we map g"{i} to meet g"{i}; since the g"{i} partition Y and
    :: Y is finite, X must be finite, too
    thus X is finite
    proof
      set S = {g"{i} where i is Element of I : i in rng g};
      a82: S is a_partition of Y by Th5;
      defpred R[object,object] means ex M being set st $1 = M & $2 = meet M;
      A83: for A being object st A in S ex B being object st B in X & R[A,B]
      proof
        let A be object;
        assume A in S;
        then consider i being Element of I such that
          A84: A = g"{i} & i in rng g;
        take meet(g"{i});
        consider x being object such that
          A85: x in Y & g.x = i by A84, FUNCT_2:11;
        i in {i} by TARSKI:def 1;
        then x in g"{i} by A85, FUNCT_2:38;
        hence meet(g"{i}) in X;
        take g"{i};
        thus thesis by A84;
      end;
      consider h being Function of S,X such that
        A86: for A being object st A in S holds R[A,h.A]
        from FUNCT_2:sch 1(A83);
      for B being object st B in X ex A being object st A in S & B = h.A
      proof
        let B be object;
        assume B in X;
        then consider i being Element of I such that
        A87: B = meet(g"{i}) & g"{i} <> {};
        take g"{i};
        consider x being object such that
          A88: x in g"{i} by A87, XBOOLE_0:def 1;
        x in Y & g.x in {i} by A88, FUNCT_2:38;
        then A90: g.x = i by TARSKI:def 1;
        dom g = Y by FUNCT_2:def 1;
        then i in rng g by A88, A90, FUNCT_1:def 3;
        hence g"{i} in S;
        then ex M being set st
           g"{i} = M & h.(g"{i}) = meet M by A86;
        hence thesis by A87;
      end;
      then rng h = X by FUNCT_2:10;
      hence X is finite by a82,A2;
    end;
    thus P = Intersect X by A4, A27, A81, SETFAM_1:def 9;
    thus dom f = X by FUNCT_2:def 1;
    :: we show that if x has the form
    :: $\pi_1^{-1}(U_1)\cap\ldots\cap\pi_n^{-1}(U_n)$ if and only if it has
    :: the form $\prod_{i\in I} U_i$ with all but finitely many of the
    :: factors being the whole factor space
    set F = Carrier J +* product_basis_selector(J,f);
    for x being object holds x in meet X iff x in product F
    proof
      let x be object;
      A92: I = I \/ rng f by XBOOLE_1:12
        .= dom Carrier J \/ rng f by PARTFUN1:def 2
        .= dom Carrier J \/ dom product_basis_selector(J,f) by PARTFUN1:def 2
        .= dom F by FUNCT_4:def 1;
      hereby
        assume A93: x in meet X;
        consider A0 being object such that
          A94: A0 in X by A27, XBOOLE_0:def 1;
        reconsider A0 as set by TARSKI:1;
        consider i0 being Element of I such that
          A95: f.A0 = i0 & A0 = meet(g"{i0}) & g"{i0} <> {} by A11, A94;
        A0 <> {} by A3, A81, A94, SETFAM_1:4;
        then consider Z0 being Subset-Family of J.(In(f.A0, I)) such that
          Z0 = {proj(J,In(f.A0, I)).:V
            where V is Subset of product Carrier J : V in g"{f.A0}} and
          Z0 is open & Z0 is finite & Z0 is non empty and
          A96: A0 = product (Carrier J +* (f.A0, meet Z0)) by A31, A94, A95;
        x in A0 by A93, A94, SETFAM_1:def 1;
        then consider h being Function such that
          A97: x = h & dom h = dom(Carrier J +* (f.A0, meet Z0)) and
          A98: for y being object st y in dom(Carrier J +* (f.A0, meet Z0))
            holds h.y in (Carrier J +* (f.A0, meet Z0)).y
          by A96, CARD_3:def 5;
        A99: dom h = I by A97, PARTFUN1:def 2;
        A100: dom h = dom F by A92, A97, PARTFUN1:def 2;
        for y being object st y in dom F holds h.y in F.y
        proof
          let y be object;
          assume y in dom F;
          then reconsider i = y as Element of I by A92;
          i in dom h by A99;
          then A101: i in dom Carrier J by A97, FUNCT_7:30;
          per cases;
          suppose A102: y in rng f;
            then y in dom product_basis_selector(J,f) by PARTFUN1:def 2;
            then F.y = product_basis_selector(J,f).i by FUNCT_4:13;
            then A103: F.y = proj(J,i).:(f".i) by A102, Th54;
            consider A being object such that
              A104: A in X & f.A = i by A102, FUNCT_2:11;
            reconsider A as set by TARSKI:1;
            consider j being Element of I such that
              A105: f.A = j & A = meet (g"{j}) & g"{j} <> {} by A11, A104;
            A <> {} by A3, A81, A104, SETFAM_1:4;
            then consider Z being Subset-Family of J.(In(f.A, I)) such that
              Z = {proj(J,In(f.A, I)).:V
                where V is Subset of product Carrier J : V in g"{f.A}} and
              Z is open & Z is finite & Z is non empty and
              A106: A = product(Carrier J +* (f.A, meet Z)) by A31, A104, A105;
            reconsider Z as Subset-Family of J.i by A104;
            a107: h in A by A93, A97, A104, SETFAM_1:def 1;
            dom(Carrier J +* (f.A, meet Z)) = I by PARTFUN1:def 2;
            then h.i in (Carrier J +* (f.A, meet Z)).i by a107,A106, CARD_3:9;
            then A108: h.i in meet Z by A104, A101, FUNCT_7:31;
            ex z being object st z in dom proj(J,i) &
              z in meet(g"{i}) & proj(J,i).z = h.i
            proof
              set z0 = the Element of product Carrier J;
              set z = z0 +* (i,h.i);
              take z;
              meet Z c= the carrier of J.i;
              then meet Z c= [#](J.i) by STRUCT_0:def 3;
              then A109: meet Z c= (Carrier J).i by PENCIL_3:7;
              A110: z in product(Carrier J +* (i, meet Z)) by A101, A108, Th37;
              product(Carrier J +* (i, meet Z)) c= product Carrier J
                by A101, A109, Th39;
              then z in product Carrier J by A110;
              then A111: z in dom proj(Carrier J,i) by CARD_3:def 16;
              hence z in dom proj(J,i) & z in meet(g"{i})
                by A104, A105, A106, A101, A108, Th37,WAYBEL18:def 4;
              A112: i in dom z0 by A101, CARD_3:9;
              thus proj(J,i).z = proj(Carrier J,i).z by WAYBEL18:def 4
                .= z.i by A111, CARD_3:def 16
                .= h.i by A112, FUNCT_7:31;
            end;
            then h.i in proj(J,i).:meet(g"{i}) by FUNCT_1:def 6;
            hence h.y in F.y by A103, A105, A12, A104, FUNCT_1:34;
          end;
          suppose not y in rng f;
            then not y in dom product_basis_selector(J,f);
            then A114: F.y = (Carrier J).y by FUNCT_4:11;
            reconsider Z0 as Subset-Family of J.i0 by A95;
            meet Z0 c= the carrier of J.i0;
            then meet Z0 c= [#](J.i0) by STRUCT_0:def 3;
            then A115: meet Z0 c= (Carrier J).i0 by PENCIL_3:7;
            i0 in I;
            then i0 in dom Carrier J by PARTFUN1:def 2;
            then A116: product(Carrier J +* (i0, meet Z0)) c= product Carrier J
              by A115, Th39;
            h in product(Carrier J +* (i0, meet Z0))
              by A95, A97, A98, CARD_3:9;
            hence h.y in F.y by A114,A101,A116, CARD_3:9;
          end;
        end;
        hence x in product F by A97, A100, CARD_3:def 5;
      end;
      assume x in product F;
      then consider h being Function such that
        A117: h = x & dom h = dom F and
        A118: for y being object st y in dom F holds h.y in F.y
        by CARD_3:def 5;
      for A being set st A in X holds h in A
      proof
        let A be set;
        assume A119: A in X;
        then consider i being Element of I such that
          A120: f.A = i & A = meet(g"{i}) & g"{i} <> {} by A11;
        A121: f".i = A by A12, A119, A120, FUNCT_1:34;
        A <> {} by A3, A81, A119, SETFAM_1:4;
        then consider Z being Subset-Family of J.(In(f.A, I)) such that
          A122: Z = {proj(J,In(f.A, I)).:V
              where V is Subset of product Carrier J : V in g"{f.A}} and
          Z is open & Z is finite & Z is non empty and
          A124: A = product (Carrier J +* (f.A, meet Z)) by A31, A119, A120;
        A125: dom h = dom(Carrier J +* (f.A, meet Z))
          by A92, A117, PARTFUN1:def 2;
        for y being object st y in dom(Carrier J +* (f.A, meet Z))
          holds h.y in (Carrier J +* (f.A, meet Z)).y
        proof
          let y be object;
          assume A126: y in dom(Carrier J +* (f.A, meet Z));
          per cases;
          suppose y <> i;
            then A127: (Carrier J +* (f.A, meet Z)).y = (Carrier J).y
              by A120, FUNCT_7:32;
            A128: y in dom Carrier J by A126, FUNCT_7:30;
            A129: h.y in F.y by A92, A118,A126;
            per cases;
            suppose A130: y in rng f;
              then reconsider i0 = y as Element of I;
              y in dom product_basis_selector(J,f) by A130, PARTFUN1:def 2;
              then F.y = product_basis_selector(J,f).i0 by FUNCT_4:13
                .= proj(J,i0).:(f".i0) by A130, Th54;
              then F.y c= rng proj(J,i0) by RELAT_1:111;
              then F.y c= rng proj(Carrier J,i0) by WAYBEL18:def 4;
              then F.y c= (Carrier J).i0 by A128, YELLOW17:3;
              hence thesis by A127, A129;
            end;
            suppose not y in rng f;
              then not y in dom product_basis_selector(J,f);
              hence thesis by A127, A129, FUNCT_4:11;
            end;
          end;
          suppose A131: y = i;
            i in I;
            then a132: i in dom Carrier J by PARTFUN1:def 2;
            A133: i in rng f by A12, A119, A120, FUNCT_1:def 3;
            then i in dom product_basis_selector(J,f) by PARTFUN1:def 2;
            then A134: F.i = product_basis_selector(J,f).i by FUNCT_4:13
              .= proj(J,i).:meet(g"{i}) by A120, A121, A133, Th54;
            reconsider G = g"{i} as Subset-Family of product Carrier J
              by XBOOLE_1:1;
            h.i in proj(J,i).:meet(g"{i}) by A92, A118, A134;
            then h.i in meet {proj(J,i).:B
              where B is Subset of product Carrier J : B in G}
              by Th3, TARSKI:def 3;
            hence thesis by A131, a132, FUNCT_7:31, A120, A122;
          end;
        end;
        hence h in A by A124, A125, CARD_3:9;
      end;
      hence thesis by A27, A117, SETFAM_1:def 1;
    end;
    hence thesis by A4, A81, TARSKI:2;
  end;
  :: trivial cases
  suppose A136: Y is empty;
    reconsider f = the empty Function as one-to-one I-valued Function
      by XBOOLE_1:2, RELAT_1:38, RELAT_1:def 19;
    take Y, f;
    thus Y c= product_prebasis J & Y is finite & P = Intersect Y by A2;
    thus dom f = Y by A136;
    product_basis_selector(J,f) is empty;
    hence thesis by A2, A136, SETFAM_1:def 9;
  end;
  suppose Y is non empty & meet Y = {};
    then A138: P = {} by A2, SETFAM_1:def 9;
    set i = the Element of I;
    set V = the empty Subset of J.i;
    a139: dom Carrier J = I by PARTFUN1:def 2;
    then A140: product (Carrier J +* (i,V)) = {} by Th36;
    then product (Carrier J +* (i,V)) in product_prebasis J by Th56;
    then reconsider A = product (Carrier J +* (i,V)) as
      Subset of product Carrier J;
    set X = {A};
    set f = A .--> i;
    take X, f;
    thus X c= product_prebasis J & X is finite by A140,Th56, ZFMISC_1:31;
    {} in X by A140, TARSKI:def 1;
    then meet X = {} by SETFAM_1:4;
    hence P = Intersect X by A138, SETFAM_1:def 9;
    thus dom f = dom ({A} --> i) by FUNCOP_1:def 9
      .= X;
    set F = Carrier J +* product_basis_selector(J,f);
    ex j being object st j in dom F & F.j = {}
    proof
      take i;
      i in dom Carrier J \/ dom product_basis_selector(J,f)
        by a139,XBOOLE_1:7, TARSKI:def 3;
      hence i in dom F by FUNCT_4:def 1;
      i in {i} by TARSKI:def 1;
      then i in rng({A} --> i) by FUNCOP_1:8;
      then A142: i in rng f by FUNCOP_1:def 9;
      then i in dom product_basis_selector(J,f) by PARTFUN1:def 2;
      hence F.i = product_basis_selector(J,f).i by FUNCT_4:13
        .= proj(J,i).:(f".i) by A142, Th54
        .= proj(J,i).:((i .--> A).i) by NECKLACE:9
        .= proj(J,i).:A by FUNCOP_1:72
        .= {} by A140;
    end;
    then {} in rng F by FUNCT_1:def 3;
    hence thesis by A138,CARD_3:26;
  end;
end;

:: Theorem of canonical product base characterization
theorem
  for I being non empty set
  for J being TopSpace-yielding non-Empty ManySortedSet of I
  for P being Subset of product Carrier J
  holds P in FinMeetCl product_prebasis J iff
    ex X being Subset-Family of product Carrier J,
      f being one-to-one I-valued Function
    st X c= product_prebasis J & X is finite & P = Intersect X & dom f = X &
      P = product(Carrier J +* product_basis_selector(J,f))
  by Lm3, CANTOR_1:def 3;

theorem Th62:
  for I being non empty set
  for J being TopSpace-yielding non-Empty ManySortedSet of I
  for P being non empty Subset of product Carrier J
  holds P in FinMeetCl product_prebasis J implies
    ex X being Subset-Family of product Carrier J,
      f being one-to-one I-valued Function
    st X c= product_prebasis J & X is finite & P = Intersect X & dom f = X &
      for i being Element of I holds proj(J,i).:P is open &
        (not i in rng f implies proj(J,i).:P = [#](J.i))
proof
  let I be non empty set;
  let J be TopSpace-yielding non-Empty ManySortedSet of I;
  let P be non empty Subset of product Carrier J;
  assume A1: P in FinMeetCl product_prebasis J;
  consider X being Subset-Family of product Carrier J,
    f being one-to-one I-valued Function such that
    A2: X c= product_prebasis J & X is finite & P = Intersect X & dom f = X and
    A3: P = product(Carrier J +* product_basis_selector(J,f)) by A1, Lm3;
  take X, f;
  thus X c= product_prebasis J & X is finite & P = Intersect X & dom f = X
    by A2;
  A4: now
    let A be Subset of product Carrier J;
    assume A5: A in X;
    A is empty implies proj(J,f/.A).:A = {}(J.(f/.A));
    hence proj(J,f/.A).:A is open by A2, A5, Th58;
  end;
  f" is non-empty
  proof
    assume f" is non non-empty;
    then {} in rng(f") by RELAT_1:def 9;
    then {} in X by A2, FUNCT_1:33;
    then X is non empty & meet X = {} by SETFAM_1:4;
    hence contradiction by A2, SETFAM_1:def 9;
  end;
  hence thesis by A2, A3, A4, Th60;
end;

theorem Th63:
  for I being non empty set
  for J being TopSpace-yielding non-Empty ManySortedSet of I
  for P being non empty Subset of product Carrier J
  holds P in FinMeetCl product_prebasis J implies
    ex I0 being finite Subset of I st for i being Element of I holds
      proj(J,i).:P is open & (not i in I0 implies proj(J,i).:P = [#](J.i))
proof
  let I be non empty set;
  let J be TopSpace-yielding non-Empty ManySortedSet of I;
  let P be non empty Subset of product Carrier J;
  assume P in FinMeetCl product_prebasis J;
  then consider X being Subset-Family of product Carrier J,
    f being one-to-one I-valued Function such that
    A1: X c= product_prebasis J & X is finite & P = Intersect X & dom f = X and
    A2: for i being Element of I holds proj(J,i).:P is open &
      (not i in rng f implies proj(J,i).:P = [#](J.i)) by Th62;
  reconsider I0 = rng f as finite Subset of I by A1, FINSET_1:8;
  take I0;
  thus thesis by A2;
end;

:: characterization of the canonical prebasis of
:: the product topology over one factor
theorem Th64:
  for I being 1-element set
  for J being TopStruct-yielding non-Empty ManySortedSet of I
  for i being Element of I, P being Subset of product Carrier J
  holds P in product_prebasis J iff ex V being Subset of J.i
    st V is open & P = product ({i} --> V)
proof
  let I be 1-element set;
  let J be TopStruct-yielding non-Empty ManySortedSet of I;
  let i be Element of I;
  card I = 1 by CARD_1:def 7;
  then A1: I = {i} by ORDERS_5:2;
  the carrier of J.i = [#](J.i) by STRUCT_0:def 3
    .= (Carrier J).i by PENCIL_3:7;
  then A2: Carrier J = {i} --> the carrier of J.i by A1, Th7;
  let P be Subset of product Carrier J;
  hereby
    assume P in product_prebasis J;
    then consider j being set, T being TopStruct, V being Subset of T such that
      A3: j in I & V is open & T = J.j and
      A4: P = product ((Carrier J) +* (j,V)) by WAYBEL18:def 2;
    A5: i = j by A1, A3, TARSKI:def 1;
    reconsider W=V as Subset of J.i by A1, A3, TARSKI:def 1;
    take W;
    thus W is open by A3, A5;
    thus P = product ( (i .--> the carrier of J.i) +* (i,W))
        by A2, A4, A5, FUNCOP_1:def 9
      .= product (i .--> W) by Th44
      .= product ({i} --> W) by FUNCOP_1:def 9;
  end;
  given V being Subset of J.i such that
    A6: V is open & P = product ({i} --> V);
    P = product (i .--> V) by A6, FUNCOP_1:def 9
      .= product ( (i .--> the carrier of J.i) +* (i,V)) by Th44
      .= product ((Carrier J) +* (i,V)) by A2, FUNCOP_1:def 9;
  hence thesis by A6,WAYBEL18:def 2;
end;

:: before I used the Theorem of canonical product base characterization
:: the Proof of this theorem was 4 times as long.
Lm4:
  for I being 1-element set
  for J being TopSpace-yielding non-Empty ManySortedSet of I
  for i being Element of I, P being Subset of product Carrier J
  holds P in FinMeetCl product_prebasis J implies ex V being Subset of J.i
    st V is open & P = product ({i} --> V)
proof
  let I be 1-element set;
  let J be TopSpace-yielding non-Empty ManySortedSet of I;
  let i be Element of I;
  card I = 1 by CARD_1:def 7;
  then A1: I = {i} by ORDERS_5:2;
  the carrier of J.i = [#](J.i) by STRUCT_0:def 3
    .= (Carrier J).i by PENCIL_3:7;
  then A2: Carrier J = {i} --> the carrier of J.i by A1, Th7;
  let P be Subset of product Carrier J;
  assume P in FinMeetCl product_prebasis J;
  then consider X being Subset-Family of product Carrier J,
    f being one-to-one I-valued Function such that
    A3: X c= product_prebasis J & X is finite & P = Intersect X & dom f = X and
    A4: P = product(Carrier J +* product_basis_selector(J,f)) by Lm3;
  set F = Carrier J +* product_basis_selector(J,f);
  per cases by A1, ZFMISC_1:33;
  suppose rng f = {};
    then a5: product_basis_selector(J,f) = {};
    take [#](J.i);
    thus thesis by a5,A2, A4, STRUCT_0:def 3;
  end;
  suppose A6: rng f = {i};
    then A7: dom f = {f".i} by Th1;
    A8: i in rng f by A6, TARSKI:def 1;
    A9: f".i in X by A3, A7, TARSKI:def 1;
    then reconsider V0 = f".i as Subset of product Carrier J;
    reconsider V = proj(J,i).:V0 as Subset of J.i;
    take V;
     V0 is empty or V0 is non empty;
    hence V is open by A3, A9, Th58;
    A10: product_basis_selector(J,f)
       = {i} --> product_basis_selector(J,f).i by A6, Th7
      .= {i} --> proj(J,i).:V0 by A8, Th54;
    dom Carrier J = {i} by A1, PARTFUN1:def 2;
    then dom Carrier J = dom product_basis_selector(J,f) by A6, PARTFUN1:def 2;
    hence thesis by A4,A10, FUNCT_4:19;
  end;
end;

Lm5:
  for I being 1-element set
  for J being TopSpace-yielding non-Empty ManySortedSet of I
  for i being Element of I, P being Subset of product Carrier J
  holds P in FinMeetCl product_prebasis J iff ex V being Subset of J.i
    st V is open & P = product ({i} --> V)
proof
  let I be 1-element set;
  let J be TopSpace-yielding non-Empty ManySortedSet of I;
  let i be Element of I;
  let P be Subset of product Carrier J;
  thus P in FinMeetCl product_prebasis J implies ex V being Subset of J.i
    st V is open & P = product ({i} --> V) by Lm4;
  given V being Subset of J.i such that
    A2: V is open & P = product ({i} --> V);
  P in product_prebasis J by A2, Th64;
  hence thesis by TARSKI:def 3, CANTOR_1:4;
end;

Lm6:
  for I being 1-element set
  for J being TopSpace-yielding non-Empty ManySortedSet of I
  for i being Element of I, P being Subset of product Carrier J
  holds P in UniCl FinMeetCl product_prebasis J iff ex V being Subset of J.i
    st V is open & P = product ({i} --> V)
proof
  let I be 1-element set;
  let J be TopSpace-yielding non-Empty ManySortedSet of I;
  let i be Element of I;
  card I = 1 by CARD_1:def 7;
  then A1: I = {i} by ORDERS_5:2;
  the carrier of J.i = [#](J.i) by STRUCT_0:def 3
    .= (Carrier J).i by PENCIL_3:7;
  then A2: Carrier J = {i} --> the carrier of J.i by A1, Th7;
  let P be Subset of product Carrier J;
  hereby
    assume P in UniCl FinMeetCl product_prebasis J;
    then consider Y being Subset-Family of product Carrier J such that
      A3: Y c= FinMeetCl product_prebasis J & P = union Y by CANTOR_1:def 1;
    :: each basis element points to an open set, we take the set
    :: of all these open sets and show that (set) P points to their union
    defpred P[object] means ex W being open Subset of J.i st
      W = $1 & product({i} --> W) in Y;
    consider Z being Subset of bool the carrier of J.i such that
      A4: for x being set holds x in Z iff
        x in bool the carrier of J.i & P[x] from SUBSET_1:sch 1;
    reconsider Z as Subset-Family of J.i;
    set V = union Z;
    take V;
    A5: for W being Subset of J.i holds W in Z iff W is open
      & product({i} --> W) in Y
    proof
      let W be Subset of J.i;
      hereby
        assume W in Z;
        then ex W2 being open Subset of J.i st
          W2 = W & product({i} --> W2) in Y by A4;
        hence W is open & product({i} --> W) in Y;
      end;
      assume W is open & product({i} --> W) in Y;
      hence thesis by A4;
    end;
    then for W being Subset of J.i holds W in Z implies W is open;
    hence V is open by TOPS_2:def 1, TOPS_2:19;
    for x being object holds x in union Y iff x in product ({i} --> V)
    proof
      let x be object;
      hereby
        assume x in union Y;
        then consider K being set such that
          A7: x in K & K in Y by TARSKI:def 4;
        reconsider K as Subset of product Carrier J by A7;
        consider L being Subset of J.i such that
          A8: L is open & K = product({i} --> L) by A3, A7, Lm5;
        A9: L in Z by A5, A7, A8;
        A10: L is non empty
        proof
          assume L is empty;
          then dom({i} --> L) = {i} & rng({i} --> L) = {{}}
            by FUNCOP_1:8;
          hence contradiction by A7, A8, Lm1;
        end;
        then consider y being Element of L such that
          A11: x = {i} --> y by A7, A8, Th16;
        y in V by A9, A10, TARSKI:def 4;
        hence x in product({i} --> V) by A11, Th16;
      end;
      assume A12: x in product({i} --> V);
      A13: V is non empty
      proof
        assume V is empty;
        then rng({i} --> V) = {{}} by FUNCOP_1:8;
        hence contradiction by A12, Lm1;
      end;
      then consider y being Element of V such that
        A14: x = {i} --> y by A12, Th16;
      consider L being set such that
        A15: y in L & L in Z by A13, TARSKI:def 4;
      reconsider L as Subset of J.i by A15;
      reconsider K= product({i} --> L) as Subset of product Carrier J
       by A2, Th14;
      A16: K in Y by A5, A15;
      x in K by A14, A15, Th16;
      hence thesis by A16, TARSKI:def 4;
    end;
    hence P = product ({i} --> V) by A3, TARSKI:2;
  end;
  assume ex V being Subset of J.i st V is open & P = product ({i} --> V);
  then P in FinMeetCl product_prebasis J by Lm5;
  hence thesis by CANTOR_1:1, TARSKI:def 3;
end;

Lm7:
  for I being 1-element set
  for J being TopSpace-yielding non-Empty ManySortedSet of I
  holds UniCl FinMeetCl product_prebasis J = product_prebasis J
proof
  let I be 1-element set;
  let J be TopSpace-yielding non-Empty ManySortedSet of I;
  for x being object holds x in UniCl FinMeetCl product_prebasis J
    iff x in product_prebasis J
  proof
    let x be object;
    set i = the Element of I;
    hereby
      assume A1: x in UniCl FinMeetCl product_prebasis J;
      then reconsider P=x as Subset of product Carrier J;
      ex V being Subset of J.i st V is open & P = product({i} --> V)
        by A1, Lm6;
      hence x in product_prebasis J by Th64;
    end;
    assume A2: x in product_prebasis J;
    then reconsider P=x as Subset of product Carrier J;
    ex V being Subset of J.i st V is open & P = product({i} --> V)
      by A2, Th64;
    hence thesis by Lm6;
  end;
  hence thesis by TARSKI:2;
end;

theorem Th65:
  for I being 1-element set
  for J being TopSpace-yielding non-Empty ManySortedSet of I
  holds the topology of product J = product_prebasis J
proof
  let I be 1-element set;
  let J be TopSpace-yielding non-Empty ManySortedSet of I;
  reconsider T = product J as TopSpace;
  reconsider K = product_prebasis J as Subset-Family of T by WAYBEL18:def 3;
  K is prebasis of T by WAYBEL18:def 3;
  then A1: UniCl FinMeetCl K = the topology of T by YELLOW_9:22, YELLOW_9:23;
  FinMeetCl K = FinMeetCl product_prebasis J by WAYBEL18:def 3;
  then UniCl FinMeetCl K = UniCl FinMeetCl product_prebasis J
    by WAYBEL18:def 3;
  hence thesis by A1, Lm7;
end;

:: characterization of open sets in the product topology over one factor
theorem
  for I being 1-element set
  for J being TopSpace-yielding non-Empty ManySortedSet of I
  for i being Element of I, P being Subset of product J
  holds P is open iff ex V being Subset of J.i
    st V is open & P = product ({i} --> V)
proof
  let I be 1-element set;
  let J be TopSpace-yielding non-Empty ManySortedSet of I;
  let i be Element of I;
  let P be Subset of product J;
  hereby
    assume P is open;
    then P in the topology of product J by PRE_TOPC:def 2;
    then P in product_prebasis J by Th65;
    hence ex V being Subset of J.i st V is open & P = product ({i} --> V)
      by Th64;
  end;
  A1: P is Subset of product Carrier J by WAYBEL18:def 3;
  assume ex V being Subset of J.i st V is open & P = product ({i} --> V);
  then P in product_prebasis J by A1, Th64;
  then P in the topology of product J by Th65;
  hence P is open by PRE_TOPC:def 2;
end;

registration
  let I being non empty set;
  let J being TopStruct-yielding non-Empty ManySortedSet of I;
  let i be Element of I;
  cluster proj(J,i) -> continuous onto;
  coherence
  proof
    rng proj(J,i) = the carrier of J.i by Th52;
    hence thesis by WAYBEL18:5, FUNCT_2:def 3;
  end;
end;

registration
  let I being non empty set;
  let J being TopSpace-yielding non-Empty ManySortedSet of I;
  let i be Element of I;
  cluster proj(J,i) -> open;
  coherence
  proof
    A1: ex B being Basis of product J st
      for P being Subset of product J st P in B holds proj(J,i).:P is open
    proof
      set B = FinMeetCl product_prebasis J;
      set T = product J;
      reconsider K = product_prebasis J as Subset-Family of T
        by WAYBEL18:def 3;
      FinMeetCl K is Basis of T by WAYBEL18:def 3, YELLOW_9:23;
      then reconsider B as Basis of product J by WAYBEL18:def 3;
      take B;
      let P be Subset of product J;
      assume A2: P in B;
      per cases;
      suppose P <> {};
        then ex I0 being finite Subset of I st
          for j being Element of I holds proj(J,j).:P is open &
            (not j in I0 implies proj(J,j).:P = [#](J.j))
          by A2, Th63;
        hence thesis;
      end;
      suppose P = {};
        then proj(J,i).:P is empty & proj(J,i).:P is Subset of J.i;
        hence thesis;
      end;
    end;
    product J is TopSpace & J.i is TopSpace;
    hence thesis by A1, Th45;
  end;
end;

theorem Th67:
  for I being 1-element set
  for J being TopSpace-yielding non-Empty ManySortedSet of I
  for i being Element of I holds proj(J,i) is being_homeomorphism
proof
  let I be 1-element set;
  let J be TopSpace-yielding non-Empty ManySortedSet of I;
  let i be Element of I;
  card I = 1 by CARD_1:def 7;
  then A1: I = {i} by ORDERS_5:2;
  :: we already have all properties ready and just need to collect them
  set f = proj(J,i);
  A2: dom f = the carrier of product J by FUNCT_2:def 1
    .= [#]product J by STRUCT_0:def 3;
  the carrier of J.i = [#](J.i) by STRUCT_0:def 3
    .= (Carrier J).i by PENCIL_3:7;
  then A3: Carrier J = {i} --> the carrier of J.i by A1, Th7;
  A4: rng f = the carrier of J.i by FUNCT_2:def 3
    .= [#](J.i) by STRUCT_0:def 3;
  a5: f = proj(Carrier J,i) by WAYBEL18:def 4
    .= proj(i .--> the carrier of J.i,i) by A3, FUNCOP_1:def 9;
  f" is continuous by a5, TOPREALA:14;
  hence f is being_homeomorphism by A2, A4, a5, TOPS_2:def 5;
end;

:: the product topology over one factor is homeomorphic to that factor
theorem
  for I being 1-element set
  for J being TopSpace-yielding non-Empty ManySortedSet of I
  for i being Element of I
  holds product J, J.i are_homeomorphic
proof
  let I be 1-element set;
  let J be TopSpace-yielding non-Empty ManySortedSet of I;
  let i be Element of I;
  proj(J,i) is being_homeomorphism by Th67;
  hence thesis by T_0TOPSP:def 1;
end;

Lm8:
  for I being 2-element set
  for J being TopSpace-yielding non-Empty ManySortedSet of I
  for i,j being Element of I, P being Subset of product Carrier J st i <> j
  holds P in product_prebasis J implies
    (ex V being Subset of J.i st
      V is open & P = product( (i,j) --> (V,[#](J.j)) ) ) or
    (ex W being Subset of J.j st
      W is open & P = product( (i,j) --> ([#](J.i),W) ) )
proof
  let I be 2-element set;
  let J be TopSpace-yielding non-Empty ManySortedSet of I;
  let i, j be Element of I, P be Subset of product Carrier J;
  assume A1: i <> j & P in product_prebasis J;
  then consider k being set, T being TopStruct, U being Subset of T such that
    A2: k in I & U is open & T = J.k & P = product ((Carrier J) +* (k,U))
    by WAYBEL18:def 2;
  k in {i,j} by A1, A2, Th8;
  then per cases by TARSKI:def 2;
  suppose A3: k = i;
    then reconsider V = U as Subset of J.i by A2;
    now
      take V;
      thus V is open by A2, A3;
      (Carrier J).j = [#](J.j) by PENCIL_3:7;
      hence P = product( (i,j) --> (V,[#](J.j)) ) by A2,A1, A3, Th34;
    end;
    hence thesis;
  end;
  suppose A4: k = j;
    then reconsider W = U as Subset of J.j by A2;
    now
      take W;
      thus W is open by A2, A4;
      (Carrier J).i = [#](J.i) by PENCIL_3:7;
      hence P = product( (i,j) --> ([#](J.i),W) ) by A2,A1, A4, Th34;
    end;
    hence thesis;
  end;
end;

:: characterization of the canonical prebasis of
:: the product topology over two factors
theorem Th69:
  for I being 2-element set
  for J being TopSpace-yielding non-Empty ManySortedSet of I
  for i,j being Element of I, P being Subset of product Carrier J st i <> j
  holds P in product_prebasis J iff
    (ex V being Subset of J.i st
      V is open & P = product((i,j) --> (V,[#](J.j)) ) ) or
    (ex W being Subset of J.j st
      W is open & P = product((i,j) --> ([#](J.i),W) ) )
proof
  let I be 2-element set;
  let J be TopSpace-yielding non-Empty ManySortedSet of I;
  let i, j be Element of I, P be Subset of product Carrier J;
  assume A1: i <> j;
  hence P in product_prebasis J implies
    (ex V being Subset of J.i st
      V is open & P = product( (i,j) --> (V,[#](J.j)) ) ) or
    (ex W being Subset of J.j st
      W is open & P = product( (i,j) --> ([#](J.i),W) ) ) by Lm8;
  assume
    (ex V being Subset of J.i st
      V is open & P = product( (i,j) --> (V,[#](J.j)) ) ) or
    (ex W being Subset of J.j st
      W is open & P = product( (i,j) --> ([#](J.i),W) ) );
  then per cases;
  suppose ex V being Subset of J.i st
    V is open & P = product( (i,j) --> (V,[#](J.j)) );
    then consider V being Subset of J.i such that
      A2: V is open & P = product( (i,j) --> (V,[#](J.j)) );
      (Carrier J).j = [#](J.j) by PENCIL_3:7;
      then P = product ((Carrier J) +* (i,V)) by A1, A2, Th34;
    hence P in product_prebasis J by A2,WAYBEL18:def 2;
  end;
  suppose ex W being Subset of J.j st
    W is open & P = product( (i,j) --> ([#](J.i),W) );
    then consider W being Subset of J.j such that
      A3: W is open & P = product( (i,j) --> ([#](J.i),W) );
      (Carrier J).i = [#](J.i) by PENCIL_3:7;
      then P = product ((Carrier J) +* (j,W)) by A1, A3, Th34;
    hence P in product_prebasis J by A3,WAYBEL18:def 2;
  end;
end;

Lm9:
  for I being 2-element set
  for J being TopSpace-yielding non-Empty ManySortedSet of I
  for i,j being Element of I, P being Subset of product Carrier J st i <> j
  holds P in FinMeetCl product_prebasis J implies
    ex V being Subset of J.i, W being Subset of J.j
    st V is open & W is open & P = product((i,j) --> (V,W))
proof
  let I be 2-element set;
  let J be TopSpace-yielding non-Empty ManySortedSet of I;
  let i,j be Element of I, P be Subset of product Carrier J;
  assume A1: i <> j & P in FinMeetCl product_prebasis J;
  then consider X being Subset-Family of product Carrier J,
    f being one-to-one I-valued Function such that
    A2: X c= product_prebasis J & X is finite & P = Intersect X & dom f = X and
    A3: P = product(Carrier J +* product_basis_selector(J,f)) by Lm3;
  set F = Carrier J +* product_basis_selector(J,f);
  i in I & j in I;
  then A4: i in dom Carrier J & j in dom Carrier J by PARTFUN1:def 2;
  rng f c= I;
  then rng f c= {i,j} by A1, Th8;
  then per cases by ZFMISC_1:36;
  :: all cases are structured the same way and are very much alike
  suppose rng f = {};
    then product_basis_selector(J,f) = {};
    then A5: P = product (i,j) --> ((Carrier J).i,(Carrier J).j)
        by A1, A3, Th9
      .= product (i,j) --> ([#](J.i),(Carrier J).j) by PENCIL_3:7
      .= product (i,j) --> ([#](J.i),[#](J.j)) by PENCIL_3:7;
    thus thesis by A5;
  end;
  suppose A6: rng f = {i};
    then A7: dom f = {f".i} by Th1;
    A8: i in rng f by A6, TARSKI:def 1;
    A9: f".i in X by A2, A7, TARSKI:def 1;
    then reconsider V0 = f".i as Subset of product Carrier J;
    reconsider V = proj(J,i).:V0 as Subset of J.i;
    take V, [#](J.j);
    V0 is empty or V0 is non empty;
    hence V is open & [#](J.j) is open by A2, A9, Th58;
    product_basis_selector(J,f)
       = {i} --> product_basis_selector(J,f).i by A6, Th7
      .= {i} --> proj(J,i).:(f".i) by A8, Th54
      .= i .--> V by FUNCOP_1:def 9;
    then F = Carrier J +* (i,V) by A4, FUNCT_7:def 3
      .= (i,j) --> (V,(Carrier J).j) by A1, Th34
      .= (i,j) --> (V,[#](J.j)) by PENCIL_3:7;
    hence thesis by A3;
  end;
  suppose A10: rng f = {j};
    then A11: dom f = {f".j} by Th1;
    A12: j in rng f by A10, TARSKI:def 1;
    A13: f".j in X by A2, A11, TARSKI:def 1;
    then reconsider W0 = f".j as Subset of product Carrier J;
    reconsider W = proj(J,j).:W0 as Subset of J.j;
    take [#](J.i), W;
    thus [#](J.i) is open;
   W0 is empty or W0 is non empty;
   hence W is open by A2, A13, Th58;
    product_basis_selector(J,f)
       = {j} --> product_basis_selector(J,f).j by A10, Th7
      .= {j} --> proj(J,j).:(f".j) by A12, Th54
      .= j .--> W by FUNCOP_1:def 9;
    then F = Carrier J +* (j,W) by A4, FUNCT_7:def 3
      .= (i,j) --> ((Carrier J).i,W) by A1, Th34
      .= (i,j) --> ([#](J.i),W) by PENCIL_3:7;
    hence thesis by A3;
  end;
  suppose A14: rng f = {i,j};
    then A15: dom f = {f".i, f".j} by Th2;
    A16: i in rng f & j in rng f by A14, TARSKI:def 2;
    A17: f".i in X & f".j in X by A2, A15, TARSKI:def 2;
    then reconsider V0 = f".i as Subset of product Carrier J;
    reconsider V = proj(J,i).:V0 as Subset of J.i;
    reconsider W0 = f".j as Subset of product Carrier J by A17;
    reconsider W = proj(J,j).:W0 as Subset of J.j;
    take V, W;
V0 is empty or V0 is non empty;
    hence V is open by A2, A17, Th58;
    W0 is empty or W0 is non empty;
    hence W is open by A2, A17, Th58;
    rng f = I by A1, A14, Th8;
    then A18: product_basis_selector(J,f) = (i,j)
        --> (product_basis_selector(J,f).i,product_basis_selector(J,f).j)
        by A1, Th9
      .= (i,j) --> (product_basis_selector(J,f).i,proj(J,j).:(f".j))
        by A16, Th54
      .= (i,j) --> (V,W) by A16, Th54;
    dom Carrier J = I by PARTFUN1:def 2
      .= {i,j} by A1, Th8;
    then dom Carrier J =dom product_basis_selector(J,f) by A14, PARTFUN1:def 2;
    hence thesis by A3, A18, FUNCT_4:19;
  end;
end;

:: characterization of the canonical basis of
:: the product topology over two factors
theorem
  for I being 2-element set
  for J being TopSpace-yielding non-Empty ManySortedSet of I
  for i,j being Element of I, P being Subset of product Carrier J st i <> j
  holds P in FinMeetCl product_prebasis J iff
    ex V being Subset of J.i, W being Subset of J.j
    st V is open & W is open & P = product((i,j) --> (V,W))
proof
  let I be 2-element set;
  let J be TopSpace-yielding non-Empty ManySortedSet of I;
  let i,j be Element of I, P be Subset of product Carrier J;
  assume A1: i <> j;
  hence P in FinMeetCl product_prebasis J implies
    ex V being Subset of J.i, W being Subset of J.j
    st V is open & W is open & P = product((i,j) --> (V,W)) by Lm9;
  given V being Subset of J.i, W being Subset of J.j such that
    A2: V is open & W is open & P = product((i,j) --> (V,W));
  ex Y being Subset-Family of product Carrier J
    st Y c= product_prebasis J & Y is finite & P = Intersect Y
  proof
    set V0 = product(Carrier J +* (i,V));
    set W0 = product(Carrier J +* (j,W));
    set Y = {V0,W0};
    A3: dom Carrier J = I by PARTFUN1:def 2;
    (Carrier J).i = [#](J.i) & (Carrier J).j = [#](J.j) by PENCIL_3:7;
    then a4: (Carrier J).i = the carrier of J.i &
      (Carrier J).j = the carrier of J.j by STRUCT_0:def 3;
    A5: V0 c= product Carrier J & W0 c= product Carrier J by a4,A3, Th39;
    then reconsider Y as Subset-Family of product Carrier J by ZFMISC_1:32;
    take Y;
    A6: V0 = product((i,j) --> (V,(Carrier J).j)) &
      W0 = product((i,j) --> ((Carrier J).i,W)) by A1, Th34;
    then V0 = product((i,j) --> (V,[#](J.j))) &
      W0 = product((i,j) --> ([#](J.i),W)) by PENCIL_3:7;
    then V0 in product_prebasis J & W0 in product_prebasis J
      by A1, A2, A5, Th69;
    hence Y c= product_prebasis J & Y is finite by ZFMISC_1:32;
    P c= V0 & P c= W0 by A2, a4, A6, Th28;
    then A7: P c= V0 /\ W0 by XBOOLE_1:19;
    V0 /\ W0 c= P
    proof
      let x be object;
      assume x in V0 /\ W0;
      then A8: x in V0 & x in W0 by XBOOLE_0:def 4;
      then consider g being Function such that
        A9: g = x & dom g = dom (i,j) --> (V,(Carrier J).j) and
        A10: for y being object st y in dom (i,j) --> (V,(Carrier J).j)
          holds g.y in ((i,j) --> (V,(Carrier J).j)).y by A6, CARD_3:def 5;
      A12: dom g = {i,j} by A9, FUNCT_4:62
        .= dom (i,j) --> (V,W) by FUNCT_4:62;
      for y being object st y in dom (i,j) --> (V,W)
        holds g.y in ((i,j) --> (V,W)).y
      proof
        let y be object;
        assume y in dom (i,j) --> (V,W);
        then A13: y in {i,j} by FUNCT_4:62;
        then per cases by TARSKI:def 2;
        suppose A14: y = i;
          then A15: ((i,j) --> (V,(Carrier J).j)).y = V by A1, FUNCT_4:63
            .= ((i,j) --> (V,W)).y by A1, A14, FUNCT_4:63;
          y in dom (i,j) --> (V,(Carrier J).j) by A13, FUNCT_4:62;
          hence thesis by A10, A15;
        end;
        suppose A16: y = j;
          then A17: ((i,j) --> ((Carrier J).i,W)).y = W by FUNCT_4:63
            .= ((i,j) --> (V,W)).y by A16, FUNCT_4:63;
          y in dom (i,j) --> ((Carrier J).i,W) by A13, FUNCT_4:62;
          hence thesis by A6, A8, A9, CARD_3:9, A17;
        end;
      end;
      hence x in P by A2, A9, A12, CARD_3:9;
    end;
    then P = V0 /\ W0 by A7, XBOOLE_0:def 10;
    then P = meet Y by SETFAM_1:11;
    hence P = Intersect Y by SETFAM_1:def 9;
  end;
  hence P in FinMeetCl product_prebasis J by CANTOR_1:def 3;
end;

theorem ::Th71:
  for I being non empty set
  for J being TopSpace-yielding non-Empty ManySortedSet of I
  for i,j being Element of I
  holds <: proj(J,i), proj(J,j) :> is Function of product J, [: J.i, J.j :]
  by BORSUK_1:def 2;

:: can be generalized: P only needs to contain the square F.i x F.j
:: at one point p, the Proof works the same
theorem Th72:
  for I being non empty set
  for J being TopSpace-yielding non-Empty ManySortedSet of I
  for P being Subset of product Carrier J
  for i,j being Element of I st i <> j &
    (ex F being ManySortedSet of I st P = product F &
      for k being Element of I holds F.k c= (Carrier J).k)
  holds <: proj(J,i), proj(J,j) :>.:P = [: proj(J,i).:P, proj(J,j).:P :]
proof
  let I be non empty set;
  let J be TopSpace-yielding non-Empty ManySortedSet of I;
  let P be Subset of product Carrier J;
  let i,j be Element of I;
  assume that A1: i <> j and
    A2: ex F being ManySortedSet of I st P = product F &
      for k being Element of I holds F.k c= (Carrier J).k;
  consider F being ManySortedSet of I such that
    A3: P = product F and
    A4: for k being Element of I holds F.k c= (Carrier J).k by A2;
  per cases;
  suppose A5: F is non-empty;
    for y being object holds y in [: proj(J,i).:P, proj(J,j).:P :]
      implies y in <: proj(J,i), proj(J,j) :>.:P
    proof
      let y be object;
      assume y in [: proj(J,i).:P, proj(J,j).:P :];
      then consider y1, y2 being object such that
        A6: y1 in proj(J,i).:P & y2 in proj(J,j).:P & y = [y1,y2]
        by ZFMISC_1:def 2;
      A7: dom F = I by PARTFUN1:def 2
        .= dom Carrier J by PARTFUN1:def 2;
      i in I & j in I;
      then A8: i in dom F & j in dom F by PARTFUN1:def 2;
      for k being object st k in dom F holds F.k c= (Carrier J).k by A4;
      :: here is the square F.i x F.j I mentioned above
      then proj(Carrier J,i).:P = F.i & proj(Carrier J,j).:P = F.j
        by A3, A5, A7, A8, Th26;
      then A9: proj(J,i).:P = F.i & proj(J,j).:P = F.j by WAYBEL18:def 4;
      set p0 = the Element of product F;
      set p = p0 +* (i,j) --> (y1,y2);
      A10: dom <: proj(J,i), proj(J,j) :> = dom proj(J,i) /\ dom proj(J,j)
          by FUNCT_3:def 7
        .= dom proj(Carrier J,i) /\ dom proj(J,j) by WAYBEL18:def 4
        .= dom proj(Carrier J,i) /\ dom proj(Carrier J,j) by WAYBEL18:def 4;
      then A11: dom <: proj(J,i), proj(J,j) :>
         = dom proj(Carrier J,i) /\ product Carrier J by CARD_3:def 16
        .= product Carrier J /\ product Carrier J by CARD_3:def 16
        .= product Carrier J;
      p in product(F +* (i,j) --> (F.i,F.j)) by A1, A6, A5, A9, Th30;
      then A12: p in P by A3, A8, Th11;
      then A14: p in dom proj(Carrier J,i) & p in dom proj(Carrier J,j)
        by A11,A10, XBOOLE_0:def 4;
      A15: proj(J,i).p = proj(Carrier J,i).p by WAYBEL18:def 4
        .= p.i by A14, CARD_3:def 16
        .= y1 by A1, FUNCT_4:84;
      A16: proj(J,j).p = proj(Carrier J,j).p by WAYBEL18:def 4
        .= p.j by A14, CARD_3:def 16
        .= y2 by A1, FUNCT_4:84;
      <: proj(J,i), proj(J,j) :>.p = [y1,y2] by A11,A12,A15,A16, FUNCT_3:def 7;
      hence thesis by A6, A12, A11, FUNCT_1:def 6;
    end;
    then A17: [: proj(J,i).:P, proj(J,j).:P :] c= <: proj(J,i), proj(J,j) :>.:P
      by TARSKI:def 3;
    <: proj(J,i), proj(J,j) :>.:P c= [: proj(J,i).:P, proj(J,j).:P :]
      by FUNCT_3:56;
    hence thesis by A17, XBOOLE_0:def 10;
  end;
  suppose not F is non-empty;
    then {} in rng F by RELAT_1:def 9;
    then P = {} by A3, CARD_3:26;
    then <: proj(J,i), proj(J,j) :>.:P = {} &  proj(J,i).:P = {};
    hence thesis by ZFMISC_1:90;
  end;
end;

theorem Th73:
  for I being non empty set
  for J being TopSpace-yielding non-Empty ManySortedSet of I
  for i,j being Element of I, f being Function of product J, [: J.i, J.j :]
  st i <> j & f = <: proj(J,i), proj(J,j) :>
  holds f is onto open
proof
  let I be non empty set;
  let J be TopSpace-yielding non-Empty ManySortedSet of I;
  let i,j be Element of I, f be Function of product J, [: J.i, J.j :];
  assume A1: i <> j & f = <: proj(J,i), proj(J,j) :>;
  :: onto is corrolary from previous theorem
  a2:  for k being Element of I holds Carrier J.k c= (Carrier J).k;
  A3: for k being Element of I holds
    proj(J,k).:[#]product Carrier J = the carrier of J.k
  proof
    let k be Element of I;
    thus proj(J,k).:[#]product Carrier J
       = proj(J,k).:product Carrier J by SUBSET_1:def 3
      .= proj(J,k).:dom proj(Carrier J,k) by CARD_3:def 16
      .= proj(J,k).:dom proj(J,k) by WAYBEL18:def 4
      .= rng proj(J,k) by RELAT_1:113
      .= the carrier of J.k by Th52;
  end;
  rng f = <: proj(J,i), proj(J,j) :>.:dom f by A1, RELAT_1:113
    .= <: proj(J,i), proj(J,j) :>.:the carrier of product J by FUNCT_2:def 1
    .= <: proj(J,i), proj(J,j) :>.:product Carrier J by WAYBEL18:def 3
    .= <: proj(J,i), proj(J,j) :>.:[#]product Carrier J by SUBSET_1:def 3
    .= [: proj(J,i).:[#]product Carrier J, proj(J,j).:[#]product Carrier J :]
      by A1, SUBSET_1:def 3,a2, Th72
    .= [: the carrier of J.i, proj(J,j).:[#]product Carrier J :] by A3
    .= [: the carrier of J.i, the carrier of J.j :] by A3
    .= the carrier of [: J.i, J.j :] by BORSUK_1:def 2;
  hence f is onto by FUNCT_2:def 3;
  :: openness will be shown using the canonical base of the product space,
  :: the Theorem of canonical base characterisation and the previous theorem
  ex B being Basis of product J st
    for P being Subset of product J st P in B holds f.:P is open
  proof
    set B = FinMeetCl product_prebasis J;
    set T = product J;
    reconsider K = product_prebasis J as Subset-Family of T
      by WAYBEL18:def 3;
    FinMeetCl K is Basis of T by WAYBEL18:def 3, YELLOW_9:23;
    then reconsider B as Basis of product J by WAYBEL18:def 3;
    take B;
    let P be Subset of product J;
    assume A4: P in B;
    A5: proj(J,i).:P is open & proj(J,j).:P is open
    proof
      per cases;
      suppose P <> {};
        then ex I0 being finite Subset of I st
          for j being Element of I holds proj(J,j).:P is open &
            (not j in I0 implies proj(J,j).:P = [#](J.j)) by A4, Th63;
        hence thesis;
      end;
      suppose P = {};
        then proj(J,i).:P is empty & proj(J,i).:P is Subset of J.i &
          proj(J,j).:P is empty & proj(J,j).:P is Subset of J.j;
        hence thesis;
      end;
    end;
    A7: ex F being ManySortedSet of I st P = product F &
      for k being Element of I holds F.k c= (Carrier J).k
    proof
      consider X being Subset-Family of product Carrier J,
        g being one-to-one I-valued Function such that
          X c= product_prebasis J & X is finite & P=Intersect X & dom g = X and
          A8: P = product(Carrier J +* product_basis_selector(J,g))
        by A4, Lm3;
      set F = Carrier J +* product_basis_selector(J,g);
      reconsider F as ManySortedSet of I;
      take F;
      thus P = product F by A8;
      let k be Element of I;
      per cases;
      suppose A9: k in rng g;
        then k in dom product_basis_selector(J,g) by PARTFUN1:def 2;
        then a10: F.k = product_basis_selector(J,g).k by FUNCT_4:13
          .= proj(J,k).:(g".k) by A9, Th54;
        rng proj(J,k) = the carrier of J.k by Th52
          .= [#](J.k) by STRUCT_0:def 3
          .= (Carrier J).k by PENCIL_3:7;
        hence thesis by a10,RELAT_1:111;
      end;
      suppose not k in rng g;
        then not k in dom product_basis_selector(J,g);
        hence thesis by FUNCT_4:11;
      end;
    end;
    P is Subset of product Carrier J by WAYBEL18:def 3;
    then f.:P = [: proj(J,i).:P, proj(J,j).:P :] by A1, A7, Th72;
    hence f.:P is open by A5, BORSUK_1:6;
  end;
  hence f is open by Th45;
end;

theorem Th74:
  for I being 2-element set
  for J being TopSpace-yielding non-Empty ManySortedSet of I
  for i,j being Element of I, f being Function of product J, [: J.i, J.j :]
  st i <> j & f = <: proj(J,i), proj(J,j) :>
  holds f is being_homeomorphism
proof
  let I be 2-element set;
  let J be TopSpace-yielding non-Empty ManySortedSet of I;
  let i,j be Element of I, f be Function of product J, [: J.i, J.j :];
  :: we need to show the one-to-one property, the rest can simply be collected
  assume A1: i <> j & f = <: proj(J,i), proj(J,j) :>;
  A2: dom f = the carrier of product J by FUNCT_2:def 1
    .= [#]product J by STRUCT_0:def 3;
  A3: f is onto open by A1, Th73;
  then rng f = the carrier of [: J.i, J.j :] by FUNCT_2:def 3;
  then A4: rng f = [#][: J.i, J.j :] by STRUCT_0:def 3;
  for x1, x2 being object st x1 in dom f & x2 in dom f & f.x1 = f.x2
    holds x1 = x2
  proof
    let x1, x2 be object;
    assume A5: x1 in dom f & x2 in dom f & f.x1 = f.x2;
    then a6:f.x1 = [proj(J,i).x1, proj(J,j).x1] &
       f.x2 = [proj(J,i).x2, proj(J,j).x2] by A1, FUNCT_3:def 7;
    x1 in dom proj(J,i) /\ dom proj(J,j) &
      x2 in dom proj(J,i) /\ dom proj(J,j) by A1, A5, FUNCT_3:def 7;
    then x1 in dom proj(J,i) & x2 in dom proj(J,j) by XBOOLE_0:def 4;
    then a7: x1 in dom proj(Carrier J,i) & x2 in dom proj(Carrier J,j)
      by WAYBEL18:def 4;
    reconsider g1 = x1, g2 = x2 as Element of product J by A5;
    proj(J,i).x1 = g1.i & proj(J,i).x2 = g2.i &
      proj(J,j).x1 = g1.j & proj(J,j).x2 = g2.j by YELLOW17:8;
    then A8: g1.i = g2.i & g1.j = g2.j by a6,A5, XTUPLE_0:1;
    A9: Carrier J = (i,j) --> ((Carrier J).i,(Carrier J).j) by A1, Th9;
    then consider a1,b1 being object such that
      a1 in (Carrier J).i & b1 in (Carrier J).j and
      A10: g1 = (i,j) --> (a1,b1) by A1, a7, Th29;
    consider a2,b2 being object such that
      a2 in (Carrier J).i & b2 in (Carrier J).j and
      A11: g2 = (i,j) --> (a2,b2) by A1, a7, A9, Th29;
    g1.i = a1 & g2.i = a2 & g1.j = b1 & g2.j = b2 by A1, A10, A11, FUNCT_4:63;
    hence thesis by A8, A10, A11;
  end;
  then A12: f is one-to-one by FUNCT_1:def 4;
  A13: f is continuous by A1, YELLOW12:41;
  f" is continuous by A3, A12, TOPREALA:14;
  hence f is being_homeomorphism by A2, A4, A12, A13, TOPS_2:def 5;
end;

:: the product topology over two factors is
:: homeomorphic to the cartesian product of these two factors
:: ( [: S,T :], [: T,S :] are_homeomorphic is a corrolary,
::  but it is already in the MML)
theorem
  for I being 2-element set
  for J being TopSpace-yielding non-Empty ManySortedSet of I
  for i,j being Element of I st i <> j
  holds product J, [: J.i,J.j :] are_homeomorphic
proof
  let I be 2-element set;
  let J be TopSpace-yielding non-Empty ManySortedSet of I;
  let i,j be Element of I;
  assume A1: i <> j;
  reconsider f = <: proj(J,i), proj(J,j) :>
    as Function of product J, [: J.i, J.j :] by BORSUK_1:def 2;
  f is being_homeomorphism by A1,Th74;
  hence thesis by T_0TOPSP:def 1;
end;

registration
  let I1, I2 be non empty set;
  let J be TopSpace-yielding non-Empty ManySortedSet of I2;
  let f be Function of I1, I2;
  cluster J*f -> TopSpace-yielding non-Empty;
  coherence
  proof
    hereby
      let y be object;
      assume y in rng(J*f);
      then y in rng J by RELAT_1:26, TARSKI:def 3;
      hence y is TopSpace by Def1;
    end;
    for S being 1-sorted st S in rng(J*f) holds S is non empty
    proof
      let S be 1-sorted;
      assume S in rng (J*f);
      then S in rng J by RELAT_1:26, TARSKI:def 3;
      hence thesis by WAYBEL_3:def 7;
    end;
    hence thesis by WAYBEL_3:def 7;
  end;
end;

definition
  let I1, I2 be non empty set;
  let J1 be TopSpace-yielding non-Empty ManySortedSet of I1;
  let J2 be TopSpace-yielding non-Empty ManySortedSet of I2;
  let p be Function of I1, I2;
  assume that A1: p is bijective and
    A2: for i being Element of I1 holds J1.i, (J2*p).i are_homeomorphic;
  mode ProductHomeo of J1, J2, p -> Function of product J1, product J2 means
  :Def5:
  ex F being ManySortedFunction of I1 st
    (for i being Element of I1 ex f being Function of J1.i, (J2*p).i
      st F.i = f & f is being_homeomorphism) &
    for g being Element of product J1, i being Element of I1 holds
      (it.g).(p.i) = (F.i).(g.i); :: H(g)_{p_i} = F_i(g_i)
  existence
  proof
    defpred P[object,object] means
      ex i being Element of I1, f being Function of J1.i, (J2*p).i
      st $1 = i & $2 = f & f is being_homeomorphism;
    A3: for x being object st x in I1 ex y being object st P[x,y]
    proof
      let x be object;
      assume x in I1;
      then reconsider i = x as Element of I1;
      consider f being Function of J1.i, (J2*p).i such that
        A4: f is being_homeomorphism by A2, T_0TOPSP:def 1;
      take f,i,f;
      thus thesis by A4;
    end;
    consider F being ManySortedSet of I1 such that
      A5: for x being object st x in I1 holds P[x,F.x] from PBOOLE:sch 3(A3);
    A6: for i being Element of I1 ex f being Function of J1.i, (J2*p).i
      st F.i = f & f is being_homeomorphism
    proof
      let i be Element of I1;
      consider j being Element of I1, f being Function of J1.j, (J2*p).j
        such that A7: i = j & F.i = f & f is being_homeomorphism by A5;
      reconsider f as Function of J1.i, (J2*p).i by A7;
      take f;
      thus thesis by A7;
    end;
    for x being object st x in dom F holds F.x is Function
    proof
      let x be object;
      assume x in dom F;
      then reconsider i = x as Element of I1;
      ex f being Function of J1.i, (J2*p).i st
         F.i = f & f is being_homeomorphism by A6;
      hence thesis;
    end;
    then reconsider F as ManySortedFunction of I1 by FUNCOP_1:def 6;
    defpred Q[object,object] means
      ex g being Element of product J1, h being Element of product J2
      st $1 = g & $2 = h &
        for i being Element of I1 holds h.(p.i) = (F.i).(g.i);
    A9: for x being object st x in the carrier of product J1
      ex y being object st y in the carrier of product J2 & Q[x,y]
    proof
      let x be object;
      assume x in the carrier of product J1;
      then reconsider g = x as Element of product J1;
      :: since Q is a little bit sophisticated, we need to
      :: construct the RHS using another scheme
      deffunc H(object) = (F.$1).(g.$1);
      consider h0 being ManySortedSet of I1 such that
        A10: for i being Element of I1 holds h0.i = H(i) from PBOOLE:sch 5;
      reconsider p9 = p as one-to-one Function by A1;
      rng(p9") = dom p9 by FUNCT_1:33
        .= I1 by FUNCT_2:def 1
        .= dom h0 by PARTFUN1:def 2;
      then dom(h0*(p9")) = dom(p9") by RELAT_1:27
        .= rng p9 by FUNCT_1:33
        .= I2 by A1, FUNCT_2:def 3;
      then reconsider h = h0*(p9") as ManySortedSet of I2
        by PARTFUN1:def 2, RELAT_1:def 18;
      take h;
      A11: dom h = I2 by PARTFUN1:def 2
        .= dom Carrier J2 by PARTFUN1:def 2;
      for x being object st x in dom Carrier J2 holds h.x in (Carrier J2).x
      proof
        let x be object;
        assume x in dom Carrier J2;
        then reconsider j = x as Element of I2;
        j in I2;
        then A12: j in rng p9 by A1, FUNCT_2:def 3;
        then A13: j in dom(p9") by FUNCT_1:33;
        then p9".j in rng(p9") by FUNCT_1:3;
        then p9".j in dom p9 by FUNCT_1:33;
        then reconsider i = p9".j as Element of I1 by FUNCT_2:def 1;
        A14: (F.i).(g.i) = h0.i by A10
          .= h.j by A13, FUNCT_1:13;
        consider f being Function of J1.i, (J2*p).i such that
          A15: F.i = f & f is being_homeomorphism by A6;
        A16: f.(g.i) in the carrier of (J2*p).i;
        i in I1;
        then i in dom p by FUNCT_2:def 1;
        then (J2*p).i = J2.(p.i) by FUNCT_1:13
          .= J2.j by A12, FUNCT_1:35;
        then h.j in [#](J2.j) by A14, A15, A16, STRUCT_0:def 3;
        hence thesis by PENCIL_3:7;
      end;
      then H: h in product Carrier J2 by A11, CARD_3:9;
      hence h in the carrier of product J2 by WAYBEL18:def 3;
      reconsider h as Element of product J2 by H,WAYBEL18:def 3;
      take g, h;
      now
        let i be Element of I1;
        i in I1;
        then A17: i in dom p by PARTFUN1:def 2;
        then p9.i in rng p9 by FUNCT_1:3;
        then A18: p9.i in dom(p9") by FUNCT_1:33;
        thus h.(p.i) = h0.(p9".(p9.i)) by A18, FUNCT_1:13
          .= h0.i by A17, FUNCT_1:34
          .= (F.i).(g.i) by A10;
      end;
      hence thesis;
    end;
    consider IT being Function
      of the carrier of product J1, the carrier of product J2 such that
      A19: for x being object st x in the carrier of product J1 holds Q[x,IT.x]
      from FUNCT_2:sch 1(A9);
    reconsider IT as Function of product J1, product J2;
    take IT, F;
    now
      let g be Element of product J1;
      A20: ex g0 being Element of product J1,
        h being Element of product J2 st
        g = g0 & IT.g = h &
          for i being Element of I1 holds h.(p.i) = (F.i).(g0.i) by A19;
      let i be Element of I1;
      thus (IT.g).(p.i) = (F.i).(g.i) by A20;
    end;
    hence thesis by A6;
  end;
end;

:: characterization of images of certain subsets under product homeomorphism
theorem Th76:
  for I1, I2 being non empty set
  for J1 being TopSpace-yielding non-Empty ManySortedSet of I1
  for J2 being TopSpace-yielding non-Empty ManySortedSet of I2
  for p being Function of I1, I2, H being ProductHomeo of J1, J2, p
  for F being ManySortedFunction of I1
  st p is bijective &
    (for i being Element of I1 ex f being Function of J1.i, (J2*p).i
      st F.i = f & f is being_homeomorphism) &
    (for g being Element of product J1, i being Element of I1 holds
      (H.g).(p.i) = (F.i).(g.i))
  holds for i being Element of I1, U being Subset of J1.i holds
    H.:product(Carrier J1 +* (i,U)) = product(Carrier J2 +* (p.i,(F.i).:U))
proof
  let I1, I2 be non empty set;
  let J1 be TopSpace-yielding non-Empty ManySortedSet of I1;
  let J2 be TopSpace-yielding non-Empty ManySortedSet of I2;
  let p be Function of I1, I2, H be ProductHomeo of J1, J2, p;
  let F be ManySortedFunction of I1;
  assume that
    A1: p is bijective and
    A2: for i being Element of I1 ex f being Function of J1.i, (J2*p).i
      st F.i = f & f is being_homeomorphism and
    A3: for g being Element of product J1, i being Element of I1 holds
      (H.g).(p.i) = (F.i).(g.i);
  let i be Element of I1, U be Subset of J1.i;
  reconsider j = p.i as Element of I2;
  i in I1;
  then A4: i in dom p by FUNCT_2:def 1;
  consider f being Function of J1.i, (J2*p).i such that
    A5: F.i = f & f is being_homeomorphism by A2;
  A6: rng f = [#]((J2*p).i) by A5, TOPS_2:def 5
    .= [#](J2.j) by A4, FUNCT_1:13
    .= the carrier of J2.j by STRUCT_0:def 3;
  :: the rest of the Proof is so sophisticated because of the sophisticated
  :: definition of H
  for y being object holds y in H.:product(Carrier J1 +* (i,U))
    iff y in product(Carrier J2 +* (j,(F.i).:U))
  proof
    let y be object;
    thus y in H.:product(Carrier J1 +* (i,U))
      implies y in product(Carrier J2 +* (j,(F.i).:U))
    proof
      assume y in H.:product(Carrier J1 +* (i,U));
      then consider x being object such that
        A8: x in dom H & x in product(Carrier J1 +* (i,U)) & y = H.x
        by FUNCT_1:def 6;
      reconsider g = x as Element of product J1 by A8;
      y in rng H by A8, FUNCT_1:3;
      then reconsider h = y as Element of product J2;
      h in the carrier of product J2;
      then A9: h in product Carrier J2 by WAYBEL18:def 3;
      then A10: dom h = dom Carrier J2 by CARD_3:9
        .= dom(Carrier J2 +* (j,(F.i).:U)) by FUNCT_7:30;
      for z being object st z in dom(Carrier J2 +* (j,(F.i).:U))
        holds h.z in (Carrier J2 +* (j,(F.i).:U)).z
      proof
        let z be object;
        assume a11: z in dom(Carrier J2 +* (j,(F.i).:U));
        then A11: z in dom Carrier J2 by FUNCT_7:30;
        reconsider j0 = z as Element of I2 by a11;
        I2 = rng p by A1, FUNCT_2:def 3;
        then consider i0 being object such that
          A12: i0 in I1 & p.i0 = j0 by FUNCT_2:11;
        reconsider i0 as Element of I1 by A12;
        consider f0 being Function of J1.i0, (J2*p).i0 such that
          A13: F.i0 = f0 & f0 is being_homeomorphism by A2;
        A14: h.j0 = f0.(g.i0) by A3, A8, A12, A13;
        per cases;
        suppose A15: j0 = j;
          then A16: (Carrier J2 +* (j,(F.i).:U)).z = (F.i).:U
            by A11, FUNCT_7:31;
          A17: i0 = i by A1, A12, A15, FUNCT_2:19;
          a18: I1 = dom Carrier J1 by PARTFUN1:def 2;
          then i in dom Carrier J1;
          then i in dom(Carrier J1 +* (i,U)) by FUNCT_7:30;
          then g.i in (Carrier J1 +* (i,U)).i by A8, CARD_3:9;
          then g.i in U by a18, FUNCT_7:31;
          hence thesis by A14, A16, A17, A13, FUNCT_2:35;
        end;
        suppose j0 <> j;
          then (Carrier J2 +* (j,(F.i).:U)).z = (Carrier J2).z by FUNCT_7:32;
          hence thesis by A9, A11, CARD_3:9;
        end;
      end;
      hence y in product(Carrier J2 +* (j,(F.i).:U)) by A10, CARD_3:9;
    end;
    assume A20: y in product(Carrier J2 +* (j,(F.i).:U));
    then reconsider h = y as Element of product (Carrier J2 +* (j,(F.i).:U));
    A21: the carrier of J1.i = [#](J1.i) by STRUCT_0:def 3
      .= (Carrier J1).i by PENCIL_3:7;
    i in I1;
    then A22: i in dom Carrier J1 by PARTFUN1:def 2;
    then A23: product(Carrier J1 +* (i,U)) c= product Carrier J1
      by A21, Th39;
    A24: (Carrier J2).j = [#](J2.j) by PENCIL_3:7
      .= the carrier of J2.j by STRUCT_0:def 3;
    a25: j in I2 & (F.i).:U c= the carrier of J2.j by A6, A5, RELAT_1:111;
    then A25: j in dom Carrier J2 & (F.i).:U c= (Carrier J2).j
      by A24, PARTFUN1:def 2;
    then A26: product(Carrier J2 +* (j,(F.i).:U)) c= product Carrier J2
      by Th39;
    ex x being object
      st x in dom H & x in product(Carrier J1 +* (i,U)) & H.x = y
    proof
      :: some parts of this Proof were copied from the onto Proof of H
      defpred P[object,object] means ex f being one-to-one Function
        st F.$1 = f & $2 = f".(h.(p.$1));
      A28: for i0 being Element of I1 ex y being object st P[i0,y]
      proof
        let i0 be Element of I1;
        consider f0 being Function of J1.i0, (J2*p).i0 such that
          A29: F.i0 = f0 & f0 is being_homeomorphism by A2;
        reconsider f0 as one-to-one Function by A29;
        take f0".(h.(p.i0)), f0;
        thus thesis by A29;
      end;
      consider g being ManySortedSet of I1 such that
        A30: for i being Element of I1 holds P[i,g.i]
          from PBOOLE:sch 6(A28);
      take g;
      A31: dom g = I1 by PARTFUN1:def 2
        .= dom(Carrier J1 +* (i,U)) by PARTFUN1:def 2;
     a36: for z being object st z in dom(Carrier J1 +* (i,U))
        holds g.z in (Carrier J1 +* (i,U)).z
      proof
        let z be object;
        assume z in dom(Carrier J1 +* (i,U));
        then reconsider i0 = z as Element of I1;
        consider f0 being one-to-one Function such that
          A32: F.i0 = f0 & g.i0 = f0".(h.(p.i0)) by A30;
        p.i0 in I2;
        then p.i0 in dom Carrier J2 by PARTFUN1: def 2;
        then h.(p.i0) in (Carrier J2).(p.i0) by A20, A26, CARD_3:9;
        then h.(p.i0) in [#](J2.(p.i0)) by PENCIL_3:7;
        then A33: h.(p.i0) in [#]((J2*p).i0) by FUNCT_2:15;
        per cases;
        suppose A35: i = i0;
          then A36: (Carrier J1 +* (i,U)).z = U by A22, FUNCT_7:31;
          j in dom(Carrier J2 +* (j,(F.i).:U))
          by a25,PARTFUN1:def 2;
          then h.j in (Carrier J2 +* (j,(F.i).:U)).j by A20, CARD_3:9;
          then A37: h.j in (F.i).:U by A25, FUNCT_7:31;
          A38: f" = f0" by A5, A32, A35, TOPS_2:def 4;
            [#]((J2*p).i0) = rng f by A5, A35, TOPS_2:def 5
              .= dom(f0") by A5, A32, A35, FUNCT_1:33;
            then g.i0 in rng(f0") by A32, A33, FUNCT_1:3;
            then A39:g.i0 in dom f by A5, A32, A35, FUNCT_1:33;
          h.j in (Carrier J2).j by A20, A26, A25, CARD_3:9;
          then h.j in [#](J2.j) by PENCIL_3:7;
          then a40: h.j in [#]((J2*p).i) by A4, FUNCT_1:13;
          a41: dom f = the carrier of J1.i by FUNCT_2:def 1;
          reconsider f1 = f as one-to-one Function by A5;
          A43: h.j in rng f1 by a40,A5, TOPS_2:def 5;
             f.(f".(h.j)) = f1.(f1".(h.j)) by A5, TOPS_2:def 4
              .= h.j by A43, FUNCT_1:35;
          then g.i0 in f0"(f0.:U) by A5, A32, A35, A38,A39,A37, FUNCT_1:def 7;
          hence thesis by A36, a41,A5, A32, A35, FUNCT_1:94;
        end;
        suppose i <> i0;
          then A44: (Carrier J1 +* (i,U)).z = (Carrier J1).z
            by FUNCT_7:32;
          consider f9 being Function of J1.i0, (J2*p).i0 such that
            A45: F.i0 = f9 & f9 is being_homeomorphism by A2;
          dom(f0") = rng f0 by FUNCT_1:33
            .= [#]((J2*p).i0) by A32, A45, TOPS_2:def 5
            .= the carrier of (J2*p).i0 by STRUCT_0:def 3;
          then f0".(h.(p.i0)) in rng(f0") by A33, FUNCT_1:3;
          then g.i0 in dom f0 by A32, FUNCT_1:33;
          then g.i0 in [#](J1.i0) by A32, A45, TOPS_2:def 5;
          hence thesis by A44, PENCIL_3:7;
        end;
      end;
      then g in product(Carrier J1 +* (i,U)) by A31, CARD_3:9;
      then g in product Carrier J1 by A23;
      then A47: g in the carrier of product J1 by WAYBEL18:def 3;
      hence g in dom H & g in product(Carrier J1 +* (i,U))
        by a36,A31, CARD_3:9, FUNCT_2:def 1;
      reconsider h0 = H.g as Element of product J2
        by A47,FUNCT_2:5;
      h0 in the carrier of product J2;
      then h0 in product Carrier J2 by WAYBEL18:def 3;
      then A48: dom h0 = dom Carrier J2 by CARD_3:9
        .= dom h by A20, A26, CARD_3:9;
      for z being object st z in dom h holds h.z = h0.z
      proof
        let z be object;
        assume z in dom h;
        then z in dom Carrier J2 by A20, A26, CARD_3:9;
        then reconsider j0 = z as Element of I2;
        reconsider p9 = p as one-to-one Function by A1;
        j0 in I2;
        then A49: j0 in rng p9 by A1, FUNCT_2:def 3;
        then j0 in dom(p9") by FUNCT_1:33;
        then p9".j0 in rng(p9") by FUNCT_1:3;
        then A50: p9".j0 in dom p9 by FUNCT_1:33;
        then reconsider i0 = p9".j0 as Element of I1 by FUNCT_2:def 1;
        consider f9 being one-to-one Function such that
          A51: F.i0 = f9 & g.i0 = f9".(h.(p.i0)) by A30;
        consider f0 being Function of J1.i0, (J2*p).i0 such that
          A52: F.i0 = f0 & f0 is being_homeomorphism by A2;
        A53: rng f9 = [#]((J2*p).i0) by A51, A52, TOPS_2:def 5
          .= the carrier of (J2*p).i0 by STRUCT_0:def 3;
        A54: p.i0 = j0 by A49, FUNCT_1:35;
        A55: (Carrier J2).(p.i0) = [#](J2.(p.i0)) by PENCIL_3:7
          .= [#]((J2*p).i0) by A50, FUNCT_1:13
          .= the carrier of (J2*p).i0 by STRUCT_0:def 3;
        p.i0 in I2;
        then p.i0 in dom Carrier J2 by PARTFUN1:def 2;
        then A56: h.(p.i0) in (Carrier J2).(p.i0) by A20, A26, CARD_3:9;
        h.j0 = f9.(f9".(h.(p.i0))) by A53, A54, A55, A56, FUNCT_1:35
          .= h0.j0 by A3, A47, A51, A54;
        hence thesis;
      end;
      hence H.g = y by A48, FUNCT_1:2;
    end;
    hence thesis by FUNCT_1:def 6;
  end;
  hence thesis by TARSKI:2;
end;

theorem Th77:
  for I1, I2 being non empty set
  for J1 being TopSpace-yielding non-Empty ManySortedSet of I1
  for J2 being TopSpace-yielding non-Empty ManySortedSet of I2
  for p being Function of I1, I2, H being ProductHomeo of J1, J2, p
  st p is bijective &
    for i being Element of I1 holds J1.i, (J2*p).i are_homeomorphic
  holds H is bijective
proof
  let I1, I2 be non empty set;
  let J1 be TopSpace-yielding non-Empty ManySortedSet of I1;
  let J2 be TopSpace-yielding non-Empty ManySortedSet of I2;
  let p be Function of I1, I2, H be ProductHomeo of J1, J2, p;
  assume that A1: p is bijective and
    A2: for i being Element of I1 holds J1.i, (J2*p).i are_homeomorphic;
  consider F being ManySortedFunction of I1 such that
    A3: for i being Element of I1 ex f being Function of J1.i, (J2*p).i
      st F.i = f & f is being_homeomorphism and
    A4: for g being Element of product J1, i being Element of I1 holds
      (H.g).(p.i) = (F.i).(g.i) by A1, A2, Def5;
  for x1,x2 being object st x1 in dom H & x2 in dom H & H.x1 = H.x2
    holds x1 = x2
  proof
    let x1,x2 be object;
    assume A5: x1 in dom H & x2 in dom H & H.x1 = H.x2;
    then reconsider g1 = x1, g2 = x2 as Element of product J1;
    A6: g1 is Element of product Carrier J1 &
      g2 is Element of product Carrier J1 by WAYBEL18:def 3;
    A7: dom g1 = dom Carrier J1 by A6, CARD_3:9
      .= dom g2 by A6, CARD_3:9;
    for z being object st z in dom g1 holds g1.z = g2.z
    proof
      let z be object;
      assume z in dom g1;
      then z in dom Carrier J1 by A6, CARD_3:9;
      then reconsider i = z as Element of I1;
      a8: (H.g1).(p.i) = (F.i).(g1.i) & (H.g2).(p.i) = (F.i).(g2.i) by A4;
      consider f being Function of J1.i, (J2*p).i such that
        A9: F.i = f & f is being_homeomorphism by A3;
      A12: (Carrier J1).i = [#](J1.i) by PENCIL_3:7
        .= the carrier of J1.i by STRUCT_0:def 3
        .= dom f by FUNCT_2:def 1;
      i in I1;
      then i in dom Carrier J1 by PARTFUN1:def 2;
      then g1.i in (Carrier J1).i & g2.i in (Carrier J1).i by A6, CARD_3:9;
      hence thesis by a8,A5, A9, A12, FUNCT_1:def 4;
    end;
    hence thesis by A7, FUNCT_1:2;
  end;
  then A13: H is one-to-one by FUNCT_1:def 4;
  set i0 = the Element of I1;
  consider f0 being Function of J1.i0, (J2*p).i0 such that
    A14: F.i0 = f0 & f0 is being_homeomorphism by A3;
  i0 in I1;
  then A15: i0 in dom p by FUNCT_2:def 1;
  rng H = H.:dom H by RELAT_1:113
    .= H.:the carrier of product J1 by FUNCT_2:def 1
    .= H.:product Carrier J1 by WAYBEL18:def 3
    .= H.:product(Carrier J1 +* (i0,(Carrier J1).i0)) by FUNCT_7:35
    .= H.:product(Carrier J1 +* (i0,[#](J1.i0))) by PENCIL_3:7
    .= product(Carrier J2 +* (p.i0,(F.i0).:[#](J1.i0))) by A1, A3, A4, Th76
    .= product(Carrier J2 +* (p.i0,f0.:dom f0)) by A14, TOPS_2:def 5
    .= product(Carrier J2 +* (p.i0,rng f0)) by RELAT_1:113
    .= product(Carrier J2 +* (p.i0,[#]((J2*p).i0))) by A14, TOPS_2:def 5
    .= product(Carrier J2 +* (p.i0,[#](J2.(p.i0)))) by A15, FUNCT_1:13
    .= product(Carrier J2 +* (p.i0,(Carrier J2).(p.i0))) by PENCIL_3:7
    .= product Carrier J2 by FUNCT_7:35
    .= the carrier of product J2 by WAYBEL18:def 3;
  then H is onto by FUNCT_2:def 3;
  hence thesis by A13;
end;

theorem Th78:
  for I1, I2 being non empty set
  for J1 being TopSpace-yielding non-Empty ManySortedSet of I1
  for J2 being TopSpace-yielding non-Empty ManySortedSet of I2
  for p being Function of I1, I2, H being ProductHomeo of J1, J2, p
  st p is bijective &
    for i being Element of I1 holds J1.i, (J2*p).i are_homeomorphic
  holds H is being_homeomorphism
proof
  let I1, I2 be non empty set;
  let J1 be TopSpace-yielding non-Empty ManySortedSet of I1;
  let J2 be TopSpace-yielding non-Empty ManySortedSet of I2;
  let p be Function of I1, I2, H be ProductHomeo of J1, J2, p;
  assume that
    A1: p is bijective and
    A2: for i being Element of I1 holds J1.i, (J2*p).i are_homeomorphic;
  consider F being ManySortedFunction of I1 such that
    A3: for i being Element of I1 ex f being Function of J1.i, (J2*p).i
      st F.i = f & f is being_homeomorphism and
    A4: for g being Element of product J1, i being Element of I1 holds
      (H.g).(p.i) = (F.i).(g.i) by A1, A2, Def5;
  A5: H is bijective by A1, A2, Th77;
  :: using the canonical product prebasis for both J1 and J2
  :: and showing that H maps one to the other, we are already done
  :: with the bijectivity of H
  ex K being prebasis of product J1, L being prebasis of product J2 st H.:K = L
  proof
    reconsider K = product_prebasis J1 as prebasis of product J1
      by WAYBEL18:def 3;
    reconsider L = product_prebasis J2 as prebasis of product J2
      by WAYBEL18:def 3;
    take K, L;
    :: we use the characterization of images under H above to show the equality
    for W being Subset of product J2 holds W in L iff
      ex V being Subset of product J1 st V in K & H.:V = W
    proof
      let W be Subset of product J2;
      thus W in L implies ex V being Subset of product J1 st V in K & H.:V = W
      proof
        assume W in L;
        then consider j being set, T being TopStruct, W0j being Subset of T
          such that A6: j in I2 & W0j is open & T = J2.j and
          A7: W = product (Carrier J2 +* (j,W0j)) by WAYBEL18:def 2;
        reconsider j as Element of I2 by A6;
        reconsider Wj = W0j as Subset of J2.j by A6;
        j in I2;
        then j in rng p by A1, FUNCT_2:def 3;
        then consider i being object such that
          A8: i in I1 & p.i = j by FUNCT_2:11;
        A9: i in dom p by A8, FUNCT_2:def 1;
        reconsider i as Element of I1 by A8;
        consider f being Function of J1.i, (J2*p).i such that
          A10: F.i = f & f is being_homeomorphism by A3;
        reconsider Vi = f"Wj as Subset of J1.i;
        A11: the carrier of J1.i = [#](J1.i) by STRUCT_0:def 3
          .= (Carrier J1).i by PENCIL_3:7;
        i in dom Carrier J1 by A8, PARTFUN1:def 2;
        then product(Carrier J1 +* (i,Vi)) c= product Carrier J1 by A11, Th39;
        then reconsider V = product(Carrier J1 +* (i,Vi))
          as Subset of product J1 by WAYBEL18:def 3;
        take V;
        A12: V is Subset of product Carrier J1 by WAYBEL18:def 3;
        ex k being set, S being TopStruct, U being Subset of S
          st k in I1 & U is open & S = J1.k & V = product(Carrier J1 +* (k,U))
        proof
          take i, J1.i, Vi;
          reconsider W1j = Wj as Subset of (J2*p).i by A8, A9, FUNCT_1:13;
          W0j in the topology of J2.j by A6, PRE_TOPC:def 2;
          then W1j in the topology of (J2*p).i by A8, A9, FUNCT_1:13;
          then A14: W1j is open by PRE_TOPC:def 2;
          [#]((J2*p).i) = {} implies [#](J1.i) = {};
          hence thesis by A10, A14, TOPS_2:43;
        end;
        hence V in K by A12, WAYBEL18:def 2;
          reconsider f0 = f as one-to-one Function by A10;
          rng f0 = [#]((J2*p).i) by A10, TOPS_2:def 5
            .= [#](J2.j) by A9, A8, FUNCT_1:13
            .= the carrier of J2.j by STRUCT_0:def 3;
          then f.:(f"Wj) = Wj by FUNCT_1:77;
        hence H.:V = W by A1, A3, A4, A7, A8, Th76,A10;
      end;
      given V being Subset of product J1 such that
        A16: V in K & H.:V = W;
      consider i being set, S being TopStruct, Vi being Subset of S such that
        A17: i in I1 & Vi is open & S = J1.i and
        A18: V = product ((Carrier J1) +* (i,Vi))
        by A16, WAYBEL18:def 2;
      reconsider i as Element of I1 by A17;
      reconsider Vi as Subset of J1.i by A17;
      A19: W is Subset of product Carrier J2 by WAYBEL18:def 3;
      ex j being set, T being TopStruct, U being Subset of T
        st j in I2 & U is open & T = J2.j & W = product(Carrier J2 +* (j,U))
      proof
        reconsider j = p.i as Element of I2;
        consider f being Function of J1.i, (J2*p).i such that
          A20: F.i = f & f is being_homeomorphism by A3;
        a21: i in dom p by A17, FUNCT_2:def 1;
        then A21: (J2*p).i = J2.j by FUNCT_1:13;
        reconsider Wj = f.:Vi as Subset of J2.j by a21,FUNCT_1:13;
        take j, J2.j, Wj;
        thus j in I2 & Wj is open & J2.j = J2.j
           by A21,A17, A20, T_0TOPSP:def 2;
        thus W = product(Carrier J2 +* (j,Wj))
            by A16,A1, A3, A4, A18, A20, Th76;
      end;
      hence W in L by A19, WAYBEL18:def 2;
    end;
    hence H.:K = L by FUNCT_2:def 10;
  end;
  hence thesis by A5, Th48;
end;

:: pairwise homeomorphic factors lead to homeomorphic products
theorem Th79:
  for I1, I2 being non empty set
  for J1 being TopSpace-yielding non-Empty ManySortedSet of I1
  for J2 being TopSpace-yielding non-Empty ManySortedSet of I2
  for p being Function of I1, I2
  st p is bijective &
    for i being Element of I1 holds J1.i, (J2*p).i are_homeomorphic
  holds product J1, product J2 are_homeomorphic
proof
  let I1, I2 be non empty set;
  let J1 be TopSpace-yielding non-Empty ManySortedSet of I1;
  let J2 be TopSpace-yielding non-Empty ManySortedSet of I2;
  let p be Function of I1, I2;
  assume that
    A1: p is bijective and
    A2: for i being Element of I1 holds J1.i, (J2*p).i are_homeomorphic;
  set H = the ProductHomeo of J1, J2, p;
  H is being_homeomorphism by A1, A2, Th78;
  hence thesis by T_0TOPSP:def 1;
end;

theorem
  for I being non empty set
  for J1, J2 being TopSpace-yielding non-Empty ManySortedSet of I
  for p being Permutation of I
  st for i being Element of I holds J1.i, (J2*p).i are_homeomorphic
  holds product J1, product J2 are_homeomorphic by Th79;

:: permutations of the underlying set family lead to a homeomorphic copy of
:: the original product
:: (the following one could also be done with TopStruct-yielding
::  but then the theorems before couldn't be used and the long argumentation
::  would have to be repeated for most parts)
theorem
  for I being non empty set
  for J being TopSpace-yielding non-Empty ManySortedSet of I
  for p being Permutation of I
  holds product J, product(J*p) are_homeomorphic
proof
  let I be non empty set;
  let J be TopSpace-yielding non-Empty ManySortedSet of I;
  let p be Permutation of I;
  reconsider q = p" as Permutation of I;
  now
    let i be Element of I;
    A1: J = J*id dom J by RELAT_1:52
      .= J*id I by PARTFUN1:def 2
      .= J*(p*q) by FUNCT_2:61
      .= (J*p)*q by RELAT_1:36;
    thus J.i, ((J*p)*q).i are_homeomorphic by A1;
  end;
  hence product J, product(J*p) are_homeomorphic by Th79;
end;

:: if each factor of the first product is a subspace of a corresponding
:: factor of the second product, the first product is a subspae of the second
theorem
  for I being non empty set
  for J1, J2 being TopSpace-yielding non-Empty ManySortedSet of I
  st for i being Element of I holds J1.i is SubSpace of J2.i
  holds product J1 is SubSpace of product J2
proof
  let I be non empty set;
  let J1 be TopSpace-yielding non-Empty ManySortedSet of I;
  let J2 be TopSpace-yielding non-Empty ManySortedSet of I;
  assume A1: for i being Element of I holds J1.i is SubSpace of J2.i;
  ex K1 being prebasis of product J1, K2 being prebasis of product J2
    st [#]product J1 in K1 & K1 = INTERSECTION(K2,{[#]product J1})
  proof
    reconsider K1 = product_prebasis J1 as prebasis of product J1
      by WAYBEL18:def 3;
    reconsider K2 = product_prebasis J2 as prebasis of product J2
      by WAYBEL18:def 3;
    take K1, K2;
    A2: [#]product J1 = the carrier of product J1 by STRUCT_0:def 3
      .= product Carrier J1 by WAYBEL18:def 3;
    then [#]product J1 = [#]product Carrier J1 by SUBSET_1:def 3;
    then reconsider P = [#]product J1 as Subset of product Carrier J1;
    ex i being set, T being TopStruct, V being Subset of T
      st i in I & V is open & T = J1.i & P = product(Carrier J1 +* (i,V))
    proof
      set i = the Element of I;
      take i, J1.i, [#](J1.i);
      thus i in I & [#](J1.i) is open & J1.i = J1.i;
      thus P = product(Carrier J1 +* (i,(Carrier J1).i)) by A2, FUNCT_7:35
        .=  product(Carrier J1 +* (i,[#](J1.i))) by PENCIL_3:7;
    end;
    hence [#]product J1 in K1 by WAYBEL18:def 2;
    for U being set holds U in K1 iff
      ex A, P0 being set st A in K2 & P0 in {[#]product J1} & U = A /\ P0
    proof
      let U be set;
      A3: for i being Element of I, V being Subset of J1.i,
        W being Subset of J2.i st V = W /\ [#](J1.i)
        holds Carrier J1 +* (i,V) = (Carrier J2 +* (i,W)) (/\) Carrier J1
      proof
        let i be Element of I, V be Subset of J1.i, W be Subset of J2.i;
        assume A4: V = W /\ [#](J1.i);
        A5: dom(Carrier J1 +* (i,V)) = I by PARTFUN1:def 2
          .= dom((Carrier J2 +* (i,W)) (/\) Carrier J1) by PARTFUN1:def 2;
        for x being object st x in dom(Carrier J1 +* (i,V))
          holds (Carrier J1 +* (i,V)).x =
            ((Carrier J2 +* (i,W)) (/\) Carrier J1).x
        proof
          let x be object;
          assume a6: x in dom(Carrier J1 +* (i,V));
          then A6: x in dom Carrier J1 by FUNCT_7:30;
          A7: x in I by a6;
          reconsider j = x as Element of I by a6;
          A8: x in dom Carrier J2 by A7, PARTFUN1:def 2;
          per cases;
          suppose A9: x = i;
            hence (Carrier J1 +* (i,V)).x = V by A6, FUNCT_7:31
              .= (Carrier J2 +* (i,W)).x /\ [#](J1.i)
                by A4, A8, A9, FUNCT_7:31
              .= (Carrier J2 +* (i,W)).x /\ (Carrier J1).i by PENCIL_3:7
              .= ((Carrier J2 +*(i,W)) (/\) Carrier J1).x
                by A9, PBOOLE:def 5;
          end;
          suppose A10: x <> i;
            A11: (Carrier J1).j = [#](J1.j) & (Carrier J2).j = [#](J2.j)
              by PENCIL_3:7;
            a12: J1.j is SubSpace of J2.j by A1;
            thus (Carrier J1 +* (i,V)).x = (Carrier J1).x by A10, FUNCT_7:32
              .= (Carrier J2).x /\ (Carrier J1).x
                  by a12, XBOOLE_1:28,A11, PRE_TOPC:def 4
              .= (Carrier J2 +* (i,W)).x /\ (Carrier J1).x by A10, FUNCT_7:32
              .= ((Carrier J2 +*(i,W)) (/\) Carrier J1).x
                by a6, PBOOLE:def 5;
          end;
        end;
        hence Carrier J1 +* (i,V) = (Carrier J2 +* (i,W)) (/\) Carrier J1
          by A5, FUNCT_1:2;
      end;
      thus U in K1 implies ex A, P0 being set
        st A in K2 & P0 in {[#]product J1} & U = A /\ P0
      proof
        assume U in K1;
        then consider i being set, T being TopStruct, V being Subset of T
          such that A13: i in I & V is open & T = J1.i and
          A14: U = product(Carrier J1 +* (i,V)) by WAYBEL18:def 2;
        reconsider i as Element of I by A13;
        A15: V in the topology of J1.i by A13, PRE_TOPC:def 2;
        reconsider V as Subset of J1.i by A13;
        J1.i is SubSpace of J2.i by A1;
        then consider W being Subset of J2.i such that
          A16: W in the topology of J2.i & V = W /\ [#](J1.i)
          by A15, PRE_TOPC:def 4;
        set A = product(Carrier J2 +* (i,W));
        take A, P;
        (Carrier J2).i = [#](J2.i) by PENCIL_3:7
          .= the carrier of J2.i by STRUCT_0:def 3;
        then i in dom Carrier J2 & W c= (Carrier J2).i by A13, PARTFUN1:def 2;
        then A17: A is Subset of product Carrier J2 by Th39;
        ex i9 being set, T9 being TopStruct, V9 being Subset of T9 st i9 in I &
          V9 is open & T9 = J2.i9 & A = product(Carrier J2 +* (i9,V9))
          by A16, PRE_TOPC:def 2;
        hence A in K2 by A17, WAYBEL18:def 2;
        thus P in {[#]product J1} by TARSKI:def 1;
        thus U = product((Carrier J2 +* (i,W)) (/\) Carrier J1) by A14, A16, A3
          .= A /\ P by A2, Th33;
      end;
      given A, P0 being set such that
        A18: A in K2 & P0 in {[#]product J1} & U = A /\ P0;
      consider i being set, T being TopStruct, W being Subset of T such that
        A19: i in I & W is open & T = J2.i and
        A20: A = product(Carrier J2 +* (i,W)) by A18, WAYBEL18:def 2;
      reconsider i as Element of I by A19;
      A21: W in the topology of J2.i by A19, PRE_TOPC:def 2;
      reconsider W as Subset of J2.i by A19;
      set V = W /\ [#](J1.i);
      A22: V c= [#](J1.i) by XBOOLE_1:17;
      reconsider V as Subset of J1.i;
      P0 = product Carrier J1 by A2, A18, TARSKI:def 1;
      then A23: U
         = product((Carrier J2 +* (i,W)) (/\) Carrier J1) by A18, A20, Th33
        .= product(Carrier J1 +* (i,V)) by A3;
      A24: i in dom Carrier J1 by A19, PARTFUN1:def 2;
      V c= (Carrier J1).i by A22, PENCIL_3:7;
      then A25: U c= product Carrier J1 by A23, A24, Th39;
      ex i9 being set, T9 being TopStruct, V9 being Subset of T9
        st i9 in I & V9 is open & T9 = J1.i9 &
          U = product(Carrier J1 +* (i9,V9))
      proof
        take i, J1.i, V;
        thus i in I;
        J1.i is SubSpace of J2.i by A1;
        then V in the topology of J1.i by A21, PRE_TOPC:def 4;
        hence thesis by A23, PRE_TOPC:def 2;
      end;
      hence U in K1 by A25, WAYBEL18:def 2;
    end;
    hence thesis by SETFAM_1:def 5;
  end;
  hence thesis by Th51;
end;