:: BHSP_1 semantic presentation

REAL is non empty V38() V39() V40() V44() V55() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V38() V39() V40() V41() V42() V43() V44() Element of bool REAL
bool REAL is non empty set
COMPLEX is non empty V38() V44() V55() set
omega is non empty epsilon-transitive epsilon-connected ordinal V38() V39() V40() V41() V42() V43() V44() set
bool omega is non empty set
bool NAT is non empty set
is non empty set
bool is non empty set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V33() real ext-real positive non negative V38() V39() V40() V41() V42() V43() Element of NAT

- 1 is V33() real ext-real non positive Element of REAL
4 is non empty epsilon-transitive epsilon-connected ordinal natural V33() real ext-real positive non negative V38() V39() V40() V41() V42() V43() Element of NAT
the non empty set is non empty set
the Element of the non empty set is Element of the non empty set
[: the non empty set , the non empty set :] is non empty set
[:[: the non empty set , the non empty set :], the non empty set :] is non empty set
bool [:[: the non empty set , the non empty set :], the non empty set :] is non empty set
the Relation-like [: the non empty set , the non empty set :] -defined the non empty set -valued Function-like non empty total V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :] is Relation-like [: the non empty set , the non empty set :] -defined the non empty set -valued Function-like non empty total V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :]
[:REAL, the non empty set :] is non empty set
[:[:REAL, the non empty set :], the non empty set :] is non empty set
bool [:[:REAL, the non empty set :], the non empty set :] is non empty set
the Relation-like [:REAL, the non empty set :] -defined the non empty set -valued Function-like non empty total V18([:REAL, the non empty set :], the non empty set ) Element of bool [:[:REAL, the non empty set :], the non empty set :] is Relation-like [:REAL, the non empty set :] -defined the non empty set -valued Function-like non empty total V18([:REAL, the non empty set :], the non empty set ) Element of bool [:[:REAL, the non empty set :], the non empty set :]
[:[: the non empty set , the non empty set :],REAL:] is non empty set
bool [:[: the non empty set , the non empty set :],REAL:] is non empty set
the Relation-like [: the non empty set , the non empty set :] -defined REAL -valued Function-like non empty total V18([: the non empty set , the non empty set :], REAL ) Element of bool [:[: the non empty set , the non empty set :],REAL:] is Relation-like [: the non empty set , the non empty set :] -defined REAL -valued Function-like non empty total V18([: the non empty set , the non empty set :], REAL ) Element of bool [:[: the non empty set , the non empty set :],REAL:]
( the non empty set , the Element of the non empty set , the Relation-like [: the non empty set , the non empty set :] -defined the non empty set -valued Function-like non empty total V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the Relation-like [:REAL, the non empty set :] -defined the non empty set -valued Function-like non empty total V18([:REAL, the non empty set :], the non empty set ) Element of bool [:[:REAL, the non empty set :], the non empty set :], the Relation-like [: the non empty set , the non empty set :] -defined REAL -valued Function-like non empty total V18([: the non empty set , the non empty set :], REAL ) Element of bool [:[: the non empty set , the non empty set :],REAL:]) is () ()
the carrier of ( the non empty set , the Element of the non empty set , the Relation-like [: the non empty set , the non empty set :] -defined the non empty set -valued Function-like non empty total V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the Relation-like [:REAL, the non empty set :] -defined the non empty set -valued Function-like non empty total V18([:REAL, the non empty set :], the non empty set ) Element of bool [:[:REAL, the non empty set :], the non empty set :], the Relation-like [: the non empty set , the non empty set :] -defined REAL -valued Function-like non empty total V18([: the non empty set , the non empty set :], REAL ) Element of bool [:[: the non empty set , the non empty set :],REAL:]) is set
V0 is non empty set
[:V0,V0:] is non empty set
[:[:V0,V0:],V0:] is non empty set
bool [:[:V0,V0:],V0:] is non empty set
[:REAL,V0:] is non empty set
[:[:REAL,V0:],V0:] is non empty set
bool [:[:REAL,V0:],V0:] is non empty set
[:[:V0,V0:],REAL:] is non empty set
bool [:[:V0,V0:],REAL:] is non empty set
nilfunc is Element of V0
X0 is Relation-like [:V0,V0:] -defined V0 -valued Function-like non empty total V18([:V0,V0:],V0) Element of bool [:[:V0,V0:],V0:]
a is Relation-like [:REAL,V0:] -defined V0 -valued Function-like non empty total V18([:REAL,V0:],V0) Element of bool [:[:REAL,V0:],V0:]
X is Relation-like [:V0,V0:] -defined REAL -valued Function-like non empty total V18([:V0,V0:], REAL ) Element of bool [:[:V0,V0:],REAL:]
(V0,nilfunc,X0,a,X) is () ()
V0 is non empty ()
the carrier of V0 is non empty set
[: the carrier of V0, the carrier of V0:] is non empty set
the of V0 is Relation-like [: the carrier of V0, the carrier of V0:] -defined REAL -valued Function-like non empty total V18([: the carrier of V0, the carrier of V0:], REAL ) Element of bool [:[: the carrier of V0, the carrier of V0:],REAL:]
[:[: the carrier of V0, the carrier of V0:],REAL:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:],REAL:] is non empty set
nilfunc is Element of the carrier of V0
X0 is Element of the carrier of V0
[nilfunc,X0] is Element of [: the carrier of V0, the carrier of V0:]
the of V0 . [nilfunc,X0] is V33() real ext-real Element of REAL

the carrier of () is non empty set

[: the carrier of (), the carrier of ():] is non empty set
[:[: the carrier of (), the carrier of ():],REAL:] is non empty set
bool [:[: the carrier of (), the carrier of ():],REAL:] is non empty set
[: the carrier of (), the carrier of ():] --> 0 is Relation-like [: the carrier of (), the carrier of ():] -defined NAT -valued Function-like non empty total V18([: the carrier of (), the carrier of ():], NAT ) Element of bool [:[: the carrier of (), the carrier of ():],NAT:]
[:[: the carrier of (), the carrier of ():],NAT:] is non empty set
bool [:[: the carrier of (), the carrier of ():],NAT:] is non empty set
nilfunc is Relation-like [: the carrier of (), the carrier of ():] -defined REAL -valued Function-like non empty total V18([: the carrier of (), the carrier of ():], REAL ) Element of bool [:[: the carrier of (), the carrier of ():],REAL:]
X0 is right_complementable Element of the carrier of ()
a is right_complementable Element of the carrier of ()
[X0,a] is Element of [: the carrier of (), the carrier of ():]
nilfunc . [X0,a] is V33() real ext-real Element of REAL
[(),()] is Element of [::]
[::] is non empty set
nilfunc . [(),()] is set
X0 is right_complementable Element of the carrier of ()
a is right_complementable Element of the carrier of ()
[X0,a] is Element of [: the carrier of (), the carrier of ():]
nilfunc . [X0,a] is V33() real ext-real Element of REAL
[a,X0] is Element of [: the carrier of (), the carrier of ():]
nilfunc . [a,X0] is V33() real ext-real Element of REAL
X0 is right_complementable Element of the carrier of ()
a is right_complementable Element of the carrier of ()
X0 + a is right_complementable Element of the carrier of ()
the addF of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like non empty total V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the addF of () . (X0,a) is right_complementable Element of the carrier of ()
X is right_complementable Element of the carrier of ()
[(X0 + a),X] is Element of [: the carrier of (), the carrier of ():]
nilfunc . [(X0 + a),X] is V33() real ext-real Element of REAL
[X0,X] is Element of [: the carrier of (), the carrier of ():]
nilfunc . [X0,X] is V33() real ext-real Element of REAL
[a,X] is Element of [: the carrier of (), the carrier of ():]
nilfunc . [a,X] is V33() real ext-real Element of REAL
(nilfunc . [X0,X]) + (nilfunc . [a,X]) is V33() real ext-real Element of REAL
X0 is right_complementable Element of the carrier of ()
a is right_complementable Element of the carrier of ()
[X0,a] is Element of [: the carrier of (), the carrier of ():]
nilfunc . [X0,a] is V33() real ext-real Element of REAL
X is V33() real ext-real Element of REAL
X * X0 is right_complementable Element of the carrier of ()
the Mult of () is Relation-like [:REAL, the carrier of ():] -defined the carrier of () -valued Function-like non empty total V18([:REAL, the carrier of ():], the carrier of ()) Element of bool [:[:REAL, the carrier of ():], the carrier of ():]
[:REAL, the carrier of ():] is non empty set
[:[:REAL, the carrier of ():], the carrier of ():] is non empty set
bool [:[:REAL, the carrier of ():], the carrier of ():] is non empty set
the Mult of () . (X,X0) is set
[(X * X0),a] is Element of [: the carrier of (), the carrier of ():]
nilfunc . [(X * X0),a] is V33() real ext-real Element of REAL
X * (nilfunc . [X0,a]) is V33() real ext-real Element of REAL

the ZeroF of () is right_complementable Element of the carrier of ()
the addF of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like non empty total V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the Mult of () is Relation-like [:REAL, the carrier of ():] -defined the carrier of () -valued Function-like non empty total V18([:REAL, the carrier of ():], the carrier of ()) Element of bool [:[:REAL, the carrier of ():], the carrier of ():]
[:REAL, the carrier of ():] is non empty set
[:[:REAL, the carrier of ():], the carrier of ():] is non empty set
bool [:[:REAL, the carrier of ():], the carrier of ():] is non empty set
( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc) is non empty () ()
the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc) is non empty set
0. ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc) is V74(( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc)) Element of the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc)
the ZeroF of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc) is Element of the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc)
a is Element of the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc)
(( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc),a,a) is V33() real ext-real Element of REAL
[: the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc), the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc):] is non empty set
the of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc) is Relation-like [: the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc), the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc):] -defined REAL -valued Function-like non empty total V18([: the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc), the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc):], REAL ) Element of bool [:[: the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc), the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc):],REAL:]
[:[: the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc), the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc):],REAL:] is non empty set
bool [:[: the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc), the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc):],REAL:] is non empty set
[a,a] is Element of [: the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc), the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc):]
the of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc) . [a,a] is V33() real ext-real Element of REAL
X is Element of the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc)
(( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc),a,X) is V33() real ext-real Element of REAL
[a,X] is Element of [: the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc), the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc):]
the of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc) . [a,X] is V33() real ext-real Element of REAL
(( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc),X,a) is V33() real ext-real Element of REAL
[X,a] is Element of [: the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc), the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc):]
the of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc) . [X,a] is V33() real ext-real Element of REAL
a + X is Element of the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc)
[:[: the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc), the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc):], the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc):] is non empty set
bool [:[: the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc), the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc):], the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc):] is non empty set
the addF of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc) . (a,X) is Element of the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc)
seq1 is Element of the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc)
(( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc),(a + X),seq1) is V33() real ext-real Element of REAL
[(a + X),seq1] is Element of [: the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc), the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc):]
the of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc) . [(a + X),seq1] is V33() real ext-real Element of REAL
(( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc),a,seq1) is V33() real ext-real Element of REAL
[a,seq1] is Element of [: the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc), the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc):]
the of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc) . [a,seq1] is V33() real ext-real Element of REAL
(( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc),X,seq1) is V33() real ext-real Element of REAL
[X,seq1] is Element of [: the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc), the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc):]
the of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc) . [X,seq1] is V33() real ext-real Element of REAL
(( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc),a,seq1) + (( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc),X,seq1) is V33() real ext-real Element of REAL
n is right_complementable Element of the carrier of ()
z is right_complementable Element of the carrier of ()
n + z is right_complementable Element of the carrier of ()
the addF of () . (n,z) is right_complementable Element of the carrier of ()
n is right_complementable Element of the carrier of ()
[(n + z),n] is Element of [: the carrier of (), the carrier of ():]
nilfunc . [(n + z),n] is V33() real ext-real Element of REAL
seq2 is V33() real ext-real Element of REAL
seq2 * a is Element of the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc)
the Mult of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc) is Relation-like [:REAL, the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc):] -defined the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc) -valued Function-like non empty total V18([:REAL, the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc):], the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc)) Element of bool [:[:REAL, the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc):], the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc):]
[:REAL, the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc):] is non empty set
[:[:REAL, the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc):], the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc):] is non empty set
bool [:[:REAL, the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc):], the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc):] is non empty set
the Mult of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc) . (seq2,a) is set
(( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc),(seq2 * a),X) is V33() real ext-real Element of REAL
[(seq2 * a),X] is Element of [: the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc), the carrier of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc):]
the of ( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc) . [(seq2 * a),X] is V33() real ext-real Element of REAL
seq2 * (( the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc),a,X) is V33() real ext-real Element of REAL
n is right_complementable Element of the carrier of ()
seq2 * n is right_complementable Element of the carrier of ()
the Mult of () . (seq2,n) is set
z is right_complementable Element of the carrier of ()
[(seq2 * n),z] is Element of [: the carrier of (), the carrier of ():]
nilfunc . [(seq2 * n),z] is V33() real ext-real Element of REAL