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
{ 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
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
{ 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
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
{ 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 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
{ 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 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
{ 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
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
{ 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 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
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 B is Element of I
indx i is Element of I
indx p is Element of I
indx a is Element of I
b1 is Segre-Coset of A
b is Segre-Coset of A
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
d1 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)
len d1 is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative Element of NAT
dom d1 is Element of bool NAT
Seg (len m) is finite len m -element Element of bool NAT
j is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative set
d1 . j is set
j + 1 is non empty V21() V22() V23() V27() finite cardinal V66() V230() ext-real positive non negative Element of NAT
d1 . (j + 1) is set
m . j is set
m . (j + 1) is set
p0 is Segre-Coset of A
u is Segre-Coset of A
f .: (m . j) is Element of bool the carrier of (Segre_Product A)
f .: (m . (j + 1)) is Element of bool the carrier of (Segre_Product A)
c2 is Segre-Coset of A
o is Segre-Coset of A
j is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative set
d1 . j is set
m . j is set
c2 is Segre-Coset of A
f .: c2 is Element of bool the carrier of (Segre_Product A)
d1 . (len d1) is set
d1 . 1 is set
I is non empty finite set
[:I,I:] is Relation-like non empty set
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-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 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):]
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 Element of bool [: the carrier of (Segre_Product A), the carrier of (Segre_Product A):]
B is Element of I
B is Element of I
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 p is non empty non trivial set
a is Segre-Coset of A
f .: a is Element of bool the carrier of (Segre_Product A)
bool the carrier of (Segre_Product A) is non empty set
b1 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
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
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
indx m is Element of I
product m is non empty non trivial set
d1 is Segre-Coset of A
f .: d1 is Element of bool the carrier of (Segre_Product A)
j is Segre-Coset of A
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
product c2 is non empty non trivial 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
s 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):]
f " is Relation-like Function-like set
s .: j is Element of bool the carrier of (Segre_Product A)
f " j is Element of bool the carrier of (Segre_Product A)
s .: b1 is Element of bool the carrier of (Segre_Product A)
f " b1 is Element of bool the carrier of (Segre_Product A)
dom f is non empty Element of bool the carrier of (Segre_Product A)
the Element of the carrier of (Segre_Product A) is Element of the carrier of (Segre_Product A)
B is Element of I
B is Relation-like I -defined Function-like non empty V14(I) V259() Element of Carrier A
{B} is Relation-like I -defined Function-like non empty V14(I) trivial-yielding Segre-like V259() set
dom A is non empty Element of bool I
bool I is non empty set
A . B is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
rng A is non empty 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
i is Relation-like I -defined Function-like non empty V14(I) V259() ManySortedSubset of Carrier A
p is non empty non trivial set
i +* (B,p) is Relation-like I -defined Function-like non empty V14(I) V259() set
dom i is non empty Element of bool 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
a . B is non empty set
indx a is Element of I
product a is non empty non trivial set
b1 is set
dom a is non empty Element of bool I
b is Relation-like Function-like set
dom b is set
dom (Carrier A) is non empty Element of bool I
m is set
b . m is set
a . m is set
d1 is Element of I
(Carrier A) . m is set
d1 is Element of I
b . d1 is set
i . d1 is set
B . d1 is set
{(B . d1)} is non empty trivial 1 -element set
(Carrier A) . d1 is set
A . d1 is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
[#] (A . d1) is non empty non proper Element of bool the carrier of (A . d1)
the carrier of (A . d1) is non empty set
bool the carrier of (A . d1) is non empty set
(Carrier A) . m is set
d1 is Element of I
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
b1 is Segre-Coset of A
f " b1 is Element of bool the carrier of (Segre_Product A)
bool the carrier of (Segre_Product A) is non empty set
b 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
d1 is Element of I
j is Segre-Coset of A
f .: j is Element of bool the carrier of (Segre_Product A)
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
product c2 is non empty non trivial set
o 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 o is non empty non trivial set
indx c2 is Element of I
indx o is Element of I
rng f is non empty Element of bool the carrier of (Segre_Product A)
f .: b is Element of bool the carrier of (Segre_Product A)
the Element of the carrier of (Segre_Product A) is Element of the carrier of (Segre_Product A)
B is Element of I
B is Relation-like I -defined Function-like non empty V14(I) V259() Element of Carrier A
{B} is Relation-like I -defined Function-like non empty V14(I) trivial-yielding Segre-like V259() set
dom A is non empty Element of bool I
bool I is non empty set
A . B is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
rng A is non empty 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
i is Relation-like I -defined Function-like non empty V14(I) V259() ManySortedSubset of Carrier A
p is non empty non trivial set
i +* (B,p) is Relation-like I -defined Function-like non empty V14(I) V259() set
dom i is non empty Element of bool 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
a . B is non empty set
indx a is Element of I
product a is non empty non trivial set
b1 is set
dom a is non empty Element of bool I
b is Relation-like Function-like set
dom b is set
dom (Carrier A) is non empty Element of bool I
m is set
b . m is set
a . m is set
d1 is Element of I
(Carrier A) . m is set
d1 is Element of I
b . d1 is set
i . d1 is set
B . d1 is set
{(B . d1)} is non empty trivial 1 -element set
(Carrier A) . d1 is set
A . d1 is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
[#] (A . d1) is non empty non proper Element of bool the carrier of (A . d1)
the carrier of (A . d1) is non empty set
bool the carrier of (A . d1) is non empty set
(Carrier A) . m is set
d1 is Element of I
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
b1 is Segre-Coset of A
f .: b1 is Element of bool the carrier of (Segre_Product A)
bool the carrier of (Segre_Product A) is non empty set
b 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
d1 is Segre-Coset of A
f .: d1 is Element of bool the carrier of (Segre_Product A)
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
product j is non empty non trivial 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
product c2 is non empty non trivial set
indx j is Element of I
indx c2 is Element of I
s is Element of I
B is Element of I
B is Element of I
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
product i is non empty non trivial set
p is Segre-Coset of A
f .: p is Element of bool the carrier of (Segre_Product A)
bool the carrier of (Segre_Product A) is non empty set
a is Segre-Coset of A
b1 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 b1 is non empty non trivial set
indx b1 is Element of I
b1 . (indx b1) is non empty set
A . (indx b1) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
[#] (A . (indx b1)) is non empty non proper Element of bool the carrier of (A . (indx b1))
the carrier of (A . (indx b1)) is non empty set
bool the carrier of (A . (indx b1)) is non empty set
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
[:I,I:] is Relation-like non empty set
bool [:I,I:] is non empty set
Carrier A is Relation-like I -defined Function-like non empty V14(I) V259() set
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 Relation-like I -defined I -valued Function-like one-to-one non empty V14(I) quasi_total onto bijective V259() Element of bool [:I,I:]
B is Relation-like I -defined I -valued Function-like one-to-one non empty V14(I) quasi_total onto bijective V259() Element of bool [:I,I:]
B is set
i is Element of I
B . i is Element of I
s . i is Element of I
b1 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 b1 is Element of I
product b1 is non empty non trivial set
b is Segre-Coset of A
f .: b is Element of bool the carrier of (Segre_Product A)
bool the carrier of (Segre_Product A) is non empty set
m is Segre-Coset of A
d1 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 d1 is non empty non trivial set
indx d1 is Element of I
d1 . (indx d1) is non empty set
A . (indx d1) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
[#] (A . (indx d1)) is non empty non proper Element of bool the carrier of (A . (indx d1))
the carrier of (A . (indx d1)) is non empty set
bool the carrier of (A . (indx d1)) is non empty set
a is Element of I
p is Element of I
s . B is set
B . B is set
dom s is non empty Element of bool I
bool I is non empty set
dom 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) 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
s 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 s is non empty non trivial set
indx s is Element of I
A . (indx s) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . (indx s)) is non empty set
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):]
(I,A,f) is Relation-like I -defined I -valued Function-like one-to-one non empty V14(I) quasi_total onto bijective V259() Element of bool [:I,I:]
[:I,I:] is Relation-like non empty set
bool [:I,I:] is non empty set
(I,A,f) . (indx s) is Element of I
A . ((I,A,f) . (indx s)) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . ((I,A,f) . (indx s))) is non empty set
[: the carrier of (A . (indx s)), the carrier of (A . ((I,A,f) . (indx s))):] is Relation-like non empty set
bool [: the carrier of (A . (indx s)), the carrier of (A . ((I,A,f) . (indx s))):] is non empty set
B is Segre-Coset of A
f .: B is Element of bool the carrier of (Segre_Product A)
bool the carrier of (Segre_Product A) is non empty set
b1 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
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
f " b1 is Element of bool 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
d1 is set
{d1} is non empty trivial 1 -element set
s +* ((indx s),{d1}) is Relation-like I -defined Function-like non empty V14(I) V259() set
product (s +* ((indx s),{d1})) is set
f .: (product (s +* ((indx s),{d1}))) is Element of bool the carrier of (Segre_Product A)
j is set
dom s is non empty Element of bool I
bool I is non empty set
o is Relation-like Function-like set
dom o is set
c2 is Relation-like I -defined Function-like non empty V14(I) V259() set
c2 +* ((indx s),d1) is Relation-like I -defined Function-like non empty V14(I) V259() set
{(c2 +* ((indx s),d1))} is functional non empty trivial 1 -element set
p0 is set
dom (s +* ((indx s),{d1})) is non empty Element of bool I
dom c2 is non empty Element of bool I
(c2 +* ((indx s),d1)) . p0 is set
(s +* ((indx s),{d1})) . p0 is set
(c2 +* ((indx s),d1)) . p0 is set
c2 . p0 is set
s . p0 is set
(s +* ((indx s),{d1})) . p0 is set
p0 is set
dom (c2 +* ((indx s),d1)) is non empty Element of bool I
p0 is set
dom (s +* ((indx s),{d1})) is non empty Element of bool I
u is Relation-like Function-like set
dom u is set
p1 is set
u . p1 is set
(s +* ((indx s),{d1})) . p1 is set
p is Element of I
(c2 +* ((indx s),d1)) . p1 is set
q is Relation-like Function-like set
dom q is set
p is Element of I
s . p is non empty set
s . p1 is set
q is set
{q} is non empty trivial 1 -element set
(c2 +* ((indx s),d1)) . p1 is set
c2 . p1 is set
q1 is Relation-like Function-like set
dom q1 is set
p is Element of I
dom (c2 +* ((indx s),d1)) is non empty Element of bool I
p0 is set
dom (Carrier A) is non empty Element of bool I
u is Element of I
(c2 +* ((indx s),d1)) . u is set
[#] (A . (indx s)) is non empty non proper Element of bool the carrier of (A . (indx s))
bool the carrier of (A . (indx s)) is non empty set
p1 is Relation-like Function-like set
dom p1 is set
(c2 +* ((indx s),d1)) . p0 is set
(Carrier A) . p0 is set
u is Element of I
s . p0 is set
(Carrier A) . p0 is set
(c2 +* ((indx s),d1)) . u is set
c2 . u is set
s . u is non empty set
(c2 +* ((indx s),d1)) . p0 is set
u is Element of I
dom (c2 +* ((indx s),d1)) is non empty Element of bool I
p0 is Element of the carrier of (Segre_Product A)
f . p0 is Element of the carrier of (Segre_Product A)
u is Relation-like I -defined Function-like non empty V14(I) V259() set
u . ((I,A,f) . (indx s)) is set
dom f is non empty Element of bool the carrier of (Segre_Product A)
Im (f,(c2 +* ((indx s),d1))) is set
f .: {(c2 +* ((indx s),d1))} is set
f . (c2 +* ((indx s),d1)) is set
{(f . (c2 +* ((indx s),d1)))} is non empty trivial 1 -element set
p1 is Relation-like I -defined Function-like non empty V14(I) V259() set
p1 . ((I,A,f) . (indx s)) is set
d1 is Relation-like Function-like set
dom d1 is set
dom f is non empty Element of bool the carrier of (Segre_Product A)
rng d1 is set
j is set
c2 is set
d1 . c2 is set
o is Element of the carrier of (A . (indx s))
{o} is non empty trivial 1 -element Element of bool the carrier of (A . (indx s))
bool the carrier of (A . (indx s)) is non empty set
s +* ((indx s),{o}) is Relation-like I -defined Function-like non empty V14(I) V259() set
product (s +* ((indx s),{o})) is set
p0 is Relation-like I -defined Function-like non empty V14(I) V259() set
p0 +* ((indx s),o) is Relation-like I -defined Function-like non empty V14(I) V259() set
{(p0 +* ((indx s),o))} is functional non empty trivial 1 -element set
u is Element of the carrier of (Segre_Product A)
f . u is Element of the carrier of (Segre_Product A)
Im (f,(p0 +* ((indx s),o))) is set
f .: {(p0 +* ((indx s),o))} is set
{(f . u)} is non empty trivial 1 -element Element of bool the carrier of (Segre_Product A)
p1 is Relation-like I -defined Function-like non empty V14(I) V259() set
f .: (product (s +* ((indx s),{o}))) is Element of bool the carrier of (Segre_Product A)
dom (Carrier A) is non empty Element of bool I
bool I is non empty set
p1 . ((I,A,f) . (indx s)) is set
(Carrier A) . ((I,A,f) . (indx s)) is set
[#] (A . ((I,A,f) . (indx s))) is non empty non proper Element of bool the carrier of (A . ((I,A,f) . (indx s)))
bool the carrier of (A . ((I,A,f) . (indx s))) is non empty set
j is Relation-like the carrier of (A . (indx s)) -defined the carrier of (A . ((I,A,f) . (indx s))) -valued Function-like non empty V14( the carrier of (A . (indx s))) quasi_total Element of bool [: the carrier of (A . (indx s)), the carrier of (A . ((I,A,f) . (indx s))):]
o is set
dom j is non empty set
p0 is set
j . o is set
j . p0 is set
dom j is non empty Element of bool the carrier of (A . (indx s))
bool the carrier of (A . (indx s)) is non empty set
u is Element of the carrier of (A . (indx s))
{u} is non empty trivial 1 -element Element of bool the carrier of (A . (indx s))
s +* ((indx s),{u}) is Relation-like I -defined Function-like non empty V14(I) V259() set
product (s +* ((indx s),{u})) is set
p is Relation-like I -defined Function-like non empty V14(I) V259() set
p +* ((indx s),u) is Relation-like I -defined Function-like non empty V14(I) V259() set
{(p +* ((indx s),u))} is functional non empty trivial 1 -element set
q is Element of the carrier of (Segre_Product A)
f . q is Element of the carrier of (Segre_Product A)
p1 is Element of the carrier of (A . (indx s))
{p1} is non empty trivial 1 -element Element of bool the carrier of (A . (indx s))
s +* ((indx s),{p1}) is Relation-like I -defined Function-like non empty V14(I) V259() set
product (s +* ((indx s),{p1})) is set
c1 is Relation-like I -defined Function-like non empty V14(I) V259() set
c1 +* ((indx s),p1) is Relation-like I -defined Function-like non empty V14(I) V259() set
{(c1 +* ((indx s),p1))} is functional non empty trivial 1 -element set
dom s is non empty Element of bool I
bool I is non empty set
dom p is non empty Element of bool I
c1 is set
(p +* ((indx s),u)) . c1 is set
[#] (A . (indx s)) is non empty non proper Element of bool the carrier of (A . (indx s))
s . c1 is set
(p +* ((indx s),u)) . c1 is set
p . c1 is set
s . c1 is set
dom (p +* ((indx s),u)) is non empty Element of bool I
q1 is Relation-like I -defined Function-like non empty V14(I) V259() set
c1 is Element of the carrier of (Segre_Product A)
f . c1 is Element of the carrier of (Segre_Product A)
Im (f,(c1 +* ((indx s),p1))) is set
f .: {(c1 +* ((indx s),p1))} is set
{(f . c1)} is non empty trivial 1 -element Element of bool the carrier of (Segre_Product A)
c2 is Relation-like I -defined Function-like non empty V14(I) V259() set
f .: (product (s +* ((indx s),{p1}))) is Element of bool the carrier of (Segre_Product A)
j . p1 is Element of the carrier of (A . ((I,A,f) . (indx s)))
c2 . ((I,A,f) . (indx s)) is set
(p +* ((indx s),u)) . (indx s) is set
dom c1 is non empty Element of bool I
t is set
(c1 +* ((indx s),p1)) . t is set
[#] (A . (indx s)) is non empty non proper Element of bool the carrier of (A . (indx s))
s . t is set
(c1 +* ((indx s),p1)) . t is set
c1 . t is set
s . t is set
dom (c1 +* ((indx s),p1)) is non empty Element of bool I
Im (f,(p +* ((indx s),u))) is set
f .: {(p +* ((indx s),u))} is set
{(f . q)} is non empty trivial 1 -element Element of bool the carrier of (Segre_Product A)
f .: (product (s +* ((indx s),{u}))) is Element of bool the carrier of (Segre_Product A)
t is set
t1 is Element of I
q1 . t is set
c2 . t is set
t1 is Element of I
q1 . t is set
c2 . t is set
t1 is Element of I
(c1 +* ((indx s),p1)) . (indx s) is set
dom q1 is non empty Element of bool I
dom c2 is non empty Element of bool I
rng f is non empty Element of bool the carrier of (Segre_Product A)
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 Element of bool [: the carrier of (Segre_Product A), the carrier of (Segre_Product A):]
f " is Relation-like Function-like set
rng j is non empty Element of bool the carrier of (A . ((I,A,f) . (indx s)))
bool the carrier of (A . ((I,A,f) . (indx s))) is non empty set
o is set
p0 is Element of the carrier of (A . ((I,A,f) . (indx s)))
{p0} is non empty trivial 1 -element Element of bool the carrier of (A . ((I,A,f) . (indx s)))
b +* ((indx b),{p0}) is Relation-like I -defined Function-like non empty V14(I) V259() set
product (b +* ((indx b),{p0})) is set
u is Relation-like I -defined Function-like non empty V14(I) V259() set
u +* ((indx b),p0) is Relation-like I -defined Function-like non empty V14(I) V259() set
{(u +* ((indx b),p0))} is functional non empty trivial 1 -element set
p1 is Element of the carrier of (Segre_Product A)
(f ") . p1 is Element of the carrier of (Segre_Product A)
f . ((f ") . p1) is Element of the carrier of (Segre_Product A)
dom s is non empty Element of bool I
bool I is non empty set
q1 is set
c1 is Element of I
q is Relation-like I -defined Function-like non empty V14(I) V259() set
q . (indx s) is set
{(q . (indx s))} is non empty trivial 1 -element set
s +* ((indx s),{(q . (indx s))}) is Relation-like I -defined Function-like non empty V14(I) V259() set
(s +* ((indx s),{(q . (indx s))})) . c1 is set
q . q1 is set
{(q . q1)} is non empty trivial 1 -element set
(s +* ((indx s),{(q . (indx s))})) . q1 is set
c1 is Element of I
q is Relation-like I -defined Function-like non empty V14(I) V259() set
q . (indx s) is set
{(q . (indx s))} is non empty trivial 1 -element set
s +* ((indx s),{(q . (indx s))}) is Relation-like I -defined Function-like non empty V14(I) V259() set
(s +* ((indx s),{(q . (indx s))})) . c1 is set
s . c1 is non empty set
dom b is non empty Element of bool I
dom u is non empty Element of bool I
c1 is set
p is Relation-like I -defined Function-like non empty V14(I) V259() set
p . c1 is set
b . c1 is set
p is Relation-like I -defined Function-like non empty V14(I) V259() set
p . c1 is set
u . c1 is set
b . c1 is set
p is Relation-like I -defined Function-like non empty V14(I) V259() set
p is Relation-like I -defined Function-like non empty V14(I) V259() set
dom p is non empty Element of bool I
c1 is set
f . c1 is set
q . q1 is set
(s +* ((indx s),{(q . (indx s))})) . q1 is set
c1 is Element of I
q is Relation-like I -defined Function-like non empty V14(I) V259() set
q . (indx s) is set
{(q . (indx s))} is non empty trivial 1 -element set
s +* ((indx s),{(q . (indx s))}) is Relation-like I -defined Function-like non empty V14(I) V259() set
q is Relation-like I -defined Function-like non empty V14(I) V259() set
q . (indx s) is set
{(q . (indx s))} is non empty trivial 1 -element set
s +* ((indx s),{(q . (indx s))}) is Relation-like I -defined Function-like non empty V14(I) V259() set
dom (Carrier A) is non empty Element of bool I
(Carrier A) . (indx s) is set
[#] (A . (indx s)) is non empty non proper Element of bool the carrier of (A . (indx s))
bool the carrier of (A . (indx s)) is non empty set
dom q is non empty Element of bool I
dom (s +* ((indx s),{(q . (indx s))})) is non empty Element of bool I
product (s +* ((indx s),{(q . (indx s))})) is set
f .: (product (s +* ((indx s),{(q . (indx s))}))) is Element of bool the carrier of (Segre_Product A)
dom u is non empty Element of bool I
j . (q . (indx s)) is set
(u +* ((indx b),p0)) . ((I,A,f) . (indx s)) is set
dom j is non empty Element of bool the carrier of (A . (indx s))
j " is Relation-like the carrier of (A . ((I,A,f) . (indx s))) -defined the carrier of (A . (indx s)) -valued Function-like non empty V14( the carrier of (A . ((I,A,f) . (indx s)))) quasi_total Element of bool [: the carrier of (A . ((I,A,f) . (indx s))), the carrier of (A . (indx s)):]
[: the carrier of (A . ((I,A,f) . (indx s))), the carrier of (A . (indx s)):] is Relation-like non empty set
bool [: the carrier of (A . ((I,A,f) . (indx s))), the carrier of (A . (indx s)):] is non empty set
j " is Relation-like Function-like set
o is Element of bool the carrier of (A . ((I,A,f) . (indx s)))
(j ") .: o is Element of bool the carrier of (A . (indx s))
bool the carrier of (A . (indx s)) is non empty set
the topology of (A . ((I,A,f) . (indx s))) is non empty Element of bool (bool the carrier of (A . ((I,A,f) . (indx s))))
bool (bool the carrier of (A . ((I,A,f) . (indx s)))) is non empty set
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
p0 is Element of the topology of (A . ((I,A,f) . (indx s)))
b +* ((indx b),p0) is Relation-like I -defined Function-like non empty V14(I) V259() set
product (b +* ((indx b),p0)) is set
u is Element of the topology of (Segre_Product A)
f " u is Element of the topology of (Segre_Product A)
p1 is Element of the topology of (Segre_Product A)
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
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
dom b is non empty Element of bool I
bool I is non empty set
q is set
(b +* ((indx b),p0)) . q is set
b . q is set
(b +* ((indx b),p0)) . q is set
b . q is set
dom (b +* ((indx b),p0)) is non empty Element of bool I
(product s) /\ (product p) is set
card ((product s) /\ (product p)) is V21() V22() V23() cardinal set
j " p0 is Element of bool the carrier of (A . (indx s))
q is set
q1 is Element of the carrier of (A . (indx s))
{q1} is non empty trivial 1 -element Element of bool the carrier of (A . (indx s))
s +* ((indx s),{q1}) is Relation-like I -defined Function-like non empty V14(I) V259() set
product (s +* ((indx s),{q1})) is set
c1 is Relation-like I -defined Function-like non empty V14(I) V259() set
c1 +* ((indx s),q1) is Relation-like I -defined Function-like non empty V14(I) V259() set
{(c1 +* ((indx s),q1))} is functional non empty trivial 1 -element set
c1 is Element of the carrier of (Segre_Product A)
f . c1 is Element of the carrier of (Segre_Product A)
Im (f,(c1 +* ((indx s),q1))) is set
f .: {(c1 +* ((indx s),q1))} is set
{(f . c1)} is non empty trivial 1 -element Element of bool the carrier of (Segre_Product A)
c2 is Relation-like I -defined Function-like non empty V14(I) V259() set
f .: (product (s +* ((indx s),{q1}))) is Element of bool the carrier of (Segre_Product A)
t is set
dom s is non empty Element of bool I
dom (s +* ((indx s),{q1})) is non empty Element of bool I
t1 is Relation-like Function-like set
dom t1 is set
o is set
t1 . o is set
(s +* ((indx s),{q1})) . o is set
[#] (A . (indx s)) is non empty non proper Element of bool the carrier of (A . (indx s))
s . o is set
s . o is set
j . q is set
c2 . ((I,A,f) . (indx s)) is set
t is set
c2 . t is set
(b +* ((indx b),p0)) . t is set
(b +* ((indx b),p0)) . t is set
b . t is set
c2 . t is set
dom c2 is non empty Element of bool I
dom p is non empty Element of bool I
dom c1 is non empty Element of bool I
(c1 +* ((indx s),q1)) . (indx s) is set
p . (indx s) is non empty set
q is set
the topology of (A . (indx s)) is non empty Element of bool (bool the carrier of (A . (indx s)))
bool (bool the carrier of (A . (indx s))) is non empty set
q1 is Element of the carrier of (A . (indx s))
{q1} is non empty trivial 1 -element Element of bool the carrier of (A . (indx s))
s +* ((indx s),{q1}) is Relation-like I -defined Function-like non empty V14(I) V259() set
product (s +* ((indx s),{q1})) is set
c1 is Relation-like I -defined Function-like non empty V14(I) V259() set
c1 +* ((indx s),q1) is Relation-like I -defined Function-like non empty V14(I) V259() set
{(c1 +* ((indx s),q1))} is functional non empty trivial 1 -element set
c1 is Element of the carrier of (Segre_Product A)
f . c1 is Element of the carrier of (Segre_Product A)
dom s is non empty Element of bool I
dom c1 is non empty Element of bool I
t is set
(c1 +* ((indx s),q1)) . t is set
p . t is set
(c1 +* ((indx s),q1)) . t is set
c1 . t is set
s . t is set
p . t is set
dom (c1 +* ((indx s),q1)) is non empty Element of bool I
dom p is non empty Element of bool I
c2 is Relation-like I -defined Function-like non empty V14(I) V259() set
c2 . (indx b) is set
(b +* ((indx b),p0)) . (indx b) is set
c2 . ((I,A,f) . (indx s)) is set
Im (f,(c1 +* ((indx s),q1))) is set
f .: {(c1 +* ((indx s),q1))} is set
{(f . c1)} is non empty trivial 1 -element Element of bool the carrier of (Segre_Product A)
f .: (product (s +* ((indx s),{q1}))) is Element of bool the carrier of (Segre_Product A)
j . q1 is Element of the carrier of (A . ((I,A,f) . (indx s)))
(j ") .: p0 is Element of bool the carrier of (A . (indx s))
the topology of (A . (indx s)) is non empty Element of bool (bool the carrier of (A . (indx s)))
bool (bool the carrier of (A . (indx s))) is non empty set
bool the carrier of (A . (indx s)) is non empty set
o is Element of bool the carrier of (A . (indx s))
j .: o is Element of bool the carrier of (A . ((I,A,f) . (indx s)))
the topology of (A . (indx s)) is non empty Element of bool (bool the carrier of (A . (indx s)))
bool (bool the carrier of (A . (indx s))) is non empty set
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
p0 is Element of the topology of (A . (indx s))
s +* ((indx s),p0) is Relation-like I -defined Function-like non empty V14(I) V259() set
product (s +* ((indx s),p0)) is set
u is Element of the topology of (Segre_Product A)
f .: u is Element of the topology of (Segre_Product A)
p1 is Element of the topology of (Segre_Product A)
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
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
dom s is non empty Element of bool I
bool I is non empty set
q is set
(s +* ((indx s),p0)) . q is set
[#] (A . (indx s)) is non empty non proper Element of bool the carrier of (A . (indx s))
s . q is set
(s +* ((indx s),p0)) . q is set
s . q is set
dom (s +* ((indx s),p0)) is non empty Element of bool I
(product b) /\ (product p) is set
card ((product b) /\ (product p)) is V21() V22() V23() cardinal set
dom p is non empty Element of bool I
j .: p0 is Element of bool the carrier of (A . ((I,A,f) . (indx s)))
q is set
dom j is non empty Element of bool the carrier of (A . (indx s))
q1 is set
j . q1 is set
c1 is Element of the carrier of (A . (indx s))
{c1} is non empty trivial 1 -element Element of bool the carrier of (A . (indx s))
s +* ((indx s),{c1}) is Relation-like I -defined Function-like non empty V14(I) V259() set
product (s +* ((indx s),{c1})) is set
c1 is Relation-like I -defined Function-like non empty V14(I) V259() set
c1 +* ((indx s),c1) is Relation-like I -defined Function-like non empty V14(I) V259() set
{(c1 +* ((indx s),c1))} is functional non empty trivial 1 -element set
c2 is Element of the carrier of (Segre_Product A)
f . c2 is Element of the carrier of (Segre_Product A)
Im (f,(c1 +* ((indx s),c1))) is set
f .: {(c1 +* ((indx s),c1))} is set
{(f . c2)} is non empty trivial 1 -element Element of bool the carrier of (Segre_Product A)
t is Relation-like I -defined Function-like non empty V14(I) V259() set
f .: (product (s +* ((indx s),{c1}))) is Element of bool the carrier of (Segre_Product A)
j . c1 is Element of the carrier of (A . ((I,A,f) . (indx s)))
t . ((I,A,f) . (indx s)) is set
dom c1 is non empty Element of bool I
t1 is set
(c1 +* ((indx s),c1)) . t1 is set
(s +* ((indx s),p0)) . t1 is set
(c1 +* ((indx s),c1)) . t1 is set
c1 . t1 is set
s . t1 is set
(s +* ((indx s),p0)) . t1 is set
dom (c1 +* ((indx s),c1)) is non empty Element of bool I
q is set
the topology of (A . ((I,A,f) . (indx s))) is non empty Element of bool (bool the carrier of (A . ((I,A,f) . (indx s))))
bool (bool the carrier of (A . ((I,A,f) . (indx s)))) is non empty set
q1 is Element of the carrier of (A . ((I,A,f) . (indx s)))
{q1} is non empty trivial 1 -element Element of bool the carrier of (A . ((I,A,f) . (indx s)))
p +* (((I,A,f) . (indx s)),{q1}) is Relation-like I -defined Function-like non empty V14(I) V259() set
product (p +* (((I,A,f) . (indx s)),{q1})) is set
c1 is Relation-like I -defined Function-like non empty V14(I) V259() set
c1 +* (((I,A,f) . (indx s)),q1) is Relation-like I -defined Function-like non empty V14(I) V259() set
{(c1 +* (((I,A,f) . (indx s)),q1))} is functional non empty trivial 1 -element set
c1 is Element of the carrier of (Segre_Product A)
(f ") . c1 is Element of the carrier of (Segre_Product A)
dom c1 is non empty Element of bool I
t is set
(c1 +* (((I,A,f) . (indx s)),q1)) . t is set
p . t is set
(c1 +* (((I,A,f) . (indx s)),q1)) . t is set
c1 . t is set
p . t is set
c2 is Relation-like I -defined Function-like non empty V14(I) V259() set
f . c2 is set
dom (c1 +* (((I,A,f) . (indx s)),q1)) is non empty Element of bool I
t is set
f . t is set
c2 . (indx s) is set
(s +* ((indx s),p0)) . (indx s) is set
t is Element of the carrier of (A . (indx s))
{t} is non empty trivial 1 -element Element of bool the carrier of (A . (indx s))
s +* ((indx s),{t}) is Relation-like I -defined Function-like non empty V14(I) V259() set
product (s +* ((indx s),{t})) is set
t1 is Relation-like I -defined Function-like non empty V14(I) V259() set
t1 +* ((indx s),t) is Relation-like I -defined Function-like non empty V14(I) V259() set
{(t1 +* ((indx s),t))} is functional non empty trivial 1 -element set
dom t1 is non empty Element of bool I
o is set
(t1 +* ((indx s),t)) . o is set
c2 . o is set
(t1 +* ((indx s),t)) . o is set
t1 . o is set
c2 . o is set
dom c2 is non empty Element of bool I
dom (t1 +* ((indx s),t)) is non empty Element of bool I
Im (f,(t1 +* ((indx s),t))) is set
f .: {(t1 +* ((indx s),t))} is set
{(f . c2)} is non empty trivial 1 -element set
f .: (product (s +* ((indx s),{t}))) is Element of bool the carrier of (Segre_Product A)
j . (c2 . (indx s)) is set
(c1 +* (((I,A,f) . (indx s)),q1)) . ((I,A,f) . (indx s)) is set
o is Relation-like I -defined Function-like non empty V14(I) V259() set
f . o is set
o . (indx s) is set
j . (o . (indx s)) is set
dom (Carrier A) is non empty Element of bool I
bool I is non empty set
(Carrier A) . (indx s) is set
[#] (A . (indx s)) is non empty non proper Element of bool the carrier of (A . (indx s))
bool the carrier of (A . (indx s)) is non empty set
dom s is non empty Element of bool I
u is set
p0 is Element of the carrier of (A . (indx s))
{p0} is non empty trivial 1 -element Element of bool the carrier of (A . (indx s))
s +* ((indx s),{p0}) is Relation-like I -defined Function-like non empty V14(I) V259() set
(s +* ((indx s),{p0})) . u is set
o . u is set
p0 is Element of the carrier of (A . (indx s))
{p0} is non empty trivial 1 -element Element of bool the carrier of (A . (indx s))
s +* ((indx s),{p0}) is Relation-like I -defined Function-like non empty V14(I) V259() set
(s +* ((indx s),{p0})) . u is set
s . u is set
o . u is set
p0 is Element of the carrier of (A . (indx s))
{p0} is non empty trivial 1 -element Element of bool the carrier of (A . (indx s))
s +* ((indx s),{p0}) is Relation-like I -defined Function-like non empty V14(I) V259() set
p0 is Element of the carrier of (A . (indx s))
{p0} is non empty trivial 1 -element Element of bool the carrier of (A . (indx s))
s +* ((indx s),{p0}) is Relation-like I -defined Function-like non empty V14(I) V259() set
dom o is non empty Element of bool I
dom (s +* ((indx s),{p0})) is non empty Element of bool I
product (s +* ((indx s),{p0})) is set
u is Relation-like I -defined Function-like non empty V14(I) V259() set
u . ((I,A,f) . (indx s)) is set
f .: (product (s +* ((indx s),{p0}))) is Element of bool the carrier of (Segre_Product A)
i is Relation-like the carrier of (A . (indx s)) -defined the carrier of (A . ((I,A,f) . (indx s))) -valued Function-like non empty V14( the carrier of (A . (indx s))) quasi_total Element of bool [: the carrier of (A . (indx s)), the carrier of (A . ((I,A,f) . (indx s))):]
p is Relation-like the carrier of (A . (indx s)) -defined the carrier of (A . ((I,A,f) . (indx s))) -valued Function-like non empty V14( the carrier of (A . (indx s))) quasi_total Element of bool [: the carrier of (A . (indx s)), the carrier of (A . ((I,A,f) . (indx s))):]
b1 is set
a is set
dom i is non empty Element of bool the carrier of (A . (indx s))
bool the carrier of (A . (indx s)) is non empty set
m is Element of the carrier of (Segre_Product A)
d1 is Relation-like I -defined Function-like non empty V14(I) V259() set
b is Element of the carrier of (A . (indx s))
d1 +* ((indx s),b) is Relation-like I -defined Function-like non empty V14(I) V259() set
dom s is non empty Element of bool I
bool I is non empty set
dom d1 is non empty Element of bool I
o is set
(d1 +* ((indx s),b)) . o is set
[#] (A . (indx s)) is non empty non proper Element of bool the carrier of (A . (indx s))
s . o is set
(d1 +* ((indx s),b)) . o is set
d1 . o is set
s . o is set
c2 is Element of the carrier of (Segre_Product A)
f . c2 is Element of the carrier of (Segre_Product A)
(d1 +* ((indx s),b)) . (indx s) is set
dom (d1 +* ((indx s),b)) is non empty Element of bool I
p . ((d1 +* ((indx s),b)) . (indx s)) is set
o is Relation-like I -defined Function-like non empty V14(I) V259() set
o . ((I,A,f) . (indx s)) is set
i . a is set
p . a is set
dom p is non empty Element of bool the carrier of (A . (indx s))
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 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):]
(I,A,f) is Relation-like I -defined I -valued Function-like one-to-one non empty V14(I) quasi_total onto bijective V259() Element of bool [:I,I:]
[:I,I:] is Relation-like non empty set
bool [:I,I:] is non empty set
s is Segre-Coset of A
B 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
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
indx B is Element of I
A . (indx B) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . (indx B)) is non empty set
(I,A,f) . (indx B) is Element of I
A . ((I,A,f) . (indx B)) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . ((I,A,f) . (indx B))) is non empty set
indx i is Element of I
A . (indx i) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . (indx i)) is non empty set
(I,A,f) . (indx i) is Element of I
A . ((I,A,f) . (indx i)) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . ((I,A,f) . (indx i))) is non empty set
(I,A,f,B) is Relation-like the carrier of (A . (indx B)) -defined the carrier of (A . ((I,A,f) . (indx B))) -valued Function-like non empty V14( the carrier of (A . (indx B))) quasi_total Element of bool [: the carrier of (A . (indx B)), the carrier of (A . ((I,A,f) . (indx B))):]
[: the carrier of (A . (indx B)), the carrier of (A . ((I,A,f) . (indx B))):] is Relation-like non empty set
bool [: the carrier of (A . (indx B)), the carrier of (A . ((I,A,f) . (indx B))):] is non empty set
(I,A,f,i) is Relation-like the carrier of (A . (indx i)) -defined the carrier of (A . ((I,A,f) . (indx i))) -valued Function-like non empty V14( the carrier of (A . (indx i))) quasi_total Element of bool [: the carrier of (A . (indx i)), the carrier of (A . ((I,A,f) . (indx i))):]
[: the carrier of (A . (indx i)), the carrier of (A . ((I,A,f) . (indx i))):] is Relation-like non empty set
bool [: the carrier of (A . (indx i)), the carrier of (A . ((I,A,f) . (indx i))):] is non empty set
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)
p is Segre-Coset of A
a is Segre-Coset of A
b is Element of I
A . b is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . b) is non empty set
B . b is non empty set
i . b is non empty set
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
d1 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 d1 is non empty non trivial set
indx d1 is Element of I
d1 . (indx d1) is non empty set
A . (indx d1) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
[#] (A . (indx d1)) is non empty non proper Element of bool the carrier of (A . (indx d1))
the carrier of (A . (indx d1)) is non empty set
bool the carrier of (A . (indx d1)) is non empty set
dom f is non empty Element of bool the carrier of (Segre_Product A)
dom B is non empty Element of bool I
bool I is non empty set
c2 is set
{c2} is non empty trivial 1 -element set
(Carrier A) . b is set
[#] (A . b) is non empty non proper Element of bool the carrier of (A . b)
bool the carrier of (A . b) is non empty set
p0 is set
o is set
p1 is Element of the carrier of (Segre_Product A)
p is Relation-like I -defined Function-like non empty V14(I) V259() set
u is Element of the carrier of (A . (indx B))
p +* ((indx B),u) is Relation-like I -defined Function-like non empty V14(I) V259() set
c1 is set
{c1} is non empty trivial 1 -element set
c2 is Element of the carrier of (A . b)
(p +* ((indx B),u)) +* (b,c2) is Relation-like I -defined Function-like non empty V14(I) V259() set
c1 is Element of the carrier of (A . b)
(p +* ((indx B),u)) . b is set
p . b is set
dom (p +* ((indx B),u)) is non empty Element of bool I
((p +* ((indx B),u)) +* (b,c2)) . b is set
o is Relation-like I -defined Function-like non empty V14(I) V259() set
q1 is Element of the carrier of (Segre_Product A)
o1 is Relation-like I -defined Function-like non empty V14(I) V259() set
t1 is Element of the carrier of (Segre_Product A)
l is Element of I
A . l is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . l) is non empty set
o . l is set
o1 . l is set
o is Element of the carrier of (A . l)
o1 is Element of the carrier of (A . l)
o is Element of I
o . o is set
o1 . o is set
f . q1 is Element of the carrier of (Segre_Product A)
f . t1 is Element of the carrier of (Segre_Product A)
dom p is non empty Element of bool I
l is set
(p +* ((indx B),u)) . l is set
B . l is set
[#] (A . (indx B)) is non empty non proper Element of bool the carrier of (A . (indx B))
bool the carrier of (A . (indx B)) is non empty set
(p +* ((indx B),u)) . l is set
p . l is set
B . l is set
l is set
((p +* ((indx B),u)) +* (b,c2)) . l is set
i . l is set
((p +* ((indx B),u)) +* (b,c2)) . l is set
(p +* ((indx B),u)) . l is set
B . l is set
i . l is set
dom ((p +* ((indx B),u)) +* (b,c2)) is non empty Element of bool I
dom i is non empty Element of bool I
((p +* ((indx B),u)) +* (b,c2)) . (indx B) is set
(I,A,f,i) . (((p +* ((indx B),u)) +* (b,c2)) . (indx B)) is set
o1 is Relation-like I -defined Function-like non empty V14(I) V259() set
o1 . ((I,A,f) . (indx B)) is set
o is Relation-like I -defined Function-like non empty V14(I) V259() set
l is Element of I
A . l is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . l) is non empty set
o . l is set
o1 . l is set
o . (indx d1) is set
o1 . (indx d1) is set
dom m is non empty Element of bool I
dom d1 is non empty Element of bool I
o is set
o1 is Element of I
o . o is set
m . o is set
o1 is Element of I
o . o1 is set
o1 . o1 is set
o . o is set
m . o is set
o1 is Element of I
dom o is non empty Element of bool I
(product d1) /\ (product m) is set
(p +* ((indx B),u)) . (indx B) is set
(I,A,f,B) . o is set
(I,A,f,i) . o is set
c1 is Element of the carrier of (A . b)
o is set
o1 is Element of I
B . o is set
i . o is set
o1 is Element of I
B . o is set
i . o is set
o1 is Element of I
dom i is non empty Element of bool I
(I,A,f,B) . o is set
(I,A,f,i) . o is set
c1 is Element of the carrier of (A . b)
dom (I,A,f,B) is non empty Element of bool the carrier of (A . (indx B))
bool the carrier of (A . (indx B)) is non empty set
dom (I,A,f,i) is non empty Element of bool the carrier of (A . (indx i))
bool the carrier of (A . (indx i)) is non empty set
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):]
(I,A,f) is Relation-like I -defined I -valued Function-like one-to-one non empty V14(I) quasi_total onto bijective V259() Element of bool [:I,I:]
[:I,I:] is Relation-like non empty set
bool [:I,I:] 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 V259() ManySortedSubset of Carrier A
product s 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 s is Element of I
indx B is Element of I
A . (indx s) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . (indx s)) is non empty set
(I,A,f) . (indx s) is Element of I
A . ((I,A,f) . (indx s)) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . ((I,A,f) . (indx s))) is non empty set
A . (indx B) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . (indx B)) is non empty set
(I,A,f) . (indx B) is Element of I
A . ((I,A,f) . (indx B)) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . ((I,A,f) . (indx B))) is non empty set
(I,A,f,s) is Relation-like the carrier of (A . (indx s)) -defined the carrier of (A . ((I,A,f) . (indx s))) -valued Function-like non empty V14( the carrier of (A . (indx s))) quasi_total Element of bool [: the carrier of (A . (indx s)), the carrier of (A . ((I,A,f) . (indx s))):]
[: the carrier of (A . (indx s)), the carrier of (A . ((I,A,f) . (indx s))):] is Relation-like non empty set
bool [: the carrier of (A . (indx s)), the carrier of (A . ((I,A,f) . (indx s))):] is non empty set
(I,A,f,B) is Relation-like the carrier of (A . (indx B)) -defined the carrier of (A . ((I,A,f) . (indx B))) -valued Function-like non empty V14( the carrier of (A . (indx B))) quasi_total Element of bool [: the carrier of (A . (indx B)), the carrier of (A . ((I,A,f) . (indx B))):]
[: the carrier of (A . (indx B)), the carrier of (A . ((I,A,f) . (indx B))):] is Relation-like non empty set
bool [: the carrier of (A . (indx B)), the carrier of (A . ((I,A,f) . (indx B))):] is non empty set
B is Segre-Coset of A
i is Segre-Coset of A
bool the carrier of (Segre_Product A) is non empty set
p 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)
p . 1 is set
len p is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative Element of NAT
p . (len p) is set
dom p is Element of bool NAT
a is V21() V22() V23() V27() finite cardinal V66() V230() ext-real non negative set
p . a is set
a + 1 is non empty V21() V22() V23() V27() finite cardinal V66() V230() ext-real positive non negative Element of NAT
p . (a + 1) is set
b1 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
indx b is Element of I
A . (indx b) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . (indx b)) is non empty set
(I,A,f) . (indx b) is Element of I
A . ((I,A,f) . (indx b)) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . ((I,A,f) . (indx b))) is non empty set
(I,A,f,b) is Relation-like the carrier of (A . (indx b)) -defined the carrier of (A . ((I,A,f) . (indx b))) -valued Function-like non empty V14( the carrier of (A . (indx b))) quasi_total Element of bool [: the carrier of (A . (indx b)), the carrier of (A . ((I,A,f) . (indx b))):]
[: the carrier of (A . (indx b)), the carrier of (A . ((I,A,f) . (indx b))):] is Relation-like non empty set
bool [: the carrier of (A . (indx b)), the carrier of (A . ((I,A,f) . (indx b))):] is non empty set
m is Segre-Coset of A
d1 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 d1 is non empty non trivial set
indx d1 is Element of I
d1 . (indx d1) is non empty set
A . (indx d1) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
[#] (A . (indx d1)) is non empty non proper Element of bool the carrier of (A . (indx d1))
the carrier of (A . (indx d1)) is non empty set
bool the carrier of (A . (indx d1)) is non empty set
(I,A,f) . (indx d1) is Element of I
A . ((I,A,f) . (indx d1)) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . ((I,A,f) . (indx d1))) is non empty set
(I,A,f,d1) is Relation-like the carrier of (A . (indx d1)) -defined the carrier of (A . ((I,A,f) . (indx d1))) -valued Function-like non empty V14( the carrier of (A . (indx d1))) quasi_total Element of bool [: the carrier of (A . (indx d1)), the carrier of (A . ((I,A,f) . (indx d1))):]
[: the carrier of (A . (indx d1)), the carrier of (A . ((I,A,f) . (indx d1))):] is Relation-like non empty set
bool [: the carrier of (A . (indx d1)), the carrier of (A . ((I,A,f) . (indx d1))):] is non empty set
p . {} is set
a is Segre-Coset of A
b1 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 b1 is non empty non trivial set
indx b1 is Element of I
A . (indx b1) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . (indx b1)) is non empty set
(I,A,f) . (indx b1) is Element of I
A . ((I,A,f) . (indx b1)) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . ((I,A,f) . (indx b1))) is non empty set
(I,A,f,b1) is Relation-like the carrier of (A . (indx b1)) -defined the carrier of (A . ((I,A,f) . (indx b1))) -valued Function-like non empty V14( the carrier of (A . (indx b1))) quasi_total Element of bool [: the carrier of (A . (indx b1)), the carrier of (A . ((I,A,f) . (indx b1))):]
[: the carrier of (A . (indx b1)), the carrier of (A . ((I,A,f) . (indx b1))):] is Relation-like non empty set
bool [: the carrier of (A . (indx b1)), the carrier of (A . ((I,A,f) . (indx b1))):] is non empty set
a is Segre-Coset of A
b1 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 b1 is non empty non trivial set
indx b1 is Element of I
A . (indx b1) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . (indx b1)) is non empty set
(I,A,f) . (indx b1) is Element of I
A . ((I,A,f) . (indx b1)) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . ((I,A,f) . (indx b1))) is non empty set
(I,A,f,b1) is Relation-like the carrier of (A . (indx b1)) -defined the carrier of (A . ((I,A,f) . (indx b1))) -valued Function-like non empty V14( the carrier of (A . (indx b1))) quasi_total Element of bool [: the carrier of (A . (indx b1)), the carrier of (A . ((I,A,f) . (indx b1))):]
[: the carrier of (A . (indx b1)), the carrier of (A . ((I,A,f) . (indx b1))):] is Relation-like non empty set
bool [: the carrier of (A . (indx b1)), the carrier of (A . ((I,A,f) . (indx b1))):] is non empty set
B is Segre-Coset of A
i is Segre-Coset of A
B is Segre-Coset of A
i is Segre-Coset of 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
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
s is Element of I
A . s is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . s) is non empty set
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):]
(I,A,f) is Relation-like I -defined I -valued Function-like one-to-one non empty V14(I) quasi_total onto bijective V259() Element of bool [:I,I:]
[:I,I:] is Relation-like non empty set
bool [:I,I:] is non empty set
(I,A,f) . s is Element of I
A . ((I,A,f) . s) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . ((I,A,f) . s)) is non empty set
[: the carrier of (A . s), the carrier of (A . ((I,A,f) . s)):] is Relation-like non empty set
bool [: the carrier of (A . s), the carrier of (A . ((I,A,f) . s)):] is non empty set
Carrier A is Relation-like I -defined Function-like non empty V14(I) V259() 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
indx B is Element of I
product B is non empty non trivial set
(I,A,f,B) is Relation-like the carrier of (A . (indx B)) -defined the carrier of (A . ((I,A,f) . (indx B))) -valued Function-like non empty V14( the carrier of (A . (indx B))) quasi_total Element of bool [: the carrier of (A . (indx B)), the carrier of (A . ((I,A,f) . (indx B))):]
A . (indx B) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . (indx B)) is non empty set
(I,A,f) . (indx B) is Element of I
A . ((I,A,f) . (indx B)) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . ((I,A,f) . (indx B))) is non empty set
[: the carrier of (A . (indx B)), the carrier of (A . ((I,A,f) . (indx B))):] is Relation-like non empty set
bool [: the carrier of (A . (indx B)), the carrier of (A . ((I,A,f) . (indx B))):] is non empty set
B is Relation-like the carrier of (A . s) -defined the carrier of (A . ((I,A,f) . s)) -valued Function-like non empty V14( the carrier of (A . s)) quasi_total Element of bool [: the carrier of (A . s), the carrier of (A . ((I,A,f) . s)):]
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
indx i is Element of I
A . (indx i) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . (indx i)) is non empty set
(I,A,f) . (indx i) is Element of I
A . ((I,A,f) . (indx i)) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . ((I,A,f) . (indx i))) is non empty set
(I,A,f,i) is Relation-like the carrier of (A . (indx i)) -defined the carrier of (A . ((I,A,f) . (indx i))) -valued Function-like non empty V14( the carrier of (A . (indx i))) quasi_total Element of bool [: the carrier of (A . (indx i)), the carrier of (A . ((I,A,f) . (indx i))):]
[: the carrier of (A . (indx i)), the carrier of (A . ((I,A,f) . (indx i))):] is Relation-like non empty set
bool [: the carrier of (A . (indx i)), the carrier of (A . ((I,A,f) . (indx i))):] is non empty set
B is Relation-like the carrier of (A . s) -defined the carrier of (A . ((I,A,f) . s)) -valued Function-like non empty V14( the carrier of (A . s)) quasi_total Element of bool [: the carrier of (A . s), the carrier of (A . ((I,A,f) . s)):]
B is Relation-like the carrier of (A . s) -defined the carrier of (A . ((I,A,f) . s)) -valued Function-like non empty V14( the carrier of (A . s)) quasi_total Element of bool [: the carrier of (A . s), the carrier of (A . ((I,A,f) . s)):]
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
product i is non empty non trivial set
(I,A,f,i) is Relation-like the carrier of (A . (indx i)) -defined the carrier of (A . ((I,A,f) . (indx i))) -valued Function-like non empty V14( the carrier of (A . (indx i))) quasi_total Element of bool [: the carrier of (A . (indx i)), the carrier of (A . ((I,A,f) . (indx i))):]
A . (indx i) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . (indx i)) is non empty set
(I,A,f) . (indx i) is Element of I
A . ((I,A,f) . (indx i)) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . ((I,A,f) . (indx i))) is non empty set
[: the carrier of (A . (indx i)), the carrier of (A . ((I,A,f) . (indx i))):] is Relation-like non empty set
bool [: the carrier of (A . (indx i)), the carrier of (A . ((I,A,f) . (indx i))):] is non empty set
I is non empty finite set
[:I,I:] is Relation-like non empty set
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-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
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):]
(I,A,f) is Relation-like I -defined I -valued Function-like one-to-one non empty V14(I) quasi_total onto bijective V259() Element of bool [:I,I:]
B is set
B is Element of I
(I,A,f,B) is Relation-like the carrier of (A . B) -defined the carrier of (A . ((I,A,f) . B)) -valued Function-like non empty V14( the carrier of (A . B)) quasi_total Element of bool [: the carrier of (A . B), the carrier of (A . ((I,A,f) . B)):]
A . B is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . B) is non empty set
(I,A,f) . B is Element of I
A . ((I,A,f) . B) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . ((I,A,f) . B)) is non empty set
[: the carrier of (A . B), the carrier of (A . ((I,A,f) . B)):] is Relation-like non empty set
bool [: the carrier of (A . B), the carrier of (A . ((I,A,f) . B)):] is non empty set
i is Element of I
(I,A,f,i) is Relation-like the carrier of (A . i) -defined the carrier of (A . ((I,A,f) . i)) -valued Function-like non empty V14( the carrier of (A . i)) quasi_total Element of bool [: the carrier of (A . i), the carrier of (A . ((I,A,f) . 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
(I,A,f) . i is Element of I
A . ((I,A,f) . i) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . ((I,A,f) . i)) is non empty set
[: the carrier of (A . i), the carrier of (A . ((I,A,f) . i)):] is Relation-like non empty set
bool [: the carrier of (A . i), the carrier of (A . ((I,A,f) . i)):] is non empty set
B is Relation-like I -defined Function-like non empty V14(I) V259() set
B is set
dom B is non empty Element of bool I
bool I is non empty set
i is Element of I
B . i is set
(I,A,f,i) is Relation-like the carrier of (A . i) -defined the carrier of (A . ((I,A,f) . i)) -valued Function-like non empty V14( the carrier of (A . i)) quasi_total Element of bool [: the carrier of (A . i), the carrier of (A . ((I,A,f) . 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
(I,A,f) . i is Element of I
A . ((I,A,f) . i) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . ((I,A,f) . i)) is non empty set
[: the carrier of (A . i), the carrier of (A . ((I,A,f) . i)):] is Relation-like non empty set
bool [: the carrier of (A . i), the carrier of (A . ((I,A,f) . i)):] is non empty set
B . B is set
B is Relation-like I -defined Function-like non empty V14(I) Function-yielding V259() set
i is Element of I
B . i is set
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
(I,A,f) . i is Element of I
A . ((I,A,f) . i) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . ((I,A,f) . i)) is non empty set
[: the carrier of (A . i), the carrier of (A . ((I,A,f) . i)):] is Relation-like non empty set
bool [: the carrier of (A . i), the carrier of (A . ((I,A,f) . i)):] is non empty set
(I,A,f,i) is Relation-like the carrier of (A . i) -defined the carrier of (A . ((I,A,f) . i)) -valued Function-like non empty V14( the carrier of (A . i)) quasi_total Element of bool [: the carrier of (A . i), the carrier of (A . ((I,A,f) . i)):]
p is Relation-like the carrier of (A . i) -defined the carrier of (A . ((I,A,f) . i)) -valued Function-like non empty V14( the carrier of (A . i)) quasi_total Element of bool [: the carrier of (A . i), the carrier of (A . ((I,A,f) . i)):]
Carrier A is Relation-like I -defined Function-like non empty V14(I) V259() 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
indx a is Element of I
product a is non empty non trivial set
(I,A,f,a) is Relation-like the carrier of (A . (indx a)) -defined the carrier of (A . ((I,A,f) . (indx a))) -valued Function-like non empty V14( the carrier of (A . (indx a))) quasi_total Element of bool [: the carrier of (A . (indx a)), the carrier of (A . ((I,A,f) . (indx a))):]
A . (indx a) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . (indx a)) is non empty set
(I,A,f) . (indx a) is Element of I
A . ((I,A,f) . (indx a)) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . ((I,A,f) . (indx a))) is non empty set
[: the carrier of (A . (indx a)), the carrier of (A . ((I,A,f) . (indx a))):] is Relation-like non empty set
bool [: the carrier of (A . (indx a)), the carrier of (A . ((I,A,f) . (indx a))):] is non empty set
p is Element of the carrier of (Segre_Product A)
f . p is Element of the carrier of (Segre_Product A)
a is Relation-like I -defined Function-like non empty V14(I) V259() set
a . i is set
Carrier A is Relation-like I -defined Function-like non empty V14(I) V259() set
b1 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 b1 is Element of I
product b1 is non empty non trivial set
b is Relation-like I -defined Function-like non empty V14(I) V259() set
b . ((I,A,f) . i) is set
m is Relation-like the carrier of (A . i) -defined the carrier of (A . ((I,A,f) . i)) -valued Function-like non empty V14( the carrier of (A . i)) quasi_total Element of bool [: the carrier of (A . i), the carrier of (A . ((I,A,f) . i)):]
m . (a . i) is set
A . (indx b1) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . (indx b1)) is non empty set
(I,A,f) . (indx b1) is Element of I
A . ((I,A,f) . (indx b1)) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . ((I,A,f) . (indx b1))) is non empty set
(I,A,f,b1) is Relation-like the carrier of (A . (indx b1)) -defined the carrier of (A . ((I,A,f) . (indx b1))) -valued Function-like non empty V14( the carrier of (A . (indx b1))) quasi_total Element of bool [: the carrier of (A . (indx b1)), the carrier of (A . ((I,A,f) . (indx b1))):]
[: the carrier of (A . (indx b1)), the carrier of (A . ((I,A,f) . (indx b1))):] is Relation-like non empty set
bool [: the carrier of (A . (indx b1)), the carrier of (A . ((I,A,f) . (indx b1))):] is non empty set