:: BHSP_6 semantic presentation

REAL is non empty non trivial non finite V135() V136() V137() V141() set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V135() V136() V137() V138() V139() V140() V141() Element of bool REAL
bool REAL is non empty non trivial non finite set
{} is Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real ext-real non positive non negative finite V48() cardinal {} -element V135() V136() V137() V138() V139() V140() V141() set
COMPLEX is non empty non trivial non finite V135() V141() set
RAT is non empty non trivial non finite V135() V136() V137() V138() V141() set
INT is non empty non trivial non finite V135() V136() V137() V138() V139() V141() set
[:COMPLEX,COMPLEX:] is non empty non trivial non finite set
bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite set
[:REAL,REAL:] is non empty non trivial non finite set
bool [:REAL,REAL:] is non empty non trivial non finite set
[:[:REAL,REAL:],REAL:] is non empty non trivial non finite set
bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite set
[:RAT,RAT:] is non empty non trivial non finite set
bool [:RAT,RAT:] is non empty non trivial non finite set
[:[:RAT,RAT:],RAT:] is non empty non trivial non finite set
bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite set
[:INT,INT:] is non empty non trivial non finite set
bool [:INT,INT:] is non empty non trivial non finite set
[:[:INT,INT:],INT:] is non empty non trivial non finite set
bool [:[:INT,INT:],INT:] is non empty non trivial non finite set
[:NAT,NAT:] is non empty non trivial non finite set
[:[:NAT,NAT:],NAT:] is non empty non trivial non finite set
bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V135() V136() V137() V138() V139() V140() V141() set
bool omega is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
K101(NAT) is V27() set
[:NAT,REAL:] is non empty non trivial non finite set
bool [:NAT,REAL:] is non empty non trivial non finite set
ExtREAL is non empty V136() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
0 is Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real ext-real non positive non negative V41() V43() finite V48() cardinal {} -element V135() V136() V137() V138() V139() V140() V141() Element of NAT
addreal is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like non empty V14([:REAL,REAL:]) quasi_total commutative associative having_a_unity Element of bool [:[:REAL,REAL:],REAL:]
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of X is non empty set
the addF of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like non empty V14([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool the carrier of X is non empty set
Y is finite Element of bool the carrier of X
x is Relation-like Function-like FinSequence-like set
rng x is set
e is Relation-like NAT -defined the carrier of X -valued Function-like FinSequence-like FinSequence of the carrier of X
the addF of X "**" e is Element of the carrier of X
Y0 is Relation-like NAT -defined the carrier of X -valued Function-like FinSequence-like FinSequence of the carrier of X
rng Y0 is Element of bool the carrier of X
the addF of X "**" Y0 is Element of the carrier of X
x is Element of the carrier of X
e is Element of the carrier of X
Y0 is Relation-like NAT -defined the carrier of X -valued Function-like FinSequence-like FinSequence of the carrier of X
rng Y0 is Element of bool the carrier of X
the addF of X "**" Y0 is Element of the carrier of X
Y0 is Relation-like NAT -defined the carrier of X -valued Function-like FinSequence-like FinSequence of the carrier of X
rng Y0 is Element of bool the carrier of X
the addF of X "**" Y0 is Element of the carrier of X
Y0 is Relation-like NAT -defined the carrier of X -valued Function-like FinSequence-like FinSequence of the carrier of X
rng Y0 is Element of bool the carrier of X
the addF of X "**" Y0 is Element of the carrier of X
Y0 is Relation-like NAT -defined the carrier of X -valued Function-like FinSequence-like FinSequence of the carrier of X
rng Y0 is Element of bool the carrier of X
the addF of X "**" Y0 is Element of the carrier of X
dom Y0 is V135() V136() V137() V138() V139() V140() Element of bool NAT
[:(dom Y0),(dom Y0):] is set
bool [:(dom Y0),(dom Y0):] is non empty set
Y1 is Relation-like dom Y0 -defined dom Y0 -valued Function-like one-to-one V14( dom Y0) quasi_total onto bijective Element of bool [:(dom Y0),(dom Y0):]
Y0 * Y1 is Relation-like dom Y0 -defined the carrier of X -valued Function-like Element of bool [:(dom Y0), the carrier of X:]
[:(dom Y0), the carrier of X:] is set
bool [:(dom Y0), the carrier of X:] is non empty set
dom Y1 is V135() V136() V137() V138() V139() V140() Element of bool (dom Y0)
bool (dom Y0) is non empty set
rng Y1 is V135() V136() V137() V138() V139() V140() Element of bool (dom Y0)
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of X is non empty set
the addF of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like non empty V14([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool the carrier of X is non empty set
bool [: the carrier of X, the carrier of X:] is non empty set
Y is finite Element of bool the carrier of X
(X,Y) is Element of the carrier of X
x is Relation-like NAT -defined the carrier of X -valued Function-like FinSequence-like FinSequence of the carrier of X
rng x is Element of bool the carrier of X
the addF of X "**" x is Element of the carrier of X
e is Relation-like the carrier of X -defined the carrier of X -valued Function-like non empty V14( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of X:]
dom e is Element of bool the carrier of X
setopfunc (Y, the carrier of X, the carrier of X,e, the addF of X) is Element of the carrier of X
Y0 is set
dom x is V135() V136() V137() V138() V139() V140() Element of bool NAT
x . Y0 is set
Func_Seq (e,x) is Relation-like NAT -defined the carrier of X -valued Function-like FinSequence-like FinSequence of the carrier of X
dom (Func_Seq (e,x)) is V135() V136() V137() V138() V139() V140() Element of bool NAT
e * x is Relation-like NAT -defined the carrier of X -valued Function-like Element of bool [:NAT, the carrier of X:]
[:NAT, the carrier of X:] is non empty non trivial non finite set
bool [:NAT, the carrier of X:] is non empty non trivial non finite set
dom (e * x) is V135() V136() V137() V138() V139() V140() Element of bool NAT
Y0 is set
Y0 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
x . Y0 is set
(Func_Seq (e,x)) . Y0 is set
(e * x) . Y0 is set
e . (x . Y0) is set
x . Y0 is set
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of X is non empty set
the addF of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like non empty V14([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool the carrier of X is non empty set
bool [: the carrier of X, the carrier of X:] is non empty set
id the carrier of X is Relation-like the carrier of X -defined the carrier of X -valued Function-like one-to-one non empty V14( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of X:]
x is finite Element of bool the carrier of X
e is finite Element of bool the carrier of X
x \/ e is finite Element of bool the carrier of X
(X,x) is Element of the carrier of X
(X,e) is Element of the carrier of X
(X,x) + (X,e) is Element of the carrier of X
the addF of X . ((X,x),(X,e)) is Element of the carrier of X
Y is Relation-like the carrier of X -defined the carrier of X -valued Function-like non empty V14( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of X:]
dom Y is Element of bool the carrier of X
Y0 is finite Element of bool the carrier of X
(X,Y0) is Element of the carrier of X
setopfunc (Y0, the carrier of X, the carrier of X,Y, the addF of X) is Element of the carrier of X
setopfunc (x, the carrier of X, the carrier of X,Y, the addF of X) is Element of the carrier of X
setopfunc (e, the carrier of X, the carrier of X,Y, the addF of X) is Element of the carrier of X
(setopfunc (x, the carrier of X, the carrier of X,Y, the addF of X)) + (setopfunc (e, the carrier of X, the carrier of X,Y, the addF of X)) is Element of the carrier of X
the addF of X . ((setopfunc (x, the carrier of X, the carrier of X,Y, the addF of X)),(setopfunc (e, the carrier of X, the carrier of X,Y, the addF of X))) is Element of the carrier of X
Y0 is set
Y . Y0 is set
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of X is non empty set
bool the carrier of X is non empty set
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of X is non empty set
bool the carrier of X is non empty set
Y is Element of bool the carrier of X
x is Element of the carrier of X
e is Element of the carrier of X
Y0 is V36() real ext-real Element of REAL
2 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
Y0 / 2 is V36() real ext-real Element of REAL
Y1 is finite Element of bool the carrier of X
Z is finite Element of bool the carrier of X
Y1 \/ Z is finite Element of bool the carrier of X
(Y0 / 2) + (Y0 / 2) is V36() real ext-real Element of REAL
(X,(Y1 \/ Z)) is Element of the carrier of X
e - (X,(Y1 \/ Z)) is Element of the carrier of X
- (X,(Y1 \/ Z)) is Element of the carrier of X
e + (- (X,(Y1 \/ Z))) is Element of the carrier of X
the addF of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like non empty V14([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the addF of X . (e,(- (X,(Y1 \/ Z)))) is Element of the carrier of X
||.(e - (X,(Y1 \/ Z))).|| is V36() real ext-real Element of REAL
- (e - (X,(Y1 \/ Z))) is Element of the carrier of X
||.(- (e - (X,(Y1 \/ Z)))).|| is V36() real ext-real Element of REAL
x - (X,(Y1 \/ Z)) is Element of the carrier of X
x + (- (X,(Y1 \/ Z))) is Element of the carrier of X
the addF of X . (x,(- (X,(Y1 \/ Z)))) is Element of the carrier of X
||.(x - (X,(Y1 \/ Z))).|| is V36() real ext-real Element of REAL
||.(x - (X,(Y1 \/ Z))).|| + ||.(- (e - (X,(Y1 \/ Z)))).|| is V36() real ext-real Element of REAL
(||.(x - (X,(Y1 \/ Z))).|| + ||.(- (e - (X,(Y1 \/ Z)))).||) + Y0 is V36() real ext-real Element of REAL
(x - (X,(Y1 \/ Z))) + (- (e - (X,(Y1 \/ Z)))) is Element of the carrier of X
the addF of X . ((x - (X,(Y1 \/ Z))),(- (e - (X,(Y1 \/ Z))))) is Element of the carrier of X
||.((x - (X,(Y1 \/ Z))) + (- (e - (X,(Y1 \/ Z))))).|| is V36() real ext-real Element of REAL
||.((x - (X,(Y1 \/ Z))) + (- (e - (X,(Y1 \/ Z))))).|| + (||.(x - (X,(Y1 \/ Z))).|| + ||.(- (e - (X,(Y1 \/ Z)))).||) is V36() real ext-real Element of REAL
Y0 + (||.(x - (X,(Y1 \/ Z))).|| + ||.(- (e - (X,(Y1 \/ Z)))).||) is V36() real ext-real Element of REAL
- (||.(x - (X,(Y1 \/ Z))).|| + ||.(- (e - (X,(Y1 \/ Z)))).||) is V36() real ext-real Element of REAL
(Y0 + (||.(x - (X,(Y1 \/ Z))).|| + ||.(- (e - (X,(Y1 \/ Z)))).||)) + (- (||.(x - (X,(Y1 \/ Z))).|| + ||.(- (e - (X,(Y1 \/ Z)))).||)) is V36() real ext-real Element of REAL
(||.((x - (X,(Y1 \/ Z))) + (- (e - (X,(Y1 \/ Z))))).|| + (||.(x - (X,(Y1 \/ Z))).|| + ||.(- (e - (X,(Y1 \/ Z)))).||)) + (- (||.(x - (X,(Y1 \/ Z))).|| + ||.(- (e - (X,(Y1 \/ Z)))).||)) is V36() real ext-real Element of REAL
x - e is Element of the carrier of X
- e is Element of the carrier of X
x + (- e) is Element of the carrier of X
the addF of X . (x,(- e)) is Element of the carrier of X
||.(x - e).|| is V36() real ext-real Element of REAL
0. X is V63(X) Element of the carrier of X
(x - e) + (0. X) is Element of the carrier of X
the addF of X . ((x - e),(0. X)) is Element of the carrier of X
||.((x - e) + (0. X)).|| is V36() real ext-real Element of REAL
(X,(Y1 \/ Z)) - (X,(Y1 \/ Z)) is Element of the carrier of X
(X,(Y1 \/ Z)) + (- (X,(Y1 \/ Z))) is Element of the carrier of X
the addF of X . ((X,(Y1 \/ Z)),(- (X,(Y1 \/ Z)))) is Element of the carrier of X
(x - e) + ((X,(Y1 \/ Z)) - (X,(Y1 \/ Z))) is Element of the carrier of X
the addF of X . ((x - e),((X,(Y1 \/ Z)) - (X,(Y1 \/ Z)))) is Element of the carrier of X
||.((x - e) + ((X,(Y1 \/ Z)) - (X,(Y1 \/ Z)))).|| is V36() real ext-real Element of REAL
(x - e) + (X,(Y1 \/ Z)) is Element of the carrier of X
the addF of X . ((x - e),(X,(Y1 \/ Z))) is Element of the carrier of X
((x - e) + (X,(Y1 \/ Z))) - (X,(Y1 \/ Z)) is Element of the carrier of X
((x - e) + (X,(Y1 \/ Z))) + (- (X,(Y1 \/ Z))) is Element of the carrier of X
the addF of X . (((x - e) + (X,(Y1 \/ Z))),(- (X,(Y1 \/ Z)))) is Element of the carrier of X
||.(((x - e) + (X,(Y1 \/ Z))) - (X,(Y1 \/ Z))).|| is V36() real ext-real Element of REAL
x - (e - (X,(Y1 \/ Z))) is Element of the carrier of X
x + (- (e - (X,(Y1 \/ Z)))) is Element of the carrier of X
the addF of X . (x,(- (e - (X,(Y1 \/ Z))))) is Element of the carrier of X
(x - (e - (X,(Y1 \/ Z)))) - (X,(Y1 \/ Z)) is Element of the carrier of X
(x - (e - (X,(Y1 \/ Z)))) + (- (X,(Y1 \/ Z))) is Element of the carrier of X
the addF of X . ((x - (e - (X,(Y1 \/ Z)))),(- (X,(Y1 \/ Z)))) is Element of the carrier of X
||.((x - (e - (X,(Y1 \/ Z)))) - (X,(Y1 \/ Z))).|| is V36() real ext-real Element of REAL
(X,(Y1 \/ Z)) + (e - (X,(Y1 \/ Z))) is Element of the carrier of X
the addF of X . ((X,(Y1 \/ Z)),(e - (X,(Y1 \/ Z)))) is Element of the carrier of X
x - ((X,(Y1 \/ Z)) + (e - (X,(Y1 \/ Z)))) is Element of the carrier of X
- ((X,(Y1 \/ Z)) + (e - (X,(Y1 \/ Z)))) is Element of the carrier of X
x + (- ((X,(Y1 \/ Z)) + (e - (X,(Y1 \/ Z))))) is Element of the carrier of X
the addF of X . (x,(- ((X,(Y1 \/ Z)) + (e - (X,(Y1 \/ Z)))))) is Element of the carrier of X
||.(x - ((X,(Y1 \/ Z)) + (e - (X,(Y1 \/ Z))))).|| is V36() real ext-real Element of REAL
(x - (X,(Y1 \/ Z))) - (e - (X,(Y1 \/ Z))) is Element of the carrier of X
(x - (X,(Y1 \/ Z))) + (- (e - (X,(Y1 \/ Z)))) is Element of the carrier of X
||.((x - (X,(Y1 \/ Z))) - (e - (X,(Y1 \/ Z)))).|| is V36() real ext-real Element of REAL
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of X is non empty set
[: the carrier of X,REAL:] is non empty non trivial non finite set
bool [: the carrier of X,REAL:] is non empty non trivial non finite set
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of X is non empty set
bool the carrier of X is non empty set
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of X is non empty set
bool the carrier of X is non empty set
[: the carrier of X,REAL:] is non empty non trivial non finite set
bool [: the carrier of X,REAL:] is non empty non trivial non finite set
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of X is non empty set
bool the carrier of X is non empty set
[: the carrier of X,REAL:] is non empty non trivial non finite set
bool [: the carrier of X,REAL:] is non empty non trivial non finite set
Y is Element of bool the carrier of X
x is Relation-like the carrier of X -defined REAL -valued Function-like non empty V14( the carrier of X) quasi_total Element of bool [: the carrier of X,REAL:]
e is V36() real ext-real Element of REAL
Y0 is V36() real ext-real Element of REAL
Y0 is V36() real ext-real set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
Y0 / 2 is V36() real ext-real Element of REAL
Z is finite Element of bool the carrier of X
i is finite Element of bool the carrier of X
Z \/ i is finite Element of bool the carrier of X
(Y0 / 2) + (Y0 / 2) is V36() real ext-real Element of REAL
setopfunc ((Z \/ i), the carrier of X,REAL,x,addreal) is V36() real ext-real Element of REAL
Y0 - (setopfunc ((Z \/ i), the carrier of X,REAL,x,addreal)) is V36() real ext-real Element of REAL
abs (Y0 - (setopfunc ((Z \/ i), the carrier of X,REAL,x,addreal))) is V36() real ext-real Element of REAL
e - (setopfunc ((Z \/ i), the carrier of X,REAL,x,addreal)) is V36() real ext-real Element of REAL
(e - (setopfunc ((Z \/ i), the carrier of X,REAL,x,addreal))) - (Y0 - (setopfunc ((Z \/ i), the carrier of X,REAL,x,addreal))) is V36() real ext-real Element of REAL
abs ((e - (setopfunc ((Z \/ i), the carrier of X,REAL,x,addreal))) - (Y0 - (setopfunc ((Z \/ i), the carrier of X,REAL,x,addreal)))) is V36() real ext-real Element of REAL
abs (e - (setopfunc ((Z \/ i), the carrier of X,REAL,x,addreal))) is V36() real ext-real Element of REAL
(abs (e - (setopfunc ((Z \/ i), the carrier of X,REAL,x,addreal)))) + (abs (Y0 - (setopfunc ((Z \/ i), the carrier of X,REAL,x,addreal)))) is V36() real ext-real Element of REAL
e - Y0 is V36() real ext-real Element of REAL
abs (e - Y0) is V36() real ext-real Element of REAL
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of X is non empty set
bool the carrier of X is non empty set
Y is Element of bool the carrier of X
x is Element of the carrier of X
[: the carrier of X,REAL:] is non empty non trivial non finite set
bool [: the carrier of X,REAL:] is non empty non trivial non finite set
e is Relation-like the carrier of X -defined REAL -valued Function-like non empty V14( the carrier of X) quasi_total V129(X) V130(X) Element of bool [: the carrier of X,REAL:]
Y0 is V36() real ext-real Element of REAL
Y0 is V36() real ext-real Element of REAL
Y0 / Y0 is V36() real ext-real Element of REAL
Z is finite Element of bool the carrier of X
(Y0 / Y0) * Y0 is V36() real ext-real Element of REAL
i is finite Element of bool the carrier of X
(X,i) is Element of the carrier of X
x - (X,i) is Element of the carrier of X
- (X,i) is Element of the carrier of X
x + (- (X,i)) is Element of the carrier of X
the addF of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like non empty V14([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the addF of X . (x,(- (X,i))) is Element of the carrier of X
||.(x - (X,i)).|| is V36() real ext-real Element of REAL
Y0 * ||.(x - (X,i)).|| is V36() real ext-real Element of REAL
(Y0 * ||.(x - (X,i)).||) + Y0 is V36() real ext-real Element of REAL
e . (x - (X,i)) is V36() real ext-real Element of REAL
abs (e . (x - (X,i))) is V36() real ext-real Element of REAL
(abs (e . (x - (X,i)))) + (Y0 * ||.(x - (X,i)).||) is V36() real ext-real Element of REAL
((Y0 * ||.(x - (X,i)).||) + Y0) - (Y0 * ||.(x - (X,i)).||) is V36() real ext-real Element of REAL
((abs (e . (x - (X,i)))) + (Y0 * ||.(x - (X,i)).||)) - (Y0 * ||.(x - (X,i)).||) is V36() real ext-real Element of REAL
Y0 is V36() real ext-real Element of REAL
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of X is non empty set
[: the carrier of X,REAL:] is non empty non trivial non finite set
bool [: the carrier of X,REAL:] is non empty non trivial non finite set
the addF of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like non empty V14([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
Y is Relation-like the carrier of X -defined REAL -valued Function-like non empty V14( the carrier of X) quasi_total V129(X) V130(X) Element of bool [: the carrier of X,REAL:]
x is Relation-like NAT -defined the carrier of X -valued Function-like FinSequence-like FinSequence of the carrier of X
len x is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
dom x is V135() V136() V137() V138() V139() V140() Element of bool NAT
the addF of X "**" x is Element of the carrier of X
Y . ( the addF of X "**" x) is V36() real ext-real Element of REAL
[:NAT, the carrier of X:] is non empty non trivial non finite set
bool [:NAT, the carrier of X:] is non empty non trivial non finite set
x . 1 is set
e is Relation-like NAT -defined the carrier of X -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of X:]
e . 1 is Element of the carrier of X
e . (len x) is Element of the carrier of X
Y0 is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
dom Y0 is V135() V136() V137() V138() V139() V140() Element of bool NAT
addreal "**" Y0 is V36() real ext-real Element of REAL
len Y0 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
Seg (len Y0) is V135() V136() V137() V138() V139() V140() Element of bool NAT
Seg (len x) is V135() V136() V137() V138() V139() V140() Element of bool NAT
Y0 . 1 is set
Y0 is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,REAL:]
Y0 . 1 is V36() real ext-real Element of REAL
Y0 . (len Y0) is V36() real ext-real Element of REAL
Y1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
Y0 . Y1 is V36() real ext-real Element of REAL
e . Y1 is Element of the carrier of X
Y . (e . Y1) is V36() real ext-real Element of REAL
Y1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
Y0 . (Y1 + 1) is V36() real ext-real Element of REAL
e . (Y1 + 1) is Element of the carrier of X
Y . (e . (Y1 + 1)) is V36() real ext-real Element of REAL
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
Z is Element of the carrier of X
x . (Y1 + 1) is set
rng x is Element of bool the carrier of X
bool the carrier of X is non empty set
Y0 is Element of the carrier of X
i is Element of the carrier of X
Y . i is V36() real ext-real Element of REAL
Y1 is Element of the carrier of X
Y . Y1 is V36() real ext-real Element of REAL
(len Y0) - 0 is V36() real ext-real non negative V41() V43() Element of INT
(Y1 + 1) - 1 is V36() real ext-real V41() V43() Element of INT
Y0 . (Y1 + 1) is V36() real ext-real Element of REAL
Y0 . (Y1 + 1) is set
addreal . ((Y0 . Y1),(Y0 . (Y1 + 1))) is set
Y . Y0 is V36() real ext-real Element of REAL
addreal . ((Y . (e . Y1)),(Y . Y0)) is V36() real ext-real Element of REAL
(Y . i) + (Y . Y1) is V36() real ext-real Element of REAL
i + Y1 is Element of the carrier of X
the addF of X . (i,Y1) is Element of the carrier of X
Y . (i + Y1) is V36() real ext-real Element of REAL
e . (Y1 + 1) is Element of the carrier of X
Y . (e . (Y1 + 1)) is V36() real ext-real Element of REAL
Y0 . (Y1 + 1) is V36() real ext-real Element of REAL
e . (Y1 + 1) is Element of the carrier of X
Y . (e . (Y1 + 1)) is V36() real ext-real Element of REAL
Y0 . (Y1 + 1) is V36() real ext-real Element of REAL
e . (Y1 + 1) is Element of the carrier of X
Y . (e . (Y1 + 1)) is V36() real ext-real Element of REAL
Y0 . 0 is V36() real ext-real Element of REAL
e . 0 is Element of the carrier of X
Y . (e . 0) is V36() real ext-real Element of REAL
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of X is non empty set
the addF of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like non empty V14([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool the carrier of X is non empty set
[: the carrier of X,REAL:] is non empty non trivial non finite set
bool [: the carrier of X,REAL:] is non empty non trivial non finite set
Y is finite Element of bool the carrier of X
(X,Y) is Element of the carrier of X
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
card Y is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of omega
x is Relation-like the carrier of X -defined REAL -valued Function-like non empty V14( the carrier of X) quasi_total V129(X) V130(X) Element of bool [: the carrier of X,REAL:]
x . (X,Y) is V36() real ext-real Element of REAL
setopfunc (Y, the carrier of X,REAL,x,addreal) is V36() real ext-real Element of REAL
e is Relation-like NAT -defined the carrier of X -valued Function-like FinSequence-like FinSequence of the carrier of X
rng e is Element of bool the carrier of X
the addF of X "**" e is Element of the carrier of X
Func_Seq (x,e) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
dom e is V135() V136() V137() V138() V139() V140() Element of bool NAT
Y0 is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
Y0 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
Y0 . Y0 is set
e . Y0 is set
x . (e . Y0) is set
x * e is Relation-like NAT -defined REAL -valued Function-like Element of bool [:NAT,REAL:]
(x * e) . Y0 is set
dom x is Element of bool the carrier of X
Y0 is set
e . Y0 is set
dom (Func_Seq (x,e)) is V135() V136() V137() V138() V139() V140() Element of bool NAT
x * e is Relation-like NAT -defined REAL -valued Function-like Element of bool [:NAT,REAL:]
dom (x * e) is V135() V136() V137() V138() V139() V140() Element of bool NAT
len e is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
x . ( the addF of X "**" e) is V36() real ext-real Element of REAL
addreal "**" Y0 is V36() real ext-real Element of REAL
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of X is non empty set
the addF of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like non empty V14([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool the carrier of X is non empty set
[: the carrier of X,REAL:] is non empty non trivial non finite set
bool [: the carrier of X,REAL:] is non empty non trivial non finite set
Y is Element of bool the carrier of X
x is Element of the carrier of X
e is Relation-like the carrier of X -defined REAL -valued Function-like non empty V14( the carrier of X) quasi_total V129(X) V130(X) Element of bool [: the carrier of X,REAL:]
Y0 is V36() real ext-real Element of REAL
Y0 is finite Element of bool the carrier of X
Y1 is finite Element of bool the carrier of X
i is finite Element of bool the carrier of X
(X,i) is Element of the carrier of X
x - (X,i) is Element of the carrier of X
- (X,i) is Element of the carrier of X
x + (- (X,i)) is Element of the carrier of X
the addF of X . (x,(- (X,i))) is Element of the carrier of X
e . (x - (X,i)) is V36() real ext-real Element of REAL
e . x is V36() real ext-real Element of REAL
e . (X,i) is V36() real ext-real Element of REAL
(e . x) - (e . (X,i)) is V36() real ext-real Element of REAL
setopfunc (i, the carrier of X,REAL,e,addreal) is V36() real ext-real Element of REAL
(e . x) - (setopfunc (i, the carrier of X,REAL,e,addreal)) is V36() real ext-real Element of REAL
abs ((e . x) - (setopfunc (i, the carrier of X,REAL,e,addreal))) is V36() real ext-real Element of REAL
Z is finite Element of bool the carrier of X
setopfunc (Z, the carrier of X,REAL,e,addreal) is V36() real ext-real Element of REAL
(e . x) - (setopfunc (Z, the carrier of X,REAL,e,addreal)) is V36() real ext-real Element of REAL
abs ((e . x) - (setopfunc (Z, the carrier of X,REAL,e,addreal))) is V36() real ext-real Element of REAL
Y0 is V36() real ext-real Element of REAL
e is Relation-like the carrier of X -defined REAL -valued Function-like non empty V14( the carrier of X) quasi_total V129(X) V130(X) Element of bool [: the carrier of X,REAL:]
Y0 is V36() real ext-real Element of REAL
e . x is V36() real ext-real Element of REAL
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of X is non empty set
the addF of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like non empty V14([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool the carrier of X is non empty set
[: the carrier of X,REAL:] is non empty non trivial non finite set
bool [: the carrier of X,REAL:] is non empty non trivial non finite set
Y is Element of bool the carrier of X
x is Element of the carrier of X
e is Relation-like the carrier of X -defined REAL -valued Function-like non empty V14( the carrier of X) quasi_total V129(X) V130(X) Element of bool [: the carrier of X,REAL:]
e . x is V36() real ext-real Element of REAL
Y0 is V36() real ext-real Element of REAL
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of X is non empty set
bool the carrier of X is non empty set
[: the carrier of X,REAL:] is non empty non trivial non finite set
bool [: the carrier of X,REAL:] is non empty non trivial non finite set
the addF of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like non empty V14([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
Y is Element of bool the carrier of X
x is Relation-like the carrier of X -defined REAL -valued Function-like non empty V14( the carrier of X) quasi_total V129(X) V130(X) Element of bool [: the carrier of X,REAL:]
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of X is non empty set
bool the carrier of X is non empty set
Y is finite Element of bool the carrier of X
(X,Y) is Element of the carrier of X
e is V36() real ext-real Element of REAL
Y0 is finite Element of bool the carrier of X
(X,Y0) is Element of the carrier of X
(X,Y) - (X,Y0) is Element of the carrier of X
- (X,Y0) is Element of the carrier of X
(X,Y) + (- (X,Y0)) is Element of the carrier of X
the addF of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like non empty V14([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the addF of X . ((X,Y),(- (X,Y0))) is Element of the carrier of X
0. X is V63(X) Element of the carrier of X
||.((X,Y) - (X,Y0)).|| is V36() real ext-real Element of REAL
Y0 is finite Element of bool the carrier of X
(X,Y0) is Element of the carrier of X
(X,Y) - (X,Y0) is Element of the carrier of X
- (X,Y0) is Element of the carrier of X
(X,Y) + (- (X,Y0)) is Element of the carrier of X
the addF of X . ((X,Y),(- (X,Y0))) is Element of the carrier of X
||.((X,Y) - (X,Y0)).|| is V36() real ext-real Element of REAL
Y0 is finite Element of bool the carrier of X
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like V127() UNITSTR
the carrier of X is non empty set
the addF of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like non empty V14([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool the carrier of X is non empty set
Y is Element of bool the carrier of X
x is set
e is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
e + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
1 / (e + 1) is V36() real ext-real non negative V43() Element of RAT
0 / (e + 1) is Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real ext-real non positive non negative V43() finite V48() cardinal {} -element V135() V136() V137() V138() V139() V140() V141() Element of RAT
Y0 is V36() real ext-real Element of REAL
Y0 is finite Element of bool the carrier of X
Y1 is V36() real ext-real Element of REAL
Z is finite Element of bool the carrier of X
Y1 + 1 is V36() real ext-real Element of REAL
1 / (Y1 + 1) is V36() real ext-real Element of REAL
(X,Z) is Element of the carrier of X
||.(X,Z).|| is V36() real ext-real Element of REAL
bool Y is non empty set
[:NAT,(bool Y):] is non empty non trivial non finite set
bool [:NAT,(bool Y):] is non empty non trivial non finite set
x is Relation-like NAT -defined bool Y -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool Y):]
x is Relation-like NAT -defined bool Y -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool Y):]
x . 0 is Element of bool Y
e is Relation-like Function-like set
dom e is set
e . 0 is set
e is Relation-like Function-like set
dom e is set
e . 0 is set
Y0 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
e . Y0 is set
Y0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
1 / (Y0 + 1) is V36() real ext-real non negative V43() Element of RAT
e . (Y0 + 1) is set
(Y0 + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
1 / ((Y0 + 1) + 1) is V36() real ext-real non negative V43() Element of RAT
Y0 is finite Element of bool the carrier of X
(X,Y0) is Element of the carrier of X
||.(X,Y0).|| is V36() real ext-real Element of REAL
x . (Y0 + 1) is Element of bool Y
(x . (Y0 + 1)) \/ (e . Y0) is set
Y0 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
e . Y0 is set
Y0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
e . (Y0 + 1) is set
x . (Y0 + 1) is Element of bool Y
(x . (Y0 + 1)) \/ (e . Y0) is set
x . (Y0 + 1) is Element of bool Y
(x . (Y0 + 1)) \/ (e . Y0) is set
Y0 is finite Element of bool the carrier of X
(X,Y0) is Element of the carrier of X
||.(X,Y0).|| is V36() real ext-real Element of REAL
Y1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
e . Y1 is set
Y0 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
e . Y0 is set
Y0 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
e . Y0 is set
Y0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
e . (Y0 + 1) is set
x . (Y0 + 1) is Element of bool Y
(x . (Y0 + 1)) \/ (e . Y0) is set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
1 / (0 + 1) is V36() real ext-real non negative V43() Element of RAT
Y0 is finite Element of bool the carrier of X
(X,Y0) is Element of the carrier of X
||.(X,Y0).|| is V36() real ext-real Element of REAL
Y0 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
e . Y0 is set
Y0 is set
rng e is set
Y0 is set
e . Y0 is set
Y1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
e . Y1 is set
x is Relation-like NAT -defined bool Y -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool Y):]
x is Relation-like NAT -defined bool Y -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool Y):]
e is set
x . e is set
Y0 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
x . Y0 is Element of bool Y
Y0 is finite Element of bool the carrier of X
(X,Y0) is Element of the carrier of X
Y1 is set
Z is finite Element of bool the carrier of X
(X,Z) is Element of the carrier of X
[:NAT, the carrier of X:] is non empty non trivial non finite set
bool [:NAT, the carrier of X:] is non empty non trivial non finite set
e is Relation-like NAT -defined the carrier of X -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of X:]
e is Relation-like NAT -defined the carrier of X -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of X:]
Y0 is V36() real ext-real Element of REAL
2 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
Y0 / 2 is V36() real ext-real Element of REAL
0 / 2 is Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real ext-real non positive non negative V43() finite V48() cardinal {} -element V135() V136() V137() V138() V139() V140() V141() Element of RAT
(Y0 / 2) " is V36() real ext-real Element of REAL
Z is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
i is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
1 / (i + 1) is V36() real ext-real non negative V43() Element of RAT
Z + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
((Y0 / 2) ") + 0 is V36() real ext-real Element of REAL
1 / ((Y0 / 2) ") is V36() real ext-real Element of REAL
1 / (Z + 1) is V36() real ext-real non negative V43() Element of RAT
((Y0 / 2) ") " is V36() real ext-real Element of REAL
1 * (((Y0 / 2) ") ") is V36() real ext-real Element of REAL
Y1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
Y1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
1 / (Y1 + 1) is V36() real ext-real non negative V43() Element of RAT
Y1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
Y1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
1 / (Y1 + 1) is V36() real ext-real non negative V43() Element of RAT
Z is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
i is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
x . i is Element of bool Y
Y0 is Relation-like NAT -defined the carrier of X -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of X:]
Y0 . i is Element of the carrier of X
Y0 is finite Element of bool the carrier of X
(X,Y0) is Element of the carrier of X
x . Y1 is Element of bool Y
Y0 . Y1 is Element of the carrier of X
Y1 is finite Element of bool the carrier of X
(X,Y1) is Element of the carrier of X
x . Z is Element of bool Y
Y0 . Z is Element of the carrier of X
Y2 is finite Element of bool the carrier of X
(X,Y2) is Element of the carrier of X
(Y0 . Z) - (Y0 . i) is Element of the carrier of X
- (Y0 . i) is Element of the carrier of X
(Y0 . Z) + (- (Y0 . i)) is Element of the carrier of X
the addF of X . ((Y0 . Z),(- (Y0 . i))) is Element of the carrier of X
0. X is V63(X) Element of the carrier of X
||.((Y0 . Z) - (Y0 . i)).|| is V36() real ext-real Element of REAL
Y0 \ Y1 is finite Element of bool the carrier of X
Y02 is finite Element of bool the carrier of X
Y1 \/ Y02 is finite Element of bool the carrier of X
Y1 \/ Y0 is finite Element of bool the carrier of X
Y02 is finite Element of bool the carrier of X
Y1 \/ Y02 is finite Element of bool the carrier of X
Y02 is finite Element of bool the carrier of X
Y1 \/ Y02 is finite Element of bool the carrier of X
(X,Y02) is Element of the carrier of X
||.(X,Y02).|| is V36() real ext-real Element of REAL
(X,Y1) + (X,Y02) is Element of the carrier of X
the addF of X . ((X,Y1),(X,Y02)) is Element of the carrier of X
(Y0 . Z) - (Y0 . i) is Element of the carrier of X
- (Y0 . i) is Element of the carrier of X
(Y0 . Z) + (- (Y0 . i)) is Element of the carrier of X
the addF of X . ((Y0 . Z),(- (Y0 . i))) is Element of the carrier of X
||.((Y0 . Z) - (Y0 . i)).|| is V36() real ext-real Element of REAL
(X,Y1) - (X,Y1) is Element of the carrier of X
- (X,Y1) is Element of the carrier of X
(X,Y1) + (- (X,Y1)) is Element of the carrier of X
the addF of X . ((X,Y1),(- (X,Y1))) is Element of the carrier of X
((X,Y1) - (X,Y1)) - (X,Y02) is Element of the carrier of X
- (X,Y02) is Element of the carrier of X
((X,Y1) - (X,Y1)) + (- (X,Y02)) is Element of the carrier of X
the addF of X . (((X,Y1) - (X,Y1)),(- (X,Y02))) is Element of the carrier of X
||.(((X,Y1) - (X,Y1)) - (X,Y02)).|| is V36() real ext-real Element of REAL
0. X is V63(X) Element of the carrier of X
(0. X) - (X,Y02) is Element of the carrier of X
(0. X) + (- (X,Y02)) is Element of the carrier of X
the addF of X . ((0. X),(- (X,Y02))) is Element of the carrier of X
||.((0. X) - (X,Y02)).|| is V36() real ext-real Element of REAL
||.(- (X,Y02)).|| is V36() real ext-real Element of REAL
Y0 * 1 is V36() real ext-real Element of REAL
1 / 2 is V36() real ext-real non negative V43() Element of RAT
Y0 * (1 / 2) is V36() real ext-real Element of REAL
(Y0 . Z) - (Y0 . i) is Element of the carrier of X
- (Y0 . i) is Element of the carrier of X
(Y0 . Z) + (- (Y0 . i)) is Element of the carrier of X
the addF of X . ((Y0 . Z),(- (Y0 . i))) is Element of the carrier of X
||.((Y0 . Z) - (Y0 . i)).|| is V36() real ext-real Element of REAL
(Y0 . Z) - (Y0 . i) is Element of the carrier of X
- (Y0 . i) is Element of the carrier of X
(Y0 . Z) + (- (Y0 . i)) is Element of the carrier of X
the addF of X . ((Y0 . Z),(- (Y0 . i))) is Element of the carrier of X
||.((Y0 . Z) - (Y0 . i)).|| is V36() real ext-real Element of REAL
(Y0 . Y1) - (Y0 . i) is Element of the carrier of X
- (Y0 . i) is Element of the carrier of X
(Y0 . Y1) + (- (Y0 . i)) is Element of the carrier of X
the addF of X . ((Y0 . Y1),(- (Y0 . i))) is Element of the carrier of X
0. X is V63(X) Element of the carrier of X
Y2 \ Y1 is finite Element of bool the carrier of X
Y02 is finite Element of bool the carrier of X
Y1 \/ Y02 is finite Element of bool the carrier of X
Y1 \/ Y2 is finite Element of bool the carrier of X
Y02 is finite Element of bool the carrier of X
Y1 \/ Y02 is finite Element of bool the carrier of X
Y02 is finite Element of bool the carrier of X
Y1 \/ Y02 is finite Element of bool the carrier of X
(X,Y02) is Element of the carrier of X
(Y0 . Y1) + (X,Y02) is Element of the carrier of X
the addF of X . ((Y0 . Y1),(X,Y02)) is Element of the carrier of X
(Y0 . Z) - (Y0 . Y1) is Element of the carrier of X
- (Y0 . Y1) is Element of the carrier of X
(Y0 . Z) + (- (Y0 . Y1)) is Element of the carrier of X
the addF of X . ((Y0 . Z),(- (Y0 . Y1))) is Element of the carrier of X
(X,Y02) + (- (Y0 . Y1)) is Element of the carrier of X
the addF of X . ((X,Y02),(- (Y0 . Y1))) is Element of the carrier of X
(Y0 . Y1) + ((X,Y02) + (- (Y0 . Y1))) is Element of the carrier of X
the addF of X . ((Y0 . Y1),((X,Y02) + (- (Y0 . Y1)))) is Element of the carrier of X
(Y0 . Y1) - (X,Y02) is Element of the carrier of X
- (X,Y02) is Element of the carrier of X
(Y0 . Y1) + (- (X,Y02)) is Element of the carrier of X
the addF of X . ((Y0 . Y1),(- (X,Y02))) is Element of the carrier of X
(Y0 . Y1) - ((Y0 . Y1) - (X,Y02)) is Element of the carrier of X
- ((Y0 . Y1) - (X,Y02)) is Element of the carrier of X
(Y0 . Y1) + (- ((Y0 . Y1) - (X,Y02))) is Element of the carrier of X
the addF of X . ((Y0 . Y1),(- ((Y0 . Y1) - (X,Y02)))) is Element of the carrier of X
(X,Y1) - (X,Y1) is Element of the carrier of X
- (X,Y1) is Element of the carrier of X
(X,Y1) + (- (X,Y1)) is Element of the carrier of X
the addF of X . ((X,Y1),(- (X,Y1))) is Element of the carrier of X
((X,Y1) - (X,Y1)) + (X,Y02) is Element of the carrier of X
the addF of X . (((X,Y1) - (X,Y1)),(X,Y02)) is Element of the carrier of X
(0. X) + (X,Y02) is Element of the carrier of X
the addF of X . ((0. X),(X,Y02)) is Element of the carrier of X
(Y0 . Z) - (Y0 . i) is Element of the carrier of X
(Y0 . Z) + (- (Y0 . i)) is Element of the carrier of X
the addF of X . ((Y0 . Z),(- (Y0 . i))) is Element of the carrier of X
((Y0 . Z) - (Y0 . i)) + (0. X) is Element of the carrier of X
the addF of X . (((Y0 . Z) - (Y0 . i)),(0. X)) is Element of the carrier of X
(Y0 . Y1) - (Y0 . Y1) is Element of the carrier of X
(Y0 . Y1) + (- (Y0 . Y1)) is Element of the carrier of X
the addF of X . ((Y0 . Y1),(- (Y0 . Y1))) is Element of the carrier of X
((Y0 . Z) - (Y0 . i)) + ((Y0 . Y1) - (Y0 . Y1)) is Element of the carrier of X
the addF of X . (((Y0 . Z) - (Y0 . i)),((Y0 . Y1) - (Y0 . Y1))) is Element of the carrier of X
(Y0 . i) - ((Y0 . Y1) - (Y0 . Y1)) is Element of the carrier of X
- ((Y0 . Y1) - (Y0 . Y1)) is Element of the carrier of X
(Y0 . i) + (- ((Y0 . Y1) - (Y0 . Y1))) is Element of the carrier of X
the addF of X . ((Y0 . i),(- ((Y0 . Y1) - (Y0 . Y1)))) is Element of the carrier of X
(Y0 . Z) - ((Y0 . i) - ((Y0 . Y1) - (Y0 . Y1))) is Element of the carrier of X
- ((Y0 . i) - ((Y0 . Y1) - (Y0 . Y1))) is Element of the carrier of X
(Y0 . Z) + (- ((Y0 . i) - ((Y0 . Y1) - (Y0 . Y1)))) is Element of the carrier of X
the addF of X . ((Y0 . Z),(- ((Y0 . i) - ((Y0 . Y1) - (Y0 . Y1))))) is Element of the carrier of X
(Y0 . i) - (Y0 . Y1) is Element of the carrier of X
(Y0 . i) + (- (Y0 . Y1)) is Element of the carrier of X
the addF of X . ((Y0 . i),(- (Y0 . Y1))) is Element of the carrier of X
((Y0 . i) - (Y0 . Y1)) + (Y0 . Y1) is Element of the carrier of X
the addF of X . (((Y0 . i) - (Y0 . Y1)),(Y0 . Y1)) is Element of the carrier of X
(Y0 . Z) - (((Y0 . i) - (Y0 . Y1)) + (Y0 . Y1)) is Element of the carrier of X
- (((Y0 . i) - (Y0 . Y1)) + (Y0 . Y1)) is Element of the carrier of X
(Y0 . Z) + (- (((Y0 . i) - (Y0 . Y1)) + (Y0 . Y1))) is Element of the carrier of X
the addF of X . ((Y0 . Z),(- (((Y0 . i) - (Y0 . Y1)) + (Y0 . Y1)))) is Element of the carrier of X
(Y0 . Y1) - ((Y0 . Y1) - (Y0 . i)) is Element of the carrier of X
- ((Y0 . Y1) - (Y0 . i)) is Element of the carrier of X
(Y0 . Y1) + (- ((Y0 . Y1) - (Y0 . i))) is Element of the carrier of X
the addF of X . ((Y0 . Y1),(- ((Y0 . Y1) - (Y0 . i)))) is Element of the carrier of X
(Y0 . Z) - ((Y0 . Y1) - ((Y0 . Y1) - (Y0 . i))) is Element of the carrier of X
- ((Y0 . Y1) - ((Y0 . Y1) - (Y0 . i))) is Element of the carrier of X
(Y0 . Z) + (- ((Y0 . Y1) - ((Y0 . Y1) - (Y0 . i)))) is Element of the carrier of X
the addF of X . ((Y0 . Z),(- ((Y0 . Y1) - ((Y0 . Y1) - (Y0 . i))))) is Element of the carrier of X
(X,Y02) + (0. X) is Element of the carrier of X
the addF of X . ((X,Y02),(0. X)) is Element of the carrier of X
||.((Y0 . Z) - (Y0 . i)).|| is V36() real ext-real Element of REAL
||.(X,Y02).|| is V36() real ext-real Element of REAL
||.(0. X).|| is V36() real ext-real Element of REAL
||.(X,Y02).|| + ||.(0. X).|| is V36() real ext-real Element of REAL
||.(X,Y02).|| + 0 is V36() real ext-real Element of REAL
(Y0 / 2) + (Y0 / 2) is V36() real ext-real Element of REAL
||.((Y0 . Z) - (Y0 . i)).|| + 0 is V36() real ext-real Element of REAL
Y0 \ Y1 is finite Element of bool the carrier of X
Y02 is finite Element of bool the carrier of X
Y1 \/ Y02 is finite Element of bool the carrier of X
Y1 \/ Y0 is finite Element of bool the carrier of X
Y02 is finite Element of bool the carrier of X
Y1 \/ Y02 is finite Element of bool the carrier of X
Y02 is finite Element of bool the carrier of X
Y1 \/ Y02 is finite Element of bool the carrier of X
(X,Y02) is Element of the carrier of X
||.(X,Y02).|| is V36() real ext-real Element of REAL
Y2 \ Y1 is finite Element of bool the carrier of X
Y01 is finite Element of bool the carrier of X
Y1 \/ Y01 is finite Element of bool the carrier of X
Y1 \/ Y2 is finite Element of bool the carrier of X
Y01 is finite Element of bool the carrier of X
Y1 \/ Y01 is finite Element of bool the carrier of X
Y01 is finite Element of bool the carrier of X
Y1 \/ Y01 is finite Element of bool the carrier of X
(X,Y01) is Element of the carrier of X
(X,Y1) + (X,Y01) is Element of the carrier of X
the addF of X . ((X,Y1),(X,Y01)) is Element of the carrier of X
(Y0 . Z) - (Y0 . Y1) is Element of the carrier of X
- (Y0 . Y1) is Element of the carrier of X
(Y0 . Z) + (- (Y0 . Y1)) is Element of the carrier of X
the addF of X . ((Y0 . Z),(- (Y0 . Y1))) is Element of the carrier of X
(Y0 . Y1) + (- (Y0 . Y1)) is Element of the carrier of X
the addF of X . ((Y0 . Y1),(- (Y0 . Y1))) is Element of the carrier of X
(X,Y01) + ((Y0 . Y1) + (- (Y0 . Y1))) is Element of the carrier of X
the addF of X . ((X,Y01),((Y0 . Y1) + (- (Y0 . Y1)))) is Element of the carrier of X
0. X is V63(X) Element of the carrier of X
(X,Y01) + (0. X) is Element of the carrier of X
the addF of X . ((X,Y01),(0. X)) is Element of the carrier of X
(X,Y1) + (X,Y02) is Element of the carrier of X
the addF of X . ((X,Y1),(X,Y02)) is Element of the carrier of X
(Y0 . i) - (Y0 . Y1) is Element of the carrier of X
(Y0 . i) + (- (Y0 . Y1)) is Element of the carrier of X
the addF of X . ((Y0 . i),(- (Y0 . Y1))) is Element of the carrier of X
(X,Y02) + ((Y0 . Y1) + (- (Y0 . Y1))) is Element of the carrier of X
the addF of X . ((X,Y02),((Y0 . Y1) + (- (Y0 . Y1)))) is Element of the carrier of X
(X,Y02) + (0. X) is Element of the carrier of X
the addF of X . ((X,Y02),(0. X)) is Element of the carrier of X
(Y0 . Z) - (Y0 . i) is Element of the carrier of X
- (Y0 . i) is Element of the carrier of X
(Y0 . Z) + (- (Y0 . i)) is Element of the carrier of X
the addF of X . ((Y0 . Z),(- (Y0 . i))) is Element of the carrier of X
((Y0 . Z) - (Y0 . i)) + (0. X) is Element of the carrier of X
the addF of X . (((Y0 . Z) - (Y0 . i)),(0. X)) is Element of the carrier of X
(Y0 . Y1) - (Y0 . Y1) is Element of the carrier of X
(Y0 . Y1) + (- (Y0 . Y1)) is Element of the carrier of X
((Y0 . Z) - (Y0 . i)) + ((Y0 . Y1) - (Y0 . Y1)) is Element of the carrier of X
the addF of X . (((Y0 . Z) - (Y0 . i)),((Y0 . Y1) - (Y0 . Y1))) is Element of the carrier of X
(Y0 . i) - ((Y0 . Y1) - (Y0 . Y1)) is Element of the carrier of X
- ((Y0 . Y1) - (Y0 . Y1)) is Element of the carrier of X
(Y0 . i) + (- ((Y0 . Y1) - (Y0 . Y1))) is Element of the carrier of X
the addF of X . ((Y0 . i),(- ((Y0 . Y1) - (Y0 . Y1)))) is Element of the carrier of X
(Y0 . Z) - ((Y0 . i) - ((Y0 . Y1) - (Y0 . Y1))) is Element of the carrier of X
- ((Y0 . i) - ((Y0 . Y1) - (Y0 . Y1))) is Element of the carrier of X
(Y0 . Z) + (- ((Y0 . i) - ((Y0 . Y1) - (Y0 . Y1)))) is Element of the carrier of X
the addF of X . ((Y0 . Z),(- ((Y0 . i) - ((Y0 . Y1) - (Y0 . Y1))))) is Element of the carrier of X
((Y0 . i) - (Y0 . Y1)) + (Y0 . Y1) is Element of the carrier of X
the addF of X . (((Y0 . i) - (Y0 . Y1)),(Y0 . Y1)) is Element of the carrier of X
(Y0 . Z) - (((Y0 . i) - (Y0 . Y1)) + (Y0 . Y1)) is Element of the carrier of X
- (((Y0 . i) - (Y0 . Y1)) + (Y0 . Y1)) is Element of the carrier of X
(Y0 . Z) + (- (((Y0 . i) - (Y0 . Y1)) + (Y0 . Y1))) is Element of the carrier of X
the addF of X . ((Y0 . Z),(- (((Y0 . i) - (Y0 . Y1)) + (Y0 . Y1)))) is Element of the carrier of X
(Y0 . Y1) - (Y0 . i) is Element of the carrier of X
(Y0 . Y1) + (- (Y0 . i)) is Element of the carrier of X
the addF of X . ((Y0 . Y1),(- (Y0 . i))) is Element of the carrier of X
(Y0 . Y1) - ((Y0 . Y1) - (Y0 . i)) is Element of the carrier of X
- ((Y0 . Y1) - (Y0 . i)) is Element of the carrier of X
(Y0 . Y1) + (- ((Y0 . Y1) - (Y0 . i))) is Element of the carrier of X
the addF of X . ((Y0 . Y1),(- ((Y0 . Y1) - (Y0 . i)))) is Element of the carrier of X
(Y0 . Z) - ((Y0 . Y1) - ((Y0 . Y1) - (Y0 . i))) is Element of the carrier of X
- ((Y0 . Y1) - ((Y0 . Y1) - (Y0 . i))) is Element of the carrier of X
(Y0 . Z) + (- ((Y0 . Y1) - ((Y0 . Y1) - (Y0 . i)))) is Element of the carrier of X
the addF of X . ((Y0 . Z),(- ((Y0 . Y1) - ((Y0 . Y1) - (Y0 . i))))) is Element of the carrier of X
(Y0 . Y1) + (- (Y0 . i)) is Element of the carrier of X
((Y0 . Z) - (Y0 . Y1)) + ((Y0 . Y1) + (- (Y0 . i))) is Element of the carrier of X
the addF of X . (((Y0 . Z) - (Y0 . Y1)),((Y0 . Y1) + (- (Y0 . i)))) is Element of the carrier of X
- (X,Y02) is Element of the carrier of X
(X,Y01) + (- (X,Y02)) is Element of the carrier of X
the addF of X . ((X,Y01),(- (X,Y02))) is Element of the carrier of X
||.((Y0 . Z) - (Y0 . i)).|| is V36() real ext-real Element of REAL
||.(X,Y01).|| is V36() real ext-real Element of REAL
||.(- (X,Y02)).|| is V36() real ext-real Element of REAL
||.(X,Y01).|| + ||.(- (X,Y02)).|| is V36() real ext-real Element of REAL
||.(X,Y01).|| + ||.(X,Y02).|| is V36() real ext-real Element of REAL
(Y0 / 2) + (Y0 / 2) is V36() real ext-real Element of REAL
(Y0 . Z) - (Y0 . i) is Element of the carrier of X
- (Y0 . i) is Element of the carrier of X
(Y0 . Z) + (- (Y0 . i)) is Element of the carrier of X
the addF of X . ((Y0 . Z),(- (Y0 . i))) is Element of the carrier of X
||.((Y0 . Z) - (Y0 . i)).|| is V36() real ext-real Element of REAL
(Y0 . Z) - (Y0 . i) is Element of the carrier of X
- (Y0 . i) is Element of the carrier of X
(Y0 . Z) + (- (Y0 . i)) is Element of the carrier of X
the addF of X . ((Y0 . Z),(- (Y0 . i))) is Element of the carrier of X
||.((Y0 . Z) - (Y0 . i)).|| is V36() real ext-real Element of REAL
(Y0 . Z) - (Y0 . i) is Element of the carrier of X
- (Y0 . i) is Element of the carrier of X
(Y0 . Z) + (- (Y0 . i)) is Element of the carrier of X
the addF of X . ((Y0 . Z),(- (Y0 . i))) is Element of the carrier of X
||.((Y0 . Z) - (Y0 . i)).|| is V36() real ext-real Element of REAL
(Y0 . Z) - (Y0 . i) is Element of the carrier of X
- (Y0 . i) is Element of the carrier of X
(Y0 . Z) + (- (Y0 . i)) is Element of the carrier of X
the addF of X . ((Y0 . Z),(- (Y0 . i))) is Element of the carrier of X
||.((Y0 . Z) - (Y0 . i)).|| is V36() real ext-real Element of REAL
Y0 is Element of the carrier of X
Y1 is V36() real ext-real Element of REAL
Y1 / 2 is V36() real ext-real Element of REAL
Z is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
(Y1 / 2) " is V36() real ext-real Element of REAL
Y0 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
Y0 + Z is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
Y1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
Y1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
1 / (Y1 + 1) is V36() real ext-real non negative V43() Element of RAT
((Y1 / 2) ") + 0 is V36() real ext-real Element of REAL
1 / ((Y1 / 2) ") is V36() real ext-real Element of REAL
((Y1 / 2) ") " is V36() real ext-real Element of REAL
1 * (((Y1 / 2) ") ") is V36() real ext-real Element of REAL
i is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
1 / (i + 1) is V36() real ext-real non negative V43() Element of RAT
i is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative V41() V43() finite cardinal V135() V136() V137() V138() V139() V140() Element of NAT
1 / (i + 1) is V36() real ext-real non negative V43() Element of RAT
x . i is Element of bool Y
Y0 . i is Element of the carrier of X
Y0 is finite Element of bool the carrier of X
(X,Y0) is Element of the carrier of X
(X,Y0) - Y0 is Element of the carrier of X
- Y0 is Element of the carrier of X
(X,Y0) + (- Y0) is Element of the carrier of X
the addF of X . ((X,Y0),(- Y0)) is Element of the carrier of X
||.((X,Y0) - Y0).|| is V36() real ext-real Element of REAL
Y1 is finite Element of bool the carrier of X
(X,Y1) is Element of the carrier of X
Y0 - (X,Y1) is Element of the carrier of X
- (X,Y1) is Element of the carrier of X
Y0 + (- (X,Y1)) is Element of the carrier of X
the addF of X . (Y0,(- (X,Y1))) is Element of the carrier of X
||.(Y0 - (X,Y1)).|| is V36() real ext-real Element of REAL
Y0 - (X,Y0) is Element of the carrier of X
- (X,Y0) is Element of the carrier of X
Y0 + (- (X,Y0)) is Element of the carrier of X
the addF of X . (Y0,(- (X,Y0))) is Element of the carrier of X
- (Y0 - (X,Y0)) is Element of the carrier of X
||.(- (Y0 - (X,Y0))).|| is V36() real ext-real Element of REAL
(Y1 / 2) + (Y1 / 2) is V36() real ext-real Element of REAL
||.(Y0 - (X,Y1)).|| + 0 is V36() real ext-real Element of REAL
Y1 \ Y0 is finite Element of bool the carrier of X
Y2 is finite Element of bool the carrier of X
Y0 \/ Y2 is finite Element of bool the carrier of X
Y0 \/ Y1 is finite Element of bool the carrier of X
Y2 is finite Element of bool the carrier of X
Y0 \/ Y2 is finite Element of bool the carrier of X
Y2 is finite Element of bool the carrier of X
Y0 \/ Y2 is finite Element of bool the carrier of X
(X,Y1) is Element of the carrier of X
(X,Y1) - Y0 is Element of the carrier of X
(X,Y1) + (- Y0) is Element of the carrier of X
the addF of X . ((X,Y1),(- Y0)) is Element of the carrier of X
(X,Y2) is Element of the carrier of X
(X,Y0) + (X,Y2) is Element of the carrier of X
the addF of X . ((X,Y0),(X,Y2)) is Element of the carrier of X
((X,Y0) + (X,Y2)) - Y0 is Element of the carrier of X
((X,Y0) + (X,Y2)) + (- Y0) is Element of the carrier of X
the addF of X . (((X,Y0) + (X,Y2)),(- Y0)) is Element of the carrier of X
((X,Y0) - Y0) + (X,Y2) is Element of the carrier of X
the addF of X . (((X,Y0) - Y0),(X,Y2)) is Element of the carrier of X
||.((X,Y1) - Y0).|| is V36() real ext-real Element of REAL
||.(X,Y2).|| is V36() real ext-real Element of REAL
||.((X,Y0) - Y0).|| + ||.(X,Y2).|| is V36() real ext-real Element of REAL
- ((X,Y1) - Y0) is Element of the carrier of X
||.(- ((X,Y1) - Y0)).|| is V36() real ext-real Element of REAL
- (X,Y1) is Element of the carrier of X
Y0 + (- (X,Y1)) is Element of the carrier of X
the addF of X . (Y0,(- (X,Y1))) is Element of the carrier of X
||.(Y0 + (- (X,Y1))).|| is V36() real ext-real Element of REAL
(Y1 / 2) + (Y1 / 2) is V36() real ext-real Element of REAL
Y0 - (X,Y1) is Element of the carrier of X
Y0 + (- (X,Y1)) is Element of the carrier of X
||.(Y0 - (X,Y1)).|| is V36() real ext-real Element of REAL
(X,Y1) is Element of the carrier of X
Y0 - (X,Y1) is Element of the carrier of X
- (X,Y1) is Element of the carrier of X
Y0 + (- (X,Y1)) is Element of the carrier of X
the addF of X . (Y0,(- (X,Y1))) is Element of the carrier of X
||.(Y0 - (X,Y1)).|| is V36() real ext-real Element of REAL
(X,Y1) is Element of the carrier of X
Y0 - (X,Y1) is Element of the carrier of X
- (X,Y1) is Element of the carrier of X
Y0 + (- (X,Y1)) is Element of the carrier of X
the addF of X . (Y0,(- (X,Y1))) is Element of the carrier of X
||.(Y0 - (X,Y1)).|| is V36() real ext-real Element of REAL
x is Element of the carrier of X
e is V36() real ext-real Element of REAL
e / 2 is V36() real ext-real Element of REAL
Y0 is finite Element of bool the carrier of X
Y1 is finite Element of bool the carrier of X
Y0 is non empty finite Element of bool the carrier of X
Y0 \/ Y1 is non empty finite Element of bool the carrier of X
(X,(Y0 \/ Y1)) is Element of the carrier of X
x - (X,(Y0 \/ Y1)) is Element of the carrier of X
- (X,(Y0 \/ Y1)) is Element of the carrier of X
x + (- (X,(Y0 \/ Y1))) is Element of the carrier of X
the addF of X . (x,(- (X,(Y0 \/ Y1)))) is Element of the carrier of X
||.(x - (X,(Y0 \/ Y1))).|| is V36() real ext-real Element of REAL
(e / 2) + (e / 2) is V36() real ext-real Element of REAL
(X,Y0) is Element of the carrier of X
x - (X,Y0) is Element of the carrier of X
- (X,Y0) is Element of the carrier of X
x + (- (X,Y0)) is Element of the carrier of X
the addF of X . (x,(- (X,Y0))) is Element of the carrier of X
||.(x - (X,Y0)).|| is V36() real ext-real Element of REAL
||.(x - (X,(Y0 \/ Y1))).|| + ||.(x - (X,Y0)).|| is V36() real ext-real Element of REAL
(x - (X,(Y0 \/ Y1))) - (x - (X,Y0)) is Element of the carrier of X
- (x - (X,Y0)) is Element of the carrier of X
(x - (X,(Y0 \/ Y1))) + (- (x - (X,Y0))) is Element of the carrier of X
the addF of X . ((x - (X,(Y0 \/ Y1))),(- (x - (X,Y0)))) is Element of the carrier of X
||.((x - (X,(Y0 \/ Y1))) - (x - (X,Y0))).|| is V36() real ext-real Element of REAL
||.(- (x - (X,Y0))).|| is V36() real ext-real Element of REAL
||.(x - (X,(Y0 \/ Y1))).|| + ||.(- (x - (X,Y0))).|| is V36() real ext-real Element of REAL
(X,(Y0 \/ Y1)) - (X,Y0) is Element of the carrier of X
(X,(Y0 \/ Y1)) + (- (X,Y0)) is Element of the carrier of X
the addF of X . ((X,(Y0 \/ Y1)),(- (X,Y0))) is Element of the carrier of X
(X,Y1) is Element of the carrier of X
(X,Y1) + (X,Y0) is Element of the carrier of X
the addF of X . ((X,Y1),(X,Y0)) is Element of the carrier of X
((X,Y1) + (X,Y0)) - (X,Y0) is Element of the carrier of X
((X,Y1) + (X,Y0)) + (- (X,Y0)) is Element of the carrier of X
the addF of X . (((X,Y1) + (X,Y0)),(- (X,Y0))) is Element of the carrier of X
(X,Y0) + (- (X,Y0)) is Element of the carrier of X
the addF of X . ((X,Y0),(- (X,Y0))) is Element of the carrier of X
(X,Y1) + ((X,Y0) + (- (X,Y0))) is Element of the carrier of X
the addF of X . ((X,Y1),((X,Y0) + (- (X,Y0)))) is Element of the carrier of X
0. X is V63(X) Element of the carrier of X
(X,Y1) + (0. X) is Element of the carrier of X
the addF of X . ((X,Y1),(0. X)) is Element of the carrier of X
||.(X,Y1).|| is V36() real ext-real Element of REAL
- ((X,(Y0 \/ Y1)) - (X,Y0)) is Element of the carrier of X
||.(- ((X,(Y0 \/ Y1)) - (X,Y0))).|| is V36() real ext-real Element of REAL
(X,Y0) - (X,(Y0 \/ Y1)) is Element of the carrier of X
(X,Y0) + (- (X,(Y0 \/ Y1))) is Element of the carrier of X
the addF of X . ((X,Y0),(- (X,(Y0 \/ Y1)))) is Element of the carrier of X
||.((X,Y0) - (X,(Y0 \/ Y1))).|| is V36() real ext-real Element of REAL
(0. X) + ((X,Y0) - (X,(Y0 \/ Y1))) is Element of the carrier of X
the addF of X . ((0. X),((X,Y0) - (X,(Y0 \/ Y1)))) is Element of the carrier of X
||.((0. X) + ((X,Y0) - (X,(Y0 \/ Y1)))).|| is V36() real ext-real Element of REAL
x - x is Element of the carrier of X
- x is Element of the carrier of X
x + (- x) is Element of the carrier of X
the addF of X . (x,(- x)) is Element of the carrier of X
(x - x) + ((X,Y0) - (X,(Y0 \/ Y1))) is Element of the carrier of X
the addF of X . ((x - x),((X,Y0) - (X,(Y0 \/ Y1)))) is Element of the carrier of X
||.((x - x) + ((X,Y0) - (X,(Y0 \/ Y1)))).|| is V36() real ext-real Element of REAL
x - ((X,Y0) - (X,(Y0 \/ Y1))) is Element of the carrier of X
- ((X,Y0) - (X,(Y0 \/ Y1))) is Element of the carrier of X
x + (- ((X,Y0) - (X,(Y0 \/ Y1)))) is Element of the carrier of X
the addF of X . (x,(- ((X,Y0) - (X,(Y0 \/ Y1))))) is Element of the carrier of X
x - (x - ((X,Y0) - (X,(Y0 \/ Y1)))) is Element of the carrier of X
- (x - ((X,Y0) - (X,(Y0 \/ Y1)))) is Element of the carrier of X
x + (- (x - ((X,Y0) - (X,(Y0 \/ Y1))))) is Element of the carrier of X
the addF of X . (x,(- (x - ((X,Y0) - (X,(Y0 \/ Y1)))))) is Element of the carrier of X
||.(x - (x - ((X,Y0) - (X,(Y0 \/ Y1))))).|| is V36() real ext-real Element of REAL
(x - (X,Y0)) + (X,(Y0 \/ Y1)) is Element of the carrier of X
the addF of X . ((x - (X,Y0)),(X,(Y0 \/ Y1))) is Element of the carrier of X
x - ((x - (X,Y0)) + (X,(Y0 \/ Y1))) is Element of the carrier of X
- ((x - (X,Y0)) + (X,(Y0 \/ Y1))) is Element of the carrier of X
x + (- ((x - (X,Y0)) + (X,(Y0 \/ Y1)))) is Element of the carrier of X
the addF of X . (x,(- ((x - (X,Y0)) + (X,(Y0 \/ Y1))))) is Element of the carrier of X
||.(x - ((x - (X,Y0)) + (X,(Y0 \/ Y1)))).|| is V36() real ext-real Element of REAL
e is V36() real ext-real Element of REAL
x is V36() real ext-real Element of REAL
e is V36() real ext-real Element of REAL