:: Some Remarks about Product Spaces :: by Sebastian Koch :: :: Received September 29, 2018 :: Copyright (c) 2018-2021 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; begin :: Preliminaries :: into FUNCT_1 ? :: compare FUNCT_1:4 theorem :: TOPS_5:1 for f being one-to-one Function, y being object st rng f = {y} holds dom f = {f".y}; :: into FUNCT_1 ? theorem :: TOPS_5:2 for f being one-to-one Function, y1, y2 being object st rng f = {y1, y2} holds dom f = {f".y1, f".y2}; :: into PARTFUN1 ? registration let X, Y be set; cluster empty X-defined Y-valued one-to-one for Function; 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; end; :: into RELSET_2 ? theorem :: TOPS_5:3 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}; :: into RELSET_2 ? theorem :: TOPS_5:4 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}; :: into EQREL_1 ? theorem :: TOPS_5:5 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; :: into FUNCOP_1 ? theorem :: TOPS_5:6 for X being non empty set, x,y being object st X --> x = X --> y holds x = y; :: into FUNCOP_1 ? theorem :: TOPS_5:7 for i being object, J being ManySortedSet of {i} holds J = {i} --> J.i; :: into CARD_1 ? theorem :: TOPS_5:8 for I being 2-element set, i,j being Element of I st i <> j holds I = {i,j}; :: into FUNCT_4 ? :: compare FUNCT_4:66 theorem :: TOPS_5:9 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); :: into FUNCT_4 ? theorem :: TOPS_5:10 for a,b,c,d being object st a <> b holds (a,b) --> (c,d) = (b,a) --> (d,c); :: into FUNCT_4 ? theorem :: TOPS_5:11 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); :: into FUNCT_4 ? :: compare FUNCT_7:15, FUNCT_4:114 theorem :: TOPS_5:12 for x,y,z being object holds (x .--> y) +* (x .--> z) = x .--> z; :: into PBOOLE ? registration cluster non non-empty for Function; end; :: BEGIN into CARD_3 ? theorem :: TOPS_5:13 for X, Y being non empty set, y being Element of Y holds X --> y in product (X --> Y); theorem :: TOPS_5:14 for X being non empty set, Y being set, Z being Subset of Y holds product(X --> Z) c= product (X --> Y); theorem :: TOPS_5:15 for X being non empty set, i being object holds product ({i} --> X) = {{i} --> x where x is Element of X : not contradiction} ; theorem :: TOPS_5:16 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; :: compare YELLOW17:8 theorem :: TOPS_5:17 for X being non empty set, i being object, x being Element of X holds proj({i} --> X,i).({i} --> x) = x; :: compare CARD_3:26 theorem :: TOPS_5:18 for X, Y being set holds X <> {} & Y = {} iff product (X --> Y) = {}; registration let f be empty Function, x be object; cluster proj(f,x) -> trivial; end; theorem :: TOPS_5:19 for f being trivial Function, x being object st x in dom f holds proj(f,x) is one-to-one; registration let x,y be object; cluster proj(x .--> y,x) -> one-to-one; 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; end; theorem :: TOPS_5:20 for X being non empty set, Y being Subset of X, i being object holds proj({i} --> X,i).:product ({i} --> Y) = Y; theorem :: TOPS_5:21 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; theorem :: TOPS_5:22 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; theorem :: TOPS_5:23 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; theorem :: TOPS_5:24 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; theorem :: TOPS_5:25 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; theorem :: TOPS_5:26 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; theorem :: TOPS_5:27 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)); theorem :: TOPS_5:28 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)); theorem :: TOPS_5:29 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); theorem :: TOPS_5:30 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)); theorem :: TOPS_5:31 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)); theorem :: TOPS_5:32 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; :: $\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 :: TOPS_5:33 for I being set, f, g being ManySortedSet of I holds product f /\ product g = product(f (/\) g); theorem :: TOPS_5:34 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); theorem :: TOPS_5:35 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; theorem :: TOPS_5:36 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; theorem :: TOPS_5:37 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)); theorem :: TOPS_5:38 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)); :: compare YELLOW17:2 theorem :: TOPS_5:39 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); theorem :: TOPS_5:40 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; theorem :: TOPS_5:41 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; theorem :: TOPS_5:42 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; theorem :: TOPS_5:43 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; theorem :: TOPS_5:44 for x,y,z being object holds (x .--> y) +* (x,z) = x .--> z; :: 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; end; begin :: Remarks about Product Spaces theorem :: TOPS_5:45 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; theorem :: TOPS_5:46 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; theorem :: TOPS_5:47 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; theorem :: TOPS_5:48 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; :: compare TOPGEN_5:71 (the converse) theorem :: TOPS_5:49 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; theorem :: TOPS_5:50 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; theorem :: TOPS_5:51 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; theorem :: TOPS_5:52 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; registration let X be set, T be TopStruct; cluster X --> T -> TopStruct-yielding; end; definition let F be Relation; attr F is TopSpace-yielding means :: TOPS_5:def 1 for x being object st x in rng F holds x is TopSpace; end; registration cluster TopSpace-yielding -> TopStruct-yielding for Relation; end; registration cluster TopSpace-yielding -> 1-sorted-yielding for Function; end; registration let X be set, T be TopSpace; cluster X --> T -> TopSpace-yielding; end; registration let I be set; cluster TopSpace-yielding non-Empty for ManySortedSet of I; 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; end; definition let f be Function; func ProjMap f -> ManySortedFunction of dom f means :: TOPS_5:def 2 for x being object st x in dom f holds it.x = proj(f,x); end; registration let f be empty Function; cluster ProjMap f -> empty; end; registration let f be non-empty Function; cluster ProjMap f -> non-empty; end; registration let f be non non-empty Function; cluster ProjMap f -> empty-yielding; 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 :: TOPS_5:def 3 ProjMap Carrier J; 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; end; theorem :: TOPS_5:53 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); :: 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 :: TOPS_5:def 4 ((ProjMap J).:.:(I-indexing(f"))) | rng f; 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; end; theorem :: TOPS_5:54 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); theorem :: TOPS_5:55 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; theorem :: TOPS_5:56 for I being non empty set for J being TopSpace-yielding non-Empty ManySortedSet of I holds {} in product_prebasis J; :: compare YELLOW17:16 theorem :: TOPS_5:57 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); theorem :: TOPS_5:58 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); theorem :: TOPS_5:59 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); theorem :: TOPS_5:60 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)); :: Theorem of canonical product base characterization theorem :: TOPS_5:61 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)); theorem :: TOPS_5:62 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)); theorem :: TOPS_5:63 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)); :: characterization of the canonical prebasis of :: the product topology over one factor theorem :: TOPS_5:64 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); theorem :: TOPS_5:65 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; :: characterization of open sets in the product topology over one factor theorem :: TOPS_5:66 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); 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; 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; end; theorem :: TOPS_5:67 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; :: the product topology over one factor is homeomorphic to that factor theorem :: TOPS_5:68 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; :: characterization of the canonical prebasis of :: the product topology over two factors theorem :: TOPS_5:69 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) ) ); :: characterization of the canonical basis of :: the product topology over two factors theorem :: TOPS_5:70 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)); theorem :: TOPS_5:71 ::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 :]; :: 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 :: TOPS_5:72 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 :]; theorem :: TOPS_5:73 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; theorem :: TOPS_5:74 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; :: 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 :: TOPS_5:75 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; 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; 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 p is bijective and 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 :: TOPS_5:def 5 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); end; :: characterization of images of certain subsets under product homeomorphism theorem :: TOPS_5:76 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)); theorem :: TOPS_5:77 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; theorem :: TOPS_5:78 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; :: pairwise homeomorphic factors lead to homeomorphic products theorem :: TOPS_5:79 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; theorem :: TOPS_5:80 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; :: 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 :: TOPS_5:81 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; :: 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 :: TOPS_5:82 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;