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
{ b1 where b1 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n : not h <= |.(b1 - x0).| } is set
i is Element of the carrier of (REAL-NS n)
{ b1 where b1 is Element of the carrier of (REAL-NS n) : not h <= ||.(b1 - i).|| } is set
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
{ b1 where b1 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n : not s0 <= |.(b1 - (x0 /. h)).| } is set
s0 is V11() real ext-real Element of REAL
{ b1 where b1 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n : not s0 <= |.(b1 - (x0 /. h)).| } is set
i /. h is Element of the carrier of (REAL-NS n)
{ b1 where b1 is Element of the carrier of (REAL-NS n) : not s0 <= ||.(b1 - (i /. h)).|| } is set
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
{ b1 where b1 is Element of the carrier of (REAL-NS n) : not s0 <= ||.(b1 - (i /. h)).|| } is set
{ b1 where b1 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n : not s0 <= |.(b1 - (x0 /. h)).| } is set
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
{ b1 where b1 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n : not s0 <= |.(b1 - (x0 /. h)).| } is set
i /. h is Element of the carrier of (REAL-NS n)
{ b1 where b1 is Element of the carrier of (REAL-NS n) : not s0 <= ||.(b1 - (i /. h)).|| } is set
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
{ b1 where b1 is Element of the carrier of (REAL-NS n) : not s0 <= ||.(b1 - (i /. h)).|| } is set
{ b1 where b1 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n : not s0 <= |.(b1 - (x0 /. h)).| } is set
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
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 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):]
i | x0 is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]
(i | h) | x0 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
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
h is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]
x0 is trivial set
h | 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 | x0 is Relation-like REAL -defined the carrier of (REAL-NS n) -valued the carrier of (REAL-NS n) -valued Function-like continuous Element of bool [:REAL, 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):]
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 Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() (n) Element of bool [:REAL,(REAL n):]
h + x0 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),h,x0) 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
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):]
i + 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 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
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 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
i | h is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]
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)))):]
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
(x0 + i) | h is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]
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)))):]
(x0 - 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):]
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):]
s0 | 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):]
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) | 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):]
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) | 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 set
x0 is set
h /\ x0 is set
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
i | h is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]
r is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]
dom r is Element of bool REAL
r | x0 is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]
i + r 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),i,r) 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)))):]
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
(i + r) | (h /\ x0) is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]
i - r 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),i,r) 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)))):]
(i - r) | (h /\ 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
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):]
s0 | 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):]
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 | x0 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 + 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):]
(s0 + rs0) | (h /\ x0) 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 - 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):]
(s0 - rs0) | (h /\ x0) 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
x0 is V11() real ext-real Element of REAL
h is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() (n) Element of bool [:REAL,(REAL n):]
x0 (#) h is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]
h [#] x0 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
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):]
x0 (#) 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 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
h is set
x0 is V11() real ext-real Element of 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
i | h is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]
x0 (#) i is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]
i [#] x0 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
(x0 (#) 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):]
x0 (#) 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):]
(x0 (#) 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 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):]
(n,REAL,x0) is Relation-like REAL -defined REAL -valued Function-like V33() V34() V35() Element of bool [:REAL,REAL:]
(n,REAL,x0) | h is Relation-like REAL -defined REAL -valued Function-like V33() V34() V35() Element of bool [:REAL,REAL:]
(n,REAL,x0) is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]
(n,REAL,x0) | 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
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 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:]
||.i.|| | h is Relation-like REAL -defined REAL -valued Function-like V33() V34() V35() Element of bool [:REAL,REAL:]
- 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 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 Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]
h | REAL is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]
x0 is V11() real ext-real 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
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 set
i /. r is Element of the carrier of (REAL-NS n)
h /. r 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
i /. s0 is Element of the carrier of (REAL-NS n)
h /. s0 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n
r + s0 is V11() real ext-real Element of REAL
i /. (r + s0) is Element of the carrier of (REAL-NS n)
h /. (r + s0) is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n
(h /. r) + (h /. s0) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like M13( REAL , REAL n)
(i /. r) + (i /. s0) is Element of the carrier of (REAL-NS n)
i | REAL 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
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
bool the carrier of (REAL-NS n) is set
h is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]
dom h is Element of bool REAL
h | (dom h) is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]
rng h is functional FinSequence-membered V227() V228() V229() Element of bool (REAL n)
bool (REAL n) is set
x0 is Element of bool the carrier of (REAL-NS n)
[: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):]
dom i is Element of bool REAL
i | (dom 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 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
bool the carrier of (REAL-NS n) is set
h is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]
dom h is Element of bool REAL
x0 is Element of bool REAL
h .: x0 is functional FinSequence-membered V227() V228() V229() Element of bool (REAL n)
bool (REAL n) is set
h | x0 is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]
i is Element of bool the carrier of (REAL-NS n)
[: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 | x0 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
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):]
dom h 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
x0 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 x0 is Element of bool REAL
i is V11() real ext-real set
r is V11() real ext-real set
s0 is V11() real ext-real set
h /. s0 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n
rs0 is V11() real ext-real set
h /. rs0 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n
(h /. s0) - (h /. rs0) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like M13( REAL , REAL n)
- (h /. rs0) is Relation-like Function-like V33() set
K38(1) is V11() real ext-real non positive set
K38(1) (#) (h /. rs0) is Relation-like Function-like set
(h /. s0) + (- (h /. rs0)) is Relation-like Function-like set
|.((h /. s0) - (h /. rs0)).| is V11() real ext-real non negative Element of REAL
s0 - rs0 is V11() real ext-real Element of REAL
abs (s0 - rs0) is V11() real ext-real Element of REAL
r * (abs (s0 - rs0)) is V11() real ext-real Element of REAL
x0 /. s0 is Element of the carrier of (REAL-NS n)
x0 /. rs0 is Element of the carrier of (REAL-NS n)
(x0 /. s0) - (x0 /. rs0) is Element of the carrier of (REAL-NS n)
||.((x0 /. s0) - (x0 /. rs0)).|| is V11() real ext-real Element of REAL
x0 is V11() real ext-real set
r 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
s0 is V11() real ext-real set
h /. r is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n
h /. s0 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n
(h /. r) - (h /. s0) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like M13( REAL , REAL n)
- (h /. s0) is Relation-like Function-like V33() set
K38(1) is V11() real ext-real non positive set
K38(1) (#) (h /. s0) is Relation-like Function-like set
(h /. r) + (- (h /. s0)) is Relation-like Function-like set
|.((h /. r) - (h /. s0)).| is V11() real ext-real non negative Element of REAL
r - s0 is V11() real ext-real Element of REAL
abs (r - s0) is V11() real ext-real Element of REAL
x0 * (abs (r - s0)) is V11() real ext-real Element of REAL
i /. r is Element of the carrier of (REAL-NS n)
i /. s0 is Element of the carrier of (REAL-NS n)
(i /. r) - (i /. s0) is Element of the carrier of (REAL-NS n)
||.((i /. r) - (i /. s0)).|| 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,(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 Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]
x0 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 h is Element of bool REAL
i is V11() real ext-real set
r is V11() real ext-real set
dom x0 is Element of bool REAL
s0 is V11() real ext-real set
h /. r is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n
h /. s0 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n
(h /. r) - (h /. s0) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like M13( REAL , REAL n)
- (h /. s0) is Relation-like Function-like V33() set
K38(1) is V11() real ext-real non positive set
K38(1) (#) (h /. s0) is Relation-like Function-like set
(h /. r) + (- (h /. s0)) is Relation-like Function-like set
|.((h /. r) - (h /. s0)).| is V11() real ext-real non negative Element of REAL
r - s0 is V11() real ext-real Element of REAL
abs (r - s0) is V11() real ext-real Element of REAL
i * (abs (r - s0)) is V11() real ext-real Element of REAL
x0 /. r is Element of the carrier of (REAL-NS n)
x0 /. s0 is Element of the carrier of (REAL-NS n)
(x0 /. r) - (x0 /. s0) is Element of the carrier of (REAL-NS n)
||.((x0 /. r) - (x0 /. s0)).|| is V11() real ext-real Element of REAL
i is V11() real ext-real set
r is V11() real ext-real set
s0 is V11() real ext-real set
x0 /. r is Element of the carrier of (REAL-NS n)
x0 /. s0 is Element of the carrier of (REAL-NS n)
(x0 /. r) - (x0 /. s0) is Element of the carrier of (REAL-NS n)
||.((x0 /. r) - (x0 /. s0)).|| is V11() real ext-real Element of REAL
r - s0 is V11() real ext-real Element of REAL
abs (r - s0) is V11() real ext-real Element of REAL
i * (abs (r - s0)) is V11() real ext-real Element of REAL
h /. r is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n
h /. s0 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n
(h /. r) - (h /. s0) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like M13( REAL , REAL n)
- (h /. s0) is Relation-like Function-like V33() set
K38(1) (#) (h /. s0) is Relation-like Function-like set
(h /. r) + (- (h /. s0)) is Relation-like Function-like set
|.((h /. r) - (h /. s0)).| 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 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 REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]
dom (x0 | h) is Element of bool REAL
i is V11() real ext-real set
r is V11() real ext-real set
s0 is V11() real ext-real set
x0 /. s0 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n
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
(x0 /. s0) - (x0 /. rs0) 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) is Relation-like Function-like V33() set
K38(1) is V11() real ext-real non positive set
K38(1) (#) (x0 /. rs0) is Relation-like Function-like set
(x0 /. s0) + (- (x0 /. rs0)) is Relation-like Function-like set
|.((x0 /. s0) - (x0 /. rs0)).| is V11() real ext-real non negative Element of REAL
s0 - rs0 is V11() real ext-real Element of REAL
abs (s0 - rs0) is V11() real ext-real Element of REAL
r * (abs (s0 - rs0)) is V11() real ext-real Element of REAL
(x0 | h) /. s0 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n
(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) /. s0) - ((x0 | h) /. rs0) 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) is Relation-like Function-like V33() set
K38(1) (#) ((x0 | h) /. rs0) is Relation-like Function-like set
((x0 | h) /. s0) + (- ((x0 | h) /. rs0)) is Relation-like Function-like set
|.(((x0 | h) /. s0) - ((x0 | h) /. rs0)).| is V11() real ext-real non negative Element of REAL
(x0 /. s0) - ((x0 | h) /. rs0) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like M13( REAL , REAL n)
(x0 /. s0) + (- ((x0 | h) /. rs0)) is Relation-like Function-like set
|.((x0 /. s0) - ((x0 | h) /. rs0)).| is V11() real ext-real non negative Element of REAL
i is V11() real ext-real set
r is V11() real ext-real set
s0 is V11() real ext-real set
x0 /. r 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 /. r) - (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)
- (x0 /. s0) is Relation-like Function-like V33() set
K38(1) is V11() real ext-real non positive set
K38(1) (#) (x0 /. s0) is Relation-like Function-like set
(x0 /. r) + (- (x0 /. s0)) is Relation-like Function-like set
|.((x0 /. r) - (x0 /. s0)).| is V11() real ext-real non negative Element of REAL
r - s0 is V11() real ext-real Element of REAL
abs (r - s0) is V11() real ext-real Element of REAL
i * (abs (r - s0)) is V11() real ext-real Element of REAL
(x0 | h) /. r is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n
((x0 | h) /. r) - (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)
((x0 | h) /. r) + (- (x0 /. s0)) is Relation-like Function-like set
|.(((x0 | h) /. r) - (x0 /. s0)).| is V11() real ext-real non negative Element of REAL
(x0 | h) /. s0 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n
((x0 | h) /. r) - ((x0 | h) /. s0) 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) /. s0) is Relation-like Function-like V33() set
K38(1) (#) ((x0 | h) /. s0) is Relation-like Function-like set
((x0 | h) /. r) + (- ((x0 | h) /. s0)) is Relation-like Function-like set
|.(((x0 | h) /. r) - ((x0 | h) /. s0)).| 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):]
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
x0 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
the empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Relation-like REAL -defined REAL n -valued Function-like one-to-one constant functional V33() V34() V35() V36() V37() V38() V39() V40() finite FinSequence-like FinSubsequence-like FinSequence-membered V227() V228() V229() V230() V231() V232() V233() V234() V235() V236() V237() V238() (n) (n) Element of bool [:REAL,(REAL n):] is empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Relation-like REAL -defined REAL n -valued Function-like one-to-one constant functional V33() V34() V35() V36() V37() V38() V39() V40() finite FinSequence-like FinSubsequence-like FinSequence-membered V227() V228() V229() V230() V231() V232() V233() V234() V235() V236() V237() V238() (n) (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):]
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 | x0 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 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
h is set
x0 is 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):]
i | x0 is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]
(i | h) | x0 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
h is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() (n) Element of bool [:REAL,(REAL n):]
x0 is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() (n) Element of bool [:REAL,(REAL n):]
h + x0 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),h,x0) 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)))):]
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
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):]
i + 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 REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]
h - x0 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),h,x0) 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-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 Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of bool [:REAL, the carrier of (REAL-NS n):]
i - 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 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
h is set
x0 is set
h /\ x0 is 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):]
r is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]
r | x0 is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]
i + r 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),i,r) 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)))):]
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
(i + r) | (h /\ 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
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):]
s0 | 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):]
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 | x0 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 + 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):]
(s0 + rs0) | (h /\ x0) 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 set
h /\ x0 is 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):]
r is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]
r | x0 is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]
i - r 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),i,r) 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)))):]
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
(i - r) | (h /\ 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
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):]
s0 | 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):]
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 | x0 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 - 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):]
(s0 - rs0) | (h /\ x0) 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
x0 is V11() real ext-real Element of REAL
h is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() (n) Element of bool [:REAL,(REAL n):]
x0 (#) h is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]
h [#] x0 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
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):]
x0 (#) 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 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
h is set
x0 is V11() real ext-real Element of REAL
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):]
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):]
i [#] x0 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
(x0 (#) 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):]
x0 (#) 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):]
(x0 (#) 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 Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() (n) Element of bool [:REAL,(REAL n):]
(n,REAL,h) 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
x0 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 -valued Function-like V33() V34() V35() Element of bool [:REAL,REAL:]
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 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 REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]
(n,REAL,(x0 | h)) is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]
(n,REAL,x0) is Relation-like REAL -defined REAL -valued Function-like V33() V34() V35() Element of bool [:REAL,REAL:]
(n,REAL,x0) | h is Relation-like REAL -defined REAL -valued Function-like V33() V34() V35() Element of bool [:REAL,REAL:]
(n,REAL,x0) is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]
(n,REAL,x0) | 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
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 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 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:]
||.i.|| | h is Relation-like REAL -defined REAL -valued Function-like V33() V34() V35() Element of bool [:REAL,REAL:]
- 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 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 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
x0 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 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
x0 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 Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]
x0 | h is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]
i is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n
r 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
s is V11() real ext-real set
s * i is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like M13( REAL , REAL n)
rs0 is Element of the carrier of (REAL-NS n)
s * rs0 is Element of 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):]
s0 /. s is Element of the carrier of (REAL-NS n)
x0 /. s is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n
(s * 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)
rs0 is Element of the carrier of (REAL-NS n)
(s * rs0) + rs0 is Element of the carrier of (REAL-NS n)
s0 | 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 )
h is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
proj (h,n) is non empty Relation-like REAL n -defined REAL -valued Function-like total quasi_total V33() V34() V35() Element of bool [:(REAL n),REAL:]
[:(REAL n),REAL:] is set
bool [:(REAL n),REAL:] is set
x0 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(n) FinSequence-like FinSubsequence-like Element of REAL n
dom (proj (h,n)) is functional FinSequence-membered V227() V228() V229() Element of bool (REAL n)
bool (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
[: the carrier of (REAL-NS n),REAL:] is set
bool [: the carrier of (REAL-NS n),REAL:] is set
s0 is V11() real ext-real Element of REAL
rs0 is V11() real ext-real Element of REAL
rs0 is Element of the carrier of (REAL-NS n)
i 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:]
dom i is Element of bool the carrier of (REAL-NS n)
bool the carrier of (REAL-NS n) is set
r is Element of the carrier of (REAL-NS n)
rs0 - r is Element of the carrier of (REAL-NS n)
||.(rs0 - r).|| is V11() real ext-real 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
s - 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
s + (- x0) is Relation-like Function-like set
|.(s - x0).| is V11() real ext-real non negative Element of REAL
(proj (h,n)) /. (s - x0) is V11() real ext-real Element of REAL
(proj (h,n)) . (s - x0) is V11() real ext-real Element of REAL
(proj (h,n)) /. s is V11() real ext-real Element of REAL
(proj (h,n)) . s is V11() real ext-real Element of REAL
(proj (h,n)) /. x0 is V11() real ext-real Element of REAL
(proj (h,n)) . x0 is V11() real ext-real Element of REAL
((proj (h,n)) /. s) - ((proj (h,n)) /. x0) is V11() real ext-real Element of REAL
|.(((proj (h,n)) /. s) - ((proj (h,n)) /. x0)).| is V11() real ext-real Element of REAL
(proj (h,n)) /. rs0 is V11() real ext-real Element of REAL
(proj (h,n)) /. r is V11() real ext-real Element of REAL
((proj (h,n)) /. rs0) - ((proj (h,n)) /. r) is V11() real ext-real Element of REAL
|.(((proj (h,n)) /. rs0) - ((proj (h,n)) /. r)).| is V11() real ext-real Element of REAL
rs0 is Element of the carrier of (REAL-NS n)
rs0 - r is Element of the carrier of (REAL-NS n)
||.(rs0 - r).|| is V11() real ext-real Element of REAL
(proj (h,n)) /. rs0 is V11() real ext-real Element of REAL
((proj (h,n)) /. rs0) - ((proj (h,n)) /. r) is V11() real ext-real Element of REAL
|.(((proj (h,n)) /. rs0) - ((proj (h,n)) /. r)).| is V11() real ext-real Element of REAL
n is V11() real ext-real set
h is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
REAL h is non empty functional FinSequence-membered V227() V228() V229() M12( REAL )
[:REAL,(REAL h):] is set
bool [:REAL,(REAL h):] is set
Seg h is non empty finite V71(h) Element of bool NAT
x0 is Relation-like REAL -defined REAL h -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL h):]
dom x0 is Element of bool REAL
i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
proj (i,h) is non empty Relation-like REAL h -defined REAL -valued Function-like total quasi_total V33() V34() V35() Element of bool [:(REAL h),REAL:]
[:(REAL h),REAL:] is set
bool [:(REAL h),REAL:] is set
(proj (i,h)) * x0 is Relation-like REAL -defined REAL -valued Function-like V33() V34() V35() Element of bool [:REAL,REAL:]
dom (proj (i,h)) is functional FinSequence-membered V227() V228() V229() Element of bool (REAL h)
bool (REAL h) is set
rng x0 is functional FinSequence-membered V227() V228() V229() Element of bool (REAL h)
dom ((proj (i,h)) * x0) is Element of bool REAL
x0 /. n is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(h) FinSequence-like FinSubsequence-like Element of REAL h
x0 /. n is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(h) FinSequence-like FinSubsequence-like Element of REAL h
i is V11() real ext-real Element of REAL
i / 2 is V11() real ext-real Element of REAL
(i / 2) / h is V11() real ext-real Element of REAL
s0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
proj (s0,h) is non empty Relation-like REAL h -defined REAL -valued Function-like total quasi_total V33() V34() V35() Element of bool [:(REAL h),REAL:]
[:(REAL h),REAL:] is set
bool [:(REAL h),REAL:] is set
(proj (s0,h)) * x0 is Relation-like REAL -defined REAL -valued Function-like V33() V34() V35() Element of bool [:REAL,REAL:]
((proj (s0,h)) * x0) . n is V11() real ext-real Element of REAL
dom (proj (s0,h)) is functional FinSequence-membered V227() V228() V229() Element of bool (REAL h)
bool (REAL h) is set
rng x0 is functional FinSequence-membered V227() V228() V229() Element of bool (REAL h)
dom ((proj (s0,h)) * x0) is Element of bool REAL
rs0 is V11() real ext-real set
s0 is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite FinSequence-like FinSubsequence-like FinSequence of REAL
dom s0 is Element of bool NAT
rng s0 is complex-membered ext-real-membered real-membered Element of bool REAL
rs0 is non empty ext-real-membered set
rs0 is non empty ext-real-membered left_end right_end set
inf rs0 is ext-real set
s is V11() real ext-real Element of REAL
i1 is set
s0 . i1 is V11() real ext-real Element of REAL
i1 is V11() real ext-real set
i1 - n is V11() real ext-real Element of REAL
abs (i1 - n) is V11() real ext-real Element of REAL
x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
s0 . x1 is V11() real ext-real Element of REAL
proj (x1,h) is non empty Relation-like REAL h -defined REAL -valued Function-like total quasi_total V33() V34() V35() Element of bool [:(REAL h),REAL:]
[:(REAL h),REAL:] is set
bool [:(REAL h),REAL:] is set
(proj (x1,h)) * x0 is Relation-like REAL -defined REAL -valued Function-like V33() V34() V35() Element of bool [:REAL,REAL:]
((proj (x1,h)) * x0) . i1 is V11() real ext-real Element of REAL
((proj (x1,h)) * x0) . n is V11() real ext-real Element of REAL
(((proj (x1,h)) * x0) . i1) - (((proj (x1,h)) * x0) . n) is V11() real ext-real Element of REAL
|.((((proj (x1,h)) * x0) . i1) - (((proj (x1,h)) * x0) . n)).| is V11() real ext-real Element of REAL
x0 . i1 is Relation-like NAT -defined Function-like V33() V34() V35() finite FinSequence-like FinSubsequence-like set
(proj (x1,h)) . (x0 . i1) is V11() real ext-real Element of REAL
x0 /. i1 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(h) FinSequence-like FinSubsequence-like Element of REAL h
(proj (x1,h)) . (x0 /. i1) is V11() real ext-real Element of REAL
x0 . n is Relation-like NAT -defined Function-like V33() V34() V35() finite FinSequence-like FinSubsequence-like set
(proj (x1,h)) . (x0 . n) is V11() real ext-real Element of REAL
(proj (x1,h)) . (x0 /. n) is V11() real ext-real Element of REAL
(x0 /. i1) - (x0 /. n) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite V71(h) FinSequence-like FinSubsequence-like M13( REAL , REAL h)
- (x0 /. n) is Relation-like Function-like V33() set
K38(1) is V11() real ext-real non positive set
K38(1) (#) (x0 /. n) is Relation-like Function-like set
(x0 /. i1) + (- (x0 /. n)) is Relation-like Function-like set
(proj (x1,h)) . ((x0 /. i1) - (x0 /. n)) is V11() real ext-real Element of REAL
|.((proj (x1,h)) . ((x0 /. i1) - (x0 /. n))).| is V11() real ext-real Element of REAL
|.((x0 /. i1) - (x0 /. n)).| is V11() real ext-real non negative Element of REAL
h * ((i / 2) / h) is V11() real ext-real Element of REAL
i1 is V11() real ext-real set
i1 - n is V11() real ext-real Element of REAL
abs (i1 - n) is V11() real ext-real Element of REAL
x0 /. i1 is Relation-like NAT -defined Function-like V33() V34() V35() finite V71(h) FinSequence-like FinSubsequence-like Element of REAL h
(x0 /. i1) - (x0 /. n) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite V71(h) FinSequence-like FinSubsequence-like M13( REAL , REAL h)
(x0 /. i1) + (- (x0 /. n)) is Relation-like Function-like set
|.((x0 /. i1) - (x0 /. n)).| is V11() real ext-real non negative Element of REAL
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive 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
Seg n is non empty finite V71(n) Element of bool NAT
h is Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() Element of bool [:REAL,(REAL n):]
x0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
proj (x0,n) is non empty Relation-like REAL n -defined REAL -valued Function-like total quasi_total V33() V34() V35() Element of bool [:(REAL n),REAL:]
[:(REAL n),REAL:] is set
bool [:(REAL n),REAL:] is set
(proj (x0,n)) * h is Relation-like REAL -defined REAL -valued Function-like V33() V34() V35() Element of bool [:REAL,REAL:]
dom (proj (x0,n)) is functional FinSequence-membered V227() V228() V229() Element of bool (REAL n)
bool (REAL n) is set
rng h is functional FinSequence-membered V227() V228() V229() Element of bool (REAL n)
dom ((proj (x0,n)) * h) is Element of bool REAL
dom h is Element of bool REAL
i is V11() real ext-real set
x0 is V11() real ext-real set
dom h is Element of bool REAL
i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
proj (i,n) is non empty Relation-like REAL n -defined REAL -valued Function-like total quasi_total V33() V34() V35() Element of bool [:(REAL n),REAL:]
[:(REAL n),REAL:] is set
bool [:(REAL n),REAL:] is set
dom (proj (i,n)) is functional FinSequence-membered V227() V228() V229() Element of bool (REAL n)
bool (REAL n) is set
rng h is functional FinSequence-membered V227() V228() V229() Element of bool (REAL n)
(proj (i,n)) * h is Relation-like REAL -defined REAL -valued Function-like V33() V34() V35() Element of bool [:REAL,REAL:]
dom ((proj (i,n)) * h) is Element of bool 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
h is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
Proj (h,n) is non empty Relation-like the carrier of (REAL-NS n) -defined the carrier of (REAL-NS 1) -valued Function-like total quasi_total Element of bool [: the carrier of (REAL-NS n), the carrier of (REAL-NS 1):]
[: the carrier of (REAL-NS n), the carrier of (REAL-NS 1):] is set
bool [: the carrier of (REAL-NS n), the carrier of (REAL-NS 1):] is set
x0 is Element of the carrier of (REAL-NS n)
dom (Proj (h,n)) is Element of bool the carrier of (REAL-NS n)
bool the carrier of (REAL-NS n) is set
i is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
s0 is Element of the carrier of (REAL-NS n)
s0 - x0 is Element of the carrier of (REAL-NS n)
||.(s0 - x0).|| is V11() real ext-real Element of REAL
(Proj (h,n)) /. (s0 - x0) is Element of the carrier of (REAL-NS 1)
(Proj (h,n)) . (s0 - x0) is Element of the carrier of (REAL-NS 1)
(Proj (h,n)) /. s0 is Element of the carrier of (REAL-NS 1)
(Proj (h,n)) . s0 is Element of the carrier of (REAL-NS 1)
(Proj (h,n)) /. x0 is Element of the carrier of (REAL-NS 1)
(Proj (h,n)) . x0 is Element of the carrier of (REAL-NS 1)
((Proj (h,n)) /. s0) - ((Proj (h,n)) /. x0) is Element of the carrier of (REAL-NS 1)
||.(((Proj (h,n)) /. s0) - ((Proj (h,n)) /. x0)).|| is V11() real ext-real Element of REAL
s0 is Element of the carrier of (REAL-NS n)
s0 - x0 is Element of the carrier of (REAL-NS n)
||.(s0 - x0).|| is V11() real ext-real Element of REAL
(Proj (h,n)) /. s0 is Element of the carrier of (REAL-NS 1)
(Proj (h,n)) . s0 is Element of the carrier of (REAL-NS 1)
((Proj (h,n)) /. s0) - ((Proj (h,n)) /. x0) is Element of the carrier of (REAL-NS 1)
||.(((Proj (h,n)) /. s0) - ((Proj (h,n)) /. x0)).|| is V11() real ext-real Element of REAL
n is V11() real ext-real set
h is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
REAL-NS h 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 h) is non empty non trivial set
[:REAL, the carrier of (REAL-NS h):] is set
bool [:REAL, the carrier of (REAL-NS h):] is set
Seg h is non empty finite V71(h) Element of bool NAT
x0 is Relation-like REAL -defined the carrier of (REAL-NS h) -valued Function-like Element of bool [:REAL, the carrier of (REAL-NS h):]
dom x0 is Element of bool REAL
i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
Proj (i,h) is non empty Relation-like the carrier of (REAL-NS h) -defined the carrier of (REAL-NS 1) -valued Function-like total quasi_total Element of bool [: the carrier of (REAL-NS h), the carrier of (REAL-NS 1):]
[: the carrier of (REAL-NS h), the carrier of (REAL-NS 1):] is set
bool [: the carrier of (REAL-NS h), the carrier of (REAL-NS 1):] is set
(Proj (i,h)) * x0 is Relation-like REAL -defined the carrier of (REAL-NS 1) -valued Function-like Element of bool [:REAL, the carrier of (REAL-NS 1):]
[:REAL, the carrier of (REAL-NS 1):] is set
bool [:REAL, the carrier of (REAL-NS 1):] is set
dom (Proj (i,h)) is Element of bool the carrier of (REAL-NS h)
bool the carrier of (REAL-NS h) is set
rng x0 is Element of bool the carrier of (REAL-NS h)
dom ((Proj (i,h)) * x0) is Element of bool REAL
x0 /. n is Element of the carrier of (REAL-NS h)
Proj (1,h) is non empty Relation-like the carrier of (REAL-NS h) -defined the carrier of (REAL-NS 1) -valued Function-like total quasi_total Element of bool [: the carrier of (REAL-NS h), the carrier of (REAL-NS 1):]
[: the carrier of (REAL-NS h), the carrier of (REAL-NS 1):] is set
bool [: the carrier of (REAL-NS h), the carrier of (REAL-NS 1):] is set
(Proj (1,h)) * x0 is Relation-like REAL -defined the carrier of (REAL-NS 1) -valued Function-like Element of bool [:REAL, the carrier of (REAL-NS 1):]
[:REAL, the carrier of (REAL-NS 1):] is set
bool [:REAL, the carrier of (REAL-NS 1):] is set
dom ((Proj (1,h)) * x0) is Element of bool REAL
x0 /. n is Element of the carrier of (REAL-NS h)
i is V11() real ext-real Element of REAL
i / 2 is V11() real ext-real Element of REAL
(i / 2) / h is V11() real ext-real Element of REAL
s0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
rs0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
Proj (rs0,h) is non empty Relation-like the carrier of (REAL-NS h) -defined the carrier of (REAL-NS 1) -valued Function-like total quasi_total Element of bool [: the carrier of (REAL-NS h), the carrier of (REAL-NS 1):]
(Proj (rs0,h)) * x0 is Relation-like REAL -defined the carrier of (REAL-NS 1) -valued Function-like Element of bool [:REAL, the carrier of (REAL-NS 1):]
dom (Proj (rs0,h)) is Element of bool the carrier of (REAL-NS h)
bool the carrier of (REAL-NS h) is set
rng x0 is Element of bool the carrier of (REAL-NS h)
dom ((Proj (rs0,h)) * x0) is Element of bool REAL
((Proj (rs0,h)) * x0) /. n is Element of the carrier of (REAL-NS 1)
rs0 is V11() real ext-real set
s0 is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite FinSequence-like FinSubsequence-like FinSequence of REAL
dom s0 is Element of bool NAT
rng s0 is complex-membered ext-real-membered real-membered Element of bool REAL
rs0 is non empty ext-real-membered set
rs0 is non empty ext-real-membered left_end right_end set
inf rs0 is ext-real set
s is V11() real ext-real Element of REAL
i1 is set
s0 . i1 is V11() real ext-real Element of REAL
x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
Proj (x1,h) is non empty Relation-like the carrier of (REAL-NS h) -defined the carrier of (REAL-NS 1) -valued Function-like total quasi_total Element of bool [: the carrier of (REAL-NS h), the carrier of (REAL-NS 1):]
(Proj (x1,h)) * x0 is Relation-like REAL -defined the carrier of (REAL-NS 1) -valued Function-like Element of bool [:REAL, the carrier of (REAL-NS 1):]
((Proj (x1,h)) * x0) /. n is Element of the carrier of (REAL-NS 1)
x1 is V11() real ext-real set
x1 - n is V11() real ext-real Element of REAL
abs (x1 - n) is V11() real ext-real Element of REAL
x0 /. x1 is Element of the carrier of (REAL-NS h)
(x0 /. x1) - (x0 /. n) is Element of the carrier of (REAL-NS h)
||.((x0 /. x1) - (x0 /. n)).|| is V11() real ext-real Element of REAL
j is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
s0 . j is V11() real ext-real Element of REAL
jj is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
Proj (jj,h) is non empty Relation-like the carrier of (REAL-NS h) -defined the carrier of (REAL-NS 1) -valued Function-like total quasi_total Element of bool [: the carrier of (REAL-NS h), the carrier of (REAL-NS 1):]
(Proj (jj,h)) * x0 is Relation-like REAL -defined the carrier of (REAL-NS 1) -valued Function-like Element of bool [:REAL, the carrier of (REAL-NS 1):]
((Proj (jj,h)) * x0) /. n is Element of the carrier of (REAL-NS 1)
Proj (j,h) is non empty Relation-like the carrier of (REAL-NS h) -defined the carrier of (REAL-NS 1) -valued Function-like total quasi_total Element of bool [: the carrier of (REAL-NS h), the carrier of (REAL-NS 1):]
(Proj (j,h)) * x0 is Relation-like REAL -defined the carrier of (REAL-NS 1) -valued Function-like Element of bool [:REAL, the carrier of (REAL-NS 1):]
((Proj (j,h)) * x0) /. x1 is Element of the carrier of (REAL-NS 1)
((Proj (j,h)) * x0) /. n is Element of the carrier of (REAL-NS 1)
(((Proj (j,h)) * x0) /. x1) - (((Proj (j,h)) * x0) /. n) is Element of the carrier of (REAL-NS 1)
||.((((Proj (j,h)) * x0) /. x1) - (((Proj (j,h)) * x0) /. n)).|| is V11() real ext-real Element of REAL
dom (Proj (j,h)) is Element of bool the carrier of (REAL-NS h)
bool the carrier of (REAL-NS h) is set
(Proj (j,h)) /. (x0 /. x1) is Element of the carrier of (REAL-NS 1)
(Proj (j,h)) . (x0 /. x1) is Element of the carrier of (REAL-NS 1)
(Proj (j,h)) /. (x0 /. n) is Element of the carrier of (REAL-NS 1)
(Proj (j,h)) . (x0 /. n) is Element of the carrier of (REAL-NS 1)
(Proj (j,h)) . ((x0 /. x1) - (x0 /. n)) is Element of the carrier of (REAL-NS 1)
||.((Proj (j,h)) . ((x0 /. x1) - (x0 /. n))).|| is V11() real ext-real Element of REAL
h * ((i / 2) / h) is V11() real ext-real Element of REAL
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
REAL-NS n 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 n) is non empty non trivial set
[:REAL, the carrier of (REAL-NS n):] is set
bool [:REAL, the carrier of (REAL-NS n):] is set
Seg n is non empty finite V71(n) Element of bool NAT
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 epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
Proj (x0,n) is non empty Relation-like the carrier of (REAL-NS n) -defined the carrier of (REAL-NS 1) -valued Function-like total quasi_total Element of bool [: the carrier of (REAL-NS n), the carrier of (REAL-NS 1):]
[: the carrier of (REAL-NS n), the carrier of (REAL-NS 1):] is set
bool [: the carrier of (REAL-NS n), the carrier of (REAL-NS 1):] is set
(Proj (x0,n)) * h is Relation-like REAL -defined the carrier of (REAL-NS 1) -valued Function-like Element of bool [:REAL, the carrier of (REAL-NS 1):]
[:REAL, the carrier of (REAL-NS 1):] is set
bool [:REAL, the carrier of (REAL-NS 1):] is set
dom (Proj (x0,n)) is Element of bool the carrier of (REAL-NS n)
bool the carrier of (REAL-NS n) is set
rng h is Element of bool the carrier of (REAL-NS n)
dom ((Proj (x0,n)) * h) is Element of bool REAL
dom h is Element of bool REAL
i is V11() real ext-real set
x0 is V11() real ext-real set
dom h is Element of bool REAL
i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
Proj (i,n) is non empty Relation-like the carrier of (REAL-NS n) -defined the carrier of (REAL-NS 1) -valued Function-like total quasi_total Element of bool [: the carrier of (REAL-NS n), the carrier of (REAL-NS 1):]
[: the carrier of (REAL-NS n), the carrier of (REAL-NS 1):] is set
bool [: the carrier of (REAL-NS n), the carrier of (REAL-NS 1):] is set
dom (Proj (i,n)) is Element of bool the carrier of (REAL-NS n)
bool the carrier of (REAL-NS n) is set
rng h is Element of bool the carrier of (REAL-NS n)
(Proj (i,n)) * h is Relation-like REAL -defined the carrier of (REAL-NS 1) -valued Function-like Element of bool [:REAL, the carrier of (REAL-NS 1):]
[:REAL, the carrier of (REAL-NS 1):] is set
bool [:REAL, the carrier of (REAL-NS 1):] is set
dom ((Proj (i,n)) * h) is Element of bool REAL