REAL is set
NAT is non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable Element of bool REAL
bool REAL is non empty set
NAT is non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable set
bool NAT is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
2 is non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real positive Element of NAT
[:2,2:] is non empty finite countable set
[:[:2,2:],2:] is non empty finite countable set
bool [:[:2,2:],2:] is non empty finite V33() countable set
K255() is set
{} is empty trivial V21() V22() V23() V25() V26() V27() V28() finite V33() cardinal {} -element countable V186() ext-real set
the empty trivial V21() V22() V23() V25() V26() V27() V28() finite V33() cardinal {} -element countable V186() ext-real set is empty trivial V21() V22() V23() V25() V26() V27() V28() finite V33() cardinal {} -element countable V186() ext-real set
{{}} is non empty trivial finite V33() 1 -element countable set
1 is non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real positive Element of NAT
K233({{}}) is M11({{}})
[:K233({{}}),{{}}:] is set
bool [:K233({{}}),{{}}:] is non empty set
K36(K233({{}}),{{}}) is set
COMPLEX is set
RAT is set
INT is set
{{},1} is non empty finite V33() countable set
3 is non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real positive Element of NAT
0 is empty trivial V21() V22() V23() V25() V26() V27() V28() finite V33() cardinal {} -element countable V186() ext-real Element of NAT
{0,1,2} is non empty finite countable Element of bool NAT
Seg 1 is countable Element of bool NAT
I is Relation-like Function-like set
product I is functional with_common_domain product-like set
A is Relation-like Function-like set
product A is functional with_common_domain product-like set
dom A is set
rng A is set
S is set
A . S is set
rng I is set
dom I is set
S is set
I . S is set
I is set
card I is V21() V22() V23() cardinal set
card 2 is non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
A is Relation-like Function-like set
dom A is set
rng A is set
A . 0 is set
S is set
A . 1 is set
B is set
A is set
S is set
{A,S} is non empty finite countable set
B is set
card {A,S} is non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
I is set
card I is V21() V22() V23() cardinal set
A is set
S is set
B is set
I is set
card I is V21() V22() V23() cardinal set
the Element of I is Element of I
S is set
B is set
l is set
{l} is non empty trivial finite 1 -element countable set
{ the Element of I} is non empty trivial finite 1 -element countable set
S is set
I is set
card I is V21() V22() V23() cardinal set
card 3 is non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
A is Relation-like Function-like set
dom A is set
rng A is set
A . 0 is set
S is set
A . 1 is set
B is set
A . 2 is set
l is set
A is set
S is set
B is set
{A,S,B} is non empty finite countable set
l is set
card {A,S,B} is non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
I is set
card I is V21() V22() V23() cardinal set
A is set
S is set
B is set
l is set
L is set
I is TopStruct
the carrier of I is set
I is TopStruct
the carrier of I is set
bool the carrier of I is non empty set
I is non empty set
card I is non empty V21() V22() V23() cardinal set
bool I is non empty set
{ b1 where b1 is Element of bool I : 2 = card b1 } is set
A is set
S is set
{A,S} is non empty finite countable set
B is set
l is TopStruct
the carrier of l is set
the topology of l is Element of bool (bool the carrier of l)
bool the carrier of l is non empty set
bool (bool the carrier of l) is non empty set
B is Element of bool I
card B is V21() V22() V23() cardinal set
L is non empty set
a is Element of bool I
card a is V21() V22() V23() cardinal set
a is Element of the carrier of l
b is Element of the carrier of l
L is set
{a,b} is non empty finite countable set
a1 is Element of the carrier of l
{a,a1} is non empty finite countable set
b1 is set
b1 is set
b1 is Element of bool I
card b1 is V21() V22() V23() cardinal set
{a,b} is non empty finite countable set
L is set
card {a,b} is non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
L is Element of bool I
a is Element of the topology of l
card a is V21() V22() V23() cardinal set
b is Element of bool I
card b is V21() V22() V23() cardinal set
a is Element of the topology of l
b is Element of the topology of l
a /\ b is set
card (a /\ b) is V21() V22() V23() cardinal set
L is set
a1 is set
{L,a1} is non empty finite countable set
b1 is set
a is Element of bool I
card a is V21() V22() V23() cardinal set
b1 is finite countable set
C is Element of bool I
card C is V21() V22() V23() cardinal set
card {L,a1} is non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
a is finite countable set
C is Element of bool I
card C is V21() V22() V23() cardinal set
C is Element of bool I
card C is V21() V22() V23() cardinal set
a is Element of the carrier of l
b is set
{a,b} is non empty finite countable set
L is set
card {a,b} is non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
L is Element of bool I
a1 is Element of the topology of l
I is non empty set
card I is non empty V21() V22() V23() cardinal set
bool I is non empty set
{ b1 where b1 is Element of bool I : 2 = card b1 } is set
A is Element of bool I
card A is V21() V22() V23() cardinal set
{A} is non empty trivial finite 1 -element countable Element of bool (bool I)
bool (bool I) is non empty set
{ b1 where b1 is Element of bool I : 2 = card b1 } \ {A} is Element of bool { b1 where b1 is Element of bool I : 2 = card b1 }
bool { b1 where b1 is Element of bool I : 2 = card b1 } is non empty set
S is finite countable Element of bool I
B is set
l is set
{B,l} is non empty finite countable set
L is TopStruct
the carrier of L is set
the topology of L is Element of bool (bool the carrier of L)
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
a is Element of the carrier of L
b is Element of the carrier of L
L is set
{a,L} is non empty finite countable set
a1 is set
a1 is Element of bool I
card a1 is V21() V22() V23() cardinal set
b1 is non empty set
a is Element of bool I
card a is V21() V22() V23() cardinal set
{a,b} is non empty finite countable set
a is Element of the topology of L
C is Element of bool I
card C is V21() V22() V23() cardinal set
j is finite countable Element of bool I
Li is set
o is set
{Li,o} is non empty finite countable set
a is Element of the topology of L
card a is V21() V22() V23() cardinal set
C is Element of bool I
card C is V21() V22() V23() cardinal set
a is Element of the topology of L
C is Element of the topology of L
a /\ C is set
card (a /\ C) is V21() V22() V23() cardinal set
j is set
Li is set
{j,Li} is non empty finite countable set
o is set
L1 is Element of bool I
card L1 is V21() V22() V23() cardinal set
o is finite countable set
L2 is Element of bool I
card L2 is V21() V22() V23() cardinal set
card {j,Li} is non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
L1 is finite countable set
L2 is Element of bool I
card L2 is V21() V22() V23() cardinal set
L2 is Element of bool I
card L2 is V21() V22() V23() cardinal set
a is Element of the carrier of L
C is set
{a,C} is non empty finite countable set
j is set
card {a,C} is non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
j is Element of bool I
Li is Element of the topology of L
C is set
{a,C} is non empty finite countable set
j is set
card {a,C} is non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
j is Element of bool I
Li is Element of the topology of L
bool 3 is non empty finite V33() countable set
{ b1 where b1 is finite countable Element of bool 3 : 2 = card b1 } is set
I is set
A is finite countable Element of bool 3
card A is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
bool (bool 3) is non empty finite V33() countable set
I is finite V33() countable Element of bool (bool 3)
TopStruct(# 3,I #) is strict TopStruct
card 3 is non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
card 2 is non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
bool 3 is non empty finite V33() countable set
I is finite countable Element of bool 3
card I is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
{ b1 where b1 is finite countable Element of bool 3 : 2 = card b1 } is set
A is set
S is finite countable Element of bool 3
card S is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
bool (bool 3) is non empty finite V33() countable set
{I} is non empty trivial finite V33() 1 -element countable Element of bool (bool 3)
{ b1 where b1 is finite countable Element of bool 3 : 2 = card b1 } \ {I} is Element of bool { b1 where b1 is finite countable Element of bool 3 : 2 = card b1 }
bool { b1 where b1 is finite countable Element of bool 3 : 2 = card b1 } is non empty set
A is finite V33() countable Element of bool (bool 3)
TopStruct(# 3,A #) is strict TopStruct
card 3 is non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
I is () TopStruct
the topology of I is Element of bool (bool the carrier of I)
the carrier of I is set
bool the carrier of I is non empty set
bool (bool the carrier of I) is non empty set
I is () TopStruct
the carrier of I is set
A is Element of the carrier of I
S is Element of the carrier of I
the topology of I is Element of bool (bool the carrier of I)
bool the carrier of I is non empty set
bool (bool the carrier of I) is non empty set
{A,S} is non empty finite countable set
B is Element of the topology of I
B is Element of the topology of I
I is Relation-like Function-like set
A is set
dom I is set
I . A is set
rng I is set
I is set
the TopStruct is TopStruct
I --> the TopStruct is Relation-like I -defined { the TopStruct } -valued Function-like constant V14(I) V18(I,{ the TopStruct }) 1-sorted-yielding Element of bool [:I,{ the TopStruct }:]
{ the TopStruct } is non empty trivial finite 1 -element countable set
[:I,{ the TopStruct }:] is set
bool [:I,{ the TopStruct }:] is non empty set
S is set
rng (I --> the TopStruct ) is set
the Relation-like {} -defined Function-like V14( {} ) 1-sorted-yielding V219() () set is Relation-like {} -defined Function-like V14( {} ) 1-sorted-yielding V219() () set
I is Relation-like Function-like 1-sorted-yielding () set
rng I is set
A is set
A is TopStruct
I is Relation-like set
A is 1-sorted
rng I is set
I is Relation-like Function-like 1-sorted-yielding set
rng I is set
A is set
dom I is set
S is set
I . S is set
A is 1-sorted
I is non empty set
A is Relation-like I -defined Function-like V14(I) 1-sorted-yielding () set
S is Element of I
A . S is set
dom A is set
A . S is 1-sorted
rng A is set
I is Relation-like Function-like set
A is 1-sorted
rng I is set
A is set
rng I is set
I is Relation-like Function-like 1-sorted-yielding () set
A is set
rng I is set
I is Relation-like Function-like 1-sorted-yielding () set
A is set
rng I is set
S is non empty () () TopStruct
the topology of S is non empty Element of bool (bool the carrier of S)
the carrier of S is non empty set
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set
B is set
l is Element of the topology of S
card l is V21() V22() V23() cardinal set
L is set
a is set
I is set
the non empty () () () () TopStruct is non empty () () () () TopStruct
I --> the non empty () () () () TopStruct is Relation-like I -defined { the non empty () () () () TopStruct } -valued Function-like constant V14(I) V18(I,{ the non empty () () () () TopStruct }) 1-sorted-yielding Element of bool [:I,{ the non empty () () () () TopStruct }:]
{ the non empty () () () () TopStruct } is non empty trivial finite 1 -element countable set
[:I,{ the non empty () () () () TopStruct }:] is set
bool [:I,{ the non empty () () () () TopStruct }:] is non empty set
S is set
rng (I --> the non empty () () () () TopStruct ) is set
I is non empty set
A is Relation-like I -defined Function-like V14(I) 1-sorted-yielding non-Empty () () () () set
S is Element of I
A . S is set
dom A is set
(I,A,S) is TopStruct
rng A is set
I is set
I is set
A is Relation-like I -defined Function-like V14(I) set
{A} is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set
S is set
rng {A} is V33() set
dom {A} is set
B is set
{A} . B is finite countable set
A . B is set
{(A . B)} is non empty trivial finite 1 -element countable set
I is non empty set
A is Relation-like I -defined Function-like V14(I) set
S is Element of I
B is non empty non trivial set
A +* (S,B) is Relation-like I -defined Function-like V14(I) set
(A +* (S,B)) . S is set
l is set
rng (A +* (S,B)) is set
dom A is set
dom (A +* (S,B)) is set
I is non empty set
A is Relation-like I -defined Function-like V14(I) set
{A} is Relation-like non-empty I -defined Function-like V14(I) finite-yielding () set
the Element of I is Element of I
B is Element of I
{A} . B is finite countable set
A . B is set
{(A . B)} is non empty trivial finite 1 -element countable set
I is non empty set
A is Relation-like I -defined Function-like V14(I) set
{A} is Relation-like non-empty I -defined Function-like V14(I) finite-yielding () (I) set
S is set
B is set
{A} +* (S,B) is Relation-like I -defined Function-like V14(I) set
dom {A} is set
l is Element of I
L is Element of I
({A} +* (S,B)) . L is set
{A} . L is finite countable set
A . L is set
{(A . L)} is non empty trivial finite 1 -element countable set
I is non empty set
A is Relation-like I -defined Function-like V14(I) 1-sorted-yielding non-Empty set
Carrier A is Relation-like non-empty I -defined Function-like V14(I) set
S is Relation-like I -defined Function-like V14(I) Element of Carrier A
{S} is Relation-like non-empty I -defined Function-like V14(I) finite-yielding () (I) set
B is set
{S} . B is finite countable set
(Carrier A) . B is set
l is Element of I
dom A is set
A . l is 1-sorted
rng A is set
S . l is set
(Carrier A) . l is set
the carrier of (A . l) is set
{(S . l)} is non empty trivial finite 1 -element countable set
{S} . l is finite countable set
I is non empty set
A is Relation-like I -defined Function-like V14(I) 1-sorted-yielding non-Empty set
Carrier A is Relation-like non-empty I -defined Function-like V14(I) set
the Relation-like I -defined Function-like V14(I) Element of Carrier A is Relation-like I -defined Function-like V14(I) Element of Carrier A
{ the Relation-like I -defined Function-like V14(I) Element of Carrier A} is Relation-like non-empty I -defined Function-like V14(I) finite-yielding () (I) set
B is Relation-like I -defined Function-like V14(I) ManySortedSubset of Carrier A
I is non empty set
A is Relation-like I -defined Function-like V14(I) 1-sorted-yielding non-Empty () set
Carrier A is Relation-like non-empty I -defined Function-like V14(I) set
the Relation-like I -defined Function-like V14(I) Element of Carrier A is Relation-like I -defined Function-like V14(I) Element of Carrier A
the Element of I is Element of I
A . the Element of I is 1-sorted
(Carrier A) . the Element of I is set
the carrier of (A . the Element of I) is set
the Relation-like I -defined Function-like V14(I) Element of Carrier A . the Element of I is set
L is 1-sorted
the carrier of L is set
dom A is set
rng A is set
a is non empty non trivial set
card the carrier of (A . the Element of I) is V21() V22() V23() cardinal set
b is Element of a
L is Element of a
l is Element of the carrier of (A . the Element of I)
b is set
L is Relation-like I -defined Function-like V14(I) set
L is Element of the carrier of (A . the Element of I)
L +* ( the Element of I,L) is Relation-like I -defined Function-like V14(I) set
b1 is set
(L +* ( the Element of I,L)) . b1 is set
(Carrier A) . b1 is set
L . b1 is set
dom L is set
a is 1-sorted
the carrier of a is set
{L,(L +* ( the Element of I,L))} is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set
b1 is set
{L,(L +* ( the Element of I,L))} . b1 is finite countable set
(Carrier A) . b1 is set
a is Element of I
A . a is 1-sorted
L . a is set
(Carrier A) . a is set
the carrier of (A . a) is set
(L +* ( the Element of I,L)) . a is set
{(L . a),((L +* ( the Element of I,L)) . a)} is non empty finite countable set
{L,(L +* ( the Element of I,L))} . a is finite countable set
dom L is set
(L +* ( the Element of I,L)) . the Element of I is set
b1 is Relation-like I -defined Function-like V14(I) ManySortedSubset of Carrier A
b1 . the Element of I is set
{l,L} is non empty finite countable set
a is set
{a} is non empty trivial finite 1 -element countable set
a is Element of I
b1 . a is set
L . a is set
(L +* ( the Element of I,L)) . a is set
{(L . a),(L . a)} is non empty finite countable set
{(L . a)} is non empty trivial finite 1 -element countable set
dom b1 is set
rng b1 is set
I is non empty set
the Relation-like I -defined Function-like V14(I) set is Relation-like I -defined Function-like V14(I) set
the Element of I is Element of I
{ the Relation-like I -defined Function-like V14(I) set } is Relation-like non-empty I -defined Function-like V14(I) finite-yielding () (I) set
{0,1} is non empty finite V33() countable Element of bool NAT
{ the Relation-like I -defined Function-like V14(I) set } +* ( the Element of I,{0,1}) is Relation-like I -defined Function-like V14(I) set
B is Relation-like I -defined Function-like V14(I) set
l is Element of I
B . l is set
{ the Relation-like I -defined Function-like V14(I) set } . l is finite countable set
dom { the Relation-like I -defined Function-like V14(I) set } is set
rng { the Relation-like I -defined Function-like V14(I) set } is V33() set
B . the Element of I is set
l is set
rng B is set
dom B is set
dom { the Relation-like I -defined Function-like V14(I) set } is set
card {0,1} is non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
I is non empty set
A is Relation-like I -defined Function-like V14(I) () (I) set
S is Element of I
A . S is set
rng A is set
B is set
dom A is set
l is set
A . l is set
L is Element of I
L is Element of I
A . L is set
L is Element of I
S is Element of I
A . S is set
B is Element of I
A . B is set
l is Element of I
I is non empty set
A is Relation-like I -defined Function-like V14(I) () (I) set
(I,A) is Element of I
S is Element of I
A . S is set
B is Element of I
A . (I,A) is set
I is non empty set
A is Relation-like I -defined Function-like V14(I) set
S is Relation-like I -defined Function-like V14(I) () (I) set
rng S is set
dom A is set
B is set
S . B is set
l is Element of I
(I,S) is Element of I
l is Element of I
(I,S) is Element of I
S . l is set
l is Element of I
(I,S) is Element of I
I is non empty set
A is Relation-like I -defined Function-like V14(I) set
product A is functional with_common_domain product-like set
card (product A) is V21() V22() V23() cardinal set
dom A is set
S is set
B is set
l is Relation-like Function-like set
dom l is set
L is set
A . L is set
L is Relation-like Function-like set
dom L is set
a is set
L . a is set
l . a is set
A . a is set
rng A is set
card (A . a) is V21() V22() V23() cardinal set
rng A is set
S is set
B is set
A . B is set
B is set
l is set
A . l is set
L is Relation-like Function-like set
dom L is set
card S is V21() V22() V23() cardinal set
a is Relation-like I -defined Function-like V14(I) set
a . l is set
b is set
L is Element of I
a +* (L,b) is Relation-like I -defined Function-like V14(I) set
b1 is set
(a +* (L,b)) . b1 is set
a . b1 is set
A . b1 is set
(a +* (L,b)) . b1 is set
A . b1 is set
dom (a +* (L,b)) is set
(a +* (L,b)) . L is set
I is non empty set
A is Relation-like non-empty I -defined Function-like V14(I) () (I) set
product A is functional non empty with_common_domain product-like set
S is set
dom A is set
l is Relation-like Function-like set
dom l is set
(I,A) is Element of I
A . (I,A) is set
card (A . (I,A)) is V21() V22() V23() cardinal set
B is Relation-like I -defined Function-like V14(I) set
B . (I,A) is set
l is set
B +* ((I,A),l) is Relation-like I -defined Function-like V14(I) set
a is set
(B +* ((I,A),l)) . a is set
A . a is set
dom B is set
B . a is set
b is Relation-like Function-like set
dom b is set
dom B is set
(B +* ((I,A),l)) . (I,A) is set
dom (B +* ((I,A),l)) is set
card (product A) is non empty V21() V22() V23() cardinal set
I is non empty set
A is Relation-like I -defined Function-like V14(I) 1-sorted-yielding non-Empty () set
Carrier A is Relation-like non-empty I -defined Function-like V14(I) set
product (Carrier A) is functional non empty with_common_domain product-like set
bool (product (Carrier A)) is non empty set
bool (bool (product (Carrier A))) is non empty set
S is set
B is set
B is Element of bool (bool (product (Carrier A)))
l is set
L is Relation-like I -defined Function-like V14(I) (I) ManySortedSubset of Carrier A
product L is functional with_common_domain product-like set
a is set
dom L is set
b is Relation-like Function-like set
dom b is set
dom (Carrier A) is set
L is set
b . L is set
(Carrier A) . L is set
L . L is set
a is Element of I
L . a is set
(I,A,a) is TopStruct
the topology of (I,A,a) is Element of bool (bool the carrier of (I,A,a))
the carrier of (I,A,a) is set
bool the carrier of (I,A,a) is non empty set
bool (bool the carrier of (I,A,a)) is non empty set
S is Element of bool (bool (product (Carrier A)))
B is Element of bool (bool (product (Carrier A)))
l is set
L is Relation-like I -defined Function-like V14(I) (I) ManySortedSubset of Carrier A
product L is functional with_common_domain product-like set
a is Element of I
L . a is set
(I,A,a) is TopStruct
the topology of (I,A,a) is Element of bool (bool the carrier of (I,A,a))
the carrier of (I,A,a) is set
bool the carrier of (I,A,a) is non empty set
bool (bool the carrier of (I,A,a)) is non empty set
L is Relation-like I -defined Function-like V14(I) (I) ManySortedSubset of Carrier A
product L is functional with_common_domain product-like set
a is Element of I
L . a is set
(I,A,a) is TopStruct
the topology of (I,A,a) is Element of bool (bool the carrier of (I,A,a))
the carrier of (I,A,a) is set
bool the carrier of (I,A,a) is non empty set
bool (bool the carrier of (I,A,a)) is non empty set
I is non empty set
A is Relation-like I -defined Function-like V14(I) 1-sorted-yielding non-Empty () set
Carrier A is Relation-like non-empty I -defined Function-like V14(I) set
product (Carrier A) is functional non empty with_common_domain product-like set
(I,A) is Element of bool (bool (product (Carrier A)))
bool (product (Carrier A)) is non empty set
bool (bool (product (Carrier A))) is non empty set
TopStruct(# (product (Carrier A)),(I,A) #) is strict TopStruct
I is non empty set
A is Relation-like I -defined Function-like V14(I) 1-sorted-yielding non-Empty () set
(I,A) is non empty TopStruct
Carrier A is Relation-like non-empty I -defined Function-like V14(I) set
product (Carrier A) is functional non empty with_common_domain product-like set
(I,A) is Element of bool (bool (product (Carrier A)))
bool (product (Carrier A)) is non empty set
bool (bool (product (Carrier A))) is non empty set
TopStruct(# (product (Carrier A)),(I,A) #) is strict TopStruct
the carrier of (I,A) is non empty set
S is Element of the carrier of (I,A)
dom (Carrier A) is set
B is Relation-like Function-like set
dom B is set
I is non empty set
A is Relation-like I -defined Function-like V14(I) 1-sorted-yielding non-Empty () set
(I,A) is non empty TopStruct
Carrier A is Relation-like non-empty I -defined Function-like V14(I) set
product (Carrier A) is functional non empty with_common_domain product-like set
(I,A) is Element of bool (bool (product (Carrier A)))
bool (product (Carrier A)) is non empty set
bool (bool (product (Carrier A))) is non empty set
TopStruct(# (product (Carrier A)),(I,A) #) is strict TopStruct
the Relation-like non-empty I -defined Function-like V14(I) () ManySortedSubset of Carrier A is Relation-like non-empty I -defined Function-like V14(I) () ManySortedSubset of Carrier A
B is Element of I
(I,A,B) is TopStruct
the topology of (I,A,B) is Element of bool (bool the carrier of (I,A,B))
the carrier of (I,A,B) is set
bool the carrier of (I,A,B) is non empty set
bool (bool the carrier of (I,A,B)) is non empty set
the Element of the topology of (I,A,B) is Element of the topology of (I,A,B)
the Relation-like non-empty I -defined Function-like V14(I) () ManySortedSubset of Carrier A +* (B, the Element of the topology of (I,A,B)) is Relation-like I -defined Function-like V14(I) set
L is set
( the Relation-like non-empty I -defined Function-like V14(I) () ManySortedSubset of Carrier A +* (B, the Element of the topology of (I,A,B))) . L is set
(Carrier A) . L is set
dom the Relation-like non-empty I -defined Function-like V14(I) () ManySortedSubset of Carrier A is set
A . L is set
a is 1-sorted
the carrier of a is set
the Relation-like non-empty I -defined Function-like V14(I) () ManySortedSubset of Carrier A . L is set
L is Element of I
( the Relation-like non-empty I -defined Function-like V14(I) () ManySortedSubset of Carrier A +* (B, the Element of the topology of (I,A,B))) . L is set
the Relation-like non-empty I -defined Function-like V14(I) () ManySortedSubset of Carrier A . L is set
dom the Relation-like non-empty I -defined Function-like V14(I) () ManySortedSubset of Carrier A is set
rng the Relation-like non-empty I -defined Function-like V14(I) () ManySortedSubset of Carrier A is set
dom the Relation-like non-empty I -defined Function-like V14(I) () ManySortedSubset of Carrier A is set
L is Relation-like I -defined Function-like V14(I) (I) ManySortedSubset of Carrier A
L . B is set
product L is functional with_common_domain product-like set
I is non empty set
A is Relation-like I -defined Function-like V14(I) 1-sorted-yielding non-Empty () set
(I,A) is non empty TopStruct
Carrier A is Relation-like non-empty I -defined Function-like V14(I) set
product (Carrier A) is functional non empty with_common_domain product-like set
(I,A) is Element of bool (bool (product (Carrier A)))
bool (product (Carrier A)) is non empty set
bool (bool (product (Carrier A))) is non empty set
TopStruct(# (product (Carrier A)),(I,A) #) is strict TopStruct
S is Element of I
(I,A,S) is TopStruct
S is non empty set
B is Relation-like I -defined Function-like V14(I) (I) ManySortedSubset of Carrier A
product B is functional with_common_domain product-like set
l is Element of I
B . l is set
(I,A,l) is TopStruct
the topology of (I,A,l) is Element of bool (bool the carrier of (I,A,l))
the carrier of (I,A,l) is set
bool the carrier of (I,A,l) is non empty set
bool (bool the carrier of (I,A,l)) is non empty set
l is Element of I
B . l is set
(I,A,l) is TopStruct
the topology of (I,A,l) is Element of bool (bool the carrier of (I,A,l))
the carrier of (I,A,l) is set
bool the carrier of (I,A,l) is non empty set
bool (bool the carrier of (I,A,l)) is non empty set
(Carrier A) . l is set
L is 1-sorted
the carrier of L is set
L is Element of I
(I,A,L) is TopStruct
I is non empty set
A is Relation-like I -defined Function-like V14(I) 1-sorted-yielding non-Empty () set
(I,A) is non empty TopStruct
Carrier A is Relation-like non-empty I -defined Function-like V14(I) set
product (Carrier A) is functional non empty with_common_domain product-like set
(I,A) is Element of bool (bool (product (Carrier A)))
bool (product (Carrier A)) is non empty set
bool (bool (product (Carrier A))) is non empty set
TopStruct(# (product (Carrier A)),(I,A) #) is strict TopStruct
the topology of (I,A) is Element of bool (bool the carrier of (I,A))
the carrier of (I,A) is non empty set
bool the carrier of (I,A) is non empty set
bool (bool the carrier of (I,A)) is non empty set
S is Element of the topology of (I,A)
card S is V21() V22() V23() cardinal set
B is Element of I
(I,A,B) is TopStruct
B is Relation-like I -defined Function-like V14(I) (I) ManySortedSubset of Carrier A
product B is functional with_common_domain product-like set
l is Element of I
B . l is set
(I,A,l) is TopStruct
the topology of (I,A,l) is Element of bool (bool the carrier of (I,A,l))
the carrier of (I,A,l) is set
bool the carrier of (I,A,l) is non empty set
bool (bool the carrier of (I,A,l)) is non empty set
l is Element of I
B . l is set
(I,A,l) is TopStruct
the topology of (I,A,l) is Element of bool (bool the carrier of (I,A,l))
the carrier of (I,A,l) is set
bool the carrier of (I,A,l) is non empty set
bool (bool the carrier of (I,A,l)) is non empty set
L is Element of I
(I,A,L) is TopStruct
card (B . l) is V21() V22() V23() cardinal set
dom B is set
rng B is set
L is Relation-like non-empty I -defined Function-like V14(I) () (I) set
product L is functional non empty non trivial with_common_domain product-like set
I is non empty set
A is Relation-like I -defined Function-like V14(I) 1-sorted-yielding non-Empty () set
(I,A) is non empty TopStruct
Carrier A is Relation-like non-empty I -defined Function-like V14(I) set
product (Carrier A) is functional non empty with_common_domain product-like set
(I,A) is Element of bool (bool (product (Carrier A)))
bool (product (Carrier A)) is non empty set
bool (bool (product (Carrier A))) is non empty set
TopStruct(# (product (Carrier A)),(I,A) #) is strict TopStruct
the topology of (I,A) is Element of bool (bool the carrier of (I,A))
the carrier of (I,A) is non empty set
bool the carrier of (I,A) is non empty set
bool (bool the carrier of (I,A)) is non empty set
S is Element of the topology of (I,A)
B is Element of the topology of (I,A)
S /\ B is set
card (S /\ B) is V21() V22() V23() cardinal set
l is set
L is set
a is Element of I
(I,A,a) is TopStruct
a is Relation-like I -defined Function-like V14(I) (I) ManySortedSubset of Carrier A
product a is functional with_common_domain product-like set
b is Relation-like Function-like set
dom b is set
dom a is set
a1 is Element of I
a . a1 is set
(I,A,a1) is TopStruct
the topology of (I,A,a1) is Element of bool (bool the carrier of (I,A,a1))
the carrier of (I,A,a1) is set
bool the carrier of (I,A,a1) is non empty set
bool (bool the carrier of (I,A,a1)) is non empty set
a1 is Element of I
a . a1 is set
(I,A,a1) is TopStruct
the topology of (I,A,a1) is Element of bool (bool the carrier of (I,A,a1))
the carrier of (I,A,a1) is set
bool the carrier of (I,A,a1) is non empty set
bool (bool the carrier of (I,A,a1)) is non empty set
b1 is Element of I
a . b1 is set
a is Element of I
C is Element of I
(I,A,C) is TopStruct
card (a . a1) is V21() V22() V23() cardinal set
b1 is Element of I
(I,A,b1) is TopStruct
b1 is Relation-like I -defined Function-like V14(I) (I) ManySortedSubset of Carrier A
product b1 is functional with_common_domain product-like set
dom b1 is set
a is Element of I
b1 . a is set
(I,A,a) is TopStruct
the topology of (I,A,a) is Element of bool (bool the carrier of (I,A,a))
the carrier of (I,A,a) is set
bool the carrier of (I,A,a) is non empty set
bool (bool the carrier of (I,A,a)) is non empty set
a is Element of I
b1 . a is set
(I,A,a) is TopStruct
the topology of (I,A,a) is Element of bool (bool the carrier of (I,A,a))
the carrier of (I,A,a) is set
bool the carrier of (I,A,a) is non empty set
bool (bool the carrier of (I,A,a)) is non empty set
C is Relation-like Function-like set
dom C is set
j is Relation-like I -defined Function-like V14(I) set
L is Relation-like I -defined Function-like V14(I) set
Li is set
j . Li is set
L . Li is set
o is Element of I
L . o is set
a . o is set
j . o is set
card (a . o) is V21() V22() V23() cardinal set
b1 . o is set
L1 is Element of I
b1 . L1 is set
L2 is Element of I
L3 is Element of I
(I,A,L3) is TopStruct
card (b1 . a) is V21() V22() V23() cardinal set
card (b1 . o) is V21() V22() V23() cardinal set
L1 is set
a . L1 is set
b1 . L1 is set
L2 is Element of I
(I,A,L2) is TopStruct
the topology of (I,A,L2) is Element of bool (bool the carrier of (I,A,L2))
the carrier of (I,A,L2) is set
bool the carrier of (I,A,L2) is non empty set
bool (bool the carrier of (I,A,L2)) is non empty set
b1 . L2 is set
a . L2 is set
j . L2 is set
x is Element of the topology of (I,A,L2)
L3 is Element of the topology of (I,A,L2)
x /\ L3 is set
L . L2 is set
card (x /\ L3) is V21() V22() V23() cardinal set
y is Element of I
(I,A,y) is TopStruct
L2 is Element of I
a . L2 is set
L3 is set
{L3} is non empty trivial finite 1 -element countable set
j . L2 is set
b1 . L2 is set
L2 is Element of I
L1 is set
b1 . L1 is set
a . L1 is set
L2 is Element of I
(I,A,L2) is TopStruct
the topology of (I,A,L2) is Element of bool (bool the carrier of (I,A,L2))
the carrier of (I,A,L2) is set
bool the carrier of (I,A,L2) is non empty set
bool (bool the carrier of (I,A,L2)) is non empty set
b1 . L2 is set
a . L2 is set
j . L2 is set
x is Element of the topology of (I,A,L2)
L3 is Element of the topology of (I,A,L2)
x /\ L3 is set
L . L2 is set
card (x /\ L3) is V21() V22() V23() cardinal set
y is Element of I
(I,A,y) is TopStruct
L2 is Element of I
b1 . L2 is set
L3 is set
{L3} is non empty trivial finite 1 -element countable set
j . L2 is set
a . L2 is set
L2 is Element of I
I is non empty set
A is Relation-like I -defined Function-like V14(I) 1-sorted-yielding non-Empty () () () () set
(I,A) is non empty TopStruct
Carrier A is Relation-like non-empty I -defined Function-like V14(I) set
product (Carrier A) is functional non empty with_common_domain product-like set
(I,A) is Element of bool (bool (product (Carrier A)))
bool (product (Carrier A)) is non empty set
bool (bool (product (Carrier A))) is non empty set
TopStruct(# (product (Carrier A)),(I,A) #) is strict TopStruct
S is Element of I
(I,A,S) is non empty () () () () TopStruct
B is Element of I
(I,A,B) is non empty () () () () TopStruct
the Element of I is Element of I
(I,A, the Element of I) is non empty () () () () TopStruct
S is Element of I
(I,A,S) is non empty () () () () TopStruct
I is TopStruct
the carrier of I is set
bool the carrier of I is non empty set
A is Element of bool the carrier of I
S is Element of the carrier of I
B is Element of the carrier of I
card A is V21() V22() V23() cardinal set
the topology of I is Element of bool (bool the carrier of I)
bool (bool the carrier of I) is non empty set
S is Element of the topology of I
S /\ A is Element of bool the carrier of I
card (S /\ A) is V21() V22() V23() cardinal set
card A is V21() V22() V23() cardinal set
I is () TopStruct
the topology of I is Element of bool (bool the carrier of I)
the carrier of I is set
bool the carrier of I is non empty set
bool (bool the carrier of I) is non empty set
A is Element of the topology of I
S is Element of bool the carrier of I
B is Element of the topology of I
B /\ S is Element of bool the carrier of I
card (B /\ S) is V21() V22() V23() cardinal set
I is TopStruct
the topology of I is Element of bool (bool the carrier of I)
the carrier of I is set
bool the carrier of I is non empty set
bool (bool the carrier of I) is non empty set
A is Element of the topology of I
S is Element of bool the carrier of I
B is Element of the carrier of I
l is Element of the carrier of I
{B,l} is non empty finite countable set
I is () TopStruct
[#] I is non proper Element of bool the carrier of I
the carrier of I is set
bool the carrier of I is non empty set
the topology of I is non empty Element of bool (bool the carrier of I)
bool (bool the carrier of I) is non empty set
A is Element of the topology of I
A /\ ([#] I) is Element of bool the carrier of I
card (A /\ ([#] I)) is V21() V22() V23() cardinal set
I is non empty set
A is Relation-like non-empty I -defined Function-like V14(I) () (I) set
product A is functional non empty non trivial with_common_domain product-like set
(I,A) is Element of I
S is Relation-like I -defined Function-like V14(I) set
B is Relation-like I -defined Function-like V14(I) set
l is set
S . l is set
B . l is set
dom A is set
dom B is set
dom S is set
a is Element of I
A . (I,A) is set
L is Element of I
A . L is set
A . l is set
b is set
{b} is non empty trivial finite 1 -element countable set
S . L is set
B . L is set
I is non empty set
A is Relation-like I -defined Function-like V14(I) 1-sorted-yielding non-Empty () () () () set
(I,A) is non empty () () () () TopStruct
Carrier A is Relation-like non-empty I -defined Function-like V14(I) set
product (Carrier A) is functional non empty with_common_domain product-like set
(I,A) is Element of bool (bool (product (Carrier A)))
bool (product (Carrier A)) is non empty set
bool (bool (product (Carrier A))) is non empty set
TopStruct(# (product (Carrier A)),(I,A) #) is strict TopStruct
the topology of (I,A) is non empty Element of bool (bool the carrier of (I,A))
the carrier of (I,A) is non empty set
bool the carrier of (I,A) is non empty set
bool (bool the carrier of (I,A)) is non empty set
S is set
B is Relation-like I -defined Function-like V14(I) (I) ManySortedSubset of Carrier A
product B is functional with_common_domain product-like set
card (product B) is V21() V22() V23() cardinal set
l is Relation-like non-empty I -defined Function-like V14(I) () (I) ManySortedSubset of Carrier A
L is Element of I
B . L is set
(I,A,L) is non empty () () () () TopStruct
the topology of (I,A,L) is non empty Element of bool (bool the carrier of (I,A,L))
the carrier of (I,A,L) is non empty set
bool the carrier of (I,A,L) is non empty set
bool (bool the carrier of (I,A,L)) is non empty set
L is Element of I
l . L is set
(I,A,L) is non empty () () () () TopStruct
the topology of (I,A,L) is non empty Element of bool (bool the carrier of (I,A,L))
the carrier of (I,A,L) is non empty set
bool the carrier of (I,A,L) is non empty set
bool (bool the carrier of (I,A,L)) is non empty set
(I,l) is Element of I
card (l . L) is V21() V22() V23() cardinal set
B is Relation-like non-empty I -defined Function-like V14(I) () (I) ManySortedSubset of Carrier A
product B is functional non empty non trivial with_common_domain product-like set
(I,B) is Element of I
B . (I,B) is set
(I,A,(I,B)) is non empty () () () () TopStruct
the topology of (I,A,(I,B)) is non empty Element of bool (bool the carrier of (I,A,(I,B)))
the carrier of (I,A,(I,B)) is non empty set
bool the carrier of (I,A,(I,B)) is non empty set
bool (bool the carrier of (I,A,(I,B))) is non empty set
I is non empty set
A is Relation-like I -defined Function-like V14(I) 1-sorted-yielding non-Empty () () () () set
(I,A) is non empty () () () () TopStruct
Carrier A is Relation-like non-empty I -defined Function-like V14(I) set
product (Carrier A) is functional non empty with_common_domain product-like set
(I,A) is Element of bool (bool (product (Carrier A)))
bool (product (Carrier A)) is non empty set
bool (bool (product (Carrier A))) is non empty set
TopStruct(# (product (Carrier A)),(I,A) #) is strict TopStruct
the carrier of (I,A) is non empty set
S is Relation-like I -defined Function-like V14(I) set
B is Element of I
(I,A,B) is non empty () () () () TopStruct
the carrier of (I,A,B) is non empty set
l is Element of the carrier of (I,A,B)
S +* (B,l) is Relation-like I -defined Function-like V14(I) set
dom (Carrier A) is set
L is set
(S +* (B,l)) . L is set
(Carrier A) . L is set
dom S is set
S . L is set
dom (S +* (B,l)) is set
I is non empty set
A is Relation-like non-empty I -defined Function-like V14(I) () (I) set
product A is functional non empty non trivial with_common_domain product-like set
S is Relation-like non-empty I -defined Function-like V14(I) () (I) set
product S is functional non empty non trivial with_common_domain product-like set
(product A) /\ (product S) is set
card ((product A) /\ (product S)) is V21() V22() V23() cardinal set
(I,A) is Element of I
(I,S) is Element of I
dom S is set
B is set
l is set
dom A is set
L is Relation-like Function-like set
dom L is set
a is Relation-like Function-like set
dom a is set
b is set
a . b is set
L . b is set
L is Element of I
L . L is set
S . L is set
a . L is set
card (S . L) is V21() V22() V23() cardinal set
A . L is set
card (A . L) is V21() V22() V23() cardinal set
a1 is set
A . a1 is set
S . a1 is set
b1 is set
{b1} is non empty trivial finite 1 -element countable set
a . a1 is set
a is set
{a} is non empty trivial finite 1 -element countable set
I is non empty set
A is Relation-like non-empty I -defined Function-like V14(I) () (I) set
(I,A) is Element of I
S is non empty non trivial set
A +* ((I,A),S) is Relation-like I -defined Function-like V14(I) set
B is Element of I
(A +* ((I,A),S)) . B is set
A . B is set
(A +* ((I,A),S)) . (I,A) is set
rng (A +* ((I,A),S)) is set
dom (A +* ((I,A),S)) is set
dom A is set
I is non empty () () () TopStruct
the carrier of I is non empty set
A is Element of the carrier of I
S is Element of the carrier of I
<*A*> is Relation-like NAT -defined the carrier of I -valued Function-like FinSequence-like FinSequence of the carrier of I
len <*A*> is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
<*S*> is Relation-like NAT -defined the carrier of I -valued Function-like FinSequence-like FinSequence of the carrier of I
len <*S*> is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
the topology of I is non empty Element of bool (bool the carrier of I)
bool the carrier of I is non empty set
bool (bool the carrier of I) is non empty set
B is Element of the topology of I
l is Element of bool the carrier of I
L is Relation-like NAT -defined bool the carrier of I -valued Function-like FinSequence-like FinSequence of bool the carrier of I
L . 1 is set
len L is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
L . (len L) is set
rng L is set
dom L is countable Element of bool NAT
(len L) - 1 is V28() V186() ext-real set
a is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real set
b is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
L is Relation-like Function-like FinSequence-like set
len L is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
dom L is countable Element of bool NAT
Seg b is countable Element of bool NAT
(len L) + 1 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
rng L is set
a1 is set
L . a1 is set
b1 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
L . b1 is set
L . b1 is set
b1 + 1 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
L . (b1 + 1) is set
(L . b1) /\ (L . (b1 + 1)) is set
card (L . b1) is V21() V22() V23() cardinal set
product L is functional with_common_domain product-like set
a1 is set
a is Relation-like Function-like set
dom a is set
b1 is Relation-like Function-like set
C is Relation-like Function-like set
dom C is set
a is Relation-like Function-like FinSequence-like set
<*A*> ^ a is Relation-like Function-like FinSequence-like set
(<*A*> ^ a) ^ <*S*> is Relation-like Function-like FinSequence-like set
rng ((<*A*> ^ a) ^ <*S*>) is set
C is set
rng (<*A*> ^ a) is set
rng <*S*> is set
(rng (<*A*> ^ a)) \/ (rng <*S*>) is set
rng <*A*> is set
rng a is set
(rng <*A*>) \/ (rng a) is set
{A} is non empty trivial finite 1 -element countable Element of bool the carrier of I
dom a is countable Element of bool NAT
j is set
a . j is set
Li is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
L . Li is set
L . Li is set
Li + 1 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
L . (Li + 1) is set
(L . Li) /\ (L . (Li + 1)) is set
o is Relation-like Function-like set
dom o is set
o is Relation-like Function-like set
dom o is set
o is Relation-like Function-like set
dom o is set
{S} is non empty trivial finite 1 -element countable Element of bool the carrier of I
len (<*A*> ^ a) is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
len a is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
(len <*A*>) + (len a) is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
(len a) + 1 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
C is Relation-like NAT -defined the carrier of I -valued Function-like FinSequence-like FinSequence of the carrier of I
C . 1 is set
len C is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
C . (len C) is set
a ^ <*S*> is Relation-like Function-like FinSequence-like set
<*A*> ^ (a ^ <*S*>) is Relation-like Function-like FinSequence-like set
(len (<*A*> ^ a)) + (len <*S*>) is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
(len (<*A*> ^ a)) + 1 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
j is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real set
C . j is set
j + 1 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
C . (j + 1) is set
Li is Element of the carrier of I
o is Element of the carrier of I
L1 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
len (a ^ <*S*>) is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
len (<*A*> ^ (a ^ <*S*>)) is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
(len <*A*>) + (len (a ^ <*S*>)) is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
1 + 1 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
(1 + 1) + (len a) is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
dom a is countable Element of bool NAT
(<*A*> ^ (a ^ <*S*>)) . 2 is set
2 - (len <*A*>) is V28() V186() ext-real set
(a ^ <*S*>) . (2 - (len <*A*>)) is set
2 - 1 is V28() V186() ext-real set
(a ^ <*S*>) . (2 - 1) is set
a . 1 is set
L . 1 is set
L . (1 + 1) is set
(L . 1) /\ (L . (1 + 1)) is set
L2 is Relation-like Function-like set
dom L2 is set
L2 is Element of bool the carrier of I
L1 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
L2 is Element of bool the carrier of I
L1 + 1 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
L3 is Relation-like Function-like set
dom L3 is set
L1 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
L2 is Relation-like Function-like set
dom L2 is set
L1 - 1 is V28() V186() ext-real set
dom (<*A*> ^ a) is countable Element of bool NAT
(<*A*> ^ a) . L1 is set
L2 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real set
a . L2 is set
L2 + 1 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
L . L1 is set
L1 + 1 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
(<*A*> ^ a) . (L1 + 1) is set
(L1 + 1) - (len <*A*>) is V28() V186() ext-real set
a . ((L1 + 1) - (len <*A*>)) is set
x is Relation-like Function-like set
dom x is set
a . L1 is set
L . L1 is set
x is Relation-like Function-like set
dom x is set
L . (L1 + 1) is set
(L . L1) /\ (L . (L1 + 1)) is set
L3 is Element of bool the carrier of I
x is Relation-like Function-like set
dom x is set
L . L2 is set
x is Relation-like Function-like set
dom x is set
L . L2 is set
L . (L2 + 1) is set
(L . L2) /\ (L . (L2 + 1)) is set
L1 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
0 + 1 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
L2 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real set
L2 + 1 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
L2 is Relation-like Function-like set
dom L2 is set
1 + (len a) is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
dom (<*A*> ^ a) is countable Element of bool NAT
(<*A*> ^ a) . L1 is set
((len a) + 1) - 1 is V28() V186() ext-real set
a . (((len a) + 1) - 1) is set
a . (len a) is set
L . (len a) is set
L2 is Relation-like Function-like set
dom L2 is set
L . (len a) is set
L . ((len a) + 1) is set
(L . (len a)) /\ (L . ((len a) + 1)) is set
L2 is Element of bool the carrier of I
L3 is Relation-like Function-like set
dom L3 is set
L1 is V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real Element of NAT
I is non empty set
A is Relation-like I -defined Function-like V14(I) 1-sorted-yielding non-Empty () () () () set
(I,A) is non empty () () () () TopStruct
Carrier A is Relation-like non-empty I -defined Function-like V14(I) set
product (Carrier A) is functional non empty with_common_domain product-like set
(I,A) is Element of bool (bool (product (Carrier A)))
bool (product (Carrier A)) is non empty set
bool (bool (product (Carrier A))) is non empty set
TopStruct(# (product (Carrier A)),(I,A) #) is strict TopStruct
the carrier of (I,A) is non empty set
bool the carrier of (I,A) is non empty set
S is Element of bool the carrier of (I,A)
card S is V21() V22() V23() cardinal set
B is set
l is set
L is Element of the carrier of (I,A)
a is Element of the carrier of (I,A)
the topology of (I,A) is non empty Element of bool (bool the carrier of (I,A))
bool (bool the carrier of (I,A)) is non empty set
{L,a} is non empty finite countable Element of bool the carrier of (I,A)
b is Element of the topology of (I,A)
L is Relation-like I -defined Function-like V14(I) (I) ManySortedSubset of Carrier A
product L is functional with_common_domain product-like set
card (product L) is V21() V22() V23() cardinal set
a1 is Relation-like non-empty I -defined Function-like V14(I) () (I) ManySortedSubset of Carrier A
dom a1 is set
b1 is Relation-like I -defined Function-like V14(I) set
dom b1 is set
a is Relation-like I -defined Function-like V14(I) set
dom a is set
(I,a1) is Element of I
b1 . (I,a1) is set
a . (I,a1) is set
C is set
b1 . C is set
a . C is set
product a1 is functional non empty non trivial with_common_domain product-like set
C is Relation-like I -defined Function-like V14(I) set
Li is Element of I
C . Li is set
a1 . Li is set
product a1 is functional non empty non trivial with_common_domain product-like set
a . Li is set
j is Element of the carrier of (I,A)
{j,a} is non empty finite countable Element of bool the carrier of (I,A)
o is Element of the topology of (I,A)
L1 is Relation-like non-empty I -defined Function-like V14(I) () (I) ManySortedSubset of Carrier A
product L1 is functional non empty non trivial with_common_domain product-like set
(I,L1) is Element of I
L1 . (I,L1) is set
(I,A,(I,L1)) is non empty () () () () TopStruct
the topology of (I,A,(I,L1)) is non empty Element of bool (bool the carrier of (I,A,(I,L1)))
the carrier of (I,A,(I,L1)) is non empty set
bool the carrier of (I,A,(I,L1)) is non empty set
bool (bool the carrier of (I,A,(I,L1))) is non empty set
L1 . (I,a1) is set
L2 is set
{L2} is non empty trivial finite 1 -element countable set
dom L1 is set
b1 . Li is set
{j,L} is non empty finite countable Element of bool the carrier of (I,A)
L3 is Element of the topology of (I,A)
x is Relation-like non-empty I -defined Function-like V14(I) () (I) ManySortedSubset of Carrier A
product x is functional non empty non trivial with_common_domain product-like set
(I,x) is Element of I
x . (I,x) is set
(I,A,(I,x)) is non empty () () () () TopStruct
the topology of (I,A,(I,x)) is non empty Element of bool (bool the carrier of (I,A,(I,x)))
the carrier of (I,A,(I,x)) is non empty set
bool the carrier of (I,A,(I,x)) is non empty set
bool (bool the carrier of (I,A,(I,x))) is non empty set
x . (I,a1) is set
y is set
{y} is non empty trivial finite 1 -element countable set
dom x is set
C . (I,a1) is set
pi (S,(I,a1)) is set
card (pi (S,(I,a1))) is V21() V22() V23() cardinal set
C is non empty non trivial set
a1 +* ((I,a1),C) is Relation-like I -defined Function-like V14(I) set
j is set
(a1 +* ((I,a1),C)) . j is set
(Carrier A) . j is set
a1 . j is set
Li is set
dom (Carrier A) is set
o is Relation-like Function-like set
o . j is set
j is Relation-like non-empty I -defined Function-like V14(I) () (I) ManySortedSubset of Carrier A
product j is functional non empty non trivial with_common_domain product-like set
(I,j) is Element of I
(I,A,(I,j)) is non empty () () () () TopStruct
the carrier of (I,A,(I,j)) is non empty set
bool the carrier of (I,A,(I,j)) is non empty set
j . (I,j) is set
dom j is set
j . (I,a1) is set
Li is set
L1 is set
L2 is Element of I
o is Relation-like I -defined Function-like V14(I) set
o . L1 is set
j . L1 is set
L2 is Element of I
o is Relation-like I -defined Function-like V14(I) set
o . L2 is set
a1 . L2 is set
o . L1 is set
j . L1 is set
L2 is Element of I
o is Relation-like I -defined Function-like V14(I) set
o is Relation-like I -defined Function-like V14(I) set
dom o is set
Li is set
o is Relation-like Function-like set
dom o is set
o . (I,a1) is set
L1 is Relation-like Function-like set
L1 . (I,a1) is set
L3 is set
o . L3 is set
L2 is Relation-like I -defined Function-like V14(I) set
L2 . L3 is set
x is Element of I
a1 . x is set
a1 . L3 is set
y is set
{y} is non empty trivial finite 1 -element countable set
L2 is Relation-like I -defined Function-like V14(I) set
L2 . x is set
o . x is set
j . x is set
o . L3 is set
L2 . L3 is set
L2 is Relation-like I -defined Function-like V14(I) set
L2 is Relation-like I -defined Function-like V14(I) set
dom L2 is set
Li is Element of bool the carrier of (I,A,(I,j))
o is Element of the carrier of (I,A,(I,j))
L1 is Element of the carrier of (I,A,(I,j))
b1 +* ((I,j),L1) is Relation-like I -defined Function-like V14(I) set
b1 +* ((I,j),o) is Relation-like I -defined Function-like V14(I) set
L3 is Element of the carrier of (I,A)
L2 is Element of the carrier of (I,A)
x is Relation-like I -defined Function-like V14(I) set
x . (I,j) is set
y1 is set
x . y1 is set
j . y1 is set
b1 . y1 is set
y is Relation-like I -defined Function-like V14(I) set
y1 is set
y . y1 is set
j . y1 is set
b1 . y1 is set
dom y is set
dom x is set
{L3,L2} is non empty finite countable Element of bool the carrier of (I,A)
y1 is Element of the topology of (I,A)
y . (I,j) is set
x1 is Relation-like non-empty I -defined Function-like V14(I) () (I) ManySortedSubset of Carrier A
product x1 is functional non empty non trivial with_common_domain product-like set
(I,x1) is Element of I
x1 . (I,x1) is set
(I,A,(I,x1)) is non empty () () () () TopStruct
the topology of (I,A,(I,x1)) is non empty Element of bool (bool the carrier of (I,A,(I,x1)))
the carrier of (I,A,(I,x1)) is non empty set
bool the carrier of (I,A,(I,x1)) is non empty set
bool (bool the carrier of (I,A,(I,x1))) is non empty set
dom x1 is set
x1 . (I,j) is set
card (x1 . (I,j)) is V21() V22() V23() cardinal set
the topology of (I,A,(I,j)) is non empty Element of bool (bool the carrier of (I,A,(I,j)))
bool (bool the carrier of (I,A,(I,j))) is non empty set
{o,L1} is non empty finite countable Element of bool the carrier of (I,A,(I,j))
e is Element of the topology of (I,A,(I,j))
the topology of (I,A,(I,j)) is non empty Element of bool (bool the carrier of (I,A,(I,j)))
bool (bool the carrier of (I,A,(I,j))) is non empty set
o is Element of the topology of (I,A,(I,j))
o /\ Li is Element of bool the carrier of (I,A,(I,j))
card (o /\ Li) is V21() V22() V23() cardinal set
card o is V21() V22() V23() cardinal set
L1 is non empty non trivial set
j +* ((I,j),L1) is Relation-like I -defined Function-like V14(I) set
L2 is set
(j +* ((I,j),L1)) . L2 is set
(Carrier A) . L2 is set
j . L2 is set
L2 is Relation-like non-empty I -defined Function-like V14(I) () (I) ManySortedSubset of Carrier A
L2 . (I,j) is set
(I,L2) is Element of I
L2 . (I,L2) is set
(I,A,(I,L2)) is non empty () () () () TopStruct
the topology of (I,A,(I,L2)) is non empty Element of bool (bool the carrier of (I,A,(I,L2)))
the carrier of (I,A,(I,L2)) is non empty set
bool the carrier of (I,A,(I,L2)) is non empty set
bool (bool the carrier of (I,A,(I,L2))) is non empty set
product L2 is functional non empty non trivial with_common_domain product-like set
x is set
y is set
b1 +* ((I,j),y) is Relation-like I -defined Function-like V14(I) set
dom (b1 +* ((I,j),y)) is set
x1 is set
(b1 +* ((I,j),y)) . x1 is set
b1 . x1 is set
j . x1 is set
(b1 +* ((I,j),y)) . x1 is set
j . x1 is set
dom L2 is set
x1 is set
(b1 +* ((I,j),y)) . x1 is set
b1 . x1 is set
j . x1 is set
L2 . x1 is set
(b1 +* ((I,j),y)) . x1 is set
L2 . x1 is set
L3 is Element of the topology of (I,A)
L3 /\ S is Element of bool the carrier of (I,A)
b1 +* ((I,j),x) is Relation-like I -defined Function-like V14(I) set
dom (b1 +* ((I,j),x)) is set
e is set
(b1 +* ((I,j),x)) . e is set
b1 . e is set
j . e is set
(b1 +* ((I,j),x)) . e is set
j . e is set
(b1 +* ((I,j),x)) . (I,j) is set
(b1 +* ((I,j),y)) . (I,j) is set
e is set
(b1 +* ((I,j),x)) . e is set
b1 . e is set
j . e is set
L2 . e is set
(b1 +* ((I,j),x)) . e is set
L2 . e is set
card (L3 /\ S) is V21() V22() V23() cardinal set
e is set
f is set
o is Relation-like Function-like set
dom o is set
o is set
f is Relation-like I -defined Function-like V14(I) set
f +* ((I,j),e) is Relation-like I -defined Function-like V14(I) set
(f +* ((I,j),e)) . o is set
f . o is set
L2 . o is set
c28 is Relation-like Function-like set
dom c28 is set
f is Relation-like I -defined Function-like V14(I) set
f +* ((I,j),e) is Relation-like I -defined Function-like V14(I) set
(f +* ((I,j),e)) . o is set
c28 is Relation-like Function-like set
dom c28 is set
L2 . o is set
f is Relation-like I -defined Function-like V14(I) set
f +* ((I,j),e) is Relation-like I -defined Function-like V14(I) set
f is Relation-like I -defined Function-like V14(I) set
f +* ((I,j),e) is Relation-like I -defined Function-like V14(I) set
dom (f +* ((I,j),e)) is set
(f +* ((I,j),e)) . (I,j) is set
o is Relation-like Function-like set
dom o is set
B is Relation-like non-empty I -defined Function-like V14(I) () (I) ManySortedSubset of Carrier A
product B is functional non empty non trivial with_common_domain product-like set
(I,B) is Element of I
(I,A,(I,B)) is non empty () () () () TopStruct
the carrier of (I,A,(I,B)) is non empty set
bool the carrier of (I,A,(I,B)) is non empty set
B . (I,B) is set
dom B is set
dom (Carrier A) is set
l is Element of the carrier of (I,A)
L is Element of the carrier of (I,A)
a is Relation-like Function-like set
dom a is set
L is Relation-like Function-like set
dom L is set
a1 is Relation-like I -defined Function-like V14(I) set
a1 . (I,B) is set
b is Relation-like I -defined Function-like V14(I) set
b . (I,B) is set
b1 is set
a1 . b1 is set
b . b1 is set
a1 . b1 is set
b . b1 is set
(Carrier A) . (I,B) is set
b1 is Element of bool the carrier of (I,A,(I,B))
a is Element of the carrier of (I,A,(I,B))
C is Element of the carrier of (I,A,(I,B))
the topology of (I,A,(I,B)) is non empty Element of bool (bool the carrier of (I,A,(I,B)))
bool (bool the carrier of (I,A,(I,B))) is non empty set
{C,a} is non empty finite countable Element of bool the carrier of (I,A,(I,B))
j is Element of the topology of (I,A,(I,B))
{a1} is Relation-like non-empty I -defined Function-like V14(I) finite-yielding () (I) set
dom {a1} is set
{a1} +* ((I,B),j) is Relation-like I -defined Function-like V14(I) set
dom ({a1} +* ((I,B),j)) is set
Li is set
b . Li is set
({a1} +* ((I,B),j)) . Li is set
a1 . Li is set
{(a1 . Li)} is non empty trivial finite 1 -element countable set
{a1} . Li is finite countable set
Li is set
({a1} +* ((I,B),j)) . Li is set
(Carrier A) . Li is set
a1 . Li is set
o is Element of I
(Carrier A) . o is set
(I,A,o) is non empty () () () () TopStruct
the carrier of (I,A,o) is non empty set
{(a1 . Li)} is non empty trivial finite 1 -element countable set
{a1} . Li is finite countable set
Li is Element of I
({a1} +* ((I,B),j)) . Li is set
{a1} . Li is finite countable set
a1 . Li is set
{(a1 . Li)} is non empty trivial finite 1 -element countable set
Li is set
a1 . Li is set
({a1} +* ((I,B),j)) . Li is set
{(a1 . Li)} is non empty trivial finite 1 -element countable set
{a1} . Li is finite countable set
({a1} +* ((I,B),j)) . (I,B) is set
the topology of (I,A) is non empty Element of bool (bool the carrier of (I,A))
bool (bool the carrier of (I,A)) is non empty set
product ({a1} +* ((I,B),j)) is functional with_common_domain product-like set
dom b is set
Li is Element of the topology of (I,A)
dom a1 is set
{l,L} is non empty finite countable Element of bool the carrier of (I,A)
the topology of (I,A) is non empty Element of bool (bool the carrier of (I,A))
bool (bool the carrier of (I,A)) is non empty set
l is Element of the topology of (I,A)
l /\ S is Element of bool the carrier of (I,A)
card (l /\ S) is V21() V22() V23() cardinal set
L is Relation-like I -defined Function-like V14(I) (I) ManySortedSubset of Carrier A
product L is functional with_common_domain product-like set
a is set
b is set
card l is V21() V22() V23() cardinal set
L is Relation-like non-empty I -defined Function-like V14(I) () (I) ManySortedSubset of Carrier A
dom L is set
(I,L) is Element of I
a is set
L . a is set
B . a is set
(Carrier A) . (I,B) is set
j is Element of I
L . j is set
(I,A,j) is non empty () () () () TopStruct
the topology of (I,A,j) is non empty Element of bool (bool the carrier of (I,A,j))
the carrier of (I,A,j) is non empty set
bool the carrier of (I,A,j) is non empty set
bool (bool the carrier of (I,A,j)) is non empty set
j is Element of I
L . j is set
(I,A,j) is non empty () () () () TopStruct
the topology of (I,A,j) is non empty Element of bool (bool the carrier of (I,A,j))
the carrier of (I,A,j) is non empty set
bool the carrier of (I,A,j) is non empty set
bool (bool the carrier of (I,A,j)) is non empty set
card (L . j) is V21() V22() V23() cardinal set
the topology of (I,A,(I,B)) is non empty Element of bool (bool the carrier of (I,A,(I,B)))
bool (bool the carrier of (I,A,(I,B))) is non empty set
L . (I,B) is set
C is Element of bool the carrier of (I,A,(I,B))
a1 is Relation-like I -defined Function-like V14(I) set
product L is functional non empty non trivial with_common_domain product-like set
a1 . (I,B) is set
b1 is Relation-like I -defined Function-like V14(I) set
b1 . (I,B) is set
Li is Element of the topology of (I,A,(I,B))
Li /\ C is Element of bool the carrier of (I,A,(I,B))
dom a1 is set
o is set
a1 . o is set
b1 . o is set
dom b1 is set
card (Li /\ C) is V21() V22() V23() cardinal set