:: NFCONT_2 semantic presentation

REAL is non empty V47() V48() V49() V53() V54() set

NAT is non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() Element of K6(REAL)

K6(REAL) is set

COMPLEX is non empty V47() V53() V54() set

RAT is non empty V47() V48() V49() V50() V53() V54() set

INT is non empty V47() V48() V49() V50() V51() V53() V54() set

NAT is non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() set

K6(NAT) is set

K6(NAT) is set

K7(COMPLEX,COMPLEX) is complex-valued set

K6(K7(COMPLEX,COMPLEX)) is set

K7(COMPLEX,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(COMPLEX,REAL)) is set

K7(NAT,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(NAT,REAL)) is set

K380() is non empty set

K7(K380(),K380()) is set

K7(K7(K380(),K380()),K380()) is set

K6(K7(K7(K380(),K380()),K380())) is set

K7(REAL,K380()) is set

K7(K7(REAL,K380()),K380()) is set

K6(K7(K7(REAL,K380()),K380())) is set

K386() is L12()

the carrier of K386() is set

K6( the carrier of K386()) is set

K390() is Element of K6( the carrier of K386())

K7(K390(),K390()) is set

K7(K7(K390(),K390()),REAL) is complex-valued ext-real-valued real-valued set

K6(K7(K7(K390(),K390()),REAL)) is set

the_set_of_l1RealSequences is Element of K6( the carrier of K386())

K7(the_set_of_l1RealSequences,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(the_set_of_l1RealSequences,REAL)) is set

{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional V47() V48() V49() V50() V51() V52() V53() set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT

0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT

- 1 is V11() real ext-real non positive Element of REAL

2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT

K7(NAT,NAT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

K6(K7(NAT,NAT)) is set

f is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR

the carrier of f is non empty set

n0 is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR

the carrier of n0 is non empty set

K7( the carrier of f, the carrier of n0) is set

K6(K7( the carrier of f, the carrier of n0)) is set

f is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR

the carrier of f is non empty set

K7( the carrier of f,REAL) is complex-valued ext-real-valued real-valued set

K6(K7( the carrier of f,REAL)) is set

X is set

f is set

n0 is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR

the carrier of n0 is non empty set

xp is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR

the carrier of xp is non empty set

K7( the carrier of n0, the carrier of xp) is set

K6(K7( the carrier of n0, the carrier of xp)) is set

x is Relation-like the carrier of n0 -defined the carrier of xp -valued Function-like Element of K6(K7( the carrier of n0, the carrier of xp))

dom x is Element of K6( the carrier of n0)

K6( the carrier of n0) is set

n is V11() real ext-real Element of REAL

xp is V11() real ext-real Element of REAL

x is Element of the carrier of n0

x /. x is Element of the carrier of xp

e is Element of the carrier of n0

x - e is Element of the carrier of n0

- e is Element of the carrier of n0

K342(n0,x,(- e)) is Element of the carrier of n0

||.(x - e).|| is V11() real ext-real non negative Element of REAL

x /. e is Element of the carrier of xp

(x /. x) - (x /. e) is Element of the carrier of xp

- (x /. e) is Element of the carrier of xp

K342(xp,(x /. x),(- (x /. e))) is Element of the carrier of xp

||.((x /. x) - (x /. e)).|| is V11() real ext-real non negative Element of REAL

X is set

f is set

X /\ f is set

n0 is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR

the carrier of n0 is non empty set

xp is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR

the carrier of xp is non empty set

K7( the carrier of n0, the carrier of xp) is set

K6(K7( the carrier of n0, the carrier of xp)) is set

x is Relation-like the carrier of n0 -defined the carrier of xp -valued Function-like Element of K6(K7( the carrier of n0, the carrier of xp))

n is Relation-like the carrier of n0 -defined the carrier of xp -valued Function-like Element of K6(K7( the carrier of n0, the carrier of xp))

x + n is Relation-like the carrier of n0 -defined the carrier of xp -valued Function-like Element of K6(K7( the carrier of n0, the carrier of xp))

dom n is Element of K6( the carrier of n0)

K6( the carrier of n0) is set

dom x is Element of K6( the carrier of n0)

(dom x) /\ (dom n) is Element of K6( the carrier of n0)

dom (x + n) is Element of K6( the carrier of n0)

xp is V11() real ext-real Element of REAL

xp / 2 is V11() real ext-real Element of REAL

x is V11() real ext-real Element of REAL

e is V11() real ext-real Element of REAL

min (x,e) is V11() real ext-real Element of REAL

n is V11() real ext-real Element of REAL

l is Element of the carrier of n0

(x + n) /. l is Element of the carrier of xp

k1 is Element of the carrier of n0

l - k1 is Element of the carrier of n0

- k1 is Element of the carrier of n0

K342(n0,l,(- k1)) is Element of the carrier of n0

||.(l - k1).|| is V11() real ext-real non negative Element of REAL

(x + n) /. k1 is Element of the carrier of xp

((x + n) /. l) - ((x + n) /. k1) is Element of the carrier of xp

- ((x + n) /. k1) is Element of the carrier of xp

K342(xp,((x + n) /. l),(- ((x + n) /. k1))) is Element of the carrier of xp

||.(((x + n) /. l) - ((x + n) /. k1)).|| is V11() real ext-real non negative Element of REAL

n /. l is Element of the carrier of xp

n /. k1 is Element of the carrier of xp

(n /. l) - (n /. k1) is Element of the carrier of xp

- (n /. k1) is Element of the carrier of xp

K342(xp,(n /. l),(- (n /. k1))) is Element of the carrier of xp

||.((n /. l) - (n /. k1)).|| is V11() real ext-real non negative Element of REAL

x /. l is Element of the carrier of xp

x /. k1 is Element of the carrier of xp

(x /. l) - (x /. k1) is Element of the carrier of xp

- (x /. k1) is Element of the carrier of xp

K342(xp,(x /. l),(- (x /. k1))) is Element of the carrier of xp

||.((x /. l) - (x /. k1)).|| is V11() real ext-real non negative Element of REAL

(xp / 2) + (xp / 2) is V11() real ext-real Element of REAL

||.((x /. l) - (x /. k1)).|| + ||.((n /. l) - (n /. k1)).|| is V11() real ext-real non negative Element of REAL

((x /. l) - (x /. k1)) + ((n /. l) - (n /. k1)) is Element of the carrier of xp

||.(((x /. l) - (x /. k1)) + ((n /. l) - (n /. k1))).|| is V11() real ext-real non negative Element of REAL

(x /. l) + (n /. l) is Element of the carrier of xp

((x /. l) + (n /. l)) - ((x + n) /. k1) is Element of the carrier of xp

K342(xp,((x /. l) + (n /. l)),(- ((x + n) /. k1))) is Element of the carrier of xp

||.(((x /. l) + (n /. l)) - ((x + n) /. k1)).|| is V11() real ext-real non negative Element of REAL

(x /. k1) + (n /. k1) is Element of the carrier of xp

((x /. l) + (n /. l)) - ((x /. k1) + (n /. k1)) is Element of the carrier of xp

- ((x /. k1) + (n /. k1)) is Element of the carrier of xp

K342(xp,((x /. l) + (n /. l)),(- ((x /. k1) + (n /. k1)))) is Element of the carrier of xp

||.(((x /. l) + (n /. l)) - ((x /. k1) + (n /. k1))).|| is V11() real ext-real non negative Element of REAL

(n /. l) - ((x /. k1) + (n /. k1)) is Element of the carrier of xp

K342(xp,(n /. l),(- ((x /. k1) + (n /. k1)))) is Element of the carrier of xp

(x /. l) + ((n /. l) - ((x /. k1) + (n /. k1))) is Element of the carrier of xp

||.((x /. l) + ((n /. l) - ((x /. k1) + (n /. k1)))).|| is V11() real ext-real non negative Element of REAL

(n /. l) - (x /. k1) is Element of the carrier of xp

K342(xp,(n /. l),(- (x /. k1))) is Element of the carrier of xp

((n /. l) - (x /. k1)) - (n /. k1) is Element of the carrier of xp

K342(xp,((n /. l) - (x /. k1)),(- (n /. k1))) is Element of the carrier of xp

(x /. l) + (((n /. l) - (x /. k1)) - (n /. k1)) is Element of the carrier of xp

||.((x /. l) + (((n /. l) - (x /. k1)) - (n /. k1))).|| is V11() real ext-real non negative Element of REAL

(- (x /. k1)) + (n /. l) is Element of the carrier of xp

((- (x /. k1)) + (n /. l)) - (n /. k1) is Element of the carrier of xp

K342(xp,((- (x /. k1)) + (n /. l)),(- (n /. k1))) is Element of the carrier of xp

(x /. l) + (((- (x /. k1)) + (n /. l)) - (n /. k1)) is Element of the carrier of xp

||.((x /. l) + (((- (x /. k1)) + (n /. l)) - (n /. k1))).|| is V11() real ext-real non negative Element of REAL

(- (x /. k1)) + ((n /. l) - (n /. k1)) is Element of the carrier of xp

(x /. l) + ((- (x /. k1)) + ((n /. l) - (n /. k1))) is Element of the carrier of xp

||.((x /. l) + ((- (x /. k1)) + ((n /. l) - (n /. k1)))).|| is V11() real ext-real non negative Element of REAL

X is set

f is set

X /\ f is set

n0 is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR

the carrier of n0 is non empty set

xp is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR

the carrier of xp is non empty set

K7( the carrier of n0, the carrier of xp) is set

K6(K7( the carrier of n0, the carrier of xp)) is set

x is Relation-like the carrier of n0 -defined the carrier of xp -valued Function-like Element of K6(K7( the carrier of n0, the carrier of xp))

n is Relation-like the carrier of n0 -defined the carrier of xp -valued Function-like Element of K6(K7( the carrier of n0, the carrier of xp))

x - n is Relation-like the carrier of n0 -defined the carrier of xp -valued Function-like Element of K6(K7( the carrier of n0, the carrier of xp))

dom n is Element of K6( the carrier of n0)

K6( the carrier of n0) is set

dom x is Element of K6( the carrier of n0)

(dom x) /\ (dom n) is Element of K6( the carrier of n0)

dom (x - n) is Element of K6( the carrier of n0)

xp is V11() real ext-real Element of REAL

xp / 2 is V11() real ext-real Element of REAL

x is V11() real ext-real Element of REAL

e is V11() real ext-real Element of REAL

min (x,e) is V11() real ext-real Element of REAL

n is V11() real ext-real Element of REAL

l is Element of the carrier of n0

(x - n) /. l is Element of the carrier of xp

k1 is Element of the carrier of n0

l - k1 is Element of the carrier of n0

- k1 is Element of the carrier of n0

K342(n0,l,(- k1)) is Element of the carrier of n0

||.(l - k1).|| is V11() real ext-real non negative Element of REAL

(x - n) /. k1 is Element of the carrier of xp

((x - n) /. l) - ((x - n) /. k1) is Element of the carrier of xp

- ((x - n) /. k1) is Element of the carrier of xp

K342(xp,((x - n) /. l),(- ((x - n) /. k1))) is Element of the carrier of xp

||.(((x - n) /. l) - ((x - n) /. k1)).|| is V11() real ext-real non negative Element of REAL

n /. l is Element of the carrier of xp

n /. k1 is Element of the carrier of xp

(n /. l) - (n /. k1) is Element of the carrier of xp

- (n /. k1) is Element of the carrier of xp

K342(xp,(n /. l),(- (n /. k1))) is Element of the carrier of xp

||.((n /. l) - (n /. k1)).|| is V11() real ext-real non negative Element of REAL

x /. l is Element of the carrier of xp

x /. k1 is Element of the carrier of xp

(x /. l) - (x /. k1) is Element of the carrier of xp

- (x /. k1) is Element of the carrier of xp

K342(xp,(x /. l),(- (x /. k1))) is Element of the carrier of xp

||.((x /. l) - (x /. k1)).|| is V11() real ext-real non negative Element of REAL

(xp / 2) + (xp / 2) is V11() real ext-real Element of REAL

||.((x /. l) - (x /. k1)).|| + ||.((n /. l) - (n /. k1)).|| is V11() real ext-real non negative Element of REAL

((x /. l) - (x /. k1)) - ((n /. l) - (n /. k1)) is Element of the carrier of xp

- ((n /. l) - (n /. k1)) is Element of the carrier of xp

K342(xp,((x /. l) - (x /. k1)),(- ((n /. l) - (n /. k1)))) is Element of the carrier of xp

||.(((x /. l) - (x /. k1)) - ((n /. l) - (n /. k1))).|| is V11() real ext-real non negative Element of REAL

(x /. l) - (n /. l) is Element of the carrier of xp

- (n /. l) is Element of the carrier of xp

K342(xp,(x /. l),(- (n /. l))) is Element of the carrier of xp

((x /. l) - (n /. l)) - ((x - n) /. k1) is Element of the carrier of xp

K342(xp,((x /. l) - (n /. l)),(- ((x - n) /. k1))) is Element of the carrier of xp

||.(((x /. l) - (n /. l)) - ((x - n) /. k1)).|| is V11() real ext-real non negative Element of REAL

(x /. k1) - (n /. k1) is Element of the carrier of xp

K342(xp,(x /. k1),(- (n /. k1))) is Element of the carrier of xp

((x /. l) - (n /. l)) - ((x /. k1) - (n /. k1)) is Element of the carrier of xp

- ((x /. k1) - (n /. k1)) is Element of the carrier of xp

K342(xp,((x /. l) - (n /. l)),(- ((x /. k1) - (n /. k1)))) is Element of the carrier of xp

||.(((x /. l) - (n /. l)) - ((x /. k1) - (n /. k1))).|| is V11() real ext-real non negative Element of REAL

(n /. l) + ((x /. k1) - (n /. k1)) is Element of the carrier of xp

(x /. l) - ((n /. l) + ((x /. k1) - (n /. k1))) is Element of the carrier of xp

- ((n /. l) + ((x /. k1) - (n /. k1))) is Element of the carrier of xp

K342(xp,(x /. l),(- ((n /. l) + ((x /. k1) - (n /. k1))))) is Element of the carrier of xp

||.((x /. l) - ((n /. l) + ((x /. k1) - (n /. k1)))).|| is V11() real ext-real non negative Element of REAL

(x /. k1) + (n /. l) is Element of the carrier of xp

((x /. k1) + (n /. l)) - (n /. k1) is Element of the carrier of xp

K342(xp,((x /. k1) + (n /. l)),(- (n /. k1))) is Element of the carrier of xp

(x /. l) - (((x /. k1) + (n /. l)) - (n /. k1)) is Element of the carrier of xp

- (((x /. k1) + (n /. l)) - (n /. k1)) is Element of the carrier of xp

K342(xp,(x /. l),(- (((x /. k1) + (n /. l)) - (n /. k1)))) is Element of the carrier of xp

||.((x /. l) - (((x /. k1) + (n /. l)) - (n /. k1))).|| is V11() real ext-real non negative Element of REAL

(x /. k1) + ((n /. l) - (n /. k1)) is Element of the carrier of xp

(x /. l) - ((x /. k1) + ((n /. l) - (n /. k1))) is Element of the carrier of xp

- ((x /. k1) + ((n /. l) - (n /. k1))) is Element of the carrier of xp

K342(xp,(x /. l),(- ((x /. k1) + ((n /. l) - (n /. k1))))) is Element of the carrier of xp

||.((x /. l) - ((x /. k1) + ((n /. l) - (n /. k1)))).|| is V11() real ext-real non negative Element of REAL

X is set

f is V11() real ext-real Element of REAL

n0 is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR

the carrier of n0 is non empty set

xp is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR

the carrier of xp is non empty set

K7( the carrier of n0, the carrier of xp) is set

K6(K7( the carrier of n0, the carrier of xp)) is set

x is Relation-like the carrier of n0 -defined the carrier of xp -valued Function-like Element of K6(K7( the carrier of n0, the carrier of xp))

f (#) x is Relation-like the carrier of n0 -defined the carrier of xp -valued Function-like Element of K6(K7( the carrier of n0, the carrier of xp))

dom x is Element of K6( the carrier of n0)

K6( the carrier of n0) is set

dom (f (#) x) is Element of K6( the carrier of n0)

n is V11() real ext-real Element of REAL

xp is V11() real ext-real Element of REAL

x is V11() real ext-real Element of REAL

e is Element of the carrier of n0

n is Element of the carrier of n0

e - n is Element of the carrier of n0

- n is Element of the carrier of n0

K342(n0,e,(- n)) is Element of the carrier of n0

||.(e - n).|| is V11() real ext-real non negative Element of REAL

(f (#) x) /. e is Element of the carrier of xp

(f (#) x) /. n is Element of the carrier of xp

((f (#) x) /. e) - ((f (#) x) /. n) is Element of the carrier of xp

- ((f (#) x) /. n) is Element of the carrier of xp

K342(xp,((f (#) x) /. e),(- ((f (#) x) /. n))) is Element of the carrier of xp

||.(((f (#) x) /. e) - ((f (#) x) /. n)).|| is V11() real ext-real non negative Element of REAL

x /. e is Element of the carrier of xp

f * (x /. e) is Element of the carrier of xp

the U7 of xp is Relation-like K7(REAL, the carrier of xp) -defined the carrier of xp -valued Function-like total quasi_total Element of K6(K7(K7(REAL, the carrier of xp), the carrier of xp))

K7(REAL, the carrier of xp) is set

K7(K7(REAL, the carrier of xp), the carrier of xp) is set

K6(K7(K7(REAL, the carrier of xp), the carrier of xp)) is set

K397( the U7 of xp,f,(x /. e)) is set

(f * (x /. e)) - ((f (#) x) /. n) is Element of the carrier of xp

K342(xp,(f * (x /. e)),(- ((f (#) x) /. n))) is Element of the carrier of xp

||.((f * (x /. e)) - ((f (#) x) /. n)).|| is V11() real ext-real non negative Element of REAL

0. xp is V99(xp) Element of the carrier of xp

(0. xp) - ((f (#) x) /. n) is Element of the carrier of xp

K342(xp,(0. xp),(- ((f (#) x) /. n))) is Element of the carrier of xp

||.((0. xp) - ((f (#) x) /. n)).|| is V11() real ext-real non negative Element of REAL

x /. n is Element of the carrier of xp

f * (x /. n) is Element of the carrier of xp

K397( the U7 of xp,f,(x /. n)) is set

(0. xp) - (f * (x /. n)) is Element of the carrier of xp

- (f * (x /. n)) is Element of the carrier of xp

K342(xp,(0. xp),(- (f * (x /. n)))) is Element of the carrier of xp

||.((0. xp) - (f * (x /. n))).|| is V11() real ext-real non negative Element of REAL

(0. xp) - (0. xp) is Element of the carrier of xp

- (0. xp) is Element of the carrier of xp

K342(xp,(0. xp),(- (0. xp))) is Element of the carrier of xp

||.((0. xp) - (0. xp)).|| is V11() real ext-real non negative Element of REAL

||.(0. xp).|| is V11() real ext-real non negative Element of REAL

abs f is V11() real ext-real Element of REAL

n is V11() real ext-real Element of REAL

n / (abs f) is V11() real ext-real Element of REAL

xp is V11() real ext-real Element of REAL

x is V11() real ext-real Element of REAL

e is Element of the carrier of n0

n is Element of the carrier of n0

e - n is Element of the carrier of n0

- n is Element of the carrier of n0

K342(n0,e,(- n)) is Element of the carrier of n0

||.(e - n).|| is V11() real ext-real non negative Element of REAL

(f (#) x) /. e is Element of the carrier of xp

(f (#) x) /. n is Element of the carrier of xp

((f (#) x) /. e) - ((f (#) x) /. n) is Element of the carrier of xp

- ((f (#) x) /. n) is Element of the carrier of xp

K342(xp,((f (#) x) /. e),(- ((f (#) x) /. n))) is Element of the carrier of xp

||.(((f (#) x) /. e) - ((f (#) x) /. n)).|| is V11() real ext-real non negative Element of REAL

x /. e is Element of the carrier of xp

f * (x /. e) is Element of the carrier of xp

the U7 of xp is Relation-like K7(REAL, the carrier of xp) -defined the carrier of xp -valued Function-like total quasi_total Element of K6(K7(K7(REAL, the carrier of xp), the carrier of xp))

K7(REAL, the carrier of xp) is set

K7(K7(REAL, the carrier of xp), the carrier of xp) is set

K6(K7(K7(REAL, the carrier of xp), the carrier of xp)) is set

K397( the U7 of xp,f,(x /. e)) is set

(f * (x /. e)) - ((f (#) x) /. n) is Element of the carrier of xp

K342(xp,(f * (x /. e)),(- ((f (#) x) /. n))) is Element of the carrier of xp

||.((f * (x /. e)) - ((f (#) x) /. n)).|| is V11() real ext-real non negative Element of REAL

x /. n is Element of the carrier of xp

f * (x /. n) is Element of the carrier of xp

K397( the U7 of xp,f,(x /. n)) is set

(f * (x /. e)) - (f * (x /. n)) is Element of the carrier of xp

- (f * (x /. n)) is Element of the carrier of xp

K342(xp,(f * (x /. e)),(- (f * (x /. n)))) is Element of the carrier of xp

||.((f * (x /. e)) - (f * (x /. n))).|| is V11() real ext-real non negative Element of REAL

(x /. e) - (x /. n) is Element of the carrier of xp

- (x /. n) is Element of the carrier of xp

K342(xp,(x /. e),(- (x /. n))) is Element of the carrier of xp

f * ((x /. e) - (x /. n)) is Element of the carrier of xp

K397( the U7 of xp,f,((x /. e) - (x /. n))) is set

||.(f * ((x /. e) - (x /. n))).|| is V11() real ext-real non negative Element of REAL

||.((x /. e) - (x /. n)).|| is V11() real ext-real non negative Element of REAL

(abs f) * ||.((x /. e) - (x /. n)).|| is V11() real ext-real Element of REAL

(n / (abs f)) * (abs f) is V11() real ext-real Element of REAL

n is V11() real ext-real Element of REAL

X is set

f is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR

the carrier of f is non empty set

n0 is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR

the carrier of n0 is non empty set

K7( the carrier of f, the carrier of n0) is set

K6(K7( the carrier of f, the carrier of n0)) is set

xp is Relation-like the carrier of f -defined the carrier of n0 -valued Function-like Element of K6(K7( the carrier of f, the carrier of n0))

- xp is Relation-like the carrier of f -defined the carrier of n0 -valued Function-like Element of K6(K7( the carrier of f, the carrier of n0))

(- 1) (#) xp is Relation-like the carrier of f -defined the carrier of n0 -valued Function-like Element of K6(K7( the carrier of f, the carrier of n0))

X is set

f is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR

the carrier of f is non empty set

n0 is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR

the carrier of n0 is non empty set

K7( the carrier of f, the carrier of n0) is set

K6(K7( the carrier of f, the carrier of n0)) is set

xp is Relation-like the carrier of f -defined the carrier of n0 -valued Function-like Element of K6(K7( the carrier of f, the carrier of n0))

||.xp.|| is Relation-like the carrier of f -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of f,REAL))

K7( the carrier of f,REAL) is complex-valued ext-real-valued real-valued set

K6(K7( the carrier of f,REAL)) is set

dom xp is Element of K6( the carrier of f)

K6( the carrier of f) is set

dom ||.xp.|| is Element of K6( the carrier of f)

x is V11() real ext-real Element of REAL

n is V11() real ext-real Element of REAL

xp is Element of the carrier of f

||.xp.|| /. xp is V11() real ext-real Element of REAL

x is Element of the carrier of f

xp - x is Element of the carrier of f

- x is Element of the carrier of f

K342(f,xp,(- x)) is Element of the carrier of f

||.(xp - x).|| is V11() real ext-real non negative Element of REAL

||.xp.|| /. x is V11() real ext-real Element of REAL

(||.xp.|| /. xp) - (||.xp.|| /. x) is V11() real ext-real Element of REAL

abs ((||.xp.|| /. xp) - (||.xp.|| /. x)) is V11() real ext-real Element of REAL

||.xp.|| . xp is V11() real ext-real Element of REAL

(||.xp.|| . xp) - (||.xp.|| /. x) is V11() real ext-real Element of REAL

abs ((||.xp.|| . xp) - (||.xp.|| /. x)) is V11() real ext-real Element of REAL

||.xp.|| . x is V11() real ext-real Element of REAL

(||.xp.|| . xp) - (||.xp.|| . x) is V11() real ext-real Element of REAL

abs ((||.xp.|| . xp) - (||.xp.|| . x)) is V11() real ext-real Element of REAL

xp /. xp is Element of the carrier of n0

||.(xp /. xp).|| is V11() real ext-real non negative Element of REAL

||.(xp /. xp).|| - (||.xp.|| . x) is V11() real ext-real Element of REAL

abs (||.(xp /. xp).|| - (||.xp.|| . x)) is V11() real ext-real Element of REAL

xp /. x is Element of the carrier of n0

||.(xp /. x).|| is V11() real ext-real non negative Element of REAL

||.(xp /. xp).|| - ||.(xp /. x).|| is V11() real ext-real Element of REAL

abs (||.(xp /. xp).|| - ||.(xp /. x).||) is V11() real ext-real Element of REAL

(xp /. xp) - (xp /. x) is Element of the carrier of n0

- (xp /. x) is Element of the carrier of n0

K342(n0,(xp /. xp),(- (xp /. x))) is Element of the carrier of n0

||.((xp /. xp) - (xp /. x)).|| is V11() real ext-real non negative Element of REAL

X is set

f is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR

the carrier of f is non empty set

n0 is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR

the carrier of n0 is non empty set

K7( the carrier of f, the carrier of n0) is set

K6(K7( the carrier of f, the carrier of n0)) is set

xp is Relation-like the carrier of f -defined the carrier of n0 -valued Function-like Element of K6(K7( the carrier of f, the carrier of n0))

x is Element of the carrier of f

n is V11() real ext-real Element of REAL

xp is V11() real ext-real Element of REAL

x is V11() real ext-real Element of REAL

e is Element of the carrier of f

e - x is Element of the carrier of f

- x is Element of the carrier of f

K342(f,e,(- x)) is Element of the carrier of f

||.(e - x).|| is V11() real ext-real non negative Element of REAL

xp /. e is Element of the carrier of n0

xp /. x is Element of the carrier of n0

(xp /. e) - (xp /. x) is Element of the carrier of n0

- (xp /. x) is Element of the carrier of n0

K342(n0,(xp /. e),(- (xp /. x))) is Element of the carrier of n0

||.((xp /. e) - (xp /. x)).|| is V11() real ext-real non negative Element of REAL

dom xp is Element of K6( the carrier of f)

K6( the carrier of f) is set

X is set

f is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR

the carrier of f is non empty set

K7( the carrier of f,REAL) is complex-valued ext-real-valued real-valued set

K6(K7( the carrier of f,REAL)) is set

n0 is Relation-like the carrier of f -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of f,REAL))

xp is Element of the carrier of f

x is V11() real ext-real Element of REAL

n is V11() real ext-real Element of REAL

xp is V11() real ext-real Element of REAL

x is Element of the carrier of f

x - xp is Element of the carrier of f

- xp is Element of the carrier of f

K342(f,x,(- xp)) is Element of the carrier of f

||.(x - xp).|| is V11() real ext-real non negative Element of REAL

n0 /. x is V11() real ext-real Element of REAL

n0 /. xp is V11() real ext-real Element of REAL

(n0 /. x) - (n0 /. xp) is V11() real ext-real Element of REAL

abs ((n0 /. x) - (n0 /. xp)) is V11() real ext-real Element of REAL

dom n0 is Element of K6( the carrier of f)

K6( the carrier of f) is set

X is set

f is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR

the carrier of f is non empty set

n0 is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR

the carrier of n0 is non empty set

K7( the carrier of f, the carrier of n0) is set

K6(K7( the carrier of f, the carrier of n0)) is set

xp is Relation-like the carrier of f -defined the carrier of n0 -valued Function-like Element of K6(K7( the carrier of f, the carrier of n0))

dom xp is Element of K6( the carrier of f)

K6( the carrier of f) is set

x is V11() real ext-real Element of REAL

n is V11() real ext-real Element of REAL

n / x is V11() real ext-real Element of REAL

xp is V11() real ext-real Element of REAL

x is Element of the carrier of f

xp /. x is Element of the carrier of n0

e is Element of the carrier of f

x - e is Element of the carrier of f

- e is Element of the carrier of f

K342(f,x,(- e)) is Element of the carrier of f

||.(x - e).|| is V11() real ext-real non negative Element of REAL

xp /. e is Element of the carrier of n0

(xp /. x) - (xp /. e) is Element of the carrier of n0

- (xp /. e) is Element of the carrier of n0

K342(n0,(xp /. x),(- (xp /. e))) is Element of the carrier of n0

||.((xp /. x) - (xp /. e)).|| is V11() real ext-real non negative Element of REAL

xp * x is V11() real ext-real Element of REAL

x * ||.(x - e).|| is V11() real ext-real Element of REAL

(n / x) * x is V11() real ext-real Element of REAL

X is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR

the carrier of X is non empty set

f is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR

the carrier of f is non empty set

K7( the carrier of f, the carrier of X) is set

K6(K7( the carrier of f, the carrier of X)) is set

K6( the carrier of f) is set

n0 is Relation-like the carrier of f -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of f, the carrier of X))

xp is Element of K6( the carrier of f)

dom n0 is Element of K6( the carrier of f)

x is V11() real ext-real Element of REAL

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT

n + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT

1 / (n + 1) is V11() real ext-real Element of REAL

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT

n + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT

1 / (n + 1) is V11() real ext-real Element of REAL

xp is Element of the carrier of f

n0 /. xp is Element of the carrier of X

x is Element of the carrier of f

n0 /. x is Element of the carrier of X

e is Element of the carrier of f

xp - e is Element of the carrier of f

- e is Element of the carrier of f

K342(f,xp,(- e)) is Element of the carrier of f

||.(xp - e).|| is V11() real ext-real non negative Element of REAL

n0 /. e is Element of the carrier of X

(n0 /. xp) - (n0 /. e) is Element of the carrier of X

- (n0 /. e) is Element of the carrier of X

K342(X,(n0 /. xp),(- (n0 /. e))) is Element of the carrier of X

||.((n0 /. xp) - (n0 /. e)).|| is V11() real ext-real non negative Element of REAL

K7(NAT, the carrier of f) is set

K6(K7(NAT, the carrier of f)) is set

n is non empty Relation-like NAT -defined the carrier of f -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of f))

xp is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT

xp + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT

1 / (xp + 1) is V11() real ext-real Element of REAL

n . xp is Element of the carrier of f

n0 /. (n . xp) is Element of the carrier of X

xp is non empty Relation-like NAT -defined the carrier of f -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of f))

x is set

rng n is Element of K6( the carrier of f)

e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT

n . e is Element of the carrier of f

x is non empty Relation-like NAT -defined the carrier of f -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of f))

lim x is Element of the carrier of f

e is non empty Relation-like NAT -defined NAT -valued Function-like total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K6(K7(NAT,NAT))

n * e is non empty Relation-like NAT -defined the carrier of f -valued Function-like total quasi_total subsequence of n

n - xp is non empty Relation-like NAT -defined the carrier of f -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of f))

(n - xp) * e is non empty Relation-like NAT -defined the carrier of f -valued Function-like total quasi_total subsequence of n - xp

x - ((n - xp) * e) is non empty Relation-like NAT -defined the carrier of f -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of f))

n0 | xp is Relation-like the carrier of f -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of f, the carrier of X))

l is set

rng xp is Element of K6( the carrier of f)

k1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT

xp . k1 is Element of the carrier of f

l is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT

(x - ((n - xp) * e)) . l is Element of the carrier of f

(n * e) . l is Element of the carrier of f

((n - xp) * e) . l is Element of the carrier of f

((n * e) . l) - (((n - xp) * e) . l) is Element of the carrier of f

- (((n - xp) * e) . l) is Element of the carrier of f

K342(f,((n * e) . l),(- (((n - xp) * e) . l))) is Element of the carrier of f

e . l is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT

n . (e . l) is Element of the carrier of f

(n . (e . l)) - (((n - xp) * e) . l) is Element of the carrier of f

K342(f,(n . (e . l)),(- (((n - xp) * e) . l))) is Element of the carrier of f

(n - xp) . (e . l) is Element of the carrier of f

(n . (e . l)) - ((n - xp) . (e . l)) is Element of the carrier of f

- ((n - xp) . (e . l)) is Element of the carrier of f

K342(f,(n . (e . l)),(- ((n - xp) . (e . l)))) is Element of the carrier of f

xp . (e . l) is Element of the carrier of f

(n . (e . l)) - (xp . (e . l)) is Element of the carrier of f

- (xp . (e . l)) is Element of the carrier of f

K342(f,(n . (e . l)),(- (xp . (e . l)))) is Element of the carrier of f

(n . (e . l)) - ((n . (e . l)) - (xp . (e . l))) is Element of the carrier of f

- ((n . (e . l)) - (xp . (e . l))) is Element of the carrier of f

K342(f,(n . (e . l)),(- ((n . (e . l)) - (xp . (e . l))))) is Element of the carrier of f

(n . (e . l)) - (n . (e . l)) is Element of the carrier of f

- (n . (e . l)) is Element of the carrier of f

K342(f,(n . (e . l)),(- (n . (e . l)))) is Element of the carrier of f

((n . (e . l)) - (n . (e . l))) + (xp . (e . l)) is Element of the carrier of f

0. f is V99(f) Element of the carrier of f

(0. f) + (xp . (e . l)) is Element of the carrier of f

xp * e is non empty Relation-like NAT -defined the carrier of f -valued Function-like total quasi_total subsequence of xp

(xp * e) . l is Element of the carrier of f

rng (x - ((n - xp) * e)) is Element of K6( the carrier of f)

(dom n0) /\ xp is Element of K6( the carrier of f)

dom (n0 | xp) is Element of K6( the carrier of f)

l is V11() real ext-real Element of REAL

l " is V11() real ext-real Element of REAL

k1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT

k2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT

k2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT

k2 + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT

k2 + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT

1 / (k2 + 1) is V11() real ext-real Element of REAL

1 / (k2 + 1) is V11() real ext-real Element of REAL

n . k2 is Element of the carrier of f

xp . k2 is Element of the carrier of f

(n . k2) - (xp . k2) is Element of the carrier of f

- (xp . k2) is Element of the carrier of f

K342(f,(n . k2),(- (xp . k2))) is Element of the carrier of f

||.((n . k2) - (xp . k2)).|| is V11() real ext-real non negative Element of REAL

1 / (l ") is V11() real ext-real Element of REAL

(n - xp) . k2 is Element of the carrier of f

((n - xp) . k2) - (0. f) is Element of the carrier of f

- (0. f) is Element of the carrier of f

K342(f,((n - xp) . k2),(- (0. f))) is Element of the carrier of f

||.(((n - xp) . k2) - (0. f)).|| is V11() real ext-real non negative Element of REAL

((n . k2) - (xp . k2)) - (0. f) is Element of the carrier of f

K342(f,((n . k2) - (xp . k2)),(- (0. f))) is Element of the carrier of f

||.(((n . k2) - (xp . k2)) - (0. f)).|| is V11() real ext-real non negative Element of REAL

rng x is Element of K6( the carrier of f)

(n0 | xp) /. (lim x) is Element of the carrier of X

(n0 | xp) /* x is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))

K7(NAT, the carrier of X) is set

K6(K7(NAT, the carrier of X)) is set

lim ((n0 | xp) /* x) is Element of the carrier of X

lim (n - xp) is Element of the carrier of f

lim ((n - xp) * e) is Element of the carrier of f

lim (x - ((n - xp) * e)) is Element of the carrier of f

(lim x) - (0. f) is Element of the carrier of f

K342(f,(lim x),(- (0. f))) is Element of the carrier of f

(n0 | xp) /* (x - ((n - xp) * e)) is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))

((n0 | xp) /* x) - ((n0 | xp) /* (x - ((n - xp) * e))) is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))

lim ((n0 | xp) /* (x - ((n - xp) * e))) is Element of the carrier of X

lim (((n0 | xp) /* x) - ((n0 | xp) /* (x - ((n - xp) * e)))) is Element of the carrier of X

((n0 | xp) /. (lim x)) - ((n0 | xp) /. (lim x)) is Element of the carrier of X

- ((n0 | xp) /. (lim x)) is Element of the carrier of X

K342(X,((n0 | xp) /. (lim x)),(- ((n0 | xp) /. (lim x)))) is Element of the carrier of X

0. X is V99(X) Element of the carrier of X

k1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT

x . k1 is Element of the carrier of f

(x - ((n - xp) * e)) . k1 is Element of the carrier of f

(((n0 | xp) /* x) - ((n0 | xp) /* (x - ((n - xp) * e)))) . k1 is Element of the carrier of X

((((n0 | xp) /* x) - ((n0 | xp) /* (x - ((n - xp) * e)))) . k1) - (0. X) is Element of the carrier of X

- (0. X) is Element of the carrier of X

K342(X,((((n0 | xp) /* x) - ((n0 | xp) /* (x - ((n - xp) * e)))) . k1),(- (0. X))) is Element of the carrier of X

||.(((((n0 | xp) /* x) - ((n0 | xp) /* (x - ((n - xp) * e)))) . k1) - (0. X)).|| is V11() real ext-real non negative Element of REAL

||.((((n0 | xp) /* x) - ((n0 | xp) /* (x - ((n - xp) * e)))) . k1).|| is V11() real ext-real non negative Element of REAL

((n0 | xp) /* x) . k1 is Element of the carrier of X

((n0 | xp) /* (x - ((n - xp) * e))) . k1 is Element of the carrier of X

(((n0 | xp) /* x) . k1) - (((n0 | xp) /* (x - ((n - xp) * e))) . k1) is Element of the carrier of X

- (((n0 | xp) /* (x - ((n - xp) * e))) . k1) is Element of the carrier of X

K342(X,(((n0 | xp) /* x) . k1),(- (((n0 | xp) /* (x - ((n - xp) * e))) . k1))) is Element of the carrier of X

||.((((n0 | xp) /* x) . k1) - (((n0 | xp) /* (x - ((n - xp) * e))) . k1)).|| is V11() real ext-real non negative Element of REAL

(n0 | xp) /. (x . k1) is Element of the carrier of X

((n0 | xp) /. (x . k1)) - (((n0 | xp) /* (x - ((n - xp) * e))) . k1) is Element of the carrier of X

K342(X,((n0 | xp) /. (x . k1)),(- (((n0 | xp) /* (x - ((n - xp) * e))) . k1))) is Element of the carrier of X

||.(((n0 | xp) /. (x . k1)) - (((n0 | xp) /* (x - ((n - xp) * e))) . k1)).|| is V11() real ext-real non negative Element of REAL

(n0 | xp) /. ((x - ((n - xp) * e)) . k1) is Element of the carrier of X

((n0 | xp) /. (x . k1)) - ((n0 | xp) /. ((x - ((n - xp) * e)) . k1)) is Element of the carrier of X

- ((n0 | xp) /. ((x - ((n - xp) * e)) . k1)) is Element of the carrier of X

K342(X,((n0 | xp) /. (x . k1)),(- ((n0 | xp) /. ((x - ((n - xp) * e)) . k1)))) is Element of the carrier of X

||.(((n0 | xp) /. (x . k1)) - ((n0 | xp) /. ((x - ((n - xp) * e)) . k1))).|| is V11() real ext-real non negative Element of REAL

n0 /. (x . k1) is Element of the carrier of X

(n0 /. (x . k1)) - ((n0 | xp) /. ((x - ((n - xp) * e)) . k1)) is Element of the carrier of X

K342(X,(n0 /. (x . k1)),(- ((n0 | xp) /. ((x - ((n - xp) * e)) . k1)))) is Element of the carrier of X

||.((n0 /. (x . k1)) - ((n0 | xp) /. ((x - ((n - xp) * e)) . k1))).|| is V11() real ext-real non negative Element of REAL

n0 /. ((x - ((n - xp) * e)) . k1) is Element of the carrier of X

(n0 /. (x . k1)) - (n0 /. ((x - ((n - xp) * e)) . k1)) is Element of the carrier of X

- (n0 /. ((x - ((n - xp) * e)) . k1)) is Element of the carrier of X

K342(X,(n0 /. (x . k1)),(- (n0 /. ((x - ((n - xp) * e)) . k1)))) is Element of the carrier of X

||.((n0 /. (x . k1)) - (n0 /. ((x - ((n - xp) * e)) . k1))).|| is V11() real ext-real non negative Element of REAL

e . k1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT

n . (e . k1) is Element of the carrier of f

n0 /. (n . (e . k1)) is Element of the carrier of X

(xp * e) . k1 is Element of the carrier of f

n0 /. ((xp * e) . k1) is Element of the carrier of X

(n0 /. (n . (e . k1))) - (n0 /. ((xp * e) . k1)) is Element of the carrier of X

- (n0 /. ((xp * e) . k1)) is Element of the carrier of X

K342(X,(n0 /. (n . (e . k1))),(- (n0 /. ((xp * e) . k1)))) is Element of the carrier of X

||.((n0 /. (n . (e . k1))) - (n0 /. ((xp * e) . k1))).|| is V11() real ext-real non negative Element of REAL

xp . (e . k1) is Element of the carrier of f

n0 /. (xp . (e . k1)) is Element of the carrier of X

(n0 /. (n . (e . k1))) - (n0 /. (xp . (e . k1))) is Element of the carrier of X

- (n0 /. (xp . (e . k1))) is Element of the carrier of X

K342(X,(n0 /. (n . (e . k1))),(- (n0 /. (xp . (e . k1))))) is Element of the carrier of X

||.((n0 /. (n . (e . k1))) - (n0 /. (xp . (e . k1)))).|| is V11() real ext-real non negative Element of REAL

f is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR

the carrier of f is non empty set

X is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR

the carrier of X is non empty set

K7( the carrier of f, the carrier of X) is set

K6(K7( the carrier of f, the carrier of X)) is set

K6( the carrier of f) is set

xp is Element of K6( the carrier of f)

n0 is Relation-like the carrier of f -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of f, the carrier of X))

dom n0 is Element of K6( the carrier of f)

n0 .: xp is Element of K6( the carrier of X)

K6( the carrier of X) is set

X is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR

the carrier of X is non empty set

K7( the carrier of X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7( the carrier of X,REAL)) is set

K6( the carrier of X) is set

n0 is Element of K6( the carrier of X)

f is Relation-like the carrier of X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of X,REAL))

dom f is Element of K6( the carrier of X)

f .: n0 is V47() V48() V49() Element of K6(REAL)

upper_bound (f .: n0) is V11() real ext-real Element of REAL

lower_bound (f .: n0) is V11() real ext-real Element of REAL

f is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR

the carrier of f is non empty set

n0 is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR

the carrier of n0 is non empty set

K7( the carrier of f, the carrier of n0) is set

K6(K7( the carrier of f, the carrier of n0)) is set

X is set

xp is Relation-like the carrier of f -defined the carrier of n0 -valued Function-like Element of K6(K7( the carrier of f, the carrier of n0))

dom xp is Element of K6( the carrier of f)

K6( the carrier of f) is set

xp | X is Relation-like the carrier of f -defined the carrier of n0 -valued Function-like Element of K6(K7( the carrier of f, the carrier of n0))

X is non empty NORMSTR

the carrier of X is non empty set

K7( the carrier of X, the carrier of X) is set

K6(K7( the carrier of X, the carrier of X)) is set

X is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR

the carrier of X is non empty set

K7( the carrier of X, the carrier of X) is set

K6(K7( the carrier of X, the carrier of X)) is set

the Element of the carrier of X is Element of the carrier of X

the carrier of X --> the Element of the carrier of X is non empty Relation-like the carrier of X -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7( the carrier of X, the carrier of X))

n0 is non empty Relation-like the carrier of X -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7( the carrier of X, the carrier of X))

1 / 2 is V11() real ext-real non negative Element of REAL

xp is Element of the carrier of X

n0 . xp is Element of the carrier of X

x is Element of the carrier of X

n0 . x is Element of the carrier of X

(n0 . xp) - (n0 . x) is Element of the carrier of X

- (n0 . x) is Element of the carrier of X

K342(X,(n0 . xp),(- (n0 . x))) is Element of the carrier of X

||.((n0 . xp) - (n0 . x)).|| is V11() real ext-real non negative Element of REAL

xp - x is Element of the carrier of X

- x is Element of the carrier of X

K342(X,xp,(- x)) is Element of the carrier of X

||.(xp - x).|| is V11() real ext-real non negative Element of REAL

(1 / 2) * ||.(xp - x).|| is V11() real ext-real non negative Element of REAL

X is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR

the carrier of X is non empty set

f is Element of the carrier of X

xp is Element of the carrier of X

f - xp is Element of the carrier of X

- xp is Element of the carrier of X

K342(X,f,(- xp)) is Element of the carrier of X

||.(f - xp).|| is V11() real ext-real non negative Element of REAL

n0 is Element of the carrier of X

xp - n0 is Element of the carrier of X

- n0 is Element of the carrier of X

K342(X,xp,(- n0)) is Element of the carrier of X

||.(xp - n0).|| is V11() real ext-real non negative Element of REAL

f - n0 is Element of the carrier of X

K342(X,f,(- n0)) is Element of the carrier of X

||.(f - n0).|| is V11() real ext-real non negative Element of REAL

x is V11() real ext-real Element of REAL

x / 2 is V11() real ext-real Element of REAL

(x / 2) + (x / 2) is V11() real ext-real Element of REAL

||.(f - xp).|| + ||.(xp - n0).|| is V11() real ext-real non negative Element of REAL

(||.(f - xp).|| + ||.(xp - n0).||) + x is V11() real ext-real Element of REAL

||.(f - n0).|| + (||.(f - xp).|| + ||.(xp - n0).||) is V11() real ext-real non negative Element of REAL

x + (||.(f - xp).|| + ||.(xp - n0).||) is V11() real ext-real Element of REAL

- (||.(f - xp).|| + ||.(xp - n0).||) is V11() real ext-real non positive Element of REAL

(x + (||.(f - xp).|| + ||.(xp - n0).||)) + (- (||.(f - xp).|| + ||.(xp - n0).||)) is V11() real ext-real Element of REAL

(||.(f - n0).|| + (||.(f - xp).|| + ||.(xp - n0).||)) + (- (||.(f - xp).|| + ||.(xp - n0).||)) is V11() real ext-real Element of REAL

X is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR

the carrier of X is non empty set

f is Element of the carrier of X

xp is Element of the carrier of X

f - xp is Element of the carrier of X

- xp is Element of the carrier of X

K342(X,f,(- xp)) is Element of the carrier of X

||.(f - xp).|| is V11() real ext-real non negative Element of REAL

n0 is Element of the carrier of X

n0 - xp is Element of the carrier of X

K342(X,n0,(- xp)) is Element of the carrier of X

||.(n0 - xp).|| is V11() real ext-real non negative Element of REAL

f - n0 is Element of the carrier of X

- n0 is Element of the carrier of X

K342(X,f,(- n0)) is Element of the carrier of X

||.(f - n0).|| is V11() real ext-real non negative Element of REAL

x is V11() real ext-real Element of REAL

x / 2 is V11() real ext-real Element of REAL

- (n0 - xp) is Element of the carrier of X

||.(- (n0 - xp)).|| is V11() real ext-real non negative Element of REAL

xp - n0 is Element of the carrier of X

K342(X,xp,(- n0)) is Element of the carrier of X

||.(xp - n0).|| is V11() real ext-real non negative Element of REAL

X is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR

the carrier of X is non empty set

f is Element of the carrier of X

n0 is Element of the carrier of X

f - n0 is Element of the carrier of X

- n0 is Element of the carrier of X

K342(X,f,(- n0)) is Element of the carrier of X

||.(f - n0).|| is V11() real ext-real non negative Element of REAL

0. X is V99(X) Element of the carrier of X

X is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR

the carrier of X is non empty set

f is Element of the carrier of X

n0 is Element of the carrier of X

f - n0 is Element of the carrier of X

- n0 is Element of the carrier of X

K342(X,f,(- n0)) is Element of the carrier of X

||.(f - n0).|| is V11() real ext-real non negative Element of REAL

n0 - f is Element of the carrier of X

- f is Element of the carrier of X

K342(X,n0,(- f)) is Element of the carrier of X

||.(n0 - f).|| is V11() real ext-real non negative Element of REAL

- (f - n0) is Element of the carrier of X

||.(- (f - n0)).|| is V11() real ext-real non negative Element of REAL

X is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR

the carrier of X is non empty set

0. X is V99(X) Element of the carrier of X

f is Element of the carrier of X

||.f.|| is V11() real ext-real non negative Element of REAL

X is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR

the carrier of X is non empty set

xp is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR

the carrier of xp is non empty set

xp is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR

the carrier of xp is non empty set

n is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR

the carrier of n is non empty set

k2 is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR

the carrier of k2 is non empty set

c

the carrier of c

c

the carrier of c

c

the carrier of c

c

the carrier of c

c

the carrier of c

c

the carrier of c

f is Element of the carrier of X

n0 is Element of the carrier of X

f - n0 is Element of the carrier of X

- n0 is Element of the carrier of X

K342(X,f,(- n0)) is Element of the carrier of X

||.(f - n0).|| is V11() real ext-real non negative Element of REAL

x is Element of the carrier of xp

n is Element of the carrier of xp

x - n is Element of the carrier of xp

- n is Element of the carrier of xp

K342(xp,x,(- n)) is Element of the carrier of xp

||.(x - n).|| is V11() real ext-real non negative Element of REAL

x is Element of the carrier of xp

e is Element of the carrier of xp

x - e is Element of the carrier of xp

- e is Element of the carrier of xp

K342(xp,x,(- e)) is Element of the carrier of xp

||.(x - e).|| is V11() real ext-real non negative Element of REAL

l is Element of the carrier of n

k1 is Element of the carrier of n

l - k1 is Element of the carrier of n

- k1 is Element of the carrier of n

K342(n,l,(- k1)) is Element of the carrier of n

||.(l - k1).|| is V11() real ext-real non negative Element of REAL

k2 is Element of the carrier of k2

k1 is Element of the carrier of k2

k2 - k1 is Element of the carrier of k2

- k1 is Element of the carrier of k2

K342(k2,k2,(- k1)) is Element of the carrier of k2

||.(k2 - k1).|| is V11() real ext-real non negative Element of REAL

c

c

c

- c

K342(c

||.(c

c

c

c

- c

K342(c

||.(c

c

- c

K342(c

||.(c

c

c

c

c

c

- c

K342(c

||.(c

c

c

- c

K342(c

||.(c

c

K342(c

||.(c

c

c

c

c

c

- c

K342(c

||.(c

c

c

K342(c

||.(c

c

- c

K342(c

||.(c

c

||.c

0. c

c

c

c

- c

K342(c

||.(c

X is V11() real ext-real set

n0 is V11() real ext-real set

f is V11() real ext-real set

xp is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

f (#) xp is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

lim xp is V11() real ext-real Element of REAL

lim (f (#) xp) is V11() real ext-real Element of REAL

f * (lim xp) is V11() real ext-real Element of REAL

x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT

(f (#) xp) . x is V11() real ext-real Element of REAL

((f (#) xp) . x) - 0 is V11() real ext-real Element of REAL

abs (((f (#) xp) . x) - 0) is V11() real ext-real Element of REAL

xp . x is V11() real ext-real Element of REAL

f * (xp . x) is V11() real ext-real Element of REAL

abs (f * (xp . x)) is V11() real ext-real Element of REAL

x + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT

X to_power (x + 1) is V11() real ext-real set

f * (X to_power (x + 1)) is V11() real ext-real set

abs (f * (X to_power (x + 1))) is V11() real ext-real Element of REAL

X is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() NORMSTR

the carrier of X is non empty set

K7( the carrier of X, the carrier of X) is set

K6(K7( the carrier of X, the carrier of X)) is set

the Element of the carrier of X is Element of the carrier of X

n0 is non empty Relation-like the carrier of X -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7( the carrier of X, the carrier of X))

xp is V11() real ext-real Element of REAL

x is Relation-like Function-like set

dom x is set

x . 0 is set

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT

x . n is set

n + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT

x . (n + 1) is set

n0 . (x . n) is set

n is set

x . n is set

K7(NAT, the carrier of X) is set

K6(K7(NAT, the carrier of X)) is set

n is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))

n ^\ 1 is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total subsequence of n

xp is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT

(n ^\ 1) . xp is Element of the carrier of X

lim n is Element of the carrier of X

n0 . (lim n) is Element of the carrier of X

((n ^\ 1) . xp) - (n0 . (lim n)) is Element of the carrier of X

- (n0 . (lim n)) is Element of the carrier of X

K342(X,((n ^\ 1) . xp),(- (n0 . (lim n)))) is Element of the carrier of X

||.(((n ^\ 1) . xp) - (n0 . (lim n))).|| is V11() real ext-real non negative Element of REAL

xp + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT

n . (xp + 1) is Element of the carrier of X

(n . (xp + 1)) - (n0 . (lim n)) is Element of the carrier of X

K342(X,(n . (xp + 1)),(- (n0 . (lim n)))) is Element of the carrier of X

||.((n . (xp + 1)) - (n0 . (lim n))).|| is V11() real ext-real non negative Element of REAL

n . xp is Element of the carrier of X

n0 . (n . xp) is Element of the carrier of X

(n0 . (n . xp)) - (n0 . (lim n)) is Element of the carrier of X

K342(X,(n0 . (n . xp)),(- (n0 . (lim n)))) is Element of the carrier of X

||.((n0 . (n . xp)) - (n0 . (lim n))).|| is V11() real