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