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