:: FINTOPO4 semantic presentation

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

NAT is non empty V4() V5() V6() set
bool NAT is non empty set
bool NAT is non empty 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

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
{ b1 where b1 is Element of the carrier of n : not U_FT b1 misses y } is set
i is Element of bool the carrier of n
i ^b is Element of bool the carrier of n
{ b1 where b1 is Element of the carrier of n : not U_FT b1 misses i } is set
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
{ b1 where b1 is Element of the carrier of n : not U_FT b1 misses f } is set
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
{ b1 where b1 is Element of the carrier of n : ex b2 being Element of the carrier of n st
( b2 in f & b1 in U_FT b2 )
}
is set

x ^f is Element of bool the carrier of n
{ b1 where b1 is Element of the carrier of n : ex b2 being Element of the carrier of n st
( b2 in x & b1 in U_FT b2 )
}
is set

f ^b is Element of bool the carrier of n
{ b1 where b1 is Element of the carrier of n : not U_FT b1 misses f } is set
x ^b is Element of bool the carrier of n
{ b1 where b1 is Element of the carrier of n : not U_FT b1 misses x } is set
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
{ b1 where b1 is Element of the carrier of n : not U_FT b1 misses f } is set
x is Element of bool the carrier of n
x ^b is Element of bool the carrier of n
{ b1 where b1 is Element of the carrier of n : not U_FT b1 misses x } is set
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
{ b1 where b1 is Element of the carrier of n : not U_FT b1 misses x } is set
f ^b is Element of bool the carrier of n
{ b1 where b1 is Element of the carrier of n : not U_FT b1 misses f } is set
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
{ b1 where b1 is Element of the carrier of n : not U_FT b1 misses f } is set
x ^b is Element of bool the carrier of n
{ b1 where b1 is Element of the carrier of n : not U_FT b1 misses x } is set
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
{ b1 where b1 is Element of the carrier of n : not U_FT b1 misses x } is set
f ^b is Element of bool the carrier of n
{ b1 where b1 is Element of the carrier of n : not U_FT b1 misses f } is set
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
{ b1 where b1 is Element of the carrier of n : not U_FT b1 misses x } is set
y ^b is Element of bool the carrier of n
{ b1 where b1 is Element of the carrier of n : not U_FT b1 misses y } is set
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
{ b1 where b1 is Element of the carrier of n : not U_FT b1 misses x } is set
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
{ b1 where b1 is Element of the carrier of n : not U_FT b1 misses x } is set
f \ x is Element of bool the carrier of n
(f \ x) ^b is Element of bool the carrier of n
{ b1 where b1 is Element of the carrier of n : not U_FT b1 misses f \ x } is set
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
{ b1 where b1 is Element of the carrier of n : not U_FT b1 misses x } is set
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
{ b1 where b1 is Element of the carrier of n : not U_FT b1 misses x } is set
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
{ b1 where b1 is Element of the carrier of n : not U_FT b1 misses x } is set
y is Element of bool the carrier of f
y ^b is Element of bool the carrier of f
{ b1 where b1 is Element of the carrier of f : not U_FT b1 misses y } is set
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
{ b1 where b1 is Element of the carrier of f : not U_FT b1 misses j } is set
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
{ b1 where b1 is Element of the carrier of n : not U_FT b1 misses B10 } is set
(B10 ^b) /\ C10 is Element of bool the carrier of n
i .: B1 is Element of bool the carrier of f
y is set
c18 is set
i . c18 is set
B20 is Element of bool the carrier of f
B20 ^b is Element of bool the carrier of f
{ b1 where b1 is Element of the carrier of f : not U_FT b1 misses B20 } is set
B1 ^b is Element of bool the carrier of n
{ b1 where b1 is Element of the carrier of n : not U_FT b1 misses B1 } is set
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
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
[:(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
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
(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
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
(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
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
(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
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
[:(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
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
(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
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
[:(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
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
[:(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