:: FINTOPO5 semantic presentation

REAL is set

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

bool REAL is non empty set

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

bool NAT is non empty set

bool NAT is non empty set

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

{ b

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

{ b

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

{ b

( b

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

{ b

( b

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

{ b

( b

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

{ b

( b

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

{ b

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

{ b

( b

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

{ b

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)

{ b

( b

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)

{ b

( b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

Seg FT1 is non empty V47() V54(FT1) Element of bool NAT

{ b

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

{ b

Seg FT1 is non empty V47() V54(FT1) Element of bool NAT

{ b

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

{ b

Seg FT1 is non empty V47() V54(FT1) Element of bool NAT

{ b

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

(n,FT1) is Relation-like [:(Seg n),(