:: PENCIL_2 semantic presentation

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

F

F

F

F

F

len F

F

rng F

bool F

I is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT

F

I + 1 is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT

F

I is V14() V15() V16() V20() V35() V36() ext-real non negative set

A is Relation-like NAT -defined F

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 F

A is Relation-like NAT -defined F

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 F

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

(F

(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 F

A /^ g is Relation-like NAT -defined F

(A | ((g + 1) -' 1)) ^ (A /^ g) is Relation-like NAT -defined F

g - (g + 1) is V35() V36() ext-real set

rng (F

len (F

u is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT

(F

u + 1 is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT

(F

(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

(F

{} + 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 (F

(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

(F

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 F

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 F

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

(F

(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 F

A /^ g is Relation-like NAT -defined F

(A | ((g + 1) -' 1)) ^ (A /^ g) is Relation-like NAT -defined F

g - (g + 1) is V35() V36() ext-real set

rng (F

len (F

u is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT

(F

u + 1 is non empty V14() V15() V16() V20() V35() V36() ext-real positive non negative Element of NAT

(F

(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

(F

{} + 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 (F

(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

(F

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 F

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 F

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)

{ b

union { b

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 +* ((