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

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 non empty trivial set

is non empty set
bool 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

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

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

(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

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

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

(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

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

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

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

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

(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

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

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

(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

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

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

(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

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

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

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

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

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

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

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

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

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

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)

dom B is Element of bool I
bool I is non empty set
g is set
(B +* (f,g)) . g is set
() . 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

Segre_Product A is non empty TopStruct

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

A . () is TopStruct
[#] (A . ()) is non proper Element of bool the carrier of (A . ())
the carrier of (A . ()) is set
bool the carrier of (A . ()) is non empty set
the Relation-like non-empty I -defined Function-like total non trivial-yielding Segre-like ManySortedSubset of Carrier A +* ((),([#] (A . ()))) is Relation-like I -defined Function-like total set
dom () is Element of bool I
bool I is non empty set
dom A is Element of bool I
rng A is set

g is set
g . g is set
() . 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 ()

g . () is set
indx g is Element of I
I is non empty set

Segre_Product A is non empty TopStruct

product () is set
Segre_Blocks A is Element of bool (bool (product ()))
bool (product ()) is non empty set
bool (bool (product ())) is non empty set
TopStruct(# (product ()),() #) is strict TopStruct
the carrier of () is non empty set
B is (I,A)
f is (I,A)
B /\ f is Element of bool the carrier of ()
bool the carrier of () is non empty set
card (B /\ f) is cardinal set

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

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

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

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

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 ())
bool (bool the carrier of ()) is non empty set
dom g is Element of bool NAT

product o is non empty non trivial set
indx o is Element of I

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

product u is non empty non trivial set

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 ()
X is Element of bool the carrier of ()
VV /\ X is Element of bool the carrier of ()
card (VV /\ X) is cardinal set
card VV is cardinal set

product X is non empty non trivial set
indx X is Element of I

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

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

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

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 ") .: 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

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

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

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

product () is set
Segre_Blocks A is Element of bool (bool (product ()))
bool (product ()) is non empty set
bool (bool (product ())) is non empty set
TopStruct(# (product ()),() #) is strict TopStruct
the carrier of () is non empty set
bool the carrier of () is non empty set
B is Element of bool the carrier of ()
{ b1 where b1 is Element of bool the carrier of () : ( 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 () : ( not b1 is trivial & b1 is strong & b1 is closed_under_lines & ( Segre_Product A,B,b1) ) } is set

product f is non empty non trivial set
indx f is Element of I

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 ()
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 . (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 ()
() . (indx f) is set
Y is set
dom u is Element of bool I

dom VV is 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

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

dom g is Element of bool NAT
g . (len pX) is set
rng g is Element of bool (bool the carrier of ())
bool (bool the carrier of ()) 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 ()
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
() . 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 . (indx f) is set
indx l is Element of I

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

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

dom l is 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 +* ((