:: NCFCONT1 semantic presentation

REAL is non empty V45() V46() V47() V51() V52() set

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

K6(REAL) is set

COMPLEX is non empty V45() V51() V52() set

RAT is non empty V45() V46() V47() V48() V51() V52() set

INT is non empty V45() V46() V47() V48() V49() V51() V52() set

omega is non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() set

K6(omega) 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

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

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

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

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

1r is V11() Element of COMPLEX

- 1r is V11() Element of COMPLEX

CNS is non empty V116() V141() V142() V143() V151() V152() V160() V161() V162() V163() ComplexNormSpace-like CNORMSTR

the carrier of CNS is non empty set

K7(NAT, the carrier of CNS) is set

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

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

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

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

f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

((- 1r) * X) . f is Element of the carrier of CNS

X . f is Element of the carrier of CNS

(- 1r) * (X . f) is Element of the carrier of CNS

- (X . f) is Element of the carrier of CNS

(- X) . f is Element of the carrier of CNS

CNS is non empty V116() V141() V142() V143() V151() V152() V160() V161() V162() V163() ComplexNormSpace-like CNORMSTR

the carrier of CNS is non empty set

K6( the carrier of CNS) is set

X is Element of the carrier of CNS

{ b

x0 is set

p is Element of the carrier of CNS

p - X is Element of the carrier of CNS

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

CNS is non empty V116() V141() V142() V143() V151() V152() V160() V161() V162() V163() ComplexNormSpace-like CNORMSTR

the carrier of CNS is non empty set

X is Element of the carrier of CNS

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

{ b

p is set

x1 is Element of the carrier of CNS

x1 - X is Element of the carrier of CNS

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

CNS is non empty V116() V141() V142() V143() V151() V152() V160() V161() V162() V163() ComplexNormSpace-like CNORMSTR

the carrier of CNS is non empty set

X is Element of the carrier of CNS

f is (CNS,X)

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

{ b

X - X is Element of the carrier of CNS

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

0. CNS is V97(CNS) Element of the carrier of CNS

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

CNS is non empty V116() V141() V142() V143() V151() V152() V160() V161() V162() V163() ComplexNormSpace-like CNORMSTR

the carrier of CNS is non empty set

K6( the carrier of CNS) is set

CNS is non empty V116() V141() V142() V143() V151() V152() V160() V161() V162() V163() ComplexNormSpace-like CNORMSTR

the carrier of CNS is non empty set

K6( the carrier of CNS) is set

CNS is non empty V116() V141() V142() V143() V151() V152() V160() V161() V162() V163() ComplexNormSpace-like CNORMSTR

the carrier of CNS is non empty set

K6( the carrier of CNS) is set

CNS is non empty V116() V141() V142() V143() V151() V152() V160() V161() V162() V163() ComplexNormSpace-like CNORMSTR

the carrier of CNS is non empty set

X is non empty V116() V141() V142() V143() V151() V152() V160() V161() V162() V163() ComplexNormSpace-like CNORMSTR

the carrier of X is non empty set

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

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

CNS is non empty V116() V141() V142() V143() V151() V152() V160() V161() V162() V163() ComplexNormSpace-like CNORMSTR

the carrier of CNS is non empty set

X is non empty V116() V141() V142() V143() V144() V145() V146() V147() V151() V152() RealNormSpace-like NORMSTR

the carrier of X is non empty set

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

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

CNS is non empty V116() V141() V142() V143() V144() V145() V146() V147() V151() V152() RealNormSpace-like NORMSTR

the carrier of CNS is non empty set

X is non empty V116() V141() V142() V143() V151() V152() V160() V161() V162() V163() ComplexNormSpace-like CNORMSTR

the carrier of X is non empty set

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

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

CNS is non empty V116() V141() V142() V143() V151() V152() V160() V161() V162() V163() ComplexNormSpace-like CNORMSTR

the carrier of CNS is non empty set

K7( the carrier of CNS,COMPLEX) is complex-valued set

K6(K7( the carrier of CNS,COMPLEX)) is set

CNS is non empty V116() V141() V142() V143() V151() V152() V160() V161() V162() V163() ComplexNormSpace-like CNORMSTR

the carrier of CNS is non empty set

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

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

CNS is non empty V116() V141() V142() V143() V144() V145() V146() V147() V151() V152() RealNormSpace-like NORMSTR

the carrier of CNS is non empty set

K7( the carrier of CNS,COMPLEX) is complex-valued set

K6(K7( the carrier of CNS,COMPLEX)) is set

CNS is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

X is non empty V116() V141() V142() V143() V151() V152() V160() V161() V162() V163() ComplexNormSpace-like CNORMSTR

the carrier of X is non empty set

K7(NAT, the carrier of X) is set

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

f is non empty V116() V141() V142() V143() V151() V152() V160() V161() V162() V163() ComplexNormSpace-like CNORMSTR

the carrier of f is non empty set

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

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

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

rng x0 is Element of K6( the carrier of X)

K6( the carrier of X) is set

x0 . CNS is Element of the carrier of X

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

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

dom x0 is V45() V46() V47() V48() V49() V50() Element of K6(NAT)

x0 (#) p is Relation-like set

dom (x0 (#) p) is set

CNS is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

X is non empty V116() V141() V142() V143() V151() V152() V160() V161() V162() V163() ComplexNormSpace-like CNORMSTR

the carrier of X is non empty set

K7(NAT, the carrier of X) is set

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

f is non empty V116() V141() V142() V143() V144() V145() V146() V147() V151() V152() RealNormSpace-like NORMSTR

the carrier of f is non empty set

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

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

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

rng x0 is Element of K6( the carrier of X)

K6( the carrier of X) is set

x0 . CNS is Element of the carrier of X

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

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

dom x0 is V45() V46() V47() V48() V49() V50() Element of K6(NAT)

x0 (#) p is Relation-like set

dom (x0 (#) p) is set

CNS is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

X is non empty V116() V141() V142() V143() V151() V152() V160() V161() V162() V163() ComplexNormSpace-like CNORMSTR

the carrier of X is non empty set

f is non empty V116() V141() V142() V143() V144() V145() V146() V147() V151() V152() RealNormSpace-like NORMSTR

the carrier of f is non empty set

K7(NAT, the carrier of f) is set

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

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

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

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

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

K6( the carrier of f) is set

x0 . CNS is Element of the carrier of f

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

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

dom x0 is V45() V46() V47() V48() V49() V50() Element of K6(NAT)

x0 (#) p is Relation-like set

dom (x0 (#) p) is set

CNS is non empty V116() V141() V142() V143() V151() V152() V160() V161() V162() V163() ComplexNormSpace-like CNORMSTR

the carrier of CNS is non empty set

K7(NAT, the carrier of CNS) is set

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

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

rng X is Element of K6( the carrier of CNS)

K6( the carrier of CNS) is set

f is set

dom X is V45() V46() V47() V48() V49() V50() Element of K6(NAT)

x0 is set

X . x0 is set

p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

X . p is Element of the carrier of CNS

x0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

X . x0 is Element of the carrier of CNS

dom X is V45() V46() V47() V48() V49() V50() Element of K6(NAT)

CNS is non empty V116() V141() V142() V143() V151() V152() V160() V161() V162() V163() ComplexNormSpace-like CNORMSTR

the carrier of CNS is non empty set

X is non empty V116() V141() V142() V143() V151() V152() V160() V161() V162() V163() ComplexNormSpace-like CNORMSTR

the carrier of X is non empty set

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

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

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

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

K6( the carrier of CNS) is set

x0 is Element of the carrier of CNS

f /. x0 is Element of the carrier of X

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

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

x1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of REAL

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

(x1 + 1) " is V11() real ext-real positive non negative Element of REAL

x2 is Element of the carrier of CNS

x2 - x0 is Element of the carrier of CNS

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

f /. x2 is Element of the carrier of X

(f /. x2) - (f /. x0) is Element of the carrier of X

||.((f /. x2) - (f /. x0)).|| is V11() real ext-real Element of REAL

K7(NAT, the carrier of CNS) is set

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

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

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

rng x2 is Element of K6( the carrier of CNS)

dom x2 is V45() V46() V47() V48() V49() V50() Element of K6(NAT)

s9 is set

x1 is set

x2 . x1 is set

s9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

x2 . s9 is Element of the carrier of CNS

f /. (x2 . s9) is Element of the carrier of X

(f /. (x2 . s9)) - (f /. x0) is Element of the carrier of X

||.((f /. (x2 . s9)) - (f /. x0)).|| is V11() real ext-real Element of REAL

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

K7(NAT, the carrier of X) is set

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

(f /* x2) . s9 is Element of the carrier of X

((f /* x2) . s9) - (f /. x0) is Element of the carrier of X

||.(((f /* x2) . s9) - (f /. x0)).|| is V11() real ext-real Element of REAL

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

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

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

x1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of REAL

(s9 ") + 0 is V11() real ext-real Element of REAL

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

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

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

x2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

x1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of REAL

x2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of REAL

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

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

x2 . x2 is Element of the carrier of CNS

(x2 . x2) - x0 is Element of the carrier of CNS

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

lim x2 is Element of the carrier of CNS

lim (f /* x2) is Element of the carrier of X

s9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

(f /* x2) . s9 is Element of the carrier of X

((f /* x2) . s9) - (f /. x0) is Element of the carrier of X

||.(((f /* x2) . s9) - (f /. x0)).|| is V11() real ext-real Element of REAL

K7(NAT, the carrier of CNS) is set

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

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

rng p is Element of K6( the carrier of CNS)

lim p is Element of the carrier of CNS

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

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

s9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

p . x1 is Element of the carrier of CNS

(p . x1) - x0 is Element of the carrier of CNS

||.((p . x1) - x0).|| is V11() real ext-real Element of REAL

dom p is V45() V46() V47() V48() V49() V50() Element of K6(NAT)

f /. (p . x1) is Element of the carrier of X

(f /. (p . x1)) - (f /. x0) is Element of the carrier of X

||.((f /. (p . x1)) - (f /. x0)).|| is V11() real ext-real Element of REAL

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

K7(NAT, the carrier of X) is set

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

(f /* p) . x1 is Element of the carrier of X

((f /* p) . x1) - (f /. x0) is Element of the carrier of X

||.(((f /* p) . x1) - (f /. x0)).|| is V11() real ext-real Element of REAL

lim (f /* p) is Element of the carrier of X

CNS is non empty V116() V141() V142() V143() V151() V152() V160() V161() V162() V163() ComplexNormSpace-like CNORMSTR

the carrier of CNS is non empty set

X is non empty V116() V141() V142() V143() V144() V145() V146() V147() V151() V152() RealNormSpace-like NORMSTR

the carrier of X is non empty set

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

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

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

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

K6( the carrier of CNS) is set

x0 is Element of the carrier of CNS

f /. x0 is Element of the carrier of X

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

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

x1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of REAL

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

(x1 + 1) " is V11() real ext-real positive non negative Element of REAL

x2 is Element of the carrier of CNS

x2 - x0 is Element of the carrier of CNS

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

f /. x2 is Element of the carrier of X

(f /. x2) - (f /. x0) is Element of the carrier of X

||.((f /. x2) - (f /. x0)).|| is V11() real ext-real Element of REAL

K7(NAT, the carrier of CNS) is set

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

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

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

rng x2 is Element of K6( the carrier of CNS)

dom x2 is V45() V46() V47() V48() V49() V50() Element of K6(NAT)

s9 is set

x1 is set

x2 . x1 is set

s9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

x2 . s9 is Element of the carrier of CNS

f /. (x2 . s9) is Element of the carrier of X

(f /. (x2 . s9)) - (f /. x0) is Element of the carrier of X

||.((f /. (x2 . s9)) - (f /. x0)).|| is V11() real ext-real Element of REAL

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

K7(NAT, the carrier of X) is set

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

(f /* x2) . s9 is Element of the carrier of X

((f /* x2) . s9) - (f /. x0) is Element of the carrier of X

||.(((f /* x2) . s9) - (f /. x0)).|| is V11() real ext-real Element of REAL

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

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

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

x1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of REAL

(s9 ") + 0 is V11() real ext-real Element of REAL

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

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

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

x2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

x1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of REAL

x2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of REAL

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

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

x2 . x2 is Element of the carrier of CNS

(x2 . x2) - x0 is Element of the carrier of CNS

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

lim x2 is Element of the carrier of CNS

lim (f /* x2) is Element of the carrier of X

s9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

(f /* x2) . s9 is Element of the carrier of X

((f /* x2) . s9) - (f /. x0) is Element of the carrier of X

||.(((f /* x2) . s9) - (f /. x0)).|| is V11() real ext-real Element of REAL

K7(NAT, the carrier of CNS) is set

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

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

rng p is Element of K6( the carrier of CNS)

lim p is Element of the carrier of CNS

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

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

s9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

p . x1 is Element of the carrier of CNS

(p . x1) - x0 is Element of the carrier of CNS

||.((p . x1) - x0).|| is V11() real ext-real Element of REAL

dom p is V45() V46() V47() V48() V49() V50() Element of K6(NAT)

f /. (p . x1) is Element of the carrier of X

(f /. (p . x1)) - (f /. x0) is Element of the carrier of X

||.((f /. (p . x1)) - (f /. x0)).|| is V11() real ext-real Element of REAL

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

K7(NAT, the carrier of X) is set

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

(f /* p) . x1 is Element of the carrier of X

((f /* p) . x1) - (f /. x0) is Element of the carrier of X

||.(((f /* p) . x1) - (f /. x0)).|| is V11() real ext-real Element of REAL

lim (f /* p) is Element of the carrier of X

CNS is non empty V116() V141() V142() V143() V151() V152() V160() V161() V162() V163() ComplexNormSpace-like CNORMSTR

the carrier of CNS is non empty set

X is non empty V116() V141() V142() V143() V144() V145() V146() V147() V151() V152() RealNormSpace-like NORMSTR

the carrier of X is non empty set

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

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

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

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

K6( the carrier of X) is set

x0 is Element of the carrier of X

f /. x0 is Element of the carrier of CNS

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

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

x1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of REAL

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

(x1 + 1) " is V11() real ext-real positive non negative Element of REAL

x2 is Element of the carrier of X

x2 - x0 is Element of the carrier of X

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

f /. x2 is Element of the carrier of CNS

(f /. x2) - (f /. x0) is Element of the carrier of CNS

||.((f /. x2) - (f /. x0)).|| is V11() real ext-real Element of REAL

K7(NAT, the carrier of X) is set

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

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

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

rng x2 is Element of K6( the carrier of X)

dom x2 is V45() V46() V47() V48() V49() V50() Element of K6(NAT)

s9 is set

x1 is set

x2 . x1 is set

s9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

x2 . s9 is Element of the carrier of X

f /. (x2 . s9) is Element of the carrier of CNS

(f /. (x2 . s9)) - (f /. x0) is Element of the carrier of CNS

||.((f /. (x2 . s9)) - (f /. x0)).|| is V11() real ext-real Element of REAL

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

K7(NAT, the carrier of CNS) is set

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

(f /* x2) . s9 is Element of the carrier of CNS

((f /* x2) . s9) - (f /. x0) is Element of the carrier of CNS

||.(((f /* x2) . s9) - (f /. x0)).|| is V11() real ext-real Element of REAL

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

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

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

x1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of REAL

(s9 ") + 0 is V11() real ext-real Element of REAL

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

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

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

x2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

x1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of REAL

x2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of REAL

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

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

x2 . x2 is Element of the carrier of X

(x2 . x2) - x0 is Element of the carrier of X

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

lim x2 is Element of the carrier of X

lim (f /* x2) is Element of the carrier of CNS

s9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

(f /* x2) . s9 is Element of the carrier of CNS

((f /* x2) . s9) - (f /. x0) is Element of the carrier of CNS

||.(((f /* x2) . s9) - (f /. x0)).|| is V11() real ext-real Element of REAL

K7(NAT, the carrier of X) is set

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

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

rng p is Element of K6( the carrier of X)

lim p is Element of the carrier of X

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

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

s9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

p . x1 is Element of the carrier of X

(p . x1) - x0 is Element of the carrier of X

||.((p . x1) - x0).|| is V11() real ext-real Element of REAL

dom p is V45() V46() V47() V48() V49() V50() Element of K6(NAT)

f /. (p . x1) is Element of the carrier of CNS

(f /. (p . x1)) - (f /. x0) is Element of the carrier of CNS

||.((f /. (p . x1)) - (f /. x0)).|| is V11() real ext-real Element of REAL

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

K7(NAT, the carrier of CNS) is set

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

(f /* p) . x1 is Element of the carrier of CNS

((f /* p) . x1) - (f /. x0) is Element of the carrier of CNS

||.(((f /* p) . x1) - (f /. x0)).|| is V11() real ext-real Element of REAL

lim (f /* p) is Element of the carrier of CNS

CNS is non empty V116() V141() V142() V143() V151() V152() V160() V161() V162() V163() ComplexNormSpace-like CNORMSTR

the carrier of CNS is non empty set

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

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

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

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

K6( the carrier of CNS) is set

f is Element of the carrier of CNS

X /. f is V11() real ext-real Element of REAL

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

p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

p + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of REAL

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

(p + 1) " is V11() real ext-real positive non negative Element of REAL

x1 is Element of the carrier of CNS

x1 - f is Element of the carrier of CNS

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

X /. x1 is V11() real ext-real Element of REAL

(X /. x1) - (X /. f) is V11() real ext-real Element of REAL

abs ((X /. x1) - (X /. f)) is V11() real ext-real Element of REAL

K7(NAT, the carrier of CNS) is set

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

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

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

rng x1 is Element of K6( the carrier of CNS)

dom x1 is V45() V46() V47() V48() V49() V50() Element of K6(NAT)

x2 is set

s9 is set

x1 . s9 is set

x2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

x1 . x2 is Element of the carrier of CNS

X /. (x1 . x2) is V11() real ext-real Element of REAL

(X /. (x1 . x2)) - (X /. f) is V11() real ext-real Element of REAL

abs ((X /. (x1 . x2)) - (X /. f)) is V11() real ext-real Element of REAL

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

(X /* x1) . x2 is V11() real ext-real Element of REAL

((X /* x1) . x2) - (X /. f) is V11() real ext-real Element of REAL

abs (((X /* x1) . x2) - (X /. f)) is V11() real ext-real Element of REAL

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

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

s9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

s9 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of REAL

(x2 ") + 0 is V11() real ext-real Element of REAL

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

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

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

x1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of REAL

x1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of REAL

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

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

x1 . x1 is Element of the carrier of CNS

(x1 . x1) - f is Element of the carrier of CNS

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

lim x1 is Element of the carrier of CNS

lim (X /* x1) is V11() real ext-real Element of REAL

x2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

(X /* x1) . x2 is V11() real ext-real Element of REAL

((X /* x1) . x2) - (X /. f) is V11() real ext-real Element of REAL

abs (((X /* x1) . x2) - (X /. f)) is V11() real ext-real Element of REAL

K7(NAT, the carrier of CNS) is set

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

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

rng x0 is Element of K6( the carrier of CNS)

lim x0 is Element of the carrier of CNS

p is V11() real ext-real set

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

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

s9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

x0 . x1 is Element of the carrier of CNS

(x0 . x1) - f is Element of the carrier of CNS

||.((x0 . x1) - f).|| is V11() real ext-real Element of REAL

dom x0 is V45() V46() V47() V48() V49() V50() Element of K6(NAT)

X /. (x0 . x1) is V11() real ext-real Element of REAL

(X /. (x0 . x1)) - (X /. f) is V11() real ext-real Element of REAL

abs ((X /. (x0 . x1)) - (X /. f)) is V11() real ext-real Element of REAL

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

(X /* x0) . x1 is V11() real ext-real Element of REAL

((X /* x0) . x1) - (X /. f) is V11() real ext-real Element of REAL

abs (((X /* x0) . x1) - (X /. f)) is V11() real ext-real Element of REAL

lim (X /* x0) is V11() real ext-real Element of REAL

CNS is non empty V116() V141() V142() V143() V151() V152() V160() V161() V162() V163() ComplexNormSpace-like CNORMSTR

the carrier of CNS is non empty set

K7( the carrier of CNS,COMPLEX) is complex-valued set

K6(K7( the carrier of CNS,COMPLEX)) is set

X is Relation-like the carrier of CNS -defined COMPLEX -valued Function-like complex-valued Element of K6(K7( the carrier of CNS,COMPLEX))

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

K6( the carrier of CNS) is set

f is Element of the carrier of CNS

X /. f is V11() Element of COMPLEX

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

p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

p + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of REAL

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

(p + 1) " is V11() real ext-real positive non negative Element of REAL

x1 is Element of the carrier of CNS

x1 - f is Element of the carrier of CNS

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

X /. x1 is V11() Element of COMPLEX

(X /. x1) - (X /. f) is V11() Element of COMPLEX

|.((X /. x1) - (X /. f)).| is V11() real ext-real Element of REAL

K7(NAT, the carrier of CNS) is set

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

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

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

rng x1 is Element of K6( the carrier of CNS)

dom x1 is V45() V46() V47() V48() V49() V50() Element of K6(NAT)

x2 is set

s9 is set

x1 . s9 is set

x2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

x1 . x2 is Element of the carrier of CNS

X /. (x1 . x2) is V11() Element of COMPLEX

(X /. (x1 . x2)) - (X /. f) is V11() Element of COMPLEX

|.((X /. (x1 . x2)) - (X /. f)).| is V11() real ext-real Element of REAL

X /* x1 is non empty Relation-like NAT -defined COMPLEX -valued Function-like total quasi_total complex-valued Element of K6(K7(NAT,COMPLEX))

(X /* x1) . x2 is V11() Element of COMPLEX

((X /* x1) . x2) - (X /. f) is V11() Element of COMPLEX

|.(((X /* x1) . x2) - (X /. f)).| is V11() real ext-real Element of REAL

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

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

s9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

s9 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of REAL

(x2 ") + 0 is V11() real ext-real Element of REAL

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

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

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

x1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of REAL

x1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of REAL

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

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

x1 . x1 is Element of the carrier of CNS

(x1 . x1) - f is Element of the carrier of CNS

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

lim x1 is Element of the carrier of CNS

lim (X /* x1) is V11() Element of COMPLEX

x2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

(X /* x1) . x2 is V11() Element of COMPLEX

((X /* x1) . x2) - (X /. f) is V11() Element of COMPLEX

|.(((X /* x1) . x2) - (X /. f)).| is V11() real ext-real Element of REAL

K7(NAT, the carrier of CNS) is set

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

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

rng x0 is Element of K6( the carrier of CNS)

lim x0 is Element of the carrier of CNS

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

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

x2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

s9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

x0 . x1 is Element of the carrier of CNS

(x0 . x1) - f is Element of the carrier of CNS

||.((x0 . x1) - f).|| is V11() real ext-real Element of REAL

dom x0 is V45() V46() V47() V48() V49() V50() Element of K6(NAT)

X /. (x0 . x1) is V11() Element of COMPLEX

(X /. (x0 . x1)) - (X /. f) is V11() Element of COMPLEX

|.((X /. (x0 . x1)) - (X /. f)).| is V11() real ext-real Element of REAL

X /* x0 is non empty Relation-like NAT -defined COMPLEX -valued Function-like total quasi_total complex-valued Element of K6(K7(NAT,COMPLEX))

(X /* x0) . x1 is V11() Element of COMPLEX

((X /* x0) . x1) - (X /. f) is V11() Element of COMPLEX

|.(((X /* x0) . x1) - (X /. f)).| is V11() real ext-real Element of REAL

lim (X /* x0) is V11() Element of COMPLEX

CNS is non empty V116() V141() V142() V143() V144() V145() V146() V147() V151() V152() RealNormSpace-like NORMSTR

the carrier of CNS is non empty set

K7( the carrier of CNS,COMPLEX) is complex-valued set

K6(K7( the carrier of CNS,COMPLEX)) is set

X is Relation-like the carrier of CNS -defined COMPLEX -valued Function-like complex-valued Element of K6(K7( the carrier of CNS,COMPLEX))

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

K6( the carrier of CNS) is set

f is Element of the carrier of CNS

X /. f is V11() Element of COMPLEX

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

p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

p + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of REAL

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

(p + 1) " is V11() real ext-real positive non negative Element of REAL

x1 is Element of the carrier of CNS

x1 - f is Element of the carrier of CNS

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

X /. x1 is V11() Element of COMPLEX

(X /. x1) - (X /. f) is V11() Element of COMPLEX

|.((X /. x1) - (X /. f)).| is V11() real ext-real Element of REAL

K7(NAT, the carrier of CNS) is set

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

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

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

rng x1 is Element of K6( the carrier of CNS)

dom x1 is V45() V46() V47() V48() V49() V50() Element of K6(NAT)

x2 is set

s9 is set

x1 . s9 is set

x2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

x1 . x2 is Element of the carrier of CNS

X /. (x1 . x2) is V11() Element of COMPLEX

(X /. (x1 . x2)) - (X /. f) is V11() Element of COMPLEX

|.((X /. (x1 . x2)) - (X /. f)).| is V11() real ext-real Element of REAL

X /* x1 is non empty Relation-like NAT -defined COMPLEX -valued Function-like total quasi_total complex-valued Element of K6(K7(NAT,COMPLEX))

(X /* x1) . x2 is V11() Element of COMPLEX

((X /* x1) . x2) - (X /. f) is V11() Element of COMPLEX

|.(((X /* x1) . x2) - (X /. f)).| is V11() real ext-real Element of REAL

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

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

s9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

s9 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of REAL

(x2 ") + 0 is V11() real ext-real Element of REAL

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

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

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

x1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of REAL

x1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of REAL

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

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

x1 . x1 is Element of the carrier of CNS

(x1 . x1) - f is Element of the carrier of CNS

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

lim x1 is Element of the carrier of CNS

lim (X /* x1) is V11() Element of COMPLEX

x2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

(X /* x1) . x2 is V11() Element of COMPLEX

((X /* x1) . x2) - (X /. f) is V11() Element of COMPLEX

|.(((X /* x1) . x2) - (X /. f)).| is V11() real ext-real Element of REAL

K7(NAT, the carrier of CNS) is set

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

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

rng x0 is Element of K6( the carrier of CNS)

lim x0 is Element of the carrier of CNS

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

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

x2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

s9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

x0 . x1 is Element of the carrier of CNS

(x0 . x1) - f is Element of the carrier of CNS

||.((x0 . x1) - f).|| is V11() real ext-real Element of REAL

dom x0 is V45() V46() V47() V48() V49() V50() Element of K6(NAT)

X /. (x0 . x1) is V11() Element of COMPLEX

(X /. (x0 . x1)) - (X /. f) is V11() Element of COMPLEX

|.((X /. (x0 . x1)) - (X /. f)).| is V11() real ext-real Element of REAL

X /* x0 is non empty Relation-like NAT -defined COMPLEX -valued Function-like total quasi_total complex-valued Element of K6(K7(NAT,COMPLEX))

(X /* x0) . x1 is V11() Element of COMPLEX

((X /* x0) . x1) - (X /. f) is V11() Element of COMPLEX

|.(((X /* x0) . x1) - (X /. f)).| is V11() real ext-real Element of REAL

lim (X /* x0) is V11() Element of COMPLEX

CNS is non empty V116() V141() V142() V143() V151() V152() V160() V161() V162() V163() ComplexNormSpace-like CNORMSTR

the carrier of CNS is non empty set

X is non empty V116() V141() V142() V143() V151() V152() V160() V161() V162() V163() ComplexNormSpace-like CNORMSTR

the carrier of X is non empty set

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

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

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

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

K6( the carrier of CNS) is set

x0 is Element of the carrier of CNS

f /. x0 is Element of the carrier of X

p is (X,f /. x0)

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

{ b

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

{ b

s9 is (CNS,x0)

x1 is Element of the carrier of CNS

f /. x1 is Element of the carrier of X

(f /. x1) - (f /. x0) is Element of the carrier of X

||.((f /. x1) - (f /. x0)).|| is V11() real ext-real Element of REAL

x1 is Element of the carrier of CNS

x1 - x0 is Element of the carrier of CNS

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

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

{ b

x1 is (X,f /. x0)

x2 is (CNS,x0)

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

{ b

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

x1 is Element of the carrier of CNS

x1 - x0 is Element of the carrier of CNS

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

f /. x1 is Element of the carrier of X

(f /. x1) - (f /. x0) is Element of the carrier of X

||.((f /. x1) - (f /. x0)).|| is V11() real ext-real Element of REAL

{ b

x2 is Element of the carrier of X

x2 - (f /. x0) is Element of the carrier of X

||.(x2 - (f /. x0)).|| is V11() real ext-real Element of REAL

x1 is Element of the carrier of CNS

x1 - x0 is Element of the carrier of CNS

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

f /. x1 is Element of the carrier of X

(f /. x1) - (f /. x0) is Element of the carrier of X

||.((f /. x1) - (f /. x0)).|| is V11() real ext-real Element of REAL

CNS is non empty V116() V141() V142() V143() V151() V152() V160() V161() V162() V163() ComplexNormSpace-like CNORMSTR

the carrier of CNS is non empty set

X is non empty V116() V141() V142() V143() V144() V145() V146() V147() V151() V152() RealNormSpace-like NORMSTR

the carrier of X is non empty set

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

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

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

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

K6( the carrier of CNS) is set

x0 is Element of the carrier of CNS

f /. x0 is Element of the carrier of X

p is Neighbourhood of f /. x0

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

{ b

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

{ b

s9 is (CNS,x0)

x1 is Element of the carrier of CNS

f /. x1 is Element of the carrier of X

(f /. x1) - (f /. x0) is Element of the carrier of X

||.((f /. x1) - (f /. x0)).|| is V11() real ext-real Element of REAL

x1 is Element of the carrier of CNS

x1 - x0 is Element of the carrier of CNS

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

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

{ b

x1 is Neighbourhood of f /. x0

x2 is (CNS,x0)

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

{ b

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

x1 is Element of the carrier of CNS

x1 - x0 is Element of the carrier of CNS

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

f /. x1 is Element of the carrier of X

(f /. x1) - (f /. x0) is Element of the carrier of X

||.((f /. x1) - (f /. x0)).|| is V11() real ext-real Element of REAL

{ b

x2 is Element of the carrier of X

x2 - (f /. x0) is Element of the carrier of X

||.(x2 - (f /. x0)).|| is V11() real ext-real Element of REAL

x1 is Element of the carrier of CNS

x1 - x0 is Element of the carrier of CNS

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

f /. x1 is Element of the carrier of X

(f /. x1) - (f /. x0) is Element of the carrier of X

||.((f /. x1) - (f /. x0)).|| is V11() real ext-real Element of REAL

CNS is non empty V116() V141() V142() V143() V151() V152() V160() V161() V162() V163() ComplexNormSpace-like CNORMSTR

the carrier of CNS is non empty set

X is non empty V116() V141() V142() V143() V144() V145() V146() V147() V151() V152() RealNormSpace-like NORMSTR

the carrier of X is non empty set

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

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

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

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

K6( the carrier of X) is set

x0 is Element of the carrier of X

f /. x0 is Element of the carrier of CNS

p is (CNS,f /. x0)

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

{ b

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

{ b

s9 is Neighbourhood of x0

x1 is Element of the carrier of X

f /. x1 is Element of the carrier of CNS

(f /. x1) - (f /. x0) is Element of the carrier of CNS

||.((f /. x1) - (f /. x0)).|| is V11() real ext-real Element of REAL

x1 is Element of the carrier of X

x1 - x0 is Element of the carrier of X

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

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

{ b

x1 is (CNS,f /. x0)

x2 is Neighbourhood of x0

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

{ b

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

x1 is Element of the carrier of X

x1 - x0 is Element of the carrier of X

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

f /. x1 is Element of the carrier of CNS

(f /. x1) - (f /. x0) is Element of the carrier of CNS

||.((f /. x1) - (f /. x0)).|| is V11() real ext-real Element of REAL

{ b

x2 is Element of the carrier of CNS

x2 - (f /. x0) is Element of the carrier of CNS

||.(x2 - (f /. x0)).|| is V11() real ext-real Element of REAL

x1 is Element of the carrier of X

x1 - x0 is Element of the carrier of X

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

f /. x1 is Element of the carrier of CNS

(f /. x1) - (f /. x0) is Element of the carrier of CNS

||.((f /. x1) - (f /. x0)).|| is V11() real ext-real Element of REAL

CNS is non empty V116() V141() V142() V143() V151() V152() V160() V161() V162() V163() ComplexNormSpace-like CNORMSTR

the carrier of CNS is non empty set

X is non empty V116() V141() V142() V143() V151() V152() V160() V161() V162() V163() ComplexNormSpace-like CNORMSTR

the carrier of X is non empty set

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

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

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

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

K6( the carrier of CNS) is set

x0 is Element of the carrier of CNS

f /. x0 is Element of the carrier of X

p is (X,f /. x0)

x1 is (CNS,x0)

f .: x1 is Element of K6( the carrier of X)

K6( the carrier of X) is set

x2 is set

s9 is Element of the carrier of CNS

f . s9 is set

f /. s9 is Element of the carrier of X

p is (X,f /. x0)

x1 is (CNS,x0)

f .: x1 is Element of K6( the carrier of X)

K6( the carrier of X) is set

s9 is Element of the carrier of CNS

x2 is (CNS,x0)

f . s9 is set

f .: x2 is Element of K6( the carrier of X)

f /. s9 is Element of the carrier of X

CNS is non empty V116() V141() V142() V143() V151() V152() V160() V161() V162() V163() ComplexNormSpace-like CNORMSTR

the carrier of CNS is non empty set

X is non empty V116() V141() V142() V143() V144() V145() V146() V147() V151() V152() RealNormSpace-like NORMSTR

the carrier of X is non empty set

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

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

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

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

K6( the carrier of CNS) is set

x0 is Element of the carrier of CNS

f /. x0 is Element of the carrier of X

p is Neighbourhood of f /. x0

x1 is (CNS,x0)

f .: x1 is Element of K6( the carrier of X)

K6( the carrier of X) is set

x2 is set

s9 is Element of the carrier of CNS

f . s9 is set

f /. s9 is Element of the carrier of X

p is Neighbourhood of f /. x0

x1 is (CNS,x0)

f .: x1 is Element of K6( the carrier of X)

K6( the carrier of X) is set

s9 is Element of the carrier of CNS

x2 is (CNS,x0)

f . s9 is set

f .: x2 is Element of K6( the carrier of X)

f /. s9 is Element of the carrier of X

CNS is non empty V116() V141() V142() V143() V151() V152() V160() V161() V162() V163() ComplexNormSpace-like CNORMSTR

the carrier of CNS is non empty set

X is non empty V116() V141() V142() V143() V144() V145() V146() V147() V151() V152() RealNormSpace-like NORMSTR

the carrier of X is non empty set

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

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

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

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

K6( the carrier of X) is set

x0 is Element of the carrier of X

f /. x0 is Element of the carrier of CNS

p is (CNS,f /. x0)

x1 is Neighbourhood of x0

f .: x1 is Element of K6( the carrier of CNS)

K6( the carrier of CNS) is set

x2 is set

s9 is Element of the carrier of X

f . s9 is set

f /. s9 is Element of the carrier of CNS

p is (CNS,f /. x0)

x1 is Neighbourhood of x0

f .: x1 is Element of K6( the carrier of CNS)

K6( the carrier of CNS) is set

s9 is Element of the carrier of X

x2 is Neighbourhood of x0

f . s9 is set

f .: x2 is Element of K6( the carrier of CNS)

f /. s9 is Element of the carrier of CNS

CNS is non empty V116() V141() V142() V143() V151() V152() V160() V161() V162() V163() ComplexNormSpace-like CNORMSTR

the carrier of CNS is non empty set

X is non empty V116() V141() V142() V143() V151() V152() V160() V161() V162() V163() ComplexNormSpace-like CNORMSTR

the carrier of X is non empty set

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

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

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

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

K6( the carrier of CNS) is set

x0 is Element of the carrier of CNS

{x0} is non empty set

p is (CNS,x0)

(dom f) /\ p is Element of K6( the carrier of CNS)

f /. x0 is Element of the carrier of X

x1 is (X,f /. x0)

x2 is (CNS,x0)

f .: x2 is Element of K6( the carrier of X)

K6( the carrier of X) is set

Im (f,x0) is set

f .: {x0} is set

f . x0 is set

{(f . x0)} is non empty set

{(f /. x0)} is non empty set

CNS is non empty V116() V141() V142() V143() V151() V152() V160() V161() V162() V163() ComplexNormSpace-like CNORMSTR

the carrier of CNS is non empty set

X is non empty V116() V141() V142() V143() V144() V145() V146() V147() V151() V152() RealNormSpace-like NORMSTR

the carrier of X is non empty set

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

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

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

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

K6( the carrier of CNS) is set

x0 is Element of the carrier of CNS

{x0} is non empty set

p is (CNS,x0)

(dom f) /\ p is Element of K6( the carrier of CNS)

f /. x0 is Element of the carrier of X

x1 is Neighbourhood of f /. x0

x2 is (CNS,x0)

f .: x2 is Element of K6( the carrier of X)

K6( the carrier of X) is set

Im (f,x0) is set

f .: {x0} is set

f . x0 is set

{(f . x0)} is non empty set

{(f /. x0)} is non empty set

CNS is non empty V116() V141() V142() V143() V151() V152() V160() V161() V162() V163() ComplexNormSpace-like CNORMSTR

the carrier of CNS is non empty set

X is non empty V116() V141() V142() V143() V144() V145() V146() V147() V151() V152() RealNormSpace-like NORMSTR

the carrier of X is non empty set

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

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

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

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

K6( the carrier of X) is set

x0 is Element of the carrier of X

{x0} is non empty set

p is Neighbourhood of x0

(dom f) /\ p is Element of K6( the carrier of X)

f /. x0 is Element of the carrier of CNS

x1 is (CNS,f /. x0)

x2 is Neighbourhood of x0

f .: x2 is Element of K6( the carrier of CNS)

K6( the carrier of CNS) is set

Im (f,x0) is set

f .: {x0} is set

f . x0 is set

{(f . x0)} is non empty set

{(f /. x0)} is non empty set

CNS is non empty V116() V141() V142() V143() V151() V152() V160() V161() V162() V163() ComplexNormSpace-like CNORMSTR

the carrier of CNS is non empty set

K7(NAT, the carrier of CNS) is set

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

X is non empty V116() V141() V142() V143() V151() V152() V160() V161() V162() V163() ComplexNormSpace-like CNORMSTR

the carrier of X is non empty set

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

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

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

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

K6( the carrier of CNS) is set

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

dom x0 is Element of K6( the carrier of CNS)

(dom f) /\ (dom x0) is Element of K6( the carrier of CNS)

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

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

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

rng p is Element of K6( the carrier of CNS)

(f + x0) /* p is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))

K7(NAT, the carrier of X) is set

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

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

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

(f /* p) + (x0 /* p) is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))

(f - x0) /* p is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))

(f /* p) - (x0 /* p) is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))

dom (f + x0) is Element of K6( the carrier of CNS)

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

p . x1 is Element of the carrier of CNS

((f + x0) /* p) . x1 is Element of the carrier of X

(f + x0) /. (p . x1) is Element of the carrier of X

f /. (p . x1) is Element of the carrier of X

x0 /. (p . x1) is Element of the carrier of X

(f /. (p . x1)) + (x0 /. (p . x1)) is Element of the carrier of X

(f /* p) . x1 is Element of the carrier of X

((f /* p) . x1) + (x0 /. (p . x1)) is Element of the carrier of X

(x0 /* p) . x1 is Element of the carrier of X

((f /* p) . x1) + ((x0 /* p) . x1) is Element of the carrier of X

dom (f - x0) is Element of K6( the carrier of CNS)

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

p . x1 is Element of the carrier of CNS

((f - x0) /* p) . x1 is Element of the carrier of X

(f - x0) /. (p . x1) is Element of the carrier of X

f /. (p . x1) is Element of the carrier of X

x0 /. (p . x1) is Element of the carrier of X

(f /. (p . x1)) - (x0 /. (p . x1)) is Element of the carrier of X

(f /* p) . x1 is Element of the carrier of X

((f /* p) . x1) - (x0 /. (p . x1)) is Element of the carrier of X

(x0 /* p) . x1 is Element of the carrier of X

((f /* p) . x1) - ((x0 /* p) . x1) is Element of the carrier of X

CNS is non empty V116() V141() V142() V143() V151() V152() V160() V161() V162() V163() ComplexNormSpace-like CNORMSTR

the carrier of CNS is non empty set

K7(NAT, the carrier of CNS) is set

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

X is non empty V116() V141() V142() V143() V144() V145() V146() V147() V151() V152() RealNormSpace-like NORMSTR

the carrier of X is non empty set

K7( the