:: NFCONT_4 semantic presentation

REAL is non empty non finite non bounded_below non bounded_above V68() set

NAT is non empty epsilon-transitive epsilon-connected ordinal Element of bool REAL

bool REAL is set

K251(REAL) is non empty functional FinSequence-membered M12( REAL )

[:NAT,K251(REAL):] is set

bool [:NAT,K251(REAL):] is set

COMPLEX is non empty non finite set

RAT is non empty non finite set

INT is non empty non finite set

omega is non empty epsilon-transitive epsilon-connected ordinal set

bool omega is set

bool NAT is set

[:COMPLEX,COMPLEX:] is set

bool [:COMPLEX,COMPLEX:] is set

[:COMPLEX,REAL:] is set

bool [:COMPLEX,REAL:] is set

[:REAL,REAL:] is set

bool [:REAL,REAL:] is set

[:NAT,REAL:] is set

bool [:NAT,REAL:] is set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is set

[:[:REAL,REAL:],REAL:] is set

bool [:[:REAL,REAL:],REAL:] is set

[:RAT,RAT:] is set

bool [:RAT,RAT:] is set

[:[:RAT,RAT:],RAT:] is set

bool [:[:RAT,RAT:],RAT:] is set

[:INT,INT:] is set

bool [:INT,INT:] is set

[:[:INT,INT:],INT:] is set

bool [:[:INT,INT:],INT:] is set

[:NAT,NAT:] is set

[:[:NAT,NAT:],NAT:] is set

bool [:[:NAT,NAT:],NAT:] is set

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

[:1,1:] is set

bool [:1,1:] is set

[:[:1,1:],1:] is set

bool [:[:1,1:],1:] is set

[:[:1,1:],REAL:] is set

bool [:[:1,1:],REAL:] is set

2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

[:2,2:] is set

[:[:2,2:],REAL:] is set

bool [:[:2,2:],REAL:] is set

K489(2) is non empty V106() V131() V132() V133() V134() V135() V136() V137() TopSpace-like V206() L20()

the carrier of K489(2) is non empty set

REAL 1 is non empty functional FinSequence-membered V227() V228() V229() M12( REAL )

[:(REAL 1),(REAL 1):] is set

bool [:(REAL 1),(REAL 1):] is set

REAL-NS 1 is non empty non trivial V106() V131() V132() V133() V134() V135() V136() V137() V141() V142() strict RealNormSpace-like V174() NORMSTR

the carrier of (REAL-NS 1) is non empty non trivial set

K434((REAL-NS 1),(REAL-NS 1)) is non empty NORMSTR

the carrier of K434((REAL-NS 1),(REAL-NS 1)) is non empty set

ExtREAL is non empty V68() set

{} is empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional FinSequence-membered V227() V228() V229() V230() V231() V232() set

3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

0 is empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional FinSequence-membered V227() V228() V229() V230() V231() V232() Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

REAL n is non empty functional FinSequence-membered V227() V228() V229() M12( REAL )

[:REAL,(REAL n):] is set

bool [:REAL,(REAL n):] is set

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

REAL n is non empty functional FinSequence-membered V227() V228() V229() M12( REAL )

[:REAL,(REAL n):] is set

bool [:REAL,(REAL n):] is set

REAL-NS n is non empty V106() V131() V132() V133() V134() V135() V136() V137() V141() V142() strict RealNormSpace-like V174() NORMSTR

the carrier of (REAL-NS n) is non empty set

[:REAL, the carrier of (REAL-NS n):] is set

bool [:REAL, the carrier of (REAL-NS n):] is set

h is V11() real ext-real set

x0 is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]

i is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of bool [:REAL, the carrier of (REAL-NS n):]

r is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of bool [:REAL, the carrier of (REAL-NS n):]

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

REAL n is non empty functional FinSequence-membered V227() V228() V229() M12( REAL )

[:REAL,(REAL n):] is set

bool [:REAL,(REAL n):] is set

h is set

x0 is V11() real ext-real set

i is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]

i | h is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]

REAL-NS n is non empty V106() V131() V132() V133() V134() V135() V136() V137() V141() V142() strict RealNormSpace-like V174() NORMSTR

the carrier of (REAL-NS n) is non empty set

[:REAL, the carrier of (REAL-NS n):] is set

bool [:REAL, the carrier of (REAL-NS n):] is set

r is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of bool [:REAL, the carrier of (REAL-NS n):]

r | h is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of bool [:REAL, the carrier of (REAL-NS n):]

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

REAL n is non empty functional FinSequence-membered V227() V228() V229() M12( REAL )

[:REAL,(REAL n):] is set

bool [:REAL,(REAL n):] is set

h is V11() real ext-real set

x0 is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]

dom x0 is Element of bool REAL

x0 /. h is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

REAL-NS n is non empty V106() V131() V132() V133() V134() V135() V136() V137() V141() V142() strict RealNormSpace-like V174() NORMSTR

the carrier of (REAL-NS n) is non empty set

[:REAL, the carrier of (REAL-NS n):] is set

bool [:REAL, the carrier of (REAL-NS n):] is set

i is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of bool [:REAL, the carrier of (REAL-NS n):]

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

dom i is Element of bool REAL

i /. h is Element of the carrier of (REAL-NS n)

s0 is V11() real ext-real set

rs0 is V11() real ext-real set

rs0 - h is V11() real ext-real Element of REAL

abs (rs0 - h) is V11() real ext-real Element of REAL

x0 /. rs0 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

(x0 /. rs0) - (x0 /. h) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like M13( REAL , REAL n)

- (x0 /. h) is Relation-like Function-like V33() set

K38(1) is V11() real ext-real non positive set

K38(1) (#) (x0 /. h) is Relation-like Function-like set

(x0 /. rs0) + (- (x0 /. h)) is Relation-like Function-like set

|.((x0 /. rs0) - (x0 /. h)).| is V11() real ext-real non negative Element of REAL

i /. rs0 is Element of the carrier of (REAL-NS n)

(i /. rs0) - (i /. h) is Element of the carrier of (REAL-NS n)

||.((i /. rs0) - (i /. h)).|| is V11() real ext-real Element of REAL

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

s0 is V11() real ext-real set

rs0 is V11() real ext-real set

rs0 is V11() real ext-real set

i is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of bool [:REAL, the carrier of (REAL-NS n):]

dom i is Element of bool REAL

rs0 - h is V11() real ext-real Element of REAL

abs (rs0 - h) is V11() real ext-real Element of REAL

x0 /. rs0 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

(x0 /. rs0) - (x0 /. h) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like M13( REAL , REAL n)

- (x0 /. h) is Relation-like Function-like V33() set

K38(1) is V11() real ext-real non positive set

K38(1) (#) (x0 /. h) is Relation-like Function-like set

(x0 /. rs0) + (- (x0 /. h)) is Relation-like Function-like set

|.((x0 /. rs0) - (x0 /. h)).| is V11() real ext-real non negative Element of REAL

i /. rs0 is Element of the carrier of (REAL-NS n)

i /. h is Element of the carrier of (REAL-NS n)

(i /. rs0) - (i /. h) is Element of the carrier of (REAL-NS n)

||.((i /. rs0) - (i /. h)).|| is V11() real ext-real Element of REAL

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

REAL n is non empty functional FinSequence-membered V227() V228() V229() M12( REAL )

REAL-NS n is non empty V106() V131() V132() V133() V134() V135() V136() V137() V141() V142() strict RealNormSpace-like V174() NORMSTR

the carrier of (REAL-NS n) is non empty set

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

x0 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

{ b

i is Element of the carrier of (REAL-NS n)

{ b

rs0 is set

rs0 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

rs0 - x0 is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like M13( REAL , REAL n)

- x0 is Relation-like Function-like V33() set

K38(1) is V11() real ext-real non positive set

K38(1) (#) x0 is Relation-like Function-like set

rs0 + (- x0) is Relation-like Function-like set

|.(rs0 - x0).| is V11() real ext-real non negative Element of REAL

s is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

i1 is Element of the carrier of (REAL-NS n)

i1 - i is Element of the carrier of (REAL-NS n)

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

rs0 is set

rs0 is Element of the carrier of (REAL-NS n)

rs0 - i is Element of the carrier of (REAL-NS n)

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

s is Element of the carrier of (REAL-NS n)

i1 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

i1 - x0 is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like M13( REAL , REAL n)

- x0 is Relation-like Function-like V33() set

K38(1) is V11() real ext-real non positive set

K38(1) (#) x0 is Relation-like Function-like set

i1 + (- x0) is Relation-like Function-like set

|.(i1 - x0).| is V11() real ext-real non negative Element of REAL

h is set

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

REAL n is non empty functional FinSequence-membered V227() V228() V229() M12( REAL )

[:h,(REAL n):] is set

bool [:h,(REAL n):] is set

x0 is Relation-like h -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:h,(REAL n):]

[:h,REAL:] is set

bool [:h,REAL:] is set

dom x0 is Element of bool h

bool h is set

i is Relation-like Function-like set

dom i is set

r is set

rng i is set

s0 is set

i . s0 is set

x0 /. s0 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

|.(x0 /. s0).| is V11() real ext-real non negative Element of REAL

PFuncs (h,REAL) is set

r is Relation-like h -defined REAL -valued Function-like V33() V34() V35() Element of bool [:h,REAL:]

dom r is Element of bool h

s0 is set

r /. s0 is V11() real ext-real Element of REAL

x0 /. s0 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

|.(x0 /. s0).| is V11() real ext-real non negative Element of REAL

r . s0 is V11() real ext-real Element of REAL

i is Relation-like h -defined REAL -valued Function-like V33() V34() V35() Element of bool [:h,REAL:]

dom i is Element of bool h

r is Relation-like h -defined REAL -valued Function-like V33() V34() V35() Element of bool [:h,REAL:]

dom r is Element of bool h

s0 is Element of h

i /. s0 is V11() real ext-real Element of REAL

x0 /. s0 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

|.(x0 /. s0).| is V11() real ext-real non negative Element of REAL

r /. s0 is V11() real ext-real Element of REAL

i . s0 is V11() real ext-real Element of REAL

r . s0 is V11() real ext-real Element of REAL

h is non empty set

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

REAL n is non empty functional FinSequence-membered V227() V228() V229() M12( REAL )

[:h,(REAL n):] is set

bool [:h,(REAL n):] is set

x0 is Relation-like h -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:h,(REAL n):]

dom x0 is Element of bool h

bool h is set

i is Relation-like h -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:h,(REAL n):]

dom i is Element of bool h

r is set

i /. r is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

x0 /. r is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

- (x0 /. r) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like M13( REAL , REAL n)

K38(1) is V11() real ext-real non positive set

K38(1) (#) (x0 /. r) is Relation-like Function-like set

i is Relation-like h -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:h,(REAL n):]

dom i is Element of bool h

r is Relation-like h -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:h,(REAL n):]

dom r is Element of bool h

s0 is Element of h

i /. s0 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

x0 /. s0 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

- (x0 /. s0) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like M13( REAL , REAL n)

K38(1) is V11() real ext-real non positive set

K38(1) (#) (x0 /. s0) is Relation-like Function-like set

r /. s0 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

i . s0 is Relation-like NAT -defined Function-like V33() V34() V35() finite FinSequence-like FinSubsequence-like set

r . s0 is Relation-like NAT -defined Function-like V33() V34() V35() finite FinSequence-like FinSubsequence-like set

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

REAL-NS n is non empty V106() V131() V132() V133() V134() V135() V136() V137() V141() V142() strict RealNormSpace-like V174() NORMSTR

the carrier of (REAL-NS n) is non empty set

REAL n is non empty functional FinSequence-membered V227() V228() V229() M12( REAL )

h is non empty set

[:h, the carrier of (REAL-NS n):] is set

bool [:h, the carrier of (REAL-NS n):] is set

[:h,(REAL n):] is set

bool [:h,(REAL n):] is set

x0 is Relation-like h -defined the carrier of (REAL-NS n) -valued Function-like Element of bool [:h, the carrier of (REAL-NS n):]

i is Relation-like h -defined the carrier of (REAL-NS n) -valued Function-like Element of bool [:h, the carrier of (REAL-NS n):]

x0 + i is Relation-like h -defined the carrier of (REAL-NS n) -valued Function-like Element of bool [:h, the carrier of (REAL-NS n):]

r is Relation-like h -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:h,(REAL n):]

s0 is Relation-like h -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:h,(REAL n):]

r + s0 is Relation-like h -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:h,(REAL n):]

K665(h,h,(REAL n),(REAL n),r,s0) is Relation-like h /\ h -defined K597((K592((REAL n)) /\ K592((REAL n)))) -valued Function-like V233() V234() V235() Element of bool [:(h /\ h),K597((K592((REAL n)) /\ K592((REAL n)))):]

h /\ h is set

K592((REAL n)) is set

K592((REAL n)) /\ K592((REAL n)) is set

K597((K592((REAL n)) /\ K592((REAL n)))) is functional V227() V228() V229() set

[:(h /\ h),K597((K592((REAL n)) /\ K592((REAL n)))):] is set

bool [:(h /\ h),K597((K592((REAL n)) /\ K592((REAL n)))):] is set

dom (x0 + i) is Element of bool h

bool h is set

dom x0 is Element of bool h

dom i is Element of bool h

(dom x0) /\ (dom i) is Element of bool h

dom (r + s0) is Element of bool h

rs0 is Element of h

dom r is Element of bool h

dom s0 is Element of bool h

x0 /. rs0 is Element of the carrier of (REAL-NS n)

r /. rs0 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

i /. rs0 is Element of the carrier of (REAL-NS n)

s0 /. rs0 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

r . rs0 is Relation-like NAT -defined Function-like V33() V34() V35() finite FinSequence-like FinSubsequence-like set

s0 . rs0 is Relation-like NAT -defined Function-like V33() V34() V35() finite FinSequence-like FinSubsequence-like set

(x0 /. rs0) + (i /. rs0) is Element of the carrier of (REAL-NS n)

(r . rs0) + (s0 . rs0) is Relation-like Function-like set

(x0 + i) /. rs0 is Element of the carrier of (REAL-NS n)

(x0 + i) . rs0 is set

(r + s0) . rs0 is Relation-like NAT -defined Function-like V33() V34() V35() finite FinSequence-like FinSubsequence-like set

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

REAL-NS n is non empty V106() V131() V132() V133() V134() V135() V136() V137() V141() V142() strict RealNormSpace-like V174() NORMSTR

the carrier of (REAL-NS n) is non empty set

REAL n is non empty functional FinSequence-membered V227() V228() V229() M12( REAL )

h is non empty set

[:h, the carrier of (REAL-NS n):] is set

bool [:h, the carrier of (REAL-NS n):] is set

[:h,(REAL n):] is set

bool [:h,(REAL n):] is set

x0 is Relation-like h -defined the carrier of (REAL-NS n) -valued Function-like Element of bool [:h, the carrier of (REAL-NS n):]

i is Relation-like h -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:h,(REAL n):]

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

r (#) x0 is Relation-like h -defined the carrier of (REAL-NS n) -valued Function-like Element of bool [:h, the carrier of (REAL-NS n):]

r (#) i is Relation-like h -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:h,(REAL n):]

i [#] r is Relation-like h -defined K597(K592((REAL n))) -valued Function-like V233() V234() V235() Element of bool [:h,K597(K592((REAL n))):]

K592((REAL n)) is set

K597(K592((REAL n))) is functional V227() V228() V229() set

[:h,K597(K592((REAL n))):] is set

bool [:h,K597(K592((REAL n))):] is set

dom (r (#) x0) is Element of bool h

bool h is set

dom x0 is Element of bool h

dom (r (#) i) is Element of bool h

s0 is Element of h

i . s0 is Relation-like NAT -defined Function-like V33() V34() V35() finite FinSequence-like FinSubsequence-like set

i /. s0 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

x0 /. s0 is Element of the carrier of (REAL-NS n)

r * (x0 /. s0) is Element of the carrier of (REAL-NS n)

r * (i /. s0) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like M13( REAL , REAL n)

(r (#) x0) /. s0 is Element of the carrier of (REAL-NS n)

(r (#) i) . s0 is Relation-like NAT -defined Function-like V33() V34() V35() finite FinSequence-like FinSubsequence-like set

r (#) (i . s0) is Relation-like Function-like set

(r (#) x0) . s0 is set

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

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

REAL n is non empty functional FinSequence-membered V227() V228() V229() M12( REAL )

h is non empty set

[:h,(REAL n):] is set

bool [:h,(REAL n):] is set

x0 is Relation-like h -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:h,(REAL n):]

(- 1) (#) x0 is Relation-like h -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:h,(REAL n):]

x0 [#] (- 1) is Relation-like h -defined K597(K592((REAL n))) -valued Function-like V233() V234() V235() Element of bool [:h,K597(K592((REAL n))):]

K592((REAL n)) is set

K597(K592((REAL n))) is functional V227() V228() V229() set

[:h,K597(K592((REAL n))):] is set

bool [:h,K597(K592((REAL n))):] is set

(n,h,x0) is Relation-like h -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:h,(REAL n):]

dom ((- 1) (#) x0) is Element of bool h

bool h is set

dom x0 is Element of bool h

dom (n,h,x0) is Element of bool h

i is Element of h

x0 . i is Relation-like NAT -defined Function-like V33() V34() V35() finite FinSequence-like FinSubsequence-like set

x0 /. i is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

(n,h,x0) /. i is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

- (x0 /. i) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like M13( REAL , REAL n)

K38(1) is V11() real ext-real non positive set

K38(1) (#) (x0 /. i) is Relation-like Function-like set

(x0 [#] (- 1)) . i is Relation-like Function-like V33() V34() V35() set

(- 1) (#) (x0 . i) is Relation-like Function-like set

((- 1) (#) x0) . i is Relation-like NAT -defined Function-like V33() V34() V35() finite FinSequence-like FinSubsequence-like set

(n,h,x0) . i is Relation-like NAT -defined Function-like V33() V34() V35() finite FinSequence-like FinSubsequence-like set

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

REAL-NS n is non empty V106() V131() V132() V133() V134() V135() V136() V137() V141() V142() strict RealNormSpace-like V174() NORMSTR

the carrier of (REAL-NS n) is non empty set

REAL n is non empty functional FinSequence-membered V227() V228() V229() M12( REAL )

h is non empty set

[:h, the carrier of (REAL-NS n):] is set

bool [:h, the carrier of (REAL-NS n):] is set

[:h,(REAL n):] is set

bool [:h,(REAL n):] is set

x0 is Relation-like h -defined the carrier of (REAL-NS n) -valued Function-like Element of bool [:h, the carrier of (REAL-NS n):]

- x0 is Relation-like h -defined the carrier of (REAL-NS n) -valued Function-like Element of bool [:h, the carrier of (REAL-NS n):]

i is Relation-like h -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:h,(REAL n):]

(n,h,i) is Relation-like h -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:h,(REAL n):]

dom (- x0) is Element of bool h

bool h is set

dom x0 is Element of bool h

dom (n,h,i) is Element of bool h

r is Element of h

x0 /. r is Element of the carrier of (REAL-NS n)

i /. r is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

- (x0 /. r) is Element of the carrier of (REAL-NS n)

- (i /. r) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like M13( REAL , REAL n)

K38(1) is V11() real ext-real non positive set

K38(1) (#) (i /. r) is Relation-like Function-like set

(- x0) /. r is Element of the carrier of (REAL-NS n)

(n,h,i) /. r is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

(- x0) . r is set

(n,h,i) . r is Relation-like NAT -defined Function-like V33() V34() V35() finite FinSequence-like FinSubsequence-like set

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

REAL-NS n is non empty V106() V131() V132() V133() V134() V135() V136() V137() V141() V142() strict RealNormSpace-like V174() NORMSTR

the carrier of (REAL-NS n) is non empty set

REAL n is non empty functional FinSequence-membered V227() V228() V229() M12( REAL )

h is non empty set

[:h, the carrier of (REAL-NS n):] is set

bool [:h, the carrier of (REAL-NS n):] is set

[:h,(REAL n):] is set

bool [:h,(REAL n):] is set

x0 is Relation-like h -defined the carrier of (REAL-NS n) -valued Function-like Element of bool [:h, the carrier of (REAL-NS n):]

||.x0.|| is Relation-like h -defined REAL -valued Function-like V33() V34() V35() Element of bool [:h,REAL:]

[:h,REAL:] is set

bool [:h,REAL:] is set

i is Relation-like h -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:h,(REAL n):]

(n,h,i) is Relation-like h -defined REAL -valued Function-like V33() V34() V35() Element of bool [:h,REAL:]

dom ||.x0.|| is Element of bool h

bool h is set

dom x0 is Element of bool h

dom (n,h,i) is Element of bool h

r is Element of h

x0 /. r is Element of the carrier of (REAL-NS n)

i /. r is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

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

|.(i /. r).| is V11() real ext-real non negative Element of REAL

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

(n,h,i) /. r is V11() real ext-real Element of REAL

(n,h,i) . r is V11() real ext-real Element of REAL

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

REAL-NS n is non empty V106() V131() V132() V133() V134() V135() V136() V137() V141() V142() strict RealNormSpace-like V174() NORMSTR

the carrier of (REAL-NS n) is non empty set

REAL n is non empty functional FinSequence-membered V227() V228() V229() M12( REAL )

h is non empty set

[:h, the carrier of (REAL-NS n):] is set

bool [:h, the carrier of (REAL-NS n):] is set

[:h,(REAL n):] is set

bool [:h,(REAL n):] is set

x0 is Relation-like h -defined the carrier of (REAL-NS n) -valued Function-like Element of bool [:h, the carrier of (REAL-NS n):]

i is Relation-like h -defined the carrier of (REAL-NS n) -valued Function-like Element of bool [:h, the carrier of (REAL-NS n):]

x0 - i is Relation-like h -defined the carrier of (REAL-NS n) -valued Function-like Element of bool [:h, the carrier of (REAL-NS n):]

r is Relation-like h -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:h,(REAL n):]

s0 is Relation-like h -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:h,(REAL n):]

r - s0 is Relation-like h -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:h,(REAL n):]

K671(h,h,(REAL n),(REAL n),r,s0) is Relation-like h /\ h -defined K597((K592((REAL n)) /\ K592((REAL n)))) -valued Function-like V233() V234() V235() Element of bool [:(h /\ h),K597((K592((REAL n)) /\ K592((REAL n)))):]

h /\ h is set

K592((REAL n)) is set

K592((REAL n)) /\ K592((REAL n)) is set

K597((K592((REAL n)) /\ K592((REAL n)))) is functional V227() V228() V229() set

[:(h /\ h),K597((K592((REAL n)) /\ K592((REAL n)))):] is set

bool [:(h /\ h),K597((K592((REAL n)) /\ K592((REAL n)))):] is set

dom (x0 - i) is Element of bool h

bool h is set

dom x0 is Element of bool h

dom i is Element of bool h

(dom x0) /\ (dom i) is Element of bool h

dom (r - s0) is Element of bool h

rs0 is Element of h

x0 /. rs0 is Element of the carrier of (REAL-NS n)

r /. rs0 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

i /. rs0 is Element of the carrier of (REAL-NS n)

s0 /. rs0 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

r . rs0 is Relation-like NAT -defined Function-like V33() V34() V35() finite FinSequence-like FinSubsequence-like set

s0 . rs0 is Relation-like NAT -defined Function-like V33() V34() V35() finite FinSequence-like FinSubsequence-like set

(x0 /. rs0) - (i /. rs0) is Element of the carrier of (REAL-NS n)

(r . rs0) - (s0 . rs0) is Relation-like Function-like set

- (s0 . rs0) is Relation-like Function-like V33() set

K38(1) is V11() real ext-real non positive set

K38(1) (#) (s0 . rs0) is Relation-like Function-like set

(r . rs0) + (- (s0 . rs0)) is Relation-like Function-like set

(x0 - i) /. rs0 is Element of the carrier of (REAL-NS n)

(x0 - i) . rs0 is set

(r - s0) . rs0 is Relation-like NAT -defined Function-like V33() V34() V35() finite FinSequence-like FinSubsequence-like set

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

REAL n is non empty functional FinSequence-membered V227() V228() V229() M12( REAL )

[:REAL,(REAL n):] is set

bool [:REAL,(REAL n):] is set

bool (REAL n) is set

h is V11() real ext-real set

x0 is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]

dom x0 is Element of bool REAL

x0 /. h is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

REAL-NS n is non empty V106() V131() V132() V133() V134() V135() V136() V137() V141() V142() strict RealNormSpace-like V174() NORMSTR

the carrier of (REAL-NS n) is non empty set

[:REAL, the carrier of (REAL-NS n):] is set

bool [:REAL, the carrier of (REAL-NS n):] is set

i is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of bool [:REAL, the carrier of (REAL-NS n):]

r is functional FinSequence-membered V227() V228() V229() Element of bool (REAL n)

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

{ b

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

{ b

i /. h is Element of the carrier of (REAL-NS n)

{ b

dom i is Element of bool REAL

rs0 is Neighbourhood of h

rs0 is V11() real ext-real set

x0 /. rs0 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

i /. rs0 is Element of the carrier of (REAL-NS n)

REAL-NS n is non empty V106() V131() V132() V133() V134() V135() V136() V137() V141() V142() strict RealNormSpace-like V174() NORMSTR

the carrier of (REAL-NS n) is non empty set

[:REAL, the carrier of (REAL-NS n):] is set

bool [:REAL, the carrier of (REAL-NS n):] is set

i is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of bool [:REAL, the carrier of (REAL-NS n):]

i /. h is Element of the carrier of (REAL-NS n)

r is Neighbourhood of i /. h

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

{ b

{ b

rs0 is set

s is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

s - (x0 /. h) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like M13( REAL , REAL n)

- (x0 /. h) is Relation-like Function-like V33() set

K38(1) is V11() real ext-real non positive set

K38(1) (#) (x0 /. h) is Relation-like Function-like set

s + (- (x0 /. h)) is Relation-like Function-like set

|.(s - (x0 /. h)).| is V11() real ext-real non negative Element of REAL

rs0 is Neighbourhood of h

i1 is V11() real ext-real set

dom i is Element of bool REAL

s is Neighbourhood of h

x0 /. i1 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

i /. i1 is Element of the carrier of (REAL-NS n)

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

REAL n is non empty functional FinSequence-membered V227() V228() V229() M12( REAL )

[:REAL,(REAL n):] is set

bool [:REAL,(REAL n):] is set

bool (REAL n) is set

h is V11() real ext-real set

x0 is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]

dom x0 is Element of bool REAL

x0 /. h is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

REAL-NS n is non empty V106() V131() V132() V133() V134() V135() V136() V137() V141() V142() strict RealNormSpace-like V174() NORMSTR

the carrier of (REAL-NS n) is non empty set

[:REAL, the carrier of (REAL-NS n):] is set

bool [:REAL, the carrier of (REAL-NS n):] is set

i is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of bool [:REAL, the carrier of (REAL-NS n):]

r is functional FinSequence-membered V227() V228() V229() Element of bool (REAL n)

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

{ b

i /. h is Element of the carrier of (REAL-NS n)

{ b

rs0 is Neighbourhood of h

i .: rs0 is Element of bool the carrier of (REAL-NS n)

bool the carrier of (REAL-NS n) is set

x0 .: rs0 is functional FinSequence-membered V227() V228() V229() Element of bool (REAL n)

i /. h is Element of the carrier of (REAL-NS n)

r is Neighbourhood of i /. h

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

{ b

{ b

rs0 is set

s is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

s - (x0 /. h) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like M13( REAL , REAL n)

- (x0 /. h) is Relation-like Function-like V33() set

K38(1) is V11() real ext-real non positive set

K38(1) (#) (x0 /. h) is Relation-like Function-like set

s + (- (x0 /. h)) is Relation-like Function-like set

|.(s - (x0 /. h)).| is V11() real ext-real non negative Element of REAL

rs0 is Neighbourhood of h

x0 .: rs0 is functional FinSequence-membered V227() V228() V229() Element of bool (REAL n)

s is Neighbourhood of h

i .: s is Element of bool the carrier of (REAL-NS n)

bool the carrier of (REAL-NS n) is set

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

REAL n is non empty functional FinSequence-membered V227() V228() V229() M12( REAL )

[:REAL,(REAL n):] is set

bool [:REAL,(REAL n):] is set

h is V11() real ext-real set

{h} is non empty trivial set

x0 is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]

dom x0 is Element of bool REAL

i is Neighbourhood of h

(dom x0) /\ i is Element of bool REAL

REAL-NS n is non empty V106() V131() V132() V133() V134() V135() V136() V137() V141() V142() strict RealNormSpace-like V174() NORMSTR

the carrier of (REAL-NS n) is non empty set

[:REAL, the carrier of (REAL-NS n):] is set

bool [:REAL, the carrier of (REAL-NS n):] is set

r is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of bool [:REAL, the carrier of (REAL-NS n):]

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

REAL n is non empty functional FinSequence-membered V227() V228() V229() M12( REAL )

[:REAL,(REAL n):] is set

bool [:REAL,(REAL n):] is set

h is V11() real ext-real set

x0 is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]

dom x0 is Element of bool REAL

i is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]

dom i is Element of bool REAL

(dom x0) /\ (dom i) is Element of bool REAL

x0 + i is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]

K665(REAL,REAL,(REAL n),(REAL n),x0,i) is Relation-like REAL /\ REAL -defined K597((K592((REAL n)) /\ K592((REAL n)))) -valued Function-like V233() V234() V235() Element of bool [:(REAL /\ REAL),K597((K592((REAL n)) /\ K592((REAL n)))):]

REAL /\ REAL is set

K592((REAL n)) is set

K592((REAL n)) /\ K592((REAL n)) is set

K597((K592((REAL n)) /\ K592((REAL n)))) is functional V227() V228() V229() set

[:(REAL /\ REAL),K597((K592((REAL n)) /\ K592((REAL n)))):] is set

bool [:(REAL /\ REAL),K597((K592((REAL n)) /\ K592((REAL n)))):] is set

REAL-NS n is non empty V106() V131() V132() V133() V134() V135() V136() V137() V141() V142() strict RealNormSpace-like V174() NORMSTR

the carrier of (REAL-NS n) is non empty set

[:REAL, the carrier of (REAL-NS n):] is set

bool [:REAL, the carrier of (REAL-NS n):] is set

r is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of bool [:REAL, the carrier of (REAL-NS n):]

s0 is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of bool [:REAL, the carrier of (REAL-NS n):]

r + s0 is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of bool [:REAL, the carrier of (REAL-NS n):]

r - s0 is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of bool [:REAL, the carrier of (REAL-NS n):]

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

REAL n is non empty functional FinSequence-membered V227() V228() V229() M12( REAL )

[:REAL,(REAL n):] is set

bool [:REAL,(REAL n):] is set

h is V11() real ext-real set

x0 is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]

dom x0 is Element of bool REAL

i is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]

dom i is Element of bool REAL

(dom x0) /\ (dom i) is Element of bool REAL

x0 - i is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]

K671(REAL,REAL,(REAL n),(REAL n),x0,i) is Relation-like REAL /\ REAL -defined K597((K592((REAL n)) /\ K592((REAL n)))) -valued Function-like V233() V234() V235() Element of bool [:(REAL /\ REAL),K597((K592((REAL n)) /\ K592((REAL n)))):]

REAL /\ REAL is set

K592((REAL n)) is set

K592((REAL n)) /\ K592((REAL n)) is set

K597((K592((REAL n)) /\ K592((REAL n)))) is functional V227() V228() V229() set

[:(REAL /\ REAL),K597((K592((REAL n)) /\ K592((REAL n)))):] is set

bool [:(REAL /\ REAL),K597((K592((REAL n)) /\ K592((REAL n)))):] is set

REAL-NS n is non empty V106() V131() V132() V133() V134() V135() V136() V137() V141() V142() strict RealNormSpace-like V174() NORMSTR

the carrier of (REAL-NS n) is non empty set

[:REAL, the carrier of (REAL-NS n):] is set

bool [:REAL, the carrier of (REAL-NS n):] is set

r is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of bool [:REAL, the carrier of (REAL-NS n):]

s0 is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of bool [:REAL, the carrier of (REAL-NS n):]

r + s0 is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of bool [:REAL, the carrier of (REAL-NS n):]

r - s0 is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of bool [:REAL, the carrier of (REAL-NS n):]

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

REAL n is non empty functional FinSequence-membered V227() V228() V229() M12( REAL )

[:REAL,(REAL n):] is set

bool [:REAL,(REAL n):] is set

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

x0 is V11() real ext-real set

i is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]

h (#) i is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]

i [#] h is Relation-like REAL -defined K597(K592((REAL n))) -valued Function-like V233() V234() V235() Element of bool [:REAL,K597(K592((REAL n))):]

K592((REAL n)) is set

K597(K592((REAL n))) is functional V227() V228() V229() set

[:REAL,K597(K592((REAL n))):] is set

bool [:REAL,K597(K592((REAL n))):] is set

REAL-NS n is non empty V106() V131() V132() V133() V134() V135() V136() V137() V141() V142() strict RealNormSpace-like V174() NORMSTR

the carrier of (REAL-NS n) is non empty set

[:REAL, the carrier of (REAL-NS n):] is set

bool [:REAL, the carrier of (REAL-NS n):] is set

r is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of bool [:REAL, the carrier of (REAL-NS n):]

h (#) r is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of bool [:REAL, the carrier of (REAL-NS n):]

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

REAL n is non empty functional FinSequence-membered V227() V228() V229() M12( REAL )

[:REAL,(REAL n):] is set

bool [:REAL,(REAL n):] is set

h is V11() real ext-real set

x0 is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]

dom x0 is Element of bool REAL

(n,REAL,x0) is Relation-like REAL -defined REAL -valued Function-like V33() V34() V35() Element of bool [:REAL,REAL:]

REAL-NS n is non empty V106() V131() V132() V133() V134() V135() V136() V137() V141() V142() strict RealNormSpace-like V174() NORMSTR

the carrier of (REAL-NS n) is non empty set

[:REAL, the carrier of (REAL-NS n):] is set

bool [:REAL, the carrier of (REAL-NS n):] is set

i is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of bool [:REAL, the carrier of (REAL-NS n):]

||.i.|| is Relation-like REAL -defined REAL -valued Function-like V33() V34() V35() Element of bool [:REAL,REAL:]

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

REAL n is non empty functional FinSequence-membered V227() V228() V229() M12( REAL )

[:REAL,(REAL n):] is set

bool [:REAL,(REAL n):] is set

h is V11() real ext-real set

x0 is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]

dom x0 is Element of bool REAL

(n,REAL,x0) is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]

REAL-NS n is non empty V106() V131() V132() V133() V134() V135() V136() V137() V141() V142() strict RealNormSpace-like V174() NORMSTR

the carrier of (REAL-NS n) is non empty set

[:REAL, the carrier of (REAL-NS n):] is set

bool [:REAL, the carrier of (REAL-NS n):] is set

i is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of bool [:REAL, the carrier of (REAL-NS n):]

- i is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of bool [:REAL, the carrier of (REAL-NS n):]

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

REAL-NS n is non empty V106() V131() V132() V133() V134() V135() V136() V137() V141() V142() strict RealNormSpace-like V174() NORMSTR

the carrier of (REAL-NS n) is non empty set

REAL n is non empty functional FinSequence-membered V227() V228() V229() M12( REAL )

[:REAL,(REAL n):] is set

bool [:REAL,(REAL n):] is set

h is V11() real ext-real set

x0 is non empty V106() V131() V132() V133() V134() V135() V136() V137() V141() V142() RealNormSpace-like NORMSTR

the carrier of x0 is non empty set

[: the carrier of (REAL-NS n), the carrier of x0:] is set

bool [: the carrier of (REAL-NS n), the carrier of x0:] is set

i is Element of the carrier of (REAL-NS n)

r is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]

r /. h is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

s0 is Relation-like the carrier of (REAL-NS n) -defined the carrier of x0 -valued Function-like Element of bool [: the carrier of (REAL-NS n), the carrier of x0:]

s0 * r is Relation-like REAL -defined the carrier of x0 -valued Function-like Element of bool [:REAL, the carrier of x0:]

[:REAL, the carrier of x0:] is set

bool [:REAL, the carrier of x0:] is set

dom (s0 * r) is Element of bool REAL

[:REAL, the carrier of (REAL-NS n):] is set

bool [:REAL, the carrier of (REAL-NS n):] is set

rs0 is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of bool [:REAL, the carrier of (REAL-NS n):]

rs0 /. h is Element of the carrier of (REAL-NS n)

n is V11() real ext-real set

h is non empty V106() V131() V132() V133() V134() V135() V136() V137() V141() V142() RealNormSpace-like NORMSTR

the carrier of h is non empty set

[:REAL, the carrier of h:] is set

bool [:REAL, the carrier of h:] is set

[: the carrier of h,REAL:] is set

bool [: the carrier of h,REAL:] is set

x0 is Relation-like REAL -defined the carrier of h -valued Function-like Element of bool [:REAL, the carrier of h:]

x0 /. n is Element of the carrier of h

i is Relation-like the carrier of h -defined REAL -valued Function-like V33() V34() V35() Element of bool [: the carrier of h,REAL:]

i * x0 is Relation-like REAL -defined REAL -valued Function-like V33() V34() V35() Element of bool [:REAL,REAL:]

dom (i * x0) is Element of bool REAL

r is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total V33() V34() V35() Element of bool [:NAT,REAL:]

rng r is complex-membered ext-real-membered real-membered Element of bool REAL

lim r is V11() real ext-real Element of REAL

(i * x0) /* r is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total V33() V34() V35() Element of bool [:NAT,REAL:]

(i * x0) . n is V11() real ext-real Element of REAL

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

dom x0 is Element of bool REAL

x0 /* r is non empty Relation-like NAT -defined the carrier of h -valued Function-like total quasi_total Element of bool [:NAT, the carrier of h:]

[:NAT, the carrier of h:] is set

bool [:NAT, the carrier of h:] is set

rng (x0 /* r) is Element of bool the carrier of h

bool the carrier of h is set

dom i is Element of bool the carrier of h

s0 is set

rs0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

(x0 /* r) . rs0 is Element of the carrier of h

r . rs0 is V11() real ext-real Element of REAL

x0 . (r . rs0) is set

s0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

r . s0 is V11() real ext-real Element of REAL

((i * x0) /* r) . s0 is V11() real ext-real Element of REAL

(i * x0) . (r . s0) is V11() real ext-real Element of REAL

x0 . (r . s0) is set

i . (x0 . (r . s0)) is V11() real ext-real Element of REAL

(x0 /* r) . s0 is Element of the carrier of h

i . ((x0 /* r) . s0) is V11() real ext-real Element of REAL

i /* (x0 /* r) is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total V33() V34() V35() Element of bool [:NAT,REAL:]

(i /* (x0 /* r)) . s0 is V11() real ext-real Element of REAL

lim (x0 /* r) is Element of the carrier of h

(i * x0) /. n is V11() real ext-real Element of REAL

i /. (x0 /. n) is V11() real ext-real Element of REAL

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

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

REAL n is non empty functional FinSequence-membered V227() V228() V229() M12( REAL )

[:(REAL n),REAL:] is set

bool [:(REAL n),REAL:] is set

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

REAL n is non empty functional FinSequence-membered V227() V228() V229() M12( REAL )

[:(REAL n),REAL:] is set

bool [:(REAL n),REAL:] is set

REAL-NS n is non empty V106() V131() V132() V133() V134() V135() V136() V137() V141() V142() strict RealNormSpace-like V174() NORMSTR

the carrier of (REAL-NS n) is non empty set

[: the carrier of (REAL-NS n),REAL:] is set

bool [: the carrier of (REAL-NS n),REAL:] is set

h is Relation-like REAL n -defined REAL -valued Function-like V33() V34() V35() Element of bool [:(REAL n),REAL:]

x0 is Relation-like the carrier of (REAL-NS n) -defined REAL -valued Function-like V33() V34() V35() Element of bool [: the carrier of (REAL-NS n),REAL:]

i is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

r is Element of the carrier of (REAL-NS n)

s0 is Element of the carrier of (REAL-NS n)

rs0 is Relation-like the carrier of (REAL-NS n) -defined REAL -valued Function-like V33() V34() V35() Element of bool [: the carrier of (REAL-NS n),REAL:]

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

REAL n is non empty functional FinSequence-membered V227() V228() V229() M12( REAL )

[:REAL,(REAL n):] is set

bool [:REAL,(REAL n):] is set

[:(REAL n),REAL:] is set

bool [:(REAL n),REAL:] is set

h is V11() real ext-real set

x0 is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]

x0 /. h is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

i is Relation-like REAL n -defined REAL -valued Function-like V33() V34() V35() Element of bool [:(REAL n),REAL:]

i * x0 is Relation-like REAL -defined REAL -valued Function-like V33() V34() V35() Element of bool [:REAL,REAL:]

dom (i * x0) is Element of bool REAL

REAL-NS n is non empty V106() V131() V132() V133() V134() V135() V136() V137() V141() V142() strict RealNormSpace-like V174() NORMSTR

the carrier of (REAL-NS n) is non empty set

[:REAL, the carrier of (REAL-NS n):] is set

bool [:REAL, the carrier of (REAL-NS n):] is set

[: the carrier of (REAL-NS n),REAL:] is set

bool [: the carrier of (REAL-NS n),REAL:] is set

r is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of bool [:REAL, the carrier of (REAL-NS n):]

r /. h is Element of the carrier of (REAL-NS n)

s0 is Relation-like the carrier of (REAL-NS n) -defined REAL -valued Function-like V33() V34() V35() Element of bool [: the carrier of (REAL-NS n),REAL:]

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

REAL n is non empty functional FinSequence-membered V227() V228() V229() M12( REAL )

[:REAL,(REAL n):] is set

bool [:REAL,(REAL n):] is set

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

REAL-NS n is non empty V106() V131() V132() V133() V134() V135() V136() V137() V141() V142() strict RealNormSpace-like V174() NORMSTR

the carrier of (REAL-NS n) is non empty set

[:REAL, the carrier of (REAL-NS n):] is set

bool [:REAL, the carrier of (REAL-NS n):] is set

REAL n is non empty functional FinSequence-membered V227() V228() V229() M12( REAL )

[:REAL,(REAL n):] is set

bool [:REAL,(REAL n):] is set

h is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of bool [:REAL, the carrier of (REAL-NS n):]

x0 is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]

i is V11() real ext-real set

dom x0 is Element of bool REAL

i is V11() real ext-real set

dom h is Element of bool REAL

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

REAL n is non empty functional FinSequence-membered V227() V228() V229() M12( REAL )

[:REAL,(REAL n):] is set

bool [:REAL,(REAL n):] is set

h is set

x0 is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]

dom x0 is Element of bool REAL

x0 | h is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]

i is V11() real ext-real set

x0 /. i is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

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

dom (x0 | h) is Element of bool REAL

(x0 | h) /. i is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

s0 is V11() real ext-real set

rs0 is V11() real ext-real set

rs0 - i is V11() real ext-real Element of REAL

abs (rs0 - i) is V11() real ext-real Element of REAL

x0 /. rs0 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

(x0 /. rs0) - (x0 /. i) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like M13( REAL , REAL n)

- (x0 /. i) is Relation-like Function-like V33() set

K38(1) is V11() real ext-real non positive set

K38(1) (#) (x0 /. i) is Relation-like Function-like set

(x0 /. rs0) + (- (x0 /. i)) is Relation-like Function-like set

|.((x0 /. rs0) - (x0 /. i)).| is V11() real ext-real non negative Element of REAL

(dom x0) /\ h is Element of bool REAL

(x0 | h) /. rs0 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

((x0 | h) /. rs0) - (x0 /. i) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like M13( REAL , REAL n)

((x0 | h) /. rs0) + (- (x0 /. i)) is Relation-like Function-like set

|.(((x0 | h) /. rs0) - (x0 /. i)).| is V11() real ext-real non negative Element of REAL

((x0 | h) /. rs0) - ((x0 | h) /. i) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like M13( REAL , REAL n)

- ((x0 | h) /. i) is Relation-like Function-like V33() set

K38(1) (#) ((x0 | h) /. i) is Relation-like Function-like set

((x0 | h) /. rs0) + (- ((x0 | h) /. i)) is Relation-like Function-like set

|.(((x0 | h) /. rs0) - ((x0 | h) /. i)).| is V11() real ext-real non negative Element of REAL

dom (x0 | h) is Element of bool REAL

(dom x0) /\ h is Element of bool REAL

i is V11() real ext-real set

(x0 | h) /. i is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

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

x0 /. i is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

s0 is V11() real ext-real set

rs0 is V11() real ext-real set

rs0 - i is V11() real ext-real Element of REAL

abs (rs0 - i) is V11() real ext-real Element of REAL

(x0 | h) /. rs0 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

((x0 | h) /. rs0) - ((x0 | h) /. i) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like M13( REAL , REAL n)

- ((x0 | h) /. i) is Relation-like Function-like V33() set

K38(1) is V11() real ext-real non positive set

K38(1) (#) ((x0 | h) /. i) is Relation-like Function-like set

((x0 | h) /. rs0) + (- ((x0 | h) /. i)) is Relation-like Function-like set

|.(((x0 | h) /. rs0) - ((x0 | h) /. i)).| is V11() real ext-real non negative Element of REAL

((x0 | h) /. rs0) - (x0 /. i) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like M13( REAL , REAL n)

- (x0 /. i) is Relation-like Function-like V33() set

K38(1) (#) (x0 /. i) is Relation-like Function-like set

((x0 | h) /. rs0) + (- (x0 /. i)) is Relation-like Function-like set

|.(((x0 | h) /. rs0) - (x0 /. i)).| is V11() real ext-real non negative Element of REAL

x0 /. rs0 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

(x0 /. rs0) - (x0 /. i) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like M13( REAL , REAL n)

(x0 /. rs0) + (- (x0 /. i)) is Relation-like Function-like set

|.((x0 /. rs0) - (x0 /. i)).| is V11() real ext-real non negative Element of REAL

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

REAL n is non empty functional FinSequence-membered V227() V228() V229() M12( REAL )

[:REAL,(REAL n):] is set

bool [:REAL,(REAL n):] is set

h is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]

i is V11() real ext-real set

dom h is Element of bool REAL

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

x0 is V11() real ext-real set

s0 is V11() real ext-real set

rs0 is V11() real ext-real set

rs0 - i is V11() real ext-real Element of REAL

abs (rs0 - i) is V11() real ext-real Element of REAL

h /. rs0 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

h . rs0 is Relation-like NAT -defined Function-like V33() V34() V35() finite FinSequence-like FinSubsequence-like set

h . i is Relation-like NAT -defined Function-like V33() V34() V35() finite FinSequence-like FinSubsequence-like set

h /. i is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n

(h /. rs0) - (h /. i) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like M13( REAL , REAL n)

- (h /. i) is Relation-like Function-like V33() set

K38(1) is V11() real ext-real non positive set

K38(1) (#) (h /. i) is Relation-like Function-like set

(h /. rs0) + (- (h /. i)) is Relation-like Function-like set

|.((h /. rs0) - (h /. i)).| is V11() real ext-real non negative Element of REAL

h | (dom h) is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

REAL n is non empty functional FinSequence-membered V227() V228() V229() M12( REAL )

[:REAL,(REAL n):] is set

bool [:REAL,(REAL n):] is set

the Relation-like REAL -defined REAL n -valued Function-like constant V233() V234() V235() (n) Element of bool [:REAL,(REAL n):] is Relation-like REAL -defined REAL n -valued Function-like constant V233() V234() V235() (n) Element of bool [:REAL,(REAL n):]

h is Relation-like REAL -defined REAL n -valued Function-like constant V233() V234() V235() (n) Element of bool [:REAL,(REAL n):]

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

REAL n is non empty functional FinSequence-membered V227() V228() V229() M12( REAL )

[:REAL,(REAL n):] is set

bool [:REAL,(REAL n):] is set

h is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() (n) Element of bool [:REAL,(REAL n):]

x0 is set

h | x0 is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]

dom (h | x0) is Element of bool REAL

i is V11() real ext-real set

dom h is Element of bool REAL

i is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT