:: PENCIL_1 semantic presentation

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

{ b

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

{ b

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

{ b

bool { b

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

{ b

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

{ b

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)

{ b

bool { b

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

c

dom c

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

c

dom c

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