REAL is set
NAT is non empty V14() V15() V16() Element of bool REAL
bool REAL is non empty set
NAT is non empty V14() V15() V16() set
bool NAT is non empty set
bool NAT is non empty set
COMPLEX is set
RAT is set
INT is set
2 is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
K412() is set
{} is Function-like functional empty trivial V14() V15() V16() V18() V19() V20() FinSequence-membered V35() V36() ext-real non positive non negative set
the Function-like functional empty trivial V14() V15() V16() V18() V19() V20() FinSequence-membered V35() V36() ext-real non positive non negative set is Function-like functional empty trivial V14() V15() V16() V18() V19() V20() FinSequence-membered V35() V36() ext-real non positive non negative set
{{}} is non empty trivial set
K302({{}}) is functional non empty FinSequence-membered M13({{}})
[:K302({{}}),{{}}:] is non empty set
bool [:K302({{}}),{{}}:] is non empty set
PFuncs (K302({{}}),{{}}) is functional non empty set
1 is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
3 is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
Seg 1 is non empty V24() 1 -element Element of bool NAT
0 is Function-like functional empty trivial V14() V15() V16() V18() V19() V20() FinSequence-membered V35() V36() ext-real non positive non negative Element of NAT
dom {} is set
rng {} is set
I is set
B is V14() V15() V16() V20() V35() V36() ext-real non negative set
B -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
A is Relation-like NAT -defined I -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of I
A | (B -' 1) is Relation-like NAT -defined I -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of I
f is V14() V15() V16() V20() V35() V36() ext-real non negative set
A /^ f is Relation-like NAT -defined I -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of I
(A | (B -' 1)) ^ (A /^ f) is Relation-like NAT -defined I -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of I
I is set
A is Relation-like NAT -defined I -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of I
rng A is Element of bool I
bool I is non empty set
B is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
f is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
(I,A,B,f) is Relation-like NAT -defined I -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of I
B -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
A | (B -' 1) is Relation-like NAT -defined I -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of I
A /^ f is Relation-like NAT -defined I -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of I
(A | (B -' 1)) ^ (A /^ f) is Relation-like NAT -defined I -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of I
rng (I,A,B,f) is Element of bool I
rng (A /^ f) is Element of bool I
len A is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
g is non empty set
g is Relation-like NAT -defined g -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of g
g /^ f is Relation-like NAT -defined g -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of g
rng (g /^ f) is Element of bool g
bool g is non empty set
rng g is Element of bool g
rng (A | (B -' 1)) is Element of bool I
Seg (B -' 1) is V24() B -' 1 -element Element of bool NAT
A | (Seg (B -' 1)) is Relation-like NAT -defined I -valued Function-like FinSubsequence-like Element of bool [:NAT,I:]
[:NAT,I:] is set
bool [:NAT,I:] is non empty set
rng (A | (Seg (B -' 1))) is Element of bool I
rng ((A | (B -' 1)) ^ (A /^ f)) is Element of bool I
(rng (A | (B -' 1))) \/ (rng (A /^ f)) is Element of bool I
I is set
A is Relation-like NAT -defined I -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of I
dom A is Element of bool NAT
len A is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
B is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
f is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
(I,A,B,f) is Relation-like NAT -defined I -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of I
B -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
A | (B -' 1) is Relation-like NAT -defined I -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of I
A /^ f is Relation-like NAT -defined I -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of I
(A | (B -' 1)) ^ (A /^ f) is Relation-like NAT -defined I -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of I
len (I,A,B,f) is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
(len A) - f is V35() V36() ext-real set
((len A) - f) + B is V35() V36() ext-real set
(((len A) - f) + B) - 1 is V35() V36() ext-real set
1 - 1 is V35() V36() ext-real set
B - 1 is V35() V36() ext-real set
len (A | (B -' 1)) is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
len (A /^ f) is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
(len (A | (B -' 1))) + (len (A /^ f)) is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
(B -' 1) + (len (A /^ f)) is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
(B -' 1) + ((len A) - f) is V35() V36() ext-real set
(B - 1) + ((len A) - f) is V35() V36() ext-real set
I is set
A is Relation-like NAT -defined I -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of I
dom A is Element of bool NAT
len A is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
B is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
f is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
(I,A,B,f) is Relation-like NAT -defined I -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of I
B -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
A | (B -' 1) is Relation-like NAT -defined I -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of I
A /^ f is Relation-like NAT -defined I -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of I
(A | (B -' 1)) ^ (A /^ f) is Relation-like NAT -defined I -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of I
len (I,A,B,f) is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
(len A) - f is V35() V36() ext-real set
((len A) - f) + B is V35() V36() ext-real set
(((len A) - f) + B) - 1 is V35() V36() ext-real set
1 - B is V35() V36() ext-real set
I is set
A is Relation-like NAT -defined I -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of I
dom A is Element of bool NAT
B is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
g is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
B - 1 is V35() V36() ext-real set
f is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
(I,A,B,f) is Relation-like NAT -defined I -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of I
B -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
A | (B -' 1) is Relation-like NAT -defined I -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of I
A /^ f is Relation-like NAT -defined I -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of I
(A | (B -' 1)) ^ (A /^ f) is Relation-like NAT -defined I -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of I
(I,A,B,f) . g is set
A . g is set
len A is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
len (A | (B -' 1)) is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
dom (A | (B -' 1)) is Element of bool NAT
(A | (B -' 1)) . g is set
(A | (B -' 1)) /. g is Element of I
A /. g is Element of I
I is Relation-like NAT -defined Function-like V24() FinSequence-like FinSubsequence-like V187() set
len I is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
(len I) + 1 is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
A is Relation-like NAT -defined Function-like V24() FinSequence-like FinSubsequence-like V187() set
I ^ A is Relation-like NAT -defined Function-like V24() FinSequence-like FinSubsequence-like V187() set
B is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
(I ^ A) . B is set
B - (len I) is V35() V36() ext-real set
A . (B - (len I)) is set
len A is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
(len I) + (len A) is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
len A is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
(len I) + (len A) is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
dom A is Element of bool NAT
len (I ^ A) is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
dom (I ^ A) is Element of bool NAT
len A is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
(len I) + (len A) is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
I is set
A is Relation-like NAT -defined I -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of I
dom A is Element of bool NAT
len A is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
B is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
f is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
g is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
(len A) - f is V35() V36() ext-real set
((len A) - f) + B is V35() V36() ext-real set
(((len A) - f) + B) - 1 is V35() V36() ext-real set
(I,A,B,f) is Relation-like NAT -defined I -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of I
B -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
A | (B -' 1) is Relation-like NAT -defined I -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of I
A /^ f is Relation-like NAT -defined I -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of I
(A | (B -' 1)) ^ (A /^ f) is Relation-like NAT -defined I -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of I
(I,A,B,f) . g is set
f -' B is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
(f -' B) + g is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
((f -' B) + g) + 1 is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
A . (((f -' B) + g) + 1) is set
(B -' 1) - (B -' 1) is V35() V36() ext-real set
g - (B -' 1) is V35() V36() ext-real set
g -' (B -' 1) is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
(B -' 1) + 1 is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
1 - 1 is V35() V36() ext-real set
B - 1 is V35() V36() ext-real set
B - B is V35() V36() ext-real set
f - B is V35() V36() ext-real set
len (A /^ f) is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
((len A) - f) + (B - 1) is V35() V36() ext-real set
dom (A /^ f) is Element of bool NAT
len (A | (B -' 1)) is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
(A /^ f) . (g - (B -' 1)) is set
1 - B is V35() V36() ext-real set
g + (1 - B) is V35() V36() ext-real set
f + (g + (1 - B)) is V35() V36() ext-real set
A . (f + (g + (1 - B))) is set
F3() is set
F1() is set
F4() is Relation-like NAT -defined F3() -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of F3()
F4() . 1 is set
F2() is set
len F4() is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
F4() . (len F4()) is set
rng F4() is Element of bool F3()
bool F3() is non empty set
I is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
F4() . I is set
I + 1 is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
F4() . (I + 1) is set
I is V14() V15() V16() V20() V35() V36() ext-real non negative set
A is Relation-like NAT -defined F3() -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of F3()
len A is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
A . 1 is set
A . (len A) is set
rng A is Element of bool F3()
A is Relation-like NAT -defined F3() -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of F3()
len A is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
A . 1 is set
A . (len A) is set
rng A is Element of bool F3()
dom A is Element of bool NAT
B is set
f is set
A . B is set
A . f is set
g is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
g is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
g + 1 is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
(F3(),A,(g + 1),g) is Relation-like NAT -defined F3() -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of F3()
(g + 1) -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
A | ((g + 1) -' 1) is Relation-like NAT -defined F3() -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of F3()
A /^ g is Relation-like NAT -defined F3() -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of F3()
(A | ((g + 1) -' 1)) ^ (A /^ g) is Relation-like NAT -defined F3() -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of F3()
g - (g + 1) is V35() V36() ext-real set
rng (F3(),A,(g + 1),g) is Element of bool F3()
len (F3(),A,(g + 1),g) is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
u is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
(F3(),A,(g + 1),g) . u is set
u + 1 is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
(F3(),A,(g + 1),g) . (u + 1) is set
(g + 1) - 1 is V35() V36() ext-real set
A . (u + 1) is set
A . u is set
(len A) - (len A) is V35() V36() ext-real set
((len A) - (len A)) + (g + 1) is V35() V36() ext-real set
(((len A) - (len A)) + (g + 1)) - 1 is V35() V36() ext-real set
(len A) - g is V35() V36() ext-real set
(len A) -' g is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
{} + 1 is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
1 - 1 is V35() V36() ext-real set
((len A) -' g) - 1 is V35() V36() ext-real set
((len A) - g) - 1 is V35() V36() ext-real set
(u + 1) + {} is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
(u + 1) + (((len A) - g) - 1) is V35() V36() ext-real set
(u + 1) + ((len A) - g) is V35() V36() ext-real set
((u + 1) + ((len A) - g)) - 1 is V35() V36() ext-real set
g -' (g + 1) is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
(g -' (g + 1)) + (u + 1) is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
((g -' (g + 1)) + (u + 1)) + 1 is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
A . (((g -' (g + 1)) + (u + 1)) + 1) is set
g + 1 is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
A . (g + 1) is set
(g + 1) - 1 is V35() V36() ext-real set
A . g is set
(len A) - g is V35() V36() ext-real set
((len A) - g) + (g + 1) is V35() V36() ext-real set
(((len A) - g) + (g + 1)) - 1 is V35() V36() ext-real set
(len A) -' g is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
((len A) -' g) + (g + 1) is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
(((len A) -' g) + (g + 1)) - 1 is V35() V36() ext-real set
((len A) -' g) + g is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
((len A) - g) + g is V35() V36() ext-real set
(((len A) - g) + g) + 1 is V35() V36() ext-real set
((((len A) - g) + g) + 1) - 1 is V35() V36() ext-real set
(((len A) -' g) + g) + 1 is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
((((len A) -' g) + g) + 1) - 1 is V35() V36() ext-real set
(((len A) - g) + g) - g is V35() V36() ext-real set
u - g is V35() V36() ext-real set
((len A) - g) + g is V35() V36() ext-real set
(u - g) + g is V35() V36() ext-real set
g - g is V35() V36() ext-real set
(g - g) - 1 is V35() V36() ext-real set
((g - g) - 1) + u is V35() V36() ext-real set
(((g - g) - 1) + u) + 1 is V35() V36() ext-real set
g -' (g + 1) is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
(g -' (g + 1)) + u is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
((g -' (g + 1)) + u) + 1 is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
(g -' (g + 1)) + (u + 1) is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
((g -' (g + 1)) + (u + 1)) + 1 is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
A . (((g -' (g + 1)) + (u + 1)) + 1) is set
(((g -' (g + 1)) + u) + 1) + 1 is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
A . ((((g -' (g + 1)) + u) + 1) + 1) is set
A . (((g -' (g + 1)) + u) + 1) is set
(F3(),A,(g + 1),g) . (len (F3(),A,(g + 1),g)) is set
{} + 1 is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
(g + 1) - 1 is V35() V36() ext-real set
A . (len (F3(),A,(g + 1),g)) is set
(len A) - g is V35() V36() ext-real set
((len A) - g) + (g + 1) is V35() V36() ext-real set
(((len A) - g) + (g + 1)) - 1 is V35() V36() ext-real set
((len A) - g) + g is V35() V36() ext-real set
(((len A) - g) + g) + 1 is V35() V36() ext-real set
((((len A) - g) + g) + 1) - 1 is V35() V36() ext-real set
(len A) - g is V35() V36() ext-real set
((len A) - g) + (g + 1) is V35() V36() ext-real set
(((len A) - g) + (g + 1)) - 1 is V35() V36() ext-real set
g -' (g + 1) is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
(g -' (g + 1)) + ((((len A) - g) + (g + 1)) - 1) is V35() V36() ext-real set
((g -' (g + 1)) + ((((len A) - g) + (g + 1)) - 1)) + 1 is V35() V36() ext-real set
A . (((g -' (g + 1)) + ((((len A) - g) + (g + 1)) - 1)) + 1) is set
((len A) - g) - 1 is V35() V36() ext-real set
(g + 1) + (((len A) - g) - 1) is V35() V36() ext-real set
(g - (g + 1)) + ((g + 1) + (((len A) - g) - 1)) is V35() V36() ext-real set
((g - (g + 1)) + ((g + 1) + (((len A) - g) - 1))) + 1 is V35() V36() ext-real set
A . (((g - (g + 1)) + ((g + 1) + (((len A) - g) - 1))) + 1) is set
(g + 1) - 1 is V35() V36() ext-real set
(F3(),A,(g + 1),g) . 1 is set
g - g is V35() V36() ext-real set
- (g - g) is V35() V36() ext-real set
- (- (g - g)) is V35() V36() ext-real set
(len A) + {} is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
(len A) + (- (g - g)) is V35() V36() ext-real set
(len A) - g is V35() V36() ext-real set
((len A) - g) + (g + 1) is V35() V36() ext-real set
(((len A) - g) + (g + 1)) - 1 is V35() V36() ext-real set
u is Relation-like NAT -defined F3() -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of F3()
len u is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
u . 1 is set
u . (len u) is set
rng u is Element of bool F3()
g is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
g is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
g + 1 is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
(F3(),A,(g + 1),g) is Relation-like NAT -defined F3() -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of F3()
(g + 1) -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
A | ((g + 1) -' 1) is Relation-like NAT -defined F3() -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of F3()
A /^ g is Relation-like NAT -defined F3() -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of F3()
(A | ((g + 1) -' 1)) ^ (A /^ g) is Relation-like NAT -defined F3() -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of F3()
g - (g + 1) is V35() V36() ext-real set
rng (F3(),A,(g + 1),g) is Element of bool F3()
len (F3(),A,(g + 1),g) is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
u is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
(F3(),A,(g + 1),g) . u is set
u + 1 is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
(F3(),A,(g + 1),g) . (u + 1) is set
(g + 1) - 1 is V35() V36() ext-real set
A . (u + 1) is set
A . u is set
(len A) - (len A) is V35() V36() ext-real set
((len A) - (len A)) + (g + 1) is V35() V36() ext-real set
(((len A) - (len A)) + (g + 1)) - 1 is V35() V36() ext-real set
(len A) - g is V35() V36() ext-real set
(len A) -' g is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
{} + 1 is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
1 - 1 is V35() V36() ext-real set
((len A) -' g) - 1 is V35() V36() ext-real set
((len A) - g) - 1 is V35() V36() ext-real set
(u + 1) + {} is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
(u + 1) + (((len A) - g) - 1) is V35() V36() ext-real set
(u + 1) + ((len A) - g) is V35() V36() ext-real set
((u + 1) + ((len A) - g)) - 1 is V35() V36() ext-real set
g -' (g + 1) is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
(g -' (g + 1)) + (u + 1) is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
((g -' (g + 1)) + (u + 1)) + 1 is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
A . (((g -' (g + 1)) + (u + 1)) + 1) is set
g + 1 is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
A . (g + 1) is set
(g + 1) - 1 is V35() V36() ext-real set
A . g is set
(len A) - g is V35() V36() ext-real set
((len A) - g) + (g + 1) is V35() V36() ext-real set
(((len A) - g) + (g + 1)) - 1 is V35() V36() ext-real set
(len A) -' g is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
((len A) -' g) + (g + 1) is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
(((len A) -' g) + (g + 1)) - 1 is V35() V36() ext-real set
((len A) -' g) + g is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
((len A) - g) + g is V35() V36() ext-real set
(((len A) - g) + g) + 1 is V35() V36() ext-real set
((((len A) - g) + g) + 1) - 1 is V35() V36() ext-real set
(((len A) -' g) + g) + 1 is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
((((len A) -' g) + g) + 1) - 1 is V35() V36() ext-real set
(((len A) - g) + g) - g is V35() V36() ext-real set
u - g is V35() V36() ext-real set
((len A) - g) + g is V35() V36() ext-real set
(u - g) + g is V35() V36() ext-real set
g - g is V35() V36() ext-real set
(g - g) - 1 is V35() V36() ext-real set
((g - g) - 1) + u is V35() V36() ext-real set
(((g - g) - 1) + u) + 1 is V35() V36() ext-real set
g -' (g + 1) is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
(g -' (g + 1)) + u is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
((g -' (g + 1)) + u) + 1 is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
(g -' (g + 1)) + (u + 1) is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
((g -' (g + 1)) + (u + 1)) + 1 is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
A . (((g -' (g + 1)) + (u + 1)) + 1) is set
(((g -' (g + 1)) + u) + 1) + 1 is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
A . ((((g -' (g + 1)) + u) + 1) + 1) is set
A . (((g -' (g + 1)) + u) + 1) is set
(F3(),A,(g + 1),g) . (len (F3(),A,(g + 1),g)) is set
{} + 1 is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
(g + 1) - 1 is V35() V36() ext-real set
A . (len (F3(),A,(g + 1),g)) is set
(len A) - g is V35() V36() ext-real set
((len A) - g) + (g + 1) is V35() V36() ext-real set
(((len A) - g) + (g + 1)) - 1 is V35() V36() ext-real set
((len A) - g) + g is V35() V36() ext-real set
(((len A) - g) + g) + 1 is V35() V36() ext-real set
((((len A) - g) + g) + 1) - 1 is V35() V36() ext-real set
(len A) - g is V35() V36() ext-real set
((len A) - g) + (g + 1) is V35() V36() ext-real set
(((len A) - g) + (g + 1)) - 1 is V35() V36() ext-real set
g -' (g + 1) is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
(g -' (g + 1)) + ((((len A) - g) + (g + 1)) - 1) is V35() V36() ext-real set
((g -' (g + 1)) + ((((len A) - g) + (g + 1)) - 1)) + 1 is V35() V36() ext-real set
A . (((g -' (g + 1)) + ((((len A) - g) + (g + 1)) - 1)) + 1) is set
((len A) - g) - 1 is V35() V36() ext-real set
(g + 1) + (((len A) - g) - 1) is V35() V36() ext-real set
(g - (g + 1)) + ((g + 1) + (((len A) - g) - 1)) is V35() V36() ext-real set
((g - (g + 1)) + ((g + 1) + (((len A) - g) - 1))) + 1 is V35() V36() ext-real set
A . (((g - (g + 1)) + ((g + 1) + (((len A) - g) - 1))) + 1) is set
(g + 1) - 1 is V35() V36() ext-real set
(F3(),A,(g + 1),g) . 1 is set
g - g is V35() V36() ext-real set
- (g - g) is V35() V36() ext-real set
- (- (g - g)) is V35() V36() ext-real set
(len A) + {} is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
(len A) + (- (g - g)) is V35() V36() ext-real set
(len A) - g is V35() V36() ext-real set
((len A) - g) + (g + 1) is V35() V36() ext-real set
(((len A) - g) + (g + 1)) - 1 is V35() V36() ext-real set
u is Relation-like NAT -defined F3() -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of F3()
len u is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
u . 1 is set
u . (len u) is set
rng u is Element of bool F3()
g is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
g is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
I is non empty set
A is Relation-like I -defined Function-like total 1-sorted-yielding set
Carrier A is Relation-like I -defined Function-like total set
B is Relation-like I -defined Function-like total ManySortedSubset of Carrier A
f is Element of I
A . f is 1-sorted
the carrier of (A . f) is set
bool the carrier of (A . f) is non empty set
g is Element of bool the carrier of (A . f)
B +* (f,g) is Relation-like I -defined Function-like total set
dom B is Element of bool I
bool I is non empty set
g is set
(B +* (f,g)) . g is set
(Carrier A) . g is set
o is Element of I
(B +* (f,g)) . o is set
A . o is 1-sorted
the carrier of (A . o) is set
o is Element of I
B . o is set
I is non empty set
A is Relation-like I -defined Function-like total 1-sorted-yielding V226() TopStruct-yielding non-Trivial-yielding set
Segre_Product A is non empty TopStruct
Carrier A is Relation-like I -defined Function-like total 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
the carrier of (Segre_Product A) is non empty set
bool the carrier of (Segre_Product A) is non empty set
the Relation-like non-empty I -defined Function-like total non trivial-yielding Segre-like ManySortedSubset of Carrier A is Relation-like non-empty I -defined Function-like total non trivial-yielding Segre-like ManySortedSubset of Carrier A
indx the Relation-like non-empty I -defined Function-like total non trivial-yielding Segre-like ManySortedSubset of Carrier A is Element of I
A . (indx the Relation-like non-empty I -defined Function-like total non trivial-yielding Segre-like ManySortedSubset of Carrier A) is TopStruct
[#] (A . (indx the Relation-like non-empty I -defined Function-like total non trivial-yielding Segre-like ManySortedSubset of Carrier A)) is non proper Element of bool the carrier of (A . (indx the Relation-like non-empty I -defined Function-like total non trivial-yielding Segre-like ManySortedSubset of Carrier A))
the carrier of (A . (indx the Relation-like non-empty I -defined Function-like total non trivial-yielding Segre-like ManySortedSubset of Carrier A)) is set
bool the carrier of (A . (indx the Relation-like non-empty I -defined Function-like total non trivial-yielding Segre-like ManySortedSubset of Carrier A)) is non empty set
the Relation-like non-empty I -defined Function-like total non trivial-yielding Segre-like ManySortedSubset of Carrier A +* ((indx the Relation-like non-empty I -defined Function-like total non trivial-yielding Segre-like ManySortedSubset of Carrier A),([#] (A . (indx the Relation-like non-empty I -defined Function-like total non trivial-yielding Segre-like ManySortedSubset of Carrier A)))) is Relation-like I -defined Function-like total set
dom (Carrier A) is Element of bool I
bool I is non empty set
dom A is Element of bool I
rng A is set
f is Relation-like I -defined Function-like total ManySortedSubset of Carrier A
g is Relation-like non-empty I -defined Function-like total non trivial-yielding Segre-like ManySortedSubset of Carrier A
g is set
g . g is set
(Carrier A) . g is set
dom g is Element of bool I
product g is non empty non trivial set
g is Element of bool the carrier of (Segre_Product A)
dom the Relation-like non-empty I -defined Function-like total non trivial-yielding Segre-like ManySortedSubset of Carrier A is Element of bool I
g . (indx the Relation-like non-empty I -defined Function-like total non trivial-yielding Segre-like ManySortedSubset of Carrier A) is set
indx g is Element of I
I is non empty set
A is Relation-like I -defined Function-like total 1-sorted-yielding V226() TopStruct-yielding non-Trivial-yielding set
Segre_Product A is non empty TopStruct
Carrier A is Relation-like I -defined Function-like total 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
the carrier of (Segre_Product A) is non empty set
B is (I,A)
f is (I,A)
B /\ f is Element of bool the carrier of (Segre_Product A)
bool the carrier of (Segre_Product A) is non empty set
card (B /\ f) is cardinal set
g is Relation-like non-empty I -defined Function-like total non trivial-yielding Segre-like ManySortedSubset of Carrier A
product g is non empty non trivial set
indx g is Element of I
g . (indx g) is set
A . (indx g) is TopStruct
[#] (A . (indx g)) is non proper Element of bool the carrier of (A . (indx g))
the carrier of (A . (indx g)) is set
bool the carrier of (A . (indx g)) is non empty set
g is Relation-like non-empty I -defined Function-like total non trivial-yielding Segre-like ManySortedSubset of Carrier A
product g is non empty non trivial set
indx g is Element of I
g . (indx g) is set
A . (indx g) is TopStruct
[#] (A . (indx g)) is non proper Element of bool the carrier of (A . (indx g))
the carrier of (A . (indx g)) is set
bool the carrier of (A . (indx g)) is non empty set
o is set
g . o is set
g . o is set
g . o is set
g . o is set
dom g is Element of bool I
bool I is non empty set
dom g is Element of bool I
I is TopStruct
the carrier of I is set
bool the carrier of I is non empty set
I is TopStruct
the carrier of I is set
bool the carrier of I is non empty set
A is Element of bool the carrier of I
B is Element of bool the carrier of I
f is Relation-like NAT -defined bool the carrier of I -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of bool the carrier of I
f . 1 is set
len f is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
f . (len f) is set
rng f is Element of bool (bool the carrier of I)
bool (bool the carrier of I) is non empty set
g is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
g is set
f . g is set
o is set
g + 1 is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
f . (g + 1) is set
g /\ o is set
card (g /\ o) is cardinal set
g is Relation-like NAT -defined bool the carrier of I -valued Function-like one-to-one V24() FinSequence-like FinSubsequence-like V187() FinSequence of bool the carrier of I
g . 1 is set
len g is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
g . (len g) is set
rng g is Element of bool (bool the carrier of I)
g is Element of bool the carrier of I
o is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
g . o is set
o + 1 is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
g . (o + 1) is set
(g . o) /\ (g . (o + 1)) is set
card ((g . o) /\ (g . (o + 1))) is cardinal set
I is TopStruct
the carrier of I is set
bool the carrier of I is non empty set
A is Element of bool the carrier of I
<*A*> is Relation-like NAT -defined bool the carrier of I -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like V187() FinSequence of bool the carrier of I
B is Relation-like NAT -defined bool the carrier of I -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of bool the carrier of I
B . 1 is set
len B is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
B . (len B) is set
rng B is Element of bool (bool the carrier of I)
bool (bool the carrier of I) is non empty set
f is Element of bool the carrier of I
{A} is non empty trivial set
f is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
B . f is set
f + 1 is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
B . (f + 1) is set
(B . f) /\ (B . (f + 1)) is set
card ((B . f) /\ (B . (f + 1))) is cardinal set
I is non empty set
A is Relation-like I -defined Function-like total 1-sorted-yielding V226() 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
Carrier A is Relation-like I -defined Function-like total 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
the carrier of (Segre_Product A) is non empty set
bool the carrier of (Segre_Product A) is non empty set
B is Element of bool the carrier of (Segre_Product A)
f is Element of bool the carrier of (Segre_Product A)
g is Relation-like NAT -defined bool the carrier of (Segre_Product A) -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of bool the carrier of (Segre_Product A)
g . 1 is set
len g is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
g . (len g) is set
rng g is Element of bool (bool the carrier of (Segre_Product A))
bool (bool the carrier of (Segre_Product A)) is non empty set
dom g is Element of bool NAT
o is Relation-like non-empty I -defined Function-like total non trivial-yielding Segre-like ManySortedSubset of Carrier A
product o is non empty non trivial set
indx o is Element of I
A . (indx o) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . (indx o)) is non empty set
bool the carrier of (A . (indx o)) is non empty set
o . (indx o) is set
u is Relation-like non-empty I -defined Function-like total non trivial-yielding Segre-like ManySortedSubset of Carrier A
product u is non empty non trivial set
Y is Relation-like non-empty I -defined Function-like total non trivial-yielding Segre-like ManySortedSubset of Carrier A
product Y is non empty non trivial set
indx u is Element of I
indx Y is Element of I
Y is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
g . Y is set
Y + 1 is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
g . (Y + 1) is set
VV is Element of bool the carrier of (Segre_Product A)
X is Element of bool the carrier of (Segre_Product A)
VV /\ X is Element of bool the carrier of (Segre_Product A)
card (VV /\ X) is cardinal set
card VV is cardinal set
X is Relation-like non-empty I -defined Function-like total non trivial-yielding Segre-like ManySortedSubset of Carrier A
product X is non empty non trivial set
indx X is Element of I
A . (indx X) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . (indx X)) is non empty set
bool the carrier of (A . (indx X)) is non empty set
X . (indx X) is set
pX is Relation-like non-empty I -defined Function-like total non trivial-yielding Segre-like ManySortedSubset of Carrier A
product pX is non empty non trivial set
indx pX is Element of I
psX is set
u . psX is set
pX . psX is set
X . psX is set
pX is Relation-like non-empty I -defined Function-like total non trivial-yielding Segre-like ManySortedSubset of Carrier A
product pX is non empty non trivial set
indx pX is Element of I
psX is set
u . psX is set
pX . psX is set
Y is Relation-like non-empty I -defined Function-like total non trivial-yielding Segre-like ManySortedSubset of Carrier A
product Y is non empty non trivial set
indx Y is Element of I
VV is set
u . VV is set
Y . VV is set
Y is set
u . Y is set
Y . Y is set
I is 1-sorted
the carrier of I is set
A is non empty 1-sorted
the carrier of A is non empty set
[: the carrier of I, the carrier of A:] is set
bool [: the carrier of I, the carrier of A:] is non empty set
B is Relation-like the carrier of I -defined the carrier of A -valued Function-like total quasi_total Element of bool [: the carrier of I, the carrier of A:]
B " is Relation-like the carrier of A -defined the carrier of I -valued Function-like quasi_total Element of bool [: the carrier of A, the carrier of I:]
[: the carrier of A, the carrier of I:] is set
bool [: the carrier of A, the carrier of I:] is non empty set
rng B is Element of bool the carrier of A
bool the carrier of A is non empty set
[#] A is non empty non proper Element of bool the carrier of A
rng (B ") is Element of bool the carrier of I
bool the carrier of I is non empty set
[#] I is non proper Element of bool the carrier of I
I is TopStruct
the carrier of I is set
A is TopStruct
the carrier of A is set
[: the carrier of I, the carrier of A:] is set
bool [: the carrier of I, the carrier of A:] is non empty set
I is non empty TopStruct
the carrier of I is non empty set
[: the carrier of I, the carrier of I:] is non empty set
bool [: the carrier of I, the carrier of I:] is non empty set
id I is Relation-like the carrier of I -defined the carrier of I -valued Function-like non empty total quasi_total V62(I,I) open Element of bool [: the carrier of I, the carrier of I:]
id the carrier of I is Relation-like the carrier of I -defined the carrier of I -valued Function-like one-to-one non empty total quasi_total onto bijective V76() V78() V79() V83() Element of bool [: the carrier of I, the carrier of I:]
A is Relation-like the carrier of I -defined the carrier of I -valued Function-like non empty total quasi_total V62(I,I) open Element of bool [: the carrier of I, the carrier of I:]
A " is Relation-like the carrier of I -defined the carrier of I -valued Function-like non empty total quasi_total Element of bool [: the carrier of I, the carrier of I:]
I is non empty non void TopStruct
the carrier of I is non empty set
[: the carrier of I, the carrier of I:] is non empty set
bool [: the carrier of I, the carrier of I:] is non empty set
the topology of I is non empty Element of bool (bool the carrier of I)
bool the carrier of I is non empty set
bool (bool the carrier of I) is non empty set
A is Relation-like the carrier of I -defined the carrier of I -valued Function-like non empty total quasi_total (I,I) Element of bool [: the carrier of I, the carrier of I:]
B is Element of the topology of I
A .: B is set
f is Element of bool the carrier of I
A .: f is Element of bool the carrier of I
I is non empty non void TopStruct
the carrier of I is non empty set
[: the carrier of I, the carrier of I:] is non empty set
bool [: the carrier of I, the carrier of I:] is non empty set
the topology of I is non empty Element of bool (bool the carrier of I)
bool the carrier of I is non empty set
bool (bool the carrier of I) is non empty set
A is Relation-like the carrier of I -defined the carrier of I -valued Function-like non empty total quasi_total (I,I) Element of bool [: the carrier of I, the carrier of I:]
B is Element of the topology of I
A " B is set
f is Element of bool the carrier of I
A " is Relation-like the carrier of I -defined the carrier of I -valued Function-like non empty total quasi_total Element of bool [: the carrier of I, the carrier of I:]
A " is Relation-like Function-like set
(A ") .: f is Element of bool the carrier of I
A " f is Element of bool the carrier of I
I is non empty TopStruct
the carrier of I is non empty set
[: the carrier of I, the carrier of I:] is 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 total quasi_total (I,I) Element of bool [: the carrier of I, the carrier of I:]
A " is Relation-like the carrier of I -defined the carrier of I -valued Function-like non empty total quasi_total Element of bool [: the carrier of I, the carrier of I:]
rng A is Element of bool the carrier of I
bool the carrier of I is non empty set
[#] I is non empty non proper Element of bool the carrier of I
(A ") " is Relation-like the carrier of I -defined the carrier of I -valued Function-like non empty total quasi_total Element of bool [: the carrier of I, the carrier of I:]
I is non empty TopStruct
the carrier of I is non empty set
[: the carrier of I, the carrier of I:] is non empty set
bool [: the carrier of I, the carrier of I:] is non empty set
bool 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 total quasi_total (I,I) Element of bool [: the carrier of I, the carrier of I:]
B is Element of bool the carrier of I
A .: B is Element of bool the carrier of I
card B is cardinal set
f is set
g is set
dom A is Element of bool the carrier of I
A . f is set
A . g is set
card (A .: B) is cardinal set
I is non empty TopStruct
the carrier of I is non empty set
[: the carrier of I, the carrier of I:] is non empty set
bool [: the carrier of I, the carrier of I:] is non empty set
bool 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 total quasi_total (I,I) Element of bool [: the carrier of I, the carrier of I:]
B is Element of bool the carrier of I
A " B is Element of bool the carrier of I
card B is cardinal set
f is set
g is set
rng A is Element of bool the carrier of I
dom A is Element of bool the carrier of I
g is set
A . g is set
o is set
A . o is set
card (A " B) is cardinal set
I is non empty non void TopStruct
the carrier of I is non empty set
[: the carrier of I, the carrier of I:] is non empty set
bool [: the carrier of I, the carrier of I:] is non empty set
bool 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 total quasi_total (I,I) Element of bool [: the carrier of I, the carrier of I:]
B is Element of bool the carrier of I
A .: B is Element of bool the carrier of I
f is Element of the carrier of I
g is Element of the carrier of I
dom A is Element of bool the carrier of I
g is set
A . g is set
o is set
A . o is set
u is Element of the carrier of I
Y 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
{u,Y} is non empty set
Y is Element of the topology of I
(I,A,Y) is Element of the topology of I
{f,g} is non empty set
I is non empty non void TopStruct
the carrier of I is non empty set
[: the carrier of I, the carrier of I:] is non empty set
bool [: the carrier of I, the carrier of I:] is non empty set
bool 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 total quasi_total (I,I) Element of bool [: the carrier of I, the carrier of I:]
A " is Relation-like the carrier of I -defined the carrier of I -valued Function-like non empty total quasi_total Element of bool [: the carrier of I, the carrier of I:]
f is Element of bool the carrier of I
A " f is Element of bool the carrier of I
B is Relation-like the carrier of I -defined the carrier of I -valued Function-like non empty total quasi_total (I,I) Element of bool [: the carrier of I, the carrier of I:]
B .: f is Element of bool the carrier of I
rng A is Element of bool the carrier of I
[#] I is non empty non proper Element of bool the carrier of I
I is non empty non void TopStruct
the carrier of I is non empty set
[: the carrier of I, the carrier of I:] is non empty set
bool [: the carrier of I, the carrier of I:] is non empty set
bool 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 total quasi_total (I,I) Element of bool [: the carrier of I, the carrier of I:]
B is Element of bool the carrier of I
A .: B is Element of bool 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 is Element of the topology of I
f /\ (A .: B) is Element of bool the carrier of I
card (f /\ (A .: B)) is cardinal set
g is set
g is set
dom A is Element of bool the carrier of I
o is set
A . o is set
(I,A,f) is Element of the topology of I
(I,A,f) /\ B is Element of bool the carrier of I
u is set
A . u is set
card ((I,A,f) /\ B) is cardinal set
(I,A,(I,A,f)) is Element of the topology of I
rng A is Element of bool the carrier of I
I is non empty non void TopStruct
the carrier of I is non empty set
[: the carrier of I, the carrier of I:] is non empty set
bool [: the carrier of I, the carrier of I:] is non empty set
bool 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 total quasi_total (I,I) Element of bool [: the carrier of I, the carrier of I:]
A " is Relation-like the carrier of I -defined the carrier of I -valued Function-like non empty total quasi_total Element of bool [: the carrier of I, the carrier of I:]
f is Element of bool the carrier of I
A " f is Element of bool the carrier of I
B is Relation-like the carrier of I -defined the carrier of I -valued Function-like non empty total quasi_total (I,I) Element of bool [: the carrier of I, the carrier of I:]
B .: f is Element of bool the carrier of I
rng A is Element of bool the carrier of I
[#] I is non empty non proper Element of bool the carrier of I
I is non empty non void TopStruct
the carrier of I is non empty set
[: the carrier of I, the carrier of I:] is non empty set
bool [: the carrier of I, the carrier of I:] is non empty set
bool 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 total quasi_total (I,I) Element of bool [: the carrier of I, the carrier of I:]
B is Element of bool the carrier of I
f is Element of bool the carrier of I
A .: B is Element of bool the carrier of I
A .: f is Element of bool the carrier of I
g is Relation-like NAT -defined bool the carrier of I -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of bool the carrier of I
g . 1 is set
len g is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
g . (len g) is set
rng g is Element of bool (bool the carrier of I)
bool (bool the carrier of I) is non empty set
g is Relation-like NAT -defined Function-like V24() FinSequence-like FinSubsequence-like V187() set
len g is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
dom g is Element of bool NAT
dom g is Element of bool NAT
Seg (len g) is V24() len g -element Element of bool NAT
Seg (len g) is V24() len g -element Element of bool NAT
rng g is set
o is set
u is set
g . u is set
Y is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
g . Y is set
g . Y is set
Y is Element of bool the carrier of I
A .: Y is Element of bool the carrier of I
o is Relation-like NAT -defined bool the carrier of I -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of bool the carrier of I
o . 1 is set
len o is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
o . (len o) is set
rng o is Element of bool (bool the carrier of I)
u is Element of bool the carrier of I
dom o is Element of bool NAT
Y is set
o . Y is set
Y is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
g . Y is set
VV is Element of bool the carrier of I
o . Y is set
A .: VV is Element of bool the carrier of I
u is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
o . u is set
u + 1 is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
o . (u + 1) is set
(o . u) /\ (o . (u + 1)) is set
card ((o . u) /\ (o . (u + 1))) is cardinal set
g . u is set
g . (u + 1) is set
(g . u) /\ (g . (u + 1)) is set
card ((g . u) /\ (g . (u + 1))) is cardinal set
Y is Element of bool the carrier of I
A .: Y is Element of bool the carrier of I
A .: (g . u) is Element of bool the carrier of I
A .: (g . (u + 1)) is Element of bool the carrier of I
(A .: (g . u)) /\ (A .: (g . (u + 1))) is Element of bool the carrier of I
dom o is Element of bool 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 non empty set
bool [: the carrier of I, the carrier of I:] is non empty set
bool 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 total quasi_total (I,I) Element of bool [: the carrier of I, the carrier of I:]
B is Element of bool the carrier of I
f is Element of bool the carrier of I
A " B is Element of bool the carrier of I
A " f is Element of bool the carrier of I
A " is Relation-like the carrier of I -defined the carrier of I -valued Function-like non empty total quasi_total Element of bool [: the carrier of I, the carrier of I:]
rng A is Element of bool the carrier of I
[#] I is non empty non proper Element of bool the carrier of I
g is Relation-like the carrier of I -defined the carrier of I -valued Function-like non empty total quasi_total (I,I) Element of bool [: the carrier of I, the carrier of I:]
g .: f is Element of bool the carrier of I
g .: B is Element of bool the carrier of I
I is non empty set
A is Relation-like I -defined Function-like total 1-sorted-yielding V226() 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
Carrier A is Relation-like I -defined Function-like total 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
the carrier of (Segre_Product A) is non empty set
bool the carrier of (Segre_Product A) is non empty set
B is Element of bool the carrier of (Segre_Product A)
{ b1 where b1 is Element of bool the carrier of (Segre_Product A) : ( not b1 is trivial & b1 is strong & b1 is closed_under_lines & ( Segre_Product A,B,b1) ) } is set
union { b1 where b1 is Element of bool the carrier of (Segre_Product A) : ( not b1 is trivial & b1 is strong & b1 is closed_under_lines & ( Segre_Product A,B,b1) ) } is set
f is Relation-like non-empty I -defined Function-like total non trivial-yielding Segre-like ManySortedSubset of Carrier A
product f is non empty non trivial set
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
bool the carrier of (A . (indx f)) is non empty set
f . (indx f) is set
[#] (A . (indx f)) is non empty non proper Element of bool the carrier of (A . (indx f))
o is set
u is set
Y is Element of bool the carrier of (Segre_Product A)
dom A is Element of bool I
bool I is non empty set
rng A is set
f +* ((indx f),([#] (A . (indx f)))) is Relation-like I -defined Function-like total set
dom f is Element of bool I
u is Relation-like non-empty I -defined Function-like total non trivial-yielding Segre-like ManySortedSubset of Carrier A
u . (indx f) is set
indx u is Element of I
product u is non empty non trivial set
o is Element of bool the carrier of (Segre_Product A)
(Carrier A) . (indx f) is set
Y is set
dom u is Element of bool I
VV is Relation-like Function-like set
dom VV is set
X is Relation-like I -defined Function-like total set
X . (indx f) is set
Y is Element of bool the carrier of (A . (indx f))
X is Element of the carrier of (A . (indx f))
pX is Relation-like NAT -defined bool the carrier of (A . (indx f)) -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of bool the carrier of (A . (indx f))
pX . 1 is set
len pX is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
pX . (len pX) is set
rng pX is Element of bool (bool the carrier of (A . (indx f)))
bool (bool the carrier of (A . (indx f))) is non empty set
dom pX is Element of bool NAT
Seg (len pX) is V24() len pX -element Element of bool NAT
(len pX) - 1 is V35() V36() ext-real set
1 + 1 is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
2 - 1 is V35() V36() ext-real set
psX is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
pX . psX is set
psX + 1 is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
pX . (psX + 1) is set
(pX . psX) /\ (pX . (psX + 1)) is set
card ((pX . psX) /\ (pX . (psX + 1))) is cardinal set
card (pX . (psX + 1)) is cardinal set
(len pX) - {} is V35() V36() ext-real non negative set
psX is non empty non trivial set
u +* ((indx f),psX) is Relation-like I -defined Function-like total set
dom X is Element of bool I
u +* ((indx f),(pX . (len pX))) is Relation-like I -defined Function-like total set
dom (u +* ((indx f),(pX . (len pX)))) is Element of bool I
a is Relation-like NAT -defined Function-like V24() FinSequence-like FinSubsequence-like V187() set
len a is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
dom a is Element of bool NAT
rng a is set
g is set
dom (Carrier A) is Element of bool I
Yb is set
a . Yb is set
o is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
i is set
pX . o is set
u +* ((indx f),(pX . o)) is Relation-like I -defined Function-like total set
(u +* ((indx f),(pX . o))) . i is set
u . i is set
f . i is set
(Carrier A) . i is set
pX . o is set
u +* ((indx f),(pX . o)) is Relation-like I -defined Function-like total set
(u +* ((indx f),(pX . o))) . i is set
(Carrier A) . i is set
pX . o is set
u +* ((indx f),(pX . o)) is Relation-like I -defined Function-like total set
pX . o is set
u +* ((indx f),(pX . o)) is Relation-like I -defined Function-like total set
dom (u +* ((indx f),(pX . o))) is Element of bool I
product (u +* ((indx f),(pX . o))) is set
g is Relation-like NAT -defined bool the carrier of (Segre_Product A) -valued Function-like V24() FinSequence-like FinSubsequence-like V187() FinSequence of bool the carrier of (Segre_Product A)
dom g is Element of bool NAT
g . (len pX) is set
rng g is Element of bool (bool the carrier of (Segre_Product A))
bool (bool the carrier of (Segre_Product A)) is non empty set
o is set
u +* ((indx f),(pX . 1)) is Relation-like I -defined Function-like total set
(u +* ((indx f),(pX . 1))) . o is set
u . o is set
f . o is set
u +* ((indx f),(pX . 1)) is Relation-like I -defined Function-like total set
(u +* ((indx f),(pX . 1))) . o is set
f . o is set
u +* ((indx f),(pX . 1)) is Relation-like I -defined Function-like total set
u +* ((indx f),(pX . 1)) is Relation-like I -defined Function-like total set
o is Element of bool the carrier of (Segre_Product A)
i is set
g . i is set
a is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
pX . a is set
a + 1 is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
pX . (a + 1) is set
(pX . a) /\ (pX . (a + 1)) is set
card ((pX . a) /\ (pX . (a + 1))) is cardinal set
card (pX . a) is cardinal set
u +* ((indx f),(pX . a)) is Relation-like I -defined Function-like total set
l is set
(u +* ((indx f),(pX . a))) . l is set
(Carrier A) . l is set
u . l is set
b is non empty non trivial set
u +* ((indx f),b) is Relation-like I -defined Function-like total set
l is Relation-like non-empty I -defined Function-like total non trivial-yielding Segre-like ManySortedSubset of Carrier A
l is Relation-like non-empty I -defined Function-like total non trivial-yielding Segre-like ManySortedSubset of Carrier A
l . (indx f) is set
indx l is Element of I
A . (indx l) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . (indx l)) is non empty set
bool the carrier of (A . (indx l)) is non empty set
l1 is Element of bool the carrier of (A . (indx l))
l . (indx l) is set
g . a is set
product (u +* ((indx f),(pX . a))) is set
Yb is Element of bool the carrier of (Segre_Product A)
Z is Relation-like non-empty I -defined Function-like total non trivial-yielding Segre-like set
product Z is non empty non trivial set
len g is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
o is set
i is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
g . i is set
i + 1 is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT
g . (i + 1) is set
(g . i) /\ (g . (i + 1)) is set
card ((g . i) /\ (g . (i + 1))) is cardinal set
pX . i is set
u +* ((indx f),(pX . i)) is Relation-like I -defined Function-like total set
product (u +* ((indx f),(pX . i))) is set
pX . (i + 1) is set
(pX . i) /\ (pX . (i + 1)) is set
card ((pX . i) /\ (pX . (i + 1))) is cardinal set
a is set
b is set
l is Relation-like Function-like set
dom l is set
l is Relation-like I -defined Function-like total set
l +* ((indx f),a) is Relation-like I -defined Function-like total set
l +* ((indx f),b) is Relation-like I -defined Function-like total set
o is set
dom (u +* ((indx f),(pX . i))) is Element of bool I
dom l is Element of bool I
(l +* ((indx f),a)) . o is set
(u +* ((indx f),(pX . i))) . o is set
(l +* ((indx f),a)) . o is set
l . o is set
u . o is set
(u +* ((indx f),(pX . i))) . o is set
u +* ((indx f),(pX . (i + 1))) is Relation-like I -defined Function-like total set
product (u +* ((indx f),(pX . (i + 1)))) is set
o is set
(l +* ((indx f),b)) . o is set
(u +* ((indx f),(pX . i))) . o is set
(l +* ((indx f),b)) . o is set
l . o is set
u . o is set
(u +* ((indx f),(pX . i))) . o is set
o is set
dom (u +* ((indx f),(pX . (i + 1)))) is Element of bool I
(l +* ((indx f),a)) . o is set
(u +* ((indx f),(pX . (i + 1)))) . o is set
(l +* ((indx f),a)) . o is set
l . o is set
u . o is set
(u +* ((indx f),(pX . (i + 1)))) . o is set
dom (l +* ((indx f),a)) is Element of bool I
o is set
(l +* ((indx f),b)) . o is set
(u +* ((indx f),(pX . (i + 1)))) . o is set
(l +* ((indx f),b)) . o is set
l . o is set
u . o is set
(u +* ((indx f),(pX . (i + 1)))) . o is set
dom (l +* ((indx f),b)) is Element of bool I
(l +* ((indx f),a)) . (indx f) is set
o is set
X . o is set
(u +* ((indx f),(pX . (len pX)))) . o is set
X . o is set
u . o is set
(u +* ((indx f),(pX . (len pX)))) . o is set
dom (u +* ((indx f),(pX . 1))) is Element of bool I
g . 1 is set
product (u +* ((indx f),(pX . (len pX)))) is set
u . (indx u) is set
A . (indx u) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
[#] (A . (indx u)) is non empty non proper Element of bool the carrier of (A . (indx u))
the carrier of (A . (indx u)) is non empty set
bool the carrier of (A . (indx u)) is non empty set
Y is set
Y is set
VV is Element of bool the carrier of (Segre_Product A)
X is Relation-like non-empty I -defined Function-like total non trivial-yielding Segre-like ManySortedSubset of Carrier A
product X is non empty non trivial set
indx X is Element of I
A . (indx X) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . (indx X)) is non empty set
bool the carrier of (A . (indx X)) is non empty set
X . (indx X) is set
dom X is Element of bool I
dom u is Element of bool I
X is Relation-like I -defined Function-like total set
pX is set
X . pX is set
u . pX is set
psX is Element of I
X . psX is set
(Carrier A) . psX is set
A . psX is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
the carrier of (A . psX) is non empty set
X . pX is set
X . pX is set
f . pX is set
dom X is Element of bool I
I is non empty set
A is Relation-like I -defined Function-like total 1-sorted-yielding V226() 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
Carrier A is Relation-like I -defined Function-like total 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
the carrier of (Segre_Product A) is non empty set
bool the carrier of (Segre_Product A) is non empty set
B is set
f is (I,A)
g is Relation-like non-empty I -defined Function-like total non trivial-yielding Segre-like ManySortedSubset of Carrier A
product g is non empty non trivial set
indx g is Element of I
g . (indx g) is set
A . (indx g) is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct
[#] (A . (indx g)) is non empty non proper Element of bool the carrier of (A . (indx g))
the carrier of (A . (indx g)) is non empty set
bool the carrier of (A . (indx g)) is non empty set
the topology of (A . (indx g)) is non empty Element of bool (bool the carrier of (A . (indx g)))
bool (bool the carrier of (A . (indx g))) is non empty set
the Element of the topology of (A . (indx g)) is Element of the topology of (A . (indx g))
o is set
dom g is Element of bool I
bool I is non empty set
Y is Relation-like Function-like set
dom Y is set
Y is Relation-like I -defined Function-like total set
Y is set
Y . Y is set
(Carrier A) . Y is set
g . Y is set
VV is Relation-like Function-like set
dom VV is set
Y is Relation-like I -defined Function-like total Element of Carrier A
{Y} is Relation-like I -defined Function-like total trivial-yielding Segre-like set
VV is Relation-like I -defined Function-like total ManySortedSubset of Carrier A
u is Element of bool the carrier of (A . (indx g))
VV +* ((indx g),u) is Relation-like I -defined Function-like total set
card u is cardinal set
X is Relation-like I -defined Function-like total ManySortedSubset of Carrier A
dom VV is Element of bool I
X is Relation-like non-empty I -defined Function-like total non trivial-yielding Segre-like ManySortedSubset of Carrier A
X . (indx g) is set
indx X is Element of 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
product X is non empty non trivial set
psX is set
X . psX is set
g . psX is set
VV . psX is set
Y . psX is set
{(Y . psX)} is non empty trivial set
Z is Relation-like Function-like set
dom Z is set
pX is Element of the topology of (Segre_Product A)
psX is Element of bool the carrier of (Segre_Product A)
{ b1 where b1 is Element of bool the carrier of (Segre_Product A) : ( not b1 is trivial & b1 is strong & b1 is closed_under_lines & ( Segre_Product A,psX,b1) ) } is set
union { b1 where b1 is Element of bool the carrier of (Segre_Product A) : ( not b1 is trivial & b1 is strong & b1 is closed_under_lines & ( Segre_Product A,psX,b1) ) } is set
Z is (I,A)
a is set
dom X is Element of bool I
B /\ Z is Element of bool the carrier of (Segre_Product A)
card psX is cardinal set
card (B /\ Z) is cardinal set
card pX is cardinal set
f is Element of bool the carrier of (Segre_Product A)
{ b1 where b1 is Element of bool the carrier of (Segre_Product A) : ( not b1 is trivial & b1 is strong & b1 is closed_under_lines & ( Segre_Product A,f,b1) ) } is set
union { b1 where b1 is Element of bool the carrier of (Segre_Product A) : ( not b1 is trivial & b1 is strong & b1 is closed_under_lines & ( Segre_Product A,f,b1) ) } is set
I is non empty set
A is Relation-like I -defined Function-like total 1-sorted-yielding V226() 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
Carrier A is Relation-like I -defined Function-like total 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
the carrier of (Segre_Product A) is non empty set
[: the carrier of (Segre_Product A), the carrier of (Segre_Product A):] is non empty set
bool [: the carrier of (Segre_Product A), the carrier of (Segre_Product A):] is non empty set
B is (I,A)
bool the carrier of (Segre_Product A) is non empty set
f is Element of bool the carrier of (Segre_Product A)
{ b1 where b1 is Element of bool the carrier of (Segre_Product A) : ( not b1 is trivial & b1 is strong & b1 is closed_under_lines & ( Segre_Product A,f,b1) ) } is set
union { b1 where b1 is Element of bool the carrier of (Segre_Product A) : ( not b1 is trivial & b1 is strong & b1 is closed_under_lines & ( Segre_Product A,f,b1) ) } is set
g is Relation-like the carrier of (Segre_Product A) -defined the carrier of (Segre_Product A) -valued Function-like non empty total quasi_total ( Segre_Product A, Segre_Product A) Element of bool [: the carrier of (Segre_Product A), the carrier of (Segre_Product A):]
g .: B is Element of bool the carrier of (Segre_Product A)
g " is Relation-like the carrier of (Segre_Product A) -defined the carrier of (Segre_Product A) -valued Function-like non empty total quasi_total Element of bool [: the carrier of (Segre_Product A), the carrier of (Segre_Product A):]
dom g is Element of bool the carrier of (Segre_Product A)
g is Relation-like the carrier of (Segre_Product A) -defined the carrier of (Segre_Product A) -valued Function-like non empty total quasi_total ( Segre_Product A, Segre_Product A) Element of bool [: the carrier of (Segre_Product A), the carrier of (Segre_Product A):]
dom g is Element of bool the carrier of (Segre_Product A)
rng g is Element of bool the carrier of (Segre_Product A)
[#] (Segre_Product A) is non empty non proper Element of bool the carrier of (Segre_Product A)
g .: f is Element of bool the carrier of (Segre_Product A)
{ b1 where b1 is Element of bool the carrier of (Segre_Product A) : ( not b1 is trivial & b1 is strong & b1 is closed_under_lines & ( Segre_Product A,g .: f,b1) ) } is set
union { b1 where b1 is Element of bool the carrier of (Segre_Product A) : ( not b1 is trivial & b1 is strong & b1 is closed_under_lines & ( Segre_Product A,g .: f,b1) ) } is set
g " (g .: f) is Element of bool the carrier of (Segre_Product A)
o is set
u is set
g . u is set
Y is set
Y is Element of bool the carrier of (Segre_Product A)
g .: Y is Element of bool the carrier of (Segre_Product A)
o is set
u is set
Y is Element of bool the carrier of (Segre_Product A)
g .: Y is Element of bool the carrier of (Segre_Product A)
g .: (g .: f) is Element of bool the carrier of (Segre_Product A)
g . o is set
g " is Relation-like Function-like set
(g ") . o is set
g . ((g ") . o) is set
g . (g . o) is set
I is non empty set
A is Relation-like I -defined Function-like total 1-sorted-yielding V226() 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
Carrier A is Relation-like I -defined Function-like total 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
the carrier of (Segre_Product A) is non empty set
[: the carrier of (Segre_Product A), the carrier of (Segre_Product A):] is non empty set
bool [: the carrier of (Segre_Product A), the carrier of (Segre_Product A):] is non empty set
B is (I,A)
f is Relation-like the carrier of (Segre_Product A) -defined the carrier of (Segre_Product A) -valued Function-like non empty total quasi_total ( Segre_Product A, Segre_Product A) Element of bool [: the carrier of (Segre_Product A), the carrier of (Segre_Product A):]
f " B is Element of bool the carrier of (Segre_Product A)
bool 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 total quasi_total Element of bool [: the carrier of (Segre_Product A), the carrier of (Segre_Product A):]
rng f is Element of bool the carrier of (Segre_Product A)
[#] (Segre_Product A) is non empty non proper Element of bool the carrier of (Segre_Product A)
g is Relation-like the carrier of (Segre_Product A) -defined the carrier of (Segre_Product A) -valued Function-like non empty total quasi_total ( Segre_Product A, Segre_Product A) Element of bool [: the carrier of (Segre_Product A), the carrier of (Segre_Product A):]
g .: B is Element of bool the carrier of (Segre_Product A)