:: YELLOW17 semantic presentation

K101() is non trivial non finite countable denumerable Element of bool K97()

K97() is set

bool K97() is non empty set

K56() is non trivial non finite countable denumerable set

bool K56() is non empty set

bool K101() is non empty set

K98() is set

K99() is set

K100() is set

[:K97(),K97():] is set

bool [:K97(),K97():] is non empty set

K331() is non empty V97() L9()

the carrier of K331() is non empty set

K336() is non empty V97() V119() V120() V121() V123() V173() V174() V175() V176() V177() V178() L9()

K337() is non empty V97() V121() V123() V176() V177() V178() M17(K336())

K338() is non empty V97() V119() V121() V123() V176() V177() V178() V179() M20(K336(),K337())

K340() is non empty V97() V119() V121() V123() L9()

K341() is non empty V97() V119() V121() V123() V179() M17(K340())

K387() is set

{} is set

the empty finite V37() countable set is empty finite V37() countable set

{{}} is finite countable set

K302({{}}) is M14({{}})

[:K302({{}}),{{}}:] is set

bool [:K302({{}}),{{}}:] is non empty set

K49(K302({{}}),{{}}) is set

1 is non empty set

union {} is set

I is Relation-like Function-like set

J is set

I . J is set

bool (I . J) is non empty set

proj (I,J) is Relation-like product I -defined Function-like V17( product I) set

product I is functional with_common_domain product-like set

B is set

{B} is finite countable set

(proj (I,J)) " {B} is set

F is Element of bool (I . J)

(proj (I,J)) " F is set

((proj (I,J)) " {B}) /\ ((proj (I,J)) " F) is set

the Element of ((proj (I,J)) " {B}) /\ ((proj (I,J)) " F) is Element of ((proj (I,J)) " {B}) /\ ((proj (I,J)) " F)

(proj (I,J)) . the Element of ((proj (I,J)) " {B}) /\ ((proj (I,J)) " F) is set

I is Relation-like Function-like set

J is Relation-like Function-like set

product I is functional with_common_domain product-like set

F is set

B is set

I . B is set

J +* (B,F) is Relation-like Function-like set

dom I is set

f is set

(J +* (B,F)) . f is set

I . f is set

dom J is set

dom J is set

dom J is set

J . f is set

dom J is set

dom (J +* (B,F)) is set

I is Relation-like Function-like set

dom I is set

product I is functional with_common_domain product-like set

J is set

proj (I,J) is Relation-like product I -defined Function-like V17( product I) set

rng (proj (I,J)) is set

I . J is set

B is set

dom (proj (I,J)) is with_common_domain Element of bool (product I)

bool (product I) is non empty set

F is set

(proj (I,J)) . F is set

f is Relation-like Function-like set

dom f is set

(proj (I,J)) . f is set

f . J is set

B is set

the Element of product I is Element of product I

f is Relation-like Function-like set

dom f is set

f +* (J,B) is Relation-like Function-like set

dom (proj (I,J)) is with_common_domain Element of bool (product I)

bool (product I) is non empty set

(f +* (J,B)) . J is set

(proj (I,J)) . (f +* (J,B)) is set

I is Relation-like Function-like set

dom I is set

product I is functional with_common_domain product-like set

J is set

proj (I,J) is Relation-like product I -defined Function-like V17( product I) set

I . J is set

(proj (I,J)) " (I . J) is set

dom (proj (I,J)) is with_common_domain Element of bool (product I)

bool (product I) is non empty set

B is set

F is Relation-like Function-like set

dom F is set

F . J is set

(proj (I,J)) . F is set

I is Relation-like Function-like set

dom I is set

J is Relation-like Function-like set

product I is functional with_common_domain product-like set

F is set

B is set

I . B is set

J +* (B,F) is Relation-like Function-like set

proj (I,B) is Relation-like product I -defined Function-like V17( product I) set

{F} is finite countable set

(proj (I,B)) " {F} is set

dom (proj (I,B)) is with_common_domain Element of bool (product I)

bool (product I) is non empty set

dom J is set

(J +* (B,F)) . B is set

(proj (I,B)) . (J +* (B,F)) is set

I is Relation-like Function-like set

J is Relation-like Function-like set

product I is functional with_common_domain product-like set

F is set

I . F is set

bool (I . F) is non empty set

B is set

f is set

J +* (B,f) is Relation-like Function-like set

proj (I,F) is Relation-like product I -defined Function-like V17( product I) set

A is Element of bool (I . F)

(proj (I,F)) " A is set

dom (proj (I,F)) is with_common_domain Element of bool (product I)

bool (product I) is non empty set

(proj (I,F)) . (J +* (B,f)) is set

(J +* (B,f)) . F is set

J . F is set

(proj (I,F)) . J is set

I is Relation-like Function-like set

J is Relation-like Function-like set

product I is functional with_common_domain product-like set

F is set

I . F is set

bool (I . F) is non empty set

f is set

B is set

I . B is set

proj (I,F) is Relation-like product I -defined Function-like V17( product I) set

J +* (B,f) is Relation-like Function-like set

A is Element of bool (I . F)

(proj (I,F)) " A is set

J . B is set

(J +* (B,f)) +* (B,(J . B)) is Relation-like Function-like set

J +* (B,(J . B)) is Relation-like Function-like set

I is Relation-like Function-like set

product I is functional with_common_domain product-like set

dom I is set

B is set

I . B is set

bool (I . B) is non empty set

F is set

J is set

I . J is set

proj (I,J) is Relation-like product I -defined Function-like V17( product I) set

{F} is finite countable set

(proj (I,J)) " {F} is set

proj (I,B) is Relation-like product I -defined Function-like V17( product I) set

f is Element of bool (I . B)

(proj (I,B)) " f is set

the Element of product I is Element of product I

G is Relation-like Function-like set

dom G is set

i is set

Ai is Element of I . B

G +* (B,Ai) is Relation-like Function-like set

(G +* (B,Ai)) . B is set

(G +* (B,Ai)) +* (J,F) is Relation-like Function-like set

dom (proj (I,B)) is with_common_domain Element of bool (product I)

bool (product I) is non empty set

(proj (I,B)) . (G +* (B,Ai)) is set

rng (proj (I,J)) is set

F

F

product F

the carrier of (product F

I is set

J is Element of F

F

the carrier of (F

B is Element of the carrier of (F

F is Element of F

F

the carrier of (F

I is Relation-like Function-like set

dom I is set

Carrier F

dom (Carrier F

bool F

J is set

I . J is set

(Carrier F

B is Element of F

I . B is set

F

the carrier of (F

product (Carrier F

J is Relation-like Function-like Element of the carrier of (product F

B is Element of F

J . B is Element of the carrier of (F

F

the carrier of (F

I is non empty set

J is Relation-like I -defined Function-like V17(I) V213() non-Empty TopStruct-yielding set

product J is non empty strict TopSpace-like V163() TopStruct

the carrier of (product J) is non empty set

B is Element of I

proj (J,B) is Relation-like the carrier of (product J) -defined the carrier of (J . B) -valued Function-like V28( the carrier of (product J), the carrier of (J . B)) Element of bool [: the carrier of (product J), the carrier of (J . B):]

J . B is non empty TopStruct

the carrier of (J . B) is non empty set

[: the carrier of (product J), the carrier of (J . B):] is non empty set

bool [: the carrier of (product J), the carrier of (J . B):] is non empty set

F is Relation-like Function-like Element of the carrier of (product J)

(proj (J,B)) . F is set

F . B is Element of the carrier of (J . B)

Carrier J is Relation-like non-empty I -defined Function-like V17(I) set

product (Carrier J) is non empty functional with_common_domain product-like set

proj ((Carrier J),B) is Relation-like product (Carrier J) -defined Function-like V17( product (Carrier J)) set

dom (proj ((Carrier J),B)) is with_common_domain Element of bool (product (Carrier J))

bool (product (Carrier J)) is non empty set

(proj ((Carrier J),B)) . F is set

I is non empty set

J is Relation-like I -defined Function-like V17(I) V213() non-Empty TopStruct-yielding set

product J is non empty strict TopSpace-like V163() TopStruct

the carrier of (product J) is non empty set

B is Element of I

J . B is non empty TopStruct

the carrier of (J . B) is non empty set

bool the carrier of (J . B) is non empty set

proj (J,B) is Relation-like the carrier of (product J) -defined the carrier of (J . B) -valued Function-like V28( the carrier of (product J), the carrier of (J . B)) Element of bool [: the carrier of (product J), the carrier of (J . B):]

[: the carrier of (product J), the carrier of (J . B):] is non empty set

bool [: the carrier of (product J), the carrier of (J . B):] is non empty set

F is Element of the carrier of (J . B)

{F} is finite countable set

(proj (J,B)) " {F} is Element of bool the carrier of (product J)

bool the carrier of (product J) is non empty set

f is Element of bool the carrier of (J . B)

(proj (J,B)) " f is Element of bool the carrier of (product J)

((proj (J,B)) " {F}) /\ ((proj (J,B)) " f) is Element of bool the carrier of (product J)

Carrier J is Relation-like non-empty I -defined Function-like V17(I) set

proj ((Carrier J),B) is Relation-like product (Carrier J) -defined Function-like V17( product (Carrier J)) set

product (Carrier J) is non empty functional with_common_domain product-like set

(proj ((Carrier J),B)) " {F} is set

((proj ((Carrier J),B)) " {F}) /\ ((proj (J,B)) " f) is Element of bool the carrier of (product J)

(proj ((Carrier J),B)) " f is set

((proj ((Carrier J),B)) " {F}) /\ ((proj ((Carrier J),B)) " f) is set

(Carrier J) . B is set

I is non empty set

J is Relation-like I -defined Function-like V17(I) V213() non-Empty TopStruct-yielding set

product J is non empty strict TopSpace-like V163() TopStruct

the carrier of (product J) is non empty set

[#] (product J) is non empty non proper closed Element of bool the carrier of (product J)

bool the carrier of (product J) is non empty set

B is Element of I

J . B is non empty TopStruct

the carrier of (J . B) is non empty set

proj (J,B) is Relation-like the carrier of (product J) -defined the carrier of (J . B) -valued Function-like V28( the carrier of (product J), the carrier of (J . B)) Element of bool [: the carrier of (product J), the carrier of (J . B):]

[: the carrier of (product J), the carrier of (J . B):] is non empty set

bool [: the carrier of (product J), the carrier of (J . B):] is non empty set

[#] (J . B) is non empty non proper Element of bool the carrier of (J . B)

bool the carrier of (J . B) is non empty set

(proj (J,B)) " ([#] (J . B)) is Element of bool the carrier of (product J)

Carrier J is Relation-like non-empty I -defined Function-like V17(I) set

dom (Carrier J) is Element of bool I

bool I is non empty set

proj ((Carrier J),B) is Relation-like product (Carrier J) -defined Function-like V17( product (Carrier J)) set

product (Carrier J) is non empty functional with_common_domain product-like set

(Carrier J) . B is set

(proj ((Carrier J),B)) " ((Carrier J) . B) is set

(proj ((Carrier J),B)) " ([#] (J . B)) is set

I is non empty set

J is Relation-like I -defined Function-like V17(I) V213() non-Empty TopStruct-yielding set

product J is non empty strict TopSpace-like V163() TopStruct

the carrier of (product J) is non empty set

B is Element of I

J . B is non empty TopStruct

the carrier of (J . B) is non empty set

proj (J,B) is Relation-like the carrier of (product J) -defined the carrier of (J . B) -valued Function-like V28( the carrier of (product J), the carrier of (J . B)) Element of bool [: the carrier of (product J), the carrier of (J . B):]

[: the carrier of (product J), the carrier of (J . B):] is non empty set

bool [: the carrier of (product J), the carrier of (J . B):] is non empty set

F is Element of the carrier of (J . B)

{F} is finite countable set

(proj (J,B)) " {F} is Element of bool the carrier of (product J)

bool the carrier of (product J) is non empty set

f is Relation-like Function-like Element of the carrier of (product J)

f +* (B,F) is Relation-like Function-like set

Carrier J is Relation-like non-empty I -defined Function-like V17(I) set

(Carrier J) . B is set

product (Carrier J) is non empty functional with_common_domain product-like set

dom (Carrier J) is Element of bool I

bool I is non empty set

proj ((Carrier J),B) is Relation-like product (Carrier J) -defined Function-like V17( product (Carrier J)) set

(proj ((Carrier J),B)) " {F} is set

I is non empty set

J is Relation-like I -defined Function-like V17(I) V213() non-Empty TopStruct-yielding set

product J is non empty strict TopSpace-like V163() TopStruct

the carrier of (product J) is non empty set

B is Element of I

J . B is non empty TopStruct

the carrier of (J . B) is non empty set

F is Element of I

J . F is non empty TopStruct

the carrier of (J . F) is non empty set

bool the carrier of (J . F) is non empty set

[#] (J . F) is non empty non proper Element of bool the carrier of (J . F)

proj (J,B) is Relation-like the carrier of (product J) -defined the carrier of (J . B) -valued Function-like V28( the carrier of (product J), the carrier of (J . B)) Element of bool [: the carrier of (product J), the carrier of (J . B):]

[: the carrier of (product J), the carrier of (J . B):] is non empty set

bool [: the carrier of (product J), the carrier of (J . B):] is non empty set

proj (J,F) is Relation-like the carrier of (product J) -defined the carrier of (J . F) -valued Function-like V28( the carrier of (product J), the carrier of (J . F)) Element of bool [: the carrier of (product J), the carrier of (J . F):]

[: the carrier of (product J), the carrier of (J . F):] is non empty set

bool [: the carrier of (product J), the carrier of (J . F):] is non empty set

f is Element of the carrier of (J . B)

{f} is finite countable set

(proj (J,B)) " {f} is Element of bool the carrier of (product J)

bool the carrier of (product J) is non empty set

A is Element of bool the carrier of (J . F)

(proj (J,F)) " A is Element of bool the carrier of (product J)

Carrier J is Relation-like non-empty I -defined Function-like V17(I) set

(Carrier J) . F is set

bool ((Carrier J) . F) is non empty set

dom (Carrier J) is Element of bool I

bool I is non empty set

G is Element of bool ((Carrier J) . F)

(Carrier J) . B is set

product (Carrier J) is non empty functional with_common_domain product-like set

proj ((Carrier J),B) is Relation-like product (Carrier J) -defined Function-like V17( product (Carrier J)) set

(proj ((Carrier J),B)) " {f} is set

proj ((Carrier J),F) is Relation-like product (Carrier J) -defined Function-like V17( product (Carrier J)) set

(proj ((Carrier J),F)) " G is set

(proj ((Carrier J),F)) " A is set

I is non empty set

J is Relation-like I -defined Function-like V17(I) V213() non-Empty TopStruct-yielding set

product J is non empty strict TopSpace-like V163() TopStruct

the carrier of (product J) is non empty set

B is Element of I

J . B is non empty TopStruct

the carrier of (J . B) is non empty set

F is Element of I

J . F is non empty TopStruct

the carrier of (J . F) is non empty set

bool the carrier of (J . F) is non empty set

proj (J,F) is Relation-like the carrier of (product J) -defined the carrier of (J . F) -valued Function-like V28( the carrier of (product J), the carrier of (J . F)) Element of bool [: the carrier of (product J), the carrier of (J . F):]

[: the carrier of (product J), the carrier of (J . F):] is non empty set

bool [: the carrier of (product J), the carrier of (J . F):] is non empty set

f is Element of the carrier of (J . B)

A is Element of bool the carrier of (J . F)

(proj (J,F)) " A is Element of bool the carrier of (product J)

bool the carrier of (product J) is non empty set

G is Relation-like Function-like Element of the carrier of (product J)

G +* (B,f) is Relation-like Function-like set

Carrier J is Relation-like non-empty I -defined Function-like V17(I) set

(Carrier J) . F is set

bool ((Carrier J) . F) is non empty set

(Carrier J) . B is set

product (Carrier J) is non empty functional with_common_domain product-like set

proj ((Carrier J),F) is Relation-like product (Carrier J) -defined Function-like V17( product (Carrier J)) set

i is Element of bool ((Carrier J) . F)

(proj ((Carrier J),F)) " i is set

I is non empty TopStruct

the carrier of I is non empty set

bool the carrier of I is non empty set

bool (bool the carrier of I) is non empty set

[#] I is non empty non proper Element of bool the carrier of I

J is Element of bool (bool the carrier of I)

union J is set

B is Element of bool (bool the carrier of I)

union B is set

J is Element of bool (bool the carrier of I)

union J is set

B is Element of bool (bool the carrier of I)

union B is set

I is non empty TopSpace-like TopStruct

the carrier of I is non empty set

bool the carrier of I is non empty set

bool (bool the carrier of I) is non empty set

[#] I is non empty non proper closed Element of bool the carrier of I

J is open quasi_prebasis Element of bool (bool the carrier of I)

bool J is non empty set

the topology of I is non empty Element of bool (bool the carrier of I)

InclPoset the topology of I is non empty V191() V193() V194() V195() L14()

the carrier of (InclPoset the topology of I) is non empty set

F is Element of the carrier of (InclPoset the topology of I)

f is Element of bool J

union f is set

bool f is non empty set

I is non empty set

J is Relation-like I -defined Function-like V17(I) V213() non-Empty TopStruct-yielding set

product_prebasis J is Element of bool (bool (product (Carrier J)))

Carrier J is Relation-like non-empty I -defined Function-like V17(I) set

product (Carrier J) is non empty functional with_common_domain product-like set

bool (product (Carrier J)) is non empty set

bool (bool (product (Carrier J))) is non empty set

product J is non empty strict TopSpace-like V163() TopStruct

the carrier of (product J) is non empty set

B is set

f is TopStruct

the carrier of f is set

bool the carrier of f is non empty set

F is set

A is Element of bool the carrier of f

J . F is set

(Carrier J) +* (F,A) is Relation-like Function-like set

product ((Carrier J) +* (F,A)) is functional with_common_domain product-like set

G is Element of I

J . G is non empty TopStruct

the carrier of (J . G) is non empty set

bool the carrier of (J . G) is non empty set

proj (J,G) is Relation-like the carrier of (product J) -defined the carrier of (J . G) -valued Function-like V28( the carrier of (product J), the carrier of (J . G)) Element of bool [: the carrier of (product J), the carrier of (J . G):]

[: the carrier of (product J), the carrier of (J . G):] is non empty set

bool [: the carrier of (product J), the carrier of (J . G):] is non empty set

i is Element of bool the carrier of (J . G)

(proj (J,G)) " i is Element of bool the carrier of (product J)

bool the carrier of (product J) is non empty set

I is non empty set

J is Relation-like I -defined Function-like V17(I) V213() non-Empty TopStruct-yielding set

product_prebasis J is Element of bool (bool (product (Carrier J)))

Carrier J is Relation-like non-empty I -defined Function-like V17(I) set

product (Carrier J) is non empty functional with_common_domain product-like set

bool (product (Carrier J)) is non empty set

bool (bool (product (Carrier J))) is non empty set

product J is non empty strict TopSpace-like V163() TopStruct

the carrier of (product J) is non empty set

[#] (product J) is non empty non proper closed Element of bool the carrier of (product J)

bool the carrier of (product J) is non empty set

B is Element of I

J . B is non empty TopStruct

the carrier of (J . B) is non empty set

proj (J,B) is Relation-like the carrier of (product J) -defined the carrier of (J . B) -valued Function-like V28( the carrier of (product J), the carrier of (J . B)) Element of bool [: the carrier of (product J), the carrier of (J . B):]

[: the carrier of (product J), the carrier of (J . B):] is non empty set

bool [: the carrier of (product J), the carrier of (J . B):] is non empty set

bool the carrier of (J . B) is non empty set

[#] (J . B) is non empty non proper Element of bool the carrier of (J . B)

F is Element of the carrier of (J . B)

{F} is finite countable set

(proj (J,B)) " {F} is Element of bool the carrier of (product J)

f is set

A is Element of I

J . A is non empty TopStruct

the carrier of (J . A) is non empty set

bool the carrier of (J . A) is non empty set

G is Element of bool the carrier of (J . A)

proj (J,A) is Relation-like the carrier of (product J) -defined the carrier of (J . A) -valued Function-like V28( the carrier of (product J), the carrier of (J . A)) Element of bool [: the carrier of (product J), the carrier of (J . A):]

[: the carrier of (product J), the carrier of (J . A):] is non empty set

bool [: the carrier of (product J), the carrier of (J . A):] is non empty set

(proj (J,A)) " G is Element of bool the carrier of (product J)

[#] (J . A) is non empty non proper Element of bool the carrier of (J . A)

i is Element of bool the carrier of (J . B)

(proj (J,B)) " i is Element of bool the carrier of (product J)

I is non empty set

J is Relation-like I -defined Function-like V17(I) V213() non-Empty TopStruct-yielding set

product J is non empty strict TopSpace-like V163() TopStruct

[#] (product J) is non empty non proper closed Element of bool the carrier of (product J)

the carrier of (product J) is non empty set

bool the carrier of (product J) is non empty set

B is Element of I

J . B is non empty TopStruct

the carrier of (J . B) is non empty set

bool the carrier of (J . B) is non empty set

bool (bool the carrier of (J . B)) is non empty set

[#] (J . B) is non empty non proper Element of bool the carrier of (J . B)

proj (J,B) is Relation-like the carrier of (product J) -defined the carrier of (J . B) -valued Function-like V28( the carrier of (product J), the carrier of (J . B)) Element of bool [: the carrier of (product J), the carrier of (J . B):]

[: the carrier of (product J), the carrier of (J . B):] is non empty set

bool [: the carrier of (product J), the carrier of (J . B):] is non empty set

F is non empty Element of bool (bool the carrier of (J . B))

union F is set

{ ((proj (J,B)) " b

union { ((proj (J,B)) " b

f is set

A is Relation-like Function-like Element of the carrier of (product J)

A . B is Element of the carrier of (J . B)

G is set

Carrier J is Relation-like non-empty I -defined Function-like V17(I) set

product (Carrier J) is non empty functional with_common_domain product-like set

proj ((Carrier J),B) is Relation-like product (Carrier J) -defined Function-like V17( product (Carrier J)) set

dom (proj ((Carrier J),B)) is with_common_domain Element of bool (product (Carrier J))

bool (product (Carrier J)) is non empty set

dom (proj (J,B)) is Element of bool the carrier of (product J)

(proj (J,B)) . A is set

i is Element of F

(proj (J,B)) " i is Element of bool the carrier of (product J)

I is non empty set

J is Relation-like I -defined Function-like V17(I) V213() non-Empty TopStruct-yielding set

product_prebasis J is Element of bool (bool (product (Carrier J)))

Carrier J is Relation-like non-empty I -defined Function-like V17(I) set

product (Carrier J) is non empty functional with_common_domain product-like set

bool (product (Carrier J)) is non empty set

bool (bool (product (Carrier J))) is non empty set

bool (product_prebasis J) is non empty set

product J is non empty strict TopSpace-like V163() TopStruct

the carrier of (product J) is non empty set

[#] (product J) is non empty non proper closed Element of bool the carrier of (product J)

bool the carrier of (product J) is non empty set

B is Element of I

J . B is non empty TopStruct

the carrier of (J . B) is non empty set

proj (J,B) is Relation-like the carrier of (product J) -defined the carrier of (J . B) -valued Function-like V28( the carrier of (product J), the carrier of (J . B)) Element of bool [: the carrier of (product J), the carrier of (J . B):]

[: the carrier of (product J), the carrier of (J . B):] is non empty set

bool [: the carrier of (product J), the carrier of (J . B):] is non empty set

F is Element of the carrier of (J . B)

{F} is finite countable set

(proj (J,B)) " {F} is Element of bool the carrier of (product J)

f is Element of bool (product_prebasis J)

union f is set

A is set

G is Relation-like Function-like Element of the carrier of (product J)

G +* (B,F) is Relation-like Function-like set

Ai is set

Gp is Element of I

J . Gp is non empty TopStruct

the carrier of (J . Gp) is non empty set

bool the carrier of (J . Gp) is non empty set

Gp is Element of bool the carrier of (J . Gp)

proj (J,Gp) is Relation-like the carrier of (product J) -defined the carrier of (J . Gp) -valued Function-like V28( the carrier of (product J), the carrier of (J . Gp)) Element of bool [: the carrier of (product J), the carrier of (J . Gp):]

[: the carrier of (product J), the carrier of (J . Gp):] is non empty set

bool [: the carrier of (product J), the carrier of (J . Gp):] is non empty set

(proj (J,Gp)) " Gp is Element of bool the carrier of (product J)

[#] (J . Gp) is non empty non proper Element of bool the carrier of (J . Gp)

bool the carrier of (J . B) is non empty set

Ai is Element of bool the carrier of (J . B)

(proj (J,B)) " Ai is Element of bool the carrier of (product J)

((proj (J,B)) " {F}) /\ ((proj (J,B)) " Ai) is Element of bool the carrier of (product J)

I is non empty set

J is Relation-like I -defined Function-like V17(I) V213() non-Empty TopStruct-yielding set

product_prebasis J is Element of bool (bool (product (Carrier J)))

Carrier J is Relation-like non-empty I -defined Function-like V17(I) set

product (Carrier J) is non empty functional with_common_domain product-like set

bool (product (Carrier J)) is non empty set

bool (bool (product (Carrier J))) is non empty set

bool (product_prebasis J) is non empty set

product J is non empty strict TopSpace-like V163() TopStruct

[#] (product J) is non empty non proper closed Element of bool the carrier of (product J)

the carrier of (product J) is non empty set

bool the carrier of (product J) is non empty set

B is Element of I

J . B is non empty TopStruct

the carrier of (J . B) is non empty set

proj (J,B) is Relation-like the carrier of (product J) -defined the carrier of (J . B) -valued Function-like V28( the carrier of (product J), the carrier of (J . B)) Element of bool [: the carrier of (product J), the carrier of (J . B):]

[: the carrier of (product J), the carrier of (J . B):] is non empty set

bool [: the carrier of (product J), the carrier of (J . B):] is non empty set

F is Element of bool (product_prebasis J)

bool F is non empty set

f is Element of the carrier of (J . B)

{f} is finite countable set

(proj (J,B)) " {f} is Element of bool the carrier of (product J)

A is finite countable Element of bool F

union A is set

G is Element of bool (product_prebasis J)

union G is set

I is non empty set

J is Relation-like I -defined Function-like V17(I) V213() non-Empty TopStruct-yielding set

product_prebasis J is Element of bool (bool (product (Carrier J)))

Carrier J is Relation-like non-empty I -defined Function-like V17(I) set

product (Carrier J) is non empty functional with_common_domain product-like set

bool (product (Carrier J)) is non empty set

bool (bool (product (Carrier J))) is non empty set

bool (product_prebasis J) is non empty set

product J is non empty strict TopSpace-like V163() TopStruct

[#] (product J) is non empty non proper closed Element of bool the carrier of (product J)

the carrier of (product J) is non empty set

bool the carrier of (product J) is non empty set

B is Element of I

J . B is non empty TopStruct

the carrier of (J . B) is non empty set

proj (J,B) is Relation-like the carrier of (product J) -defined the carrier of (J . B) -valued Function-like V28( the carrier of (product J), the carrier of (J . B)) Element of bool [: the carrier of (product J), the carrier of (J . B):]

[: the carrier of (product J), the carrier of (J . B):] is non empty set

bool [: the carrier of (product J), the carrier of (J . B):] is non empty set

bool the carrier of (J . B) is non empty set

[#] (J . B) is non empty non proper Element of bool the carrier of (J . B)

F is Element of bool (product_prebasis J)

bool F is non empty set

f is Element of the carrier of (J . B)

{f} is finite countable set

(proj (J,B)) " {f} is Element of bool the carrier of (product J)

A is finite countable Element of bool F

union A is set

G is set

{G} is finite countable set

i is finite countable Element of bool F

union i is set

i is Element of bool the carrier of (J . B)

(proj (J,B)) " i is Element of bool the carrier of (product J)

I is non empty set

J is Relation-like I -defined Function-like V17(I) V213() non-Empty TopStruct-yielding set

product_prebasis J is Element of bool (bool (product (Carrier J)))

Carrier J is Relation-like non-empty I -defined Function-like V17(I) set

product (Carrier J) is non empty functional with_common_domain product-like set

bool (product (Carrier J)) is non empty set

bool (bool (product (Carrier J))) is non empty set

bool (product_prebasis J) is non empty set

product J is non empty strict TopSpace-like V163() TopStruct

[#] (product J) is non empty non proper closed Element of bool the carrier of (product J)

the carrier of (product J) is non empty set

bool the carrier of (product J) is non empty set

B is Element of I

J . B is non empty TopStruct

the carrier of (J . B) is non empty set

proj (J,B) is Relation-like the carrier of (product J) -defined the carrier of (J . B) -valued Function-like V28( the carrier of (product J), the carrier of (J . B)) Element of bool [: the carrier of (product J), the carrier of (J . B):]

[: the carrier of (product J), the carrier of (J . B):] is non empty set

bool [: the carrier of (product J), the carrier of (J . B):] is non empty set

F is Element of bool (product_prebasis J)

bool F is non empty set

bool the carrier of (J . B) is non empty set

f is set

A is Element of the carrier of (J . B)

{A} is finite countable set

(proj (J,B)) " {A} is Element of bool the carrier of (product J)

G is finite countable Element of bool F

union G is set

[#] (J . B) is non empty non proper Element of bool the carrier of (J . B)

i is Element of bool the carrier of (J . B)

(proj (J,B)) " i is Element of bool the carrier of (product J)

Ai is Element of bool the carrier of (J . B)

f is Relation-like Function-like set

dom f is set

rng f is set

bool (bool the carrier of (J . B)) is non empty set

A is Element of bool (bool the carrier of (J . B))

[#] (J . B) is non empty non proper Element of bool the carrier of (J . B)

G is Element of bool (bool the carrier of (J . B))

union G is set

i is set

f . i is set

i is Element of bool the carrier of (J . B)

Ai is set

f . Ai is set

i is Element of bool (bool the carrier of (J . B))

union i is set

Ai is non empty finite countable Element of bool (bool the carrier of (J . B))

{ H

Gp is set

Ai is Element of Ai

(proj (J,B)) " Ai is Element of bool the carrier of (product J)

c

f . c

Gp is finite countable Element of bool F

union Gp is set

I is non empty set

J is Relation-like I -defined Function-like V17(I) V213() non-Empty TopStruct-yielding set

product J is non empty strict TopSpace-like V163() TopStruct

the carrier of (product J) is non empty set

bool the carrier of (product J) is non empty set

bool (bool the carrier of (product J)) is non empty set

product_prebasis J is Element of bool (bool (product (Carrier J)))

Carrier J is Relation-like non-empty I -defined Function-like V17(I) set

product (Carrier J) is non empty functional with_common_domain product-like set

bool (product (Carrier J)) is non empty set

bool (bool (product (Carrier J))) is non empty set

B is open quasi_prebasis Element of bool (bool the carrier of (product J))

bool B is non empty set

[#] (product J) is non empty non proper closed Element of bool the carrier of (product J)

F is Element of bool B

union F is set

bool F is non empty set

f is Element of I

J . f is non empty TopStruct

the carrier of (J . f) is non empty set

proj (J,f) is Relation-like the carrier of (product J) -defined the carrier of (J . f) -valued Function-like V28( the carrier of (product J), the carrier of (J . f)) Element of bool [: the carrier of (product J), the carrier of (J . f):]

[: the carrier of (product J), the carrier of (J . f):] is non empty set

bool [: the carrier of (product J), the carrier of (J . f):] is non empty set

f is Relation-like Function-like Element of the carrier of (product J)

A is set

{A} is finite countable set

i is Element of I

J . i is non empty TopStruct

the carrier of (J . i) is non empty set

bool the carrier of (J . i) is non empty set

Ai is Element of bool the carrier of (J . i)

proj (J,i) is Relation-like the carrier of (product J) -defined the carrier of (J . i) -valued Function-like V28( the carrier of (product J), the carrier of (J . i)) Element of bool [: the carrier of (product J), the carrier of (J . i):]

[: the carrier of (product J), the carrier of (J . i):] is non empty set

bool [: the carrier of (product J), the carrier of (J . i):] is non empty set

(proj (J,i)) " Ai is Element of bool the carrier of (product J)

(proj (J,i)) . f is set

f . i is Element of the carrier of (J . i)

{(f . i)} is finite countable set

(proj (J,i)) " {(f . i)} is Element of bool the carrier of (product J)

G is finite countable Element of bool F

union G is set