begin
definition
let V be ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100()
unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
Ring) ;
mode Subring of
V -> ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100()
unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
Ring)
means
( the
carrier of
it : ( ( ) ( )
set ) : ( ( ) ( )
set )
c= the
carrier of
V : ( ( non
empty ) ( non
empty )
addLoopStr ) : ( ( ) ( non
empty )
set ) & the
addF of
it : ( ( ) ( )
set ) : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set )
-defined the
carrier of
it : ( ( ) ( )
set ) : ( ( ) ( )
set )
-valued Function-like quasi_total )
Element of
bool [:[: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) )
= the
addF of
V : ( ( non
empty ) ( non
empty )
addLoopStr ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [: the carrier of V : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
V : ( ( non
empty ) ( non
empty )
addLoopStr ) : ( ( ) ( non
empty )
set )
-valued Function-like V23(
[: the carrier of V : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
bool [:[: the carrier of V : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
|| the
carrier of
it : ( ( ) ( )
set ) : ( ( ) ( )
set ) : ( ( ) (
Relation-like Function-like )
set ) & the
multF of
it : ( ( ) ( )
set ) : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set )
-defined the
carrier of
it : ( ( ) ( )
set ) : ( ( ) ( )
set )
-valued Function-like quasi_total )
Element of
bool [:[: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) )
= the
multF of
V : ( ( non
empty ) ( non
empty )
addLoopStr ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [: the carrier of V : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
V : ( ( non
empty ) ( non
empty )
addLoopStr ) : ( ( ) ( non
empty )
set )
-valued Function-like V23(
[: the carrier of V : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
bool [:[: the carrier of V : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
|| the
carrier of
it : ( ( ) ( )
set ) : ( ( ) ( )
set ) : ( ( ) (
Relation-like Function-like )
set ) &
1. it : ( ( ) ( )
set ) : ( ( ) ( )
Element of the
carrier of
it : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
= 1. V : ( ( non
empty ) ( non
empty )
addLoopStr ) : ( ( ) ( )
Element of the
carrier of
V : ( ( non
empty ) ( non
empty )
addLoopStr ) : ( ( ) ( non
empty )
set ) ) &
0. it : ( ( ) ( )
set ) : ( ( ) ( )
Element of the
carrier of
it : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
= 0. V : ( ( non
empty ) ( non
empty )
addLoopStr ) : ( ( ) (
V49(
V : ( ( non
empty ) ( non
empty )
addLoopStr ) ) )
Element of the
carrier of
V : ( ( non
empty ) ( non
empty )
addLoopStr ) : ( ( ) ( non
empty )
set ) ) );
end;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
d1,
d2 being ( ( ) ( )
Element of
X : ( ( non
empty ) ( non
empty )
set ) )
for
A being ( (
Function-like quasi_total ) ( non
empty Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like V23(
[:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
BinOp of
X : ( ( non
empty ) ( non
empty )
set ) )
for
M being ( (
Function-like quasi_total ) ( non
empty Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like V23(
[:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of
[:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
X : ( ( non
empty ) ( non
empty )
set ) )
for
V being ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100()
unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
Ring)
for
V1 being ( ( ) ( )
Subset of ) st
V1 : ( ( ) ( )
Subset of )
= X : ( ( non
empty ) ( non
empty )
set ) &
A : ( (
Function-like quasi_total ) ( non
empty Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like V23(
[:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
BinOp of
b1 : ( ( non
empty ) ( non
empty )
set ) )
= the
addF of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100()
unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
Ring) : ( (
Function-like quasi_total ) ( non
empty Relation-like [: the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) Ring) : ( ( ) ( non empty ) set ) , the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) Ring) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
b6 : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100()
unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
Ring) : ( ( ) ( non
empty )
set )
-valued Function-like V23(
[: the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) Ring) : ( ( ) ( non empty ) set ) , the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) Ring) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
bool [:[: the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) Ring) : ( ( ) ( non empty ) set ) , the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) Ring) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) Ring) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
|| V1 : ( ( ) ( )
Subset of ) : ( ( ) (
Relation-like Function-like )
set ) &
M : ( (
Function-like quasi_total ) ( non
empty Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like V23(
[:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of
[:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
b1 : ( ( non
empty ) ( non
empty )
set ) )
= the
multF of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100()
unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
Ring) : ( (
Function-like quasi_total ) ( non
empty Relation-like [: the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) Ring) : ( ( ) ( non empty ) set ) , the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) Ring) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
b6 : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100()
unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
Ring) : ( ( ) ( non
empty )
set )
-valued Function-like V23(
[: the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) Ring) : ( ( ) ( non empty ) set ) , the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) Ring) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
bool [:[: the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) Ring) : ( ( ) ( non empty ) set ) , the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) Ring) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) Ring) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
|| V1 : ( ( ) ( )
Subset of ) : ( ( ) (
Relation-like Function-like )
set ) &
d1 : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) )
= 1. V : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100()
unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
Ring) : ( ( ) (
left_complementable right_complementable complementable )
Element of the
carrier of
b6 : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100()
unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
Ring) : ( ( ) ( non
empty )
set ) ) &
d2 : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) )
= 0. V : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100()
unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
Ring) : ( ( ) (
V49(
b6 : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100()
unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
Ring) )
left_complementable right_complementable complementable )
Element of the
carrier of
b6 : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100()
unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
Ring) : ( ( ) ( non
empty )
set ) ) &
V1 : ( ( ) ( )
Subset of ) is
having-inverse holds
doubleLoopStr(#
X : ( ( non
empty ) ( non
empty )
set ) ,
A : ( (
Function-like quasi_total ) ( non
empty Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like V23(
[:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
BinOp of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
M : ( (
Function-like quasi_total ) ( non
empty Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like V23(
[:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of
[:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
d1 : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
d2 : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) is ( ( ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100()
unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
Subring of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100()
unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
Ring) ) ;
theorem
for
V being ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100()
unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
Ring)
for
V1 being ( ( ) ( )
Subset of ) st
V1 : ( ( ) ( )
Subset of ) is
additively-closed &
V1 : ( ( ) ( )
Subset of ) is
multiplicatively-closed & not
V1 : ( ( ) ( )
Subset of ) is
empty holds
doubleLoopStr(#
V1 : ( ( ) ( )
Subset of ) ,
(Add_ (V1 : ( ( ) ( ) Subset of ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) Ring) )) : ( (
Function-like quasi_total ) (
Relation-like [:b2 : ( ( ) ( ) Subset of ) ,b2 : ( ( ) ( ) Subset of ) :] : ( ( ) ( )
set )
-defined b2 : ( ( ) ( )
Subset of )
-valued Function-like quasi_total )
BinOp of
b2 : ( ( ) ( )
Subset of ) ) ,
(mult_ (V1 : ( ( ) ( ) Subset of ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) Ring) )) : ( (
Function-like quasi_total ) (
Relation-like [:b2 : ( ( ) ( ) Subset of ) ,b2 : ( ( ) ( ) Subset of ) :] : ( ( ) ( )
set )
-defined b2 : ( ( ) ( )
Subset of )
-valued Function-like quasi_total )
BinOp of
b2 : ( ( ) ( )
Subset of ) ) ,
(One_ (V1 : ( ( ) ( ) Subset of ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) Ring) )) : ( ( ) ( )
Element of
b2 : ( ( ) ( )
Subset of ) ) ,
(Zero_ (V1 : ( ( ) ( ) Subset of ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) Ring) )) : ( ( ) ( )
Element of
b2 : ( ( ) ( )
Subset of ) ) #) : ( (
strict ) (
strict )
doubleLoopStr ) is ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100()
unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
Ring) ;
begin
definition
let V be ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
Algebra) ;
mode Subalgebra of
V -> ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
Algebra)
means
( the
carrier of
it : ( ( ) ( )
set ) : ( ( ) ( )
set )
c= the
carrier of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100()
unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) & the
addF of
it : ( ( ) ( )
set ) : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set )
-defined the
carrier of
it : ( ( ) ( )
set ) : ( ( ) ( )
set )
-valued Function-like quasi_total )
Element of
bool [:[: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) )
= the
addF of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100()
unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [: the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100()
unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) : ( ( ) ( non
empty )
set )
-valued Function-like V23(
[: the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
bool [:[: the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
|| the
carrier of
it : ( ( ) ( )
set ) : ( ( ) ( )
set ) : ( ( ) (
Relation-like Function-like )
set ) & the
multF of
it : ( ( ) ( )
set ) : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set )
-defined the
carrier of
it : ( ( ) ( )
set ) : ( ( ) ( )
set )
-valued Function-like quasi_total )
Element of
bool [:[: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) )
= the
multF of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100()
unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [: the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100()
unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) : ( ( ) ( non
empty )
set )
-valued Function-like V23(
[: the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
bool [:[: the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
|| the
carrier of
it : ( ( ) ( )
set ) : ( ( ) ( )
set ) : ( ( ) (
Relation-like Function-like )
set ) & the
Mult of
it : ( ( ) ( )
set ) : ( (
Function-like quasi_total ) (
Relation-like [:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set )
-defined the
carrier of
it : ( ( ) ( )
set ) : ( ( ) ( )
set )
-valued Function-like quasi_total )
Element of
bool [:[:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) )
= the
Mult of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100()
unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100()
unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) : ( ( ) ( non
empty )
set )
-valued Function-like V23(
[:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
bool [:[:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
| [:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) : ( (
Function-like ) (
Relation-like [:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100()
unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) : ( ( ) ( non
empty )
set )
-valued Function-like )
Element of
bool [:[:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) &
1. it : ( ( ) ( )
set ) : ( ( ) ( )
Element of the
carrier of
it : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
= 1. V : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100()
unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) : ( ( ) (
left_complementable right_complementable complementable )
Element of the
carrier of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100()
unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) ) &
0. it : ( ( ) ( )
set ) : ( ( ) ( )
Element of the
carrier of
it : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
= 0. V : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100()
unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) : ( ( ) (
V49(
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100()
unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) )
left_complementable right_complementable complementable )
Element of the
carrier of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100()
unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) ) );
end;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
d1,
d2 being ( ( ) ( )
Element of
X : ( ( non
empty ) ( non
empty )
set ) )
for
A being ( (
Function-like quasi_total ) ( non
empty Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like V23(
[:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
BinOp of
X : ( ( non
empty ) ( non
empty )
set ) )
for
M being ( (
Function-like quasi_total ) ( non
empty Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like V23(
[:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of
[:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
X : ( ( non
empty ) ( non
empty )
set ) )
for
V being ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
Algebra)
for
V1 being ( ( ) ( )
Subset of )
for
MR being ( (
Function-like quasi_total ) ( non
empty Relation-like [:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like V23(
[:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of
[:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
X : ( ( non
empty ) ( non
empty )
set ) ) st
V1 : ( ( ) ( )
Subset of )
= X : ( ( non
empty ) ( non
empty )
set ) &
d1 : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) )
= 0. V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
Algebra) : ( ( ) (
V49(
b6 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
Algebra) )
left_complementable right_complementable complementable )
Element of the
carrier of
b6 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
Algebra) : ( ( ) ( non
empty )
set ) ) &
d2 : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) )
= 1. V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
Algebra) : ( ( ) (
left_complementable right_complementable complementable )
Element of the
carrier of
b6 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
Algebra) : ( ( ) ( non
empty )
set ) ) &
A : ( (
Function-like quasi_total ) ( non
empty Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like V23(
[:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
BinOp of
b1 : ( ( non
empty ) ( non
empty )
set ) )
= the
addF of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
Algebra) : ( (
Function-like quasi_total ) ( non
empty Relation-like [: the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) Algebra) : ( ( ) ( non empty ) set ) , the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) Algebra) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
b6 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
Algebra) : ( ( ) ( non
empty )
set )
-valued Function-like V23(
[: the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) Algebra) : ( ( ) ( non empty ) set ) , the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) Algebra) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
bool [:[: the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) Algebra) : ( ( ) ( non empty ) set ) , the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) Algebra) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) Algebra) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
|| V1 : ( ( ) ( )
Subset of ) : ( ( ) (
Relation-like Function-like )
set ) &
M : ( (
Function-like quasi_total ) ( non
empty Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like V23(
[:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of
[:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
b1 : ( ( non
empty ) ( non
empty )
set ) )
= the
multF of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
Algebra) : ( (
Function-like quasi_total ) ( non
empty Relation-like [: the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) Algebra) : ( ( ) ( non empty ) set ) , the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) Algebra) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
b6 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
Algebra) : ( ( ) ( non
empty )
set )
-valued Function-like V23(
[: the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) Algebra) : ( ( ) ( non empty ) set ) , the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) Algebra) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
bool [:[: the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) Algebra) : ( ( ) ( non empty ) set ) , the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) Algebra) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) Algebra) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
|| V1 : ( ( ) ( )
Subset of ) : ( ( ) (
Relation-like Function-like )
set ) &
MR : ( (
Function-like quasi_total ) ( non
empty Relation-like [:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like V23(
[:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of
[:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
b1 : ( ( non
empty ) ( non
empty )
set ) )
= the
Mult of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
Algebra) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) , the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) Algebra) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
b6 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
Algebra) : ( ( ) ( non
empty )
set )
-valued Function-like V23(
[:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) , the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) Algebra) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
bool [:[:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) , the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) Algebra) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) Algebra) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
| [:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) ,V1 : ( ( ) ( ) Subset of ) :] : ( ( ) ( )
set ) : ( (
Function-like ) (
Relation-like [:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) , the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) Algebra) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
b6 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
Algebra) : ( ( ) ( non
empty )
set )
-valued Function-like )
Element of
bool [:[:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) , the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) Algebra) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) Algebra) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) &
V1 : ( ( ) ( )
Subset of ) is
having-inverse holds
AlgebraStr(#
X : ( ( non
empty ) ( non
empty )
set ) ,
M : ( (
Function-like quasi_total ) ( non
empty Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like V23(
[:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of
[:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
A : ( (
Function-like quasi_total ) ( non
empty Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like V23(
[:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
BinOp of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
MR : ( (
Function-like quasi_total ) ( non
empty Relation-like [:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like V23(
[:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of
[:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
d2 : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
d1 : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) ) #) : ( (
strict ) (
strict )
AlgebraStr ) is ( ( ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
Subalgebra of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
Algebra) ) ;
definition
let V be ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
Algebra) ;
let V1 be ( ( ) ( )
Subset of ) ;
assume
(
V1 : ( ( ) ( )
Subset of ) is
additively-linearly-closed & not
V1 : ( ( ) ( )
Subset of ) is
empty )
;
func Mult_ (
V1,
V)
-> ( (
Function-like quasi_total ) (
Relation-like [:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) ,V1 : ( ( ) ( ) set ) :] : ( ( ) ( )
set )
-defined V1 : ( ( ) ( )
set )
-valued Function-like quasi_total )
Function of
[:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) ,V1 : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) ,
V1 : ( ( ) ( )
set ) )
equals
the
Mult of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
AlgebraStr ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
AlgebraStr ) : ( ( ) ( non
empty )
set )
-valued Function-like V23(
[:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
bool [:[:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
| [:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) ,V1 : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) : ( (
Function-like ) (
Relation-like [:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
AlgebraStr ) : ( ( ) ( non
empty )
set )
-valued Function-like )
Element of
bool [:[:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ;
end;
theorem
for
V being ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
Algebra)
for
V1 being ( ( ) ( )
Subset of ) st
V1 : ( ( ) ( )
Subset of ) is
additively-linearly-closed &
V1 : ( ( ) ( )
Subset of ) is
multiplicatively-closed & not
V1 : ( ( ) ( )
Subset of ) is
empty holds
AlgebraStr(#
V1 : ( ( ) ( )
Subset of ) ,
(mult_ (V1 : ( ( ) ( ) Subset of ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) Algebra) )) : ( (
Function-like quasi_total ) (
Relation-like [:b2 : ( ( ) ( ) Subset of ) ,b2 : ( ( ) ( ) Subset of ) :] : ( ( ) ( )
set )
-defined b2 : ( ( ) ( )
Subset of )
-valued Function-like quasi_total )
BinOp of
b2 : ( ( ) ( )
Subset of ) ) ,
(Add_ (V1 : ( ( ) ( ) Subset of ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) Algebra) )) : ( (
Function-like quasi_total ) (
Relation-like [:b2 : ( ( ) ( ) Subset of ) ,b2 : ( ( ) ( ) Subset of ) :] : ( ( ) ( )
set )
-defined b2 : ( ( ) ( )
Subset of )
-valued Function-like quasi_total )
BinOp of
b2 : ( ( ) ( )
Subset of ) ) ,
(Mult_ (V1 : ( ( ) ( ) Subset of ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) Algebra) )) : ( (
Function-like quasi_total ) (
Relation-like [:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) ,b2 : ( ( ) ( ) Subset of ) :] : ( ( ) ( )
set )
-defined b2 : ( ( ) ( )
Subset of )
-valued Function-like quasi_total )
Function of
[:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) ,b2 : ( ( ) ( ) Subset of ) :] : ( ( ) ( )
set ) ,
b2 : ( ( ) ( )
Subset of ) ) ,
(One_ (V1 : ( ( ) ( ) Subset of ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) Algebra) )) : ( ( ) ( )
Element of
b2 : ( ( ) ( )
Subset of ) ) ,
(Zero_ (V1 : ( ( ) ( ) Subset of ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) Algebra) )) : ( ( ) ( )
Element of
b2 : ( ( ) ( )
Subset of ) ) #) : ( (
strict ) (
strict )
AlgebraStr ) is ( ( ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
Subalgebra of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
Algebra) ) ;
begin
definition
let X be ( ( non
empty ) ( non
empty )
set ) ;
func R_Algebra_of_BoundedFunctions X -> ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
Algebra)
equals
AlgebraStr(#
(BoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( non
empty ) ( non
empty )
Subset of ) ,
(mult_ ((BoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(RAlgebra X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() strict vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) )) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:(BoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(BoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non
empty )
set )
-defined BoundedFunctions X : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
AlgebraStr ) : ( ( non
empty ) ( non
empty )
Subset of )
-valued Function-like V23(
[:(BoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(BoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
BinOp of
BoundedFunctions X : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
AlgebraStr ) : ( ( non
empty ) ( non
empty )
Subset of ) ) ,
(Add_ ((BoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(RAlgebra X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() strict vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) )) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:(BoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(BoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non
empty )
set )
-defined BoundedFunctions X : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
AlgebraStr ) : ( ( non
empty ) ( non
empty )
Subset of )
-valued Function-like V23(
[:(BoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(BoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
BinOp of
BoundedFunctions X : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
AlgebraStr ) : ( ( non
empty ) ( non
empty )
Subset of ) ) ,
(Mult_ ((BoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(RAlgebra X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() strict vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) )) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) ,(BoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non
empty )
set )
-defined BoundedFunctions X : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
AlgebraStr ) : ( ( non
empty ) ( non
empty )
Subset of )
-valued Function-like V23(
[:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) ,(BoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of
[:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) ,(BoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non
empty )
set ) ,
BoundedFunctions X : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
AlgebraStr ) : ( ( non
empty ) ( non
empty )
Subset of ) ) ,
(One_ ((BoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(RAlgebra X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() strict vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) )) : ( ( ) ( )
Element of
BoundedFunctions X : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
AlgebraStr ) : ( ( non
empty ) ( non
empty )
Subset of ) ) ,
(Zero_ ((BoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(RAlgebra X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() strict vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) )) : ( ( ) ( )
Element of
BoundedFunctions X : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
AlgebraStr ) : ( ( non
empty ) ( non
empty )
Subset of ) ) #) : ( (
strict ) (
strict )
AlgebraStr ) ;
end;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
F,
G,
H being ( ( ) (
left_complementable right_complementable complementable )
VECTOR of ( ( ) ( non
empty )
set ) )
for
f,
g,
h being ( (
Function-like quasi_total ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set )
-valued Function-like V23(
b1 : ( ( non
empty ) ( non
empty )
set ) )
quasi_total V150()
V151()
V152() )
Function of
X : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) ) st
f : ( (
Function-like quasi_total ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set )
-valued Function-like V23(
b1 : ( ( non
empty ) ( non
empty )
set ) )
quasi_total V150()
V151()
V152() )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) )
= F : ( ( ) (
left_complementable right_complementable complementable )
VECTOR of ( ( ) ( non
empty )
set ) ) &
g : ( (
Function-like quasi_total ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set )
-valued Function-like V23(
b1 : ( ( non
empty ) ( non
empty )
set ) )
quasi_total V150()
V151()
V152() )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) )
= G : ( ( ) (
left_complementable right_complementable complementable )
VECTOR of ( ( ) ( non
empty )
set ) ) &
h : ( (
Function-like quasi_total ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set )
-valued Function-like V23(
b1 : ( ( non
empty ) ( non
empty )
set ) )
quasi_total V150()
V151()
V152() )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) )
= H : ( ( ) (
left_complementable right_complementable complementable )
VECTOR of ( ( ) ( non
empty )
set ) ) holds
(
H : ( ( ) (
left_complementable right_complementable complementable )
VECTOR of ( ( ) ( non
empty )
set ) )
= F : ( ( ) (
left_complementable right_complementable complementable )
VECTOR of ( ( ) ( non
empty )
set ) )
+ G : ( ( ) (
left_complementable right_complementable complementable )
VECTOR of ( ( ) ( non
empty )
set ) ) : ( ( ) (
left_complementable right_complementable complementable )
Element of the
carrier of
(R_Algebra_of_BoundedFunctions b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
Algebra) : ( ( ) ( non
empty )
set ) ) iff for
x being ( ( ) ( )
Element of
X : ( ( non
empty ) ( non
empty )
set ) ) holds
h : ( (
Function-like quasi_total ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set )
-valued Function-like V23(
b1 : ( ( non
empty ) ( non
empty )
set ) )
quasi_total V150()
V151()
V152() )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) )
. x : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) )
= (f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total V150() V151() V152() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) )
+ (g : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total V150() V151() V152() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
F,
G,
H being ( ( ) (
left_complementable right_complementable complementable )
VECTOR of ( ( ) ( non
empty )
set ) )
for
f,
g,
h being ( (
Function-like quasi_total ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set )
-valued Function-like V23(
b1 : ( ( non
empty ) ( non
empty )
set ) )
quasi_total V150()
V151()
V152() )
Function of
X : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) ) st
f : ( (
Function-like quasi_total ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set )
-valued Function-like V23(
b1 : ( ( non
empty ) ( non
empty )
set ) )
quasi_total V150()
V151()
V152() )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) )
= F : ( ( ) (
left_complementable right_complementable complementable )
VECTOR of ( ( ) ( non
empty )
set ) ) &
g : ( (
Function-like quasi_total ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set )
-valued Function-like V23(
b1 : ( ( non
empty ) ( non
empty )
set ) )
quasi_total V150()
V151()
V152() )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) )
= G : ( ( ) (
left_complementable right_complementable complementable )
VECTOR of ( ( ) ( non
empty )
set ) ) &
h : ( (
Function-like quasi_total ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set )
-valued Function-like V23(
b1 : ( ( non
empty ) ( non
empty )
set ) )
quasi_total V150()
V151()
V152() )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) )
= H : ( ( ) (
left_complementable right_complementable complementable )
VECTOR of ( ( ) ( non
empty )
set ) ) holds
(
H : ( ( ) (
left_complementable right_complementable complementable )
VECTOR of ( ( ) ( non
empty )
set ) )
= F : ( ( ) (
left_complementable right_complementable complementable )
VECTOR of ( ( ) ( non
empty )
set ) )
* G : ( ( ) (
left_complementable right_complementable complementable )
VECTOR of ( ( ) ( non
empty )
set ) ) : ( ( ) (
left_complementable right_complementable complementable )
Element of the
carrier of
(R_Algebra_of_BoundedFunctions b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
Algebra) : ( ( ) ( non
empty )
set ) ) iff for
x being ( ( ) ( )
Element of
X : ( ( non
empty ) ( non
empty )
set ) ) holds
h : ( (
Function-like quasi_total ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set )
-valued Function-like V23(
b1 : ( ( non
empty ) ( non
empty )
set ) )
quasi_total V150()
V151()
V152() )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) )
. x : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) )
= (f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total V150() V151() V152() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) )
* (g : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total V150() V151() V152() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) ) ) ;
definition
let X be ( ( non
empty ) ( non
empty )
set ) ;
func R_Normed_Algebra_of_BoundedFunctions X -> ( ( ) ( )
Normed_AlgebraStr )
equals
Normed_AlgebraStr(#
(BoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( non
empty ) ( non
empty )
Subset of ) ,
(mult_ ((BoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(RAlgebra X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() strict vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) )) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:(BoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(BoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non
empty )
set )
-defined BoundedFunctions X : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
AlgebraStr ) : ( ( non
empty ) ( non
empty )
Subset of )
-valued Function-like V23(
[:(BoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(BoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
BinOp of
BoundedFunctions X : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
AlgebraStr ) : ( ( non
empty ) ( non
empty )
Subset of ) ) ,
(Add_ ((BoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(RAlgebra X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() strict vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) )) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:(BoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(BoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non
empty )
set )
-defined BoundedFunctions X : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
AlgebraStr ) : ( ( non
empty ) ( non
empty )
Subset of )
-valued Function-like V23(
[:(BoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(BoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
BinOp of
BoundedFunctions X : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
AlgebraStr ) : ( ( non
empty ) ( non
empty )
Subset of ) ) ,
(Mult_ ((BoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(RAlgebra X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() strict vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) )) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) ,(BoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non
empty )
set )
-defined BoundedFunctions X : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
AlgebraStr ) : ( ( non
empty ) ( non
empty )
Subset of )
-valued Function-like V23(
[:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) ,(BoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of
[:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) ,(BoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non
empty )
set ) ,
BoundedFunctions X : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
AlgebraStr ) : ( ( non
empty ) ( non
empty )
Subset of ) ) ,
(One_ ((BoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(RAlgebra X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() strict vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) )) : ( ( ) ( )
Element of
BoundedFunctions X : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
AlgebraStr ) : ( ( non
empty ) ( non
empty )
Subset of ) ) ,
(Zero_ ((BoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(RAlgebra X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() strict vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) )) : ( ( ) ( )
Element of
BoundedFunctions X : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
AlgebraStr ) : ( ( non
empty ) ( non
empty )
Subset of ) ) ,
(BoundedFunctionsNorm X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital ) AlgebraStr ) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like BoundedFunctions X : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
AlgebraStr ) : ( ( non
empty ) ( non
empty )
Subset of )
-defined REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set )
-valued Function-like V23(
BoundedFunctions X : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
AlgebraStr ) : ( ( non
empty ) ( non
empty )
Subset of ) )
quasi_total V150()
V151()
V152() )
Function of
BoundedFunctions X : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
AlgebraStr ) : ( ( non
empty ) ( non
empty )
Subset of ) ,
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) ) #) : ( (
strict ) (
strict )
Normed_AlgebraStr ) ;
end;
theorem
for
W being ( ( ) ( )
Normed_AlgebraStr )
for
V being ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
Algebra) st
AlgebraStr(# the
carrier of
W : ( ( ) ( )
Normed_AlgebraStr ) : ( ( ) ( )
set ) , the
multF of
W : ( ( ) ( )
Normed_AlgebraStr ) : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of b1 : ( ( ) ( ) Normed_AlgebraStr ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( ) ( ) Normed_AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set )
-defined the
carrier of
b1 : ( ( ) ( )
Normed_AlgebraStr ) : ( ( ) ( )
set )
-valued Function-like quasi_total )
Element of
bool [:[: the carrier of b1 : ( ( ) ( ) Normed_AlgebraStr ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( ) ( ) Normed_AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( ) ( ) Normed_AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) , the
addF of
W : ( ( ) ( )
Normed_AlgebraStr ) : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of b1 : ( ( ) ( ) Normed_AlgebraStr ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( ) ( ) Normed_AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set )
-defined the
carrier of
b1 : ( ( ) ( )
Normed_AlgebraStr ) : ( ( ) ( )
set )
-valued Function-like quasi_total )
Element of
bool [:[: the carrier of b1 : ( ( ) ( ) Normed_AlgebraStr ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( ) ( ) Normed_AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( ) ( ) Normed_AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) , the
Mult of
W : ( ( ) ( )
Normed_AlgebraStr ) : ( (
Function-like quasi_total ) (
Relation-like [:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) , the carrier of b1 : ( ( ) ( ) Normed_AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set )
-defined the
carrier of
b1 : ( ( ) ( )
Normed_AlgebraStr ) : ( ( ) ( )
set )
-valued Function-like quasi_total )
Element of
bool [:[:REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) , the carrier of b1 : ( ( ) ( ) Normed_AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( ) ( ) Normed_AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) , the
OneF of
W : ( ( ) ( )
Normed_AlgebraStr ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( ) ( )
Normed_AlgebraStr ) : ( ( ) ( )
set ) ) , the
ZeroF of
W : ( ( ) ( )
Normed_AlgebraStr ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( ) ( )
Normed_AlgebraStr ) : ( ( ) ( )
set ) ) #) : ( (
strict ) (
strict )
AlgebraStr )
= V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
Algebra) holds
W : ( ( ) ( )
Normed_AlgebraStr ) is ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100()
vector-associative unital associative commutative right-distributive right_unital well-unital left_unital )
Algebra) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
f,
g,
h being ( (
Function-like quasi_total ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set )
-valued Function-like V23(
b1 : ( ( non
empty ) ( non
empty )
set ) )
quasi_total V150()
V151()
V152() )
Function of
X : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) )
for
F,
G,
H being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) st
f : ( (
Function-like quasi_total ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set )
-valued Function-like V23(
b1 : ( ( non
empty ) ( non
empty )
set ) )
quasi_total V150()
V151()
V152() )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) )
= F : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) &
g : ( (
Function-like quasi_total ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set )
-valued Function-like V23(
b1 : ( ( non
empty ) ( non
empty )
set ) )
quasi_total V150()
V151()
V152() )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) )
= G : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) &
h : ( (
Function-like quasi_total ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set )
-valued Function-like V23(
b1 : ( ( non
empty ) ( non
empty )
set ) )
quasi_total V150()
V151()
V152() )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) )
= H : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) holds
(
H : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) )
= F : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) )
+ G : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
(R_Normed_Algebra_of_BoundedFunctions b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty unital )
Normed_AlgebraStr ) : ( ( ) ( non
empty )
set ) ) iff for
x being ( ( ) ( )
Element of
X : ( ( non
empty ) ( non
empty )
set ) ) holds
h : ( (
Function-like quasi_total ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set )
-valued Function-like V23(
b1 : ( ( non
empty ) ( non
empty )
set ) )
quasi_total V150()
V151()
V152() )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) )
. x : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) )
= (f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total V150() V151() V152() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) )
+ (g : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total V150() V151() V152() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
f,
g,
h being ( (
Function-like quasi_total ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set )
-valued Function-like V23(
b1 : ( ( non
empty ) ( non
empty )
set ) )
quasi_total V150()
V151()
V152() )
Function of
X : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) )
for
F,
G,
H being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) st
f : ( (
Function-like quasi_total ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set )
-valued Function-like V23(
b1 : ( ( non
empty ) ( non
empty )
set ) )
quasi_total V150()
V151()
V152() )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) )
= F : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) &
g : ( (
Function-like quasi_total ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set )
-valued Function-like V23(
b1 : ( ( non
empty ) ( non
empty )
set ) )
quasi_total V150()
V151()
V152() )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) )
= G : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) &
h : ( (
Function-like quasi_total ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set )
-valued Function-like V23(
b1 : ( ( non
empty ) ( non
empty )
set ) )
quasi_total V150()
V151()
V152() )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) )
= H : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) holds
(
H : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) )
= F : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) )
* G : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
(R_Normed_Algebra_of_BoundedFunctions b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty unital )
Normed_AlgebraStr ) : ( ( ) ( non
empty )
set ) ) iff for
x being ( ( ) ( )
Element of
X : ( ( non
empty ) ( non
empty )
set ) ) holds
h : ( (
Function-like quasi_total ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set )
-valued Function-like V23(
b1 : ( ( non
empty ) ( non
empty )
set ) )
quasi_total V150()
V151()
V152() )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) )
. x : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) )
= (f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total V150() V151() V152() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) )
* (g : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total V150() V151() V152() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
f,
g,
h being ( (
Function-like quasi_total ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set )
-valued Function-like V23(
b1 : ( ( non
empty ) ( non
empty )
set ) )
quasi_total V150()
V151()
V152() )
Function of
X : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) )
for
F,
G,
H being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) st
f : ( (
Function-like quasi_total ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set )
-valued Function-like V23(
b1 : ( ( non
empty ) ( non
empty )
set ) )
quasi_total V150()
V151()
V152() )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) )
= F : ( ( ) (
left_complementable right_complementable complementable )
Point of ( ( ) ( non
empty )
set ) ) &
g : ( (
Function-like quasi_total ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set )
-valued Function-like V23(
b1 : ( ( non
empty ) ( non
empty )
set ) )
quasi_total V150()
V151()
V152() )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) )
= G : ( ( ) (
left_complementable right_complementable complementable )
Point of ( ( ) ( non
empty )
set ) ) &
h : ( (
Function-like quasi_total ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set )
-valued Function-like V23(
b1 : ( ( non
empty ) ( non
empty )
set ) )
quasi_total V150()
V151()
V152() )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) )
= H : ( ( ) (
left_complementable right_complementable complementable )
Point of ( ( ) ( non
empty )
set ) ) holds
(
H : ( ( ) (
left_complementable right_complementable complementable )
Point of ( ( ) ( non
empty )
set ) )
= F : ( ( ) (
left_complementable right_complementable complementable )
Point of ( ( ) ( non
empty )
set ) )
- G : ( ( ) (
left_complementable right_complementable complementable )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
left_complementable right_complementable complementable )
Element of the
carrier of
(R_Normed_Algebra_of_BoundedFunctions b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100()
discerning reflexive RealNormSpace-like unital )
Normed_AlgebraStr ) : ( ( ) ( non
empty )
set ) ) iff for
x being ( ( ) ( )
Element of
X : ( ( non
empty ) ( non
empty )
set ) ) holds
h : ( (
Function-like quasi_total ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set )
-valued Function-like V23(
b1 : ( ( non
empty ) ( non
empty )
set ) )
quasi_total V150()
V151()
V152() )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) )
. x : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) )
= (f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total V150() V151() V152() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) )
- (g : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total V150() V151() V152() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V30() V177() V178() V179() V183() ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V30()
V177()
V178()
V179()
V183() )
set ) ) ) ;