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

K302() is M14()
is set
bool is non empty set
K49(K302(),) is set
1 is non empty set

J is set
I . J is set
bool (I . J) is non empty set

B is 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

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

dom I is set

J is 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 ()
bool () is non empty set
F is set
(proj (I,J)) . F is 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

dom f is set
f +* (J,B) is Relation-like Function-like set
dom (proj (I,J)) is with_common_domain Element of bool ()
bool () is non empty set
(f +* (J,B)) . J is set
(proj (I,J)) . (f +* (J,B)) is set

dom I is set

J is set

I . J is set
(proj (I,J)) " (I . J) is set
dom (proj (I,J)) is with_common_domain Element of bool ()
bool () is non empty set
B is set

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

dom I is set

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

(proj (I,B)) " {F} is set
dom (proj (I,B)) is with_common_domain Element of bool ()
bool () is non empty set
dom J is set
(J +* (B,F)) . B is set
(proj (I,B)) . (J +* (B,F)) is 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

A is Element of bool (I . F)
(proj (I,F)) " A is set
dom (proj (I,F)) is with_common_domain Element of bool ()
bool () 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

F is set
I . F is set
bool (I . F) is non empty set
f is set
B is set
I . B is 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

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)) " {F} is set

f is Element of bool (I . B)
(proj (I,B)) " f is set
the Element of product I is Element of product I

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

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

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

product J is non empty strict TopSpace-like V163() TopStruct
the carrier of () is non empty set
B is Element of I
proj (J,B) is Relation-like the carrier of () -defined the carrier of (J . B) -valued Function-like V28( the carrier of (), the carrier of (J . B)) Element of bool [: the carrier of (), the carrier of (J . B):]
J . B is non empty TopStruct
the carrier of (J . B) is non empty set
[: the carrier of (), the carrier of (J . B):] is non empty set
bool [: the carrier of (), the carrier of (J . B):] is non empty set
F is Relation-like Function-like Element of the carrier of ()
(proj (J,B)) . F is set
F . B is Element of the carrier of (J . B)

proj ((),B) is Relation-like product () -defined Function-like V17( product ()) set
dom (proj ((),B)) is with_common_domain Element of bool (product ())
bool (product ()) is non empty set
(proj ((),B)) . F is set
I is non empty set

product J is non empty strict TopSpace-like V163() TopStruct
the carrier of () 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 () -defined the carrier of (J . B) -valued Function-like V28( the carrier of (), the carrier of (J . B)) Element of bool [: the carrier of (), the carrier of (J . B):]
[: the carrier of (), the carrier of (J . B):] is non empty set
bool [: the carrier of (), the carrier of (J . B):] is non empty set
F is Element of the carrier of (J . B)

(proj (J,B)) " {F} is Element of bool the carrier of ()
bool the carrier of () 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 ()
((proj (J,B)) " {F}) /\ ((proj (J,B)) " f) is Element of bool the carrier of ()

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

(proj ((),B)) " {F} is set
((proj ((),B)) " {F}) /\ ((proj (J,B)) " f) is Element of bool the carrier of ()
(proj ((),B)) " f is set
((proj ((),B)) " {F}) /\ ((proj ((),B)) " f) is set
() . B is set
I is non empty set

product J is non empty strict TopSpace-like V163() TopStruct
the carrier of () is non empty set
[#] () is non empty non proper closed Element of bool the carrier of ()
bool the carrier of () 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 () -defined the carrier of (J . B) -valued Function-like V28( the carrier of (), the carrier of (J . B)) Element of bool [: the carrier of (), the carrier of (J . B):]
[: the carrier of (), the carrier of (J . B):] is non empty set
bool [: the carrier of (), 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 ()

dom () is Element of bool I
bool I is non empty set
proj ((),B) is Relation-like product () -defined Function-like V17( product ()) set

() . B is set
(proj ((),B)) " (() . B) is set
(proj ((),B)) " ([#] (J . B)) is set
I is non empty set

product J is non empty strict TopSpace-like V163() TopStruct
the carrier of () 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 () -defined the carrier of (J . B) -valued Function-like V28( the carrier of (), the carrier of (J . B)) Element of bool [: the carrier of (), the carrier of (J . B):]
[: the carrier of (), the carrier of (J . B):] is non empty set
bool [: the carrier of (), the carrier of (J . B):] is non empty set
F is Element of the carrier of (J . B)

(proj (J,B)) " {F} is Element of bool the carrier of ()
bool the carrier of () is non empty set
f is Relation-like Function-like Element of the carrier of ()
f +* (B,F) is Relation-like Function-like set

() . B is set

dom () is Element of bool I
bool I is non empty set
proj ((),B) is Relation-like product () -defined Function-like V17( product ()) set
(proj ((),B)) " {F} is set
I is non empty set

product J is non empty strict TopSpace-like V163() TopStruct
the carrier of () 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 () -defined the carrier of (J . B) -valued Function-like V28( the carrier of (), the carrier of (J . B)) Element of bool [: the carrier of (), the carrier of (J . B):]
[: the carrier of (), the carrier of (J . B):] is non empty set
bool [: the carrier of (), the carrier of (J . B):] is non empty set
proj (J,F) is Relation-like the carrier of () -defined the carrier of (J . F) -valued Function-like V28( the carrier of (), the carrier of (J . F)) Element of bool [: the carrier of (), the carrier of (J . F):]
[: the carrier of (), the carrier of (J . F):] is non empty set
bool [: the carrier of (), the carrier of (J . F):] is non empty set
f is Element of the carrier of (J . B)

(proj (J,B)) " {f} is Element of bool the carrier of ()
bool the carrier of () 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 ()

() . F is set
bool (() . F) is non empty set
dom () is Element of bool I
bool I is non empty set
G is Element of bool (() . F)
() . B is set

proj ((),B) is Relation-like product () -defined Function-like V17( product ()) set
(proj ((),B)) " {f} is set
proj ((),F) is Relation-like product () -defined Function-like V17( product ()) set
(proj ((),F)) " G is set
(proj ((),F)) " A is set
I is non empty set

product J is non empty strict TopSpace-like V163() TopStruct
the carrier of () 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 () -defined the carrier of (J . F) -valued Function-like V28( the carrier of (), the carrier of (J . F)) Element of bool [: the carrier of (), the carrier of (J . F):]
[: the carrier of (), the carrier of (J . F):] is non empty set
bool [: the carrier of (), 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 ()
bool the carrier of () is non empty set
G is Relation-like Function-like Element of the carrier of ()
G +* (B,f) is Relation-like Function-like set

() . F is set
bool (() . F) is non empty set
() . B is set

proj ((),F) is Relation-like product () -defined Function-like V17( product ()) set
i is Element of bool (() . F)
(proj ((),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

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

bool (product ()) is non empty set
bool (bool (product ())) is non empty set
product J is non empty strict TopSpace-like V163() TopStruct
the carrier of () 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
() +* (F,A) is Relation-like Function-like set
product (() +* (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 () -defined the carrier of (J . G) -valued Function-like V28( the carrier of (), the carrier of (J . G)) Element of bool [: the carrier of (), the carrier of (J . G):]
[: the carrier of (), the carrier of (J . G):] is non empty set
bool [: the carrier of (), 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 ()
bool the carrier of () is non empty set
I is non empty set

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

bool (product ()) is non empty set
bool (bool (product ())) is non empty set
product J is non empty strict TopSpace-like V163() TopStruct
the carrier of () is non empty set
[#] () is non empty non proper closed Element of bool the carrier of ()
bool the carrier of () 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 () -defined the carrier of (J . B) -valued Function-like V28( the carrier of (), the carrier of (J . B)) Element of bool [: the carrier of (), the carrier of (J . B):]
[: the carrier of (), the carrier of (J . B):] is non empty set
bool [: the carrier of (), 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)

(proj (J,B)) " {F} is Element of bool the carrier of ()
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 () -defined the carrier of (J . A) -valued Function-like V28( the carrier of (), the carrier of (J . A)) Element of bool [: the carrier of (), the carrier of (J . A):]
[: the carrier of (), the carrier of (J . A):] is non empty set
bool [: the carrier of (), the carrier of (J . A):] is non empty set
(proj (J,A)) " G is Element of bool the carrier of ()
[#] (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 ()
I is non empty set

product J is non empty strict TopSpace-like V163() TopStruct
[#] () is non empty non proper closed Element of bool the carrier of ()
the carrier of () is non empty set
bool the carrier of () 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 () -defined the carrier of (J . B) -valued Function-like V28( the carrier of (), the carrier of (J . B)) Element of bool [: the carrier of (), the carrier of (J . B):]
[: the carrier of (), the carrier of (J . B):] is non empty set
bool [: the carrier of (), 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 ()
A . B is Element of the carrier of (J . B)
G is set

proj ((),B) is Relation-like product () -defined Function-like V17( product ()) set
dom (proj ((),B)) is with_common_domain Element of bool (product ())
bool (product ()) is non empty set
dom (proj (J,B)) is Element of bool the carrier of ()
(proj (J,B)) . A is set
i is Element of F
(proj (J,B)) " i is Element of bool the carrier of ()
I is non empty set

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

bool (product ()) is non empty set
bool (bool (product ())) is non empty set
bool () is non empty set
product J is non empty strict TopSpace-like V163() TopStruct
the carrier of () is non empty set
[#] () is non empty non proper closed Element of bool the carrier of ()
bool the carrier of () 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 () -defined the carrier of (J . B) -valued Function-like V28( the carrier of (), the carrier of (J . B)) Element of bool [: the carrier of (), the carrier of (J . B):]
[: the carrier of (), the carrier of (J . B):] is non empty set
bool [: the carrier of (), the carrier of (J . B):] is non empty set
F is Element of the carrier of (J . B)

(proj (J,B)) " {F} is Element of bool the carrier of ()
f is Element of bool ()
union f is set
A is set
G is Relation-like Function-like Element of the carrier of ()
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 () -defined the carrier of (J . Gp) -valued Function-like V28( the carrier of (), the carrier of (J . Gp)) Element of bool [: the carrier of (), the carrier of (J . Gp):]
[: the carrier of (), the carrier of (J . Gp):] is non empty set
bool [: the carrier of (), the carrier of (J . Gp):] is non empty set
(proj (J,Gp)) " Gp is Element of bool the carrier of ()
[#] (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 ()
((proj (J,B)) " {F}) /\ ((proj (J,B)) " Ai) is Element of bool the carrier of ()
I is non empty set

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

bool (product ()) is non empty set
bool (bool (product ())) is non empty set
bool () is non empty set
product J is non empty strict TopSpace-like V163() TopStruct
[#] () is non empty non proper closed Element of bool the carrier of ()
the carrier of () is non empty set
bool the carrier of () 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 () -defined the carrier of (J . B) -valued Function-like V28( the carrier of (), the carrier of (J . B)) Element of bool [: the carrier of (), the carrier of (J . B):]
[: the carrier of (), the carrier of (J . B):] is non empty set
bool [: the carrier of (), the carrier of (J . B):] is non empty set
F is Element of bool ()
bool F is non empty set
f is Element of the carrier of (J . B)

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

union A is set
G is Element of bool ()
union G is set
I is non empty set

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

bool (product ()) is non empty set
bool (bool (product ())) is non empty set
bool () is non empty set
product J is non empty strict TopSpace-like V163() TopStruct
[#] () is non empty non proper closed Element of bool the carrier of ()
the carrier of () is non empty set
bool the carrier of () 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 () -defined the carrier of (J . B) -valued Function-like V28( the carrier of (), the carrier of (J . B)) Element of bool [: the carrier of (), the carrier of (J . B):]
[: the carrier of (), the carrier of (J . B):] is non empty set
bool [: the carrier of (), 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 ()
bool F is non empty set
f is Element of the carrier of (J . B)

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

union A is set
G is set

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 ()
I is non empty set

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

bool (product ()) is non empty set
bool (bool (product ())) is non empty set
bool () is non empty set
product J is non empty strict TopSpace-like V163() TopStruct
[#] () is non empty non proper closed Element of bool the carrier of ()
the carrier of () is non empty set
bool the carrier of () 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 () -defined the carrier of (J . B) -valued Function-like V28( the carrier of (), the carrier of (J . B)) Element of bool [: the carrier of (), the carrier of (J . B):]
[: the carrier of (), the carrier of (J . B):] is non empty set
bool [: the carrier of (), the carrier of (J . B):] is non empty set
F is Element of bool ()
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)

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

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 ()
Ai is Element of bool the carrier of (J . B)

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 ()
c13 is set
f . c13 is set
Gp is finite countable Element of bool F
union Gp is set
I is non empty set

product J is non empty strict TopSpace-like V163() TopStruct
the carrier of () is non empty set
bool the carrier of () is non empty set
bool (bool the carrier of ()) is non empty set
product_prebasis J is Element of bool (bool (product ()))

bool (product ()) is non empty set
bool (bool (product ())) is non empty set
B is open quasi_prebasis Element of bool (bool the carrier of ())
bool B is non empty set
[#] () is non empty non proper closed Element of bool the carrier of ()
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 () -defined the carrier of (J . f) -valued Function-like V28( the carrier of (), the carrier of (J . f)) Element of bool [: the carrier of (), the carrier of (J . f):]
[: the carrier of (), the carrier of (J . f):] is non empty set
bool [: the carrier of (), the carrier of (J . f):] is non empty set
f is Relation-like Function-like Element of the carrier of ()
A is 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 () -defined the carrier of (J . i) -valued Function-like V28( the carrier of (), the carrier of (J . i)) Element of bool [: the carrier of (), the carrier of (J . i):]
[: the carrier of (), the carrier of (J . i):] is non empty set
bool [: the carrier of (), the carrier of (J . i):] is non empty set
(proj (J,i)) " Ai is Element of bool the carrier of ()
(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 ()

union G is set