:: PENCIL_3 semantic presentation

REAL is set
NAT is non empty V21() V22() V23() non finite cardinal limit_cardinal Element of bool REAL
bool REAL is non empty set
NAT is non empty V21() V22() V23() non finite cardinal limit_cardinal set
bool NAT is non empty non finite set
bool NAT is non empty non finite set
2 is non empty V21() V22() V23() V27() finite cardinal V66() V230() ext-real positive non negative Element of NAT
[:2,2:] is Relation-like non empty set
[:[:2,2:],2:] is Relation-like non empty set
bool [:[:2,2:],2:] is non empty set
K304() is set

1 is non empty V21() V22() V23() V27() finite cardinal V66() V230() ext-real positive non negative Element of NAT

bool is non empty set
K36(K251(),) is set

RAT is set
INT is set
3 is non empty V21() V22() V23() V27() finite cardinal V66() V230() ext-real positive non negative Element of NAT

I is non empty non void TopStruct
the carrier of I is non empty set
[: the carrier of I, the carrier of I:] is Relation-like non empty set
bool [: the carrier of I, the carrier of I:] is non empty set
A is Relation-like the carrier of I -defined the carrier of I -valued Function-like non empty V14( the carrier of I) quasi_total isomorphic Element of bool [: the carrier of I, the carrier of I:]
dom A is non empty Element of bool the carrier of I
bool the carrier of I is non empty set
f is Element of the carrier of I
s is Element of the carrier of I
A . f is Element of the carrier of I
A . s is Element of the carrier of I
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
{f,s} is non empty Element of bool the carrier of I
B is Element of the topology of I
A .: B is Element of the topology of I
{(A . f),(A . s)} is non empty Element of bool the carrier of I
I is non empty set
A is Element of I

f . A is 1-sorted
dom f is non empty Element of bool I
bool I is non empty set
rng f is non empty set

the topology of I is non empty 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 set
f is Element of the topology of I
s is Element of bool the carrier of I
B is Element of the carrier of I

B . 1 is set
len B is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative Element of NAT
B . (len B) is set
rng B is Element of bool (bool the carrier of I)
dom B is Element of bool NAT
(len B) - 1 is V66() V230() ext-real set
p is Element of bool the carrier of I
((len B) - 1) + 1 is V66() V230() ext-real set
i is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative set
B . i is set
i + 1 is non empty V21() V22() V23() V27() finite cardinal V66() V230() ext-real positive non negative Element of NAT
B . (i + 1) is set
(B . i) /\ (B . (i + 1)) is set
card ((B . i) /\ (B . (i + 1))) is V21() V22() V23() cardinal set
(B . i) /\ (B . (len B)) is set
a is set
b1 is Element of the carrier of I
{B,b1} is non empty set
b is Element of the topology of I
I is non empty non void identifying_close_blocks TopStruct
I is non void non degenerated TopStruct
the topology of I is non empty 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
[#] I is non proper Element of bool the carrier of I
f is set
s is Element of the carrier of I
I is non empty set

Segre_Product A is non empty TopStruct
the carrier of () is non empty set

f is Element of the carrier of ()
product () is set
Segre_Blocks A is Element of bool (bool (product ()))
bool (product ()) is non empty set
bool (bool (product ())) is non empty set
TopStruct(# (product ()),() #) is strict TopStruct
dom () is non empty Element of bool I
bool I is non empty set

dom s is set

B is set
B . B is set
() . B is set
I is non empty set

f is Element of I
() . f is set
A . f is 1-sorted
[#] (A . f) is non proper Element of bool the carrier of (A . f)
the carrier of (A . f) is set
bool the carrier of (A . f) is non empty set
s is 1-sorted
the carrier of s is set
I is non empty set
A is Element of I

Segre_Product f is non empty TopStruct
the carrier of () is non empty set
the Element of the carrier of () is Element of the carrier of ()
dom f is non empty Element of bool I
bool I is non empty set
f . A is TopStruct
rng f is non empty set
[#] (f . A) is non proper Element of bool the carrier of (f . A)
the carrier of (f . A) is set
bool the carrier of (f . A) is non empty set

B is non empty non trivial set
i +* (A,B) is Relation-like I -defined Function-like non empty V14(I) set

indx p is Element of I
product p is non empty non trivial set
dom i is non empty Element of bool I
p . A is non empty set
a is set
dom p is non empty Element of bool I

dom b1 is set
dom () is non empty Element of bool I
b is set
b1 . b is set
p . b is set
m is Element of I
() . b is set
m is Element of I
f . m is TopStruct
the carrier of (f . m) is set
b1 . m is set
i . m is set
B . m is set
{(B . m)} is non empty trivial 1 -element set
() . m is set
d1 is non empty non trivial set
[#] (f . m) is non proper Element of bool the carrier of (f . m)
bool the carrier of (f . m) is non empty set
() . b is set
m is Element of I
product () is set
Segre_Blocks f is Element of bool (bool (product ()))
bool (product ()) is non empty set
bool (bool (product ())) is non empty set
TopStruct(# (product ()),() #) is strict TopStruct
I is non empty set
A is Element of I

Segre_Product f is non empty TopStruct
the carrier of () is non empty set

s is Element of the carrier of ()
dom f is non empty Element of bool I
bool I is non empty set
f . A is TopStruct
rng f is non empty set
[#] (f . A) is non proper Element of bool the carrier of (f . A)
the carrier of (f . A) is set
bool the carrier of (f . A) is non empty set

B is non empty non trivial set
i +* (A,B) is Relation-like I -defined Function-like non empty V14(I) set

indx p is Element of I
product p is non empty non trivial set
dom i is non empty Element of bool I
p . A is non empty set
a is set
dom p is non empty Element of bool I

dom b1 is set
dom () is non empty Element of bool I
b is set
b1 . b is set
p . b is set
m is Element of I
() . b is set
m is Element of I
f . m is TopStruct
the carrier of (f . m) is set
b1 . m is set
i . m is set
B . m is set
{(B . m)} is non empty trivial 1 -element set
() . m is set
d1 is non empty non trivial set
[#] (f . m) is non proper Element of bool the carrier of (f . m)
bool the carrier of (f . m) is non empty set
() . b is set
m is Element of I
product () is set
Segre_Blocks f is Element of bool (bool (product ()))
bool (product ()) is non empty set
bool (bool (product ())) is non empty set
TopStruct(# (product ()),() #) is strict TopStruct
a is set
f . a is set
b1 is Element of I
f . b1 is TopStruct
the carrier of (f . b1) is set
b is non empty non trivial set
B . b1 is set
() . b1 is set
[#] (f . b1) is non proper Element of bool the carrier of (f . b1)
bool the carrier of (f . b1) is non empty set
B . a is set
(i +* (A,B)) . a is set
(i +* (A,B)) . a is set
i . a is set
B . a is set
{(B . a)} is non empty trivial 1 -element set
dom B is non empty Element of bool I
dom (i +* (A,B)) is non empty Element of bool I
I is non empty set

product f is non empty non trivial set
indx f is Element of I
f . (indx f) is non empty set
A . (indx f) is TopStruct
[#] (A . (indx f)) is non proper Element of bool the carrier of (A . (indx f))
the carrier of (A . (indx f)) is set
bool the carrier of (A . (indx f)) is non empty set

product s is non empty non trivial set
indx s is Element of I
s . (indx s) is non empty set
A . (indx s) is TopStruct
[#] (A . (indx s)) is non proper Element of bool the carrier of (A . (indx s))
the carrier of (A . (indx s)) is set
bool the carrier of (A . (indx s)) is non empty set
I is non empty set

product f is non empty non trivial set

product s is non empty non trivial set
indx f is Element of I
indx s is Element of I
Segre_Product A is non empty TopStruct
the carrier of () is non empty set
B is Segre-Coset of A
B is Segre-Coset of A
B /\ B is Element of bool the carrier of ()
bool the carrier of () is non empty set
i is set

product a is non empty non trivial set
indx a is Element of I
a . (indx a) is non empty set
A . (indx a) is TopStruct
[#] (A . (indx a)) is non proper Element of bool the carrier of (A . (indx a))
the carrier of (A . (indx a)) is set
bool the carrier of (A . (indx a)) is non empty set

product b1 is non empty non trivial set
indx b1 is Element of I
b1 . (indx b1) is non empty set
A . (indx b1) is TopStruct
[#] (A . (indx b1)) is non proper Element of bool the carrier of (A . (indx b1))
the carrier of (A . (indx b1)) is set
bool the carrier of (A . (indx b1)) is non empty set
dom f is non empty Element of bool I
bool I is non empty set
dom s is non empty Element of bool I
b is set
m is Element of I
f . b is set
s . b is set
m is Element of I
f . m is non empty set
d1 is set
{d1} is non empty trivial 1 -element set
s . m is non empty set
j is set
{j} is non empty trivial 1 -element set

p . m is set
f . b is set
s . b is set
m is Element of I
I is non empty set

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

indx f is Element of I

the topology of (A . (indx f)) is non empty Element of bool (bool the carrier of (A . (indx f)))
the carrier of (A . (indx f)) is non empty set
bool the carrier of (A . (indx f)) is non empty set
bool (bool the carrier of (A . (indx f))) is non empty set
s is Element of the topology of (A . (indx f))
f +* ((indx f),s) is Relation-like I -defined Function-like non empty V14(I) set
product (f +* ((indx f),s)) is set
B is Element of I
B is Element of bool the carrier of (A . (indx f))
f +* ((indx f),B) is Relation-like I -defined Function-like non empty V14(I) set
(f +* ((indx f),B)) . B is set
f . B is non empty set
card s is V21() V22() V23() cardinal set

indx B is Element of I
B . (indx B) is non empty set
dom f is non empty Element of bool I
bool I is non empty set
I is non empty set

f is Element of I

the carrier of (A . f) is non empty set
s is Element of the carrier of (A . f)
{s} is non empty trivial 1 -element Element of bool the carrier of (A . f)
bool the carrier of (A . f) is non empty set

indx B is Element of I
B +* (f,{s}) is Relation-like I -defined Function-like non empty V14(I) set
dom B is non empty Element of bool I
bool I is non empty set
B is Element of I
(B +* (f,{s})) . B is set
(B +* (f,{s})) . B is set
B . B is non empty set
B is set
(B +* (f,{s})) . B is set
() . B is set
i is Element of I
(B +* (f,{s})) . i is set

[#] (A . i) is non empty non proper Element of bool the carrier of (A . i)
the carrier of (A . i) is non empty set
bool the carrier of (A . i) is non empty set
(B +* (f,{s})) . i is set
B . i is non empty set
(B +* (f,{s})) . (indx B) is set
B . (indx B) is non empty set
dom (B +* (f,{s})) is non empty Element of bool I
rng (B +* (f,{s})) is non empty set
I is non empty set

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

the carrier of (A . f) is non empty set
bool the carrier of (A . f) is non empty set
s is Element of bool the carrier of (A . f)

B +* (f,s) is Relation-like I -defined Function-like non empty V14(I) set
product (B +* (f,s)) is set
dom (B +* (f,s)) is non empty Element of bool I
bool I is non empty set
dom () is non empty Element of bool I
B is set
dom B is non empty Element of bool I
(B +* (f,s)) . B is set
[#] (A . f) is non empty non proper Element of bool the carrier of (A . f)
() . B is set
(B +* (f,s)) . B is set
B . B is set
() . B is set
product () is set
Segre_Blocks A is Element of bool (bool (product ()))
bool (product ()) is non empty set
bool (bool (product ())) is non empty set
TopStruct(# (product ()),() #) is strict TopStruct
I is non empty set

f is Element of I
{A} . f is set
A . f is set
{(A . f)} is non empty trivial 1 -element set
I is non empty set
A is Element of I

the topology of (f . A) is non empty Element of bool (bool the carrier of (f . A))
the carrier of (f . A) is non empty set
bool the carrier of (f . A) is non empty set
bool (bool the carrier of (f . A)) is non empty set

the topology of () is non empty Element of bool (bool the carrier of ())
the carrier of () is non empty set
bool the carrier of () is non empty set
bool (bool the carrier of ()) is non empty set
s is Element of the topology of (f . A)

{B} +* (A,s) is Relation-like I -defined Function-like non empty V14(I) set
product ({B} +* (A,s)) is set
p is Element of I
i is Element of bool the carrier of (f . A)
{B} +* (A,i) is Relation-like I -defined Function-like non empty V14(I) set
({B} +* (A,i)) . p is set
{B} . p is set
card s is V21() V22() V23() cardinal set

B +* (A,i) is Relation-like I -defined Function-like non empty V14(I) set

indx p is Element of I
p . (indx p) is non empty set
dom {B} is non empty Element of bool I
bool I is non empty set
I is non empty set

the carrier of () is non empty set
f is Element of the carrier of ()
s is Element of the carrier of ()
the topology of () is non empty Element of bool (bool the carrier of ())
bool the carrier of () is non empty set
bool (bool the carrier of ()) is non empty set
{f,s} is non empty Element of bool the carrier of ()
B is Element of the topology of ()

product p is non empty non trivial set
indx p is Element of I
p . (indx p) is non empty set

the topology of (A . (indx p)) is non empty Element of bool (bool the carrier of (A . (indx p)))
the carrier of (A . (indx p)) is non empty set
bool the carrier of (A . (indx p)) is non empty set
bool (bool the carrier of (A . (indx p))) is non empty set
a is Element of I

the carrier of (A . a) is non empty set
B . a is set
i . a is set
b is Element of the carrier of (A . a)
m is Element of the carrier of (A . a)
dom p is non empty Element of bool I
bool I is non empty set
d1 is set
dom B is non empty Element of bool I
j is Element of I
B . d1 is set
i . d1 is set
j is Element of I
p . j is non empty set
c2 is set
{c2} is non empty trivial 1 -element set
B . d1 is set

dom o is set
i . d1 is set

dom o is set

dom p0 is set
j is Element of I
dom i is non empty Element of bool I
b1 is Element of the topology of (A . (indx p))

dom d1 is set

dom d1 is set
{b,m} is non empty Element of bool the carrier of (A . a)
bool the carrier of (A . a) is non empty set
b1 is Element of I
B . b1 is set
i . b1 is set

i is Element of I

the carrier of (A . i) is non empty set
B . i is set
B . i is set
() . i is set
[#] (A . i) is non empty non proper Element of bool the carrier of (A . i)
bool the carrier of (A . i) is non empty set
a is Element of the carrier of (A . i)
p is Element of the carrier of (A . i)
the topology of (A . i) is non empty Element of bool (bool the carrier of (A . i))
bool (bool the carrier of (A . i)) is non empty set
{a,p} is non empty Element of bool the carrier of (A . i)
b1 is Element of the topology of (A . i)
b1 is Element of the topology of (A . i)
the topology of () is non empty Element of bool (bool the carrier of ())
bool the carrier of () is non empty set
bool (bool the carrier of ()) is non empty set

{B} +* (i,b1) is Relation-like I -defined Function-like non empty V14(I) set
product ({B} +* (i,b1)) is set
dom ({B} +* (i,b1)) is non empty Element of bool I
bool I is non empty set
dom {B} is non empty Element of bool I
m is set
B . m is set
({B} +* (i,b1)) . m is set
d1 is Element of I
d1 is Element of I
{B} . m is set
B . m is set
{(B . m)} is non empty trivial 1 -element set
B . d1 is set
{(B . d1)} is non empty trivial 1 -element set
d1 is Element of I
m is set
B . m is set
({B} +* (i,b1)) . m is set
{B} . m is set
{(B . m)} is non empty trivial 1 -element set
dom B is non empty Element of bool I
b is Element of the topology of ()
dom B is non empty Element of bool I
{f,s} is non empty Element of bool the carrier of ()
the topology of (A . i) is non empty Element of bool (bool the carrier of (A . i))
bool (bool the carrier of (A . i)) is non empty set
{a,p} is non empty Element of bool the carrier of (A . i)
I is non empty set

indx f is Element of I

the carrier of (A . (indx f)) is non empty set
product f is non empty non trivial set
B is Element of the carrier of (A . (indx f))
{B} is non empty trivial 1 -element Element of bool the carrier of (A . (indx f))
bool the carrier of (A . (indx f)) is non empty set
f +* ((indx f),{B}) is Relation-like I -defined Function-like non empty V14(I) set
product (f +* ((indx f),{B})) is set
B is set
dom f is non empty Element of bool I
bool I is non empty set

dom p is set

p +* ((indx f),B) is Relation-like I -defined Function-like non empty V14(I) set
{(p +* ((indx f),B))} is functional non empty trivial 1 -element set
i +* ((indx f),B) is Relation-like I -defined Function-like non empty V14(I) set
b1 is set
dom (f +* ((indx f),{B})) is non empty Element of bool I
dom i is non empty Element of bool I
(i +* ((indx f),B)) . b1 is set
(f +* ((indx f),{B})) . b1 is set
(i +* ((indx f),B)) . b1 is set
i . b1 is set
f . b1 is set
(f +* ((indx f),{B})) . b1 is set
b1 is set
dom (i +* ((indx f),B)) is non empty Element of bool I
b1 is set
dom (f +* ((indx f),{B})) is non empty Element of bool I

dom b is set
m is set
b . m is set
(f +* ((indx f),{B})) . m is set
d1 is Element of I
(i +* ((indx f),B)) . m is set

dom j is set
d1 is Element of I
f . d1 is non empty set
f . m is set
j is set
{j} is non empty trivial 1 -element set
(i +* ((indx f),B)) . m is set
i . m is set

dom c2 is set
d1 is Element of I
dom (i +* ((indx f),B)) is non empty Element of bool I
I is non empty finite set

{ b1 where b1 is Element of I : not A . b1 = f . b1 } is set
card { b1 where b1 is Element of I : not A . b1 = f . b1 } is V21() V22() V23() cardinal set
s is set
B is Element of I
A . B is set
f . B is set
s is finite set
card s is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative Element of NAT
I is non empty finite set

(I,A,f) is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative set
{ b1 where b1 is Element of I : not A . b1 = f . b1 } is set
card { b1 where b1 is Element of I : not A . b1 = f . b1 } is V21() V22() V23() cardinal set
s is Element of I
A . s is set
f . s is set
f +* (s,(A . s)) is Relation-like I -defined Function-like non empty V14(I) V259() set
(I,A,(f +* (s,(A . s)))) is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative set
{ b1 where b1 is Element of I : not A . b1 = (f +* (s,(A . s))) . b1 } is set
card { b1 where b1 is Element of I : not A . b1 = (f +* (s,(A . s))) . b1 } is V21() V22() V23() cardinal set
(I,A,(f +* (s,(A . s)))) + 1 is non empty V21() V22() V23() V27() finite cardinal V66() V230() ext-real positive non negative Element of NAT
B is set
i is Element of I
A . i is set
f . i is set
i is set
p is Element of I
A . p is set
(f +* (s,(A . s))) . p is set
B is finite set
i is finite set
{s} is non empty trivial 1 -element Element of bool I
bool I is non empty set
i \/ {s} is non empty set
p is set
a is Element of I
A . a is set
f . a is set
(f +* (s,(A . s))) . a is set
p is set
a is Element of I
A . a is set
(f +* (s,(A . s))) . a is set
f . a is set
dom f is non empty Element of bool I
p is Element of I
A . p is set
(f +* (s,(A . s))) . p is set
I is non empty set

I is non empty set

the carrier of () is non empty set
[: the carrier of (), the carrier of ():] is Relation-like non empty set
bool [: the carrier of (), the carrier of ():] is non empty set
f is Segre-Coset of A
s is Segre-Coset of A
B is Relation-like the carrier of () -defined the carrier of () -valued Function-like non empty V14( the carrier of ()) quasi_total isomorphic Element of bool [: the carrier of (), the carrier of ():]
B .: f is Element of bool the carrier of ()
bool the carrier of () is non empty set
B .: s is Element of bool the carrier of ()
B is Segre-Coset of A
i is Segre-Coset of A
p is Element of the carrier of ()
dom B is non empty Element of bool the carrier of ()
a is set
B . a is set
b1 is Element of the carrier of ()
b is Element of the carrier of ()
B . b is Element of the carrier of ()
m is Element of the carrier of ()
the topology of () is non empty Element of bool (bool the carrier of ())
bool (bool the carrier of ()) is non empty set
{b1,b} is non empty Element of bool the carrier of ()
d1 is Element of the topology of ()
B .: d1 is Element of the topology of ()
j is Element of the topology of ()
{p,m} is non empty Element of bool the carrier of ()
I is non empty set

f is Segre-Coset of A
s is Segre-Coset of A

product B is non empty non trivial set
indx B is Element of I
B . (indx B) is non empty set

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

product B is non empty non trivial set
indx B is Element of I
B . (indx B) is non empty set

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

product i is non empty non trivial set
indx i is Element of I
i . (indx i) is non empty set

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

product p is non empty non trivial set

product a is non empty non trivial set
indx p is Element of I
indx a is Element of I
a . (indx p) is non empty set
b1 is set
{b1} is non empty trivial 1 -element set

the topology of (A . (indx p)) is non empty Element of bool (bool the carrier of (A . (indx p)))
the carrier of (A . (indx p)) is non empty set
bool the carrier of (A . (indx p)) is non empty set
bool (bool the carrier of (A . (indx p))) is non empty set
the Element of the topology of (A . (indx p)) is Element of the topology of (A . (indx p))
m is set

the carrier of () is non empty set
d1 is Element of the carrier of ()
card the Element of the topology of (A . (indx p)) is V21() V22() V23() cardinal set
card the carrier of (A . (indx p)) is non empty V21() V22() V23() cardinal set
c2 is set

o is Element of the carrier of (A . (indx p))
j +* ((indx p),o) is Relation-like I -defined Function-like non empty V14(I) set
p0 is Element of the carrier of ()

dom u is non empty Element of bool I
bool I is non empty set
dom p is non empty Element of bool I
p1 is set
dom j is non empty Element of bool I
u . p1 is set
p . p1 is set
u . p1 is set
j . p1 is set
p . p1 is set

dom p is set
p1 is Element of the carrier of ()
f /\ s is Element of bool the carrier of ()
bool the carrier of () is non empty set

q is Element of I

the carrier of (A . q) is non empty set
u . q is set
p . q is set
dom p is non empty Element of bool I
q1 is set
c1 is Element of I
p . c1 is set
() . c1 is set

the carrier of (A . c1) is non empty set
[#] (A . c1) is non empty non proper Element of bool the carrier of (A . c1)
bool the carrier of (A . c1) is non empty set
p . q1 is set
p . q1 is set
dom a is non empty Element of bool I
p . (indx p) is set

dom c1 is set
u . (indx p) is set
c1 is Element of I
p . c1 is set
u . c1 is set
u . q1 is set
j . q1 is set
p . q1 is set
p . q1 is set

dom c1 is set
f /\ s is Element of bool the carrier of ()
bool the carrier of () is non empty set
b1 is set

the carrier of () is non empty set
b is Element of the carrier of ()
m is Element of the carrier of ()
f /\ s is Element of bool the carrier of ()
bool the carrier of () is non empty set

d1 is Relation-like I -defined Function-like non empty V14(I) Element of Carrier A
c2 is Element of I

the carrier of (A . c2) is non empty set
j . c2 is set
d1 . c2 is set
p . c2 is non empty set
a . c2 is non empty set
o is set
dom p is non empty Element of bool I
bool I is non empty set
p0 is Element of I
d1 . p0 is set
() . p0 is set

the carrier of (A . p0) is non empty set
[#] (A . p0) is non empty non proper Element of bool the carrier of (A . p0)
bool the carrier of (A . p0) is non empty set
d1 . o is set
p . o is set
p0 is Element of I
p . p0 is non empty set
u is set
{u} is non empty trivial 1 -element set
j . p0 is set
d1 . p0 is set
d1 . o is set
p . o is set
p0 is Element of I
dom d1 is non empty Element of bool I
o is Element of I
p . o is non empty set
a . o is non empty set
dom a is non empty Element of bool I
d1 . o is set
p0 is set
{p0} is non empty trivial 1 -element set
j . o is set
u is set
{u} is non empty trivial 1 -element set
o is Element of the carrier of (A . c2)
{o} is non empty trivial 1 -element Element of bool the carrier of (A . c2)
bool the carrier of (A . c2) is non empty set
p0 is Element of the carrier of (A . c2)
{p0} is non empty trivial 1 -element Element of bool the carrier of (A . c2)
dom B is non empty Element of bool I
dom i is non empty Element of bool I

product B is non empty non trivial set
indx B is Element of I
B . (indx B) is non empty set

[#] (A . (indx B)) is non empty non proper Element of bool the carrier of (A . (indx B))
the carrier of (A . (indx B)) is non empty set
bool the carrier of (A . (indx B)) is non empty set
i is Element of I

the carrier of (A . i) is non empty set
B . i is non empty set
B . i is non empty set
p is set
{p} is non empty trivial 1 -element set
() . i is set
[#] (A . i) is non empty non proper Element of bool the carrier of (A . i)
bool the carrier of (A . i) is non empty set
b1 is set
{b1} is non empty trivial 1 -element set
b is Element of the carrier of (A . i)
a is Element of the carrier of (A . i)
m is set
dom B is non empty Element of bool I
bool I is non empty set
d1 is Element of I
B . m is set
B . m is set
d1 is Element of I
B . m is set
B . m is set
d1 is Element of I
dom B is non empty Element of bool I

the carrier of () is non empty set
f /\ f is Element of bool the carrier of ()
bool the carrier of () is non empty set
the topology of (A . i) is non empty Element of bool (bool the carrier of (A . i))
bool (bool the carrier of (A . i)) is non empty set
{b,a} is non empty Element of bool the carrier of (A . i)
m is Element of the topology of (A . i)
d1 is Element of the carrier of ()

j +* (i,a) is Relation-like I -defined Function-like non empty V14(I) set
c2 is Element of the carrier of ()
p0 is set
u is Element of I
dom j is non empty Element of bool I

o . p0 is set
B . p0 is set
u is Element of I
dom j is non empty Element of bool I

o . u is set
j . u is set
B . u is non empty set

dom p1 is set
o . p0 is set
B . p0 is set
u is Element of I

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

{j} +* (i,m) is Relation-like I -defined Function-like non empty V14(I) set
product ({j} +* (i,m)) is set
u is set
dom {j} is non empty Element of bool I
dom j is non empty Element of bool I
o . u is set
({j} +* (i,m)) . u is set
{j} . u is set
({j} +* (i,m)) . u is set
j . u is set
{(j . u)} is non empty trivial 1 -element set
o . u is set
dom ({j} +* (i,m)) is non empty Element of bool I
p0 is Element of the topology of ()
u is set
j . u is set
B . u is set

dom p1 is set
({j} +* (i,m)) . u is set
{j} . u is set
({j} +* (i,m)) . u is set
j . u is set
{(j . u)} is non empty trivial 1 -element set
{d1,c2} is non empty Element of bool the carrier of ()
I is non empty finite set

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

the carrier of (A . f) is non empty set
s is Element of the carrier of (A . f)
{s} is non empty trivial 1 -element Element of bool the carrier of (A . f)
bool the carrier of (A . f) is non empty set

product B is non empty non trivial set

B +* (f,{s}) is Relation-like I -defined Function-like non empty V14(I) V259() set
B . f is non empty set
product B is non empty non trivial set
indx B is Element of I
[#] (A . f) is non empty non proper Element of bool the carrier of (A . f)
i is set
{i} is non empty trivial 1 -element set
() . f is set
p is Element of the carrier of (A . f)
a is Relation-like NAT -defined the carrier of (A . f) -valued Function-like finite FinSequence-like FinSubsequence-like V259() FinSequence of the carrier of (A . f)
a . 1 is set
len a is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative Element of NAT
a . (len a) is set
b1 is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative Element of NAT
b is set
a . b1 is set
m is set
b1 + 1 is non empty V21() V22() V23() V27() finite cardinal V66() V230() ext-real positive non negative Element of NAT
a . (b1 + 1) is set
d1 is Element of the carrier of (A . f)
j is Element of the carrier of (A . f)
rng a is Element of bool the carrier of (A . f)
b1 is Relation-like NAT -defined the carrier of (A . f) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like V259() FinSequence of the carrier of (A . f)
b1 . 1 is set
len b1 is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative Element of NAT
b1 . (len b1) is set
rng b1 is Element of bool the carrier of (A . f)
dom b1 is Element of bool NAT

len b is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative Element of NAT
dom b is Element of bool NAT
rng b is set
m is set
d1 is set
b . d1 is set
j is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative Element of NAT
b1 . j is set
{(b1 . j)} is non empty trivial 1 -element set
B +* (f,{(b1 . j)}) is Relation-like I -defined Function-like non empty V14(I) V259() set
product (B +* (f,{(b1 . j)})) is set
b . j is set

m . 1 is set
len m is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative Element of NAT
m . (len m) is set
dom m is Element of bool NAT
Seg (len b1) is finite len b1 -element Element of bool NAT
{(b1 . (len b1))} is non empty trivial 1 -element set
B +* (f,{(b1 . (len b1))}) is Relation-like I -defined Function-like non empty V14(I) V259() set
product (B +* (f,{(b1 . (len b1))})) is set
d1 is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative set
m . d1 is set
b1 . d1 is set
j is Element of the carrier of (A . f)
{j} is non empty trivial 1 -element Element of bool the carrier of (A . f)
B +* (f,{j}) is Relation-like I -defined Function-like non empty V14(I) V259() set

c2 . (indx B) is non empty set
B . (indx B) is non empty set
indx c2 is Element of I
c2 . (indx c2) is non empty set

[#] (A . (indx c2)) is non empty non proper Element of bool the carrier of (A . (indx c2))
the carrier of (A . (indx c2)) is non empty set
bool the carrier of (A . (indx c2)) is non empty set
product c2 is non empty non trivial set
dom B is non empty Element of bool I
bool I is non empty set
d1 is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative set
m . d1 is set
d1 + 1 is non empty V21() V22() V23() V27() finite cardinal V66() V230() ext-real positive non negative Element of NAT
m . (d1 + 1) is set
j is Segre-Coset of A
c2 is Segre-Coset of A
o is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative Element of NAT
b1 . o is set
p0 is Element of the carrier of (A . f)
{p0} is non empty trivial 1 -element Element of bool the carrier of (A . f)
B +* (f,{p0}) is Relation-like I -defined Function-like non empty V14(I) V259() set
m . o is set

product u is non empty non trivial set
o + 1 is non empty V21() V22() V23() V27() finite cardinal V66() V230() ext-real positive non negative Element of NAT
b1 . (o + 1) is set
p1 is Element of the carrier of (A . f)
{p1} is non empty trivial 1 -element Element of bool the carrier of (A . f)
B +* (f,{p1}) is Relation-like I -defined Function-like non empty V14(I) V259() set
m . (o + 1) is set

product p is non empty non trivial set
j /\ c2 is Element of bool the carrier of ()
q is set
{(b1 . (o + 1))} is non empty trivial 1 -element set
B +* (f,{(b1 . (o + 1))}) is Relation-like I -defined Function-like non empty V14(I) V259() set
dom (B +* (f,{(b1 . (o + 1))})) is non empty Element of bool I

dom q1 is set
q1 . f is set
(B +* (f,{(b1 . (o + 1))})) . f is set
{(b1 . o)} is non empty trivial 1 -element set
B +* (f,{(b1 . o)}) is Relation-like I -defined Function-like non empty V14(I) V259() set
dom (B +* (f,{(b1 . o)})) is non empty Element of bool I

dom c1 is set
c1 . f is set
(B +* (f,{(b1 . o)})) . f is set

product q is non empty non trivial set

product q1 is non empty non trivial set
{(b1 . (o + 1))} is non empty trivial 1 -element set
B +* (f,{(b1 . (o + 1))}) is Relation-like I -defined Function-like non empty V14(I) V259() set
q1 . (indx B) is non empty set
B . (indx B) is non empty set
{(b1 . o)} is non empty trivial 1 -element set
B +* (f,{(b1 . o)}) is Relation-like I -defined Function-like non empty V14(I) V259() set
q . (indx B) is non empty set
indx q is Element of I
indx q1 is Element of I
c1 is Element of I
c1 is Element of I
q . c1 is non empty set
q1 . c1 is non empty set
B . c1 is non empty set

the carrier of (A . c1) is non empty set
q . c1 is non empty set
q1 . c1 is non empty set
c1 is Element of the carrier of (A . c1)
{c1} is non empty trivial 1 -element Element of bool the carrier of (A . c1)
bool the carrier of (A . c1) is non empty set
c2 is Element of the carrier of (A . c1)
{c2} is non empty trivial 1 -element Element of bool the carrier of (A . c1)
I is non empty finite set

the carrier of () is non empty set
bool the carrier of () is non empty set
f is Segre-Coset of A
s is Segre-Coset of A

product B is non empty non trivial set

product B is non empty non trivial set
indx B is Element of I
indx B is Element of I
i is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative set
i + 1 is non empty V21() V22() V23() V27() finite cardinal V66() V230() ext-real positive non negative Element of NAT

indx p is Element of I

indx a is Element of I
product p is non empty non trivial set
product a is non empty non trivial set
(I,p,a) is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative set
{ b1 where b1 is Element of I : not p . b1 = a . b1 } is set
card { b1 where b1 is Element of I : not p . b1 = a . b1 } is V21() V22() V23() cardinal set
b1 is set
b is Element of I
p . b is non empty set
a . b is non empty set
a . (indx p) is non empty set

[#] (A . (indx p)) is non empty non proper Element of bool the carrier of (A . (indx p))
the carrier of (A . (indx p)) is non empty set
bool the carrier of (A . (indx p)) is non empty set
m is set
{m} is non empty trivial 1 -element set
() . b is set

[#] (A . b) is non empty non proper Element of bool the carrier of (A . b)
the carrier of (A . b) is non empty set
bool the carrier of (A . b) is non empty set
d1 is Element of the carrier of (A . b)
{d1} is non empty trivial 1 -element Element of bool the carrier of (A . b)
a +* (b,{d1}) is Relation-like I -defined Function-like non empty V14(I) V259() set

j . (indx p) is non empty set
indx j is Element of I
product j is non empty non trivial set
(I,p,j) is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative set
{ b1 where b1 is Element of I : not p . b1 = j . b1 } is set
card { b1 where b1 is Element of I : not p . b1 = j . b1 } is V21() V22() V23() cardinal set
(I,p,j) + 1 is non empty V21() V22() V23() V27() finite cardinal V66() V230() ext-real positive non negative Element of NAT

c2 . 1 is set
len c2 is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative Element of NAT
c2 . (len c2) is set
dom c2 is Element of bool NAT
o is set
{o} is non empty trivial 1 -element set

o . 1 is set
len o is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative Element of NAT
o . (len o) is set
dom o is Element of bool NAT
dom a is non empty Element of bool I
bool I is non empty set
j . b is non empty set

p0 . 1 is set
len p0 is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative Element of NAT
p0 . (len p0) is set
dom p0 is Element of bool NAT
u is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative set
p0 . u is set
rng p0 is Element of bool (bool the carrier of ())
bool (bool the carrier of ()) is non empty set
rng c2 is Element of bool (bool the carrier of ())
rng o is Element of bool (bool the carrier of ())
(rng c2) \/ (rng o) is Element of bool (bool the carrier of ())
p1 is set
c2 . p1 is set
p1 is set
o . p1 is set
u is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative set
p0 . u is set
u + 1 is non empty V21() V22() V23() V27() finite cardinal V66() V230() ext-real positive non negative Element of NAT
p0 . (u + 1) is set
p1 is Segre-Coset of A
p is Segre-Coset of A
q is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative Element of NAT
q + 1 is non empty V21() V22() V23() V27() finite cardinal V66() V230() ext-real positive non negative Element of NAT
c2 . (q + 1) is set
c2 . q is set
q is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative Element of NAT
q1 is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative set
(len c2) + q1 is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative Element of NAT
c1 is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative Element of NAT
(len p0) + 1 is non empty V21() V22() V23() V27() finite cardinal V66() V230() ext-real positive non negative Element of NAT
(len c2) + c1 is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative Element of NAT
((len c2) + c1) + 1 is non empty V21() V22() V23() V27() finite cardinal V66() V230() ext-real positive non negative Element of NAT
(len c2) + (len o) is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative Element of NAT
c1 + 1 is non empty V21() V22() V23() V27() finite cardinal V66() V230() ext-real positive non negative Element of NAT
(len c2) + (c1 + 1) is non empty V21() V22() V23() V27() finite cardinal V66() V230() ext-real positive non negative Element of NAT
p0 . ((len c2) + (c1 + 1)) is set
(c1 + 1) + 1 is non empty V21() V22() V23() V27() finite cardinal V66() V230() ext-real positive non negative Element of NAT
o . ((c1 + 1) + 1) is set
{} + 1 is non empty V21() V22() V23() V27() finite cardinal V66() V230() ext-real positive non negative Element of NAT
o . (c1 + 1) is set
c1 is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative Element of NAT
1 + 1 is non empty V21() V22() V23() V27() finite cardinal V66() V230() ext-real positive non negative Element of NAT
o . (1 + 1) is set
c1 is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative Element of NAT
q is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative Element of NAT
c2 is set
{c2} is non empty trivial 1 -element set

indx i is Element of I

indx p is Element of I
product i is non empty non trivial set
product p is non empty non trivial set
(I,i,p) is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative set
{ b1 where b1 is Element of I : not i . b1 = p . b1 } is set
card { b1 where b1 is Element of I : not i . b1 = p . b1 } is V21() V22() V23() cardinal set
a is set
dom i is non empty Element of bool I
bool I is non empty set
i . a is set
p . a is set
b1 is Element of I
dom p is non empty Element of bool I
(I,B,B) is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative set
{ b1 where b1 is Element of I : not B . b1 = B . b1 } is set
card { b1 where b1 is Element of I : not B . b1 = B . b1 } is V21() V22() V23() cardinal set

indx i is Element of I

indx p is Element of I
product i is non empty non trivial set
product p is non empty non trivial set
(I,i,p) is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative set
{ b1 where b1 is Element of I : not i . b1 = p . b1 } is set
card { b1 where b1 is Element of I : not i . b1 = p . b1 } is V21() V22() V23() cardinal set

i . 1 is set
len i is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative Element of NAT
i . (len i) is set
dom i is Element of bool NAT
p is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative set
i . p is set
a is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative set
b1 is Segre-Coset of A
i . a is set
b is Segre-Coset of A
a + 1 is non empty V21() V22() V23() V27() finite cardinal V66() V230() ext-real positive non negative Element of NAT
i . (a + 1) is set

i . 1 is set
len i is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative Element of NAT
i . (len i) is set
dom i is Element of bool NAT
p is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative set
i . p is set
p + 1 is non empty V21() V22() V23() V27() finite cardinal V66() V230() ext-real positive non negative Element of NAT
i . (p + 1) is set

product a is non empty non trivial set
indx a is Element of I
{} + 1 is non empty V21() V22() V23() V27() finite cardinal V66() V230() ext-real positive non negative Element of NAT
b1 is Segre-Coset of A

product m is non empty non trivial set
indx m is Element of I
m . (indx m) is non empty set

[#] (A . (indx m)) is non empty non proper Element of bool the carrier of (A . (indx m))
the carrier of (A . (indx m)) is non empty set
bool the carrier of (A . (indx m)) is non empty set
b is Segre-Coset of A
i . {} is set

product p is non empty non trivial set
indx p is Element of I
I is non empty finite set

the carrier of () is non empty set
[: the carrier of (), the carrier of ():] is Relation-like non empty set
bool [: the carrier of (), the carrier of ():] is non empty set

f is Element of I

f is Relation-like the carrier of () -defined the carrier of () -valued Function-like non empty V14( the carrier of ()) quasi_total isomorphic Element of bool [: the carrier of (), the carrier of ():]
s is Segre-Coset of A
B is Segre-Coset of A
f .: s is Element of bool the carrier of ()
bool the carrier of () is non empty set
f .: B is Element of bool the carrier of ()

product B is non empty non trivial set

product i is non empty non trivial set

product p is non empty non trivial set