:: FINTOPO4 semantic presentation

REAL is set

NAT is non empty V4() V5() V6() Element of bool REAL

bool REAL is non empty set

COMPLEX is set

NAT is non empty V4() V5() V6() set

bool NAT is non empty set

bool NAT is non empty set

{} is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding functional V44() FinSequence-like FinSequence-membered set

1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

2 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

3 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

0 is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding functional V44() FinSequence-like FinSequence-membered Element of NAT

n is non empty RelStr

the carrier of n is non empty set

bool the carrier of n is non empty set

y is Element of bool the carrier of n

y ^b is Element of bool the carrier of n

{ b

i is Element of bool the carrier of n

i ^b is Element of bool the carrier of n

{ b

n is non empty reflexive RelStr

the carrier of n is non empty set

bool the carrier of n is non empty set

f is Element of bool the carrier of n

x is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

y is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

Finf (f,x) is Element of bool the carrier of n

Finf (f,y) is Element of bool the carrier of n

i is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

x + i is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

Finf (f,(x + i)) is Element of bool the carrier of n

i + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

x + (i + 1) is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

Finf (f,(x + (i + 1))) is Element of bool the carrier of n

(x + i) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

Finf (f,((x + i) + 1)) is Element of bool the carrier of n

y - x is V11() ext-real V44() set

y -' x is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

x + (y -' x) is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

x + (y - x) is V11() ext-real V44() set

x + 0 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

Finf (f,(x + 0)) is Element of bool the carrier of n

n is non empty reflexive RelStr

the carrier of n is non empty set

bool the carrier of n is non empty set

f is Element of bool the carrier of n

x is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

y is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

Fcl (f,x) is Element of bool the carrier of n

Fcl (f,y) is Element of bool the carrier of n

i is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

x + i is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

Fcl (f,(x + i)) is Element of bool the carrier of n

i + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

x + (i + 1) is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

Fcl (f,(x + (i + 1))) is Element of bool the carrier of n

(x + i) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

Fcl (f,((x + i) + 1)) is Element of bool the carrier of n

y - x is V11() ext-real V44() set

y -' x is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

x + (y -' x) is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

x + (y - x) is V11() ext-real V44() set

x + 0 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

Fcl (f,(x + 0)) is Element of bool the carrier of n

n is non empty reflexive RelStr

the carrier of n is non empty set

bool the carrier of n is non empty set

f is Element of bool the carrier of n

x is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

y is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

Fdfl (f,y) is Element of bool the carrier of n

Fdfl (f,x) is Element of bool the carrier of n

i is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

x + i is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

Fdfl (f,(x + i)) is Element of bool the carrier of n

i + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

x + (i + 1) is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

Fdfl (f,(x + (i + 1))) is Element of bool the carrier of n

(x + i) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

Fdfl (f,((x + i) + 1)) is Element of bool the carrier of n

y - x is V11() ext-real V44() set

y -' x is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

x + (y -' x) is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

x + (y - x) is V11() ext-real V44() set

x + 0 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

Fdfl (f,(x + 0)) is Element of bool the carrier of n

n is non empty reflexive RelStr

the carrier of n is non empty set

bool the carrier of n is non empty set

f is Element of bool the carrier of n

x is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

y is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

Fint (f,y) is Element of bool the carrier of n

Fint (f,x) is Element of bool the carrier of n

i is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

x + i is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

Fint (f,(x + i)) is Element of bool the carrier of n

i + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

x + (i + 1) is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

Fint (f,(x + (i + 1))) is Element of bool the carrier of n

(x + i) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

Fint (f,((x + i) + 1)) is Element of bool the carrier of n

y - x is V11() ext-real V44() set

y -' x is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

x + (y -' x) is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

x + (y - x) is V11() ext-real V44() set

x + 0 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

Fint (f,(x + 0)) is Element of bool the carrier of n

n is non empty RelStr

the carrier of n is non empty set

bool the carrier of n is non empty set

f is Element of bool the carrier of n

x is Element of bool the carrier of n

n is non empty reflexive RelStr

the carrier of n is non empty set

bool the carrier of n is non empty set

f is Element of bool the carrier of n

x is Element of bool the carrier of n

f ^b is Element of bool the carrier of n

{ b

n is non empty RelStr

the carrier of n is non empty set

bool the carrier of n is non empty set

f is Element of bool the carrier of n

x is Element of bool the carrier of n

f ^f is Element of bool the carrier of n

{ b

( b

x ^f is Element of bool the carrier of n

{ b

( b

f ^b is Element of bool the carrier of n

{ b

x ^b is Element of bool the carrier of n

{ b

n is non empty reflexive RelStr

the carrier of n is non empty set

bool the carrier of n is non empty set

f is Element of bool the carrier of n

f ^b is Element of bool the carrier of n

{ b

x is Element of bool the carrier of n

x ^b is Element of bool the carrier of n

{ b

y is set

i is Element of the carrier of n

U_FT i is Element of bool the carrier of n

the InternalRel of n is Relation-like the carrier of n -defined the carrier of n -valued Element of bool [: the carrier of n, the carrier of n:]

[: the carrier of n, the carrier of n:] is non empty Relation-like set

bool [: the carrier of n, the carrier of n:] is non empty set

K139( the carrier of n, the carrier of n, the InternalRel of n,i) is Element of bool the carrier of n

(U_FT i) /\ x is Element of bool the carrier of n

the Element of (U_FT i) /\ x is Element of (U_FT i) /\ x

C2 is Element of the carrier of n

U_FT C2 is Element of bool the carrier of n

K139( the carrier of n, the carrier of n, the InternalRel of n,C2) is Element of bool the carrier of n

(U_FT C2) /\ f is Element of bool the carrier of n

n is non empty reflexive RelStr

the carrier of n is non empty set

bool the carrier of n is non empty set

f is Element of bool the carrier of n

x is Element of bool the carrier of n

x ^b is Element of bool the carrier of n

{ b

f ^b is Element of bool the carrier of n

{ b

n is non empty reflexive RelStr

the carrier of n is non empty set

bool the carrier of n is non empty set

f is Element of bool the carrier of n

x is Element of bool the carrier of n

f ^b is Element of bool the carrier of n

{ b

x ^b is Element of bool the carrier of n

{ b

n is non empty reflexive RelStr

the carrier of n is non empty set

bool the carrier of n is non empty set

f is Element of bool the carrier of n

x is Element of bool the carrier of n

x ^b is Element of bool the carrier of n

{ b

f ^b is Element of bool the carrier of n

{ b

n is non empty reflexive RelStr

the carrier of n is non empty set

bool the carrier of n is non empty set

f is Element of bool the carrier of n

x is Element of bool the carrier of n

y is Element of bool the carrier of n

x \/ y is Element of bool the carrier of n

x ^b is Element of bool the carrier of n

{ b

y ^b is Element of bool the carrier of n

{ b

i is set

j is Element of the carrier of n

U_FT j is Element of bool the carrier of n

the InternalRel of n is Relation-like the carrier of n -defined the carrier of n -valued Element of bool [: the carrier of n, the carrier of n:]

[: the carrier of n, the carrier of n:] is non empty Relation-like set

bool [: the carrier of n, the carrier of n:] is non empty set

K139( the carrier of n, the carrier of n, the InternalRel of n,j) is Element of bool the carrier of n

(U_FT j) /\ y is Element of bool the carrier of n

the Element of (U_FT j) /\ y is Element of (U_FT j) /\ y

C1 is Element of the carrier of n

U_FT C1 is Element of bool the carrier of n

K139( the carrier of n, the carrier of n, the InternalRel of n,C1) is Element of bool the carrier of n

(U_FT C1) /\ x is Element of bool the carrier of n

(x ^b) /\ y is Element of bool the carrier of n

x /\ y is Element of bool the carrier of n

x is Element of bool the carrier of n

y is Element of bool the carrier of n

x \/ y is Element of bool the carrier of n

x ^b is Element of bool the carrier of n

{ b

x is Element of bool the carrier of n

y is Element of bool the carrier of n

x \/ y is Element of bool the carrier of n

i is Element of bool the carrier of n

j is Element of bool the carrier of n

i \/ j is Element of bool the carrier of n

n is non empty reflexive RelStr

the carrier of n is non empty set

bool the carrier of n is non empty set

f is Element of bool the carrier of n

x is Element of bool the carrier of n

x ^b is Element of bool the carrier of n

{ b

f \ x is Element of bool the carrier of n

(f \ x) ^b is Element of bool the carrier of n

{ b

x \/ (f \ x) is Element of bool the carrier of n

x \/ f is Element of bool the carrier of n

x is Element of bool the carrier of n

f \ x is Element of bool the carrier of n

x ^b is Element of bool the carrier of n

{ b

x is Element of bool the carrier of n

y is Element of bool the carrier of n

x \/ y is Element of bool the carrier of n

(x \/ y) \ x is Element of bool the carrier of n

y \ x is Element of bool the carrier of n

x ^b is Element of bool the carrier of n

{ b

f \ x is Element of bool the carrier of n

n is non empty RelStr

the carrier of n is non empty set

f is non empty RelStr

the carrier of f is non empty set

[: the carrier of n, the carrier of f:] is non empty Relation-like set

bool [: the carrier of n, the carrier of f:] is non empty set

n is non empty RelStr

the carrier of n is non empty set

f is non empty reflexive RelStr

the carrier of f is non empty set

[: the carrier of n, the carrier of f:] is non empty Relation-like set

bool [: the carrier of n, the carrier of f:] is non empty set

x is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

y is Relation-like the carrier of n -defined the carrier of f -valued Function-like V29( the carrier of n, the carrier of f) Element of bool [: the carrier of n, the carrier of f:]

i is Element of the carrier of n

y . i is Element of the carrier of f

U_FT (i,0) is Element of bool the carrier of n

bool the carrier of n is non empty set

y .: (U_FT (i,0)) is Element of bool the carrier of f

bool the carrier of f is non empty set

j is Element of the carrier of f

U_FT (j,x) is Element of bool the carrier of f

U_FT j is Element of bool the carrier of f

the InternalRel of f is Relation-like the carrier of f -defined the carrier of f -valued Element of bool [: the carrier of f, the carrier of f:]

[: the carrier of f, the carrier of f:] is non empty Relation-like set

bool [: the carrier of f, the carrier of f:] is non empty set

K139( the carrier of f, the carrier of f, the InternalRel of f,j) is Element of bool the carrier of f

U_FT (j,0) is Element of bool the carrier of f

Finf ((U_FT j),x) is Element of bool the carrier of f

n is non empty RelStr

the carrier of n is non empty set

f is non empty reflexive RelStr

the carrier of f is non empty set

[: the carrier of n, the carrier of f:] is non empty Relation-like set

bool [: the carrier of n, the carrier of f:] is non empty set

x is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

y is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

i is Relation-like the carrier of n -defined the carrier of f -valued Function-like V29( the carrier of n, the carrier of f) Element of bool [: the carrier of n, the carrier of f:]

j is Element of the carrier of n

i . j is Element of the carrier of f

U_FT (j,0) is Element of bool the carrier of n

bool the carrier of n is non empty set

i .: (U_FT (j,0)) is Element of bool the carrier of f

bool the carrier of f is non empty set

C2 is Element of the carrier of f

U_FT (C2,y) is Element of bool the carrier of f

U_FT (C2,x) is Element of bool the carrier of f

U_FT C2 is Element of bool the carrier of f

the InternalRel of f is Relation-like the carrier of f -defined the carrier of f -valued Element of bool [: the carrier of f, the carrier of f:]

[: the carrier of f, the carrier of f:] is non empty Relation-like set

bool [: the carrier of f, the carrier of f:] is non empty set

K139( the carrier of f, the carrier of f, the InternalRel of f,C2) is Element of bool the carrier of f

Finf ((U_FT C2),x) is Element of bool the carrier of f

Finf ((U_FT C2),y) is Element of bool the carrier of f

n is non empty RelStr

the carrier of n is non empty set

bool the carrier of n is non empty set

f is non empty RelStr

the carrier of f is non empty set

bool the carrier of f is non empty set

[: the carrier of n, the carrier of f:] is non empty Relation-like set

bool [: the carrier of n, the carrier of f:] is non empty set

x is Element of bool the carrier of n

x ^b is Element of bool the carrier of n

{ b

y is Element of bool the carrier of f

y ^b is Element of bool the carrier of f

{ b

i is Relation-like the carrier of n -defined the carrier of f -valued Function-like V29( the carrier of n, the carrier of f) Element of bool [: the carrier of n, the carrier of f:]

i .: x is Element of bool the carrier of f

i .: (x ^b) is Element of bool the carrier of f

j is set

dom i is Element of bool the carrier of n

C2 is set

i . C2 is set

C1 is Element of the carrier of n

U_FT (C1,0) is Element of bool the carrier of n

i .: (U_FT (C1,0)) is Element of bool the carrier of f

C10 is Element of the carrier of f

U_FT (C10,0) is Element of bool the carrier of f

U_FT C1 is Element of bool the carrier of n

the InternalRel of n is Relation-like the carrier of n -defined the carrier of n -valued Element of bool [: the carrier of n, the carrier of n:]

[: the carrier of n, the carrier of n:] is non empty Relation-like set

bool [: the carrier of n, the carrier of n:] is non empty set

K139( the carrier of n, the carrier of n, the InternalRel of n,C1) is Element of bool the carrier of n

i .: (U_FT C1) is Element of bool the carrier of f

U_FT C10 is Element of bool the carrier of f

the InternalRel of f is Relation-like the carrier of f -defined the carrier of f -valued Element of bool [: the carrier of f, the carrier of f:]

[: the carrier of f, the carrier of f:] is non empty Relation-like set

bool [: the carrier of f, the carrier of f:] is non empty set

K139( the carrier of f, the carrier of f, the InternalRel of f,C10) is Element of bool the carrier of f

(U_FT C1) /\ x is Element of bool the carrier of n

i .: ((U_FT C1) /\ x) is Element of bool the carrier of f

(i .: (U_FT C1)) /\ (i .: x) is Element of bool the carrier of f

(U_FT C10) /\ (i .: x) is Element of bool the carrier of f

B1 is Element of the carrier of n

U_FT B1 is Element of bool the carrier of n

K139( the carrier of n, the carrier of n, the InternalRel of n,B1) is Element of bool the carrier of n

n is non empty RelStr

the carrier of n is non empty set

bool the carrier of n is non empty set

f is non empty RelStr

the carrier of f is non empty set

bool the carrier of f is non empty set

[: the carrier of n, the carrier of f:] is non empty Relation-like set

bool [: the carrier of n, the carrier of f:] is non empty set

x is Element of bool the carrier of n

y is Element of bool the carrier of f

i is Relation-like the carrier of n -defined the carrier of f -valued Function-like V29( the carrier of n, the carrier of f) Element of bool [: the carrier of n, the carrier of f:]

i .: x is Element of bool the carrier of f

j is Element of bool the carrier of f

C2 is Element of bool the carrier of f

j \/ C2 is Element of bool the carrier of f

j ^b is Element of bool the carrier of f

{ b

i " C2 is Element of bool the carrier of n

C1 is Element of bool the carrier of n

C1 /\ x is Element of bool the carrier of n

i " j is Element of bool the carrier of n

B1 is Element of bool the carrier of n

B1 /\ x is Element of bool the carrier of n

C10 is Element of bool the carrier of n

the Element of C2 is Element of C2

dom i is Element of bool the carrier of n

z6 is set

i . z6 is set

the Element of j is Element of j

z5 is set

i . z5 is set

j /\ C2 is Element of bool the carrier of f

i " (j /\ C2) is Element of bool the carrier of n

B10 is Element of bool the carrier of n

(i " j) /\ (i " C2) is Element of bool the carrier of n

B10 /\ C10 is Element of bool the carrier of n

(i " j) \/ (i " C2) is Element of bool the carrier of n

i " (i .: x) is Element of bool the carrier of n

B1 \/ C1 is Element of bool the carrier of n

x /\ (B1 \/ C1) is Element of bool the carrier of n

B10 \/ C10 is Element of bool the carrier of n

B10 ^b is Element of bool the carrier of n

{ b

(B10 ^b) /\ C10 is Element of bool the carrier of n

i .: B1 is Element of bool the carrier of f

y is set

c

i . c

B20 is Element of bool the carrier of f

B20 ^b is Element of bool the carrier of f

{ b

B1 ^b is Element of bool the carrier of n

{ b

i .: (B1 ^b) is Element of bool the carrier of f

i .: C1 is Element of bool the carrier of f

(i .: (B1 ^b)) /\ (i .: C1) is Element of bool the carrier of f

(i .: (B1 ^b)) /\ C2 is Element of bool the carrier of f

(j ^b) /\ C2 is Element of bool the carrier of f

(B1 ^b) /\ C1 is Element of bool the carrier of n

i .: ((B1 ^b) /\ C1) is Element of bool the carrier of f

n is V4() V5() V6() V10() V11() ext-real non negative V44() set

Seg n is V49() V56(n) Element of bool NAT

{ b

[:(Seg n),(Seg n):] is Relation-like set

bool [:(Seg n),(Seg n):] is non empty set

f is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

f -' 1 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

max ((f -' 1),1) is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

f + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

min ((f + 1),n) is V4() V5() V6() V10() V11() ext-real non negative V44() set

{f,(max ((f -' 1),1)),(min ((f + 1),n))} is non empty set

f + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

min ((f + 1),n) is V4() V5() V6() V10() V11() ext-real non negative V44() set

{f,(max ((f -' 1),1)),(min ((f + 1),n))} is non empty set

0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

y is set

i is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

f is Relation-like Seg n -defined Seg n -valued Element of bool [:(Seg n),(Seg n):]

x is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

Im (f,x) is set

x -' 1 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

max ((x -' 1),1) is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

x + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

min ((x + 1),n) is V4() V5() V6() V10() V11() ext-real non negative V44() set

{x,(max ((x -' 1),1)),(min ((x + 1),n))} is non empty set

f is Relation-like Seg n -defined Seg n -valued Element of bool [:(Seg n),(Seg n):]

x is Relation-like Seg n -defined Seg n -valued Element of bool [:(Seg n),(Seg n):]

y is set

Im (f,y) is set

Im (x,y) is set

i is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

Im (f,i) is set

i -' 1 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

max ((i -' 1),1) is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

i + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

min ((i + 1),n) is V4() V5() V6() V10() V11() ext-real non negative V44() set

{i,(max ((i -' 1),1)),(min ((i + 1),n))} is non empty set

n is V4() V5() V6() V10() V11() ext-real non negative V44() set

Seg n is V49() V56(n) Element of bool NAT

{ b

(n) is Relation-like Seg n -defined Seg n -valued Element of bool [:(Seg n),(Seg n):]

[:(Seg n),(Seg n):] is Relation-like set

bool [:(Seg n),(Seg n):] is non empty set

RelStr(# (Seg n),(n) #) is strict RelStr

n is V4() V5() V6() V10() V11() ext-real non negative V44() set

(n) is non empty RelStr

Seg n is V49() V56(n) Element of bool NAT

{ b

(n) is Relation-like Seg n -defined Seg n -valued Element of bool [:(Seg n),(Seg n):]

[:(Seg n),(Seg n):] is Relation-like set

bool [:(Seg n),(Seg n):] is non empty set

RelStr(# (Seg n),(n) #) is strict RelStr

the carrier of (n) is non empty set

f is Element of the carrier of (n)

U_FT f is Element of bool the carrier of (n)

bool the carrier of (n) is non empty set

the InternalRel of (n) is Relation-like the carrier of (n) -defined the carrier of (n) -valued Element of bool [: the carrier of (n), the carrier of (n):]

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

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

K139( the carrier of (n), the carrier of (n), the InternalRel of (n),f) is Element of bool the carrier of (n)

x is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

x -' 1 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

max ((x -' 1),1) is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

x + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

min ((x + 1),n) is V4() V5() V6() V10() V11() ext-real non negative V44() set

{x,(max ((x -' 1),1)),(min ((x + 1),n))} is non empty set

n is V4() V5() V6() V10() V11() ext-real non negative V44() set

(n) is non empty RelStr

Seg n is V49() V56(n) Element of bool NAT

{ b

(n) is Relation-like Seg n -defined Seg n -valued Element of bool [:(Seg n),(Seg n):]

[:(Seg n),(Seg n):] is Relation-like set

bool [:(Seg n),(Seg n):] is non empty set

RelStr(# (Seg n),(n) #) is strict RelStr

the carrier of (n) is non empty set

x is Element of the carrier of (n)

f is Element of the carrier of (n)

U_FT f is Element of bool the carrier of (n)

bool the carrier of (n) is non empty set

the InternalRel of (n) is Relation-like the carrier of (n) -defined the carrier of (n) -valued Element of bool [: the carrier of (n), the carrier of (n):]

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

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

K139( the carrier of (n), the carrier of (n), the InternalRel of (n),f) is Element of bool the carrier of (n)

U_FT x is Element of bool the carrier of (n)

K139( the carrier of (n), the carrier of (n), the InternalRel of (n),x) is Element of bool the carrier of (n)

y is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

i is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

i -' 1 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

max ((i -' 1),1) is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

i + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

min ((i + 1),n) is V4() V5() V6() V10() V11() ext-real non negative V44() set

{i,(max ((i -' 1),1)),(min ((i + 1),n))} is non empty set

y -' 1 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

max ((y -' 1),1) is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

y + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

min ((y + 1),n) is V4() V5() V6() V10() V11() ext-real non negative V44() set

{y,(max ((y -' 1),1)),(min ((y + 1),n))} is non empty set

y - 1 is V11() ext-real V44() set

y - 1 is V11() ext-real V44() set

y - 1 is V11() ext-real V44() set

y - 1 is V11() ext-real V44() set

y - 1 is V11() ext-real V44() set

0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

y - 1 is V11() ext-real V44() set

y - 1 is V11() ext-real V44() set

y - 1 is V11() ext-real V44() set

y - 1 is V11() ext-real V44() set

y - 1 is V11() ext-real V44() set

0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

i - 1 is V11() ext-real V44() set

n is V4() V5() V6() V10() V11() ext-real non negative V44() set

Seg n is V49() V56(n) Element of bool NAT

{ b

[:(Seg n),(Seg n):] is Relation-like set

bool [:(Seg n),(Seg n):] is non empty set

bool (Seg n) is non empty set

f is set

x is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

x + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

x -' 1 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

{x,(x -' 1),(x + 1)} is non empty set

x - 1 is V11() ext-real V44() set

0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

i is set

i is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

i -' 1 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

i + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

{i,(i -' 1),(i + 1)} is non empty set

{i,n,(i + 1)} is non empty set

{i,(i -' 1),1} is non empty set

{i} is non empty set

x + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

{x,n,(x + 1)} is non empty set

i is set

i is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

i -' 1 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

i + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

{i,(i -' 1),(i + 1)} is non empty set

{i,n,(i + 1)} is non empty set

{i,(i -' 1),1} is non empty set

{i} is non empty set

x - 1 is V11() ext-real V44() set

x -' 1 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

{x,(x -' 1),1} is non empty set

i is set

i is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

i -' 1 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

i + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

{i,(i -' 1),(i + 1)} is non empty set

{i,n,(i + 1)} is non empty set

{i,(i -' 1),1} is non empty set

{i} is non empty set

{x} is non empty set

i is set

i is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

i -' 1 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

i + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

{i,(i -' 1),(i + 1)} is non empty set

{i,n,(i + 1)} is non empty set

{i,(i -' 1),1} is non empty set

{i} is non empty set

y is set

i is set

j is set

C2 is set

[:(Seg n),(bool (Seg n)):] is Relation-like set

bool [:(Seg n),(bool (Seg n)):] is non empty set

f is Relation-like Seg n -defined bool (Seg n) -valued Function-like V29( Seg n, bool (Seg n)) Element of bool [:(Seg n),(bool (Seg n)):]

x is Relation-like Seg n -defined Seg n -valued Element of bool [:(Seg n),(Seg n):]

y is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

Im (x,y) is set

y -' 1 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

y + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

{y,(y -' 1),(y + 1)} is non empty set

{y,n,(y + 1)} is non empty set

{y,(y -' 1),1} is non empty set

{y} is non empty set

f . y is set

f is Relation-like Seg n -defined Seg n -valued Element of bool [:(Seg n),(Seg n):]

x is Relation-like Seg n -defined Seg n -valued Element of bool [:(Seg n),(Seg n):]

y is set

Im (f,y) is set

Im (x,y) is set

i is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

i -' 1 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

i + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

{i,(i -' 1),(i + 1)} is non empty set

i + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

{i,n,(i + 1)} is non empty set

i -' 1 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

{i,(i -' 1),1} is non empty set

{i} is non empty set

n is V4() V5() V6() V10() V11() ext-real non negative V44() set

Seg n is V49() V56(n) Element of bool NAT

{ b

(n) is Relation-like Seg n -defined Seg n -valued Element of bool [:(Seg n),(Seg n):]

[:(Seg n),(Seg n):] is Relation-like set

bool [:(Seg n),(Seg n):] is non empty set

RelStr(# (Seg n),(n) #) is strict RelStr

n is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

(n) is non empty RelStr

(n) is Relation-like Seg n -defined Seg n -valued Element of bool [:(Seg n),(Seg n):]

Seg n is V49() V56(n) Element of bool NAT

{ b

[:(Seg n),(Seg n):] is Relation-like set

bool [:(Seg n),(Seg n):] is non empty set

RelStr(# (Seg n),(n) #) is strict RelStr

the carrier of (n) is non empty set

x is Element of the carrier of (n)

U_FT x is Element of bool the carrier of (n)

bool the carrier of (n) is non empty set

the InternalRel of (n) is Relation-like the carrier of (n) -defined the carrier of (n) -valued Element of bool [: the carrier of (n), the carrier of (n):]

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

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

K139( the carrier of (n), the carrier of (n), the InternalRel of (n),x) is Element of bool the carrier of (n)

y is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

Im ((n),y) is set

y + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

{y,n,(y + 1)} is non empty set

y -' 1 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

{y,(y -' 1),(y + 1)} is non empty set

{y} is non empty set

{y,(y -' 1),1} is non empty set

n is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

(n) is non empty RelStr

(n) is Relation-like Seg n -defined Seg n -valued Element of bool [:(Seg n),(Seg n):]

Seg n is V49() V56(n) Element of bool NAT

{ b

[:(Seg n),(Seg n):] is Relation-like set

bool [:(Seg n),(Seg n):] is non empty set

RelStr(# (Seg n),(n) #) is strict RelStr

the carrier of (n) is non empty set

y is Element of the carrier of (n)

x is Element of the carrier of (n)

U_FT x is Element of bool the carrier of (n)

bool the carrier of (n) is non empty set

the InternalRel of (n) is Relation-like the carrier of (n) -defined the carrier of (n) -valued Element of bool [: the carrier of (n), the carrier of (n):]

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

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

K139( the carrier of (n), the carrier of (n), the InternalRel of (n),x) is Element of bool the carrier of (n)

U_FT y is Element of bool the carrier of (n)

K139( the carrier of (n), the carrier of (n), the InternalRel of (n),y) is Element of bool the carrier of (n)

i is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

Im ((n),i) is set

i + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

{i,n,(i + 1)} is non empty set

{i} is non empty set

j is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

i -' 1 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

{i,(i -' 1),1} is non empty set

{i,(i -' 1),(i + 1)} is non empty set

i - 1 is V11() ext-real V44() set

Im ( the InternalRel of (n),y) is set

j -' 1 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

j + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

{j,(j -' 1),(j + 1)} is non empty set

j -' 1 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

(i -' 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

1 - 1 is V11() ext-real V44() set

(i -' 1) - 1 is V11() ext-real V44() set

j + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

Im ( the InternalRel of (n),y) is set

j -' 1 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

{j,(j -' 1),(j + 1)} is non empty set

{j,n,(j + 1)} is non empty set

j -' 1 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

j + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

j - 1 is V11() ext-real V44() set

Im ( the InternalRel of (n),y) is set

j -' 1 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

j + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

{j,(j -' 1),(j + 1)} is non empty set

j -' 1 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

Im ( the InternalRel of (n),y) is set

j + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

{j,(j -' 1),(j + 1)} is non empty set

{j,(j -' 1),1} is non empty set

j + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

j -' 1 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

j + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

j -' 1 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

j + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

Im ( the InternalRel of (n),y) is set

j -' 1 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

{j,(j -' 1),1} is non empty set

j - 1 is V11() ext-real V44() set

j -' 1 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

Im ( the InternalRel of (n),y) is set

j + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

{j,(j -' 1),(j + 1)} is non empty set

Im ( the InternalRel of (n),y) is set

j + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

{j,n,(j + 1)} is non empty set

n - 1 is V11() ext-real V44() set

n -' 1 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

(n - 1) + 1 is V11() ext-real V44() set

Im ( the InternalRel of (n),y) is set

j -' 1 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT

j + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V44() Element of NAT

{j,(j -' 1),(j + 1)} is non empty set