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
COMPLEX is set
{} is empty V4() V5() V6() V8() V9() V10() complex V12() ext-real non positive non negative functional FinSequence-membered integer set
1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
2 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
3 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
0 is empty V4() V5() V6() V8() V9() V10() complex V12() ext-real non positive non negative functional FinSequence-membered integer Element of NAT
n is set
bool n is non empty set
FT1 is non empty set
[:n,FT1:] is set
bool [:n,FT1:] is non empty set
FT2 is Relation-like n -defined FT1 -valued Function-like quasi_total Element of bool [:n,FT1:]
FT2 " is Relation-like Function-like set
f is Element of bool n
FT2 .: f is Element of bool FT1
bool FT1 is non empty set
(FT2 ") .: (FT2 .: f) is set
dom FT2 is Element of bool n
n is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
Seg n is V47() V54(n) Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
FT1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
Seg FT1 is V47() V54(FT1) Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT : ( 1 <= b1 & b1 <= FT1 ) } is set
n is RelStr
the carrier of n is set
FT1 is RelStr
the carrier of FT1 is set
[: the carrier of n, the carrier of FT1:] is set
bool [: the carrier of n, the carrier of FT1:] is non empty set
n is non empty RelStr
the carrier of n is non empty set
FT1 is non empty RelStr
the carrier of FT1 is non empty set
[: the carrier of n, the carrier of FT1:] is non empty set
bool [: the carrier of n, the carrier of FT1:] is non empty set
[: the carrier of FT1, the carrier of n:] is non empty set
bool [: the carrier of FT1, the carrier of n:] is non empty set
FT2 is Relation-like the carrier of n -defined the carrier of FT1 -valued Function-like quasi_total Element of bool [: the carrier of n, the carrier of FT1:]
FT2 " is Relation-like Function-like set
rng FT2 is Element of bool the carrier of FT1
bool the carrier of FT1 is non empty set
f is Relation-like the carrier of FT1 -defined the carrier of n -valued Function-like quasi_total Element of bool [: the carrier of FT1, 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 set
bool [: the carrier of n, the carrier of n:] is non empty set
x1 is Element of the carrier of FT1
U_FT x1 is Element of bool the carrier of FT1
the InternalRel of FT1 is Relation-like the carrier of FT1 -defined the carrier of FT1 -valued Element of bool [: the carrier of FT1, the carrier of FT1:]
[: the carrier of FT1, the carrier of FT1:] is non empty set
bool [: the carrier of FT1, the carrier of FT1:] is non empty set
Class ( the InternalRel of FT1,x1) is Element of bool the carrier of FT1
{x1} is non empty set
the InternalRel of FT1 .: {x1} is set
f .: (U_FT x1) is Element of bool the carrier of n
bool the carrier of n is non empty set
f . x1 is Element of the carrier of n
Im ( the InternalRel of n,(f . x1)) is set
{(f . x1)} is non empty set
the InternalRel of n .: {(f . x1)} is set
x2 is Element of the carrier of n
FT2 . x2 is Element of the carrier of FT1
U_FT x2 is Element of bool the carrier of n
Class ( the InternalRel of n,x2) is Element of bool the carrier of n
{x2} is non empty set
the InternalRel of n .: {x2} is set
FT2 .: (U_FT x2) is Element of bool the carrier of FT1
Im ( the InternalRel of FT1,(FT2 . x2)) is set
{(FT2 . x2)} is non empty set
the InternalRel of FT1 .: {(FT2 . x2)} is set
rng f is Element of bool the carrier of n
bool the carrier of n is non empty set
dom FT2 is Element of bool the carrier of n
n is non empty RelStr
the carrier of n is non empty set
FT1 is non empty RelStr
the carrier of FT1 is non empty set
[: the carrier of n, the carrier of FT1:] is non empty set
bool [: the carrier of n, the carrier of FT1:] is non empty set
FT2 is Relation-like the carrier of n -defined the carrier of FT1 -valued Function-like quasi_total Element of bool [: the carrier of n, the carrier of FT1:]
f is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
x1 is Element of the carrier of n
FT2 . x1 is Element of the carrier of FT1
U_FT (x1,f) is Element of bool the carrier of n
bool the carrier of n is non empty set
x2 is Element of the carrier of FT1
U_FT (x2,f) is Element of bool the carrier of FT1
bool the carrier of FT1 is non empty set
v is Element of the carrier of n
FT2 . v is Element of the carrier of FT1
dom FT2 is Element of bool the carrier of n
FT2 " is Relation-like Function-like set
[: the carrier of FT1, the carrier of n:] is non empty set
bool [: the carrier of FT1, the carrier of n:] is non empty set
X is Relation-like the carrier of FT1 -defined the carrier of n -valued Function-like quasi_total Element of bool [: the carrier of FT1, the carrier of n:]
Y is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
U_FT (x2,Y) is Element of bool the carrier of FT1
U_FT (x1,Y) is Element of bool the carrier of n
Y + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
U_FT (x2,(Y + 1)) is Element of bool the carrier of FT1
U_FT (x1,(Y + 1)) is Element of bool the carrier of n
nv is Element of the carrier of FT1
(FT2 ") . nv is set
(U_FT (x2,Y)) ^f is Element of bool the carrier of FT1
{ b1 where b1 is Element of the carrier of FT1 : ex b2 being Element of the carrier of FT1 st
( b2 in U_FT (x2,Y) & b1 in U_FT b2 ) } is set
y is Element of the carrier of FT1
x3 is Element of the carrier of FT1
U_FT x3 is Element of bool the carrier of FT1
the InternalRel of FT1 is Relation-like the carrier of FT1 -defined the carrier of FT1 -valued Element of bool [: the carrier of FT1, the carrier of FT1:]
[: the carrier of FT1, the carrier of FT1:] is non empty set
bool [: the carrier of FT1, the carrier of FT1:] is non empty set
Class ( the InternalRel of FT1,x3) is Element of bool the carrier of FT1
{x3} is non empty set
the InternalRel of FT1 .: {x3} is set
x3 is Element of the carrier of FT1
U_FT x3 is Element of bool the carrier of FT1
the InternalRel of FT1 is Relation-like the carrier of FT1 -defined the carrier of FT1 -valued Element of bool [: the carrier of FT1, the carrier of FT1:]
[: the carrier of FT1, the carrier of FT1:] is non empty set
bool [: the carrier of FT1, the carrier of FT1:] is non empty set
Class ( the InternalRel of FT1,x3) is Element of bool the carrier of FT1
{x3} is non empty set
the InternalRel of FT1 .: {x3} is set
X . x3 is Element of the carrier of n
X . y is Element of the carrier of n
U_FT (x3,0) is Element of bool the carrier of FT1
u2 is Element of the carrier of n
U_FT (u2,0) is Element of bool the carrier of n
pj2 is Element of the carrier of FT1
(FT2 ") . pj2 is set
dom X is Element of bool the carrier of FT1
(FT2 ") .: (U_FT x3) is 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 set
bool [: the carrier of n, the carrier of n:] is non empty set
(FT2 ") . x3 is set
Class ( the InternalRel of n,((FT2 ") . x3)) is Element of bool the carrier of n
{((FT2 ") . x3)} is non empty set
the InternalRel of n .: {((FT2 ") . x3)} is set
U_FT u2 is Element of bool the carrier of n
Class ( the InternalRel of n,u2) is Element of bool the carrier of n
{u2} is non empty set
the InternalRel of n .: {u2} is set
v2 is Element of the carrier of n
U_FT u2 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 set
bool [: the carrier of n, the carrier of n:] is non empty set
Class ( the InternalRel of n,u2) is Element of bool the carrier of n
{u2} is non empty set
the InternalRel of n .: {u2} is set
(U_FT (x1,Y)) ^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 U_FT (x1,Y) & b1 in U_FT b2 ) } is set
nv is Element of the carrier of FT1
(FT2 ") . nv is set
X . x2 is Element of the carrier of n
U_FT (x2,0) is Element of bool the carrier of FT1
U_FT (x1,0) is Element of bool the carrier of n
Y is Element of the carrier of FT1
(FT2 ") . Y is set
dom X is Element of bool the carrier of FT1
U_FT x2 is Element of bool the carrier of FT1
the InternalRel of FT1 is Relation-like the carrier of FT1 -defined the carrier of FT1 -valued Element of bool [: the carrier of FT1, the carrier of FT1:]
[: the carrier of FT1, the carrier of FT1:] is non empty set
bool [: the carrier of FT1, the carrier of FT1:] is non empty set
Class ( the InternalRel of FT1,x2) is Element of bool the carrier of FT1
{x2} is non empty set
the InternalRel of FT1 .: {x2} is set
X .: (U_FT x2) 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 set
bool [: the carrier of n, the carrier of n:] is non empty set
Class ( the InternalRel of n,(X . x2)) is Element of bool the carrier of n
{(X . x2)} is non empty set
the InternalRel of n .: {(X . x2)} is set
X . Y is Element of the carrier of n
U_FT x1 is Element of bool the carrier of n
Class ( the InternalRel of n,x1) is Element of bool the carrier of n
{x1} is non empty set
the InternalRel of n .: {x1} is set
Y is Element of the carrier of FT1
(FT2 ") . Y is set
(FT2 ") . (FT2 . v) is set
X is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
U_FT (x1,X) is Element of bool the carrier of n
U_FT (x2,X) is Element of bool the carrier of FT1
X + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
U_FT (x1,(X + 1)) is Element of bool the carrier of n
U_FT (x2,(X + 1)) is Element of bool the carrier of FT1
Y is Element of the carrier of n
FT2 . Y is Element of the carrier of FT1
(U_FT (x1,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 U_FT (x1,X) & b1 in U_FT b2 ) } is set
nv is Element of the carrier of n
y is Element of the carrier of n
U_FT y 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 set
bool [: the carrier of n, the carrier of n:] is non empty set
Class ( the InternalRel of n,y) is Element of bool the carrier of n
{y} is non empty set
the InternalRel of n .: {y} is set
y is Element of the carrier of n
U_FT y 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 set
bool [: the carrier of n, the carrier of n:] is non empty set
Class ( the InternalRel of n,y) is Element of bool the carrier of n
{y} is non empty set
the InternalRel of n .: {y} is set
FT2 . y is Element of the carrier of FT1
FT2 . nv is Element of the carrier of FT1
U_FT (y,0) is Element of bool the carrier of n
x3 is Element of the carrier of FT1
U_FT (x3,0) is Element of bool the carrier of FT1
v2 is Element of the carrier of n
FT2 . v2 is Element of the carrier of FT1
FT2 .: (U_FT y) is Element of bool the carrier of FT1
the InternalRel of FT1 is Relation-like the carrier of FT1 -defined the carrier of FT1 -valued Element of bool [: the carrier of FT1, the carrier of FT1:]
[: the carrier of FT1, the carrier of FT1:] is non empty set
bool [: the carrier of FT1, the carrier of FT1:] is non empty set
Class ( the InternalRel of FT1,(FT2 . y)) is Element of bool the carrier of FT1
{(FT2 . y)} is non empty set
the InternalRel of FT1 .: {(FT2 . y)} is set
U_FT x3 is Element of bool the carrier of FT1
Class ( the InternalRel of FT1,x3) is Element of bool the carrier of FT1
{x3} is non empty set
the InternalRel of FT1 .: {x3} is set
u2 is Element of the carrier of FT1
U_FT x3 is Element of bool the carrier of FT1
the InternalRel of FT1 is Relation-like the carrier of FT1 -defined the carrier of FT1 -valued Element of bool [: the carrier of FT1, the carrier of FT1:]
[: the carrier of FT1, the carrier of FT1:] is non empty set
bool [: the carrier of FT1, the carrier of FT1:] is non empty set
Class ( the InternalRel of FT1,x3) is Element of bool the carrier of FT1
{x3} is non empty set
the InternalRel of FT1 .: {x3} is set
(U_FT (x2,X)) ^f is Element of bool the carrier of FT1
{ b1 where b1 is Element of the carrier of FT1 : ex b2 being Element of the carrier of FT1 st
( b2 in U_FT (x2,X) & b1 in U_FT b2 ) } is set
Y is Element of the carrier of n
FT2 . Y is Element of the carrier of FT1
X is Element of the carrier of n
FT2 . X is Element of the carrier of FT1
U_FT x1 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 set
bool [: the carrier of n, the carrier of n:] is non empty set
Class ( the InternalRel of n,x1) is Element of bool the carrier of n
{x1} is non empty set
the InternalRel of n .: {x1} is set
FT2 .: (U_FT x1) is Element of bool the carrier of FT1
the InternalRel of FT1 is Relation-like the carrier of FT1 -defined the carrier of FT1 -valued Element of bool [: the carrier of FT1, the carrier of FT1:]
[: the carrier of FT1, the carrier of FT1:] is non empty set
bool [: the carrier of FT1, the carrier of FT1:] is non empty set
Class ( the InternalRel of FT1,(FT2 . x1)) is Element of bool the carrier of FT1
{(FT2 . x1)} is non empty set
the InternalRel of FT1 .: {(FT2 . x1)} is set
U_FT x2 is Element of bool the carrier of FT1
Class ( the InternalRel of FT1,x2) is Element of bool the carrier of FT1
{x2} is non empty set
the InternalRel of FT1 .: {x2} is set
X is Element of the carrier of n
FT2 . X is Element of the carrier of FT1
n is non empty RelStr
the carrier of n is non empty set
FT1 is non empty RelStr
the carrier of FT1 is non empty set
[: the carrier of n, the carrier of FT1:] is non empty set
bool [: the carrier of n, the carrier of FT1:] is non empty set
FT2 is Relation-like the carrier of n -defined the carrier of FT1 -valued Function-like quasi_total Element of bool [: the carrier of n, the carrier of FT1:]
FT2 " is Relation-like Function-like set
f is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
x1 is Element of the carrier of n
FT2 . x1 is Element of the carrier of FT1
U_FT (x1,f) is Element of bool the carrier of n
bool the carrier of n is non empty set
x2 is Element of the carrier of FT1
U_FT (x2,f) is Element of bool the carrier of FT1
bool the carrier of FT1 is non empty set
dom FT2 is Element of bool the carrier of n
[: the carrier of FT1, the carrier of n:] is non empty set
bool [: the carrier of FT1, the carrier of n:] is non empty set
v is Relation-like the carrier of FT1 -defined the carrier of n -valued Function-like quasi_total Element of bool [: the carrier of FT1, the carrier of n:]
v . x2 is Element of the carrier of n
X is Element of the carrier of FT1
(FT2 ") . X is set
Y is Element of the carrier of FT1
(FT2 ") . Y is set
n is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
FTSL1 n is non empty RelStr
the carrier of (FTSL1 n) is non empty set
[: the carrier of (FTSL1 n), the carrier of (FTSL1 n):] is non empty set
bool [: the carrier of (FTSL1 n), the carrier of (FTSL1 n):] is non empty set
FT1 is Relation-like the carrier of (FTSL1 n) -defined the carrier of (FTSL1 n) -valued Function-like quasi_total Element of bool [: the carrier of (FTSL1 n), the carrier of (FTSL1 n):]
0 + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
Seg n is non empty V47() V54(n) Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
Nbdl1 n is Relation-like Seg n -defined Seg n -valued Element of bool [:(Seg n),(Seg n):]
[:(Seg n),(Seg n):] is non empty set
bool [:(Seg n),(Seg n):] is non empty set
RelStr(# (Seg n),(Nbdl1 n) #) is strict RelStr
FT2 is Element of the carrier of (FTSL1 n)
U_FT FT2 is Element of bool the carrier of (FTSL1 n)
bool the carrier of (FTSL1 n) is non empty set
the InternalRel of (FTSL1 n) is Relation-like the carrier of (FTSL1 n) -defined the carrier of (FTSL1 n) -valued Element of bool [: the carrier of (FTSL1 n), the carrier of (FTSL1 n):]
Class ( the InternalRel of (FTSL1 n),FT2) is Element of bool the carrier of (FTSL1 n)
{FT2} is non empty set
the InternalRel of (FTSL1 n) .: {FT2} is set
U_FT (FT2,0) is Element of bool the carrier of (FTSL1 n)
FT1 . n is set
f is V4() V5() V6() V10() complex V12() ext-real non negative integer set
FT2 is V4() V5() V6() V10() complex V12() ext-real non negative integer set
FT2 is V4() V5() V6() V10() complex V12() ext-real non negative integer set
FT1 . FT2 is set
FT2 is V4() V5() V6() V10() complex V12() ext-real non negative integer set
FT1 . FT2 is set
FT2 - 1 is complex V12() ext-real integer set
FT2 -' 1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
FT2 + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
(FT2 + 1) - 1 is complex V12() ext-real integer set
FT1 . 1 is set
x1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
FT1 . (FT2 -' 1) is set
x1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
x1 + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
(x1 + 1) - 1 is complex V12() ext-real integer set
x1 - 1 is complex V12() ext-real integer set
x2 is V4() V5() V6() V10() complex V12() ext-real non negative integer set
max ((FT2 -' 1),1) is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
min ((FT2 + 1),n) is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
x2 is V4() V5() V6() V10() complex V12() ext-real non negative integer set
x2 is V4() V5() V6() V10() complex V12() ext-real non negative integer set
v is Element of the carrier of (FTSL1 n)
Im ((Nbdl1 n),v) is set
{v} is non empty set
(Nbdl1 n) .: {v} is set
(FT2 -' 1) -' 1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
max (((FT2 -' 1) -' 1),1) is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
(FT2 -' 1) + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
min (((FT2 -' 1) + 1),n) is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
{(FT2 -' 1),(max (((FT2 -' 1) -' 1),1)),(min (((FT2 -' 1) + 1),n))} is non empty set
Im ((Nbdl1 n),FT2) is set
{FT2} is non empty set
(Nbdl1 n) .: {FT2} is set
{FT2,(max ((FT2 -' 1),1)),(min ((FT2 + 1),n))} is non empty set
f is Element of the carrier of (FTSL1 n)
U_FT f is Element of bool the carrier of (FTSL1 n)
Class ( the InternalRel of (FTSL1 n),f) is Element of bool the carrier of (FTSL1 n)
{f} is non empty set
the InternalRel of (FTSL1 n) .: {f} is set
U_FT (f,0) is Element of bool the carrier of (FTSL1 n)
FT1 .: (U_FT (f,0)) is Element of bool the carrier of (FTSL1 n)
X is Element of the carrier of (FTSL1 n)
U_FT (X,0) is Element of bool the carrier of (FTSL1 n)
Y is Element of the carrier of (FTSL1 n)
U_FT Y is Element of bool the carrier of (FTSL1 n)
Class ( the InternalRel of (FTSL1 n),Y) is Element of bool the carrier of (FTSL1 n)
{Y} is non empty set
the InternalRel of (FTSL1 n) .: {Y} is set
FT1 . x2 is set
U_FT (Y,0) is Element of bool the carrier of (FTSL1 n)
U_FT v is Element of bool the carrier of (FTSL1 n)
Class ( the InternalRel of (FTSL1 n),v) is Element of bool the carrier of (FTSL1 n)
the InternalRel of (FTSL1 n) .: {v} is set
U_FT (v,0) is Element of bool the carrier of (FTSL1 n)
min ((x1 + 1),n) is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
min ((x1 + 1),n) is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
min ((x1 + 1),n) is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
min ((x1 + 1),n) is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
x1 -' 1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
max ((x1 -' 1),1) is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
max ((x1 -' 1),1) is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
max ((x1 -' 1),1) is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
max ((x1 -' 1),1) is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
dom FT1 is Element of bool the carrier of (FTSL1 n)
Im ((Nbdl1 n),x1) is set
{x1} is non empty set
(Nbdl1 n) .: {x1} is set
{x1,(max ((x1 -' 1),1)),(min ((x1 + 1),n))} is non empty set
U_FT X is Element of bool the carrier of (FTSL1 n)
Class ( the InternalRel of (FTSL1 n),X) is Element of bool the carrier of (FTSL1 n)
{X} is non empty set
the InternalRel of (FTSL1 n) .: {X} is set
FT1 . (FT2 -' 1) is set
FT1 . (FT2 -' 1) is set
x1 is V4() V5() V6() V10() complex V12() ext-real non negative integer set
n is non empty RelStr
the carrier of n is non empty set
FT1 is Element of the carrier of n
FT2 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
U_FT (FT1,FT2) is Element of bool the carrier of n
bool the carrier of n is non empty set
FT2 + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
U_FT (FT1,(FT2 + 1)) is Element of bool the carrier of n
(U_FT (FT1,FT2)) ^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 U_FT (FT1,FT2) & b1 in U_FT b2 ) } is set
n is non empty RelStr
the carrier of n is non empty set
FT1 is Element of the carrier of n
U_FT (FT1,0) is Element of bool the carrier of n
bool the carrier of n is non empty set
FT2 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
U_FT (FT1,FT2) is Element of bool the carrier of n
f is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
U_FT (FT1,f) is Element of bool the carrier of n
f + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
U_FT (FT1,(f + 1)) is Element of bool the carrier of n
n is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer set
FTSL1 n is non empty RelStr
the carrier of (FTSL1 n) is non empty set
Seg n is non empty V47() V54(n) Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
FT1 is V4() V5() V6() V10() complex V12() ext-real non negative integer set
FT2 is V4() V5() V6() V10() complex V12() ext-real non negative integer set
f is V4() V5() V6() V10() complex V12() ext-real non negative integer set
FT1 - FT2 is complex V12() ext-real integer set
abs (FT1 - FT2) is complex V12() ext-real Element of REAL
f + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
x1 is Element of the carrier of (FTSL1 n)
U_FT (x1,f) is Element of bool the carrier of (FTSL1 n)
bool the carrier of (FTSL1 n) is non empty set
Nbdl1 n is Relation-like Seg n -defined Seg n -valued Element of bool [:(Seg n),(Seg n):]
[:(Seg n),(Seg n):] is non empty set
bool [:(Seg n),(Seg n):] is non empty set
RelStr(# (Seg n),(Nbdl1 n) #) is strict RelStr
0 + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
v is V4() V5() V6() V10() complex V12() ext-real non negative integer set
x2 is V4() V5() V6() V10() complex V12() ext-real non negative integer set
v - x2 is complex V12() ext-real integer set
abs (v - x2) is complex V12() ext-real Element of REAL
X is Element of the carrier of (FTSL1 n)
U_FT (X,0) is Element of bool the carrier of (FTSL1 n)
0 + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
v -' x2 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
v - 1 is complex V12() ext-real integer set
v -' 1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
max ((v -' 1),1) is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
v + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
min ((v + 1),n) is V4() V5() V6() V10() complex V12() ext-real non negative integer set
v -' 1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
max ((v -' 1),1) is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
v + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
min ((v + 1),n) is V4() V5() V6() V10() complex V12() ext-real non negative integer set
v - 1 is complex V12() ext-real integer set
v -' 1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
max ((v -' 1),1) is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
v + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
min ((v + 1),n) is V4() V5() V6() V10() complex V12() ext-real non negative integer set
v -' 1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
max ((v -' 1),1) is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
v + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
min ((v + 1),n) is V4() V5() V6() V10() complex V12() ext-real non negative integer set
0 + x2 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
(v - x2) + x2 is complex V12() ext-real integer set
v + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
- (v - x2) is complex V12() ext-real integer set
x2 - v is complex V12() ext-real integer set
(x2 - v) + v is complex V12() ext-real integer set
1 + v is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
v -' 1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
max ((v -' 1),1) is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
min ((v + 1),n) is V4() V5() V6() V10() complex V12() ext-real non negative integer set
v -' 1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
max ((v -' 1),1) is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
v + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
min ((v + 1),n) is V4() V5() V6() V10() complex V12() ext-real non negative integer set
v -' 1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
max ((v -' 1),1) is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
v + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
min ((v + 1),n) is V4() V5() V6() V10() complex V12() ext-real non negative integer set
{v,(max ((v -' 1),1)),(min ((v + 1),n))} is non empty set
U_FT X is Element of bool the carrier of (FTSL1 n)
the InternalRel of (FTSL1 n) is Relation-like the carrier of (FTSL1 n) -defined the carrier of (FTSL1 n) -valued Element of bool [: the carrier of (FTSL1 n), the carrier of (FTSL1 n):]
[: the carrier of (FTSL1 n), the carrier of (FTSL1 n):] is non empty set
bool [: the carrier of (FTSL1 n), the carrier of (FTSL1 n):] is non empty set
Class ( the InternalRel of (FTSL1 n),X) is Element of bool the carrier of (FTSL1 n)
{X} is non empty set
the InternalRel of (FTSL1 n) .: {X} is set
x2 is V4() V5() V6() V10() complex V12() ext-real non negative integer set
x2 + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
(x2 + 1) + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
X is V4() V5() V6() V10() complex V12() ext-real non negative integer set
v is V4() V5() V6() V10() complex V12() ext-real non negative integer set
X - v is complex V12() ext-real integer set
abs (X - v) is complex V12() ext-real Element of REAL
Y is Element of the carrier of (FTSL1 n)
U_FT (Y,(x2 + 1)) is Element of bool the carrier of (FTSL1 n)
(x2 + 1) + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
nv is Element of the carrier of (FTSL1 n)
U_FT Y is Element of bool the carrier of (FTSL1 n)
the InternalRel of (FTSL1 n) is Relation-like the carrier of (FTSL1 n) -defined the carrier of (FTSL1 n) -valued Element of bool [: the carrier of (FTSL1 n), the carrier of (FTSL1 n):]
[: the carrier of (FTSL1 n), the carrier of (FTSL1 n):] is non empty set
bool [: the carrier of (FTSL1 n), the carrier of (FTSL1 n):] is non empty set
Class ( the InternalRel of (FTSL1 n),Y) is Element of bool the carrier of (FTSL1 n)
{Y} is non empty set
the InternalRel of (FTSL1 n) .: {Y} is set
U_FT (Y,x2) is Element of bool the carrier of (FTSL1 n)
X -' v is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
0 + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
1 + v is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
(X - v) + v is complex V12() ext-real integer set
v + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
X - (v + 1) is complex V12() ext-real integer set
1 - 1 is complex V12() ext-real integer set
(X - v) - 1 is complex V12() ext-real integer set
X -' (v + 1) is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
abs (X - (v + 1)) is complex V12() ext-real Element of REAL
(v + 1) - v is complex V12() ext-real integer set
abs ((v + 1) - v) is complex V12() ext-real Element of REAL
nv is Element of the carrier of (FTSL1 n)
y is Element of the carrier of (FTSL1 n)
U_FT (y,0) is Element of bool the carrier of (FTSL1 n)
U_FT y is Element of bool the carrier of (FTSL1 n)
the InternalRel of (FTSL1 n) is Relation-like the carrier of (FTSL1 n) -defined the carrier of (FTSL1 n) -valued Element of bool [: the carrier of (FTSL1 n), the carrier of (FTSL1 n):]
[: the carrier of (FTSL1 n), the carrier of (FTSL1 n):] is non empty set
bool [: the carrier of (FTSL1 n), the carrier of (FTSL1 n):] is non empty set
Class ( the InternalRel of (FTSL1 n),y) is Element of bool the carrier of (FTSL1 n)
{y} is non empty set
the InternalRel of (FTSL1 n) .: {y} is set
U_FT (Y,x2) is Element of bool the carrier of (FTSL1 n)
U_FT (Y,x2) is Element of bool the carrier of (FTSL1 n)
nv is Element of the carrier of (FTSL1 n)
U_FT (Y,x2) is Element of bool the carrier of (FTSL1 n)
nv is Element of the carrier of (FTSL1 n)
0 + v is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
(X - v) + v is complex V12() ext-real integer set
v - X is complex V12() ext-real integer set
v - 1 is complex V12() ext-real integer set
v -' 1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
X + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
(X + 1) - 1 is complex V12() ext-real integer set
(v - 1) - X is complex V12() ext-real integer set
(v -' 1) - X is complex V12() ext-real integer set
abs ((v -' 1) - X) is complex V12() ext-real Element of REAL
v + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
(v + 1) - 1 is complex V12() ext-real integer set
abs (v - X) is complex V12() ext-real Element of REAL
1 + ((v -' 1) - X) is complex V12() ext-real integer set
X - (v -' 1) is complex V12() ext-real integer set
abs (X - (v -' 1)) is complex V12() ext-real Element of REAL
1 + (abs (X - (v -' 1))) is complex V12() ext-real set
(v -' 1) - v is complex V12() ext-real integer set
abs ((v -' 1) - v) is complex V12() ext-real Element of REAL
v - (v -' 1) is complex V12() ext-real integer set
abs (v - (v -' 1)) is complex V12() ext-real Element of REAL
nv is Element of the carrier of (FTSL1 n)
y is Element of the carrier of (FTSL1 n)
U_FT (y,0) is Element of bool the carrier of (FTSL1 n)
U_FT y is Element of bool the carrier of (FTSL1 n)
the InternalRel of (FTSL1 n) is Relation-like the carrier of (FTSL1 n) -defined the carrier of (FTSL1 n) -valued Element of bool [: the carrier of (FTSL1 n), the carrier of (FTSL1 n):]
[: the carrier of (FTSL1 n), the carrier of (FTSL1 n):] is non empty set
bool [: the carrier of (FTSL1 n), the carrier of (FTSL1 n):] is non empty set
Class ( the InternalRel of (FTSL1 n),y) is Element of bool the carrier of (FTSL1 n)
{y} is non empty set
the InternalRel of (FTSL1 n) .: {y} is set
U_FT (Y,x2) is Element of bool the carrier of (FTSL1 n)
U_FT (Y,x2) is Element of bool the carrier of (FTSL1 n)
nv is Element of the carrier of (FTSL1 n)
U_FT (Y,x2) is Element of bool the carrier of (FTSL1 n)
nv is Element of the carrier of (FTSL1 n)
(U_FT (Y,x2)) ^f is Element of bool the carrier of (FTSL1 n)
{ b1 where b1 is Element of the carrier of (FTSL1 n) : ex b2 being Element of the carrier of (FTSL1 n) st
( b2 in U_FT (Y,x2) & b1 in U_FT b2 ) } is set
y is Element of the carrier of (FTSL1 n)
U_FT y is Element of bool the carrier of (FTSL1 n)
the InternalRel of (FTSL1 n) is Relation-like the carrier of (FTSL1 n) -defined the carrier of (FTSL1 n) -valued Element of bool [: the carrier of (FTSL1 n), the carrier of (FTSL1 n):]
[: the carrier of (FTSL1 n), the carrier of (FTSL1 n):] is non empty set
bool [: the carrier of (FTSL1 n), the carrier of (FTSL1 n):] is non empty set
Class ( the InternalRel of (FTSL1 n),y) is Element of bool the carrier of (FTSL1 n)
{y} is non empty set
the InternalRel of (FTSL1 n) .: {y} is set
v is V4() V5() V6() V10() complex V12() ext-real non negative integer set
x2 is V4() V5() V6() V10() complex V12() ext-real non negative integer set
v - x2 is complex V12() ext-real integer set
abs (v - x2) is complex V12() ext-real Element of REAL
X is Element of the carrier of (FTSL1 n)
U_FT (X,0) is Element of bool the carrier of (FTSL1 n)
U_FT X is Element of bool the carrier of (FTSL1 n)
the InternalRel of (FTSL1 n) is Relation-like the carrier of (FTSL1 n) -defined the carrier of (FTSL1 n) -valued Element of bool [: the carrier of (FTSL1 n), the carrier of (FTSL1 n):]
[: the carrier of (FTSL1 n), the carrier of (FTSL1 n):] is non empty set
bool [: the carrier of (FTSL1 n), the carrier of (FTSL1 n):] is non empty set
Class ( the InternalRel of (FTSL1 n),X) is Element of bool the carrier of (FTSL1 n)
{X} is non empty set
the InternalRel of (FTSL1 n) .: {X} is set
Im ((Nbdl1 n),v) is set
{v} is non empty set
(Nbdl1 n) .: {v} is set
v -' 1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
max ((v -' 1),1) is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
v + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
min ((v + 1),n) is V4() V5() V6() V10() complex V12() ext-real non negative integer set
{v,(max ((v -' 1),1)),(min ((v + 1),n))} is non empty set
0 + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
v - 1 is complex V12() ext-real integer set
0 + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
0 + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
1 - v is complex V12() ext-real integer set
1 + v is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
(1 + v) - v is complex V12() ext-real integer set
x2 - v is complex V12() ext-real integer set
abs (x2 - v) is complex V12() ext-real Element of REAL
x2 - v is complex V12() ext-real integer set
abs (x2 - v) is complex V12() ext-real Element of REAL
0 + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
0 + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
x2 is V4() V5() V6() V10() complex V12() ext-real non negative integer set
x2 + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
(x2 + 1) + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
X is V4() V5() V6() V10() complex V12() ext-real non negative integer set
v is V4() V5() V6() V10() complex V12() ext-real non negative integer set
X - v is complex V12() ext-real integer set
abs (X - v) is complex V12() ext-real Element of REAL
Y is Element of the carrier of (FTSL1 n)
U_FT (Y,(x2 + 1)) is Element of bool the carrier of (FTSL1 n)
U_FT (Y,x2) is Element of bool the carrier of (FTSL1 n)
(U_FT (Y,x2)) ^f is Element of bool the carrier of (FTSL1 n)
{ b1 where b1 is Element of the carrier of (FTSL1 n) : ex b2 being Element of the carrier of (FTSL1 n) st
( b2 in U_FT (Y,x2) & b1 in U_FT b2 ) } is set
nv is Element of the carrier of (FTSL1 n)
y is Element of the carrier of (FTSL1 n)
U_FT y is Element of bool the carrier of (FTSL1 n)
the InternalRel of (FTSL1 n) is Relation-like the carrier of (FTSL1 n) -defined the carrier of (FTSL1 n) -valued Element of bool [: the carrier of (FTSL1 n), the carrier of (FTSL1 n):]
[: the carrier of (FTSL1 n), the carrier of (FTSL1 n):] is non empty set
bool [: the carrier of (FTSL1 n), the carrier of (FTSL1 n):] is non empty set
Class ( the InternalRel of (FTSL1 n),y) is Element of bool the carrier of (FTSL1 n)
{y} is non empty set
the InternalRel of (FTSL1 n) .: {y} is set
y is Element of the carrier of (FTSL1 n)
U_FT y is Element of bool the carrier of (FTSL1 n)
the InternalRel of (FTSL1 n) is Relation-like the carrier of (FTSL1 n) -defined the carrier of (FTSL1 n) -valued Element of bool [: the carrier of (FTSL1 n), the carrier of (FTSL1 n):]
[: the carrier of (FTSL1 n), the carrier of (FTSL1 n):] is non empty set
bool [: the carrier of (FTSL1 n), the carrier of (FTSL1 n):] is non empty set
Class ( the InternalRel of (FTSL1 n),y) is Element of bool the carrier of (FTSL1 n)
{y} is non empty set
the InternalRel of (FTSL1 n) .: {y} is set
U_FT (y,0) is Element of bool the carrier of (FTSL1 n)
x3 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
x3 - v is complex V12() ext-real integer set
abs (x3 - v) is complex V12() ext-real Element of REAL
X - x3 is complex V12() ext-real integer set
abs (X - x3) is complex V12() ext-real Element of REAL
(abs (X - x3)) + (abs (x3 - v)) is complex V12() ext-real set
(x2 + 1) + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
(X - x3) + (x3 - v) is complex V12() ext-real integer set
abs ((X - x3) + (x3 - v)) is complex V12() ext-real Element of REAL
n is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
FT1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
n / 2 is complex V12() ext-real non negative Element of COMPLEX
[/(n / 2)\] is complex V12() ext-real integer set
FT2 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
FTSL1 FT2 is non empty RelStr
the carrier of (FTSL1 FT2) is non empty set
[: the carrier of (FTSL1 FT2), the carrier of (FTSL1 FT2):] is non empty set
bool [: the carrier of (FTSL1 FT2), the carrier of (FTSL1 FT2):] is non empty set
f is Relation-like the carrier of (FTSL1 FT2) -defined the carrier of (FTSL1 FT2) -valued Function-like quasi_total Element of bool [: the carrier of (FTSL1 FT2), the carrier of (FTSL1 FT2):]
0 + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
Seg FT2 is non empty V47() V54(FT2) Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT : ( 1 <= b1 & b1 <= FT2 ) } is set
Nbdl1 FT2 is Relation-like Seg FT2 -defined Seg FT2 -valued Element of bool [:(Seg FT2),(Seg FT2):]
[:(Seg FT2),(Seg FT2):] is non empty set
bool [:(Seg FT2),(Seg FT2):] is non empty set
RelStr(# (Seg FT2),(Nbdl1 FT2) #) is strict RelStr
f . FT2 is set
x2 is V4() V5() V6() V10() complex V12() ext-real non negative integer set
x1 is Element of the carrier of (FTSL1 FT2)
U_FT x1 is Element of bool the carrier of (FTSL1 FT2)
bool the carrier of (FTSL1 FT2) is non empty set
the InternalRel of (FTSL1 FT2) is Relation-like the carrier of (FTSL1 FT2) -defined the carrier of (FTSL1 FT2) -valued Element of bool [: the carrier of (FTSL1 FT2), the carrier of (FTSL1 FT2):]
Class ( the InternalRel of (FTSL1 FT2),x1) is Element of bool the carrier of (FTSL1 FT2)
{x1} is non empty set
the InternalRel of (FTSL1 FT2) .: {x1} is set
U_FT (x1,0) is Element of bool the carrier of (FTSL1 FT2)
U_FT (x1,FT1) is Element of bool the carrier of (FTSL1 FT2)
x1 is V4() V5() V6() V10() complex V12() ext-real non negative integer set
x1 is V4() V5() V6() V10() complex V12() ext-real non negative integer set
f . x1 is set
x1 is V4() V5() V6() V10() complex V12() ext-real non negative integer set
f . x1 is set
x1 - 1 is complex V12() ext-real integer set
x1 -' 1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
x1 + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
(x1 + 1) - 1 is complex V12() ext-real integer set
f . 1 is set
v is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
f . (x1 -' 1) is set
v is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
x2 is Element of the carrier of (FTSL1 FT2)
U_FT (x2,FT1) is Element of bool the carrier of (FTSL1 FT2)
x1 - v is complex V12() ext-real integer set
abs (x1 - v) is complex V12() ext-real Element of REAL
FT1 + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
x1 -' v is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
(FT1 + 1) + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
n + 2 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
Y is V4() V5() V6() V10() complex V12() ext-real non negative integer set
max ((x1 -' 1),1) is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
Im ((Nbdl1 FT2),x1) is set
{x1} is non empty set
(Nbdl1 FT2) .: {x1} is set
min ((x1 + 1),FT2) is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
{x1,(max ((x1 -' 1),1)),(min ((x1 + 1),FT2))} is non empty set
U_FT x2 is Element of bool the carrier of (FTSL1 FT2)
Class ( the InternalRel of (FTSL1 FT2),x2) is Element of bool the carrier of (FTSL1 FT2)
{x2} is non empty set
the InternalRel of (FTSL1 FT2) .: {x2} is set
U_FT (x2,0) is Element of bool the carrier of (FTSL1 FT2)
Y is V4() V5() V6() V10() complex V12() ext-real non negative integer set
Y is V4() V5() V6() V10() complex V12() ext-real non negative integer set
nv is Element of the carrier of (FTSL1 FT2)
U_FT (nv,FT1) is Element of bool the carrier of (FTSL1 FT2)
dom f is Element of bool the carrier of (FTSL1 FT2)
f .: (U_FT (x2,0)) is Element of bool the carrier of (FTSL1 FT2)
y is Element of the carrier of (FTSL1 FT2)
U_FT y is Element of bool the carrier of (FTSL1 FT2)
Class ( the InternalRel of (FTSL1 FT2),y) is Element of bool the carrier of (FTSL1 FT2)
{y} is non empty set
the InternalRel of (FTSL1 FT2) .: {y} is set
U_FT (y,0) is Element of bool the carrier of (FTSL1 FT2)
U_FT (y,FT1) is Element of bool the carrier of (FTSL1 FT2)
(x1 -' 1) + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
Y - x1 is complex V12() ext-real integer set
Y -' x1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
(x1 -' 1) - Y is complex V12() ext-real integer set
abs ((x1 -' 1) - Y) is complex V12() ext-real Element of REAL
Y - (x1 -' 1) is complex V12() ext-real integer set
abs (Y - (x1 -' 1)) is complex V12() ext-real Element of REAL
(Y -' x1) + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
(Y - x1) + 1 is complex V12() ext-real integer set
((FT1 + 1) + 1) + ((FT1 + 1) + 1) is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
(x1 - v) + ((Y - x1) + 1) is complex V12() ext-real integer set
((FT1 + 1) + 1) + (FT1 + 1) is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
(((FT1 + 1) + 1) + (FT1 + 1)) + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
Y - v is complex V12() ext-real integer set
(Y - v) + 1 is complex V12() ext-real integer set
((FT1 + 1) + 1) + FT1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
(((FT1 + 1) + 1) + FT1) + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
((((FT1 + 1) + 1) + FT1) + 1) - 1 is complex V12() ext-real integer set
(Y - v) - 1 is complex V12() ext-real integer set
2 * FT1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
(2 * FT1) + 2 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
((2 * FT1) + 2) / 2 is complex V12() ext-real non negative Element of COMPLEX
((Y - v) - 1) / 2 is complex V12() ext-real Element of COMPLEX
2 / 2 is complex V12() ext-real non negative Element of COMPLEX
(n / 2) + (2 / 2) is complex V12() ext-real non negative Element of COMPLEX
[/(n / 2)\] + (2 / 2) is complex V12() ext-real set
((n / 2) + (2 / 2)) * 2 is complex V12() ext-real non negative set
(((Y - v) - 1) / 2) * 2 is complex V12() ext-real set
((Y - v) - 1) + 1 is complex V12() ext-real integer set
n + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
abs (Y - v) is complex V12() ext-real Element of REAL
X is Element of the carrier of (FTSL1 FT2)
U_FT (X,n) is Element of bool the carrier of (FTSL1 FT2)
v - Y is complex V12() ext-real integer set
abs (v - Y) is complex V12() ext-real Element of REAL
f . (x1 -' 1) is set
n is set
FT1 is set
[:n,FT1:] is set
bool [:n,FT1:] is non empty set
FT2 is Relation-like n -defined FT1 -valued Element of bool [:n,FT1:]
f is set
Im (FT2,f) is set
{f} is non empty set
FT2 .: {f} is set
bool FT1 is non empty set
FT2 .: {f} is Element of bool FT1
n is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
Seg n is V47() V54(n) Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
FT1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
Seg FT1 is V47() V54(FT1) Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT : ( 1 <= b1 & b1 <= FT1 ) } is set
[:(Seg n),(Seg FT1):] is set
[:[:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):]:] is set
bool [:[:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):]:] is non empty set
Nbdl1 n is Relation-like Seg n -defined Seg n -valued Element of bool [:(Seg n),(Seg n):]
[:(Seg n),(Seg n):] is set
bool [:(Seg n),(Seg n):] is non empty set
Nbdl1 FT1 is Relation-like Seg FT1 -defined Seg FT1 -valued Element of bool [:(Seg FT1),(Seg FT1):]
[:(Seg FT1),(Seg FT1):] is set
bool [:(Seg FT1),(Seg FT1):] is non empty set
bool [:(Seg n),(Seg FT1):] is non empty set
FT2 is set
f is set
x1 is set
[f,x1] is set
{f,x1} is non empty set
{f} is non empty set
{{f,x1},{f}} is non empty set
x2 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
((Seg n),(Seg n),(Nbdl1 n),x2) is Element of bool (Seg n)
bool (Seg n) is non empty set
{x2} is non empty set
(Nbdl1 n) .: {x2} is set
v is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
((Seg FT1),(Seg FT1),(Nbdl1 FT1),v) is Element of bool (Seg FT1)
bool (Seg FT1) is non empty set
{v} is non empty set
(Nbdl1 FT1) .: {v} is set
[:((Seg n),(Seg n),(Nbdl1 n),x2),((Seg FT1),(Seg FT1),(Nbdl1 FT1),v):] is set
Y is set
nv is set
y is set
[nv,y] is set
{nv,y} is non empty set
{nv} is non empty set
{{nv,y},{nv}} is non empty set
Y is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
nv is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
[Y,nv] is set
{Y,nv} is non empty set
{Y} is non empty set
{{Y,nv},{Y}} is non empty set
((Seg n),(Seg n),(Nbdl1 n),Y) is Element of bool (Seg n)
(Nbdl1 n) .: {Y} is set
((Seg FT1),(Seg FT1),(Nbdl1 FT1),nv) is Element of bool (Seg FT1)
{nv} is non empty set
(Nbdl1 FT1) .: {nv} is set
[:((Seg n),(Seg n),(Nbdl1 n),Y),((Seg FT1),(Seg FT1),(Nbdl1 FT1),nv):] is set
[:[:(Seg n),(Seg FT1):],(bool [:(Seg n),(Seg FT1):]):] is set
bool [:[:(Seg n),(Seg FT1):],(bool [:(Seg n),(Seg FT1):]):] is non empty set
FT2 is Relation-like [:(Seg n),(Seg FT1):] -defined bool [:(Seg n),(Seg FT1):] -valued Function-like quasi_total Element of bool [:[:(Seg n),(Seg FT1):],(bool [:(Seg n),(Seg FT1):]):]
f is Relation-like [:(Seg n),(Seg FT1):] -defined [:(Seg n),(Seg FT1):] -valued Element of bool [:[:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):]:]
x1 is set
([:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):],f,x1) is Relation-like Seg n -defined Seg FT1 -valued Element of bool [:(Seg n),(Seg FT1):]
{x1} is non empty set
f .: {x1} is set
x2 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
v is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
[x2,v] is set
{x2,v} is non empty set
{x2} is non empty set
{{x2,v},{x2}} is non empty set
((Seg n),(Seg n),(Nbdl1 n),x2) is Element of bool (Seg n)
bool (Seg n) is non empty set
(Nbdl1 n) .: {x2} is set
((Seg FT1),(Seg FT1),(Nbdl1 FT1),v) is Element of bool (Seg FT1)
bool (Seg FT1) is non empty set
{v} is non empty set
(Nbdl1 FT1) .: {v} is set
[:((Seg n),(Seg n),(Nbdl1 n),x2),((Seg FT1),(Seg FT1),(Nbdl1 FT1),v):] is set
FT2 . x1 is set
FT2 is Relation-like [:(Seg n),(Seg FT1):] -defined [:(Seg n),(Seg FT1):] -valued Element of bool [:[:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):]:]
f is Relation-like [:(Seg n),(Seg FT1):] -defined [:(Seg n),(Seg FT1):] -valued Element of bool [:[:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):]:]
x1 is set
([:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):],FT2,x1) is Relation-like Seg n -defined Seg FT1 -valued Element of bool [:(Seg n),(Seg FT1):]
bool [:(Seg n),(Seg FT1):] is non empty set
{x1} is non empty set
FT2 .: {x1} is set
([:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):],f,x1) is Relation-like Seg n -defined Seg FT1 -valued Element of bool [:(Seg n),(Seg FT1):]
f .: {x1} is set
x2 is set
v is set
[x2,v] is set
{x2,v} is non empty set
{x2} is non empty set
{{x2,v},{x2}} is non empty set
X is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
((Seg n),(Seg n),(Nbdl1 n),X) is Element of bool (Seg n)
bool (Seg n) is non empty set
{X} is non empty set
(Nbdl1 n) .: {X} is set
Y is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
((Seg FT1),(Seg FT1),(Nbdl1 FT1),Y) is Element of bool (Seg FT1)
bool (Seg FT1) is non empty set
{Y} is non empty set
(Nbdl1 FT1) .: {Y} is set
[:((Seg n),(Seg n),(Nbdl1 n),X),((Seg FT1),(Seg FT1),(Nbdl1 FT1),Y):] is set
n is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
Seg n is V47() V54(n) Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
FT1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
Seg FT1 is V47() V54(FT1) Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT : ( 1 <= b1 & b1 <= FT1 ) } is set
[:(Seg n),(Seg FT1):] is set
(n,FT1) is Relation-like [:(Seg n),(Seg FT1):] -defined [:(Seg n),(Seg FT1):] -valued Element of bool [:[:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):]:]
[:[:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):]:] is set
bool [:[:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):]:] is non empty set
RelStr(# [:(Seg n),(Seg FT1):],(n,FT1) #) is strict RelStr
n is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
FT1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
(n,FT1) is strict RelStr
Seg n is non empty V47() V54(n) Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
Seg FT1 is non empty V47() V54(FT1) Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT : ( 1 <= b1 & b1 <= FT1 ) } is set
[:(Seg n),(Seg FT1):] is non empty set
(n,FT1) is Relation-like [:(Seg n),(Seg FT1):] -defined [:(Seg n),(Seg FT1):] -valued Element of bool [:[:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):]:]
[:[:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):]:] is non empty set
bool [:[:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):]:] is non empty set
RelStr(# [:(Seg n),(Seg FT1):],(n,FT1) #) is strict RelStr
n is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
FT1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
(n,FT1) is non empty strict RelStr
Seg n is non empty V47() V54(n) Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
Seg FT1 is non empty V47() V54(FT1) Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT : ( 1 <= b1 & b1 <= FT1 ) } is set
[:(Seg n),(Seg FT1):] is non empty set
(n,FT1) is Relation-like [:(Seg n),(Seg FT1):] -defined [:(Seg n),(Seg FT1):] -valued Element of bool [:[:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):]:]
[:[:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):]:] is non empty set
bool [:[:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):]:] is non empty set
RelStr(# [:(Seg n),(Seg FT1):],(n,FT1) #) is strict RelStr
the carrier of (n,FT1) is non empty set
FT2 is Element of the carrier of (n,FT1)
U_FT FT2 is Element of bool the carrier of (n,FT1)
bool the carrier of (n,FT1) is non empty set
the InternalRel of (n,FT1) is Relation-like the carrier of (n,FT1) -defined the carrier of (n,FT1) -valued Element of bool [: the carrier of (n,FT1), the carrier of (n,FT1):]
[: the carrier of (n,FT1), the carrier of (n,FT1):] is non empty set
bool [: the carrier of (n,FT1), the carrier of (n,FT1):] is non empty set
Class ( the InternalRel of (n,FT1),FT2) is Element of bool the carrier of (n,FT1)
{FT2} is non empty set
the InternalRel of (n,FT1) .: {FT2} is set
f is set
x1 is set
[f,x1] is set
{f,x1} is non empty set
{f} is non empty set
{{f,x1},{f}} is non empty set
FTSL1 FT1 is non empty RelStr
Nbdl1 FT1 is Relation-like Seg FT1 -defined Seg FT1 -valued Element of bool [:(Seg FT1),(Seg FT1):]
[:(Seg FT1),(Seg FT1):] is non empty set
bool [:(Seg FT1),(Seg FT1):] is non empty set
RelStr(# (Seg FT1),(Nbdl1 FT1) #) is strict RelStr
the carrier of (FTSL1 FT1) is non empty set
v is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
FTSL1 n is non empty RelStr
Nbdl1 n is Relation-like Seg n -defined Seg n -valued Element of bool [:(Seg n),(Seg n):]
[:(Seg n),(Seg n):] is non empty set
bool [:(Seg n),(Seg n):] is non empty set
RelStr(# (Seg n),(Nbdl1 n) #) is strict RelStr
the carrier of (FTSL1 n) is non empty set
x2 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
X is Element of the carrier of (FTSL1 FT1)
U_FT X is Element of bool the carrier of (FTSL1 FT1)
bool the carrier of (FTSL1 FT1) is non empty set
the InternalRel of (FTSL1 FT1) is Relation-like the carrier of (FTSL1 FT1) -defined the carrier of (FTSL1 FT1) -valued Element of bool [: the carrier of (FTSL1 FT1), the carrier of (FTSL1 FT1):]
[: the carrier of (FTSL1 FT1), the carrier of (FTSL1 FT1):] is non empty set
bool [: the carrier of (FTSL1 FT1), the carrier of (FTSL1 FT1):] is non empty set
Class ( the InternalRel of (FTSL1 FT1),X) is Element of bool the carrier of (FTSL1 FT1)
{X} is non empty set
the InternalRel of (FTSL1 FT1) .: {X} is set
Y is Element of the carrier of (FTSL1 n)
U_FT Y is Element of bool the carrier of (FTSL1 n)
bool the carrier of (FTSL1 n) is non empty set
the InternalRel of (FTSL1 n) is Relation-like the carrier of (FTSL1 n) -defined the carrier of (FTSL1 n) -valued Element of bool [: the carrier of (FTSL1 n), the carrier of (FTSL1 n):]
[: the carrier of (FTSL1 n), the carrier of (FTSL1 n):] is non empty set
bool [: the carrier of (FTSL1 n), the carrier of (FTSL1 n):] is non empty set
Class ( the InternalRel of (FTSL1 n),Y) is Element of bool the carrier of (FTSL1 n)
{Y} is non empty set
the InternalRel of (FTSL1 n) .: {Y} is set
((Seg n),(Seg n),(Nbdl1 n),x2) is Element of bool (Seg n)
bool (Seg n) is non empty set
{x2} is non empty set
(Nbdl1 n) .: {x2} is set
((Seg FT1),(Seg FT1),(Nbdl1 FT1),v) is Element of bool (Seg FT1)
bool (Seg FT1) is non empty set
{v} is non empty set
(Nbdl1 FT1) .: {v} is set
[:((Seg n),(Seg n),(Nbdl1 n),x2),((Seg FT1),(Seg FT1),(Nbdl1 FT1),v):] is set
n is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
FT1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
(n,FT1) is non empty strict RelStr
Seg n is non empty V47() V54(n) Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
Seg FT1 is non empty V47() V54(FT1) Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT : ( 1 <= b1 & b1 <= FT1 ) } is set
[:(Seg n),(Seg FT1):] is non empty set
(n,FT1) is Relation-like [:(Seg n),(Seg FT1):] -defined [:(Seg n),(Seg FT1):] -valued Element of bool [:[:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):]:]
[:[:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):]:] is non empty set
bool [:[:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):]:] is non empty set
RelStr(# [:(Seg n),(Seg FT1):],(n,FT1) #) is strict RelStr
the carrier of (n,FT1) is non empty set
FTSL1 FT1 is non empty RelStr
f is Element of the carrier of (n,FT1)
FT2 is Element of the carrier of (n,FT1)
U_FT FT2 is Element of bool the carrier of (n,FT1)
bool the carrier of (n,FT1) is non empty set
the InternalRel of (n,FT1) is Relation-like the carrier of (n,FT1) -defined the carrier of (n,FT1) -valued Element of bool [: the carrier of (n,FT1), the carrier of (n,FT1):]
[: the carrier of (n,FT1), the carrier of (n,FT1):] is non empty set
bool [: the carrier of (n,FT1), the carrier of (n,FT1):] is non empty set
Class ( the InternalRel of (n,FT1),FT2) is Element of bool the carrier of (n,FT1)
{FT2} is non empty set
the InternalRel of (n,FT1) .: {FT2} is set
U_FT f is Element of bool the carrier of (n,FT1)
Class ( the InternalRel of (n,FT1),f) is Element of bool the carrier of (n,FT1)
{f} is non empty set
the InternalRel of (n,FT1) .: {f} is set
x1 is set
x2 is set
[x1,x2] is set
{x1,x2} is non empty set
{x1} is non empty set
{{x1,x2},{x1}} is non empty set
Y is set
nv is set
[Y,nv] is set
{Y,nv} is non empty set
{Y} is non empty set
{{Y,nv},{Y}} is non empty set
Nbdl1 FT1 is Relation-like Seg FT1 -defined Seg FT1 -valued Element of bool [:(Seg FT1),(Seg FT1):]
[:(Seg FT1),(Seg FT1):] is non empty set
bool [:(Seg FT1),(Seg FT1):] is non empty set
RelStr(# (Seg FT1),(Nbdl1 FT1) #) is strict RelStr
the carrier of (FTSL1 FT1) is non empty set
X is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
x3 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
Nbdl1 n is Relation-like Seg n -defined Seg n -valued Element of bool [:(Seg n),(Seg n):]
[:(Seg n),(Seg n):] is non empty set
bool [:(Seg n),(Seg n):] is non empty set
v is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
((Seg n),(Seg n),(Nbdl1 n),v) is Element of bool (Seg n)
bool (Seg n) is non empty set
{v} is non empty set
(Nbdl1 n) .: {v} is set
((Seg FT1),(Seg FT1),(Nbdl1 FT1),X) is Element of bool (Seg FT1)
bool (Seg FT1) is non empty set
{X} is non empty set
(Nbdl1 FT1) .: {X} is set
[:((Seg n),(Seg n),(Nbdl1 n),v),((Seg FT1),(Seg FT1),(Nbdl1 FT1),X):] is set
Class ((Nbdl1 n),v) is Element of bool (Seg n)
Class ((Nbdl1 FT1),X) is Element of bool (Seg FT1)
u2 is Element of the carrier of (FTSL1 FT1)
U_FT u2 is Element of bool the carrier of (FTSL1 FT1)
bool the carrier of (FTSL1 FT1) is non empty set
the InternalRel of (FTSL1 FT1) is Relation-like the carrier of (FTSL1 FT1) -defined the carrier of (FTSL1 FT1) -valued Element of bool [: the carrier of (FTSL1 FT1), the carrier of (FTSL1 FT1):]
[: the carrier of (FTSL1 FT1), the carrier of (FTSL1 FT1):] is non empty set
bool [: the carrier of (FTSL1 FT1), the carrier of (FTSL1 FT1):] is non empty set
Class ( the InternalRel of (FTSL1 FT1),u2) is Element of bool the carrier of (FTSL1 FT1)
{u2} is non empty set
the InternalRel of (FTSL1 FT1) .: {u2} is set
pj2 is set
pi2 is set
[pj2,pi2] is set
{pj2,pi2} is non empty set
{pj2} is non empty set
{{pj2,pi2},{pj2}} is non empty set
v2 is Element of the carrier of (FTSL1 FT1)
U_FT v2 is Element of bool the carrier of (FTSL1 FT1)
Class ( the InternalRel of (FTSL1 FT1),v2) is Element of bool the carrier of (FTSL1 FT1)
{v2} is non empty set
the InternalRel of (FTSL1 FT1) .: {v2} is set
FTSL1 n is non empty RelStr
RelStr(# (Seg n),(Nbdl1 n) #) is strict RelStr
the carrier of (FTSL1 n) is non empty set
y is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
pi2 is Element of the carrier of (FTSL1 n)
pj2 is Element of the carrier of (FTSL1 n)
U_FT pj2 is Element of bool the carrier of (FTSL1 n)
bool the carrier of (FTSL1 n) is non empty set
the InternalRel of (FTSL1 n) is Relation-like the carrier of (FTSL1 n) -defined the carrier of (FTSL1 n) -valued Element of bool [: the carrier of (FTSL1 n), the carrier of (FTSL1 n):]
[: the carrier of (FTSL1 n), the carrier of (FTSL1 n):] is non empty set
bool [: the carrier of (FTSL1 n), the carrier of (FTSL1 n):] is non empty set
Class ( the InternalRel of (FTSL1 n),pj2) is Element of bool the carrier of (FTSL1 n)
{pj2} is non empty set
the InternalRel of (FTSL1 n) .: {pj2} is set
y1 is set
y2 is set
[y1,y2] is set
{y1,y2} is non empty set
{y1} is non empty set
{{y1,y2},{y1}} is non empty set
U_FT pi2 is Element of bool the carrier of (FTSL1 n)
Class ( the InternalRel of (FTSL1 n),pi2) is Element of bool the carrier of (FTSL1 n)
{pi2} is non empty set
the InternalRel of (FTSL1 n) .: {pi2} is set
((Seg n),(Seg n),(Nbdl1 n),y) is Element of bool (Seg n)
{y} is non empty set
(Nbdl1 n) .: {y} is set
((Seg FT1),(Seg FT1),(Nbdl1 FT1),x3) is Element of bool (Seg FT1)
{x3} is non empty set
(Nbdl1 FT1) .: {x3} is set
[:((Seg n),(Seg n),(Nbdl1 n),y),((Seg FT1),(Seg FT1),(Nbdl1 FT1),x3):] is set
n is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
(n,1) is non empty strict RelStr
Seg n is non empty V47() V54(n) Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
Seg 1 is non empty V47() V54(1) Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
[:(Seg n),(Seg 1):] is non empty set
(n,1) is Relation-like [:(Seg n),(Seg 1):] -defined [:(Seg n),(Seg 1):] -valued Element of bool [:[:(Seg n),(Seg 1):],[:(Seg n),(Seg 1):]:]
[:[:(Seg n),(Seg 1):],[:(Seg n),(Seg 1):]:] is non empty set
bool [:[:(Seg n),(Seg 1):],[:(Seg n),(Seg 1):]:] is non empty set
RelStr(# [:(Seg n),(Seg 1):],(n,1) #) is strict RelStr
the carrier of (n,1) is non empty set
FTSL1 n is non empty RelStr
the carrier of (FTSL1 n) is non empty set
[: the carrier of (n,1), the carrier of (FTSL1 n):] is non empty set
bool [: the carrier of (n,1), the carrier of (FTSL1 n):] is non empty set
f is set
Nbdl1 n is Relation-like Seg n -defined Seg n -valued Element of bool [:(Seg n),(Seg n):]
[:(Seg n),(Seg n):] is non empty set
bool [:(Seg n),(Seg n):] is non empty set
RelStr(# (Seg n),(Nbdl1 n) #) is strict RelStr
x1 is set
x2 is set
[x1,x2] is set
{x1,x2} is non empty set
{x1} is non empty set
{{x1,x2},{x1}} is non empty set
X is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
v is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
[v,1] is set
{v,1} is non empty set
{v} is non empty set
{{v,1},{v}} is non empty set
f is Relation-like the carrier of (n,1) -defined the carrier of (FTSL1 n) -valued Function-like quasi_total Element of bool [: the carrier of (n,1), the carrier of (FTSL1 n):]
f is Relation-like the carrier of (n,1) -defined the carrier of (FTSL1 n) -valued Function-like quasi_total Element of bool [: the carrier of (n,1), the carrier of (FTSL1 n):]
Nbdl1 n is Relation-like Seg n -defined Seg n -valued Element of bool [:(Seg n),(Seg n):]
[:(Seg n),(Seg n):] is non empty set
bool [:(Seg n),(Seg n):] is non empty set
RelStr(# (Seg n),(Nbdl1 n) #) is strict RelStr
rng f is Element of bool the carrier of (FTSL1 n)
bool the carrier of (FTSL1 n) is non empty set
x1 is set
[x1,1] is set
{x1,1} is non empty set
{x1} is non empty set
{{x1,1},{x1}} is non empty set
f . [x1,1] is set
[(f . [x1,1]),1] is set
{(f . [x1,1]),1} is non empty set
{(f . [x1,1])} is non empty set
{{(f . [x1,1]),1},{(f . [x1,1])}} is non empty set
dom f is Element of bool the carrier of (n,1)
bool the carrier of (n,1) is non empty set
the InternalRel of (FTSL1 n) is Relation-like the carrier of (FTSL1 n) -defined the carrier of (FTSL1 n) -valued Element of bool [: the carrier of (FTSL1 n), the carrier of (FTSL1 n):]
[: the carrier of (FTSL1 n), the carrier of (FTSL1 n):] is non empty set
bool [: the carrier of (FTSL1 n), the carrier of (FTSL1 n):] is non empty set
x1 is Element of the carrier of (n,1)
U_FT x1 is Element of bool the carrier of (n,1)
bool the carrier of (n,1) is non empty set
the InternalRel of (n,1) is Relation-like the carrier of (n,1) -defined the carrier of (n,1) -valued Element of bool [: the carrier of (n,1), the carrier of (n,1):]
[: the carrier of (n,1), the carrier of (n,1):] is non empty set
bool [: the carrier of (n,1), the carrier of (n,1):] is non empty set
Class ( the InternalRel of (n,1),x1) is Element of bool the carrier of (n,1)
{x1} is non empty set
the InternalRel of (n,1) .: {x1} is set
f .: (U_FT x1) is Element of bool the carrier of (FTSL1 n)
f . x1 is Element of the carrier of (FTSL1 n)
( the carrier of (FTSL1 n), the carrier of (FTSL1 n), the InternalRel of (FTSL1 n),(f . x1)) is Element of bool the carrier of (FTSL1 n)
{(f . x1)} is non empty set
the InternalRel of (FTSL1 n) .: {(f . x1)} is set
x2 is set
v is set
[x2,v] is set
{x2,v} is non empty set
{x2} is non empty set
{{x2,v},{x2}} is non empty set
Y is set
X is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
((Seg n),(Seg n),(Nbdl1 n),(f . x1)) is Element of bool (Seg n)
bool (Seg n) is non empty set
(Nbdl1 n) .: {(f . x1)} is set
dom f is Element of bool the carrier of (n,1)
nv is set
f . nv is set
Nbdl1 1 is Relation-like Seg 1 -defined Seg 1 -valued Element of bool [:(Seg 1),(Seg 1):]
[:(Seg 1),(Seg 1):] is non empty set
bool [:(Seg 1),(Seg 1):] is non empty set
((Seg 1),(Seg 1),(Nbdl1 1),v) is Element of bool (Seg 1)
bool (Seg 1) is non empty set
{v} is non empty set
(Nbdl1 1) .: {v} is set
X -' 1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
max ((X -' 1),1) is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
X + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
min ((X + 1),1) is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
{X,(max ((X -' 1),1)),(min ((X + 1),1))} is non empty set
max (0,1) is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
min (2,1) is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
{1,(max (0,1)),(min (2,1))} is non empty set
{1,1,(min (2,1))} is non empty set
{1,(min (2,1))} is non empty set
{1,1} is non empty set
{1} is non empty set
([:(Seg n),(Seg 1):],[:(Seg n),(Seg 1):],(n,1),x1) is Relation-like Seg n -defined Seg 1 -valued Element of bool [:(Seg n),(Seg 1):]
bool [:(Seg n),(Seg 1):] is non empty set
(n,1) .: {x1} is set
((Seg n),(Seg n),(Nbdl1 n),x2) is Element of bool (Seg n)
(Nbdl1 n) .: {x2} is set
[:((Seg n),(Seg n),(Nbdl1 n),x2),((Seg 1),(Seg 1),(Nbdl1 1),v):] is set
[(f . x1),1] is set
{(f . x1),1} is non empty set
{{(f . x1),1},{(f . x1)}} is non empty set
[(f . nv),1] is set
{(f . nv),1} is non empty set
{(f . nv)} is non empty set
{{(f . nv),1},{(f . nv)}} is non empty set
[(f . x1),1] is set
{(f . x1),1} is non empty set
{{(f . x1),1},{(f . x1)}} is non empty set
X is set
dom f is Element of bool the carrier of (n,1)
([:(Seg n),(Seg 1):],[:(Seg n),(Seg 1):],(n,1),x1) is Relation-like Seg n -defined Seg 1 -valued Element of bool [:(Seg n),(Seg 1):]
bool [:(Seg n),(Seg 1):] is non empty set
(n,1) .: {x1} is set
Y is set
f . Y is set
((Seg n),(Seg n),(Nbdl1 n),x2) is Element of bool (Seg n)
bool (Seg n) is non empty set
(Nbdl1 n) .: {x2} is set
Nbdl1 1 is Relation-like Seg 1 -defined Seg 1 -valued Element of bool [:(Seg 1),(Seg 1):]
[:(Seg 1),(Seg 1):] is non empty set
bool [:(Seg 1),(Seg 1):] is non empty set
((Seg 1),(Seg 1),(Nbdl1 1),v) is Element of bool (Seg 1)
bool (Seg 1) is non empty set
{v} is non empty set
(Nbdl1 1) .: {v} is set
[:((Seg n),(Seg n),(Nbdl1 n),x2),((Seg 1),(Seg 1),(Nbdl1 1),v):] is set
[(f . Y),1] is set
{(f . Y),1} is non empty set
{(f . Y)} is non empty set
{{(f . Y),1},{(f . Y)}} is non empty set
dom f is Element of bool the carrier of (n,1)
bool the carrier of (n,1) is non empty set
x1 is set
x2 is set
f . x1 is set
f . x2 is set
[(f . x1),1] is set
{(f . x1),1} is non empty set
{(f . x1)} is non empty set
{{(f . x1),1},{(f . x1)}} is non empty set
n is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
Seg n is V47() V54(n) Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
FT1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
Seg FT1 is V47() V54(FT1) Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT : ( 1 <= b1 & b1 <= FT1 ) } is set
[:(Seg n),(Seg FT1):] is set
[:[:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):]:] is set
bool [:[:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):]:] is non empty set
Nbdl1 FT1 is Relation-like Seg FT1 -defined Seg FT1 -valued Element of bool [:(Seg FT1),(Seg FT1):]
[:(Seg FT1),(Seg FT1):] is set
bool [:(Seg FT1),(Seg FT1):] is non empty set
Nbdl1 n is Relation-like Seg n -defined Seg n -valued Element of bool [:(Seg n),(Seg n):]
[:(Seg n),(Seg n):] is set
bool [:(Seg n),(Seg n):] is non empty set
bool [:(Seg n),(Seg FT1):] is non empty set
FT2 is set
f is set
x1 is set
[f,x1] is set
{f,x1} is non empty set
{f} is non empty set
{{f,x1},{f}} is non empty set
x2 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
{x2} is non empty set
v is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
((Seg FT1),(Seg FT1),(Nbdl1 FT1),v) is Element of bool (Seg FT1)
bool (Seg FT1) is non empty set
{v} is non empty set
(Nbdl1 FT1) .: {v} is set
[:{x2},((Seg FT1),(Seg FT1),(Nbdl1 FT1),v):] is set
((Seg n),(Seg n),(Nbdl1 n),f) is Element of bool (Seg n)
bool (Seg n) is non empty set
(Nbdl1 n) .: {f} is set
[:((Seg n),(Seg n),(Nbdl1 n),f),{v}:] is set
[:{x2},((Seg FT1),(Seg FT1),(Nbdl1 FT1),v):] \/ [:((Seg n),(Seg n),(Nbdl1 n),f),{v}:] is set
Y is set
nv is set
y is set
[nv,y] is set
{nv,y} is non empty set
{nv} is non empty set
{{nv,y},{nv}} is non empty set
nv is set
y is set
[nv,y] is set
{nv,y} is non empty set
{nv} is non empty set
{{nv,y},{nv}} is non empty set
Y is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
nv is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
[Y,nv] is set
{Y,nv} is non empty set
{Y} is non empty set
{{Y,nv},{Y}} is non empty set
((Seg FT1),(Seg FT1),(Nbdl1 FT1),nv) is Element of bool (Seg FT1)
{nv} is non empty set
(Nbdl1 FT1) .: {nv} is set
[:{Y},((Seg FT1),(Seg FT1),(Nbdl1 FT1),nv):] is set
((Seg n),(Seg n),(Nbdl1 n),Y) is Element of bool (Seg n)
(Nbdl1 n) .: {Y} is set
[:((Seg n),(Seg n),(Nbdl1 n),Y),{nv}:] is set
[:{Y},((Seg FT1),(Seg FT1),(Nbdl1 FT1),nv):] \/ [:((Seg n),(Seg n),(Nbdl1 n),Y),{nv}:] is set
[:[:(Seg n),(Seg FT1):],(bool [:(Seg n),(Seg FT1):]):] is set
bool [:[:(Seg n),(Seg FT1):],(bool [:(Seg n),(Seg FT1):]):] is non empty set
FT2 is Relation-like [:(Seg n),(Seg FT1):] -defined bool [:(Seg n),(Seg FT1):] -valued Function-like quasi_total Element of bool [:[:(Seg n),(Seg FT1):],(bool [:(Seg n),(Seg FT1):]):]
f is Relation-like [:(Seg n),(Seg FT1):] -defined [:(Seg n),(Seg FT1):] -valued Element of bool [:[:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):]:]
x1 is set
([:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):],f,x1) is Relation-like Seg n -defined Seg FT1 -valued Element of bool [:(Seg n),(Seg FT1):]
{x1} is non empty set
f .: {x1} is set
x2 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
v is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
[x2,v] is set
{x2,v} is non empty set
{x2} is non empty set
{{x2,v},{x2}} is non empty set
((Seg FT1),(Seg FT1),(Nbdl1 FT1),v) is Element of bool (Seg FT1)
bool (Seg FT1) is non empty set
{v} is non empty set
(Nbdl1 FT1) .: {v} is set
[:{x2},((Seg FT1),(Seg FT1),(Nbdl1 FT1),v):] is set
((Seg n),(Seg n),(Nbdl1 n),x2) is Element of bool (Seg n)
bool (Seg n) is non empty set
(Nbdl1 n) .: {x2} is set
[:((Seg n),(Seg n),(Nbdl1 n),x2),{v}:] is set
[:{x2},((Seg FT1),(Seg FT1),(Nbdl1 FT1),v):] \/ [:((Seg n),(Seg n),(Nbdl1 n),x2),{v}:] is set
FT2 . x1 is set
FT2 is Relation-like [:(Seg n),(Seg FT1):] -defined [:(Seg n),(Seg FT1):] -valued Element of bool [:[:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):]:]
f is Relation-like [:(Seg n),(Seg FT1):] -defined [:(Seg n),(Seg FT1):] -valued Element of bool [:[:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):]:]
x1 is set
([:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):],FT2,x1) is Relation-like Seg n -defined Seg FT1 -valued Element of bool [:(Seg n),(Seg FT1):]
bool [:(Seg n),(Seg FT1):] is non empty set
{x1} is non empty set
FT2 .: {x1} is set
([:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):],f,x1) is Relation-like Seg n -defined Seg FT1 -valued Element of bool [:(Seg n),(Seg FT1):]
f .: {x1} is set
x2 is set
v is set
[x2,v] is set
{x2,v} is non empty set
{x2} is non empty set
{{x2,v},{x2}} is non empty set
X is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
{X} is non empty set
Y is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
((Seg FT1),(Seg FT1),(Nbdl1 FT1),Y) is Element of bool (Seg FT1)
bool (Seg FT1) is non empty set
{Y} is non empty set
(Nbdl1 FT1) .: {Y} is set
[:{X},((Seg FT1),(Seg FT1),(Nbdl1 FT1),Y):] is set
((Seg n),(Seg n),(Nbdl1 n),x2) is Element of bool (Seg n)
bool (Seg n) is non empty set
(Nbdl1 n) .: {x2} is set
[:((Seg n),(Seg n),(Nbdl1 n),x2),{Y}:] is set
[:{X},((Seg FT1),(Seg FT1),(Nbdl1 FT1),Y):] \/ [:((Seg n),(Seg n),(Nbdl1 n),x2),{Y}:] is set
n is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
Seg n is V47() V54(n) Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
FT1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
Seg FT1 is V47() V54(FT1) Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT : ( 1 <= b1 & b1 <= FT1 ) } is set
[:(Seg n),(Seg FT1):] is set
(n,FT1) is Relation-like [:(Seg n),(Seg FT1):] -defined [:(Seg n),(Seg FT1):] -valued Element of bool [:[:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):]:]
[:[:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):]:] is set
bool [:[:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):]:] is non empty set
RelStr(# [:(Seg n),(Seg FT1):],(n,FT1) #) is strict RelStr
n is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
FT1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
(n,FT1) is strict RelStr
Seg n is non empty V47() V54(n) Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
Seg FT1 is non empty V47() V54(FT1) Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT : ( 1 <= b1 & b1 <= FT1 ) } is set
[:(Seg n),(Seg FT1):] is non empty set
(n,FT1) is Relation-like [:(Seg n),(Seg FT1):] -defined [:(Seg n),(Seg FT1):] -valued Element of bool [:[:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):]:]
[:[:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):]:] is non empty set
bool [:[:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):]:] is non empty set
RelStr(# [:(Seg n),(Seg FT1):],(n,FT1) #) is strict RelStr
n is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
FT1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
(n,FT1) is non empty strict RelStr
Seg n is non empty V47() V54(n) Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
Seg FT1 is non empty V47() V54(FT1) Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT : ( 1 <= b1 & b1 <= FT1 ) } is set
[:(Seg n),(Seg FT1):] is non empty set
(n,FT1) is Relation-like [:(Seg n),(Seg FT1):] -defined [:(Seg n),(Seg FT1):] -valued Element of bool [:[:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):]:]
[:[:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):]:] is non empty set
bool [:[:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):]:] is non empty set
RelStr(# [:(Seg n),(Seg FT1):],(n,FT1) #) is strict RelStr
the carrier of (n,FT1) is non empty set
FT2 is Element of the carrier of (n,FT1)
U_FT FT2 is Element of bool the carrier of (n,FT1)
bool the carrier of (n,FT1) is non empty set
the InternalRel of (n,FT1) is Relation-like the carrier of (n,FT1) -defined the carrier of (n,FT1) -valued Element of bool [: the carrier of (n,FT1), the carrier of (n,FT1):]
[: the carrier of (n,FT1), the carrier of (n,FT1):] is non empty set
bool [: the carrier of (n,FT1), the carrier of (n,FT1):] is non empty set
Class ( the InternalRel of (n,FT1),FT2) is Element of bool the carrier of (n,FT1)
{FT2} is non empty set
the InternalRel of (n,FT1) .: {FT2} is set
f is set
x1 is set
[f,x1] is set
{f,x1} is non empty set
{f} is non empty set
{{f,x1},{f}} is non empty set
FTSL1 FT1 is non empty RelStr
Nbdl1 FT1 is Relation-like Seg FT1 -defined Seg FT1 -valued Element of bool [:(Seg FT1),(Seg FT1):]
[:(Seg FT1),(Seg FT1):] is non empty set
bool [:(Seg FT1),(Seg FT1):] is non empty set
RelStr(# (Seg FT1),(Nbdl1 FT1) #) is strict RelStr
the carrier of (FTSL1 FT1) is non empty set
v is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
x2 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
{x2} is non empty set
X is Element of the carrier of (FTSL1 FT1)
U_FT X is Element of bool the carrier of (FTSL1 FT1)
bool the carrier of (FTSL1 FT1) is non empty set
the InternalRel of (FTSL1 FT1) is Relation-like the carrier of (FTSL1 FT1) -defined the carrier of (FTSL1 FT1) -valued Element of bool [: the carrier of (FTSL1 FT1), the carrier of (FTSL1 FT1):]
[: the carrier of (FTSL1 FT1), the carrier of (FTSL1 FT1):] is non empty set
bool [: the carrier of (FTSL1 FT1), the carrier of (FTSL1 FT1):] is non empty set
Class ( the InternalRel of (FTSL1 FT1),X) is Element of bool the carrier of (FTSL1 FT1)
{X} is non empty set
the InternalRel of (FTSL1 FT1) .: {X} is set
((Seg FT1),(Seg FT1),(Nbdl1 FT1),v) is Element of bool (Seg FT1)
bool (Seg FT1) is non empty set
{v} is non empty set
(Nbdl1 FT1) .: {v} is set
[:{x2},((Seg FT1),(Seg FT1),(Nbdl1 FT1),v):] is set
Nbdl1 n is Relation-like Seg n -defined Seg n -valued Element of bool [:(Seg n),(Seg n):]
[:(Seg n),(Seg n):] is non empty set
bool [:(Seg n),(Seg n):] is non empty set
((Seg n),(Seg n),(Nbdl1 n),f) is Element of bool (Seg n)
bool (Seg n) is non empty set
(Nbdl1 n) .: {f} is set
[:((Seg n),(Seg n),(Nbdl1 n),f),{v}:] is set
[:{x2},((Seg FT1),(Seg FT1),(Nbdl1 FT1),v):] \/ [:((Seg n),(Seg n),(Nbdl1 n),f),{v}:] is set
n is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
FT1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
(n,FT1) is non empty strict RelStr
Seg n is non empty V47() V54(n) Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
Seg FT1 is non empty V47() V54(FT1) Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT : ( 1 <= b1 & b1 <= FT1 ) } is set
[:(Seg n),(Seg FT1):] is non empty set
(n,FT1) is Relation-like [:(Seg n),(Seg FT1):] -defined [:(Seg n),(Seg FT1):] -valued Element of bool [:[:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):]:]
[:[:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):]:] is non empty set
bool [:[:(Seg n),(Seg FT1):],[:(Seg n),(Seg FT1):]:] is non empty set
RelStr(# [:(Seg n),(Seg FT1):],(n,FT1) #) is strict RelStr
the carrier of (n,FT1) is non empty set
f is Element of the carrier of (n,FT1)
FT2 is Element of the carrier of (n,FT1)
U_FT FT2 is Element of bool the carrier of (n,FT1)
bool the carrier of (n,FT1) is non empty set
the InternalRel of (n,FT1) is Relation-like the carrier of (n,FT1) -defined the carrier of (n,FT1) -valued Element of bool [: the carrier of (n,FT1), the carrier of (n,FT1):]
[: the carrier of (n,FT1), the carrier of (n,FT1):] is non empty set
bool [: the carrier of (n,FT1), the carrier of (n,FT1):] is non empty set
Class ( the InternalRel of (n,FT1),FT2) is Element of bool the carrier of (n,FT1)
{FT2} is non empty set
the InternalRel of (n,FT1) .: {FT2} is set
U_FT f is Element of bool the carrier of (n,FT1)
Class ( the InternalRel of (n,FT1),f) is Element of bool the carrier of (n,FT1)
{f} is non empty set
the InternalRel of (n,FT1) .: {f} is set
x1 is set
x2 is set
[x1,x2] is set
{x1,x2} is non empty set
{x1} is non empty set
{{x1,x2},{x1}} is non empty set
Y is set
nv is set
[Y,nv] is set
{Y,nv} is non empty set
{Y} is non empty set
{{Y,nv},{Y}} is non empty set
FTSL1 FT1 is non empty RelStr
Nbdl1 FT1 is Relation-like Seg FT1 -defined Seg FT1 -valued Element of bool [:(Seg FT1),(Seg FT1):]
[:(Seg FT1),(Seg FT1):] is non empty set
bool [:(Seg FT1),(Seg FT1):] is non empty set
RelStr(# (Seg FT1),(Nbdl1 FT1) #) is strict RelStr
the carrier of (FTSL1 FT1) is non empty set
X is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
FTSL1 n is non empty RelStr
Nbdl1 n is Relation-like Seg n -defined Seg n -valued Element of bool [:(Seg n),(Seg n):]
[:(Seg n),(Seg n):] is non empty set
bool [:(Seg n),(Seg n):] is non empty set
RelStr(# (Seg n),(Nbdl1 n) #) is strict RelStr
the carrier of (FTSL1 n) is non empty set
v is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
x3 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
y is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
{v} is non empty set
((Seg FT1),(Seg FT1),(Nbdl1 FT1),X) is Element of bool (Seg FT1)
bool (Seg FT1) is non empty set
{X} is non empty set
(Nbdl1 FT1) .: {X} is set
[:{v},((Seg FT1),(Seg FT1),(Nbdl1 FT1),X):] is set
((Seg n),(Seg n),(Nbdl1 n),v) is Element of bool (Seg n)
bool (Seg n) is non empty set
(Nbdl1 n) .: {v} is set
[:((Seg n),(Seg n),(Nbdl1 n),v),{X}:] is set
[:{v},((Seg FT1),(Seg FT1),(Nbdl1 FT1),X):] \/ [:((Seg n),(Seg n),(Nbdl1 n),v),{X}:] is set
Class ((Nbdl1 FT1),X) is Element of bool (Seg FT1)
y1 is set
y2 is set
[y1,y2] is set
{y1,y2} is non empty set
{y1} is non empty set
{{y1,y2},{y1}} is non empty set
{y} is non empty set
pj2 is Element of the carrier of (FTSL1 FT1)
u2 is Element of the carrier of (FTSL1 FT1)
U_FT u2 is Element of bool the carrier of (FTSL1 FT1)
bool the carrier of (FTSL1 FT1) is non empty set
the InternalRel of (FTSL1 FT1) is Relation-like the carrier of (FTSL1 FT1) -defined the carrier of (FTSL1 FT1) -valued Element of bool [: the carrier of (FTSL1 FT1), the carrier of (FTSL1 FT1):]
[: the carrier of (FTSL1 FT1), the carrier of (FTSL1 FT1):] is non empty set
bool [: the carrier of (FTSL1 FT1), the carrier of (FTSL1 FT1):] is non empty set
Class ( the InternalRel of (FTSL1 FT1),u2) is Element of bool the carrier of (FTSL1 FT1)
{u2} is non empty set
the InternalRel of (FTSL1 FT1) .: {u2} is set
U_FT pj2 is Element of bool the carrier of (FTSL1 FT1)
Class ( the InternalRel of (FTSL1 FT1),pj2) is Element of bool the carrier of (FTSL1 FT1)
{pj2} is non empty set
the InternalRel of (FTSL1 FT1) .: {pj2} is set
((Seg FT1),(Seg FT1),(Nbdl1 FT1),x3) is Element of bool (Seg FT1)
{x3} is non empty set
(Nbdl1 FT1) .: {x3} is set
[:{y},((Seg FT1),(Seg FT1),(Nbdl1 FT1),x3):] is set
Class ((Nbdl1 n),v) is Element of bool (Seg n)
y1 is set
y2 is set
[y1,y2] is set
{y1,y2} is non empty set
{y1} is non empty set
{{y1,y2},{y1}} is non empty set
{x3} is non empty set
pi2 is Element of the carrier of (FTSL1 n)
v2 is Element of the carrier of (FTSL1 n)
U_FT v2 is Element of bool the carrier of (FTSL1 n)
bool the carrier of (FTSL1 n) is non empty set
the InternalRel of (FTSL1 n) is Relation-like the carrier of (FTSL1 n) -defined the carrier of (FTSL1 n) -valued Element of bool [: the carrier of (FTSL1 n), the carrier of (FTSL1 n):]
[: the carrier of (FTSL1 n), the carrier of (FTSL1 n):] is non empty set
bool [: the carrier of (FTSL1 n), the carrier of (FTSL1 n):] is non empty set
Class ( the InternalRel of (FTSL1 n),v2) is Element of bool the carrier of (FTSL1 n)
{v2} is non empty set
the InternalRel of (FTSL1 n) .: {v2} is set
U_FT pi2 is Element of bool the carrier of (FTSL1 n)
Class ( the InternalRel of (FTSL1 n),pi2) is Element of bool the carrier of (FTSL1 n)
{pi2} is non empty set
the InternalRel of (FTSL1 n) .: {pi2} is set
((Seg n),(Seg n),(Nbdl1 n),y) is Element of bool (Seg n)
{y} is non empty set
(Nbdl1 n) .: {y} is set
[:((Seg n),(Seg n),(Nbdl1 n),y),{x3}:] is set
{y} is non empty set
((Seg FT1),(Seg FT1),(Nbdl1 FT1),x3) is Element of bool (Seg FT1)
{x3} is non empty set
(Nbdl1 FT1) .: {x3} is set
[:{y},((Seg FT1),(Seg FT1),(Nbdl1 FT1),x3):] is set
((Seg n),(Seg n),(Nbdl1 n),y) is Element of bool (Seg n)
(Nbdl1 n) .: {y} is set
[:((Seg n),(Seg n),(Nbdl1 n),y),{x3}:] is set
{y} is non empty set
((Seg FT1),(Seg FT1),(Nbdl1 FT1),x3) is Element of bool (Seg FT1)
{x3} is non empty set
(Nbdl1 FT1) .: {x3} is set
[:{y},((Seg FT1),(Seg FT1),(Nbdl1 FT1),x3):] is set
((Seg n),(Seg n),(Nbdl1 n),y) is Element of bool (Seg n)
(Nbdl1 n) .: {y} is set
[:((Seg n),(Seg n),(Nbdl1 n),y),{x3}:] is set
[:{y},((Seg FT1),(Seg FT1),(Nbdl1 FT1),x3):] \/ [:((Seg n),(Seg n),(Nbdl1 n),y),{x3}:] is set
n is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
(n,1) is non empty strict RelStr
Seg n is non empty V47() V54(n) Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
Seg 1 is non empty V47() V54(1) Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
[:(Seg n),(Seg 1):] is non empty set
(n,1) is Relation-like [:(Seg n),(Seg 1):] -defined [:(Seg n),(Seg 1):] -valued Element of bool [:[:(Seg n),(Seg 1):],[:(Seg n),(Seg 1):]:]
[:[:(Seg n),(Seg 1):],[:(Seg n),(Seg 1):]:] is non empty set
bool [:[:(Seg n),(Seg 1):],[:(Seg n),(Seg 1):]:] is non empty set
RelStr(# [:(Seg n),(Seg 1):],(n,1) #) is strict RelStr
the carrier of (n,1) is non empty set
FTSL1 n is non empty RelStr
the carrier of (FTSL1 n) is non empty set
[: the carrier of (n,1), the carrier of (FTSL1 n):] is non empty set
bool [: the carrier of (n,1), the carrier of (FTSL1 n):] is non empty set
f is set
Nbdl1 n is Relation-like Seg n -defined Seg n -valued Element of bool [:(Seg n),(Seg n):]
[:(Seg n),(Seg n):] is non empty set
bool [:(Seg n),(Seg n):] is non empty set
RelStr(# (Seg n),(Nbdl1 n) #) is strict RelStr
x1 is set
x2 is set
[x1,x2] is set
{x1,x2} is non empty set
{x1} is non empty set
{{x1,x2},{x1}} is non empty set
X is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
v is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
[v,1] is set
{v,1} is non empty set
{v} is non empty set
{{v,1},{v}} is non empty set
f is Relation-like the carrier of (n,1) -defined the carrier of (FTSL1 n) -valued Function-like quasi_total Element of bool [: the carrier of (n,1), the carrier of (FTSL1 n):]
f is Relation-like the carrier of (n,1) -defined the carrier of (FTSL1 n) -valued Function-like quasi_total Element of bool [: the carrier of (n,1), the carrier of (FTSL1 n):]
Nbdl1 n is Relation-like Seg n -defined Seg n -valued Element of bool [:(Seg n),(Seg n):]
[:(Seg n),(Seg n):] is non empty set
bool [:(Seg n),(Seg n):] is non empty set
RelStr(# (Seg n),(Nbdl1 n) #) is strict RelStr
rng f is Element of bool the carrier of (FTSL1 n)
bool the carrier of (FTSL1 n) is non empty set
x1 is set
[x1,1] is set
{x1,1} is non empty set
{x1} is non empty set
{{x1,1},{x1}} is non empty set
f . [x1,1] is set
[(f . [x1,1]),1] is set
{(f . [x1,1]),1} is non empty set
{(f . [x1,1])} is non empty set
{{(f . [x1,1]),1},{(f . [x1,1])}} is non empty set
dom f is Element of bool the carrier of (n,1)
bool the carrier of (n,1) is non empty set
the InternalRel of (FTSL1 n) is Relation-like the carrier of (FTSL1 n) -defined the carrier of (FTSL1 n) -valued Element of bool [: the carrier of (FTSL1 n), the carrier of (FTSL1 n):]
[: the carrier of (FTSL1 n), the carrier of (FTSL1 n):] is non empty set
bool [: the carrier of (FTSL1 n), the carrier of (FTSL1 n):] is non empty set
x1 is Element of the carrier of (n,1)
U_FT x1 is Element of bool the carrier of (n,1)
bool the carrier of (n,1) is non empty set
the InternalRel of (n,1) is Relation-like the carrier of (n,1) -defined the carrier of (n,1) -valued Element of bool [: the carrier of (n,1), the carrier of (n,1):]
[: the carrier of (n,1), the carrier of (n,1):] is non empty set
bool [: the carrier of (n,1), the carrier of (n,1):] is non empty set
Class ( the InternalRel of (n,1),x1) is Element of bool the carrier of (n,1)
{x1} is non empty set
the InternalRel of (n,1) .: {x1} is set
f .: (U_FT x1) is Element of bool the carrier of (FTSL1 n)
f . x1 is Element of the carrier of (FTSL1 n)
( the carrier of (FTSL1 n), the carrier of (FTSL1 n), the InternalRel of (FTSL1 n),(f . x1)) is Element of bool the carrier of (FTSL1 n)
{(f . x1)} is non empty set
the InternalRel of (FTSL1 n) .: {(f . x1)} is set
x2 is set
v is set
[x2,v] is set
{x2,v} is non empty set
{x2} is non empty set
{{x2,v},{x2}} is non empty set
X is set
dom f is Element of bool the carrier of (n,1)
([:(Seg n),(Seg 1):],[:(Seg n),(Seg 1):],(n,1),x1) is Relation-like Seg n -defined Seg 1 -valued Element of bool [:(Seg n),(Seg 1):]
bool [:(Seg n),(Seg 1):] is non empty set
(n,1) .: {x1} is set
Y is set
f . Y is set
nv is set
y is set
[nv,y] is set
{nv,y} is non empty set
{nv} is non empty set
{{nv,y},{nv}} is non empty set
[(f . Y),1] is set
{(f . Y),1} is non empty set
{(f . Y)} is non empty set
{{(f . Y),1},{(f . Y)}} is non empty set
Nbdl1 1 is Relation-like Seg 1 -defined Seg 1 -valued Element of bool [:(Seg 1),(Seg 1):]
[:(Seg 1),(Seg 1):] is non empty set
bool [:(Seg 1),(Seg 1):] is non empty set
((Seg 1),(Seg 1),(Nbdl1 1),v) is Element of bool (Seg 1)
bool (Seg 1) is non empty set
{v} is non empty set
(Nbdl1 1) .: {v} is set
[:{x2},((Seg 1),(Seg 1),(Nbdl1 1),v):] is set
((Seg n),(Seg n),(Nbdl1 n),x2) is Element of bool (Seg n)
bool (Seg n) is non empty set
(Nbdl1 n) .: {x2} is set
[:((Seg n),(Seg n),(Nbdl1 n),x2),{v}:] is set
[:{x2},((Seg 1),(Seg 1),(Nbdl1 1),v):] \/ [:((Seg n),(Seg n),(Nbdl1 n),x2),{v}:] is set
x3 is Element of the carrier of (FTSL1 n)
U_FT x3 is Element of bool the carrier of (FTSL1 n)
Class ( the InternalRel of (FTSL1 n),x3) is Element of bool the carrier of (FTSL1 n)
{x3} is non empty set
the InternalRel of (FTSL1 n) .: {x3} is set
Class ((Nbdl1 n),x2) is Element of bool (Seg n)
Class ((Nbdl1 n),x2) is Element of bool (Seg n)
Class ((Nbdl1 n),x2) is Element of bool (Seg n)
Class ((Nbdl1 n),x2) is Element of bool (Seg n)
[(f . x1),1] is set
{(f . x1),1} is non empty set
{{(f . x1),1},{(f . x1)}} is non empty set
((Seg n),(Seg n),(Nbdl1 n),x2) is Element of bool (Seg n)
bool (Seg n) is non empty set
(Nbdl1 n) .: {x2} is set
Nbdl1 1 is Relation-like Seg 1 -defined Seg 1 -valued Element of bool [:(Seg 1),(Seg 1):]
[:(Seg 1),(Seg 1):] is non empty set
bool [:(Seg 1),(Seg 1):] is non empty set
((Seg 1),(Seg 1),(Nbdl1 1),v) is Element of bool (Seg 1)
bool (Seg 1) is non empty set
{v} is non empty set
(Nbdl1 1) .: {v} is set
y is set
((Seg n),(Seg n),(Nbdl1 n),(f . x1)) is Element of bool (Seg n)
(Nbdl1 n) .: {(f . x1)} is set
dom f is Element of bool the carrier of (n,1)
x3 is set
f . x3 is set
[(f . x1),1] is set
{(f . x1),1} is non empty set
{{(f . x1),1},{(f . x1)}} is non empty set
([:(Seg n),(Seg 1):],[:(Seg n),(Seg 1):],(n,1),x1) is Relation-like Seg n -defined Seg 1 -valued Element of bool [:(Seg n),(Seg 1):]
bool [:(Seg n),(Seg 1):] is non empty set
(n,1) .: {x1} is set
[:{x2},((Seg 1),(Seg 1),(Nbdl1 1),v):] is set
[:((Seg n),(Seg n),(Nbdl1 n),x2),{v}:] is set
[:{x2},((Seg 1),(Seg 1),(Nbdl1 1),v):] \/ [:((Seg n),(Seg n),(Nbdl1 n),x2),{v}:] is set
nv is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
nv -' 1 is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
max ((nv -' 1),1) is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
nv + 1 is non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer Element of NAT
min ((nv + 1),1) is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
{nv,(max ((nv -' 1),1)),(min ((nv + 1),1))} is non empty set
max (0,1) is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
min (2,1) is V4() V5() V6() V10() complex V12() ext-real non negative integer Element of NAT
{1,(max (0,1)),(min (2,1))} is non empty set
{1,1,(min (2,1))} is non empty set
{1,(min (2,1))} is non empty set
{1,1} is non empty set
{1} is non empty set
[(f . x3),1] is set
{(f . x3),1} is non empty set
{(f . x3)} is non empty set
{{(f . x3),1},{(f . x3)}} is non empty set
[:((Seg n),(Seg n),(Nbdl1 n),x2),((Seg 1),(Seg 1),(Nbdl1 1),v):] is set
[:((Seg n),(Seg n),(Nbdl1 n),x2),{v}:] \/ [:{x2},((Seg 1),(Seg 1),(Nbdl1 1),v):] is set
dom f is Element of bool the carrier of (n,1)
bool the carrier of (n,1) is non empty set
x1 is set
x2 is set
f . x1 is set
f . x2 is set
[(f . x1),1] is set
{(f . x1),1} is non empty set
{(f . x1)} is non empty set
{{(f . x1),1},{(f . x1)}} is non empty set