:: C0SP2 semantic presentation

REAL is non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below Element of bool REAL
bool REAL is non empty set
omega is non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below set
bool omega is non empty set
bool NAT is non empty set
[:NAT,REAL:] is non empty V152() V153() V154() set
bool [:NAT,REAL:] is non empty set
the_set_of_RealSequences is non empty set
[:the_set_of_RealSequences,the_set_of_RealSequences:] is non empty set
[:[:the_set_of_RealSequences,the_set_of_RealSequences:],the_set_of_RealSequences:] is non empty set
bool [:[:the_set_of_RealSequences,the_set_of_RealSequences:],the_set_of_RealSequences:] is non empty set
[:REAL,the_set_of_RealSequences:] is non empty set
[:[:REAL,the_set_of_RealSequences:],the_set_of_RealSequences:] is non empty set
bool [:[:REAL,the_set_of_RealSequences:],the_set_of_RealSequences:] is non empty set
Linear_Space_of_RealSequences is RLSStruct
the carrier of Linear_Space_of_RealSequences is set
bool the carrier of Linear_Space_of_RealSequences is non empty set
the_set_of_l2RealSequences is Element of bool the carrier of Linear_Space_of_RealSequences
[:the_set_of_l2RealSequences,the_set_of_l2RealSequences:] is set
[:[:the_set_of_l2RealSequences,the_set_of_l2RealSequences:],REAL:] is V152() V153() V154() set
bool [:[:the_set_of_l2RealSequences,the_set_of_l2RealSequences:],REAL:] is non empty set
the_set_of_l1RealSequences is Element of bool the carrier of Linear_Space_of_RealSequences
[:the_set_of_l1RealSequences,REAL:] is V152() V153() V154() set
bool [:the_set_of_l1RealSequences,REAL:] is non empty set
COMPLEX is non empty V30() V185() V191() set
ExtREAL is non empty V186() V268() set
RAT is non empty V30() V185() V186() V187() V188() V191() set
INT is non empty V30() V185() V186() V187() V188() V189() V191() set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V117() V185() V186() V187() V188() V189() V190() V197() left_end bounded_below Element of NAT
K597() is V261() TopStruct
the carrier of K597() is V185() V186() V187() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V117() V185() V186() V187() V188() V189() V190() V197() left_end bounded_below Element of NAT
[:1,1:] is non empty RAT -valued INT -valued V152() V153() V154() V155() set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty RAT -valued INT -valued V152() V153() V154() V155() set
bool [:[:1,1:],1:] is non empty set
[:[:1,1:],REAL:] is non empty V152() V153() V154() set
bool [:[:1,1:],REAL:] is non empty set
[:REAL,REAL:] is non empty V152() V153() V154() set
[:[:REAL,REAL:],REAL:] is non empty V152() V153() V154() set
bool [:[:REAL,REAL:],REAL:] is non empty set
[:2,2:] is non empty RAT -valued INT -valued V152() V153() V154() V155() set
[:[:2,2:],REAL:] is non empty V152() V153() V154() set
bool [:[:2,2:],REAL:] is non empty set
K620() is V247() V261() L21()
R^1 is non empty strict TopSpace-like V261() TopStruct
[:COMPLEX,COMPLEX:] is non empty V152() set
bool [:COMPLEX,COMPLEX:] is non empty set
[:COMPLEX,REAL:] is non empty V152() V153() V154() set
bool [:COMPLEX,REAL:] is non empty set
bool [:REAL,REAL:] is non empty set
K689(2) is V281() L22()
the carrier of K689(2) is set
[: the carrier of K689(2),REAL:] is V152() V153() V154() set
bool [: the carrier of K689(2),REAL:] is non empty set
bool the carrier of K689(2) is non empty set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V185() V186() V187() V188() V189() V190() V191() bounded_below V268() set
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V117() V185() V186() V187() V188() V189() V190() V191() V197() bounded_below V268() Element of NAT
|.0.| is V11() real ext-real V197() Element of REAL
3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V117() V185() V186() V187() V188() V189() V190() V197() left_end bounded_below Element of NAT
- 1 is V11() real ext-real non positive Element of REAL
the carrier of R^1 is non empty V185() V186() V187() set
X is 1-sorted
the carrier of X is set
X is V11() real ext-real set
the carrier of X --> X is Relation-like the carrier of X -defined {X} -valued Function-like total quasi_total V152() V153() V154() Element of bool [: the carrier of X,{X}:]
{X} is non empty V185() V186() V187() set
[: the carrier of X,{X}:] is V152() V153() V154() set
bool [: the carrier of X,{X}:] is non empty set
[: the carrier of X,REAL:] is V152() V153() V154() set
bool [: the carrier of X,REAL:] is non empty set
X is TopSpace-like TopStruct
X is V11() real ext-real set
(X,X) is Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() Element of bool [: the carrier of X,REAL:]
the carrier of X is set
[: the carrier of X,REAL:] is V152() V153() V154() set
bool [: the carrier of X,REAL:] is non empty set
the carrier of X --> X is Relation-like the carrier of X -defined {X} -valued Function-like total quasi_total V152() V153() V154() Element of bool [: the carrier of X,{X}:]
{X} is non empty V185() V186() V187() set
[: the carrier of X,{X}:] is V152() V153() V154() set
bool [: the carrier of X,{X}:] is non empty set
[#] X is non proper closed Element of bool the carrier of X
bool the carrier of X is non empty set
FB is V185() V186() V187() Element of bool REAL
(X,X) " FB is Element of bool the carrier of X
{} X is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V185() V186() V187() V188() V189() V190() V191() closed bounded_below V268() compact Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
[: the carrier of X,REAL:] is non empty V152() V153() V154() set
bool [: the carrier of X,REAL:] is non empty set
bool the carrier of X is non empty set
X is non empty Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() Element of bool [: the carrier of X,REAL:]
F is Element of the carrier of X
X . F is V11() real ext-real Element of REAL
G is V185() V186() V187() Element of bool REAL
GB is V11() real ext-real set
(X . F) - GB is V11() real ext-real Element of REAL
- GB is V11() real ext-real set
(X . F) + (- GB) is V11() real ext-real set
(X . F) + GB is V11() real ext-real Element of REAL
].((X . F) - GB),((X . F) + GB).[ is open V185() V186() V187() non left_end non right_end V268() Element of bool REAL
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= (X . F) - GB & not (X . F) + GB <= b₁ ) } is set
X " ].((X . F) - GB),((X . F) + GB).[ is Element of bool the carrier of X
(X . F) - (X . F) is V11() real ext-real Element of REAL
- (X . F) is V11() real ext-real set
(X . F) + (- (X . F)) is V11() real ext-real set
abs ((X . F) - (X . F)) is V11() real ext-real Element of REAL
aF is Element of bool the carrier of X
X .: (X " ].((X . F) - GB),((X . F) + GB).[) is V185() V186() V187() Element of bool REAL
X .: aF is V185() V186() V187() Element of bool REAL
F is Element of the carrier of X
X . F is V11() real ext-real Element of REAL
G is V185() V186() V187() Element of bool REAL
F is V185() V186() V187() Element of bool REAL
F ` is V185() V186() V187() Element of bool REAL
(F `) ` is V185() V186() V187() Element of bool REAL
X " F is Element of bool the carrier of X
(X " F) ` is Element of bool the carrier of X
G is Element of the carrier of X
X " (F `) is Element of bool the carrier of X
X . G is V11() real ext-real Element of REAL
FB is V185() V186() V187() Element of bool REAL
GB is Element of bool the carrier of X
X .: GB is V185() V186() V187() Element of bool REAL
X " (X .: GB) is Element of bool the carrier of X
((X " F) `) ` is Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
[: the carrier of X,REAL:] is non empty V152() V153() V154() set
bool [: the carrier of X,REAL:] is non empty set
{ b₁ where b₁ is non empty Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() continuous Element of bool [: the carrier of X,REAL:] : verum } is set
RAlgebra the carrier of X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative AlgebraStr
Funcs ( the carrier of X,REAL) is non empty functional FUNCTION_DOMAIN of the carrier of X, REAL
RealFuncMult the carrier of X is non empty Relation-like [:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):] -defined Funcs ( the carrier of X,REAL) -valued Function-like total quasi_total Element of bool [:[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):]
[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):] is non empty set
[:[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):] is non empty set
bool [:[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):] is non empty set
RealFuncAdd the carrier of X is non empty Relation-like [:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):] -defined Funcs ( the carrier of X,REAL) -valued Function-like total quasi_total Element of bool [:[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):]
RealFuncExtMult the carrier of X is non empty Relation-like [:REAL,(Funcs ( the carrier of X,REAL)):] -defined Funcs ( the carrier of X,REAL) -valued Function-like total quasi_total Element of bool [:[:REAL,(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):]
[:REAL,(Funcs ( the carrier of X,REAL)):] is non empty set
[:[:REAL,(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):] is non empty set
bool [:[:REAL,(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):] is non empty set
RealFuncUnit the carrier of X is Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() Element of Funcs ( the carrier of X,REAL)
the carrier of X --> 1 is non empty Relation-like the carrier of X -defined NAT -valued RAT -valued INT -valued Function-like total quasi_total V152() V153() V154() V155() Element of bool [: the carrier of X,NAT:]
[: the carrier of X,NAT:] is non empty RAT -valued INT -valued V152() V153() V154() V155() set
bool [: the carrier of X,NAT:] is non empty set
RealFuncZero the carrier of X is Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() Element of Funcs ( the carrier of X,REAL)
the carrier of X --> 0 is non empty Relation-like the carrier of X -defined NAT -valued RAT -valued INT -valued Function-like total quasi_total V152() V153() V154() V155() Element of bool [: the carrier of X,NAT:]
AlgebraStr(# (Funcs ( the carrier of X,REAL)),(RealFuncMult the carrier of X),(RealFuncAdd the carrier of X),(RealFuncExtMult the carrier of X),(RealFuncUnit the carrier of X),(RealFuncZero the carrier of X) #) is strict AlgebraStr
the carrier of (RAlgebra the carrier of X) is non empty set
bool the carrier of (RAlgebra the carrier of X) is non empty set
F is set
G is non empty Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() continuous Element of bool [: the carrier of X,REAL:]
X is non empty TopSpace-like TopStruct
(X) is Element of bool the carrier of (RAlgebra the carrier of X)
the carrier of X is non empty set
RAlgebra the carrier of X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative AlgebraStr
Funcs ( the carrier of X,REAL) is non empty functional FUNCTION_DOMAIN of the carrier of X, REAL
RealFuncMult the carrier of X is non empty Relation-like [:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):] -defined Funcs ( the carrier of X,REAL) -valued Function-like total quasi_total Element of bool [:[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):]
[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):] is non empty set
[:[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):] is non empty set
bool [:[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):] is non empty set
RealFuncAdd the carrier of X is non empty Relation-like [:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):] -defined Funcs ( the carrier of X,REAL) -valued Function-like total quasi_total Element of bool [:[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):]
RealFuncExtMult the carrier of X is non empty Relation-like [:REAL,(Funcs ( the carrier of X,REAL)):] -defined Funcs ( the carrier of X,REAL) -valued Function-like total quasi_total Element of bool [:[:REAL,(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):]
[:REAL,(Funcs ( the carrier of X,REAL)):] is non empty set
[:[:REAL,(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):] is non empty set
bool [:[:REAL,(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):] is non empty set
RealFuncUnit the carrier of X is Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() Element of Funcs ( the carrier of X,REAL)
the carrier of X --> 1 is non empty Relation-like the carrier of X -defined NAT -valued RAT -valued INT -valued Function-like total quasi_total V152() V153() V154() V155() Element of bool [: the carrier of X,NAT:]
[: the carrier of X,NAT:] is non empty RAT -valued INT -valued V152() V153() V154() V155() set
bool [: the carrier of X,NAT:] is non empty set
RealFuncZero the carrier of X is Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() Element of Funcs ( the carrier of X,REAL)
the carrier of X --> 0 is non empty Relation-like the carrier of X -defined NAT -valued RAT -valued INT -valued Function-like total quasi_total V152() V153() V154() V155() Element of bool [: the carrier of X,NAT:]
AlgebraStr(# (Funcs ( the carrier of X,REAL)),(RealFuncMult the carrier of X),(RealFuncAdd the carrier of X),(RealFuncExtMult the carrier of X),(RealFuncUnit the carrier of X),(RealFuncZero the carrier of X) #) is strict AlgebraStr
the carrier of (RAlgebra the carrier of X) is non empty set
bool the carrier of (RAlgebra the carrier of X) is non empty set
[: the carrier of X,REAL:] is non empty V152() V153() V154() set
bool [: the carrier of X,REAL:] is non empty set
{ b₁ where b₁ is non empty Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() continuous Element of bool [: the carrier of X,REAL:] : verum } is set
(X,0) is non empty Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() continuous Element of bool [: the carrier of X,REAL:]
the carrier of X --> 0 is non empty Relation-like the carrier of X -defined RAT -valued INT -valued {0} -valued Function-like total quasi_total V152() V153() V154() V155() Element of bool [: the carrier of X,{0}:]
{0} is non empty V185() V186() V187() V188() V189() V190() left_end bounded_below set
[: the carrier of X,{0}:] is non empty RAT -valued INT -valued V152() V153() V154() V155() set
bool [: the carrier of X,{0}:] is non empty set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
RAlgebra the carrier of X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative AlgebraStr
Funcs ( the carrier of X,REAL) is non empty functional FUNCTION_DOMAIN of the carrier of X, REAL
RealFuncMult the carrier of X is non empty Relation-like [:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):] -defined Funcs ( the carrier of X,REAL) -valued Function-like total quasi_total Element of bool [:[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):]
[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):] is non empty set
[:[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):] is non empty set
bool [:[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):] is non empty set
RealFuncAdd the carrier of X is non empty Relation-like [:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):] -defined Funcs ( the carrier of X,REAL) -valued Function-like total quasi_total Element of bool [:[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):]
RealFuncExtMult the carrier of X is non empty Relation-like [:REAL,(Funcs ( the carrier of X,REAL)):] -defined Funcs ( the carrier of X,REAL) -valued Function-like total quasi_total Element of bool [:[:REAL,(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):]
[:REAL,(Funcs ( the carrier of X,REAL)):] is non empty set
[:[:REAL,(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):] is non empty set
bool [:[:REAL,(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):] is non empty set
RealFuncUnit the carrier of X is Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() Element of Funcs ( the carrier of X,REAL)
the carrier of X --> 1 is non empty Relation-like the carrier of X -defined NAT -valued RAT -valued INT -valued Function-like total quasi_total V152() V153() V154() V155() Element of bool [: the carrier of X,NAT:]
[: the carrier of X,NAT:] is non empty RAT -valued INT -valued V152() V153() V154() V155() set
bool [: the carrier of X,NAT:] is non empty set
RealFuncZero the carrier of X is Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() Element of Funcs ( the carrier of X,REAL)
the carrier of X --> 0 is non empty Relation-like the carrier of X -defined NAT -valued RAT -valued INT -valued Function-like total quasi_total V152() V153() V154() V155() Element of bool [: the carrier of X,NAT:]
AlgebraStr(# (Funcs ( the carrier of X,REAL)),(RealFuncMult the carrier of X),(RealFuncAdd the carrier of X),(RealFuncExtMult the carrier of X),(RealFuncUnit the carrier of X),(RealFuncZero the carrier of X) #) is strict AlgebraStr
(X) is non empty Element of bool the carrier of (RAlgebra the carrier of X)
the carrier of (RAlgebra the carrier of X) is non empty set
bool the carrier of (RAlgebra the carrier of X) is non empty set
[: the carrier of X,REAL:] is non empty V152() V153() V154() set
bool [: the carrier of X,REAL:] is non empty set
{ b₁ where b₁ is non empty Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() continuous Element of bool [: the carrier of X,REAL:] : verum } is set
G is right_complementable Element of the carrier of (RAlgebra the carrier of X)
FB is right_complementable Element of the carrier of (RAlgebra the carrier of X)
G + FB is right_complementable Element of the carrier of (RAlgebra the carrier of X)
the addF of (RAlgebra the carrier of X) is non empty Relation-like [: the carrier of (RAlgebra the carrier of X), the carrier of (RAlgebra the carrier of X):] -defined the carrier of (RAlgebra the carrier of X) -valued Function-like total quasi_total Element of bool [:[: the carrier of (RAlgebra the carrier of X), the carrier of (RAlgebra the carrier of X):], the carrier of (RAlgebra the carrier of X):]
[: the carrier of (RAlgebra the carrier of X), the carrier of (RAlgebra the carrier of X):] is non empty set
[:[: the carrier of (RAlgebra the carrier of X), the carrier of (RAlgebra the carrier of X):], the carrier of (RAlgebra the carrier of X):] is non empty set
bool [:[: the carrier of (RAlgebra the carrier of X), the carrier of (RAlgebra the carrier of X):], the carrier of (RAlgebra the carrier of X):] is non empty set
the addF of (RAlgebra the carrier of X) . (G,FB) is right_complementable Element of the carrier of (RAlgebra the carrier of X)
[G,FB] is set
{G,FB} is non empty set
{G} is non empty set
{{G,FB},{G}} is non empty set
the addF of (RAlgebra the carrier of X) . [G,FB] is set
GB is non empty Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() continuous Element of bool [: the carrier of X,REAL:]
aFB is non empty Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() continuous Element of bool [: the carrier of X,REAL:]
GB + aFB is non empty Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() Element of bool [: the carrier of X,REAL:]
aF is Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() Element of Funcs ( the carrier of X,REAL)
dom GB is Element of bool the carrier of X
bool the carrier of X is non empty set
dom aFB is Element of bool the carrier of X
(dom GB) /\ (dom aFB) is Element of bool the carrier of X
the carrier of X /\ (dom aFB) is Element of bool the carrier of X
the carrier of X /\ the carrier of X is set
dom aF is Element of bool the carrier of X
aG is set
aF . aG is V11() real ext-real set
GB . aG is V11() real ext-real set
aFB . aG is V11() real ext-real set
(GB . aG) + (aFB . aG) is V11() real ext-real set
aG is Relation-like Function-like set
dom aG is set
rng aG is set
G is right_complementable Element of the carrier of (RAlgebra the carrier of X)
- G is right_complementable Element of the carrier of (RAlgebra the carrier of X)
FB is non empty Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() continuous Element of bool [: the carrier of X,REAL:]
- FB is non empty Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() Element of bool [: the carrier of X,REAL:]
GB is Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() Element of Funcs ( the carrier of X,REAL)
(- 1) * G is right_complementable Element of the carrier of (RAlgebra the carrier of X)
the Mult of (RAlgebra the carrier of X) is non empty Relation-like [:REAL, the carrier of (RAlgebra the carrier of X):] -defined the carrier of (RAlgebra the carrier of X) -valued Function-like total quasi_total Element of bool [:[:REAL, the carrier of (RAlgebra the carrier of X):], the carrier of (RAlgebra the carrier of X):]
[:REAL, the carrier of (RAlgebra the carrier of X):] is non empty set
[:[:REAL, the carrier of (RAlgebra the carrier of X):], the carrier of (RAlgebra the carrier of X):] is non empty set
bool [:[:REAL, the carrier of (RAlgebra the carrier of X):], the carrier of (RAlgebra the carrier of X):] is non empty set
the Mult of (RAlgebra the carrier of X) . ((- 1),G) is set
[(- 1),G] is set
{(- 1),G} is non empty set
{(- 1)} is non empty V185() V186() V187() set
{{(- 1),G},{(- 1)}} is non empty set
the Mult of (RAlgebra the carrier of X) . [(- 1),G] is set
dom FB is Element of bool the carrier of X
bool the carrier of X is non empty set
aF is set
dom GB is Element of bool the carrier of X
GB . aF is V11() real ext-real set
aFB is Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() Element of Funcs ( the carrier of X,REAL)
aG is Element of the carrier of X
aFB . aG is V11() real ext-real Element of REAL
(- 1) * (aFB . aG) is V11() real ext-real Element of REAL
FB . aF is V11() real ext-real set
- (FB . aF) is V11() real ext-real set
aF is Relation-like Function-like set
dom aF is set
rng aF is set
G is V11() real ext-real Element of REAL
FB is right_complementable Element of the carrier of (RAlgebra the carrier of X)
G * FB is right_complementable Element of the carrier of (RAlgebra the carrier of X)
the Mult of (RAlgebra the carrier of X) is non empty Relation-like [:REAL, the carrier of (RAlgebra the carrier of X):] -defined the carrier of (RAlgebra the carrier of X) -valued Function-like total quasi_total Element of bool [:[:REAL, the carrier of (RAlgebra the carrier of X):], the carrier of (RAlgebra the carrier of X):]
[:REAL, the carrier of (RAlgebra the carrier of X):] is non empty set
[:[:REAL, the carrier of (RAlgebra the carrier of X):], the carrier of (RAlgebra the carrier of X):] is non empty set
bool [:[:REAL, the carrier of (RAlgebra the carrier of X):], the carrier of (RAlgebra the carrier of X):] is non empty set
the Mult of (RAlgebra the carrier of X) . (G,FB) is set
[G,FB] is set
{G,FB} is non empty set
{G} is non empty V185() V186() V187() set
{{G,FB},{G}} is non empty set
the Mult of (RAlgebra the carrier of X) . [G,FB] is set
GB is non empty Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() continuous Element of bool [: the carrier of X,REAL:]
G (#) GB is non empty Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() Element of bool [: the carrier of X,REAL:]
[: the carrier of X, the carrier of R^1:] is non empty V152() V153() V154() set
bool [: the carrier of X, the carrier of R^1:] is non empty set
aFB is non empty Relation-like the carrier of X -defined the carrier of R^1 -valued Function-like total quasi_total V152() V153() V154() continuous Element of bool [: the carrier of X, the carrier of R^1:]
aG is non empty Relation-like the carrier of X -defined the carrier of R^1 -valued Function-like total quasi_total V152() V153() V154() Element of bool [: the carrier of X, the carrier of R^1:]
r is non empty Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() Element of bool [: the carrier of X,REAL:]
dom r is Element of bool the carrier of X
bool the carrier of X is non empty set
dom GB is Element of bool the carrier of X
s1 is set
r . s1 is V11() real ext-real set
GB . s1 is V11() real ext-real set
G * (GB . s1) is V11() real ext-real Element of REAL
aFB is Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() Element of Funcs ( the carrier of X,REAL)
dom GB is Element of bool the carrier of X
bool the carrier of X is non empty set
dom aFB is Element of bool the carrier of X
aF is set
aFB . aF is V11() real ext-real set
GB . aF is V11() real ext-real set
G * (GB . aF) is V11() real ext-real Element of REAL
aF is Relation-like Function-like set
dom aF is set
rng aF is set
G is right_complementable Element of the carrier of (RAlgebra the carrier of X)
FB is right_complementable Element of the carrier of (RAlgebra the carrier of X)
G * FB is right_complementable Element of the carrier of (RAlgebra the carrier of X)
the multF of (RAlgebra the carrier of X) is non empty Relation-like [: the carrier of (RAlgebra the carrier of X), the carrier of (RAlgebra the carrier of X):] -defined the carrier of (RAlgebra the carrier of X) -valued Function-like total quasi_total Element of bool [:[: the carrier of (RAlgebra the carrier of X), the carrier of (RAlgebra the carrier of X):], the carrier of (RAlgebra the carrier of X):]
[: the carrier of (RAlgebra the carrier of X), the carrier of (RAlgebra the carrier of X):] is non empty set
[:[: the carrier of (RAlgebra the carrier of X), the carrier of (RAlgebra the carrier of X):], the carrier of (RAlgebra the carrier of X):] is non empty set
bool [:[: the carrier of (RAlgebra the carrier of X), the carrier of (RAlgebra the carrier of X):], the carrier of (RAlgebra the carrier of X):] is non empty set
the multF of (RAlgebra the carrier of X) . (G,FB) is right_complementable Element of the carrier of (RAlgebra the carrier of X)
[G,FB] is set
{G,FB} is non empty set
{G} is non empty set
{{G,FB},{G}} is non empty set
the multF of (RAlgebra the carrier of X) . [G,FB] is set
GB is non empty Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() continuous Element of bool [: the carrier of X,REAL:]
aFB is non empty Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() continuous Element of bool [: the carrier of X,REAL:]
GB (#) aFB is non empty Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() Element of bool [: the carrier of X,REAL:]
[: the carrier of X, the carrier of R^1:] is non empty V152() V153() V154() set
bool [: the carrier of X, the carrier of R^1:] is non empty set
aF is non empty Relation-like the carrier of X -defined the carrier of R^1 -valued Function-like total quasi_total V152() V153() V154() continuous Element of bool [: the carrier of X, the carrier of R^1:]
aG is non empty Relation-like the carrier of X -defined the carrier of R^1 -valued Function-like total quasi_total V152() V153() V154() continuous Element of bool [: the carrier of X, the carrier of R^1:]
r is non empty Relation-like the carrier of X -defined the carrier of R^1 -valued Function-like total quasi_total V152() V153() V154() Element of bool [: the carrier of X, the carrier of R^1:]
s1 is non empty Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() Element of bool [: the carrier of X,REAL:]
dom s1 is Element of bool the carrier of X
bool the carrier of X is non empty set
the carrier of X /\ the carrier of X is set
dom aFB is Element of bool the carrier of X
the carrier of X /\ (dom aFB) is Element of bool the carrier of X
dom GB is Element of bool the carrier of X
(dom GB) /\ (dom aFB) is Element of bool the carrier of X
uu1 is set
s1 . uu1 is V11() real ext-real set
GB . uu1 is V11() real ext-real set
aFB . uu1 is V11() real ext-real set
(GB . uu1) * (aFB . uu1) is V11() real ext-real set
aF is Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() Element of Funcs ( the carrier of X,REAL)
dom GB is Element of bool the carrier of X
bool the carrier of X is non empty set
dom aFB is Element of bool the carrier of X
(dom GB) /\ (dom aFB) is Element of bool the carrier of X
the carrier of X /\ (dom aFB) is Element of bool the carrier of X
the carrier of X /\ the carrier of X is set
dom aF is Element of bool the carrier of X
aG is set
aF . aG is V11() real ext-real set
GB . aG is V11() real ext-real set
aFB . aG is V11() real ext-real set
(GB . aG) * (aFB . aG) is V11() real ext-real set
aG is Relation-like Function-like set
dom aG is set
rng aG is set
G is non empty Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() Element of bool [: the carrier of X,REAL:]
(X,1) is non empty Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() continuous Element of bool [: the carrier of X,REAL:]
the carrier of X --> 1 is non empty Relation-like the carrier of X -defined RAT -valued INT -valued {1} -valued Function-like total quasi_total V152() V153() V154() V155() Element of bool [: the carrier of X,{1}:]
{1} is non empty V185() V186() V187() V188() V189() V190() left_end bounded_below set
[: the carrier of X,{1}:] is non empty RAT -valued INT -valued V152() V153() V154() V155() set
bool [: the carrier of X,{1}:] is non empty set
1. (RAlgebra the carrier of X) is right_complementable Element of the carrier of (RAlgebra the carrier of X)
the OneF of (RAlgebra the carrier of X) is right_complementable Element of the carrier of (RAlgebra the carrier of X)
X is non empty TopSpace-like TopStruct
(X) is non empty add-closed having-inverse additively-closed multiplicatively-closed additively-linearly-closed Element of bool the carrier of (RAlgebra the carrier of X)
the carrier of X is non empty set
RAlgebra the carrier of X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative AlgebraStr
Funcs ( the carrier of X,REAL) is non empty functional FUNCTION_DOMAIN of the carrier of X, REAL
RealFuncMult the carrier of X is non empty Relation-like [:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):] -defined Funcs ( the carrier of X,REAL) -valued Function-like total quasi_total Element of bool [:[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):]
[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):] is non empty set
[:[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):] is non empty set
bool [:[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):] is non empty set
RealFuncAdd the carrier of X is non empty Relation-like [:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):] -defined Funcs ( the carrier of X,REAL) -valued Function-like total quasi_total Element of bool [:[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):]
RealFuncExtMult the carrier of X is non empty Relation-like [:REAL,(Funcs ( the carrier of X,REAL)):] -defined Funcs ( the carrier of X,REAL) -valued Function-like total quasi_total Element of bool [:[:REAL,(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):]
[:REAL,(Funcs ( the carrier of X,REAL)):] is non empty set
[:[:REAL,(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):] is non empty set
bool [:[:REAL,(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):] is non empty set
RealFuncUnit the carrier of X is Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() Element of Funcs ( the carrier of X,REAL)
the carrier of X --> 1 is non empty Relation-like the carrier of X -defined NAT -valued RAT -valued INT -valued Function-like total quasi_total V152() V153() V154() V155() Element of bool [: the carrier of X,NAT:]
[: the carrier of X,NAT:] is non empty RAT -valued INT -valued V152() V153() V154() V155() set
bool [: the carrier of X,NAT:] is non empty set
RealFuncZero the carrier of X is Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() Element of Funcs ( the carrier of X,REAL)
the carrier of X --> 0 is non empty Relation-like the carrier of X -defined NAT -valued RAT -valued INT -valued Function-like total quasi_total V152() V153() V154() V155() Element of bool [: the carrier of X,NAT:]
AlgebraStr(# (Funcs ( the carrier of X,REAL)),(RealFuncMult the carrier of X),(RealFuncAdd the carrier of X),(RealFuncExtMult the carrier of X),(RealFuncUnit the carrier of X),(RealFuncZero the carrier of X) #) is strict AlgebraStr
the carrier of (RAlgebra the carrier of X) is non empty set
bool the carrier of (RAlgebra the carrier of X) is non empty set
[: the carrier of X,REAL:] is non empty V152() V153() V154() set
bool [: the carrier of X,REAL:] is non empty set
{ b₁ where b₁ is non empty Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() continuous Element of bool [: the carrier of X,REAL:] : verum } is set
mult_ ((X),(RAlgebra the carrier of X)) is non empty Relation-like [:(X),(X):] -defined (X) -valued Function-like total quasi_total Element of bool [:[:(X),(X):],(X):]
[:(X),(X):] is non empty set
[:[:(X),(X):],(X):] is non empty set
bool [:[:(X),(X):],(X):] is non empty set
Add_ ((X),(RAlgebra the carrier of X)) is non empty Relation-like [:(X),(X):] -defined (X) -valued Function-like total quasi_total Element of bool [:[:(X),(X):],(X):]
Mult_ ((X),(RAlgebra the carrier of X)) is non empty Relation-like [:REAL,(X):] -defined (X) -valued Function-like total quasi_total Element of bool [:[:REAL,(X):],(X):]
[:REAL,(X):] is non empty set
[:[:REAL,(X):],(X):] is non empty set
bool [:[:REAL,(X):],(X):] is non empty set
One_ ((X),(RAlgebra the carrier of X)) is Element of (X)
Zero_ ((X),(RAlgebra the carrier of X)) is Element of (X)
AlgebraStr(# (X),(mult_ ((X),(RAlgebra the carrier of X))),(Add_ ((X),(RAlgebra the carrier of X))),(Mult_ ((X),(RAlgebra the carrier of X))),(One_ ((X),(RAlgebra the carrier of X))),(Zero_ ((X),(RAlgebra the carrier of X))) #) is strict AlgebraStr
X is non empty TopSpace-like TopStruct
(X) is AlgebraStr
(X) is non empty add-closed having-inverse additively-closed multiplicatively-closed additively-linearly-closed Element of bool the carrier of (RAlgebra the carrier of X)
the carrier of X is non empty set
RAlgebra the carrier of X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative AlgebraStr
Funcs ( the carrier of X,REAL) is non empty functional FUNCTION_DOMAIN of the carrier of X, REAL
RealFuncMult the carrier of X is non empty Relation-like [:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):] -defined Funcs ( the carrier of X,REAL) -valued Function-like total quasi_total Element of bool [:[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):]
[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):] is non empty set
[:[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):] is non empty set
bool [:[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):] is non empty set
RealFuncAdd the carrier of X is non empty Relation-like [:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):] -defined Funcs ( the carrier of X,REAL) -valued Function-like total quasi_total Element of bool [:[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):]
RealFuncExtMult the carrier of X is non empty Relation-like [:REAL,(Funcs ( the carrier of X,REAL)):] -defined Funcs ( the carrier of X,REAL) -valued Function-like total quasi_total Element of bool [:[:REAL,(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):]
[:REAL,(Funcs ( the carrier of X,REAL)):] is non empty set
[:[:REAL,(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):] is non empty set
bool [:[:REAL,(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):] is non empty set
RealFuncUnit the carrier of X is Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() Element of Funcs ( the carrier of X,REAL)
the carrier of X --> 1 is non empty Relation-like the carrier of X -defined NAT -valued RAT -valued INT -valued Function-like total quasi_total V152() V153() V154() V155() Element of bool [: the carrier of X,NAT:]
[: the carrier of X,NAT:] is non empty RAT -valued INT -valued V152() V153() V154() V155() set
bool [: the carrier of X,NAT:] is non empty set
RealFuncZero the carrier of X is Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() Element of Funcs ( the carrier of X,REAL)
the carrier of X --> 0 is non empty Relation-like the carrier of X -defined NAT -valued RAT -valued INT -valued Function-like total quasi_total V152() V153() V154() V155() Element of bool [: the carrier of X,NAT:]
AlgebraStr(# (Funcs ( the carrier of X,REAL)),(RealFuncMult the carrier of X),(RealFuncAdd the carrier of X),(RealFuncExtMult the carrier of X),(RealFuncUnit the carrier of X),(RealFuncZero the carrier of X) #) is strict AlgebraStr
the carrier of (RAlgebra the carrier of X) is non empty set
bool the carrier of (RAlgebra the carrier of X) is non empty set
[: the carrier of X,REAL:] is non empty V152() V153() V154() set
bool [: the carrier of X,REAL:] is non empty set
{ b₁ where b₁ is non empty Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() continuous Element of bool [: the carrier of X,REAL:] : verum } is set
mult_ ((X),(RAlgebra the carrier of X)) is non empty Relation-like [:(X),(X):] -defined (X) -valued Function-like total quasi_total Element of bool [:[:(X),(X):],(X):]
[:(X),(X):] is non empty set
[:[:(X),(X):],(X):] is non empty set
bool [:[:(X),(X):],(X):] is non empty set
Add_ ((X),(RAlgebra the carrier of X)) is non empty Relation-like [:(X),(X):] -defined (X) -valued Function-like total quasi_total Element of bool [:[:(X),(X):],(X):]
Mult_ ((X),(RAlgebra the carrier of X)) is non empty Relation-like [:REAL,(X):] -defined (X) -valued Function-like total quasi_total Element of bool [:[:REAL,(X):],(X):]
[:REAL,(X):] is non empty set
[:[:REAL,(X):],(X):] is non empty set
bool [:[:REAL,(X):],(X):] is non empty set
One_ ((X),(RAlgebra the carrier of X)) is Element of (X)
Zero_ ((X),(RAlgebra the carrier of X)) is Element of (X)
AlgebraStr(# (X),(mult_ ((X),(RAlgebra the carrier of X))),(Add_ ((X),(RAlgebra the carrier of X))),(Mult_ ((X),(RAlgebra the carrier of X))),(One_ ((X),(RAlgebra the carrier of X))),(Zero_ ((X),(RAlgebra the carrier of X))) #) is strict AlgebraStr
X is non empty TopSpace-like TopStruct
(X) is AlgebraStr
(X) is non empty add-closed having-inverse additively-closed multiplicatively-closed additively-linearly-closed Element of bool the carrier of (RAlgebra the carrier of X)
the carrier of X is non empty set
RAlgebra the carrier of X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative AlgebraStr
Funcs ( the carrier of X,REAL) is non empty functional FUNCTION_DOMAIN of the carrier of X, REAL
RealFuncMult the carrier of X is non empty Relation-like [:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):] -defined Funcs ( the carrier of X,REAL) -valued Function-like total quasi_total Element of bool [:[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):]
[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):] is non empty set
[:[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):] is non empty set
bool [:[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):] is non empty set
RealFuncAdd the carrier of X is non empty Relation-like [:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):] -defined Funcs ( the carrier of X,REAL) -valued Function-like total quasi_total Element of bool [:[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):]
RealFuncExtMult the carrier of X is non empty Relation-like [:REAL,(Funcs ( the carrier of X,REAL)):] -defined Funcs ( the carrier of X,REAL) -valued Function-like total quasi_total Element of bool [:[:REAL,(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):]
[:REAL,(Funcs ( the carrier of X,REAL)):] is non empty set
[:[:REAL,(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):] is non empty set
bool [:[:REAL,(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):] is non empty set
RealFuncUnit the carrier of X is Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() Element of Funcs ( the carrier of X,REAL)
the carrier of X --> 1 is non empty Relation-like the carrier of X -defined NAT -valued RAT -valued INT -valued Function-like total quasi_total V152() V153() V154() V155() Element of bool [: the carrier of X,NAT:]
[: the carrier of X,NAT:] is non empty RAT -valued INT -valued V152() V153() V154() V155() set
bool [: the carrier of X,NAT:] is non empty set
RealFuncZero the carrier of X is Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() Element of Funcs ( the carrier of X,REAL)
the carrier of X --> 0 is non empty Relation-like the carrier of X -defined NAT -valued RAT -valued INT -valued Function-like total quasi_total V152() V153() V154() V155() Element of bool [: the carrier of X,NAT:]
AlgebraStr(# (Funcs ( the carrier of X,REAL)),(RealFuncMult the carrier of X),(RealFuncAdd the carrier of X),(RealFuncExtMult the carrier of X),(RealFuncUnit the carrier of X),(RealFuncZero the carrier of X) #) is strict AlgebraStr
the carrier of (RAlgebra the carrier of X) is non empty set
bool the carrier of (RAlgebra the carrier of X) is non empty set
[: the carrier of X,REAL:] is non empty V152() V153() V154() set
bool [: the carrier of X,REAL:] is non empty set
{ b₁ where b₁ is non empty Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() continuous Element of bool [: the carrier of X,REAL:] : verum } is set
mult_ ((X),(RAlgebra the carrier of X)) is non empty Relation-like [:(X),(X):] -defined (X) -valued Function-like total quasi_total Element of bool [:[:(X),(X):],(X):]
[:(X),(X):] is non empty set
[:[:(X),(X):],(X):] is non empty set
bool [:[:(X),(X):],(X):] is non empty set
Add_ ((X),(RAlgebra the carrier of X)) is non empty Relation-like [:(X),(X):] -defined (X) -valued Function-like total quasi_total Element of bool [:[:(X),(X):],(X):]
Mult_ ((X),(RAlgebra the carrier of X)) is non empty Relation-like [:REAL,(X):] -defined (X) -valued Function-like total quasi_total Element of bool [:[:REAL,(X):],(X):]
[:REAL,(X):] is non empty set
[:[:REAL,(X):],(X):] is non empty set
bool [:[:REAL,(X):],(X):] is non empty set
One_ ((X),(RAlgebra the carrier of X)) is Element of (X)
Zero_ ((X),(RAlgebra the carrier of X)) is Element of (X)
AlgebraStr(# (X),(mult_ ((X),(RAlgebra the carrier of X))),(Add_ ((X),(RAlgebra the carrier of X))),(Mult_ ((X),(RAlgebra the carrier of X))),(One_ ((X),(RAlgebra the carrier of X))),(Zero_ ((X),(RAlgebra the carrier of X))) #) is strict AlgebraStr
X is non empty TopSpace-like TopStruct
(X) is non empty strict AlgebraStr
(X) is non empty add-closed having-inverse additively-closed multiplicatively-closed additively-linearly-closed Element of bool the carrier of (RAlgebra the carrier of X)
the carrier of X is non empty set
RAlgebra the carrier of X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative AlgebraStr
Funcs ( the carrier of X,REAL) is non empty functional FUNCTION_DOMAIN of the carrier of X, REAL
RealFuncMult the carrier of X is non empty Relation-like [:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):] -defined Funcs ( the carrier of X,REAL) -valued Function-like total quasi_total Element of bool [:[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):]
[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):] is non empty set
[:[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):] is non empty set
bool [:[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):] is non empty set
RealFuncAdd the carrier of X is non empty Relation-like [:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):] -defined Funcs ( the carrier of X,REAL) -valued Function-like total quasi_total Element of bool [:[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):]
RealFuncExtMult the carrier of X is non empty Relation-like [:REAL,(Funcs ( the carrier of X,REAL)):] -defined Funcs ( the carrier of X,REAL) -valued Function-like total quasi_total Element of bool [:[:REAL,(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):]
[:REAL,(Funcs ( the carrier of X,REAL)):] is non empty set
[:[:REAL,(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):] is non empty set
bool [:[:REAL,(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):] is non empty set
RealFuncUnit the carrier of X is Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() Element of Funcs ( the carrier of X,REAL)
the carrier of X --> 1 is non empty Relation-like the carrier of X -defined NAT -valued RAT -valued INT -valued Function-like total quasi_total V152() V153() V154() V155() Element of bool [: the carrier of X,NAT:]
[: the carrier of X,NAT:] is non empty RAT -valued INT -valued V152() V153() V154() V155() set
bool [: the carrier of X,NAT:] is non empty set
RealFuncZero the carrier of X is Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() Element of Funcs ( the carrier of X,REAL)
the carrier of X --> 0 is non empty Relation-like the carrier of X -defined NAT -valued RAT -valued INT -valued Function-like total quasi_total V152() V153() V154() V155() Element of bool [: the carrier of X,NAT:]
AlgebraStr(# (Funcs ( the carrier of X,REAL)),(RealFuncMult the carrier of X),(RealFuncAdd the carrier of X),(RealFuncExtMult the carrier of X),(RealFuncUnit the carrier of X),(RealFuncZero the carrier of X) #) is strict AlgebraStr
the carrier of (RAlgebra the carrier of X) is non empty set
bool the carrier of (RAlgebra the carrier of X) is non empty set
[: the carrier of X,REAL:] is non empty V152() V153() V154() set
bool [: the carrier of X,REAL:] is non empty set
{ b₁ where b₁ is non empty Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() continuous Element of bool [: the carrier of X,REAL:] : verum } is set
mult_ ((X),(RAlgebra the carrier of X)) is non empty Relation-like [:(X),(X):] -defined (X) -valued Function-like total quasi_total Element of bool [:[:(X),(X):],(X):]
[:(X),(X):] is non empty set
[:[:(X),(X):],(X):] is non empty set
bool [:[:(X),(X):],(X):] is non empty set
Add_ ((X),(RAlgebra the carrier of X)) is non empty Relation-like [:(X),(X):] -defined (X) -valued Function-like total quasi_total Element of bool [:[:(X),(X):],(X):]
Mult_ ((X),(RAlgebra the carrier of X)) is non empty Relation-like [:REAL,(X):] -defined (X) -valued Function-like total quasi_total Element of bool [:[:REAL,(X):],(X):]
[:REAL,(X):] is non empty set
[:[:REAL,(X):],(X):] is non empty set
bool [:[:REAL,(X):],(X):] is non empty set
One_ ((X),(RAlgebra the carrier of X)) is Element of (X)
Zero_ ((X),(RAlgebra the carrier of X)) is Element of (X)
AlgebraStr(# (X),(mult_ ((X),(RAlgebra the carrier of X))),(Add_ ((X),(RAlgebra the carrier of X))),(Mult_ ((X),(RAlgebra the carrier of X))),(One_ ((X),(RAlgebra the carrier of X))),(Zero_ ((X),(RAlgebra the carrier of X))) #) is strict AlgebraStr
the carrier of (X) is non empty set
X is Element of the carrier of (X)
1 * X is Element of the carrier of (X)
the Mult of (X) is non empty Relation-like [:REAL, the carrier of (X):] -defined the carrier of (X) -valued Function-like total quasi_total Element of bool [:[:REAL, the carrier of (X):], the carrier of (X):]
[:REAL, the carrier of (X):] is non empty set
[:[:REAL, the carrier of (X):], the carrier of (X):] is non empty set
bool [:[:REAL, the carrier of (X):], the carrier of (X):] is non empty set
the Mult of (X) . (1,X) is set
[1,X] is set
{1,X} is non empty set
{1} is non empty V185() V186() V187() V188() V189() V190() left_end bounded_below set
{{1,X},{1}} is non empty set
the Mult of (X) . [1,X] is set
F is right_complementable Element of the carrier of (RAlgebra the carrier of X)
1 * F is right_complementable Element of the carrier of (RAlgebra the carrier of X)
the Mult of (RAlgebra the carrier of X) is non empty Relation-like [:REAL, the carrier of (RAlgebra the carrier of X):] -defined the carrier of (RAlgebra the carrier of X) -valued Function-like total quasi_total Element of bool [:[:REAL, the carrier of (RAlgebra the carrier of X):], the carrier of (RAlgebra the carrier of X):]
[:REAL, the carrier of (RAlgebra the carrier of X):] is non empty set
[:[:REAL, the carrier of (RAlgebra the carrier of X):], the carrier of (RAlgebra the carrier of X):] is non empty set
bool [:[:REAL, the carrier of (RAlgebra the carrier of X):], the carrier of (RAlgebra the carrier of X):] is non empty set
the Mult of (RAlgebra the carrier of X) . (1,F) is set
[1,F] is set
{1,F} is non empty set
{{1,F},{1}} is non empty set
the Mult of (RAlgebra the carrier of X) . [1,F] is set
X is non empty TopSpace-like TopStruct
(X) is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative AlgebraStr
(X) is non empty add-closed having-inverse additively-closed multiplicatively-closed additively-linearly-closed Element of bool the carrier of (RAlgebra the carrier of X)
the carrier of X is non empty set
RAlgebra the carrier of X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative AlgebraStr
Funcs ( the carrier of X,REAL) is non empty functional FUNCTION_DOMAIN of the carrier of X, REAL
RealFuncMult the carrier of X is non empty Relation-like [:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):] -defined Funcs ( the carrier of X,REAL) -valued Function-like total quasi_total Element of bool [:[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):]
[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):] is non empty set
[:[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):] is non empty set
bool [:[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):] is non empty set
RealFuncAdd the carrier of X is non empty Relation-like [:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):] -defined Funcs ( the carrier of X,REAL) -valued Function-like total quasi_total Element of bool [:[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):]
RealFuncExtMult the carrier of X is non empty Relation-like [:REAL,(Funcs ( the carrier of X,REAL)):] -defined Funcs ( the carrier of X,REAL) -valued Function-like total quasi_total Element of bool [:[:REAL,(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):]
[:REAL,(Funcs ( the carrier of X,REAL)):] is non empty set
[:[:REAL,(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):] is non empty set
bool [:[:REAL,(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):] is non empty set
RealFuncUnit the carrier of X is Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() Element of Funcs ( the carrier of X,REAL)
the carrier of X --> 1 is non empty Relation-like the carrier of X -defined NAT -valued RAT -valued INT -valued Function-like total quasi_total V152() V153() V154() V155() Element of bool [: the carrier of X,NAT:]
[: the carrier of X,NAT:] is non empty RAT -valued INT -valued V152() V153() V154() V155() set
bool [: the carrier of X,NAT:] is non empty set
RealFuncZero the carrier of X is Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() Element of Funcs ( the carrier of X,REAL)
the carrier of X --> 0 is non empty Relation-like the carrier of X -defined NAT -valued RAT -valued INT -valued Function-like total quasi_total V152() V153() V154() V155() Element of bool [: the carrier of X,NAT:]
AlgebraStr(# (Funcs ( the carrier of X,REAL)),(RealFuncMult the carrier of X),(RealFuncAdd the carrier of X),(RealFuncExtMult the carrier of X),(RealFuncUnit the carrier of X),(RealFuncZero the carrier of X) #) is strict AlgebraStr
the carrier of (RAlgebra the carrier of X) is non empty set
bool the carrier of (RAlgebra the carrier of X) is non empty set
[: the carrier of X,REAL:] is non empty V152() V153() V154() set
bool [: the carrier of X,REAL:] is non empty set
{ b₁ where b₁ is non empty Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() continuous Element of bool [: the carrier of X,REAL:] : verum } is set
mult_ ((X),(RAlgebra the carrier of X)) is non empty Relation-like [:(X),(X):] -defined (X) -valued Function-like total quasi_total Element of bool [:[:(X),(X):],(X):]
[:(X),(X):] is non empty set
[:[:(X),(X):],(X):] is non empty set
bool [:[:(X),(X):],(X):] is non empty set
Add_ ((X),(RAlgebra the carrier of X)) is non empty Relation-like [:(X),(X):] -defined (X) -valued Function-like total quasi_total Element of bool [:[:(X),(X):],(X):]
Mult_ ((X),(RAlgebra the carrier of X)) is non empty Relation-like [:REAL,(X):] -defined (X) -valued Function-like total quasi_total Element of bool [:[:REAL,(X):],(X):]
[:REAL,(X):] is non empty set
[:[:REAL,(X):],(X):] is non empty set
bool [:[:REAL,(X):],(X):] is non empty set
One_ ((X),(RAlgebra the carrier of X)) is Element of (X)
Zero_ ((X),(RAlgebra the carrier of X)) is Element of (X)
AlgebraStr(# (X),(mult_ ((X),(RAlgebra the carrier of X))),(Add_ ((X),(RAlgebra the carrier of X))),(Mult_ ((X),(RAlgebra the carrier of X))),(One_ ((X),(RAlgebra the carrier of X))),(Zero_ ((X),(RAlgebra the carrier of X))) #) is strict AlgebraStr
the carrier of (X) is non empty set
X is right_complementable Element of the carrier of (X)
F is right_complementable Element of the carrier of (X)
G is right_complementable Element of the carrier of (X)
X + F is right_complementable Element of the carrier of (X)
the addF of (X) is non empty Relation-like [: the carrier of (X), the carrier of (X):] -defined the carrier of (X) -valued Function-like total 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,F) is right_complementable Element of the carrier of (X)
[X,F] is set
{X,F} is non empty set
{X} is non empty set
{{X,F},{X}} is non empty set
the addF of (X) . [X,F] is set
FB is non empty Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() Element of bool [: the carrier of X,REAL:]
GB is non empty Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() Element of bool [: the carrier of X,REAL:]
aFB is non empty Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() Element of bool [: the carrier of X,REAL:]
r is right_complementable Element of the carrier of (RAlgebra the carrier of X)
aF is right_complementable Element of the carrier of (RAlgebra the carrier of X)
aG is right_complementable Element of the carrier of (RAlgebra the carrier of X)
aF + aG is right_complementable Element of the carrier of (RAlgebra the carrier of X)
the addF of (RAlgebra the carrier of X) is non empty Relation-like [: the carrier of (RAlgebra the carrier of X), the carrier of (RAlgebra the carrier of X):] -defined the carrier of (RAlgebra the carrier of X) -valued Function-like total quasi_total Element of bool [:[: the carrier of (RAlgebra the carrier of X), the carrier of (RAlgebra the carrier of X):], the carrier of (RAlgebra the carrier of X):]
[: the carrier of (RAlgebra the carrier of X), the carrier of (RAlgebra the carrier of X):] is non empty set
[:[: the carrier of (RAlgebra the carrier of X), the carrier of (RAlgebra the carrier of X):], the carrier of (RAlgebra the carrier of X):] is non empty set
bool [:[: the carrier of (RAlgebra the carrier of X), the carrier of (RAlgebra the carrier of X):], the carrier of (RAlgebra the carrier of X):] is non empty set
the addF of (RAlgebra the carrier of X) . (aF,aG) is right_complementable Element of the carrier of (RAlgebra the carrier of X)
[aF,aG] is set
{aF,aG} is non empty set
{aF} is non empty set
{{aF,aG},{aF}} is non empty set
the addF of (RAlgebra the carrier of X) . [aF,aG] is set
s1 is Element of the carrier of X
aFB . s1 is V11() real ext-real Element of REAL
FB . s1 is V11() real ext-real Element of REAL
GB . s1 is V11() real ext-real Element of REAL
(FB . s1) + (GB . s1) is V11() real ext-real Element of REAL
X is non empty TopSpace-like TopStruct
(X) is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative AlgebraStr
(X) is non empty add-closed having-inverse additively-closed multiplicatively-closed additively-linearly-closed Element of bool the carrier of (RAlgebra the carrier of X)
the carrier of X is non empty set
RAlgebra the carrier of X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative AlgebraStr
Funcs ( the carrier of X,REAL) is non empty functional FUNCTION_DOMAIN of the carrier of X, REAL
RealFuncMult the carrier of X is non empty Relation-like [:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):] -defined Funcs ( the carrier of X,REAL) -valued Function-like total quasi_total Element of bool [:[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):]
[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):] is non empty set
[:[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):] is non empty set
bool [:[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):] is non empty set
RealFuncAdd the carrier of X is non empty Relation-like [:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):] -defined Funcs ( the carrier of X,REAL) -valued Function-like total quasi_total Element of bool [:[:(Funcs ( the carrier of X,REAL)),(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):]
RealFuncExtMult the carrier of X is non empty Relation-like [:REAL,(Funcs ( the carrier of X,REAL)):] -defined Funcs ( the carrier of X,REAL) -valued Function-like total quasi_total Element of bool [:[:REAL,(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):]
[:REAL,(Funcs ( the carrier of X,REAL)):] is non empty set
[:[:REAL,(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):] is non empty set
bool [:[:REAL,(Funcs ( the carrier of X,REAL)):],(Funcs ( the carrier of X,REAL)):] is non empty set
RealFuncUnit the carrier of X is Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() Element of Funcs ( the carrier of X,REAL)
the carrier of X --> 1 is non empty Relation-like the carrier of X -defined NAT -valued RAT -valued INT -valued Function-like total quasi_total V152() V153() V154() V155() Element of bool [: the carrier of X,NAT:]
[: the carrier of X,NAT:] is non empty RAT -valued INT -valued V152() V153() V154() V155() set
bool [: the carrier of X,NAT:] is non empty set
RealFuncZero the carrier of X is Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() Element of Funcs ( the carrier of X,REAL)
the carrier of X --> 0 is non empty Relation-like the carrier of X -defined NAT -valued RAT -valued INT -valued Function-like total quasi_total V152() V153() V154() V155() Element of bool [: the carrier of X,NAT:]
AlgebraStr(# (Funcs ( the carrier of X,REAL)),(RealFuncMult the carrier of X),(RealFuncAdd the carrier of X),(RealFuncExtMult the carrier of X),(RealFuncUnit the carrier of X),(RealFuncZero the carrier of X) #) is strict AlgebraStr
the carrier of (RAlgebra the carrier of X) is non empty set
bool the carrier of (RAlgebra the carrier of X) is non empty set
[: the carrier of X,REAL:] is non empty V152() V153() V154() set
bool [: the carrier of X,REAL:] is non empty set
{ b₁ where b₁ is non empty Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V152() V153() V154() continuous Element of bool [: the carrier of X,REAL:] : verum } is set
mult_ ((X),(RAlgebra the carrier of X)) is non empty Relation-like [:(X),(X):] -defined (X) -valued Function-like total quasi_total Element of bool [:[:(X),(X):],(X):]
[:(X),(X):] is non empty set
[:[:(X),(X):],(X):] is non empty set
bool [:[:(X),(X):],(X):] is non empty set
Add_ ((X),(RAlgebra the carrier of X)) is non empty Relation-like [:(X),(X):] -defined (X) -valued Function-like total quasi_total Element of bool [:[:(X),(X):],(X):]
Mult_ ((X),(RAlgebra the carrier of X)) is non empty Relation-like [:REAL,(X):] -defined (X) -valued Function-like total quasi_total Element of bool [:[:REAL,(X):],(X):]
[:REAL,(X):] is non empty set
[:[:REAL,(X):],(X):] is non empty set
bool [:[:REAL,(X):],(X):] is non empty set
One_ ((X),(RAlgebra the carrier of X)) is Element of (X)
Zero_ ((X),(RAlgebra the carrier of X)) is Element of (X)
AlgebraStr(# (X),(mult_ ((X),(RAlgebra the carrier of X))),(Add_ ((X),(RAlgebra the carrier of X))),(Mult_ ((X),(RAlgebra the carrier of X))),(One_ ((X),(RAlgebra the carrier of X))),(Zero_ ((X),(RAlgebra the carrier of X))) #) is