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