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

{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty trivial V21() V22() V23() V25() V26() V27() finite cardinal {} -element V66() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V230() ext-real non positive non negative V258() V259() set

the Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty trivial V21() V22() V23() V25() V26() V27() finite cardinal {} -element V66() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V230() ext-real non positive non negative V258() V259() set is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty trivial V21() V22() V23() V25() V26() V27() finite cardinal {} -element V66() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V230() ext-real non positive non negative V258() V259() set

{{}} is functional non empty trivial 1 -element set

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

K251({{}}) is functional non empty FinSequence-membered M17({{}})

[:K251({{}}),{{}}:] is Relation-like non empty set

bool [:K251({{}}),{{}}:] is non empty set

K36(K251({{}}),{{}}) is set

COMPLEX 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

0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty trivial V21() V22() V23() V25() V26() V27() finite cardinal {} -element V66() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V230() ext-real non positive non negative V258() V259() 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 is Relation-like I -defined Function-like non empty V14(I) 1-sorted-yielding non-Empty non-Trivial-yielding set

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

I is non void identifying_close_blocks 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 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 is Relation-like NAT -defined bool the carrier of I -valued Function-like finite FinSequence-like FinSubsequence-like V259() FinSequence of bool 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

A is Relation-like I -defined Function-like non empty V14(I) 1-sorted-yielding non-Empty TopStruct-yielding set

Segre_Product A is non empty TopStruct

the carrier of (Segre_Product A) is non empty set

Carrier A is Relation-like I -defined Function-like non empty V14(I) set

f is Element of the carrier of (Segre_Product A)

product (Carrier A) is set

Segre_Blocks 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)),(Segre_Blocks A) #) is strict TopStruct

dom (Carrier A) is non empty Element of bool I

bool I is non empty set

s is Relation-like Function-like set

dom s is set

B is Relation-like I -defined Function-like non empty V14(I) set

B is set

B . B is set

(Carrier A) . B is set

I is non empty set

A is Relation-like I -defined Function-like non empty V14(I) 1-sorted-yielding set

Carrier A is Relation-like I -defined Function-like non empty V14(I) set

f is Element of I

(Carrier A) . 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

f is Relation-like I -defined Function-like non empty V14(I) 1-sorted-yielding non-Empty TopStruct-yielding non-Trivial-yielding set

Carrier f is Relation-like I -defined Function-like non empty V14(I) set

Segre_Product f is non empty TopStruct

the carrier of (Segre_Product f) is non empty set

the Element of the carrier of (Segre_Product f) is Element of the carrier of (Segre_Product f)

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 Relation-like I -defined Function-like non empty V14(I) Element of Carrier f

{B} is Relation-like I -defined Function-like non empty V14(I) trivial-yielding Segre-like set

i is Relation-like I -defined Function-like non empty V14(I) ManySortedSubset of Carrier f

B is non empty non trivial set

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

p is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like ManySortedSubset of Carrier f

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

b1 is Relation-like Function-like set

dom b1 is set

dom (Carrier f) is non empty Element of bool I

b is set

b1 . b is set

p . b is set

m is Element of I

(Carrier f) . 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

(Carrier f) . 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

(Carrier f) . b is set

m is Element of I

product (Carrier f) is set

Segre_Blocks f is Element of bool (bool (product (Carrier f)))

bool (product (Carrier f)) is non empty set

bool (bool (product (Carrier f))) is non empty set

TopStruct(# (product (Carrier f)),(Segre_Blocks f) #) is strict TopStruct

I is non empty set

A is Element of I

f is Relation-like I -defined Function-like non empty V14(I) 1-sorted-yielding non-Empty TopStruct-yielding non-Trivial-yielding set

Segre_Product f is non empty TopStruct

the carrier of (Segre_Product f) is non empty set

Carrier f is Relation-like I -defined Function-like non empty V14(I) set

s is Element of the carrier of (Segre_Product f)

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 Relation-like I -defined Function-like non empty V14(I) Element of Carrier f

{B} is Relation-like I -defined Function-like non empty V14(I) trivial-yielding Segre-like set

i is Relation-like I -defined Function-like non empty V14(I) ManySortedSubset of Carrier f

B is non empty non trivial set

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

p is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like ManySortedSubset of Carrier f

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

b1 is Relation-like Function-like set

dom b1 is set

dom (Carrier f) is non empty Element of bool I

b is set

b1 . b is set

p . b is set

m is Element of I

(Carrier f) . 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

(Carrier f) . 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

(Carrier f) . b is set

m is Element of I

product (Carrier f) is set

Segre_Blocks f is Element of bool (bool (product (Carrier f)))

bool (product (Carrier f)) is non empty set

bool (bool (product (Carrier f))) is non empty set

TopStruct(# (product (Carrier f)),(Segre_Blocks f) #) 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

(Carrier f) . 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

A is Relation-like I -defined Function-like non empty V14(I) 1-sorted-yielding non-Empty TopStruct-yielding non-Trivial-yielding set

Carrier A is Relation-like I -defined Function-like non empty V14(I) set

f is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like ManySortedSubset of Carrier A

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

s is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like ManySortedSubset of Carrier A

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

A is Relation-like I -defined Function-like non empty V14(I) 1-sorted-yielding non-Empty TopStruct-yielding non-Trivial-yielding set

Carrier A is Relation-like I -defined Function-like non empty V14(I) set

f is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like ManySortedSubset of Carrier A

product f is non empty non trivial set

s is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like ManySortedSubset of Carrier A

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 (Segre_Product A) 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 (Segre_Product A)

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

i is set

a is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like ManySortedSubset of Carrier A

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

b1 is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like ManySortedSubset of Carrier A

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 is Relation-like I -defined Function-like non empty V14(I) Element of Carrier A

p . m is set

f . b is set

s . b is set

m is Element of I

I is non empty set

A is Relation-like I -defined Function-like non empty V14(I) 1-sorted-yielding non-Empty TopStruct-yielding non-void-yielding non-Trivial-yielding PLS-yielding set

Carrier A is Relation-like I -defined Function-like non empty V14(I) set

Segre_Product A is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct

the topology of (Segre_Product A) is non empty Element of bool (bool the carrier of (Segre_Product A))

the carrier of (Segre_Product A) is non empty set

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

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

f is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like ManySortedSubset of Carrier A

indx f is Element of I

A . (indx f) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct

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

B is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like ManySortedSubset of Carrier A

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

A is Relation-like I -defined Function-like non empty V14(I) 1-sorted-yielding non-Empty TopStruct-yielding non-void-yielding non-Trivial-yielding PLS-yielding set

Carrier A is Relation-like I -defined Function-like non empty V14(I) set

f is Element of I

A . f is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct

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

B is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like ManySortedSubset of Carrier A

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

(Carrier A) . B is set

i is Element of I

(B +* (f,{s})) . i is set

A . i is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct

[#] (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

A is Relation-like I -defined Function-like non empty V14(I) 1-sorted-yielding non-Empty TopStruct-yielding non-void-yielding non-Trivial-yielding PLS-yielding set

Carrier A is Relation-like I -defined Function-like non empty V14(I) set

Segre_Product A is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct

the carrier of (Segre_Product A) is non empty set

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

f is Element of I

A . f is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct

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 is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like ManySortedSubset of Carrier A

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 (Carrier A) 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)

(Carrier A) . B is set

(B +* (f,s)) . B is set

B . B is set

(Carrier A) . B is set

product (Carrier A) is set

Segre_Blocks 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)),(Segre_Blocks A) #) is strict TopStruct

I is non empty set

A is Relation-like I -defined Function-like non empty V14(I) set

{A} is Relation-like I -defined Function-like non empty V14(I) trivial-yielding Segre-like 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

f is Relation-like I -defined Function-like non empty V14(I) 1-sorted-yielding non-Empty TopStruct-yielding non-void-yielding non-Trivial-yielding PLS-yielding set

f . A is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct

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

Carrier f is Relation-like I -defined Function-like non empty V14(I) set

Segre_Product f is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct

the topology of (Segre_Product f) is non empty Element of bool (bool the carrier of (Segre_Product f))

the carrier of (Segre_Product f) is non empty set

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

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

s is Element of the topology of (f . A)

B is Relation-like I -defined Function-like non empty V14(I) Element of Carrier f

{B} is Relation-like I -defined Function-like non empty V14(I) trivial-yielding Segre-like set

{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 is Relation-like I -defined Function-like non empty V14(I) ManySortedSubset of Carrier f

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

p is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like ManySortedSubset of Carrier f

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

A is Relation-like I -defined Function-like non empty V14(I) 1-sorted-yielding non-Empty TopStruct-yielding non-void-yielding non-Trivial-yielding PLS-yielding set

Segre_Product A is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct

the carrier of (Segre_Product A) is non empty set

f is Element of the carrier of (Segre_Product A)

s is Element of the carrier of (Segre_Product A)

the topology of (Segre_Product A) is non empty Element of bool (bool the carrier of (Segre_Product A))

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

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

{f,s} is non empty Element of bool the carrier of (Segre_Product A)

B is Element of the topology of (Segre_Product A)

B is Relation-like I -defined Function-like non empty V14(I) set

i is Relation-like I -defined Function-like non empty V14(I) set

Carrier A is Relation-like I -defined Function-like non empty V14(I) set

p is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like ManySortedSubset of Carrier A

product p is non empty non trivial set

indx p is Element of I

p . (indx p) is non empty set

A . (indx p) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct

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

A . a is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct

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

o is Relation-like Function-like set

dom o is set

i . d1 is set

o is Relation-like Function-like set

dom o is set

p0 is Relation-like Function-like 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))

d1 is Relation-like Function-like set

dom d1 is set

d1 is Relation-like Function-like 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

Carrier A is Relation-like I -defined Function-like non empty V14(I) set

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

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

i is Element of I

A . i is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct

the carrier of (A . i) is non empty set

B . i is set

B . i is set

(Carrier A) . 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 (Segre_Product A) is non empty Element of bool (bool the carrier of (Segre_Product A))

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

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

{B} is Relation-like I -defined Function-like non empty V14(I) trivial-yielding Segre-like 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 (Segre_Product A)

dom B is non empty Element of bool I

{f,s} is non empty Element of bool the carrier of (Segre_Product A)

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

A is Relation-like I -defined Function-like non empty V14(I) 1-sorted-yielding non-Empty TopStruct-yielding non-void-yielding non-Trivial-yielding PLS-yielding set

Carrier A is Relation-like I -defined Function-like non empty V14(I) set

f is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like ManySortedSubset of Carrier A

indx f is Element of I

A . (indx f) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct

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

p is Relation-like Function-like set

dom p is set

i is Relation-like I -defined Function-like non empty V14(I) set

p is Relation-like I -defined Function-like non empty V14(I) 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

b is Relation-like Function-like set

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

j is Relation-like Function-like 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

c2 is Relation-like Function-like 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

A is Relation-like I -defined Function-like non empty V14(I) V259() set

f is Relation-like I -defined Function-like non empty V14(I) V259() set

{ b

card { b

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

A is Relation-like I -defined Function-like non empty V14(I) V259() set

f is Relation-like I -defined Function-like non empty V14(I) V259() set

(I,A,f) is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative set

{ b

card { b

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

{ b

card { b

(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

A is Relation-like I -defined Function-like non empty V14(I) 1-sorted-yielding non-Empty TopStruct-yielding non-void-yielding non-Trivial-yielding PLS-yielding set

I is non empty set

A is Relation-like I -defined Function-like non empty V14(I) 1-sorted-yielding non-Empty TopStruct-yielding non-void-yielding non-Trivial-yielding PLS-yielding set

Segre_Product A is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct

the carrier of (Segre_Product A) is non empty set

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

bool [: the carrier of (Segre_Product A), the carrier of (Segre_Product A):] is non empty set

f is Segre-Coset of A

s is Segre-Coset of A

B is Relation-like the carrier of (Segre_Product A) -defined the carrier of (Segre_Product A) -valued Function-like non empty V14( the carrier of (Segre_Product A)) quasi_total isomorphic Element of bool [: the carrier of (Segre_Product A), the carrier of (Segre_Product A):]

B .: f is Element of bool the carrier of (Segre_Product A)

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

B .: s is Element of bool the carrier of (Segre_Product A)

B is Segre-Coset of A

i is Segre-Coset of A

p is Element of the carrier of (Segre_Product A)

dom B is non empty Element of bool the carrier of (Segre_Product A)

a is set

B . a is set

b1 is Element of the carrier of (Segre_Product A)

b is Element of the carrier of (Segre_Product A)

B . b is Element of the carrier of (Segre_Product A)

m is Element of the carrier of (Segre_Product A)

the topology of (Segre_Product A) is non empty Element of bool (bool the carrier of (Segre_Product A))

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

{b1,b} is non empty Element of bool the carrier of (Segre_Product A)

d1 is Element of the topology of (Segre_Product A)

B .: d1 is Element of the topology of (Segre_Product A)

j is Element of the topology of (Segre_Product A)

{p,m} is non empty Element of bool the carrier of (Segre_Product A)

I is non empty set

A is Relation-like I -defined Function-like non empty V14(I) 1-sorted-yielding non-Empty TopStruct-yielding non-void-yielding non-Trivial-yielding PLS-yielding set

Carrier A is Relation-like I -defined Function-like non empty V14(I) set

f is Segre-Coset of A

s is Segre-Coset of A

B is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like ManySortedSubset of Carrier 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 void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct

[#] (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

B is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like ManySortedSubset of Carrier 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 void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct

[#] (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 Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like ManySortedSubset of Carrier A

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 void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct

[#] (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

p is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like ManySortedSubset of Carrier A

product p is non empty non trivial set

a is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like ManySortedSubset of Carrier A

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

A . (indx p) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct

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

Segre_Product A is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct

the carrier of (Segre_Product A) is non empty set

d1 is Element of the carrier of (Segre_Product A)

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

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

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 (Segre_Product A)

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

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

p is Relation-like Function-like set

dom p is set

p1 is Element of the carrier of (Segre_Product A)

f /\ s is Element of bool the carrier of (Segre_Product A)

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

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

q is Element of I

A . q is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct

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

(Carrier A) . c1 is set

A . c1 is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct

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

c1 is Relation-like Function-like 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

c1 is Relation-like Function-like set

dom c1 is set

f /\ s is Element of bool the carrier of (Segre_Product A)

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

b1 is set

Segre_Product A is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct

the carrier of (Segre_Product A) is non empty set

b is Element of the carrier of (Segre_Product A)

m is Element of the carrier of (Segre_Product A)

f /\ s is Element of bool the carrier of (Segre_Product A)

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

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

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

c2 is Element of I

A . c2 is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct

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

(Carrier A) . p0 is set

A . p0 is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct

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

B is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like ManySortedSubset of Carrier 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 void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct

[#] (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

A . i is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct

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

(Carrier A) . 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

Segre_Product A is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct

the carrier of (Segre_Product A) is non empty set

f /\ f is Element of bool the carrier of (Segre_Product A)

bool the carrier of (Segre_Product A) 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 (Segre_Product A)

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

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

c2 is Element of the carrier of (Segre_Product A)

p0 is set

u is Element of I

dom j is non empty Element of bool I

o is Relation-like I -defined Function-like non empty V14(I) set

o . p0 is set

B . p0 is set

u is Element of I

dom j is non empty Element of bool I

o is Relation-like I -defined Function-like non empty V14(I) set

o . u is set

j . u is set

B . u is non empty set

p1 is Relation-like Function-like set

dom p1 is set

o . p0 is set

B . p0 is set

u is Element of I

o is Relation-like I -defined Function-like non empty V14(I) set

o is Relation-like I -defined Function-like non empty V14(I) set

dom o is non empty Element of bool I

the topology of (Segre_Product A) is non empty Element of bool (bool the carrier of (Segre_Product A))

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

{j} is Relation-like I -defined Function-like non empty V14(I) trivial-yielding Segre-like 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 (Segre_Product A)

u is set

j . u is set

B . u is set

p1 is Relation-like Function-like 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 (Segre_Product A)

I is non empty finite set

A is Relation-like I -defined Function-like non empty V14(I) 1-sorted-yielding non-Empty TopStruct-yielding non-void-yielding non-Trivial-yielding PLS-yielding V259() set

Carrier A is Relation-like I -defined Function-like non empty V14(I) V259() set

Segre_Product A is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct

the carrier of (Segre_Product A) is non empty set

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

f is Element of I

A . f is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct

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

B is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like V259() ManySortedSubset of Carrier A

product B is non empty non trivial set

B is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like V259() ManySortedSubset of Carrier A

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

(Carrier A) . 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

b is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V259() set

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 is Relation-like NAT -defined bool the carrier of (Segre_Product A) -valued Function-like finite FinSequence-like FinSubsequence-like V259() FinSequence of bool the carrier of (Segre_Product A)

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 is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like V259() ManySortedSubset of Carrier A

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 void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct

[#] (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

u is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like V259() ManySortedSubset of Carrier A

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

p is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like V259() ManySortedSubset of Carrier A

product p is non empty non trivial set

j /\ c2 is Element of bool the carrier of (Segre_Product A)

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

q1 is Relation-like Function-like set

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

c1 is Relation-like Function-like set

dom c1 is set

c1 . f is set

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

q is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like V259() ManySortedSubset of Carrier A

product q is non empty non trivial set

q1 is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like V259() ManySortedSubset of Carrier A

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

A . c1 is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct

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

A is Relation-like I -defined Function-like non empty V14(I) 1-sorted-yielding non-Empty TopStruct-yielding non-void-yielding non-Trivial-yielding PLS-yielding V259() set

Carrier A is Relation-like I -defined Function-like non empty V14(I) V259() set

Segre_Product A is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct

the carrier of (Segre_Product A) is non empty set

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

f is Segre-Coset of A

s is Segre-Coset of A

B is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like V259() ManySortedSubset of Carrier A

product B is non empty non trivial set

B is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like V259() ManySortedSubset of Carrier A

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

p is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like V259() ManySortedSubset of Carrier A

indx p is Element of I

a is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like V259() ManySortedSubset of Carrier A

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

{ b

card { b

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 void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct

[#] (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

(Carrier A) . b is set

A . b is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct

[#] (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 is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like V259() ManySortedSubset of Carrier A

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

{ b

card { b

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

c2 is Relation-like NAT -defined bool the carrier of (Segre_Product A) -valued Function-like finite FinSequence-like FinSubsequence-like V259() FinSequence of bool the carrier of (Segre_Product A)

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 is Relation-like NAT -defined bool the carrier of (Segre_Product A) -valued Function-like finite FinSequence-like FinSubsequence-like V259() FinSequence of bool the carrier of (Segre_Product A)

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

c2 ^' o is Relation-like NAT -defined bool the carrier of (Segre_Product A) -valued Function-like finite FinSequence-like FinSubsequence-like V259() FinSequence of bool the carrier of (Segre_Product A)

p0 is Relation-like NAT -defined bool the carrier of (Segre_Product A) -valued Function-like finite FinSequence-like FinSubsequence-like V259() FinSequence of bool the carrier of (Segre_Product A)

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 (Segre_Product A))

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

rng c2 is Element of bool (bool the carrier of (Segre_Product A))

rng o is Element of bool (bool the carrier of (Segre_Product A))

(rng c2) \/ (rng o) is Element of bool (bool the carrier of (Segre_Product A))

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

i is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like V259() ManySortedSubset of Carrier A

indx i is Element of I

p is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like V259() ManySortedSubset of Carrier A

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

{ b

card { b

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

{ b

card { b

i is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like V259() ManySortedSubset of Carrier A

indx i is Element of I

p is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like V259() ManySortedSubset of Carrier A

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

{ b

card { b

i is Relation-like NAT -defined bool the carrier of (Segre_Product A) -valued Function-like finite FinSequence-like FinSubsequence-like V259() FinSequence of bool the carrier of (Segre_Product A)

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 is Relation-like NAT -defined bool the carrier of (Segre_Product A) -valued Function-like finite FinSequence-like FinSubsequence-like V259() FinSequence of bool the carrier of (Segre_Product A)

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

a is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like V259() ManySortedSubset of Carrier A

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

m is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like V259() ManySortedSubset of Carrier 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 void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct

[#] (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

p is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like V259() ManySortedSubset of Carrier A

product p is non empty non trivial set

indx p is Element of I

I is non empty finite set

A is Relation-like I -defined Function-like non empty V14(I) 1-sorted-yielding non-Empty TopStruct-yielding non-void-yielding non-Trivial-yielding PLS-yielding V259() set

Segre_Product A is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct

the carrier of (Segre_Product A) is non empty set

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

bool [: the carrier of (Segre_Product A), the carrier of (Segre_Product A):] is non empty set

Carrier A is Relation-like I -defined Function-like non empty V14(I) V259() set

f is Element of I

A . f is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct

f is Relation-like the carrier of (Segre_Product A) -defined the carrier of (Segre_Product A) -valued Function-like non empty V14( the carrier of (Segre_Product A)) quasi_total isomorphic Element of bool [: the carrier of (Segre_Product A), the carrier of (Segre_Product A):]

s is Segre-Coset of A

B is Segre-Coset of A

f .: s is Element of bool the carrier of (Segre_Product A)

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

f .: B is Element of bool the carrier of (Segre_Product A)

B is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like V259() ManySortedSubset of Carrier A

product B is non empty non trivial set

i is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like V259() ManySortedSubset of Carrier A

product i is non empty non trivial set

p is Relation-like non-empty non empty-yielding I -defined Function-like non empty V14(I) non trivial-yielding Segre-like V259() ManySortedSubset of Carrier A

product p is non empty non trivial set