:: 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₁ where b₁ is Element of the carrier of n : not U_FT b₁ misses y } is set
i is Element of bool the carrier of n
i ^b is Element of bool the carrier of n
{ b₁ where b₁ is Element of the carrier of n : not U_FT b₁ 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
{ b₁ where b₁ is Element of the carrier of n : not U_FT b₁ 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
{ b₁ where b₁ is Element of the carrier of n : ex b₂ being Element of the carrier of n st
( b₂ in f & b₁ in U_FT b₂ ) } is set
x ^f is Element of bool the carrier of n
{ b₁ where b₁ is Element of the carrier of n : ex b₂ being Element of the carrier of n st
( b₂ in x & b₁ in U_FT b₂ ) } is set
f ^b is Element of bool the carrier of n
{ b₁ where b₁ is Element of the carrier of n : not U_FT b₁ misses f } is set
x ^b is Element of bool the carrier of n
{ b₁ where b₁ is Element of the carrier of n : not U_FT b₁ 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
{ b₁ where b₁ is Element of the carrier of n : not U_FT b₁ misses f } is set
x is Element of bool the carrier of n
x ^b is Element of bool the carrier of n
{ b₁ where b₁ is Element of the carrier of n : not U_FT b₁ 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
{ b₁ where b₁ is Element of the carrier of n : not U_FT b₁ misses x } is set
f ^b is Element of bool the carrier of n
{ b₁ where b₁ is Element of the carrier of n : not U_FT b₁ 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
{ b₁ where b₁ is Element of the carrier of n : not U_FT b₁ misses f } is set
x ^b is Element of bool the carrier of n
{ b₁ where b₁ is Element of the carrier of n : not U_FT b₁ 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
{ b₁ where b₁ is Element of the carrier of n : not U_FT b₁ misses x } is set
f ^b is Element of bool the carrier of n
{ b₁ where b₁ is Element of the carrier of n : not U_FT b₁ 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
{ b₁ where b₁ is Element of the carrier of n : not U_FT b₁ misses x } is set
y ^b is Element of bool the carrier of n
{ b₁ where b₁ is Element of the carrier of n : not U_FT b₁ 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
{ b₁ where b₁ is Element of the carrier of n : not U_FT b₁ 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
{ b₁ where b₁ is Element of the carrier of n : not U_FT b₁ 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
{ b₁ where b₁ is Element of the carrier of n : not U_FT b₁ 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
{ b₁ where b₁ is Element of the carrier of n : not U_FT b₁ 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
{ b₁ where b₁ is Element of the carrier of n : not U_FT b₁ 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
{ b₁ where b₁ is Element of the carrier of n : not U_FT b₁ misses x } is set
y is Element of bool the carrier of f
y ^b is Element of bool the carrier of f
{ b₁ where b₁ is Element of the carrier of f : not U_FT b₁ 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
{ b₁ where b₁ is Element of the carrier of f : not U_FT b₁ 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
{ b₁ where b₁ is Element of the carrier of n : not U_FT b₁ 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
c₁₈ is set
i . c₁₈ is set
B20 is Element of bool the carrier of f
B20 ^b is Element of bool the carrier of f
{ b₁ where b₁ is Element of the carrier of f : not U_FT b₁ misses B20 } is set
B1 ^b is Element of bool the carrier of n
{ b₁ where b₁ is Element of the carrier of n : not U_FT b₁ 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
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT : ( 1 <= b₁ & b₁ <= 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
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT : ( 1 <= b₁ & b₁ <= 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
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT : ( 1 <= b₁ & b₁ <= 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
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT : ( 1 <= b₁ & b₁ <= 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
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT : ( 1 <= b₁ & b₁ <= 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
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT : ( 1 <= b₁ & b₁ <= 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
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT : ( 1 <= b₁ & b₁ <= 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
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V44() Element of NAT : ( 1 <= b₁ & b₁ <= 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