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

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

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

(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

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

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

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

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

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

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

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