:: NCFCONT2 semantic presentation

REAL is non empty V47() V48() V49() V53() V54() set
NAT is non empty V4() V5() V6() 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 V4() V5() V6() 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
K7(NAT,COMPLEX) is complex-valued set
K6(K7(NAT,COMPLEX)) is set
K373() is non empty set
K7(K373(),K373()) is set
K7(K7(K373(),K373()),K373()) is set
K6(K7(K7(K373(),K373()),K373())) is set
K7(COMPLEX,K373()) is set
K7(K7(COMPLEX,K373()),K373()) is set
K6(K7(K7(COMPLEX,K373()),K373())) is set
K379() is non empty strict CLSStruct
the carrier of K379() is non empty set
K6( the carrier of K379()) is set
K383() is Element of K6( the carrier of K379())
K7(K383(),K383()) is set
K7(K7(K383(),K383()),COMPLEX) is complex-valued set
K6(K7(K7(K383(),K383()),COMPLEX)) is set
K391() is Element of K6( the carrier of K379())
K7(K391(),REAL) is complex-valued ext-real-valued real-valued set
K6(K7(K391(),REAL)) is set
{} is empty V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative Function-like functional V47() V48() V49() V50() V51() V52() V53() set
1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
0 is empty V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
- 1 is V11() V12() ext-real non positive Element of REAL
1r is V11() Element of COMPLEX
- 1r is V11() Element of COMPLEX
2 is non empty V4() V5() V6() V10() V11() V12() 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 V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
the carrier of f is non empty set
n0 is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
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
n0 is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
the carrier of n0 is non empty set
f is non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like NORMSTR
the carrier of f is non empty set
K7( the carrier of n0, the carrier of f) is set
K6(K7( the carrier of n0, the carrier of f)) is set
f is non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like NORMSTR
the carrier of f is non empty set
n0 is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
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 V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
the carrier of f is non empty set
K7( the carrier of f,COMPLEX) is complex-valued set
K6(K7( the carrier of f,COMPLEX)) is set
f is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
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
f is non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like NORMSTR
the carrier of f is non empty set
K7( the carrier of f,COMPLEX) is complex-valued set
K6(K7( the carrier of f,COMPLEX)) is set
X is set
f is set
n0 is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
the carrier of n0 is non empty set
xp is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
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() V12() ext-real Element of REAL
xp is V11() V12() ext-real Element of REAL
x is Element of the carrier of n0
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
K340(n0,x,(- e)) is Element of the carrier of n0
||.(x - e).|| is V11() V12() ext-real Element of REAL
x /. x is Element of the carrier of xp
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
K340(xp,(x /. x),(- (x /. e))) is Element of the carrier of xp
||.((x /. x) - (x /. e)).|| is V11() V12() ext-real Element of REAL
X is set
f is set
n0 is non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like NORMSTR
the carrier of n0 is non empty set
xp is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
the carrier of xp is non empty set
K7( the carrier of xp, the carrier of n0) is set
K6(K7( the carrier of xp, the carrier of n0)) is set
x is Relation-like the carrier of xp -defined the carrier of n0 -valued Function-like Element of K6(K7( the carrier of xp, the carrier of n0))
dom x is Element of K6( the carrier of xp)
K6( the carrier of xp) is set
n is V11() V12() ext-real Element of REAL
xp is V11() V12() ext-real 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
K340(xp,x,(- e)) is Element of the carrier of xp
||.(x - e).|| is V11() V12() ext-real Element of REAL
x /. x is Element of the carrier of n0
x /. e is Element of the carrier of n0
(x /. x) - (x /. e) is Element of the carrier of n0
- (x /. e) is Element of the carrier of n0
K340(n0,(x /. x),(- (x /. e))) is Element of the carrier of n0
||.((x /. x) - (x /. e)).|| is V11() V12() ext-real Element of REAL
X is set
f is set
n0 is non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like NORMSTR
the carrier of n0 is non empty set
xp is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
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() V12() ext-real Element of REAL
xp is V11() V12() ext-real Element of REAL
x is Element of the carrier of n0
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
K340(n0,x,(- e)) is Element of the carrier of n0
||.(x - e).|| is V11() V12() ext-real Element of REAL
x /. x is Element of the carrier of xp
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
K340(xp,(x /. x),(- (x /. e))) is Element of the carrier of xp
||.((x /. x) - (x /. e)).|| is V11() V12() ext-real Element of REAL
X is set
f is set
X /\ f is set
n0 is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
the carrier of n0 is non empty set
xp is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
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() V12() ext-real Element of REAL
xp / 2 is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
e is V11() V12() ext-real Element of REAL
min (x,e) is V11() V12() ext-real Element of REAL
n is V11() V12() ext-real Element of REAL
l is Element of the carrier of n0
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
K340(n0,l,(- k1)) is Element of the carrier of n0
||.(l - k1).|| is V11() V12() ext-real Element of REAL
(x + n) /. l is Element of the carrier of xp
(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
K340(xp,((x + n) /. l),(- ((x + n) /. k1))) is Element of the carrier of xp
||.(((x + n) /. l) - ((x + n) /. k1)).|| is V11() V12() ext-real 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
K340(xp,(n /. l),(- (n /. k1))) is Element of the carrier of xp
||.((n /. l) - (n /. k1)).|| is V11() V12() ext-real 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
K340(xp,(x /. l),(- (x /. k1))) is Element of the carrier of xp
||.((x /. l) - (x /. k1)).|| is V11() V12() ext-real Element of REAL
(xp / 2) + (xp / 2) is V11() V12() ext-real Element of REAL
||.((x /. l) - (x /. k1)).|| + ||.((n /. l) - (n /. k1)).|| is V11() V12() ext-real 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() V12() ext-real 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
K340(xp,((x /. l) + (n /. l)),(- ((x + n) /. k1))) is Element of the carrier of xp
||.(((x /. l) + (n /. l)) - ((x + n) /. k1)).|| is V11() V12() ext-real 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
K340(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() V12() ext-real Element of REAL
(n /. l) - ((x /. k1) + (n /. k1)) is Element of the carrier of xp
K340(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() V12() ext-real Element of REAL
(n /. l) - (x /. k1) is Element of the carrier of xp
K340(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
K340(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() V12() ext-real 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
K340(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() V12() ext-real 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() V12() ext-real Element of REAL
X is set
f is set
X /\ f is set
n0 is non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like NORMSTR
the carrier of n0 is non empty set
xp is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
the carrier of xp is non empty set
K7( the carrier of xp, the carrier of n0) is set
K6(K7( the carrier of xp, the carrier of n0)) is set
x is Relation-like the carrier of xp -defined the carrier of n0 -valued Function-like Element of K6(K7( the carrier of xp, the carrier of n0))
n is Relation-like the carrier of xp -defined the carrier of n0 -valued Function-like Element of K6(K7( the carrier of xp, the carrier of n0))
x + n is Relation-like the carrier of xp -defined the carrier of n0 -valued Function-like Element of K6(K7( the carrier of xp, the carrier of n0))
dom n is Element of K6( the carrier of xp)
K6( the carrier of xp) is set
dom x is Element of K6( the carrier of xp)
(dom x) /\ (dom n) is Element of K6( the carrier of xp)
dom (x + n) is Element of K6( the carrier of xp)
xp is V11() V12() ext-real Element of REAL
xp / 2 is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
e is V11() V12() ext-real Element of REAL
min (x,e) is V11() V12() ext-real Element of REAL
n is V11() V12() ext-real Element of REAL
l is Element of the carrier of xp
k1 is Element of the carrier of xp
l - k1 is Element of the carrier of xp
- k1 is Element of the carrier of xp
K340(xp,l,(- k1)) is Element of the carrier of xp
||.(l - k1).|| is V11() V12() ext-real Element of REAL
(x + n) /. l is Element of the carrier of n0
(x + n) /. k1 is Element of the carrier of n0
((x + n) /. l) - ((x + n) /. k1) is Element of the carrier of n0
- ((x + n) /. k1) is Element of the carrier of n0
K340(n0,((x + n) /. l),(- ((x + n) /. k1))) is Element of the carrier of n0
||.(((x + n) /. l) - ((x + n) /. k1)).|| is V11() V12() ext-real Element of REAL
n /. l is Element of the carrier of n0
n /. k1 is Element of the carrier of n0
(n /. l) - (n /. k1) is Element of the carrier of n0
- (n /. k1) is Element of the carrier of n0
K340(n0,(n /. l),(- (n /. k1))) is Element of the carrier of n0
||.((n /. l) - (n /. k1)).|| is V11() V12() ext-real Element of REAL
x /. l is Element of the carrier of n0
x /. k1 is Element of the carrier of n0
(x /. l) - (x /. k1) is Element of the carrier of n0
- (x /. k1) is Element of the carrier of n0
K340(n0,(x /. l),(- (x /. k1))) is Element of the carrier of n0
||.((x /. l) - (x /. k1)).|| is V11() V12() ext-real Element of REAL
(xp / 2) + (xp / 2) is V11() V12() ext-real Element of REAL
||.((x /. l) - (x /. k1)).|| + ||.((n /. l) - (n /. k1)).|| is V11() V12() ext-real Element of REAL
((x /. l) - (x /. k1)) + ((n /. l) - (n /. k1)) is Element of the carrier of n0
||.(((x /. l) - (x /. k1)) + ((n /. l) - (n /. k1))).|| is V11() V12() ext-real Element of REAL
(x /. l) + (n /. l) is Element of the carrier of n0
((x /. l) + (n /. l)) - ((x + n) /. k1) is Element of the carrier of n0
K340(n0,((x /. l) + (n /. l)),(- ((x + n) /. k1))) is Element of the carrier of n0
||.(((x /. l) + (n /. l)) - ((x + n) /. k1)).|| is V11() V12() ext-real Element of REAL
(x /. k1) + (n /. k1) is Element of the carrier of n0
((x /. l) + (n /. l)) - ((x /. k1) + (n /. k1)) is Element of the carrier of n0
- ((x /. k1) + (n /. k1)) is Element of the carrier of n0
K340(n0,((x /. l) + (n /. l)),(- ((x /. k1) + (n /. k1)))) is Element of the carrier of n0
||.(((x /. l) + (n /. l)) - ((x /. k1) + (n /. k1))).|| is V11() V12() ext-real Element of REAL
(n /. l) - ((x /. k1) + (n /. k1)) is Element of the carrier of n0
K340(n0,(n /. l),(- ((x /. k1) + (n /. k1)))) is Element of the carrier of n0
(x /. l) + ((n /. l) - ((x /. k1) + (n /. k1))) is Element of the carrier of n0
||.((x /. l) + ((n /. l) - ((x /. k1) + (n /. k1)))).|| is V11() V12() ext-real Element of REAL
(n /. l) - (x /. k1) is Element of the carrier of n0
K340(n0,(n /. l),(- (x /. k1))) is Element of the carrier of n0
((n /. l) - (x /. k1)) - (n /. k1) is Element of the carrier of n0
K340(n0,((n /. l) - (x /. k1)),(- (n /. k1))) is Element of the carrier of n0
(x /. l) + (((n /. l) - (x /. k1)) - (n /. k1)) is Element of the carrier of n0
||.((x /. l) + (((n /. l) - (x /. k1)) - (n /. k1))).|| is V11() V12() ext-real Element of REAL
(- (x /. k1)) + (n /. l) is Element of the carrier of n0
((- (x /. k1)) + (n /. l)) - (n /. k1) is Element of the carrier of n0
K340(n0,((- (x /. k1)) + (n /. l)),(- (n /. k1))) is Element of the carrier of n0
(x /. l) + (((- (x /. k1)) + (n /. l)) - (n /. k1)) is Element of the carrier of n0
||.((x /. l) + (((- (x /. k1)) + (n /. l)) - (n /. k1))).|| is V11() V12() ext-real Element of REAL
(- (x /. k1)) + ((n /. l) - (n /. k1)) is Element of the carrier of n0
(x /. l) + ((- (x /. k1)) + ((n /. l) - (n /. k1))) is Element of the carrier of n0
||.((x /. l) + ((- (x /. k1)) + ((n /. l) - (n /. k1)))).|| is V11() V12() ext-real Element of REAL
X is set
f is set
X /\ f is set
n0 is non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like NORMSTR
the carrier of n0 is non empty set
xp is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
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() V12() ext-real Element of REAL
xp / 2 is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
e is V11() V12() ext-real Element of REAL
min (x,e) is V11() V12() ext-real Element of REAL
n is V11() V12() ext-real Element of REAL
l is Element of the carrier of n0
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
K340(n0,l,(- k1)) is Element of the carrier of n0
||.(l - k1).|| is V11() V12() ext-real Element of REAL
(x + n) /. l is Element of the carrier of xp
(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
K340(xp,((x + n) /. l),(- ((x + n) /. k1))) is Element of the carrier of xp
||.(((x + n) /. l) - ((x + n) /. k1)).|| is V11() V12() ext-real 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
K340(xp,(n /. l),(- (n /. k1))) is Element of the carrier of xp
||.((n /. l) - (n /. k1)).|| is V11() V12() ext-real 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
K340(xp,(x /. l),(- (x /. k1))) is Element of the carrier of xp
||.((x /. l) - (x /. k1)).|| is V11() V12() ext-real Element of REAL
(xp / 2) + (xp / 2) is V11() V12() ext-real Element of REAL
||.((x /. l) - (x /. k1)).|| + ||.((n /. l) - (n /. k1)).|| is V11() V12() ext-real 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() V12() ext-real 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
K340(xp,((x /. l) + (n /. l)),(- ((x + n) /. k1))) is Element of the carrier of xp
||.(((x /. l) + (n /. l)) - ((x + n) /. k1)).|| is V11() V12() ext-real 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
K340(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() V12() ext-real Element of REAL
(n /. l) - ((x /. k1) + (n /. k1)) is Element of the carrier of xp
K340(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() V12() ext-real Element of REAL
(n /. l) - (x /. k1) is Element of the carrier of xp
K340(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
K340(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() V12() ext-real 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
K340(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() V12() ext-real 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() V12() ext-real Element of REAL
X is set
f is set
X /\ f is set
n0 is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
the carrier of n0 is non empty set
xp is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
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() V12() ext-real Element of REAL
xp / 2 is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
e is V11() V12() ext-real Element of REAL
min (x,e) is V11() V12() ext-real Element of REAL
n is V11() V12() ext-real Element of REAL
l is Element of the carrier of n0
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
K340(n0,l,(- k1)) is Element of the carrier of n0
||.(l - k1).|| is V11() V12() ext-real Element of REAL
(x - n) /. l is Element of the carrier of xp
(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
K340(xp,((x - n) /. l),(- ((x - n) /. k1))) is Element of the carrier of xp
||.(((x - n) /. l) - ((x - n) /. k1)).|| is V11() V12() ext-real 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
K340(xp,(n /. l),(- (n /. k1))) is Element of the carrier of xp
||.((n /. l) - (n /. k1)).|| is V11() V12() ext-real 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
K340(xp,(x /. l),(- (x /. k1))) is Element of the carrier of xp
||.((x /. l) - (x /. k1)).|| is V11() V12() ext-real Element of REAL
(xp / 2) + (xp / 2) is V11() V12() ext-real Element of REAL
||.((x /. l) - (x /. k1)).|| + ||.((n /. l) - (n /. k1)).|| is V11() V12() ext-real 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
K340(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() V12() ext-real Element of REAL
(x /. l) - (n /. l) is Element of the carrier of xp
- (n /. l) is Element of the carrier of xp
K340(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
K340(xp,((x /. l) - (n /. l)),(- ((x - n) /. k1))) is Element of the carrier of xp
||.(((x /. l) - (n /. l)) - ((x - n) /. k1)).|| is V11() V12() ext-real Element of REAL
(x /. k1) - (n /. k1) is Element of the carrier of xp
K340(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
K340(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() V12() ext-real 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
K340(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() V12() ext-real 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
K340(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
K340(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() V12() ext-real 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
K340(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() V12() ext-real Element of REAL
X is set
f is set
X /\ f is set
n0 is non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like NORMSTR
the carrier of n0 is non empty set
xp is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
the carrier of xp is non empty set
K7( the carrier of xp, the carrier of n0) is set
K6(K7( the carrier of xp, the carrier of n0)) is set
x is Relation-like the carrier of xp -defined the carrier of n0 -valued Function-like Element of K6(K7( the carrier of xp, the carrier of n0))
n is Relation-like the carrier of xp -defined the carrier of n0 -valued Function-like Element of K6(K7( the carrier of xp, the carrier of n0))
x - n is Relation-like the carrier of xp -defined the carrier of n0 -valued Function-like Element of K6(K7( the carrier of xp, the carrier of n0))
dom n is Element of K6( the carrier of xp)
K6( the carrier of xp) is set
dom x is Element of K6( the carrier of xp)
(dom x) /\ (dom n) is Element of K6( the carrier of xp)
dom (x - n) is Element of K6( the carrier of xp)
xp is V11() V12() ext-real Element of REAL
xp / 2 is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
e is V11() V12() ext-real Element of REAL
min (x,e) is V11() V12() ext-real Element of REAL
n is V11() V12() ext-real Element of REAL
l is Element of the carrier of xp
k1 is Element of the carrier of xp
l - k1 is Element of the carrier of xp
- k1 is Element of the carrier of xp
K340(xp,l,(- k1)) is Element of the carrier of xp
||.(l - k1).|| is V11() V12() ext-real Element of REAL
(x - n) /. l is Element of the carrier of n0
(x - n) /. k1 is Element of the carrier of n0
((x - n) /. l) - ((x - n) /. k1) is Element of the carrier of n0
- ((x - n) /. k1) is Element of the carrier of n0
K340(n0,((x - n) /. l),(- ((x - n) /. k1))) is Element of the carrier of n0
||.(((x - n) /. l) - ((x - n) /. k1)).|| is V11() V12() ext-real Element of REAL
n /. l is Element of the carrier of n0
n /. k1 is Element of the carrier of n0
(n /. l) - (n /. k1) is Element of the carrier of n0
- (n /. k1) is Element of the carrier of n0
K340(n0,(n /. l),(- (n /. k1))) is Element of the carrier of n0
||.((n /. l) - (n /. k1)).|| is V11() V12() ext-real Element of REAL
x /. l is Element of the carrier of n0
x /. k1 is Element of the carrier of n0
(x /. l) - (x /. k1) is Element of the carrier of n0
- (x /. k1) is Element of the carrier of n0
K340(n0,(x /. l),(- (x /. k1))) is Element of the carrier of n0
||.((x /. l) - (x /. k1)).|| is V11() V12() ext-real Element of REAL
(xp / 2) + (xp / 2) is V11() V12() ext-real Element of REAL
||.((x /. l) - (x /. k1)).|| + ||.((n /. l) - (n /. k1)).|| is V11() V12() ext-real Element of REAL
((x /. l) - (x /. k1)) - ((n /. l) - (n /. k1)) is Element of the carrier of n0
- ((n /. l) - (n /. k1)) is Element of the carrier of n0
K340(n0,((x /. l) - (x /. k1)),(- ((n /. l) - (n /. k1)))) is Element of the carrier of n0
||.(((x /. l) - (x /. k1)) - ((n /. l) - (n /. k1))).|| is V11() V12() ext-real Element of REAL
(x /. l) - (n /. l) is Element of the carrier of n0
- (n /. l) is Element of the carrier of n0
K340(n0,(x /. l),(- (n /. l))) is Element of the carrier of n0
((x /. l) - (n /. l)) - ((x - n) /. k1) is Element of the carrier of n0
K340(n0,((x /. l) - (n /. l)),(- ((x - n) /. k1))) is Element of the carrier of n0
||.(((x /. l) - (n /. l)) - ((x - n) /. k1)).|| is V11() V12() ext-real Element of REAL
(x /. k1) - (n /. k1) is Element of the carrier of n0
K340(n0,(x /. k1),(- (n /. k1))) is Element of the carrier of n0
((x /. l) - (n /. l)) - ((x /. k1) - (n /. k1)) is Element of the carrier of n0
- ((x /. k1) - (n /. k1)) is Element of the carrier of n0
K340(n0,((x /. l) - (n /. l)),(- ((x /. k1) - (n /. k1)))) is Element of the carrier of n0
||.(((x /. l) - (n /. l)) - ((x /. k1) - (n /. k1))).|| is V11() V12() ext-real Element of REAL
(n /. l) + ((x /. k1) - (n /. k1)) is Element of the carrier of n0
(x /. l) - ((n /. l) + ((x /. k1) - (n /. k1))) is Element of the carrier of n0
- ((n /. l) + ((x /. k1) - (n /. k1))) is Element of the carrier of n0
K340(n0,(x /. l),(- ((n /. l) + ((x /. k1) - (n /. k1))))) is Element of the carrier of n0
||.((x /. l) - ((n /. l) + ((x /. k1) - (n /. k1)))).|| is V11() V12() ext-real Element of REAL
(x /. k1) + (n /. l) is Element of the carrier of n0
((x /. k1) + (n /. l)) - (n /. k1) is Element of the carrier of n0
K340(n0,((x /. k1) + (n /. l)),(- (n /. k1))) is Element of the carrier of n0
(x /. l) - (((x /. k1) + (n /. l)) - (n /. k1)) is Element of the carrier of n0
- (((x /. k1) + (n /. l)) - (n /. k1)) is Element of the carrier of n0
K340(n0,(x /. l),(- (((x /. k1) + (n /. l)) - (n /. k1)))) is Element of the carrier of n0
||.((x /. l) - (((x /. k1) + (n /. l)) - (n /. k1))).|| is V11() V12() ext-real Element of REAL
(x /. k1) + ((n /. l) - (n /. k1)) is Element of the carrier of n0
(x /. l) - ((x /. k1) + ((n /. l) - (n /. k1))) is Element of the carrier of n0
- ((x /. k1) + ((n /. l) - (n /. k1))) is Element of the carrier of n0
K340(n0,(x /. l),(- ((x /. k1) + ((n /. l) - (n /. k1))))) is Element of the carrier of n0
||.((x /. l) - ((x /. k1) + ((n /. l) - (n /. k1)))).|| is V11() V12() ext-real Element of REAL
X is set
f is set
X /\ f is set
n0 is non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like NORMSTR
the carrier of n0 is non empty set
xp is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
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() V12() ext-real Element of REAL
xp / 2 is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
e is V11() V12() ext-real Element of REAL
min (x,e) is V11() V12() ext-real Element of REAL
n is V11() V12() ext-real Element of REAL
l is Element of the carrier of n0
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
K340(n0,l,(- k1)) is Element of the carrier of n0
||.(l - k1).|| is V11() V12() ext-real Element of REAL
(x - n) /. l is Element of the carrier of xp
(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
K340(xp,((x - n) /. l),(- ((x - n) /. k1))) is Element of the carrier of xp
||.(((x - n) /. l) - ((x - n) /. k1)).|| is V11() V12() ext-real 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
K340(xp,(n /. l),(- (n /. k1))) is Element of the carrier of xp
||.((n /. l) - (n /. k1)).|| is V11() V12() ext-real 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
K340(xp,(x /. l),(- (x /. k1))) is Element of the carrier of xp
||.((x /. l) - (x /. k1)).|| is V11() V12() ext-real Element of REAL
(xp / 2) + (xp / 2) is V11() V12() ext-real Element of REAL
||.((x /. l) - (x /. k1)).|| + ||.((n /. l) - (n /. k1)).|| is V11() V12() ext-real 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
K340(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() V12() ext-real Element of REAL
(x /. l) - (n /. l) is Element of the carrier of xp
- (n /. l) is Element of the carrier of xp
K340(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
K340(xp,((x /. l) - (n /. l)),(- ((x - n) /. k1))) is Element of the carrier of xp
||.(((x /. l) - (n /. l)) - ((x - n) /. k1)).|| is V11() V12() ext-real Element of REAL
(x /. k1) - (n /. k1) is Element of the carrier of xp
K340(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
K340(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() V12() ext-real 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
K340(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() V12() ext-real 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
K340(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
K340(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() V12() ext-real 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
K340(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() V12() ext-real Element of REAL
X is set
f is V11() set
n0 is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
the carrier of n0 is non empty set
xp is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
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() V12() ext-real Element of REAL
xp is V11() V12() ext-real Element of REAL
x is V11() V12() 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
K340(n0,e,(- n)) is Element of the carrier of n0
||.(e - n).|| is V11() V12() ext-real 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
K340(xp,((f (#) x) /. e),(- ((f (#) x) /. n))) is Element of the carrier of xp
||.(((f (#) x) /. e) - ((f (#) x) /. n)).|| is V11() V12() ext-real Element of REAL
x /. e is Element of the carrier of xp
f * (x /. e) is Element of the carrier of xp
(f * (x /. e)) - ((f (#) x) /. n) is Element of the carrier of xp
K340(xp,(f * (x /. e)),(- ((f (#) x) /. n))) is Element of the carrier of xp
||.((f * (x /. e)) - ((f (#) x) /. n)).|| is V11() V12() ext-real Element of REAL
0. xp is V88(xp) Element of the carrier of xp
(0. xp) - ((f (#) x) /. n) is Element of the carrier of xp
K340(xp,(0. xp),(- ((f (#) x) /. n))) is Element of the carrier of xp
||.((0. xp) - ((f (#) x) /. n)).|| is V11() V12() ext-real Element of REAL
x /. n is Element of the carrier of xp
f * (x /. n) is Element of the carrier of xp
(0. xp) - (f * (x /. n)) is Element of the carrier of xp
- (f * (x /. n)) is Element of the carrier of xp
K340(xp,(0. xp),(- (f * (x /. n)))) is Element of the carrier of xp
||.((0. xp) - (f * (x /. n))).|| is V11() V12() ext-real Element of REAL
(0. xp) - (0. xp) is Element of the carrier of xp
- (0. xp) is Element of the carrier of xp
K340(xp,(0. xp),(- (0. xp))) is Element of the carrier of xp
||.((0. xp) - (0. xp)).|| is V11() V12() ext-real Element of REAL
||.(0. xp).|| is V11() V12() ext-real Element of REAL
|.f.| is V11() V12() ext-real Element of REAL
n is V11() V12() ext-real Element of REAL
n / |.f.| is V11() V12() ext-real Element of REAL
xp is V11() V12() ext-real Element of REAL
x is V11() V12() 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
K340(n0,e,(- n)) is Element of the carrier of n0
||.(e - n).|| is V11() V12() ext-real 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
K340(xp,((f (#) x) /. e),(- ((f (#) x) /. n))) is Element of the carrier of xp
||.(((f (#) x) /. e) - ((f (#) x) /. n)).|| is V11() V12() ext-real Element of REAL
x /. e is Element of the carrier of xp
f * (x /. e) is Element of the carrier of xp
(f * (x /. e)) - ((f (#) x) /. n) is Element of the carrier of xp
K340(xp,(f * (x /. e)),(- ((f (#) x) /. n))) is Element of the carrier of xp
||.((f * (x /. e)) - ((f (#) x) /. n)).|| is V11() V12() ext-real Element of REAL
x /. n 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
K340(xp,(f * (x /. e)),(- (f * (x /. n)))) is Element of the carrier of xp
||.((f * (x /. e)) - (f * (x /. n))).|| is V11() V12() ext-real Element of REAL
(x /. e) - (x /. n) is Element of the carrier of xp
- (x /. n) is Element of the carrier of xp
K340(xp,(x /. e),(- (x /. n))) is Element of the carrier of xp
f * ((x /. e) - (x /. n)) is Element of the carrier of xp
||.(f * ((x /. e) - (x /. n))).|| is V11() V12() ext-real Element of REAL
||.((x /. e) - (x /. n)).|| is V11() V12() ext-real Element of REAL
|.f.| * ||.((x /. e) - (x /. n)).|| is V11() V12() ext-real Element of REAL
(n / |.f.|) * |.f.| is V11() V12() ext-real Element of REAL
n is V11() V12() ext-real Element of REAL
X is set
f is V11() V12() ext-real Element of REAL
n0 is non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like NORMSTR
the carrier of n0 is non empty set
xp is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
the carrier of xp is non empty set
K7( the carrier of xp, the carrier of n0) is set
K6(K7( the carrier of xp, the carrier of n0)) is set
x is Relation-like the carrier of xp -defined the carrier of n0 -valued Function-like Element of K6(K7( the carrier of xp, the carrier of n0))
f (#) x is Relation-like the carrier of xp -defined the carrier of n0 -valued Function-like Element of K6(K7( the carrier of xp, the carrier of n0))
dom x is Element of K6( the carrier of xp)
K6( the carrier of xp) is set
dom (f (#) x) is Element of K6( the carrier of xp)
n is V11() V12() ext-real Element of REAL
xp is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
e is Element of the carrier of xp
n is Element of the carrier of xp
e - n is Element of the carrier of xp
- n is Element of the carrier of xp
K340(xp,e,(- n)) is Element of the carrier of xp
||.(e - n).|| is V11() V12() ext-real Element of REAL
(f (#) x) /. e is Element of the carrier of n0
(f (#) x) /. n is Element of the carrier of n0
((f (#) x) /. e) - ((f (#) x) /. n) is Element of the carrier of n0
- ((f (#) x) /. n) is Element of the carrier of n0
K340(n0,((f (#) x) /. e),(- ((f (#) x) /. n))) is Element of the carrier of n0
||.(((f (#) x) /. e) - ((f (#) x) /. n)).|| is V11() V12() ext-real Element of REAL
x /. e is Element of the carrier of n0
f * (x /. e) is Element of the carrier of n0
(f * (x /. e)) - ((f (#) x) /. n) is Element of the carrier of n0
K340(n0,(f * (x /. e)),(- ((f (#) x) /. n))) is Element of the carrier of n0
||.((f * (x /. e)) - ((f (#) x) /. n)).|| is V11() V12() ext-real Element of REAL
0. n0 is V88(n0) Element of the carrier of n0
(0. n0) - ((f (#) x) /. n) is Element of the carrier of n0
K340(n0,(0. n0),(- ((f (#) x) /. n))) is Element of the carrier of n0
||.((0. n0) - ((f (#) x) /. n)).|| is V11() V12() ext-real Element of REAL
x /. n is Element of the carrier of n0
f * (x /. n) is Element of the carrier of n0
(0. n0) - (f * (x /. n)) is Element of the carrier of n0
- (f * (x /. n)) is Element of the carrier of n0
K340(n0,(0. n0),(- (f * (x /. n)))) is Element of the carrier of n0
||.((0. n0) - (f * (x /. n))).|| is V11() V12() ext-real Element of REAL
(0. n0) - (0. n0) is Element of the carrier of n0
- (0. n0) is Element of the carrier of n0
K340(n0,(0. n0),(- (0. n0))) is Element of the carrier of n0
||.((0. n0) - (0. n0)).|| is V11() V12() ext-real Element of REAL
||.(0. n0).|| is V11() V12() ext-real Element of REAL
abs f is V11() V12() ext-real Element of REAL
n is V11() V12() ext-real Element of REAL
n / (abs f) is V11() V12() ext-real Element of REAL
xp is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
e is Element of the carrier of xp
n is Element of the carrier of xp
e - n is Element of the carrier of xp
- n is Element of the carrier of xp
K340(xp,e,(- n)) is Element of the carrier of xp
||.(e - n).|| is V11() V12() ext-real Element of REAL
(f (#) x) /. e is Element of the carrier of n0
(f (#) x) /. n is Element of the carrier of n0
((f (#) x) /. e) - ((f (#) x) /. n) is Element of the carrier of n0
- ((f (#) x) /. n) is Element of the carrier of n0
K340(n0,((f (#) x) /. e),(- ((f (#) x) /. n))) is Element of the carrier of n0
||.(((f (#) x) /. e) - ((f (#) x) /. n)).|| is V11() V12() ext-real Element of REAL
x /. e is Element of the carrier of n0
f * (x /. e) is Element of the carrier of n0
(f * (x /. e)) - ((f (#) x) /. n) is Element of the carrier of n0
K340(n0,(f * (x /. e)),(- ((f (#) x) /. n))) is Element of the carrier of n0
||.((f * (x /. e)) - ((f (#) x) /. n)).|| is V11() V12() ext-real Element of REAL
x /. n is Element of the carrier of n0
f * (x /. n) is Element of the carrier of n0
(f * (x /. e)) - (f * (x /. n)) is Element of the carrier of n0
- (f * (x /. n)) is Element of the carrier of n0
K340(n0,(f * (x /. e)),(- (f * (x /. n)))) is Element of the carrier of n0
||.((f * (x /. e)) - (f * (x /. n))).|| is V11() V12() ext-real Element of REAL
(x /. e) - (x /. n) is Element of the carrier of n0
- (x /. n) is Element of the carrier of n0
K340(n0,(x /. e),(- (x /. n))) is Element of the carrier of n0
f * ((x /. e) - (x /. n)) is Element of the carrier of n0
||.(f * ((x /. e) - (x /. n))).|| is V11() V12() ext-real Element of REAL
||.((x /. e) - (x /. n)).|| is V11() V12() ext-real Element of REAL
(abs f) * ||.((x /. e) - (x /. n)).|| is V11() V12() ext-real Element of REAL
(n / (abs f)) * (abs f) is V11() V12() ext-real Element of REAL
n is V11() V12() ext-real Element of REAL
X is set
f is V11() set
n0 is non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like NORMSTR
the carrier of n0 is non empty set
xp is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
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() V12() ext-real Element of REAL
xp is V11() V12() ext-real Element of REAL
x is V11() V12() 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
K340(n0,e,(- n)) is Element of the carrier of n0
||.(e - n).|| is V11() V12() ext-real 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
K340(xp,((f (#) x) /. e),(- ((f (#) x) /. n))) is Element of the carrier of xp
||.(((f (#) x) /. e) - ((f (#) x) /. n)).|| is V11() V12() ext-real Element of REAL
x /. e is Element of the carrier of xp
f * (x /. e) is Element of the carrier of xp
(f * (x /. e)) - ((f (#) x) /. n) is Element of the carrier of xp
K340(xp,(f * (x /. e)),(- ((f (#) x) /. n))) is Element of the carrier of xp
||.((f * (x /. e)) - ((f (#) x) /. n)).|| is V11() V12() ext-real Element of REAL
0. xp is V88(xp) Element of the carrier of xp
(0. xp) - ((f (#) x) /. n) is Element of the carrier of xp
K340(xp,(0. xp),(- ((f (#) x) /. n))) is Element of the carrier of xp
||.((0. xp) - ((f (#) x) /. n)).|| is V11() V12() ext-real Element of REAL
x /. n is Element of the carrier of xp
f * (x /. n) is Element of the carrier of xp
(0. xp) - (f * (x /. n)) is Element of the carrier of xp
- (f * (x /. n)) is Element of the carrier of xp
K340(xp,(0. xp),(- (f * (x /. n)))) is Element of the carrier of xp
||.((0. xp) - (f * (x /. n))).|| is V11() V12() ext-real Element of REAL
(0. xp) - (0. xp) is Element of the carrier of xp
- (0. xp) is Element of the carrier of xp
K340(xp,(0. xp),(- (0. xp))) is Element of the carrier of xp
||.((0. xp) - (0. xp)).|| is V11() V12() ext-real Element of REAL
||.(0. xp).|| is V11() V12() ext-real Element of REAL
|.f.| is V11() V12() ext-real Element of REAL
n is V11() V12() ext-real Element of REAL
n / |.f.| is V11() V12() ext-real Element of REAL
xp is V11() V12() ext-real Element of REAL
x is V11() V12() 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
K340(n0,e,(- n)) is Element of the carrier of n0
||.(e - n).|| is V11() V12() ext-real 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
K340(xp,((f (#) x) /. e),(- ((f (#) x) /. n))) is Element of the carrier of xp
||.(((f (#) x) /. e) - ((f (#) x) /. n)).|| is V11() V12() ext-real Element of REAL
x /. e is Element of the carrier of xp
f * (x /. e) is Element of the carrier of xp
(f * (x /. e)) - ((f (#) x) /. n) is Element of the carrier of xp
K340(xp,(f * (x /. e)),(- ((f (#) x) /. n))) is Element of the carrier of xp
||.((f * (x /. e)) - ((f (#) x) /. n)).|| is V11() V12() ext-real Element of REAL
x /. n 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
K340(xp,(f * (x /. e)),(- (f * (x /. n)))) is Element of the carrier of xp
||.((f * (x /. e)) - (f * (x /. n))).|| is V11() V12() ext-real Element of REAL
(x /. e) - (x /. n) is Element of the carrier of xp
- (x /. n) is Element of the carrier of xp
K340(xp,(x /. e),(- (x /. n))) is Element of the carrier of xp
f * ((x /. e) - (x /. n)) is Element of the carrier of xp
||.(f * ((x /. e) - (x /. n))).|| is V11() V12() ext-real Element of REAL
||.((x /. e) - (x /. n)).|| is V11() V12() ext-real Element of REAL
|.f.| * ||.((x /. e) - (x /. n)).|| is V11() V12() ext-real Element of REAL
(n / |.f.|) * |.f.| is V11() V12() ext-real Element of REAL
n is V11() V12() ext-real Element of REAL
X is set
f is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
the carrier of f is non empty set
n0 is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
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))
(- 1r) (#) 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 V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like NORMSTR
the carrier of f is non empty set
n0 is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
the carrier of n0 is non empty set
K7( the carrier of n0, the carrier of f) is set
K6(K7( the carrier of n0, the carrier of f)) is set
xp is Relation-like the carrier of n0 -defined the carrier of f -valued Function-like Element of K6(K7( the carrier of n0, the carrier of f))
- xp is Relation-like the carrier of n0 -defined the carrier of f -valued Function-like Element of K6(K7( the carrier of n0, the carrier of f))
(- 1) (#) xp is Relation-like the carrier of n0 -defined the carrier of f -valued Function-like Element of K6(K7( the carrier of n0, the carrier of f))
X is set
f is non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like NORMSTR
the carrier of f is non empty set
n0 is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
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))
(- 1r) (#) 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 V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
the carrier of f is non empty set
n0 is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
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() V12() ext-real Element of REAL
n is V11() V12() ext-real Element of REAL
xp is Element of the carrier of f
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
K340(f,xp,(- x)) is Element of the carrier of f
||.(xp - x).|| is V11() V12() ext-real Element of REAL
||.xp.|| /. xp is V11() V12() ext-real Element of REAL
||.xp.|| /. x is V11() V12() ext-real Element of REAL
(||.xp.|| /. xp) - (||.xp.|| /. x) is V11() V12() ext-real Element of REAL
abs ((||.xp.|| /. xp) - (||.xp.|| /. x)) is V11() V12() ext-real Element of REAL
||.xp.|| . xp is V11() V12() ext-real set
(||.xp.|| . xp) - (||.xp.|| /. x) is V11() V12() ext-real Element of REAL
abs ((||.xp.|| . xp) - (||.xp.|| /. x)) is V11() V12() ext-real Element of REAL
||.xp.|| . x is V11() V12() ext-real set
(||.xp.|| . xp) - (||.xp.|| . x) is V11() V12() ext-real set
abs ((||.xp.|| . xp) - (||.xp.|| . x)) is V11() V12() ext-real Element of REAL
xp /. xp is Element of the carrier of n0
||.(xp /. xp).|| is V11() V12() ext-real Element of REAL
||.(xp /. xp).|| - (||.xp.|| . x) is V11() V12() ext-real Element of REAL
abs (||.(xp /. xp).|| - (||.xp.|| . x)) is V11() V12() ext-real Element of REAL
xp /. x is Element of the carrier of n0
||.(xp /. x).|| is V11() V12() ext-real Element of REAL
||.(xp /. xp).|| - ||.(xp /. x).|| is V11() V12() ext-real Element of REAL
abs (||.(xp /. xp).|| - ||.(xp /. x).||) is V11() V12() 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
K340(n0,(xp /. xp),(- (xp /. x))) is Element of the carrier of n0
||.((xp /. xp) - (xp /. x)).|| is V11() V12() ext-real Element of REAL
X is set
f is non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like NORMSTR
the carrier of f is non empty set
n0 is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
the carrier of n0 is non empty set
K7( the carrier of n0, the carrier of f) is set
K6(K7( the carrier of n0, the carrier of f)) is set
xp is Relation-like the carrier of n0 -defined the carrier of f -valued Function-like Element of K6(K7( the carrier of n0, the carrier of f))
||.xp.|| is Relation-like the carrier of n0 -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of n0,REAL))
K7( the carrier of n0,REAL) is complex-valued ext-real-valued real-valued set
K6(K7( the carrier of n0,REAL)) is set
dom xp is Element of K6( the carrier of n0)
K6( the carrier of n0) is set
dom ||.xp.|| is Element of K6( the carrier of n0)
x is V11() V12() ext-real Element of REAL
n is V11() V12() ext-real Element of REAL
xp is Element of the carrier of n0
x is Element of the carrier of n0
xp - x is Element of the carrier of n0
- x is Element of the carrier of n0
K340(n0,xp,(- x)) is Element of the carrier of n0
||.(xp - x).|| is V11() V12() ext-real Element of REAL
||.xp.|| /. xp is V11() V12() ext-real Element of REAL
||.xp.|| /. x is V11() V12() ext-real Element of REAL
(||.xp.|| /. xp) - (||.xp.|| /. x) is V11() V12() ext-real Element of REAL
abs ((||.xp.|| /. xp) - (||.xp.|| /. x)) is V11() V12() ext-real Element of REAL
||.xp.|| . xp is V11() V12() ext-real set
(||.xp.|| . xp) - (||.xp.|| /. x) is V11() V12() ext-real Element of REAL
abs ((||.xp.|| . xp) - (||.xp.|| /. x)) is V11() V12() ext-real Element of REAL
||.xp.|| . x is V11() V12() ext-real set
(||.xp.|| . xp) - (||.xp.|| . x) is V11() V12() ext-real set
abs ((||.xp.|| . xp) - (||.xp.|| . x)) is V11() V12() ext-real Element of REAL
xp /. xp is Element of the carrier of f
||.(xp /. xp).|| is V11() V12() ext-real Element of REAL
||.(xp /. xp).|| - (||.xp.|| . x) is V11() V12() ext-real Element of REAL
abs (||.(xp /. xp).|| - (||.xp.|| . x)) is V11() V12() ext-real Element of REAL
xp /. x is Element of the carrier of f
||.(xp /. x).|| is V11() V12() ext-real Element of REAL
||.(xp /. xp).|| - ||.(xp /. x).|| is V11() V12() ext-real Element of REAL
abs (||.(xp /. xp).|| - ||.(xp /. x).||) is V11() V12() ext-real Element of REAL
(xp /. xp) - (xp /. x) is Element of the carrier of f
- (xp /. x) is Element of the carrier of f
K340(f,(xp /. xp),(- (xp /. x))) is Element of the carrier of f
||.((xp /. xp) - (xp /. x)).|| is V11() V12() ext-real Element of REAL
X is set
f is non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like NORMSTR
the carrier of f is non empty set
n0 is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
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() V12() ext-real Element of REAL
n is V11() V12() ext-real Element of REAL
xp is Element of the carrier of f
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
K340(f,xp,(- x)) is Element of the carrier of f
||.(xp - x).|| is V11() V12() ext-real Element of REAL
||.xp.|| /. xp is V11() V12() ext-real Element of REAL
||.xp.|| /. x is V11() V12() ext-real Element of REAL
(||.xp.|| /. xp) - (||.xp.|| /. x) is V11() V12() ext-real Element of REAL
abs ((||.xp.|| /. xp) - (||.xp.|| /. x)) is V11() V12() ext-real Element of REAL
||.xp.|| . xp is V11() V12() ext-real set
(||.xp.|| . xp) - (||.xp.|| /. x) is V11() V12() ext-real Element of REAL
abs ((||.xp.|| . xp) - (||.xp.|| /. x)) is V11() V12() ext-real Element of REAL
||.xp.|| . x is V11() V12() ext-real set
(||.xp.|| . xp) - (||.xp.|| . x) is V11() V12() ext-real set
abs ((||.xp.|| . xp) - (||.xp.|| . x)) is V11() V12() ext-real Element of REAL
xp /. xp is Element of the carrier of n0
||.(xp /. xp).|| is V11() V12() ext-real Element of REAL
||.(xp /. xp).|| - (||.xp.|| . x) is V11() V12() ext-real Element of REAL
abs (||.(xp /. xp).|| - (||.xp.|| . x)) is V11() V12() ext-real Element of REAL
xp /. x is Element of the carrier of n0
||.(xp /. x).|| is V11() V12() ext-real Element of REAL
||.(xp /. xp).|| - ||.(xp /. x).|| is V11() V12() ext-real Element of REAL
abs (||.(xp /. xp).|| - ||.(xp /. x).||) is V11() V12() 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
K340(n0,(xp /. xp),(- (xp /. x))) is Element of the carrier of n0
||.((xp /. xp) - (xp /. x)).|| is V11() V12() ext-real Element of REAL
X is set
f is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
the carrier of f is non empty set
n0 is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
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() V12() ext-real Element of REAL
xp is V11() V12() ext-real Element of REAL
x is V11() V12() 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
K340(f,e,(- x)) is Element of the carrier of f
||.(e - x).|| is V11() V12() ext-real 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
K340(n0,(xp /. e),(- (xp /. x))) is Element of the carrier of n0
||.((xp /. e) - (xp /. x)).|| is V11() V12() ext-real 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 V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like NORMSTR
the carrier of f is non empty set
n0 is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
the carrier of n0 is non empty set
K7( the carrier of n0, the carrier of f) is set
K6(K7( the carrier of n0, the carrier of f)) is set
xp is Relation-like the carrier of n0 -defined the carrier of f -valued Function-like Element of K6(K7( the carrier of n0, the carrier of f))
x is Element of the carrier of n0
n is V11() V12() ext-real Element of REAL
xp is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
e is Element of the carrier of n0
e - x is Element of the carrier of n0
- x is Element of the carrier of n0
K340(n0,e,(- x)) is Element of the carrier of n0
||.(e - x).|| is V11() V12() ext-real Element of REAL
xp /. e is Element of the carrier of f
xp /. x is Element of the carrier of f
(xp /. e) - (xp /. x) is Element of the carrier of f
- (xp /. x) is Element of the carrier of f
K340(f,(xp /. e),(- (xp /. x))) is Element of the carrier of f
||.((xp /. e) - (xp /. x)).|| is V11() V12() ext-real Element of REAL
dom xp is Element of K6( the carrier of n0)
K6( the carrier of n0) is set
X is set
f is non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like NORMSTR
the carrier of f is non empty set
n0 is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
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() V12() ext-real Element of REAL
xp is V11() V12() ext-real Element of REAL
x is V11() V12() 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
K340(f,e,(- x)) is Element of the carrier of f
||.(e - x).|| is V11() V12() ext-real 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
K340(n0,(xp /. e),(- (xp /. x))) is Element of the carrier of n0
||.((xp /. e) - (xp /. x)).|| is V11() V12() ext-real 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 V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
the carrier of f is non empty set
K7( the carrier of f,COMPLEX) is complex-valued set
K6(K7( the carrier of f,COMPLEX)) is set
n0 is Relation-like the carrier of f -defined COMPLEX -valued Function-like complex-valued Element of K6(K7( the carrier of f,COMPLEX))
xp is Element of the carrier of f
x is V11() V12() ext-real Element of REAL
n is V11() V12() ext-real Element of REAL
xp is V11() V12() 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
K340(f,x,(- xp)) is Element of the carrier of f
||.(x - xp).|| is V11() V12() ext-real Element of REAL
n0 /. x is V11() Element of COMPLEX
n0 /. xp is V11() Element of COMPLEX
(n0 /. x) - (n0 /. xp) is V11() Element of COMPLEX
|.((n0 /. x) - (n0 /. xp)).| is V11() V12() 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 V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
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() V12() ext-real Element of REAL
n is V11() V12() ext-real Element of REAL
xp is V11() V12() 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
K340(f,x,(- xp)) is Element of the carrier of f
||.(x - xp).|| is V11() V12() ext-real Element of REAL
n0 /. x is V11() V12() ext-real Element of REAL
n0 /. xp is V11() V12() ext-real Element of REAL
(n0 /. x) - (n0 /. xp) is V11() V12() ext-real Element of REAL
abs ((n0 /. x) - (n0 /. xp)) is V11() V12() 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 V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like NORMSTR
the carrier of f is non empty set
K7( the carrier of f,COMPLEX) is complex-valued set
K6(K7( the carrier of f,COMPLEX)) is set
n0 is Relation-like the carrier of f -defined COMPLEX -valued Function-like complex-valued Element of K6(K7( the carrier of f,COMPLEX))
xp is Element of the carrier of f
x is V11() V12() ext-real Element of REAL
n is V11() V12() ext-real Element of REAL
xp is V11() V12() 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
K340(f,x,(- xp)) is Element of the carrier of f
||.(x - xp).|| is V11() V12() ext-real Element of REAL
n0 /. x is V11() Element of COMPLEX
n0 /. xp is V11() Element of COMPLEX
(n0 /. x) - (n0 /. xp) is V11() Element of COMPLEX
|.((n0 /. x) - (n0 /. xp)).| is V11() V12() 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 V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
the carrier of f is non empty set
n0 is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
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() V12() ext-real Element of REAL
n is V11() V12() ext-real Element of REAL
n / x is V11() V12() ext-real Element of REAL
xp is V11() V12() ext-real Element of REAL
x is Element of the carrier of f
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
K340(f,x,(- e)) is Element of the carrier of f
||.(x - e).|| is V11() V12() ext-real Element of REAL
xp /. x is Element of the carrier of n0
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
K340(n0,(xp /. x),(- (xp /. e))) is Element of the carrier of n0
||.((xp /. x) - (xp /. e)).|| is V11() V12() ext-real Element of REAL
xp * x is V11() V12() ext-real Element of REAL
x * ||.(x - e).|| is V11() V12() ext-real Element of REAL
(n / x) * x is V11() V12() ext-real Element of REAL
X is set
f is non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like NORMSTR
the carrier of f is non empty set
n0 is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
the carrier of n0 is non empty set
K7( the carrier of n0, the carrier of f) is set
K6(K7( the carrier of n0, the carrier of f)) is set
xp is Relation-like the carrier of n0 -defined the carrier of f -valued Function-like Element of K6(K7( the carrier of n0, the carrier of f))
dom xp is Element of K6( the carrier of n0)
K6( the carrier of n0) is set
x is V11() V12() ext-real Element of REAL
n is V11() V12() ext-real Element of REAL
n / x is V11() V12() ext-real Element of REAL
xp is V11() V12() ext-real Element of REAL
x is Element of the carrier of n0
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
K340(n0,x,(- e)) is Element of the carrier of n0
||.(x - e).|| is V11() V12() ext-real Element of REAL
xp /. x is Element of the carrier of f
xp /. e is Element of the carrier of f
(xp /. x) - (xp /. e) is Element of the carrier of f
- (xp /. e) is Element of the carrier of f
K340(f,(xp /. x),(- (xp /. e))) is Element of the carrier of f
||.((xp /. x) - (xp /. e)).|| is V11() V12() ext-real Element of REAL
xp * x is V11() V12() ext-real Element of REAL
x * ||.(x - e).|| is V11() V12() ext-real Element of REAL
(n / x) * x is V11() V12() ext-real Element of REAL
X is set
f is non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like NORMSTR
the carrier of f is non empty set
n0 is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
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() V12() ext-real Element of REAL
n is V11() V12() ext-real Element of REAL
n / x is V11() V12() ext-real Element of REAL
xp is V11() V12() ext-real Element of REAL
x is Element of the carrier of f
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
K340(f,x,(- e)) is Element of the carrier of f
||.(x - e).|| is V11() V12() ext-real Element of REAL
xp /. x is Element of the carrier of n0
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
K340(n0,(xp /. x),(- (xp /. e))) is Element of the carrier of n0
||.((xp /. x) - (xp /. e)).|| is V11() V12() ext-real Element of REAL
xp * x is V11() V12() ext-real Element of REAL
x * ||.(x - e).|| is V11() V12() ext-real Element of REAL
(n / x) * x is V11() V12() ext-real Element of REAL
X is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
the carrier of X is non empty set
K6( the carrier of X) is set
f is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
the carrier of f is non empty set
K7( the carrier of X, the carrier of f) is set
K6(K7( the carrier of X, the carrier of f)) is set
n0 is Relation-like the carrier of X -defined the carrier of f -valued Function-like Element of K6(K7( the carrier of X, the carrier of f))
xp is Element of K6( the carrier of X)
dom n0 is Element of K6( the carrier of X)
x is V11() V12() ext-real Element of REAL
n is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
n + 1 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
1 / (n + 1) is V11() V12() ext-real Element of REAL
n is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
n + 1 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
1 / (n + 1) is V11() V12() ext-real Element of REAL
xp is Element of the carrier of X
n0 /. xp is Element of the carrier of f
x is Element of the carrier of X
n0 /. x is Element of the carrier of f
e is Element of the carrier of X
xp - e is Element of the carrier of X
- e is Element of the carrier of X
K340(X,xp,(- e)) is Element of the carrier of X
||.(xp - e).|| is V11() V12() ext-real Element of REAL
n0 /. e is Element of the carrier of f
(n0 /. xp) - (n0 /. e) is Element of the carrier of f
- (n0 /. e) is Element of the carrier of f
K340(f,(n0 /. xp),(- (n0 /. e))) is Element of the carrier of f
||.((n0 /. xp) - (n0 /. e)).|| is V11() V12() ext-real Element of REAL
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))
xp is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
xp + 1 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
1 / (xp + 1) is V11() V12() ext-real Element of REAL
n . xp is Element of the carrier of X
n0 /. (n . xp) is Element of the carrier of f
xp 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))
x is Element of the carrier of X
rng n is Element of K6( the carrier of X)
e is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
n . e is Element of the carrier of X
x is set
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))
lim x is Element of the carrier of X
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 X -valued Function-like total quasi_total subsequence of n
n - xp 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 - xp) * e is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total subsequence of n - 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 is Relation-like the carrier of X -defined the carrier of f -valued Function-like Element of K6(K7( the carrier of X, the carrier of f))
l is set
rng xp is Element of K6( the carrier of X)
k1 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
xp . k1 is Element of the carrier of X
l is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
(x - ((n - xp) * e)) . l is Element of the carrier of X
(n * e) . l is Element of the carrier of X
((n - xp) * e) . l is Element of the carrier of X
((n * e) . l) - (((n - xp) * e) . l) is Element of the carrier of X
- (((n - xp) * e) . l) is Element of the carrier of X
K340(X,((n * e) . l),(- (((n - xp) * e) . l))) is Element of the carrier of X
e . l is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
n . (e . l) is Element of the carrier of X
(n . (e . l)) - (((n - xp) * e) . l) is Element of the carrier of X
K340(X,(n . (e . l)),(- (((n - xp) * e) . l))) is Element of the carrier of X
(n - xp) . (e . l) is Element of the carrier of X
(n . (e . l)) - ((n - xp) . (e . l)) is Element of the carrier of X
- ((n - xp) . (e . l)) is Element of the carrier of X
K340(X,(n . (e . l)),(- ((n - xp) . (e . l)))) is Element of the carrier of X
xp . (e . l) is Element of the carrier of X
(n . (e . l)) - (xp . (e . l)) is Element of the carrier of X
- (xp . (e . l)) is Element of the carrier of X
K340(X,(n . (e . l)),(- (xp . (e . l)))) is Element of the carrier of X
(n . (e . l)) - ((n . (e . l)) - (xp . (e . l))) is Element of the carrier of X
- ((n . (e . l)) - (xp . (e . l))) is Element of the carrier of X
K340(X,(n . (e . l)),(- ((n . (e . l)) - (xp . (e . l))))) is Element of the carrier of X
(n . (e . l)) - (n . (e . l)) is Element of the carrier of X
- (n . (e . l)) is Element of the carrier of X
K340(X,(n . (e . l)),(- (n . (e . l)))) is Element of the carrier of X
((n . (e . l)) - (n . (e . l))) + (xp . (e . l)) is Element of the carrier of X
0. X is V88(X) Element of the carrier of X
(0. X) + (xp . (e . l)) is Element of the carrier of X
xp * e is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total subsequence of xp
(xp * e) . l is Element of the carrier of X
rng (x - ((n - xp) * e)) is Element of K6( the carrier of X)
(dom n0) /\ xp is Element of K6( the carrier of X)
dom (n0 | xp) is Element of K6( the carrier of X)
l is V11() V12() ext-real Element of REAL
l " is V11() V12() ext-real Element of REAL
k1 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
k2 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
k2 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
k2 + 1 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
k2 + 1 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
1 / (k2 + 1) is V11() V12() ext-real Element of REAL
1 / (k2 + 1) is V11() V12() ext-real Element of REAL
n . k2 is Element of the carrier of X
xp . k2 is Element of the carrier of X
(n . k2) - (xp . k2) is Element of the carrier of X
- (xp . k2) is Element of the carrier of X
K340(X,(n . k2),(- (xp . k2))) is Element of the carrier of X
||.((n . k2) - (xp . k2)).|| is V11() V12() ext-real Element of REAL
1 / (l ") is V11() V12() ext-real Element of REAL
(n - xp) . k2 is Element of the carrier of X
((n - xp) . k2) - (0. X) is Element of the carrier of X
- (0. X) is Element of the carrier of X
K340(X,((n - xp) . k2),(- (0. X))) is Element of the carrier of X
||.(((n - xp) . k2) - (0. X)).|| is V11() V12() ext-real Element of REAL
((n . k2) - (xp . k2)) - (0. X) is Element of the carrier of X
K340(X,((n . k2) - (xp . k2)),(- (0. X))) is Element of the carrier of X
||.(((n . k2) - (xp . k2)) - (0. X)).|| is V11() V12() ext-real Element of REAL
rng x is Element of K6( the carrier of X)
(n0 | xp) /. (lim x) is Element of the carrier of f
(n0 | xp) /* 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))
K7(NAT, the carrier of f) is set
K6(K7(NAT, the carrier of f)) is set
lim ((n0 | xp) /* x) is Element of the carrier of f
lim (n - xp) is Element of the carrier of X
lim ((n - xp) * e) is Element of the carrier of X
lim (x - ((n - xp) * e)) is Element of the carrier of X
(lim x) - (0. X) is Element of the carrier of X
K340(X,(lim x),(- (0. X))) is Element of the carrier of X
(n0 | 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) /* x) - ((n0 | 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))
lim ((n0 | xp) /* (x - ((n - xp) * e))) is Element of the carrier of f
lim (((n0 | xp) /* x) - ((n0 | xp) /* (x - ((n - xp) * e)))) is Element of the carrier of f
((n0 | xp) /. (lim x)) - ((n0 | xp) /. (lim x)) is Element of the carrier of f
- ((n0 | xp) /. (lim x)) is Element of the carrier of f
K340(f,((n0 | xp) /. (lim x)),(- ((n0 | xp) /. (lim x)))) is Element of the carrier of f
0. f is V88(f) Element of the carrier of f
k1 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
x . k1 is Element of the carrier of X
(x - ((n - xp) * e)) . k1 is Element of the carrier of X
(((n0 | xp) /* x) - ((n0 | xp) /* (x - ((n - xp) * e)))) . k1 is Element of the carrier of f
((((n0 | xp) /* x) - ((n0 | xp) /* (x - ((n - xp) * e)))) . k1) - (0. f) is Element of the carrier of f
- (0. f) is Element of the carrier of f
K340(f,((((n0 | xp) /* x) - ((n0 | xp) /* (x - ((n - xp) * e)))) . k1),(- (0. f))) is Element of the carrier of f
||.(((((n0 | xp) /* x) - ((n0 | xp) /* (x - ((n - xp) * e)))) . k1) - (0. f)).|| is V11() V12() ext-real Element of REAL
||.((((n0 | xp) /* x) - ((n0 | xp) /* (x - ((n - xp) * e)))) . k1).|| is V11() V12() ext-real Element of REAL
((n0 | xp) /* x) . k1 is Element of the carrier of f
((n0 | xp) /* (x - ((n - xp) * e))) . k1 is Element of the carrier of f
(((n0 | xp) /* x) . k1) - (((n0 | xp) /* (x - ((n - xp) * e))) . k1) is Element of the carrier of f
- (((n0 | xp) /* (x - ((n - xp) * e))) . k1) is Element of the carrier of f
K340(f,(((n0 | xp) /* x) . k1),(- (((n0 | xp) /* (x - ((n - xp) * e))) . k1))) is Element of the carrier of f
||.((((n0 | xp) /* x) . k1) - (((n0 | xp) /* (x - ((n - xp) * e))) . k1)).|| is V11() V12() ext-real Element of REAL
(n0 | xp) /. (x . k1) is Element of the carrier of f
((n0 | xp) /. (x . k1)) - (((n0 | xp) /* (x - ((n - xp) * e))) . k1) is Element of the carrier of f
K340(f,((n0 | xp) /. (x . k1)),(- (((n0 | xp) /* (x - ((n - xp) * e))) . k1))) is Element of the carrier of f
||.(((n0 | xp) /. (x . k1)) - (((n0 | xp) /* (x - ((n - xp) * e))) . k1)).|| is V11() V12() ext-real Element of REAL
(n0 | xp) /. ((x - ((n - xp) * e)) . k1) is Element of the carrier of f
((n0 | xp) /. (x . k1)) - ((n0 | xp) /. ((x - ((n - xp) * e)) . k1)) is Element of the carrier of f
- ((n0 | xp) /. ((x - ((n - xp) * e)) . k1)) is Element of the carrier of f
K340(f,((n0 | xp) /. (x . k1)),(- ((n0 | xp) /. ((x - ((n - xp) * e)) . k1)))) is Element of the carrier of f
||.(((n0 | xp) /. (x . k1)) - ((n0 | xp) /. ((x - ((n - xp) * e)) . k1))).|| is V11() V12() ext-real Element of REAL
n0 /. (x . k1) is Element of the carrier of f
(n0 /. (x . k1)) - ((n0 | xp) /. ((x - ((n - xp) * e)) . k1)) is Element of the carrier of f
K340(f,(n0 /. (x . k1)),(- ((n0 | xp) /. ((x - ((n - xp) * e)) . k1)))) is Element of the carrier of f
||.((n0 /. (x . k1)) - ((n0 | xp) /. ((x - ((n - xp) * e)) . k1))).|| is V11() V12() ext-real Element of REAL
n0 /. ((x - ((n - xp) * e)) . k1) is Element of the carrier of f
(n0 /. (x . k1)) - (n0 /. ((x - ((n - xp) * e)) . k1)) is Element of the carrier of f
- (n0 /. ((x - ((n - xp) * e)) . k1)) is Element of the carrier of f
K340(f,(n0 /. (x . k1)),(- (n0 /. ((x - ((n - xp) * e)) . k1)))) is Element of the carrier of f
||.((n0 /. (x . k1)) - (n0 /. ((x - ((n - xp) * e)) . k1))).|| is V11() V12() ext-real Element of REAL
e . k1 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
n . (e . k1) is Element of the carrier of X
n0 /. (n . (e . k1)) is Element of the carrier of f
(xp * e) . k1 is Element of the carrier of X
n0 /. ((xp * e) . k1) is Element of the carrier of f
(n0 /. (n . (e . k1))) - (n0 /. ((xp * e) . k1)) is Element of the carrier of f
- (n0 /. ((xp * e) . k1)) is Element of the carrier of f
K340(f,(n0 /. (n . (e . k1))),(- (n0 /. ((xp * e) . k1)))) is Element of the carrier of f
||.((n0 /. (n . (e . k1))) - (n0 /. ((xp * e) . k1))).|| is V11() V12() ext-real Element of REAL
xp . (e . k1) is Element of the carrier of X
n0 /. (xp . (e . k1)) is Element of the carrier of f
(n0 /. (n . (e . k1))) - (n0 /. (xp . (e . k1))) is Element of the carrier of f
- (n0 /. (xp . (e . k1))) is Element of the carrier of f
K340(f,(n0 /. (n . (e . k1))),(- (n0 /. (xp . (e . k1))))) is Element of the carrier of f
||.((n0 /. (n . (e . k1))) - (n0 /. (xp . (e . k1)))).|| is V11() V12() ext-real Element of REAL
X is non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like NORMSTR
the carrier of X is non empty set
f is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
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() V12() ext-real Element of REAL
n is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
n + 1 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
1 / (n + 1) is V11() V12() ext-real Element of REAL
n is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
n + 1 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
1 / (n + 1) is V11() V12() 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
K340(f,xp,(- e)) is Element of the carrier of f
||.(xp - e).|| is V11() V12() ext-real 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
K340(X,(n0 /. xp),(- (n0 /. e))) is Element of the carrier of X
||.((n0 /. xp) - (n0 /. e)).|| is V11() V12() ext-real 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 V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
xp + 1 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
1 / (xp + 1) is V11() V12() 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 Element of the carrier of f
rng n is Element of K6( the carrier of f)
e is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
n . e is Element of the carrier of f
x is set
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 V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
xp . k1 is Element of the carrier of f
l is V4() V5() V6() V10() V11() V12() 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
K340(f,((n * e) . l),(- (((n - xp) * e) . l))) is Element of the carrier of f
e . l is V4() V5() V6() V10() V11() V12() 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
K340(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
K340(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
K340(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
K340(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
K340(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 V88(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() V12() ext-real Element of REAL
l " is V11() V12() ext-real Element of REAL
k1 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
k2 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
k2 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
k2 + 1 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
k2 + 1 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
1 / (k2 + 1) is V11() V12() ext-real Element of REAL
1 / (k2 + 1) is V11() V12() 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
K340(f,(n . k2),(- (xp . k2))) is Element of the carrier of f
||.((n . k2) - (xp . k2)).|| is V11() V12() ext-real Element of REAL
1 / (l ") is V11() V12() 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
K340(f,((n - xp) . k2),(- (0. f))) is Element of the carrier of f
||.(((n - xp) . k2) - (0. f)).|| is V11() V12() ext-real Element of REAL
((n . k2) - (xp . k2)) - (0. f) is Element of the carrier of f
K340(f,((n . k2) - (xp . k2)),(- (0. f))) is Element of the carrier of f
||.(((n . k2) - (xp . k2)) - (0. f)).|| is V11() V12() ext-real 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
K340(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
K340(X,((n0 | xp) /. (lim x)),(- ((n0 | xp) /. (lim x)))) is Element of the carrier of X
0. X is V88(X) Element of the carrier of X
k1 is V4() V5() V6() V10() V11() V12() 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
K340(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() V12() ext-real Element of REAL
||.((((n0 | xp) /* x) - ((n0 | xp) /* (x - ((n - xp) * e)))) . k1).|| is V11() V12() ext-real 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
K340(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() V12() ext-real 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
K340(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() V12() ext-real 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
K340(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() V12() ext-real 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
K340(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() V12() ext-real 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
K340(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() V12() ext-real Element of REAL
e . k1 is V4() V5() V6() V10() V11() V12() 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
K340(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() V12() ext-real 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
K340(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() V12() ext-real Element of REAL
X is non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like NORMSTR
the carrier of X is non empty set
K6( the carrier of X) is set
f is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
the carrier of f is non empty set
K7( the carrier of X, the carrier of f) is set
K6(K7( the carrier of X, the carrier of f)) is set
n0 is Relation-like the carrier of X -defined the carrier of f -valued Function-like Element of K6(K7( the carrier of X, the carrier of f))
xp is Element of K6( the carrier of X)
dom n0 is Element of K6( the carrier of X)
x is V11() V12() ext-real Element of REAL
n is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
n + 1 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
1 / (n + 1) is V11() V12() ext-real Element of REAL
n is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
n + 1 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
1 / (n + 1) is V11() V12() ext-real Element of REAL
xp is Element of the carrier of X
n0 /. xp is Element of the carrier of f
x is Element of the carrier of X
n0 /. x is Element of the carrier of f
e is Element of the carrier of X
xp - e is Element of the carrier of X
- e is Element of the carrier of X
K340(X,xp,(- e)) is Element of the carrier of X
||.(xp - e).|| is V11() V12() ext-real Element of REAL
n0 /. e is Element of the carrier of f
(n0 /. xp) - (n0 /. e) is Element of the carrier of f
- (n0 /. e) is Element of the carrier of f
K340(f,(n0 /. xp),(- (n0 /. e))) is Element of the carrier of f
||.((n0 /. xp) - (n0 /. e)).|| is V11() V12() ext-real Element of REAL
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))
xp is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
xp + 1 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
1 / (xp + 1) is V11() V12() ext-real Element of REAL
n . xp is Element of the carrier of X
n0 /. (n . xp) is Element of the carrier of f
xp 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))
x is Element of the carrier of X
rng n is Element of K6( the carrier of X)
e is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
n . e is Element of the carrier of X
x is set
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))
lim x is Element of the carrier of X
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 X -valued Function-like total quasi_total subsequence of n
n - xp 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 - xp) * e is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total subsequence of n - 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 is Relation-like the carrier of X -defined the carrier of f -valued Function-like Element of K6(K7( the carrier of X, the carrier of f))
l is set
rng xp is Element of K6( the carrier of X)
k1 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
xp . k1 is Element of the carrier of X
l is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
(x - ((n - xp) * e)) . l is Element of the carrier of X
(n * e) . l is Element of the carrier of X
((n - xp) * e) . l is Element of the carrier of X
((n * e) . l) - (((n - xp) * e) . l) is Element of the carrier of X
- (((n - xp) * e) . l) is Element of the carrier of X
K340(X,((n * e) . l),(- (((n - xp) * e) . l))) is Element of the carrier of X
e . l is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
n . (e . l) is Element of the carrier of X
(n . (e . l)) - (((n - xp) * e) . l) is Element of the carrier of X
K340(X,(n . (e . l)),(- (((n - xp) * e) . l))) is Element of the carrier of X
(n - xp) . (e . l) is Element of the carrier of X
(n . (e . l)) - ((n - xp) . (e . l)) is Element of the carrier of X
- ((n - xp) . (e . l)) is Element of the carrier of X
K340(X,(n . (e . l)),(- ((n - xp) . (e . l)))) is Element of the carrier of X
xp . (e . l) is Element of the carrier of X
(n . (e . l)) - (xp . (e . l)) is Element of the carrier of X
- (xp . (e . l)) is Element of the carrier of X
K340(X,(n . (e . l)),(- (xp . (e . l)))) is Element of the carrier of X
(n . (e . l)) - ((n . (e . l)) - (xp . (e . l))) is Element of the carrier of X
- ((n . (e . l)) - (xp . (e . l))) is Element of the carrier of X
K340(X,(n . (e . l)),(- ((n . (e . l)) - (xp . (e . l))))) is Element of the carrier of X
(n . (e . l)) - (n . (e . l)) is Element of the carrier of X
- (n . (e . l)) is Element of the carrier of X
K340(X,(n . (e . l)),(- (n . (e . l)))) is Element of the carrier of X
((n . (e . l)) - (n . (e . l))) + (xp . (e . l)) is Element of the carrier of X
0. X is V88(X) Element of the carrier of X
(0. X) + (xp . (e . l)) is Element of the carrier of X
xp * e is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total subsequence of xp
(xp * e) . l is Element of the carrier of X
rng (x - ((n - xp) * e)) is Element of K6( the carrier of X)
(dom n0) /\ xp is Element of K6( the carrier of X)
dom (n0 | xp) is Element of K6( the carrier of X)
l is V11() V12() ext-real Element of REAL
l " is V11() V12() ext-real Element of REAL
k1 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
k2 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
k2 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
k2 + 1 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
k2 + 1 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
1 / (k2 + 1) is V11() V12() ext-real Element of REAL
1 / (k2 + 1) is V11() V12() ext-real Element of REAL
n . k2 is Element of the carrier of X
xp . k2 is Element of the carrier of X
(n . k2) - (xp . k2) is Element of the carrier of X
- (xp . k2) is Element of the carrier of X
K340(X,(n . k2),(- (xp . k2))) is Element of the carrier of X
||.((n . k2) - (xp . k2)).|| is V11() V12() ext-real Element of REAL
1 / (l ") is V11() V12() ext-real Element of REAL
(n - xp) . k2 is Element of the carrier of X
((n - xp) . k2) - (0. X) is Element of the carrier of X
- (0. X) is Element of the carrier of X
K340(X,((n - xp) . k2),(- (0. X))) is Element of the carrier of X
||.(((n - xp) . k2) - (0. X)).|| is V11() V12() ext-real Element of REAL
((n . k2) - (xp . k2)) - (0. X) is Element of the carrier of X
K340(X,((n . k2) - (xp . k2)),(- (0. X))) is Element of the carrier of X
||.(((n . k2) - (xp . k2)) - (0. X)).|| is V11() V12() ext-real Element of REAL
rng x is Element of K6( the carrier of X)
(n0 | xp) /. (lim x) is Element of the carrier of f
(n0 | xp) /* 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))
K7(NAT, the carrier of f) is set
K6(K7(NAT, the carrier of f)) is set
lim ((n0 | xp) /* x) is Element of the carrier of f
lim (n - xp) is Element of the carrier of X
lim ((n - xp) * e) is Element of the carrier of X
lim (x - ((n - xp) * e)) is Element of the carrier of X
(lim x) - (0. X) is Element of the carrier of X
K340(X,(lim x),(- (0. X))) is Element of the carrier of X
(n0 | 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) /* x) - ((n0 | 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))
lim ((n0 | xp) /* (x - ((n - xp) * e))) is Element of the carrier of f
lim (((n0 | xp) /* x) - ((n0 | xp) /* (x - ((n - xp) * e)))) is Element of the carrier of f
((n0 | xp) /. (lim x)) - ((n0 | xp) /. (lim x)) is Element of the carrier of f
- ((n0 | xp) /. (lim x)) is Element of the carrier of f
K340(f,((n0 | xp) /. (lim x)),(- ((n0 | xp) /. (lim x)))) is Element of the carrier of f
0. f is V88(f) Element of the carrier of f
k1 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
x . k1 is Element of the carrier of X
(x - ((n - xp) * e)) . k1 is Element of the carrier of X
(((n0 | xp) /* x) - ((n0 | xp) /* (x - ((n - xp) * e)))) . k1 is Element of the carrier of f
((((n0 | xp) /* x) - ((n0 | xp) /* (x - ((n - xp) * e)))) . k1) - (0. f) is Element of the carrier of f
- (0. f) is Element of the carrier of f
K340(f,((((n0 | xp) /* x) - ((n0 | xp) /* (x - ((n - xp) * e)))) . k1),(- (0. f))) is Element of the carrier of f
||.(((((n0 | xp) /* x) - ((n0 | xp) /* (x - ((n - xp) * e)))) . k1) - (0. f)).|| is V11() V12() ext-real Element of REAL
||.((((n0 | xp) /* x) - ((n0 | xp) /* (x - ((n - xp) * e)))) . k1).|| is V11() V12() ext-real Element of REAL
((n0 | xp) /* x) . k1 is Element of the carrier of f
((n0 | xp) /* (x - ((n - xp) * e))) . k1 is Element of the carrier of f
(((n0 | xp) /* x) . k1) - (((n0 | xp) /* (x - ((n - xp) * e))) . k1) is Element of the carrier of f
- (((n0 | xp) /* (x - ((n - xp) * e))) . k1) is Element of the carrier of f
K340(f,(((n0 | xp) /* x) . k1),(- (((n0 | xp) /* (x - ((n - xp) * e))) . k1))) is Element of the carrier of f
||.((((n0 | xp) /* x) . k1) - (((n0 | xp) /* (x - ((n - xp) * e))) . k1)).|| is V11() V12() ext-real Element of REAL
(n0 | xp) /. (x . k1) is Element of the carrier of f
((n0 | xp) /. (x . k1)) - (((n0 | xp) /* (x - ((n - xp) * e))) . k1) is Element of the carrier of f
K340(f,((n0 | xp) /. (x . k1)),(- (((n0 | xp) /* (x - ((n - xp) * e))) . k1))) is Element of the carrier of f
||.(((n0 | xp) /. (x . k1)) - (((n0 | xp) /* (x - ((n - xp) * e))) . k1)).|| is V11() V12() ext-real Element of REAL
(n0 | xp) /. ((x - ((n - xp) * e)) . k1) is Element of the carrier of f
((n0 | xp) /. (x . k1)) - ((n0 | xp) /. ((x - ((n - xp) * e)) . k1)) is Element of the carrier of f
- ((n0 | xp) /. ((x - ((n - xp) * e)) . k1)) is Element of the carrier of f
K340(f,((n0 | xp) /. (x . k1)),(- ((n0 | xp) /. ((x - ((n - xp) * e)) . k1)))) is Element of the carrier of f
||.(((n0 | xp) /. (x . k1)) - ((n0 | xp) /. ((x - ((n - xp) * e)) . k1))).|| is V11() V12() ext-real Element of REAL
n0 /. (x . k1) is Element of the carrier of f
(n0 /. (x . k1)) - ((n0 | xp) /. ((x - ((n - xp) * e)) . k1)) is Element of the carrier of f
K340(f,(n0 /. (x . k1)),(- ((n0 | xp) /. ((x - ((n - xp) * e)) . k1)))) is Element of the carrier of f
||.((n0 /. (x . k1)) - ((n0 | xp) /. ((x - ((n - xp) * e)) . k1))).|| is V11() V12() ext-real Element of REAL
n0 /. ((x - ((n - xp) * e)) . k1) is Element of the carrier of f
(n0 /. (x . k1)) - (n0 /. ((x - ((n - xp) * e)) . k1)) is Element of the carrier of f
- (n0 /. ((x - ((n - xp) * e)) . k1)) is Element of the carrier of f
K340(f,(n0 /. (x . k1)),(- (n0 /. ((x - ((n - xp) * e)) . k1)))) is Element of the carrier of f
||.((n0 /. (x . k1)) - (n0 /. ((x - ((n - xp) * e)) . k1))).|| is V11() V12() ext-real Element of REAL
e . k1 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
n . (e . k1) is Element of the carrier of X
n0 /. (n . (e . k1)) is Element of the carrier of f
(xp * e) . k1 is Element of the carrier of X
n0 /. ((xp * e) . k1) is Element of the carrier of f
(n0 /. (n . (e . k1))) - (n0 /. ((xp * e) . k1)) is Element of the carrier of f
- (n0 /. ((xp * e) . k1)) is Element of the carrier of f
K340(f,(n0 /. (n . (e . k1))),(- (n0 /. ((xp * e) . k1)))) is Element of the carrier of f
||.((n0 /. (n . (e . k1))) - (n0 /. ((xp * e) . k1))).|| is V11() V12() ext-real Element of REAL
xp . (e . k1) is Element of the carrier of X
n0 /. (xp . (e . k1)) is Element of the carrier of f
(n0 /. (n . (e . k1))) - (n0 /. (xp . (e . k1))) is Element of the carrier of f
- (n0 /. (xp . (e . k1))) is Element of the carrier of f
K340(f,(n0 /. (n . (e . k1))),(- (n0 /. (xp . (e . k1))))) is Element of the carrier of f
||.((n0 /. (n . (e . k1))) - (n0 /. (xp . (e . k1)))).|| is V11() V12() ext-real Element of REAL
X is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
the carrier of X is non empty set
f is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
the carrier of f is non empty set
K7( the carrier of X, the carrier of f) is set
K6(K7( the carrier of X, the carrier of f)) is set
K6( the carrier of X) is set
xp is Element of K6( the carrier of X)
n0 is Relation-like the carrier of X -defined the carrier of f -valued Function-like Element of K6(K7( the carrier of X, the carrier of f))
dom n0 is Element of K6( the carrier of X)
n0 .: xp is Element of K6( the carrier of f)
K6( the carrier of f) is set
f is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
the carrier of f is non empty set
X is non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() 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 V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like NORMSTR
the carrier of X is non empty set
f is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
the carrier of f is non empty set
K7( the carrier of X, the carrier of f) is set
K6(K7( the carrier of X, the carrier of f)) is set
K6( the carrier of X) is set
xp is Element of K6( the carrier of X)
n0 is Relation-like the carrier of X -defined the carrier of f -valued Function-like Element of K6(K7( the carrier of X, the carrier of f))
dom n0 is Element of K6( the carrier of X)
n0 .: xp is Element of K6( the carrier of f)
K6( the carrier of f) is set
X is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
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() V12() ext-real Element of REAL
lower_bound (f .: n0) is V11() V12() ext-real Element of REAL
f is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
the carrier of f is non empty set
n0 is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
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))
n0 is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
the carrier of n0 is non empty set
f is non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like NORMSTR
the carrier of f is non empty set
K7( the carrier of n0, the carrier of f) is set
K6(K7( the carrier of n0, the carrier of f)) is set
X is set
xp is Relation-like the carrier of n0 -defined the carrier of f -valued Function-like Element of K6(K7( the carrier of n0, the carrier of f))
dom xp is Element of K6( the carrier of n0)
K6( the carrier of n0) is set
xp | X is Relation-like the carrier of n0 -defined the carrier of f -valued Function-like Element of K6(K7( the carrier of n0, the carrier of f))
f is non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like NORMSTR
the carrier of f is non empty set
n0 is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
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 CNORMSTR
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 V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() CNORMSTR
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() V12() 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
K340(X,(n0 . xp),(- (n0 . x))) is Element of the carrier of X
||.((n0 . xp) - (n0 . x)).|| is V11() V12() ext-real Element of REAL
xp - x is Element of the carrier of X
- x is Element of the carrier of X
K340(X,xp,(- x)) is Element of the carrier of X
||.(xp - x).|| is V11() V12() ext-real Element of REAL
(1 / 2) * ||.(xp - x).|| is V11() V12() ext-real Element of REAL
X is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
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
K340(X,f,(- n0)) is Element of the carrier of X
||.(f - n0).|| is V11() V12() ext-real Element of REAL
0. X is V88(X) Element of the carrier of X
X is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
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
K340(X,f,(- n0)) is Element of the carrier of X
||.(f - n0).|| is V11() V12() ext-real Element of REAL
n0 - f is Element of the carrier of X
- f is Element of the carrier of X
K340(X,n0,(- f)) is Element of the carrier of X
||.(n0 - f).|| is V11() V12() ext-real Element of REAL
- (f - n0) is Element of the carrier of X
||.(- (f - n0)).|| is V11() V12() ext-real Element of REAL
X is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
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
K340(X,f,(- xp)) is Element of the carrier of X
||.(f - xp).|| is V11() V12() ext-real 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
K340(X,xp,(- n0)) is Element of the carrier of X
||.(xp - n0).|| is V11() V12() ext-real Element of REAL
f - n0 is Element of the carrier of X
K340(X,f,(- n0)) is Element of the carrier of X
||.(f - n0).|| is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
x / 2 is V11() V12() ext-real Element of REAL
(x / 2) + (x / 2) is V11() V12() ext-real Element of REAL
||.(f - xp).|| + ||.(xp - n0).|| is V11() V12() ext-real Element of REAL
(||.(f - xp).|| + ||.(xp - n0).||) + x is V11() V12() ext-real Element of REAL
||.(f - n0).|| + (||.(f - xp).|| + ||.(xp - n0).||) is V11() V12() ext-real Element of REAL
x + (||.(f - xp).|| + ||.(xp - n0).||) is V11() V12() ext-real Element of REAL
- (||.(f - xp).|| + ||.(xp - n0).||) is V11() V12() ext-real Element of REAL
(x + (||.(f - xp).|| + ||.(xp - n0).||)) + (- (||.(f - xp).|| + ||.(xp - n0).||)) is V11() V12() ext-real Element of REAL
(||.(f - n0).|| + (||.(f - xp).|| + ||.(xp - n0).||)) + (- (||.(f - xp).|| + ||.(xp - n0).||)) is V11() V12() ext-real Element of REAL
X is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
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
K340(X,f,(- xp)) is Element of the carrier of X
||.(f - xp).|| is V11() V12() ext-real Element of REAL
n0 is Element of the carrier of X
n0 - xp is Element of the carrier of X
K340(X,n0,(- xp)) is Element of the carrier of X
||.(n0 - xp).|| is V11() V12() ext-real Element of REAL
f - n0 is Element of the carrier of X
- n0 is Element of the carrier of X
K340(X,f,(- n0)) is Element of the carrier of X
||.(f - n0).|| is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
x / 2 is V11() V12() ext-real Element of REAL
- (n0 - xp) is Element of the carrier of X
||.(- (n0 - xp)).|| is V11() V12() ext-real Element of REAL
xp - n0 is Element of the carrier of X
K340(X,xp,(- n0)) is Element of the carrier of X
||.(xp - n0).|| is V11() V12() ext-real Element of REAL
X is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
the carrier of X is non empty set
0. X is V88(X) Element of the carrier of X
f is Element of the carrier of X
||.f.|| is V11() V12() ext-real Element of REAL
X is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like CNORMSTR
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
K340(X,f,(- n0)) is Element of the carrier of X
||.(f - n0).|| is V11() V12() ext-real Element of REAL
0. X is V88(X) Element of the carrier of X
X is non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() CNORMSTR
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() V12() ext-real Element of REAL
x is Relation-like Function-like set
dom x is set
x . 0 is set
n is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
x . n is set
n + 1 is V4() V5() V6() V10() V11() V12() 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 V4() V5() V6() V10() V11() V12() 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
K340(X,((n ^\ 1) . xp),(- (n0 . (lim n)))) is Element of the carrier of X
||.(((n ^\ 1) . xp) - (n0 . (lim n))).|| is V11() V12() ext-real Element of REAL
xp + 1 is V4() V5() V6() V10() V11() V12() 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
K340(X,(n . (xp + 1)),(- (n0 . (lim n)))) is Element of the carrier of X
||.((n . (xp + 1)) - (n0 . (lim n))).|| is V11() V12() ext-real 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
K340(X,(n0 . (n . xp)),(- (n0 . (lim n)))) is Element of the carrier of X
||.((n0 . (n . xp)) - (n0 . (lim n))).|| is V11() V12() ext-real Element of REAL
(n . xp) - (lim n) is Element of the carrier of X
- (lim n) is Element of the carrier of X
K340(X,(n . xp),(- (lim n))) is Element of the carrier of X
||.((n . xp) - (lim n)).|| is V11() V12() ext-real Element of REAL
xp * ||.((n . xp) - (lim n)).|| is V11() V12() 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
K340(X,(n . 1),(- (n . 0))) is Element of the carrier of X
||.((n . 1) - (n . 0)).|| is V11() V12() ext-real Element of REAL
xp is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
xp + 1 is V4() V5() V6() V10() V11() V12() 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
K340(X,(n . (xp + 1)),(- (n . xp))) is Element of the carrier of X
||.((n . (xp + 1)) - (n . xp)).|| is V11() V12() ext-real Element of REAL
xp to_power xp is V11() V12() ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * (xp to_power xp) is V11() V12() ext-real Element of REAL
(xp + 1) + 1 is V4() V5() V6() V10() V11() V12() 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
K340(X,(n . ((xp + 1) + 1)),(- (n . (xp + 1)))) is Element of the carrier of X
||.((n . ((xp + 1) + 1)) - (n . (xp + 1))).|| is V11() V12() ext-real Element of REAL
xp to_power (xp + 1) is V11() V12() ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * (xp to_power (xp + 1)) is V11() V12() ext-real Element of REAL
xp * ||.((n . (xp + 1)) - (n . xp)).|| is V11() V12() ext-real Element of REAL
xp * (||.((n . 1) - (n . 0)).|| * (xp to_power xp)) is V11() V12() 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
K340(X,(n0 . (n . (xp + 1))),(- (n0 . (n . xp)))) is Element of the carrier of X
||.((n0 . (n . (xp + 1))) - (n0 . (n . xp))).|| is V11() V12() ext-real Element of REAL
xp * (xp to_power xp) is V11() V12() ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * (xp * (xp to_power xp)) is V11() V12() ext-real Element of REAL
xp to_power 1 is V11() V12() ext-real Element of REAL
(xp to_power 1) * (xp to_power xp) is V11() V12() ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * ((xp to_power 1) * (xp to_power xp)) is V11() V12() ext-real Element of REAL
0 + 1 is non empty V4() V5() V6() V10() V11() V12() 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
K340(X,(n . (0 + 1)),(- (n . 0))) is Element of the carrier of X
||.((n . (0 + 1)) - (n . 0)).|| is V11() V12() ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * 1 is V11() V12() ext-real Element of REAL
xp to_power 0 is V11() V12() ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * (xp to_power 0) is V11() V12() ext-real Element of REAL
xp is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
xp + 1 is V4() V5() V6() V10() V11() V12() 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
K340(X,(n . (xp + 1)),(- (n . xp))) is Element of the carrier of X
||.((n . (xp + 1)) - (n . xp)).|| is V11() V12() ext-real Element of REAL
xp to_power xp is V11() V12() ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * (xp to_power xp) is V11() V12() ext-real Element of REAL
1 - xp is V11() V12() ext-real Element of REAL
xp is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
x is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
xp to_power x is V11() V12() ext-real Element of REAL
x + xp is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
xp to_power (x + xp) is V11() V12() ext-real Element of REAL
(xp to_power x) - (xp to_power (x + xp)) is V11() V12() ext-real Element of REAL
((xp to_power x) - (xp to_power (x + xp))) / (1 - xp) is V11() V12() ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * (((xp to_power x) - (xp to_power (x + xp))) / (1 - xp)) is V11() V12() ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * (xp to_power (x + xp)) is V11() V12() 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() V12() ext-real Element of REAL
(||.((n . 1) - (n . 0)).|| * (xp to_power (x + xp))) * (1 - xp) is V11() V12() ext-real Element of REAL
((||.((n . 1) - (n . 0)).|| * (xp to_power (x + xp))) * (1 - xp)) / (1 - xp) is V11() V12() 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() V12() ext-real Element of REAL
(xp to_power (x + xp)) * (1 - xp) is V11() V12() ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * ((xp to_power (x + xp)) * (1 - xp)) is V11() V12() ext-real Element of REAL
(||.((n . 1) - (n . 0)).|| * ((xp to_power (x + xp)) * (1 - xp))) / (1 - xp) is V11() V12() 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() V12() ext-real Element of REAL
((xp to_power (x + xp)) * (1 - xp)) / (1 - xp) is V11() V12() ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * (((xp to_power (x + xp)) * (1 - xp)) / (1 - xp)) is V11() V12() 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() V12() 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() V12() 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() V12() ext-real Element of REAL
1 * (xp to_power (x + xp)) is V11() V12() ext-real Element of REAL
xp * (xp to_power (x + xp)) is V11() V12() ext-real Element of REAL
(1 * (xp to_power (x + xp))) - (xp * (xp to_power (x + xp))) is V11() V12() ext-real Element of REAL
((xp to_power x) - (xp to_power (x + xp))) + ((1 * (xp to_power (x + xp))) - (xp * (xp to_power (x + xp)))) is V11() V12() ext-real Element of REAL
(((xp to_power x) - (xp to_power (x + xp))) + ((1 * (xp to_power (x + xp))) - (xp * (xp to_power (x + xp))))) / (1 - xp) is V11() V12() ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * ((((xp to_power x) - (xp to_power (x + xp))) + ((1 * (xp to_power (x + xp))) - (xp * (xp to_power (x + xp))))) / (1 - xp)) is V11() V12() ext-real Element of REAL
(xp to_power x) - (xp * (xp to_power (x + xp))) is V11() V12() ext-real Element of REAL
((xp to_power x) - (xp * (xp to_power (x + xp)))) / (1 - xp) is V11() V12() ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * (((xp to_power x) - (xp * (xp to_power (x + xp)))) / (1 - xp)) is V11() V12() ext-real Element of REAL
xp to_power 1 is V11() V12() ext-real Element of REAL
(xp to_power 1) * (xp to_power (x + xp)) is V11() V12() ext-real Element of REAL
(xp to_power x) - ((xp to_power 1) * (xp to_power (x + xp))) is V11() V12() ext-real Element of REAL
((xp to_power x) - ((xp to_power 1) * (xp to_power (x + xp)))) / (1 - xp) is V11() V12() 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() V12() ext-real Element of REAL
(x + xp) + 1 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
xp to_power ((x + xp) + 1) is V11() V12() ext-real Element of REAL
(xp to_power x) - (xp to_power ((x + xp) + 1)) is V11() V12() ext-real Element of REAL
((xp to_power x) - (xp to_power ((x + xp) + 1))) / (1 - xp) is V11() V12() ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * (((xp to_power x) - (xp to_power ((x + xp) + 1))) / (1 - xp)) is V11() V12() 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
K340(X,(n . (x + xp)),(- (n . x))) is Element of the carrier of X
||.((n . (x + xp)) - (n . x)).|| is V11() V12() ext-real 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
K340(X,(n . ((x + xp) + 1)),(- (n . (x + xp)))) is Element of the carrier of X
||.((n . ((x + xp) + 1)) - (n . (x + xp))).|| is V11() V12() ext-real Element of REAL
xp + 1 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
x + (xp + 1) is V4() V5() V6() V10() V11() V12() 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
K340(X,(n . (x + (xp + 1))),(- (n . x))) is Element of the carrier of X
||.((n . (x + (xp + 1))) - (n . x)).|| is V11() V12() ext-real Element of REAL
(n . (x + (xp + 1))) - (n . (x + xp)) is Element of the carrier of X
K340(X,(n . (x + (xp + 1))),(- (n . (x + xp)))) is Element of the carrier of X
||.((n . (x + (xp + 1))) - (n . (x + xp))).|| is V11() V12() ext-real Element of REAL
||.((n . (x + (xp + 1))) - (n . (x + xp))).|| + ||.((n . (x + xp)) - (n . x)).|| is V11() V12() ext-real 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() V12() ext-real Element of REAL
xp to_power (x + (xp + 1)) is V11() V12() ext-real Element of REAL
(xp to_power x) - (xp to_power (x + (xp + 1))) is V11() V12() ext-real Element of REAL
((xp to_power x) - (xp to_power (x + (xp + 1)))) / (1 - xp) is V11() V12() ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * (((xp to_power x) - (xp to_power (x + (xp + 1)))) / (1 - xp)) is V11() V12() ext-real Element of REAL
x is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
x + (xp + 1) is V4() V5() V6() V10() V11() V12() 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
K340(X,(n . (x + (xp + 1))),(- (n . x))) is Element of the carrier of X
||.((n . (x + (xp + 1))) - (n . x)).|| is V11() V12() ext-real Element of REAL
xp to_power x is V11() V12() ext-real Element of REAL
xp to_power (x + (xp + 1)) is V11() V12() ext-real Element of REAL
(xp to_power x) - (xp to_power (x + (xp + 1))) is V11() V12() ext-real Element of REAL
((xp to_power x) - (xp to_power (x + (xp + 1)))) / (1 - xp) is V11() V12() ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * (((xp to_power x) - (xp to_power (x + (xp + 1)))) / (1 - xp)) is V11() V12() ext-real Element of REAL
xp is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
xp + 0 is V4() V5() V6() V10() V11() V12() 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
K340(X,(n . (xp + 0)),(- (n . xp))) is Element of the carrier of X
||.((n . (xp + 0)) - (n . xp)).|| is V11() V12() ext-real Element of REAL
0. X is V88(X) Element of the carrier of X
||.(0. X).|| is V11() V12() ext-real Element of REAL
xp to_power xp is V11() V12() ext-real Element of REAL
xp to_power (xp + 0) is V11() V12() ext-real Element of REAL
(xp to_power xp) - (xp to_power (xp + 0)) is V11() V12() ext-real Element of REAL
((xp to_power xp) - (xp to_power (xp + 0))) / (1 - xp) is V11() V12() ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * (((xp to_power xp) - (xp to_power (xp + 0))) / (1 - xp)) is V11() V12() ext-real Element of REAL
xp is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
xp + 0 is V4() V5() V6() V10() V11() V12() 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
K340(X,(n . (xp + 0)),(- (n . xp))) is Element of the carrier of X
||.((n . (xp + 0)) - (n . xp)).|| is V11() V12() ext-real Element of REAL
xp to_power xp is V11() V12() ext-real Element of REAL
xp to_power (xp + 0) is V11() V12() ext-real Element of REAL
(xp to_power xp) - (xp to_power (xp + 0)) is V11() V12() ext-real Element of REAL
((xp to_power xp) - (xp to_power (xp + 0))) / (1 - xp) is V11() V12() ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * (((xp to_power xp) - (xp to_power (xp + 0))) / (1 - xp)) is V11() V12() ext-real Element of REAL
x is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
xp is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
x + xp is V4() V5() V6() V10() V11() V12() 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
K340(X,(n . (x + xp)),(- (n . x))) is Element of the carrier of X
||.((n . (x + xp)) - (n . x)).|| is V11() V12() ext-real Element of REAL
xp to_power x is V11() V12() ext-real Element of REAL
xp to_power (x + xp) is V11() V12() ext-real Element of REAL
(xp to_power x) - (xp to_power (x + xp)) is V11() V12() ext-real Element of REAL
((xp to_power x) - (xp to_power (x + xp))) / (1 - xp) is V11() V12() ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * (((xp to_power x) - (xp to_power (x + xp))) / (1 - xp)) is V11() V12() ext-real Element of REAL
xp is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
x is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
x + xp is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
xp to_power (x + xp) is V11() V12() ext-real Element of REAL
xp to_power x is V11() V12() ext-real Element of REAL
(xp to_power x) - (xp to_power (x + xp)) is V11() V12() ext-real Element of REAL
(xp to_power x) - 0 is V11() V12() ext-real Element of REAL
1 - 1 is V11() V12() ext-real Element of REAL
((xp to_power x) - (xp to_power (x + xp))) / (1 - xp) is V11() V12() ext-real Element of REAL
(xp to_power x) / (1 - xp) is V11() V12() ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * (((xp to_power x) - (xp to_power (x + xp))) / (1 - xp)) is V11() V12() ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * ((xp to_power x) / (1 - xp)) is V11() V12() 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
K340(X,(n . (x + xp)),(- (n . x))) is Element of the carrier of X
||.((n . (x + xp)) - (n . x)).|| is V11() V12() ext-real Element of REAL
x is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
x + xp is V4() V5() V6() V10() V11() V12() 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
K340(X,(n . (x + xp)),(- (n . x))) is Element of the carrier of X
||.((n . (x + xp)) - (n . x)).|| is V11() V12() ext-real Element of REAL
xp to_power x is V11() V12() ext-real Element of REAL
(xp to_power x) / (1 - xp) is V11() V12() ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * ((xp to_power x) / (1 - xp)) is V11() V12() ext-real Element of REAL
xp is V11() V12() ext-real Element of REAL
xp / 2 is V11() V12() ext-real Element of REAL
||.((n . 1) - (n . 0)).|| / (1 - xp) is V11() V12() ext-real Element of REAL
x is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
xp to_power x is V11() V12() ext-real Element of REAL
(||.((n . 1) - (n . 0)).|| / (1 - xp)) * (xp to_power x) is V11() V12() ext-real Element of REAL
abs ((||.((n . 1) - (n . 0)).|| / (1 - xp)) * (xp to_power x)) is V11() V12() ext-real Element of REAL
x + 1 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
(xp to_power x) / (1 - xp) is V11() V12() ext-real Element of REAL
||.((n . 1) - (n . 0)).|| * ((xp to_power x) / (1 - xp)) is V11() V12() ext-real Element of REAL
e is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
n is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
l is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
k1 is V4() V5() V6() V10() V11() V12() ext-real set
x + k1 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
k2 is V4() V5() V6() V10() V11() V12() ext-real set
x + k2 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
k2 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
x + k2 is V4() V5() V6() V10() V11() V12() 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
K340(X,(n . (x + k2)),(- (n . x))) is Element of the carrier of X
||.((n . (x + k2)) - (n . x)).|| is V11() V12() ext-real Element of REAL
n . l is Element of the carrier of X
(n . l) - (n . x) is Element of the carrier of X
K340(X,(n . l),(- (n . x))) is Element of the carrier of X
||.((n . l) - (n . x)).|| is V11() V12() ext-real Element of REAL
k1 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
x + k1 is V4() V5() V6() V10() V11() V12() 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
K340(X,(n . (x + k1)),(- (n . x))) is Element of the carrier of X
||.((n . (x + k1)) - (n . x)).|| is V11() V12() ext-real Element of REAL
n . n is Element of the carrier of X
(n . n) - (n . x) is Element of the carrier of X
K340(X,(n . n),(- (n . x))) is Element of the carrier of X
||.((n . n) - (n . x)).|| is V11() V12() ext-real Element of REAL
(n . l) - (n . n) is Element of the carrier of X
- (n . n) is Element of the carrier of X
K340(X,(n . l),(- (n . n))) is Element of the carrier of X
||.((n . l) - (n . n)).|| is V11() V12() ext-real Element of REAL
n is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
l is V4() V5() V6() V10() V11() V12() 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
K340(X,(n . n),(- (n . l))) is Element of the carrier of X
||.((n . n) - (n . l)).|| is V11() V12() ext-real 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() V12() ext-real Element of REAL
lim ||.(n - (lim n)).|| is V11() V12() ext-real Element of REAL
xp * (lim ||.(n - (lim n)).||) is V11() V12() ext-real Element of REAL
xp * 0 is V11() V12() ext-real Element of REAL
xp is V11() V12() ext-real Element of REAL
x is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
e is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
(xp (#) ||.(n - (lim n)).||) . e is V11() V12() ext-real Element of REAL
((xp (#) ||.(n - (lim n)).||) . e) - 0 is V11() V12() ext-real Element of REAL
abs (((xp (#) ||.(n - (lim n)).||) . e) - 0) is V11() V12() ext-real Element of REAL
||.(n - (lim n)).|| . e is V11() V12() ext-real Element of REAL
xp * (||.(n - (lim n)).|| . e) is V11() V12() ext-real Element of REAL
abs (xp * (||.(n - (lim n)).|| . e)) is V11() V12() ext-real Element of REAL
(n - (lim n)) . e is Element of the carrier of X
||.((n - (lim n)) . e).|| is V11() V12() ext-real Element of REAL
xp * ||.((n - (lim n)) . e).|| is V11() V12() ext-real Element of REAL
abs (xp * ||.((n - (lim n)) . e).||) is V11() V12() 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
K340(X,(n . e),(- (lim n))) is Element of the carrier of X
||.((n . e) - (lim n)).|| is V11() V12() ext-real Element of REAL
xp * ||.((n . e) - (lim n)).|| is V11() V12() ext-real Element of REAL
abs (xp * ||.((n . e) - (lim n)).||) is V11() V12() 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
K340(X,((n ^\ 1) . e),(- (n0 . (lim n)))) is Element of the carrier of X
||.(((n ^\ 1) . e) - (n0 . (lim n))).|| is V11() V12() ext-real Element of REAL
e is V4() V5() V6() V10() V11() V12() 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
K340(X,((n ^\ 1) . e),(- (n0 . (lim n)))) is Element of the carrier of X
||.(((n ^\ 1) . e) - (n0 . (lim n))).|| is V11() V12() ext-real 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
K340(X,x,(- xp)) is Element of the carrier of X
||.(x - xp).|| is V11() V12() ext-real Element of REAL
e is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
xp to_power e is V11() V12() ext-real Element of REAL
||.(x - xp).|| * (xp to_power e) is V11() V12() ext-real Element of REAL
e + 1 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
xp to_power (e + 1) is V11() V12() ext-real Element of REAL
||.(x - xp).|| * (xp to_power (e + 1)) is V11() V12() ext-real Element of REAL
xp * ||.(x - xp).|| is V11() V12() ext-real Element of REAL
xp * (||.(x - xp).|| * (xp to_power e)) is V11() V12() 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
K340(X,(n0 . x),(- (n0 . xp))) is Element of the carrier of X
||.((n0 . x) - (n0 . xp)).|| is V11() V12() ext-real Element of REAL
xp * (xp to_power e) is V11() V12() ext-real Element of REAL
||.(x - xp).|| * (xp * (xp to_power e)) is V11() V12() ext-real Element of REAL
xp to_power 1 is V11() V12() ext-real Element of REAL
(xp to_power 1) * (xp to_power e) is V11() V12() ext-real Element of REAL
||.(x - xp).|| * ((xp to_power 1) * (xp to_power e)) is V11() V12() ext-real Element of REAL
||.(x - xp).|| * 1 is V11() V12() ext-real Element of REAL
xp to_power 0 is V11() V12() ext-real Element of REAL
||.(x - xp).|| * (xp to_power 0) is V11() V12() ext-real Element of REAL
e is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
xp to_power e is V11() V12() ext-real Element of REAL
||.(x - xp).|| * (xp to_power e) is V11() V12() ext-real Element of REAL
e is V11() V12() ext-real Element of REAL
n is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
xp to_power n is V11() V12() ext-real Element of REAL
||.(x - xp).|| * (xp to_power n) is V11() V12() ext-real Element of REAL
abs (||.(x - xp).|| * (xp to_power n)) is V11() V12() 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 V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() CNORMSTR
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 V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
iter (f,n0) is Relation-like Function-like set
xp is Element of the carrier of X
(iter (f,n0)) . xp is set
x is Element of the carrier of X
f . x is Element of the carrier of X
n is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
iter (f,n) is Relation-like Function-like set
(iter (f,n)) . x is set
n + 1 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
iter (f,(n + 1)) is Relation-like Function-like set
(iter (f,(n + 1))) . x is set
(iter (f,n)) (#) f is Relation-like Function-like set
((iter (f,n)) (#) f) . x is set
iter (f,0) is Relation-like Function-like set
(iter (f,0)) . x is set
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 V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
iter (f,n) is Relation-like Function-like set
(iter (f,n)) . x is set
(iter (f,n0)) . x is set
f . xp is Element of the carrier of X
(iter (f,n0)) . (f . xp) is set
f (#) (iter (f,n0)) is Relation-like Function-like set
(f (#) (iter (f,n0))) . xp is set
n0 + 1 is V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
iter (f,(n0 + 1)) is Relation-like Function-like set
(iter (f,(n0 + 1))) . xp is set
(iter (f,n0)) (#) f is Relation-like Function-like set
((iter (f,n0)) (#) f) . xp is set