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
F1() is non empty set
F2() is Relation-like F1() -defined Function-like V17(F1()) V213() non-Empty TopStruct-yielding set
product F2() is non empty strict TopSpace-like V163() TopStruct
the carrier of (product F2()) is non empty set
I is set
J is Element of F1()
F2() . J is non empty TopStruct
the carrier of (F2() . J) is non empty set
B is Element of the carrier of (F2() . J)
F is Element of F1()
F2() . F is non empty TopStruct
the carrier of (F2() . F) is non empty set
I is Relation-like Function-like set
dom I is set
Carrier F2() is Relation-like non-empty F1() -defined Function-like V17(F1()) set
dom (Carrier F2()) is Element of bool F1()
bool F1() is non empty set
J is set
I . J is set
(Carrier F2()) . J is set
B is Element of F1()
I . B is set
F2() . B is non empty TopStruct
the carrier of (F2() . B) is non empty set
product (Carrier F2()) is non empty functional with_common_domain product-like set
J is Relation-like Function-like Element of the carrier of (product F2())
B is Element of F1()
J . B is Element of the carrier of (F2() . B)
F2() . B is non empty TopStruct
the carrier of (F2() . B) 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 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)) " b1) where b1 is Element of F : verum } is set
union { ((proj (J,B)) " b1) where b1 is Element of F : verum } is set
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))
{ H1(b1) where b1 is Element of Ai : S1[b1] } is set
Gp is set
Ai is Element of Ai
(proj (J,B)) " Ai is Element of bool the carrier of (product J)
c13 is set
f . c13 is set
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