:: 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₁₆ is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR
the carrier of c₁₆ is non empty set
c₁₉ is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR
the carrier of c₁₉ is non empty set
c₂₂ is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR
the carrier of c₂₂ is non empty set
c₂₇ is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR
the carrier of c₂₇ is non empty set
c₃₂ is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR
the carrier of c₃₂ is non empty set
c₃₄ is non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like NORMSTR
the carrier of c₃₄ 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
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₁₇ is Element of the carrier of c₁₆
c₁₈ is Element of the carrier of c₁₆
c₁₇ - c₁₈ is Element of the carrier of c₁₆
- c₁₈ is Element of the carrier of c₁₆
K342(c₁₆,c₁₇,(- c₁₈)) is Element of the carrier of c₁₆
||.(c₁₇ - c₁₈).|| is V11() real ext-real non negative Element of REAL
c₂₀ is Element of the carrier of c₁₉
c₂₁ is Element of the carrier of c₁₉
c₂₀ - c₂₁ is Element of the carrier of c₁₉
- c₂₁ is Element of the carrier of c₁₉
K342(c₁₉,c₂₀,(- c₂₁)) is Element of the carrier of c₁₉
||.(c₂₀ - c₂₁).|| is V11() real ext-real non negative Element of REAL
c₂₁ - c₂₀ is Element of the carrier of c₁₉
- c₂₀ is Element of the carrier of c₁₉
K342(c₁₉,c₂₁,(- c₂₀)) is Element of the carrier of c₁₉
||.(c₂₁ - c₂₀).|| is V11() real ext-real non negative Element of REAL
c₂₆ is V11() real ext-real Element of REAL
c₂₆ / 2 is V11() real ext-real Element of REAL
c₂₃ is Element of the carrier of c₂₂
c₂₅ is Element of the carrier of c₂₂
c₂₃ - c₂₅ is Element of the carrier of c₂₂
- c₂₅ is Element of the carrier of c₂₂
K342(c₂₂,c₂₃,(- c₂₅)) is Element of the carrier of c₂₂
||.(c₂₃ - c₂₅).|| is V11() real ext-real non negative Element of REAL
c₂₄ is Element of the carrier of c₂₂
c₂₅ - c₂₄ is Element of the carrier of c₂₂
- c₂₄ is Element of the carrier of c₂₂
K342(c₂₂,c₂₅,(- c₂₄)) is Element of the carrier of c₂₂
||.(c₂₅ - c₂₄).|| is V11() real ext-real non negative Element of REAL
c₂₃ - c₂₄ is Element of the carrier of c₂₂
K342(c₂₂,c₂₃,(- c₂₄)) is Element of the carrier of c₂₂
||.(c₂₃ - c₂₄).|| is V11() real ext-real non negative Element of REAL
c₃₁ is V11() real ext-real Element of REAL
c₃₁ / 2 is V11() real ext-real Element of REAL
c₂₈ is Element of the carrier of c₂₇
c₃₀ is Element of the carrier of c₂₇
c₂₈ - c₃₀ is Element of the carrier of c₂₇
- c₃₀ is Element of the carrier of c₂₇
K342(c₂₇,c₂₈,(- c₃₀)) is Element of the carrier of c₂₇
||.(c₂₈ - c₃₀).|| is V11() real ext-real non negative Element of REAL
c₂₉ is Element of the carrier of c₂₇
c₂₉ - c₃₀ is Element of the carrier of c₂₇
K342(c₂₇,c₂₉,(- c₃₀)) is Element of the carrier of c₂₇
||.(c₂₉ - c₃₀).|| is V11() real ext-real non negative Element of REAL
c₂₈ - c₂₉ is Element of the carrier of c₂₇
- c₂₉ is Element of the carrier of c₂₇
K342(c₂₇,c₂₈,(- c₂₉)) is Element of the carrier of c₂₇
||.(c₂₈ - c₂₉).|| is V11() real ext-real non negative Element of REAL
c₃₃ is Element of the carrier of c₃₂
||.c₃₃.|| is V11() real ext-real non negative Element of REAL
0. c₃₂ is V99(c₃₂) Element of the carrier of c₃₂
c₃₅ is Element of the carrier of c₃₄
c₃₆ is Element of the carrier of c₃₄
c₃₅ - c₃₆ is Element of the carrier of c₃₄
- c₃₆ is Element of the carrier of c₃₄
K342(c₃₄,c₃₅,(- c₃₆)) is Element of the carrier of c₃₄
||.(c₃₅ - c₃₆).|| is V11() real ext-real non negative Element of REAL
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 ext-real non negative Element of REAL
(n . xp) - (lim n) is Element of the carrier of X
- (lim n) is Element of the carrier of X
K342(X,(n . xp),(- (lim n))) is Element of the carrier of X
||.((n . xp) - (lim n)).|| is V11() real ext-real non negative Element of REAL
xp * ||.((n . xp) - (lim n)).|| is V11() real ext-real Element of REAL
n . 1 is Element of the carrier of X
n . 0 is Element of the carrier of X
(n . 1) - (n . 0) is Element of the carrier of X
- (n . 0) is Element of the carrier of X
K342(X,(n . 1),(- (n . 0))) is Element of the carrier of X
||.((n . 1) - (n . 0)).|| is V11() real ext-real non negative Element of REAL
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
n . (xp + 1) is Element of the carrier of X
n . xp is Element of the carrier of X
(n . (xp + 1)) - (n . xp) is Element of the carrier of X
- (n . xp) is Element of the carrier of X
K342(X,(n . (xp + 1)),(- (n . xp))) is Element of the carrier of X
||.((n . (xp + 1)) - (n . xp)).|| is V11() real ext-real non negative Element of REAL
xp to_power xp is V11() real ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * (xp to_power xp) is V11() real ext-real Element of REAL
(xp + 1) + 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) + 1) is Element of the carrier of X
(n . ((xp + 1) + 1)) - (n . (xp + 1)) is Element of the carrier of X
- (n . (xp + 1)) is Element of the carrier of X
K342(X,(n . ((xp + 1) + 1)),(- (n . (xp + 1)))) is Element of the carrier of X
||.((n . ((xp + 1) + 1)) - (n . (xp + 1))).|| is V11() real ext-real non negative Element of REAL
xp to_power (xp + 1) is V11() real ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * (xp to_power (xp + 1)) is V11() real ext-real Element of REAL
xp * ||.((n . (xp + 1)) - (n . xp)).|| is V11() real ext-real Element of REAL
xp * (||.((n . 1) - (n . 0)).|| * (xp to_power xp)) is V11() real ext-real Element of REAL
n0 . (n . (xp + 1)) is Element of the carrier of X
n0 . (n . xp) is Element of the carrier of X
(n0 . (n . (xp + 1))) - (n0 . (n . xp)) is Element of the carrier of X
- (n0 . (n . xp)) is Element of the carrier of X
K342(X,(n0 . (n . (xp + 1))),(- (n0 . (n . xp)))) is Element of the carrier of X
||.((n0 . (n . (xp + 1))) - (n0 . (n . xp))).|| is V11() real ext-real non negative Element of REAL
xp * (xp to_power xp) is V11() real ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * (xp * (xp to_power xp)) is V11() real ext-real Element of REAL
xp to_power 1 is V11() real ext-real Element of REAL
(xp to_power 1) * (xp to_power xp) is V11() real ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * ((xp to_power 1) * (xp to_power xp)) is V11() real ext-real Element of REAL
0 + 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
n . (0 + 1) is Element of the carrier of X
(n . (0 + 1)) - (n . 0) is Element of the carrier of X
K342(X,(n . (0 + 1)),(- (n . 0))) is Element of the carrier of X
||.((n . (0 + 1)) - (n . 0)).|| is V11() real ext-real non negative Element of REAL
||.((n . 1) - (n . 0)).|| * 1 is V11() real ext-real non negative Element of REAL
xp to_power 0 is V11() real ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * (xp to_power 0) is V11() real ext-real Element of REAL
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
n . (xp + 1) is Element of the carrier of X
n . xp is Element of the carrier of X
(n . (xp + 1)) - (n . xp) is Element of the carrier of X
- (n . xp) is Element of the carrier of X
K342(X,(n . (xp + 1)),(- (n . xp))) is Element of the carrier of X
||.((n . (xp + 1)) - (n . xp)).|| is V11() real ext-real non negative Element of REAL
xp to_power xp is V11() real ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * (xp to_power xp) is V11() real ext-real Element of REAL
1 - xp is V11() real ext-real Element of REAL
xp is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
xp to_power x is V11() real ext-real Element of REAL
x + xp is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
xp to_power (x + xp) is V11() real ext-real Element of REAL
(xp to_power x) - (xp to_power (x + xp)) is V11() real ext-real Element of REAL
((xp to_power x) - (xp to_power (x + xp))) / (1 - xp) is V11() real ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * (((xp to_power x) - (xp to_power (x + xp))) / (1 - xp)) is V11() real ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * (xp to_power (x + xp)) is V11() real ext-real Element of REAL
(||.((n . 1) - (n . 0)).|| * (((xp to_power x) - (xp to_power (x + xp))) / (1 - xp))) + (||.((n . 1) - (n . 0)).|| * (xp to_power (x + xp))) is V11() real ext-real Element of REAL
(||.((n . 1) - (n . 0)).|| * (xp to_power (x + xp))) * (1 - xp) is V11() real ext-real Element of REAL
((||.((n . 1) - (n . 0)).|| * (xp to_power (x + xp))) * (1 - xp)) / (1 - xp) is V11() real ext-real Element of REAL
(||.((n . 1) - (n . 0)).|| * (((xp to_power x) - (xp to_power (x + xp))) / (1 - xp))) + (((||.((n . 1) - (n . 0)).|| * (xp to_power (x + xp))) * (1 - xp)) / (1 - xp)) is V11() real ext-real Element of REAL
(xp to_power (x + xp)) * (1 - xp) is V11() real ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * ((xp to_power (x + xp)) * (1 - xp)) is V11() real ext-real Element of REAL
(||.((n . 1) - (n . 0)).|| * ((xp to_power (x + xp)) * (1 - xp))) / (1 - xp) is V11() real ext-real Element of REAL
(||.((n . 1) - (n . 0)).|| * (((xp to_power x) - (xp to_power (x + xp))) / (1 - xp))) + ((||.((n . 1) - (n . 0)).|| * ((xp to_power (x + xp)) * (1 - xp))) / (1 - xp)) is V11() real ext-real Element of REAL
((xp to_power (x + xp)) * (1 - xp)) / (1 - xp) is V11() real ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * (((xp to_power (x + xp)) * (1 - xp)) / (1 - xp)) is V11() real ext-real Element of REAL
(||.((n . 1) - (n . 0)).|| * (((xp to_power x) - (xp to_power (x + xp))) / (1 - xp))) + (||.((n . 1) - (n . 0)).|| * (((xp to_power (x + xp)) * (1 - xp)) / (1 - xp))) is V11() real ext-real Element of REAL
(((xp to_power x) - (xp to_power (x + xp))) / (1 - xp)) + (((xp to_power (x + xp)) * (1 - xp)) / (1 - xp)) is V11() real ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * ((((xp to_power x) - (xp to_power (x + xp))) / (1 - xp)) + (((xp to_power (x + xp)) * (1 - xp)) / (1 - xp))) is V11() real ext-real Element of REAL
((xp to_power x) - (xp to_power (x + xp))) + ((xp to_power (x + xp)) * (1 - xp)) is V11() real ext-real Element of REAL
(((xp to_power x) - (xp to_power (x + xp))) + ((xp to_power (x + xp)) * (1 - xp))) / (1 - xp) is V11() real ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * ((((xp to_power x) - (xp to_power (x + xp))) + ((xp to_power (x + xp)) * (1 - xp))) / (1 - xp)) is V11() real ext-real Element of REAL
xp * (xp to_power (x + xp)) is V11() real ext-real Element of REAL
(xp to_power x) - (xp * (xp to_power (x + xp))) is V11() real ext-real Element of REAL
((xp to_power x) - (xp * (xp to_power (x + xp)))) / (1 - xp) is V11() real ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * (((xp to_power x) - (xp * (xp to_power (x + xp)))) / (1 - xp)) is V11() real ext-real Element of REAL
xp to_power 1 is V11() real ext-real Element of REAL
(xp to_power 1) * (xp to_power (x + xp)) is V11() real ext-real Element of REAL
(xp to_power x) - ((xp to_power 1) * (xp to_power (x + xp))) is V11() real ext-real Element of REAL
((xp to_power x) - ((xp to_power 1) * (xp to_power (x + xp)))) / (1 - xp) is V11() real ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * (((xp to_power x) - ((xp to_power 1) * (xp to_power (x + xp)))) / (1 - xp)) is V11() real ext-real Element of REAL
(x + xp) + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
xp to_power ((x + xp) + 1) is V11() real ext-real Element of REAL
(xp to_power x) - (xp to_power ((x + xp) + 1)) is V11() real ext-real Element of REAL
((xp to_power x) - (xp to_power ((x + xp) + 1))) / (1 - xp) is V11() real ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * (((xp to_power x) - (xp to_power ((x + xp) + 1))) / (1 - xp)) is V11() real ext-real Element of REAL
n . (x + xp) is Element of the carrier of X
n . x is Element of the carrier of X
(n . (x + xp)) - (n . x) is Element of the carrier of X
- (n . x) is Element of the carrier of X
K342(X,(n . (x + xp)),(- (n . x))) is Element of the carrier of X
||.((n . (x + xp)) - (n . x)).|| is V11() real ext-real non negative Element of REAL
n . ((x + xp) + 1) is Element of the carrier of X
(n . ((x + xp) + 1)) - (n . (x + xp)) is Element of the carrier of X
- (n . (x + xp)) is Element of the carrier of X
K342(X,(n . ((x + xp) + 1)),(- (n . (x + xp)))) is Element of the carrier of X
||.((n . ((x + xp) + 1)) - (n . (x + xp))).|| 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
x + (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 . (x + (xp + 1)) is Element of the carrier of X
(n . (x + (xp + 1))) - (n . x) is Element of the carrier of X
K342(X,(n . (x + (xp + 1))),(- (n . x))) is Element of the carrier of X
||.((n . (x + (xp + 1))) - (n . x)).|| is V11() real ext-real non negative Element of REAL
(n . (x + (xp + 1))) - (n . (x + xp)) is Element of the carrier of X
K342(X,(n . (x + (xp + 1))),(- (n . (x + xp)))) is Element of the carrier of X
||.((n . (x + (xp + 1))) - (n . (x + xp))).|| is V11() real ext-real non negative Element of REAL
||.((n . (x + (xp + 1))) - (n . (x + xp))).|| + ||.((n . (x + xp)) - (n . x)).|| is V11() real ext-real non negative Element of REAL
(||.((n . 1) - (n . 0)).|| * (xp to_power (x + xp))) + (||.((n . 1) - (n . 0)).|| * (((xp to_power x) - (xp to_power (x + xp))) / (1 - xp))) is V11() real ext-real Element of REAL
xp to_power (x + (xp + 1)) is V11() real ext-real Element of REAL
(xp to_power x) - (xp to_power (x + (xp + 1))) is V11() real ext-real Element of REAL
((xp to_power x) - (xp to_power (x + (xp + 1)))) / (1 - xp) is V11() real ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * (((xp to_power x) - (xp to_power (x + (xp + 1)))) / (1 - 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
x + (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 . (x + (xp + 1)) is Element of the carrier of X
n . x is Element of the carrier of X
(n . (x + (xp + 1))) - (n . x) is Element of the carrier of X
- (n . x) is Element of the carrier of X
K342(X,(n . (x + (xp + 1))),(- (n . x))) is Element of the carrier of X
||.((n . (x + (xp + 1))) - (n . x)).|| is V11() real ext-real non negative Element of REAL
xp to_power x is V11() real ext-real Element of REAL
xp to_power (x + (xp + 1)) is V11() real ext-real Element of REAL
(xp to_power x) - (xp to_power (x + (xp + 1))) is V11() real ext-real Element of REAL
((xp to_power x) - (xp to_power (x + (xp + 1)))) / (1 - xp) is V11() real ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * (((xp to_power x) - (xp to_power (x + (xp + 1)))) / (1 - xp)) is V11() real ext-real Element of REAL
xp is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
xp + 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
n . (xp + 0) is Element of the carrier of X
n . xp is Element of the carrier of X
(n . (xp + 0)) - (n . xp) is Element of the carrier of X
- (n . xp) is Element of the carrier of X
K342(X,(n . (xp + 0)),(- (n . xp))) is Element of the carrier of X
||.((n . (xp + 0)) - (n . xp)).|| is V11() real ext-real non negative Element of REAL
0. X is V99(X) Element of the carrier of X
||.(0. X).|| is V11() real ext-real non negative Element of REAL
xp to_power xp is V11() real ext-real Element of REAL
xp to_power (xp + 0) is V11() real ext-real Element of REAL
(xp to_power xp) - (xp to_power (xp + 0)) is V11() real ext-real Element of REAL
((xp to_power xp) - (xp to_power (xp + 0))) / (1 - xp) is V11() real ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * (((xp to_power xp) - (xp to_power (xp + 0))) / (1 - xp)) is V11() real ext-real Element of REAL
xp is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
xp + 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
n . (xp + 0) is Element of the carrier of X
n . xp is Element of the carrier of X
(n . (xp + 0)) - (n . xp) is Element of the carrier of X
- (n . xp) is Element of the carrier of X
K342(X,(n . (xp + 0)),(- (n . xp))) is Element of the carrier of X
||.((n . (xp + 0)) - (n . xp)).|| is V11() real ext-real non negative Element of REAL
xp to_power xp is V11() real ext-real Element of REAL
xp to_power (xp + 0) is V11() real ext-real Element of REAL
(xp to_power xp) - (xp to_power (xp + 0)) is V11() real ext-real Element of REAL
((xp to_power xp) - (xp to_power (xp + 0))) / (1 - xp) is V11() real ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * (((xp to_power xp) - (xp to_power (xp + 0))) / (1 - 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
xp is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
x + xp is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
n . (x + xp) is Element of the carrier of X
n . x is Element of the carrier of X
(n . (x + xp)) - (n . x) is Element of the carrier of X
- (n . x) is Element of the carrier of X
K342(X,(n . (x + xp)),(- (n . x))) is Element of the carrier of X
||.((n . (x + xp)) - (n . x)).|| is V11() real ext-real non negative Element of REAL
xp to_power x is V11() real ext-real Element of REAL
xp to_power (x + xp) is V11() real ext-real Element of REAL
(xp to_power x) - (xp to_power (x + xp)) is V11() real ext-real Element of REAL
((xp to_power x) - (xp to_power (x + xp))) / (1 - xp) is V11() real ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * (((xp to_power x) - (xp to_power (x + xp))) / (1 - xp)) is V11() real ext-real Element of REAL
xp is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
x + xp is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
xp to_power (x + xp) is V11() real ext-real Element of REAL
xp to_power x is V11() real ext-real Element of REAL
(xp to_power x) - (xp to_power (x + xp)) is V11() real ext-real Element of REAL
(xp to_power x) - 0 is V11() real ext-real Element of REAL
1 - 1 is V11() real ext-real Element of REAL
((xp to_power x) - (xp to_power (x + xp))) / (1 - xp) is V11() real ext-real Element of REAL
(xp to_power x) / (1 - xp) is V11() real ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * (((xp to_power x) - (xp to_power (x + xp))) / (1 - xp)) is V11() real ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * ((xp to_power x) / (1 - xp)) is V11() real ext-real Element of REAL
n . (x + xp) is Element of the carrier of X
n . x is Element of the carrier of X
(n . (x + xp)) - (n . x) is Element of the carrier of X
- (n . x) is Element of the carrier of X
K342(X,(n . (x + xp)),(- (n . x))) is Element of the carrier of X
||.((n . (x + xp)) - (n . x)).|| is V11() real ext-real non negative 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
x + xp is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
n . (x + xp) is Element of the carrier of X
n . x is Element of the carrier of X
(n . (x + xp)) - (n . x) is Element of the carrier of X
- (n . x) is Element of the carrier of X
K342(X,(n . (x + xp)),(- (n . x))) is Element of the carrier of X
||.((n . (x + xp)) - (n . x)).|| is V11() real ext-real non negative Element of REAL
xp to_power x is V11() real ext-real Element of REAL
(xp to_power x) / (1 - xp) is V11() real ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * ((xp to_power x) / (1 - xp)) is V11() real ext-real Element of REAL
xp is V11() real ext-real Element of REAL
xp / 2 is V11() real ext-real Element of REAL
||.((n . 1) - (n . 0)).|| / (1 - 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
xp to_power x is V11() real ext-real Element of REAL
(||.((n . 1) - (n . 0)).|| / (1 - xp)) * (xp to_power x) is V11() real ext-real Element of REAL
abs ((||.((n . 1) - (n . 0)).|| / (1 - xp)) * (xp to_power 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
(xp to_power x) / (1 - xp) is V11() real ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * ((xp to_power x) / (1 - xp)) is V11() real ext-real Element of REAL
e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
l is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
k1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set
x + 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 set
x + 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
x + k2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
n . (x + k2) is Element of the carrier of X
n . x is Element of the carrier of X
(n . (x + k2)) - (n . x) is Element of the carrier of X
- (n . x) is Element of the carrier of X
K342(X,(n . (x + k2)),(- (n . x))) is Element of the carrier of X
||.((n . (x + k2)) - (n . x)).|| is V11() real ext-real non negative Element of REAL
n . l is Element of the carrier of X
(n . l) - (n . x) is Element of the carrier of X
K342(X,(n . l),(- (n . x))) is Element of the carrier of X
||.((n . l) - (n . x)).|| is V11() real ext-real non negative 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
x + k1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
n . (x + k1) is Element of the carrier of X
(n . (x + k1)) - (n . x) is Element of the carrier of X
K342(X,(n . (x + k1)),(- (n . x))) is Element of the carrier of X
||.((n . (x + k1)) - (n . x)).|| is V11() real ext-real non negative Element of REAL
n . n is Element of the carrier of X
(n . n) - (n . x) is Element of the carrier of X
K342(X,(n . n),(- (n . x))) is Element of the carrier of X
||.((n . n) - (n . x)).|| is V11() real ext-real non negative Element of REAL
(n . l) - (n . n) is Element of the carrier of X
- (n . n) is Element of the carrier of X
K342(X,(n . l),(- (n . n))) is Element of the carrier of X
||.((n . l) - (n . n)).|| is V11() real ext-real non negative 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
l is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
n . n is Element of the carrier of X
n . l is Element of the carrier of X
(n . n) - (n . l) is Element of the carrier of X
- (n . l) is Element of the carrier of X
K342(X,(n . n),(- (n . l))) is Element of the carrier of X
||.((n . n) - (n . l)).|| is V11() real ext-real non negative Element of REAL
n - (lim 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 - (lim n)).|| 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))
xp (#) ||.(n - (lim n)).|| 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 (#) ||.(n - (lim n)).||) is V11() real ext-real Element of REAL
lim ||.(n - (lim n)).|| is V11() real ext-real Element of REAL
xp * (lim ||.(n - (lim n)).||) is V11() real ext-real Element of REAL
xp * 0 is V11() real ext-real Element of REAL
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
e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
(xp (#) ||.(n - (lim n)).||) . e is V11() real ext-real Element of REAL
((xp (#) ||.(n - (lim n)).||) . e) - 0 is V11() real ext-real Element of REAL
abs (((xp (#) ||.(n - (lim n)).||) . e) - 0) is V11() real ext-real Element of REAL
||.(n - (lim n)).|| . e is V11() real ext-real Element of REAL
xp * (||.(n - (lim n)).|| . e) is V11() real ext-real Element of REAL
abs (xp * (||.(n - (lim n)).|| . e)) is V11() real ext-real Element of REAL
(n - (lim n)) . e is Element of the carrier of X
||.((n - (lim n)) . e).|| is V11() real ext-real non negative Element of REAL
xp * ||.((n - (lim n)) . e).|| is V11() real ext-real Element of REAL
abs (xp * ||.((n - (lim n)) . e).||) is V11() real ext-real Element of REAL
n . e is Element of the carrier of X
(n . e) - (lim n) is Element of the carrier of X
K342(X,(n . e),(- (lim n))) is Element of the carrier of X
||.((n . e) - (lim n)).|| is V11() real ext-real non negative Element of REAL
xp * ||.((n . e) - (lim n)).|| is V11() real ext-real Element of REAL
abs (xp * ||.((n . e) - (lim n)).||) is V11() real ext-real Element of REAL
(n ^\ 1) . e is Element of the carrier of X
((n ^\ 1) . e) - (n0 . (lim n)) is Element of the carrier of X
K342(X,((n ^\ 1) . e),(- (n0 . (lim n)))) is Element of the carrier of X
||.(((n ^\ 1) . e) - (n0 . (lim n))).|| is V11() real ext-real non negative Element of REAL
e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
(n ^\ 1) . e is Element of the carrier of X
((n ^\ 1) . e) - (n0 . (lim n)) is Element of the carrier of X
K342(X,((n ^\ 1) . e),(- (n0 . (lim n)))) is Element of the carrier of X
||.(((n ^\ 1) . e) - (n0 . (lim n))).|| 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
lim (n ^\ 1) is Element of the carrier of X
x is Element of the carrier of X
n0 . x is Element of the carrier of X
x - xp is Element of the carrier of X
- xp is Element of the carrier of X
K342(X,x,(- xp)) is Element of the carrier of X
||.(x - xp).|| is V11() real ext-real non negative Element of REAL
e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
xp to_power e is V11() real ext-real Element of REAL
||.(x - xp).|| * (xp to_power e) is V11() real ext-real Element of REAL
e + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
xp to_power (e + 1) is V11() real ext-real Element of REAL
||.(x - xp).|| * (xp to_power (e + 1)) is V11() real ext-real Element of REAL
xp * ||.(x - xp).|| is V11() real ext-real Element of REAL
xp * (||.(x - xp).|| * (xp to_power e)) is V11() real ext-real Element of REAL
(n0 . x) - (n0 . xp) is Element of the carrier of X
- (n0 . xp) is Element of the carrier of X
K342(X,(n0 . x),(- (n0 . xp))) is Element of the carrier of X
||.((n0 . x) - (n0 . xp)).|| is V11() real ext-real non negative Element of REAL
xp * (xp to_power e) is V11() real ext-real Element of REAL
||.(x - xp).|| * (xp * (xp to_power e)) is V11() real ext-real Element of REAL
xp to_power 1 is V11() real ext-real Element of REAL
(xp to_power 1) * (xp to_power e) is V11() real ext-real Element of REAL
||.(x - xp).|| * ((xp to_power 1) * (xp to_power e)) is V11() real ext-real Element of REAL
||.(x - xp).|| * 1 is V11() real ext-real non negative Element of REAL
xp to_power 0 is V11() real ext-real Element of REAL
||.(x - xp).|| * (xp to_power 0) is V11() real ext-real Element of REAL
e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
xp to_power e is V11() real ext-real Element of REAL
||.(x - xp).|| * (xp to_power e) is V11() real ext-real Element of REAL
e 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
xp to_power n is V11() real ext-real Element of REAL
||.(x - xp).|| * (xp to_power n) is V11() real ext-real Element of REAL
abs (||.(x - xp).|| * (xp to_power n)) is V11() real ext-real Element of REAL
x is Element of the carrier of X
n0 . x is Element of the carrier of X
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
f 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 epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
iter (f,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 Element of the carrier of X
(iter (f,n0)) . xp is Element of the carrier of X
x is Element of the carrier of X
f . x is Element of the carrier of X
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
iter (f,n) 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))
(iter (f,n)) . x is Element of the carrier of X
n + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
iter (f,(n + 1)) 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))
(iter (f,(n + 1))) . x is Element of the carrier of X
f * (iter (f,n)) 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))
(f * (iter (f,n))) . x is Element of the carrier of X
iter (f,0) 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))
(iter (f,0)) . x is Element of the carrier of X
id the carrier of X is non empty Relation-like the carrier of X -defined the carrier of X -valued Function-like one-to-one total quasi_total Element of K6(K7( the carrier of X, the carrier of X))
(id the carrier of X) . x is Element of the carrier of X
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
iter (f,n) 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))
(iter (f,n)) . x is Element of the carrier of X
(iter (f,n0)) . x is Element of the carrier of X
f . xp is Element of the carrier of X
(iter (f,n0)) . (f . xp) is Element of the carrier of X
(iter (f,n0)) * f 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))
((iter (f,n0)) * f) . xp is Element of the carrier of X
n0 + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
iter (f,(n0 + 1)) 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))
(iter (f,(n0 + 1))) . xp is Element of the carrier of X
f * (iter (f,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))
(f * (iter (f,n0))) . xp is Element of the carrier of X
X is V11() real ext-real set
n0 is V11() real ext-real set
f is V11() real ext-real set