:: by Sebastian Koch

::

:: Received September 29, 2018

:: Copyright (c) 2018-2019 Association of Mizar Users

:: into FUNCT_1 ?

theorem Th2: :: TOPS_5:2

for f being one-to-one Function

for y1, y2 being object st rng f = {y1,y2} holds

dom f = {((f ") . y1),((f ") . y2)}

for y1, y2 being object st rng f = {y1,y2} holds

dom f = {((f ") . y1),((f ") . y2)}

proof end;

:: into PARTFUN1 ?

registration

let X, Y be set ;

existence

ex b_{1} being Function st

( b_{1} is empty & b_{1} is X -defined & b_{1} is Y -valued & b_{1} is one-to-one )

end;
existence

ex b

( b

proof 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;

coherence

f .: G is finite

end;
let f be Function of T,S;

let G be finite Subset-Family of T;

coherence

f .: G is finite

proof end;

:: into RELSET_2 ?

theorem Th3: :: TOPS_5:3

for A being set

for F being Subset-Family of A

for R being Relation holds R .: (meet F) c= meet { (R .: X) where X is Subset of A : X in F }

for F being Subset-Family of A

for R being Relation holds R .: (meet F) c= meet { (R .: X) where X is Subset of A : X in F }

proof end;

:: into RELSET_2 ?

theorem Th4: :: TOPS_5:4

for A being set

for F being Subset-Family of A

for f being one-to-one Function holds f .: (meet F) = meet { (f .: X) where X is Subset of A : X in F }

for F being Subset-Family of A

for f being one-to-one Function holds f .: (meet F) = meet { (f .: X) where X is Subset of A : X in F }

proof end;

:: into EQREL_1 ?

theorem Th5: :: TOPS_5:5

for X being set

for Y being non empty set

for f being Function of X,Y holds { (f " {y}) where y is Element of Y : y in rng f } is a_partition of X

for Y being non empty set

for 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 end;

:: into FUNCOP_1 ?

:: into FUNCOP_1 ?

:: into CARD_1 ?

:: into FUNCT_4 ?

:: compare FUNCT_4:66

:: compare FUNCT_4:66

theorem Th9: :: TOPS_5:9

for I being 2 -element set

for f being ManySortedSet of I

for i, j being Element of I st i <> j holds

f = (i,j) --> ((f . i),(f . j))

for f being ManySortedSet of I

for i, j being Element of I st i <> j holds

f = (i,j) --> ((f . i),(f . j))

proof end;

:: into FUNCT_4 ?

:: into FUNCT_4 ?

theorem Th11: :: TOPS_5:11

for f being Function

for i, j being object st i in dom f & j in dom f holds

f = f +* ((i,j) --> ((f . i),(f . j)))

for i, j being object st i in dom f & j in dom f holds

f = f +* ((i,j) --> ((f . i),(f . j)))

proof end;

:: into FUNCT_4 ?

:: compare FUNCT_7:15, FUNCT_4:114

:: compare FUNCT_7:15, FUNCT_4:114

:: into PBOOLE ?

:: BEGIN into CARD_3 ?

theorem Th14: :: TOPS_5:14

for X being non empty set

for Y being set

for Z being Subset of Y holds product (X --> Z) c= product (X --> Y)

for Y being set

for Z being Subset of Y holds product (X --> Z) c= product (X --> Y)

proof end;

theorem Th15: :: TOPS_5:15

for X being non empty set

for i being object holds product ({i} --> X) = { ({i} --> x) where x is Element of X : verum }

for i being object holds product ({i} --> X) = { ({i} --> x) where x is Element of X : verum }

proof end;

theorem Th16: :: TOPS_5:16

for X being non empty set

for i, f being object holds

( f in product ({i} --> X) iff ex x being Element of X st f = {i} --> x )

for i, f being object holds

( f in product ({i} --> X) iff ex x being Element of X st f = {i} --> x )

proof end;

:: compare YELLOW17:8

theorem :: TOPS_5:17

for X being non empty set

for i being object

for x being Element of X holds (proj (({i} --> X),i)) . ({i} --> x) = x

for i being object

for x being Element of X holds (proj (({i} --> X),i)) . ({i} --> x) = x

proof end;

Lm1: for f being Function st rng f = {{}} holds

product f = {}

proof end;

:: compare CARD_3:26

registration
end;

registration

let I be 1 -element set ;

let J be ManySortedSet of I;

let i be Element of I;

coherence

proj (J,i) is one-to-one

end;
let J be ManySortedSet of I;

let i be Element of I;

coherence

proj (J,i) is one-to-one

proof end;

theorem :: TOPS_5:20

for X being non empty set

for Y being Subset of X

for i being object holds (proj (({i} --> X),i)) .: (product ({i} --> Y)) = Y

for Y being Subset of X

for i being object holds (proj (({i} --> X),i)) .: (product ({i} --> Y)) = Y

proof end;

theorem Th21: :: TOPS_5:21

for f, g being non-empty Function

for i, x being object st x in (product f) /\ (product (f +* g)) holds

(proj (f,i)) . x = (proj ((f +* g),i)) . x

for i, x being object st x in (product f) /\ (product (f +* g)) holds

(proj (f,i)) . x = (proj ((f +* g),i)) . x

proof end;

theorem Th22: :: TOPS_5:22

for f, g being non-empty Function

for i being object

for A being set st A c= (product f) /\ (product (f +* g)) holds

(proj (f,i)) .: A = (proj ((f +* g),i)) .: A

for i being object

for A being set st A c= (product f) /\ (product (f +* g)) holds

(proj (f,i)) .: A = (proj ((f +* g),i)) .: A

proof end;

theorem Th23: :: 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

g . i c= f . i ) holds

product (f +* g) c= product f

proof end;

theorem Th24: :: 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

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 end;

theorem Th25: :: 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

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 end;

theorem Th26: :: 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

g . i c= f . i ) holds

for i being object st i in dom g holds

(proj (f,i)) .: (product g) = g . i

proof end;

theorem Th27: :: TOPS_5:27

for f being Function

for X, Y being set

for i being object st X c= Y holds

product (f +* (i .--> X)) c= product (f +* (i .--> Y))

for X, Y being set

for i being object st X c= Y holds

product (f +* (i .--> X)) c= product (f +* (i .--> Y))

proof end;

theorem Th28: :: TOPS_5:28

for i, j being object

for 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))

for 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 end;

theorem Th29: :: TOPS_5:29

for X, Y being set

for 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) ) )

for 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 end;

theorem Th30: :: TOPS_5:30

for f being non-empty Function

for X, Y being set

for 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)))

for X, Y being set

for 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 end;

theorem Th31: :: TOPS_5:31

for f being Function

for A, B, C, D being set

for 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)))

for A, B, C, D being set

for 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 end;

theorem :: TOPS_5:32

for f being Function

for A, B being set

for 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

for A, B being set

for 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 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

:: compare MSUALG_2:1

theorem Th33: :: TOPS_5:33

for I being set

for f, g being ManySortedSet of I holds (product f) /\ (product g) = product (f (/\) g)

for f, g being ManySortedSet of I holds (product f) /\ (product g) = product (f (/\) g)

proof end;

Lm2: for I being 2 -element set

for f being ManySortedSet of I

for i, j being Element of I

for x being object st i <> j holds

f +* (i,x) = (i,j) --> (x,(f . j))

proof end;

theorem Th34: :: TOPS_5:34

for I being 2 -element set

for f being ManySortedSet of I

for i, j being Element of I

for x being object st i <> j holds

( f +* (i,x) = (i,j) --> (x,(f . j)) & f +* (j,x) = (i,j) --> ((f . i),x) )

for f being ManySortedSet of I

for i, j being Element of I

for x being object st i <> j holds

( f +* (i,x) = (i,j) --> (x,(f . j)) & f +* (j,x) = (i,j) --> ((f . i),x) )

proof end;

theorem Th35: :: TOPS_5:35

for f being non-empty Function

for X being set

for i being object st i in dom f holds

( f +* (i,X) is non-empty iff not X is empty )

for X being set

for i being object st i in dom f holds

( f +* (i,X) is non-empty iff not X is empty )

proof end;

theorem Th36: :: TOPS_5:36

for f being non-empty Function

for X being set

for i being object st i in dom f holds

( product (f +* (i,X)) = {} iff X is empty )

for X being set

for i being object st i in dom f holds

( product (f +* (i,X)) = {} iff X is empty )

proof end;

theorem Th37: :: TOPS_5:37

for f being non-empty Function

for X being set

for 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))

for X being set

for 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 end;

theorem Th38: :: TOPS_5:38

for f being Function

for X, Y being set

for i being object st i in dom f & X c= Y holds

product (f +* (i,X)) c= product (f +* (i,Y))

for X, Y being set

for i being object st i in dom f & X c= Y holds

product (f +* (i,X)) c= product (f +* (i,Y))

proof end;

:: compare YELLOW17:2

theorem Th39: :: TOPS_5:39

for f being Function

for X being set

for i being object st i in dom f & X c= f . i holds

product (f +* (i,X)) c= product f

for X being set

for i being object st i in dom f & X c= f . i holds

product (f +* (i,X)) c= product f

proof end;

theorem :: TOPS_5:40

for f being non-empty Function

for X, Y being non empty set

for 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 )

for X, Y being non empty set

for 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 end;

theorem :: TOPS_5:41

for f being non-empty Function

for X being set

for i being object st i in dom f & product (f +* (i,X)) c= product f holds

X c= f . i

for X being set

for i being object st i in dom f & product (f +* (i,X)) c= product f holds

X c= f . i

proof end;

theorem Th42: :: TOPS_5:42

for f being non-empty Function

for X, Y being non empty set

for 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 )

for X, Y being non empty set

for 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 end;

theorem Th43: :: TOPS_5:43

for f being non-empty Function

for X being set

for i being object st i in dom f & X c= f . i holds

(proj (f,i)) .: (product (f +* (i,X))) = X

for X being set

for i being object st i in dom f & X c= f . i holds

(proj (f,i)) .: (product (f +* (i,X))) = X

proof end;

:: END into FUNCT_7 ?

:: into PRALG_1 ?

:: into PRALG_1 ?

registration

let I be non empty set ;

let J be 1-sorted-yielding non-Empty ManySortedSet of I;

coherence

Carrier J is non-empty

end;
let J be 1-sorted-yielding non-Empty ManySortedSet of I;

coherence

Carrier J is non-empty

proof end;

theorem Th45: :: TOPS_5:45

for T, S being TopSpace

for 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 )

for 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 end;

theorem :: TOPS_5:46

for T1, T2, S1, S2 being non empty TopSpace

for f being Function of T1,S1

for g being Function of T2,S2 st f is open & g is open holds

[:f,g:] is open

for f being Function of T1,S1

for g being Function of T2,S2 st f is open & g is open holds

[:f,g:] is open

proof end;

theorem Th47: :: TOPS_5:47

for S, T being non empty TopSpace

for f being Function of S,T st f is bijective & ex K being Basis of S ex L being Basis of T st f .: K = L holds

f is being_homeomorphism

for f being Function of S,T st f is bijective & ex K being Basis of S ex L being Basis of T st f .: K = L holds

f is being_homeomorphism

proof end;

theorem Th48: :: TOPS_5:48

for S, T being non empty TopSpace

for f being Function of S,T st f is bijective & ex K being prebasis of S ex L being prebasis of T st f .: K = L holds

f is being_homeomorphism

for f being Function of S,T st f is bijective & ex K being prebasis of S ex L being prebasis of T st f .: K = L holds

f is being_homeomorphism

proof end;

:: compare TOPGEN_5:71 (the converse)

theorem Th49: :: TOPS_5:49

for S, T being TopSpace st ex K being Basis of S ex L being Basis of T st K = INTERSECTION (L,{([#] S)}) holds

S is SubSpace of T

S is SubSpace of T

proof end;

theorem Th50: :: TOPS_5:50

for S, T being TopSpace st [#] S c= [#] T & ex K being prebasis of S ex L being prebasis of T st K = INTERSECTION (L,{([#] S)}) holds

S is SubSpace of T

S is SubSpace of T

proof end;

theorem Th51: :: TOPS_5:51

for S, T being TopSpace st ex K being prebasis of S ex L being prebasis of T st

( [#] S in K & K = INTERSECTION (L,{([#] S)}) ) holds

S is SubSpace of T

( [#] S in K & K = INTERSECTION (L,{([#] S)}) ) holds

S is SubSpace of T

proof end;

theorem Th52: :: TOPS_5:52

for I being non empty set

for J being non-Empty TopStruct-yielding ManySortedSet of I

for i being Element of I holds rng (proj (J,i)) = the carrier of (J . i)

for J being non-Empty TopStruct-yielding ManySortedSet of I

for i being Element of I holds rng (proj (J,i)) = the carrier of (J . i)

proof end;

definition

let F be Relation;

end;
attr F is TopSpace-yielding means :Def1: :: TOPS_5:def 1

for x being object st x in rng F holds

x is TopSpace;

for x being object st x in rng F holds

x is TopSpace;

:: deftheorem Def1 defines TopSpace-yielding TOPS_5:def 1 :

for F being Relation holds

( F is TopSpace-yielding iff for x being object st x in rng F holds

x is TopSpace );

for F being Relation holds

( F is TopSpace-yielding iff for x being object st x in rng F holds

x is TopSpace );

registration

coherence

for b_{1} being Relation st b_{1} is TopSpace-yielding holds

b_{1} is TopStruct-yielding

end;
for b

b

proof end;

registration
end;

registration
end;

registration

let I be set ;

existence

ex b_{1} being ManySortedSet of I st

( b_{1} is TopSpace-yielding & b_{1} is non-Empty )

end;
existence

ex b

( b

proof end;

definition

let I be non empty set ;

let J be non-Empty TopSpace-yielding ManySortedSet of I;

let i be Element of I;

:: original: .

redefine func J . i -> non empty TopSpace;

coherence

J . i is non empty TopSpace

end;
let J be non-Empty TopSpace-yielding ManySortedSet of I;

let i be Element of I;

:: original: .

redefine func J . i -> non empty TopSpace;

coherence

J . i is non empty TopSpace

proof end;

definition

let f be Function;

ex b_{1} being ManySortedFunction of dom f st

for x being object st x in dom f holds

b_{1} . x = proj (f,x)

for b_{1}, b_{2} being ManySortedFunction of dom f st ( for x being object st x in dom f holds

b_{1} . x = proj (f,x) ) & ( for x being object st x in dom f holds

b_{2} . x = proj (f,x) ) holds

b_{1} = b_{2}

end;
func ProjMap f -> ManySortedFunction of dom f means :Def2: :: TOPS_5:def 2

for x being object st x in dom f holds

it . x = proj (f,x);

existence for x being object st x in dom f holds

it . x = proj (f,x);

ex b

for x being object st x in dom f holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def2 defines ProjMap TOPS_5:def 2 :

for f being Function

for b_{2} being ManySortedFunction of dom f holds

( b_{2} = ProjMap f iff for x being object st x in dom f holds

b_{2} . x = proj (f,x) );

for f being Function

for b

( b

b

registration
end;

definition

let I be non empty set ;

let J be non-Empty TopStruct-yielding ManySortedSet of I;

coherence

ProjMap (Carrier J) is ManySortedSet of I

end;
let J be non-Empty TopStruct-yielding ManySortedSet of I;

coherence

ProjMap (Carrier J) is ManySortedSet of I

proof end;

:: deftheorem defines ProjMap TOPS_5:def 3 :

for I being non empty set

for J being non-Empty TopStruct-yielding ManySortedSet of I holds ProjMap J = ProjMap (Carrier J);

for I being non empty set

for J being non-Empty TopStruct-yielding ManySortedSet of I holds ProjMap J = ProjMap (Carrier J);

registration

let I be non empty set ;

let J be non-Empty TopStruct-yielding ManySortedSet of I;

coherence

( ProjMap J is Function-yielding & not ProjMap J is empty & ProjMap J is non-empty ) ;

end;
let J be non-Empty TopStruct-yielding ManySortedSet of I;

coherence

( ProjMap J is Function-yielding & not ProjMap J is empty & ProjMap J is non-empty ) ;

theorem Th53: :: TOPS_5:53

for I being non empty set

for J being non-Empty TopStruct-yielding ManySortedSet of I

for i being Element of I holds (ProjMap J) . i = proj (J,i)

for J being non-Empty TopStruct-yielding ManySortedSet of I

for i being Element of I holds (ProjMap J) . i = proj (J,i)

proof 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

:: "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 non-Empty TopStruct-yielding ManySortedSet of I;

let f be I -valued one-to-one Function;

((ProjMap J) .:.: (I -indexing (f "))) | (rng f) is ManySortedSet of rng f

end;
let J be non-Empty TopStruct-yielding ManySortedSet of I;

let f be I -valued one-to-one Function;

func product_basis_selector (J,f) -> ManySortedSet of rng f equals :: TOPS_5:def 4

((ProjMap J) .:.: (I -indexing (f "))) | (rng f);

coherence ((ProjMap J) .:.: (I -indexing (f "))) | (rng f);

((ProjMap J) .:.: (I -indexing (f "))) | (rng f) is ManySortedSet of rng f

proof end;

:: deftheorem defines product_basis_selector TOPS_5:def 4 :

for I being non empty set

for J being non-Empty TopStruct-yielding ManySortedSet of I

for f being b_{1} -valued one-to-one Function holds product_basis_selector (J,f) = ((ProjMap J) .:.: (I -indexing (f "))) | (rng f);

for I being non empty set

for J being non-Empty TopStruct-yielding ManySortedSet of I

for f being b

registration

let I be non empty set ;

let J be non-Empty TopStruct-yielding ManySortedSet of I;

let f be empty I -valued one-to-one Function;

coherence

product_basis_selector (J,f) is empty ;

end;
let J be non-Empty TopStruct-yielding ManySortedSet of I;

let f be empty I -valued one-to-one Function;

coherence

product_basis_selector (J,f) is empty ;

theorem Th54: :: TOPS_5:54

for I being non empty set

for J being non-Empty TopStruct-yielding ManySortedSet of I

for f being b_{1} -valued one-to-one Function

for i being Element of I st i in rng f holds

(product_basis_selector (J,f)) . i = (proj (J,i)) .: ((f ") . i)

for J being non-Empty TopStruct-yielding ManySortedSet of I

for f being b

for i being Element of I st i in rng f holds

(product_basis_selector (J,f)) . i = (proj (J,i)) .: ((f ") . i)

proof end;

theorem Th55: :: TOPS_5:55

for I being non empty set

for J being non-Empty TopStruct-yielding ManySortedSet of I

for f being b_{1} -valued one-to-one Function st f " is non-empty & dom f c= bool (product (Carrier J)) holds

product_basis_selector (J,f) is non-empty

for J being non-Empty TopStruct-yielding ManySortedSet of I

for f being b

product_basis_selector (J,f) is non-empty

proof end;

theorem Th56: :: TOPS_5:56

for I being non empty set

for J being non-Empty TopSpace-yielding ManySortedSet of I holds {} in product_prebasis J

for J being non-Empty TopSpace-yielding ManySortedSet of I holds {} in product_prebasis J

proof end;

:: compare YELLOW17:16

theorem Th57: :: TOPS_5:57

for I being non empty set

for J being non-Empty TopStruct-yielding 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) ) )

for J being non-Empty TopStruct-yielding 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 end;

theorem Th58: :: TOPS_5:58

for I being non empty set

for J being non-Empty TopSpace-yielding 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) )

for J being non-Empty TopSpace-yielding 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 end;

theorem Th59: :: TOPS_5:59

for I being non empty set

for J being non-Empty TopStruct-yielding ManySortedSet of I

for f being b_{1} -valued one-to-one 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 ) )

for J being non-Empty TopStruct-yielding ManySortedSet of I

for f being b

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 end;

theorem Th60: :: TOPS_5:60

for I being non empty set

for J being non-Empty TopSpace-yielding ManySortedSet of I

for f being b_{1} -valued one-to-one 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) ) )

for J being non-Empty TopSpace-yielding ManySortedSet of I

for f being b

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 end;

Lm3: for I being non empty set

for J being non-Empty TopSpace-yielding ManySortedSet of I

for P being Subset of (product (Carrier J)) st P in FinMeetCl (product_prebasis J) holds

ex X being Subset-Family of (product (Carrier J)) ex f being b

( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & P = product ((Carrier J) +* (product_basis_selector (J,f))) )

proof end;

:: Theorem of canonical product base characterization

theorem :: TOPS_5:61

for I being non empty set

for J being non-Empty TopSpace-yielding 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)) ex f being b_{1} -valued one-to-one 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;

for J being non-Empty TopSpace-yielding 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)) ex f being b

( 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: :: TOPS_5:62

for I being non empty set

for J being non-Empty TopSpace-yielding ManySortedSet of I

for P being non empty Subset of (product (Carrier J)) st P in FinMeetCl (product_prebasis J) holds

ex X being Subset-Family of (product (Carrier J)) ex f being b_{1} -valued one-to-one 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) ) ) ) )

for J being non-Empty TopSpace-yielding ManySortedSet of I

for P being non empty Subset of (product (Carrier J)) st P in FinMeetCl (product_prebasis J) holds

ex X being Subset-Family of (product (Carrier J)) ex f being b

( 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 end;

theorem Th63: :: TOPS_5:63

for I being non empty set

for J being non-Empty TopSpace-yielding ManySortedSet of I

for P being non empty Subset of (product (Carrier J)) st P in FinMeetCl (product_prebasis J) holds

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) ) )

for J being non-Empty TopSpace-yielding ManySortedSet of I

for P being non empty Subset of (product (Carrier J)) st P in FinMeetCl (product_prebasis J) holds

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 end;

:: characterization of the canonical prebasis of

:: the product topology over one factor

:: the product topology over one factor

theorem Th64: :: TOPS_5:64

for I being 1 -element set

for J being non-Empty TopStruct-yielding ManySortedSet of I

for i being Element of I

for 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) ) )

for J being non-Empty TopStruct-yielding ManySortedSet of I

for i being Element of I

for 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 end;

Lm4: for I being 1 -element set

for J being non-Empty TopSpace-yielding ManySortedSet of I

for i being Element of I

for P being Subset of (product (Carrier J)) st P in FinMeetCl (product_prebasis J) holds

ex V being Subset of (J . i) st

( V is open & P = product ({i} --> V) )

proof end;

Lm5: for I being 1 -element set

for J being non-Empty TopSpace-yielding ManySortedSet of I

for i being Element of I

for 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 end;

Lm6: for I being 1 -element set

for J being non-Empty TopSpace-yielding ManySortedSet of I

for i being Element of I

for 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 end;

Lm7: for I being 1 -element set

for J being non-Empty TopSpace-yielding ManySortedSet of I holds UniCl (FinMeetCl (product_prebasis J)) = product_prebasis J

proof end;

theorem Th65: :: TOPS_5:65

for I being 1 -element set

for J being non-Empty TopSpace-yielding ManySortedSet of I holds the topology of (product J) = product_prebasis J

for J being non-Empty TopSpace-yielding ManySortedSet of I holds the topology of (product J) = product_prebasis J

proof end;

:: characterization of open sets in the product topology over one factor

theorem :: TOPS_5:66

for I being 1 -element set

for J being non-Empty TopSpace-yielding ManySortedSet of I

for i being Element of I

for 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) ) )

for J being non-Empty TopSpace-yielding ManySortedSet of I

for i being Element of I

for 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 end;

registration

let I be non empty set ;

let J be non-Empty TopStruct-yielding ManySortedSet of I;

let i be Element of I;

coherence

( proj (J,i) is continuous & proj (J,i) is onto )

end;
let J be non-Empty TopStruct-yielding ManySortedSet of I;

let i be Element of I;

coherence

( proj (J,i) is continuous & proj (J,i) is onto )

proof end;

registration

let I be non empty set ;

let J be non-Empty TopSpace-yielding ManySortedSet of I;

let i be Element of I;

coherence

proj (J,i) is open

end;
let J be non-Empty TopSpace-yielding ManySortedSet of I;

let i be Element of I;

coherence

proj (J,i) is open

proof end;

theorem Th67: :: TOPS_5:67

for I being 1 -element set

for J being non-Empty TopSpace-yielding ManySortedSet of I

for i being Element of I holds proj (J,i) is being_homeomorphism

for J being non-Empty TopSpace-yielding ManySortedSet of I

for i being Element of I holds proj (J,i) is being_homeomorphism

proof end;

:: the product topology over one factor is homeomorphic to that factor

theorem :: TOPS_5:68

for I being 1 -element set

for J being non-Empty TopSpace-yielding ManySortedSet of I

for i being Element of I holds product J,J . i are_homeomorphic

for J being non-Empty TopSpace-yielding ManySortedSet of I

for i being Element of I holds product J,J . i are_homeomorphic

proof end;

Lm8: for I being 2 -element set

for J being non-Empty TopSpace-yielding ManySortedSet of I

for i, j being Element of I

for P being Subset of (product (Carrier J)) holds

( not i <> j or not P in product_prebasis J or 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 end;

:: characterization of the canonical prebasis of

:: the product topology over two factors

:: the product topology over two factors

theorem Th69: :: TOPS_5:69

for I being 2 -element set

for J being non-Empty TopSpace-yielding ManySortedSet of I

for i, j being Element of I

for 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)) ) ) )

for J being non-Empty TopSpace-yielding ManySortedSet of I

for i, j being Element of I

for 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 end;

Lm9: for I being 2 -element set

for J being non-Empty TopSpace-yielding ManySortedSet of I

for i, j being Element of I

for P being Subset of (product (Carrier J)) st i <> j & P in FinMeetCl (product_prebasis J) holds

ex V being Subset of (J . i) ex W being Subset of (J . j) st

( V is open & W is open & P = product ((i,j) --> (V,W)) )

proof end;

:: characterization of the canonical basis of

:: the product topology over two factors

:: the product topology over two factors

theorem :: TOPS_5:70

for I being 2 -element set

for J being non-Empty TopSpace-yielding ManySortedSet of I

for i, j being Element of I

for 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) ex W being Subset of (J . j) st

( V is open & W is open & P = product ((i,j) --> (V,W)) ) )

for J being non-Empty TopSpace-yielding ManySortedSet of I

for i, j being Element of I

for 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) ex W being Subset of (J . j) st

( V is open & W is open & P = product ((i,j) --> (V,W)) ) )

proof end;

theorem :: TOPS_5:71

:: can be generalized: P only needs to contain the square F.i x F.j

:: at one point p, the Proof works the same

:: at one point p, the Proof works the same

theorem Th72: :: TOPS_5:72

for I being non empty set

for J being non-Empty TopSpace-yielding 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):]

for J being non-Empty TopSpace-yielding 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 end;

theorem Th73: :: TOPS_5:73

for I being non empty set

for J being non-Empty TopSpace-yielding ManySortedSet of I

for i, j being Element of I

for f being Function of (product J),[:(J . i),(J . j):] st i <> j & f = <:(proj (J,i)),(proj (J,j)):> holds

( f is onto & f is open )

for J being non-Empty TopSpace-yielding ManySortedSet of I

for i, j being Element of I

for f being Function of (product J),[:(J . i),(J . j):] st i <> j & f = <:(proj (J,i)),(proj (J,j)):> holds

( f is onto & f is open )

proof end;

theorem Th74: :: TOPS_5:74

for I being 2 -element set

for J being non-Empty TopSpace-yielding ManySortedSet of I

for i, j being Element of I

for 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

for J being non-Empty TopSpace-yielding ManySortedSet of I

for i, j being Element of I

for 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 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)

:: 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 non-Empty TopSpace-yielding ManySortedSet of I

for i, j being Element of I st i <> j holds

product J,[:(J . i),(J . j):] are_homeomorphic

for J being non-Empty TopSpace-yielding ManySortedSet of I

for i, j being Element of I st i <> j holds

product J,[:(J . i),(J . j):] are_homeomorphic

proof end;

registration

let I1, I2 be non empty set ;

let J be non-Empty TopSpace-yielding ManySortedSet of I2;

let f be Function of I1,I2;

coherence

( J * f is TopSpace-yielding & J * f is non-Empty )

end;
let J be non-Empty TopSpace-yielding ManySortedSet of I2;

let f be Function of I1,I2;

coherence

( J * f is TopSpace-yielding & J * f is non-Empty )

proof end;

definition

let I1, I2 be non empty set ;

let J1 be non-Empty TopSpace-yielding ManySortedSet of I1;

let J2 be non-Empty TopSpace-yielding 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 ;

ex b_{1} being Function of (product J1),(product J2) 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)

for i being Element of I1 holds (b_{1} . g) . (p . i) = (F . i) . (g . i) ) )

end;
let J1 be non-Empty TopSpace-yielding ManySortedSet of I1;

let J2 be non-Empty TopSpace-yielding 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: :: 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)

for i being Element of I1 holds (it . g) . (p . i) = (F . i) . (g . i) ) );

existence 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)

for i being Element of I1 holds (it . g) . (p . i) = (F . i) . (g . i) ) );

ex b

( ( 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)

for i being Element of I1 holds (b

proof end;

:: deftheorem Def5 defines ProductHomeo TOPS_5:def 5 :

for I1, I2 being non empty set

for J1 being non-Empty TopSpace-yielding ManySortedSet of I1

for J2 being non-Empty TopSpace-yielding 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

for b_{6} being Function of (product J1),(product J2) holds

( b_{6} is ProductHomeo of J1,J2,p iff 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)

for i being Element of I1 holds (b_{6} . g) . (p . i) = (F . i) . (g . i) ) ) );

for I1, I2 being non empty set

for J1 being non-Empty TopSpace-yielding ManySortedSet of I1

for J2 being non-Empty TopSpace-yielding 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

for b

( b

( ( 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)

for i being Element of I1 holds (b

:: characterization of images of certain subsets under product homeomorphism

theorem Th76: :: TOPS_5:76

for I1, I2 being non empty set

for J1 being non-Empty TopSpace-yielding ManySortedSet of I1

for J2 being non-Empty TopSpace-yielding ManySortedSet of I2

for p being Function of I1,I2

for 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)

for i being Element of I1 holds (H . g) . (p . i) = (F . i) . (g . i) ) holds

for i being Element of I1

for U being Subset of (J1 . i) holds H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U)))

for J1 being non-Empty TopSpace-yielding ManySortedSet of I1

for J2 being non-Empty TopSpace-yielding ManySortedSet of I2

for p being Function of I1,I2

for 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)

for i being Element of I1 holds (H . g) . (p . i) = (F . i) . (g . i) ) holds

for i being Element of I1

for U being Subset of (J1 . i) holds H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U)))

proof end;

theorem Th77: :: TOPS_5:77

for I1, I2 being non empty set

for J1 being non-Empty TopSpace-yielding ManySortedSet of I1

for J2 being non-Empty TopSpace-yielding ManySortedSet of I2

for p being Function of I1,I2

for 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

for J1 being non-Empty TopSpace-yielding ManySortedSet of I1

for J2 being non-Empty TopSpace-yielding ManySortedSet of I2

for p being Function of I1,I2

for 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 end;

theorem Th78: :: TOPS_5:78

for I1, I2 being non empty set

for J1 being non-Empty TopSpace-yielding ManySortedSet of I1

for J2 being non-Empty TopSpace-yielding ManySortedSet of I2

for p being Function of I1,I2

for 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

for J1 being non-Empty TopSpace-yielding ManySortedSet of I1

for J2 being non-Empty TopSpace-yielding ManySortedSet of I2

for p being Function of I1,I2

for 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 end;

:: pairwise homeomorphic factors lead to homeomorphic products

theorem Th79: :: TOPS_5:79

for I1, I2 being non empty set

for J1 being non-Empty TopSpace-yielding ManySortedSet of I1

for J2 being non-Empty TopSpace-yielding 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

for J1 being non-Empty TopSpace-yielding ManySortedSet of I1

for J2 being non-Empty TopSpace-yielding 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 end;

theorem :: TOPS_5:80

for I being non empty set

for J1, J2 being non-Empty TopSpace-yielding 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;

for J1, J2 being non-Empty TopSpace-yielding 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)

:: 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 non-Empty TopSpace-yielding ManySortedSet of I

for p being Permutation of I holds product J, product (J * p) are_homeomorphic

for J being non-Empty TopSpace-yielding ManySortedSet of I

for p being Permutation of I holds product J, product (J * p) are_homeomorphic

proof 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

:: 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 non-Empty TopSpace-yielding 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

for J1, J2 being non-Empty TopSpace-yielding 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 end;

:: compare FUNCT_1:4