:: CC0SP1 semantic presentation

begin

definition
let V be ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) ;
mode ComplexSubAlgebra of V -> ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) means :: CC0SP1:def 1
( the carrier of it : ( ( ) ( ) VectSpStr over V : ( ( ) ( ) Normed_Complex_AlgebraStr ) ) : ( ( ) ( ) set ) c= the carrier of V : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) & the addF of it : ( ( ) ( ) VectSpStr over V : ( ( ) ( ) Normed_Complex_AlgebraStr ) ) : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of it : ( ( ) ( ) VectSpStr over V : ( ( ) ( ) Normed_Complex_AlgebraStr ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) VectSpStr over V : ( ( ) ( ) Normed_Complex_AlgebraStr ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined the carrier of it : ( ( ) ( ) VectSpStr over V : ( ( ) ( ) Normed_Complex_AlgebraStr ) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[: the carrier of it : ( ( ) ( ) VectSpStr over V : ( ( ) ( ) Normed_Complex_AlgebraStr ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) VectSpStr over V : ( ( ) ( ) Normed_Complex_AlgebraStr ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) VectSpStr over V : ( ( ) ( ) Normed_Complex_AlgebraStr ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = the addF of V : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of V : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined the carrier of V : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[: the carrier of V : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) || the carrier of it : ( ( ) ( ) VectSpStr over V : ( ( ) ( ) Normed_Complex_AlgebraStr ) ) : ( ( ) ( ) set ) : ( ( ) ( Relation-like Function-like ) set ) & the multF of it : ( ( ) ( ) VectSpStr over V : ( ( ) ( ) Normed_Complex_AlgebraStr ) ) : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of it : ( ( ) ( ) VectSpStr over V : ( ( ) ( ) Normed_Complex_AlgebraStr ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) VectSpStr over V : ( ( ) ( ) Normed_Complex_AlgebraStr ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined the carrier of it : ( ( ) ( ) VectSpStr over V : ( ( ) ( ) Normed_Complex_AlgebraStr ) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[: the carrier of it : ( ( ) ( ) VectSpStr over V : ( ( ) ( ) Normed_Complex_AlgebraStr ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) VectSpStr over V : ( ( ) ( ) Normed_Complex_AlgebraStr ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) VectSpStr over V : ( ( ) ( ) Normed_Complex_AlgebraStr ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = the multF of V : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of V : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined the carrier of V : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[: the carrier of V : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) || the carrier of it : ( ( ) ( ) VectSpStr over V : ( ( ) ( ) Normed_Complex_AlgebraStr ) ) : ( ( ) ( ) set ) : ( ( ) ( Relation-like Function-like ) set ) & the Mult of it : ( ( ) ( ) VectSpStr over V : ( ( ) ( ) Normed_Complex_AlgebraStr ) ) : ( ( Function-like quasi_total ) ( Relation-like [:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) , the carrier of it : ( ( ) ( ) VectSpStr over V : ( ( ) ( ) Normed_Complex_AlgebraStr ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined the carrier of it : ( ( ) ( ) VectSpStr over V : ( ( ) ( ) Normed_Complex_AlgebraStr ) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) , the carrier of it : ( ( ) ( ) VectSpStr over V : ( ( ) ( ) Normed_Complex_AlgebraStr ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) VectSpStr over V : ( ( ) ( ) Normed_Complex_AlgebraStr ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = the Mult of V : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( Function-like quasi_total ) ( Relation-like [:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) , the carrier of V : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined the carrier of V : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) , the carrier of V : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) | [:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) , the carrier of it : ( ( ) ( ) VectSpStr over V : ( ( ) ( ) Normed_Complex_AlgebraStr ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like [:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) , the carrier of V : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined the carrier of V : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) -valued Function-like ) Element of bool [:[:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) , the carrier of V : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) & 1. it : ( ( ) ( ) VectSpStr over V : ( ( ) ( ) Normed_Complex_AlgebraStr ) ) : ( ( ) ( ) Element of the carrier of it : ( ( ) ( ) VectSpStr over V : ( ( ) ( ) Normed_Complex_AlgebraStr ) ) : ( ( ) ( ) set ) ) = 1. V : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) Element of the carrier of V : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) ) & 0. it : ( ( ) ( ) VectSpStr over V : ( ( ) ( ) Normed_Complex_AlgebraStr ) ) : ( ( ) ( V49(it : ( ( ) ( ) VectSpStr over V : ( ( ) ( ) Normed_Complex_AlgebraStr ) ) ) ) Element of the carrier of it : ( ( ) ( ) VectSpStr over V : ( ( ) ( ) Normed_Complex_AlgebraStr ) ) : ( ( ) ( ) set ) ) = 0. V : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( V49(V : ( ( ) ( ) Normed_Complex_AlgebraStr ) ) ) Element of the carrier of V : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) ) );
end;

theorem :: CC0SP1:1
for X being ( ( non empty ) ( non empty ) set )
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra)
for V1 being ( ( non empty ) ( non empty ) Subset of )
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 total 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 total 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 MR being ( ( Function-like quasi_total ) ( non empty Relation-like [:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of [:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) ) st V1 : ( ( non empty ) ( non empty ) 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 associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) : ( ( ) ( V49(b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) ) right_complementable ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) : ( ( ) ( non empty ) set ) ) & d2 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) = 1. V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) : ( ( ) ( right_complementable ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) : ( ( ) ( 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 total quasi_total ) BinOp of b1 : ( ( non empty ) ( non empty ) set ) ) = the addF of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) : ( ( Function-like quasi_total ) ( non empty Relation-like [: the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of bool [:[: the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) || V1 : ( ( non empty ) ( non empty ) 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 total 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 commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) : ( ( Function-like quasi_total ) ( non empty Relation-like [: the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of bool [:[: the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) || V1 : ( ( non empty ) ( non empty ) Subset of ) : ( ( ) ( Relation-like Function-like ) set ) & MR : ( ( Function-like quasi_total ) ( non empty Relation-like [:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of [:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) 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 associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) : ( ( Function-like quasi_total ) ( non empty Relation-like [:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of bool [:[:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) | [:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ,V1 : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( Function-like ) ( Relation-like [:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [:[:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & V1 : ( ( non empty ) ( non empty ) Subset of ) is having-inverse holds
ComplexAlgebraStr(# 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 total 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 total quasi_total ) BinOp of b1 : ( ( non empty ) ( non empty ) set ) ) ,MR : ( ( Function-like quasi_total ) ( non empty Relation-like [:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of [:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) 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 ) ComplexAlgebraStr ) is ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexSubAlgebra of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) ) ;

registration
let V be ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) ;
cluster non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative strict vector-associative for ( ( ) ( ) ComplexSubAlgebra of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) ;
end;

definition
let V be ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) ;
let V1 be ( ( ) ( ) Subset of ) ;
attr V1 is Cadditively-linearly-closed means :: CC0SP1:def 2
( V1 : ( ( ) ( ) VectSpStr over V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) is add-closed & V1 : ( ( ) ( ) VectSpStr over V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) is having-inverse & ( for a being ( ( V11() ) ( V11() ) Complex)
for v being ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) st v : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) in V1 : ( ( ) ( ) VectSpStr over V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) holds
a : ( ( V11() ) ( V11() ) Complex) * v : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) : ( ( ) ( non empty ) set ) ) in V1 : ( ( ) ( ) VectSpStr over V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) ) );
end;

definition
let V be ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) ;
let V1 be ( ( ) ( ) Subset of ) ;
assume ( V1 : ( ( ) ( ) Subset of ) is Cadditively-linearly-closed & not V1 : ( ( ) ( ) Subset of ) is empty ) ;
func Mult_ (V1,V) -> ( ( Function-like quasi_total ) ( Relation-like [:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ,V1 : ( ( ) ( ) VectSpStr over V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) :] : ( ( ) ( ) set ) -defined V1 : ( ( ) ( ) VectSpStr over V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) -valued Function-like quasi_total ) Function of [:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ,V1 : ( ( ) ( ) VectSpStr over V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) :] : ( ( ) ( ) set ) ,V1 : ( ( ) ( ) VectSpStr over V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) ) equals :: CC0SP1:def 3
 the Mult of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) : ( ( Function-like quasi_total ) ( non empty Relation-like [:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of bool [:[:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) | [:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ,V1 : ( ( ) ( ) VectSpStr over V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) :] : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like [:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [:[:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

definition
let X be ( ( non empty ) ( non empty ) set ) ;
func ComplexBoundedFunctions X -> ( ( non empty ) ( non empty ) Subset of ) equals :: CC0SP1:def 4
 { f : ( ( Function-like quasi_total ) ( non empty Relation-like X : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of X : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) where f is ( ( Function-like quasi_total ) ( non empty Relation-like X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) : f : ( ( Function-like quasi_total ) ( non empty Relation-like X : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of X : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) | X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) : ( ( Function-like ) ( Relation-like X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like V139() ) Element of bool [:X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ,COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) :] : ( ( ) ( V139() ) set ) : ( ( ) ( non empty ) set ) ) is bounded } ;
end;

registration
let X be ( ( non empty ) ( non empty ) set ) ;
cluster CAlgebra X : ( ( non empty ) ( non empty ) set ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative strict vector-associative ) ComplexAlgebraStr ) -> scalar-unital strict ;
end;

registration
let X be ( ( non empty ) ( non empty ) set ) ;
cluster ComplexBoundedFunctions X : ( ( non empty ) ( non empty ) set ) : ( ( non empty ) ( non empty ) Subset of ) -> non empty multiplicatively-closed Cadditively-linearly-closed ;
end;

registration
let V be ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) ;
cluster non empty multiplicatively-closed Cadditively-linearly-closed for ( ( ) ( ) Element of bool the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

definition
let V be ( ( non empty ) ( non empty ) CLSStruct ) ;
attr V is scalar-mult-cancelable means :: CC0SP1:def 5
 for a being ( ( V11() ) ( V11() ) Complex)
for v being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( not a : ( ( V11() ) ( V11() ) Complex) * v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) : ( ( ) ( non empty ) set ) ) = 0. V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) : ( ( ) ( V49(V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) right_complementable ) Element of the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) : ( ( ) ( non empty ) set ) ) or a : ( ( V11() ) ( V11() ) Complex) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V101() ext-real non positive non negative V176() V177() V178() V179() V180() V181() V182() V187() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( non empty ) set ) ) ) or v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = 0. V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) : ( ( ) ( V49(V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) right_complementable ) Element of the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) : ( ( ) ( non empty ) set ) ) );
end;

theorem :: CC0SP1:2
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra)
for V1 being ( ( non empty multiplicatively-closed Cadditively-linearly-closed ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) holds ComplexAlgebraStr(# V1 : ( ( non empty multiplicatively-closed Cadditively-linearly-closed ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ,(mult_ (V1 : ( ( non empty multiplicatively-closed Cadditively-linearly-closed ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:b2 : ( ( non empty multiplicatively-closed Cadditively-linearly-closed ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ,b2 : ( ( non empty multiplicatively-closed Cadditively-linearly-closed ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined b2 : ( ( non empty multiplicatively-closed Cadditively-linearly-closed ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) -valued Function-like total quasi_total ) Element of bool [:[:b2 : ( ( non empty multiplicatively-closed Cadditively-linearly-closed ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ,b2 : ( ( non empty multiplicatively-closed Cadditively-linearly-closed ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) ,b2 : ( ( non empty multiplicatively-closed Cadditively-linearly-closed ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(Add_ (V1 : ( ( non empty multiplicatively-closed Cadditively-linearly-closed ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:b2 : ( ( non empty multiplicatively-closed Cadditively-linearly-closed ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ,b2 : ( ( non empty multiplicatively-closed Cadditively-linearly-closed ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined b2 : ( ( non empty multiplicatively-closed Cadditively-linearly-closed ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) -valued Function-like total quasi_total ) Element of bool [:[:b2 : ( ( non empty multiplicatively-closed Cadditively-linearly-closed ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ,b2 : ( ( non empty multiplicatively-closed Cadditively-linearly-closed ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) ,b2 : ( ( non empty multiplicatively-closed Cadditively-linearly-closed ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ (V1 : ( ( non empty multiplicatively-closed Cadditively-linearly-closed ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ,b2 : ( ( non empty multiplicatively-closed Cadditively-linearly-closed ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined b2 : ( ( non empty multiplicatively-closed Cadditively-linearly-closed ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) -valued Function-like total quasi_total ) Function of [:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ,b2 : ( ( non empty multiplicatively-closed Cadditively-linearly-closed ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) ,b2 : ( ( non empty multiplicatively-closed Cadditively-linearly-closed ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ) ,(One_ (V1 : ( ( non empty multiplicatively-closed Cadditively-linearly-closed ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) )) : ( ( ) ( ) Element of b2 : ( ( non empty multiplicatively-closed Cadditively-linearly-closed ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ) ,(Zero_ (V1 : ( ( non empty multiplicatively-closed Cadditively-linearly-closed ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) )) : ( ( ) ( ) Element of b2 : ( ( non empty multiplicatively-closed Cadditively-linearly-closed ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ) #) : ( ( strict ) ( strict ) ComplexAlgebraStr ) is ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexSubAlgebra of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) ) ;

theorem :: CC0SP1:3
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra)
for V1 being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexSubAlgebra of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) ) holds
( ( for v1, w1 being ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) )
for v, w being ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) st v1 : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) = v : ( ( V11() ) ( V11() ) Complex) & w1 : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) = w : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) holds
v1 : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) + w1 : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexSubAlgebra of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) ) : ( ( ) ( non empty ) set ) ) = v : ( ( V11() ) ( V11() ) Complex) + w : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) : ( ( ) ( non empty ) set ) ) ) & ( for v1, w1 being ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) )
for v, w being ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) st v1 : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) = v : ( ( V11() ) ( V11() ) Complex) & w1 : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) = w : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) holds
v1 : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) * w1 : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexSubAlgebra of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) ) : ( ( ) ( non empty ) set ) ) = v : ( ( V11() ) ( V11() ) Complex) * w : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) : ( ( ) ( non empty ) set ) ) ) & ( for v1 being ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) )
for v being ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) )
for a being ( ( V11() ) ( V11() ) Complex) st v1 : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) = v : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) holds
a : ( ( V11() ) ( V11() ) Complex) * v1 : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexSubAlgebra of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) ) : ( ( ) ( non empty ) set ) ) = a : ( ( V11() ) ( V11() ) Complex) * v : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) : ( ( ) ( non empty ) set ) ) ) & 1_ V1 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexSubAlgebra of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) ) : ( ( ) ( right_complementable ) Element of the carrier of b2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexSubAlgebra of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) ) : ( ( ) ( non empty ) set ) ) = 1_ V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) : ( ( ) ( non empty ) set ) ) & 0. V1 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexSubAlgebra of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) ) : ( ( ) ( V49(b2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexSubAlgebra of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) ) ) right_complementable ) Element of the carrier of b2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexSubAlgebra of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) ) : ( ( ) ( non empty ) set ) ) = 0. V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) : ( ( ) ( V49(b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) ) right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) : ( ( ) ( non empty ) set ) ) ) ;

definition
let X be ( ( non empty ) ( non empty ) set ) ;
func C_Algebra_of_BoundedFunctions X -> ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) equals :: CC0SP1:def 6
 ComplexAlgebraStr(# (ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(mult_ ((ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(CAlgebra X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( strict ) ( strict ) ComplexAlgebraStr ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:(ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like total quasi_total ) Element of bool [:[:(ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(Add_ ((ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(CAlgebra X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( strict ) ( strict ) ComplexAlgebraStr ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:(ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like total quasi_total ) Element of bool [:[:(ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ ((ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(CAlgebra X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( strict ) ( strict ) ComplexAlgebraStr ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ,(ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like total quasi_total ) Function of [:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ,(ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) : ( ( non empty ) ( non empty ) Subset of ) ) ,(One_ ((ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(CAlgebra X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( strict ) ( strict ) ComplexAlgebraStr ) )) : ( ( ) ( ) Element of ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) : ( ( non empty ) ( non empty ) Subset of ) ) ,(Zero_ ((ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(CAlgebra X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( strict ) ( strict ) ComplexAlgebraStr ) )) : ( ( ) ( ) Element of ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) : ( ( non empty ) ( non empty ) Subset of ) ) #) : ( ( strict ) ( strict ) ComplexAlgebraStr ) ;
end;

theorem :: CC0SP1:4
for X being ( ( non empty ) ( non empty ) set ) holds C_Algebra_of_BoundedFunctions X : ( ( non empty ) ( non empty ) set ) : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) is ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexSubAlgebra of CAlgebra X : ( ( non empty ) ( non empty ) set ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative scalar-unital strict vector-associative ) ComplexAlgebraStr ) ) ;

registration
let X be ( ( non empty ) ( non empty ) set ) ;
cluster C_Algebra_of_BoundedFunctions X : ( ( non empty ) ( non empty ) set ) : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) -> non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative scalar-unital vector-associative ;
end;

theorem :: CC0SP1:5
for X being ( ( non empty ) ( non empty ) set )
for F, G, H being ( ( ) ( right_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 COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of X : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = F : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) & g : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = G : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) & h : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = H : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( H : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) = F : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + G : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of (C_Algebra_of_BoundedFunctions b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative scalar-unital vector-associative ) ComplexAlgebra) : ( ( ) ( 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 COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = (f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) + (g : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) ) ;

theorem :: CC0SP1:6
for X being ( ( non empty ) ( non empty ) set )
for a being ( ( V11() ) ( V11() ) Complex)
for F, G being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) )
for f, g being ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of X : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = F : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) & g : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = G : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( G : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) = a : ( ( V11() ) ( V11() ) Complex) * F : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of (C_Algebra_of_BoundedFunctions b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative scalar-unital vector-associative ) ComplexAlgebra) : ( ( ) ( non empty ) set ) ) iff for x being ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) holds g : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = a : ( ( V11() ) ( V11() ) Complex) * (f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) ) ;

theorem :: CC0SP1:7
for X being ( ( non empty ) ( non empty ) set )
for F, G, H being ( ( ) ( right_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 COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of X : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = F : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) & g : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = G : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) & h : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = H : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( H : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) = F : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) * G : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of (C_Algebra_of_BoundedFunctions b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative scalar-unital vector-associative ) ComplexAlgebra) : ( ( ) ( 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 COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = (f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) * (g : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) ) ;

theorem :: CC0SP1:8
for X being ( ( non empty ) ( non empty ) set ) holds 0. (C_Algebra_of_BoundedFunctions X : ( ( non empty ) ( non empty ) set ) ) : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative scalar-unital vector-associative ) ComplexAlgebra) : ( ( ) ( V49( C_Algebra_of_BoundedFunctions b1 : ( ( non empty ) ( non empty ) set ) : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative scalar-unital vector-associative ) ComplexAlgebra) ) right_complementable ) Element of the carrier of (C_Algebra_of_BoundedFunctions b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative scalar-unital vector-associative ) ComplexAlgebra) : ( ( ) ( non empty ) set ) ) = X : ( ( non empty ) ( non empty ) set ) --> 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V101() ext-real non positive non negative V176() V177() V178() V179() V180() V181() V182() V187() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined RAT : ( ( ) ( non empty V30() V176() V177() V178() V179() V182() ) set ) -valued INT : ( ( ) ( non empty V30() V176() V177() V178() V179() V180() V182() ) set ) -valued NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like constant total quasi_total V139() V140() V141() V142() bounded_above bounded_below bounded ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty RAT : ( ( ) ( non empty V30() V176() V177() V178() V179() V182() ) set ) -valued INT : ( ( ) ( non empty V30() V176() V177() V178() V179() V180() V182() ) set ) -valued V139() V140() V141() V142() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: CC0SP1:9
for X being ( ( non empty ) ( non empty ) set ) holds 1_ (C_Algebra_of_BoundedFunctions X : ( ( non empty ) ( non empty ) set ) ) : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative scalar-unital vector-associative ) ComplexAlgebra) : ( ( ) ( right_complementable ) Element of the carrier of (C_Algebra_of_BoundedFunctions b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative scalar-unital vector-associative ) ComplexAlgebra) : ( ( ) ( non empty ) set ) ) = X : ( ( non empty ) ( non empty ) set ) --> 1r : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like constant total quasi_total V139() ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) :] : ( ( ) ( non empty V139() ) set ) : ( ( ) ( non empty ) set ) ) ;

definition
let X be ( ( non empty ) ( non empty ) set ) ;
let F be ( ( ) ( ) set ) ;
assume F : ( ( ) ( ) set ) in ComplexBoundedFunctions X : ( ( non empty ) ( non empty ) set ) : ( ( non empty ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ;
func modetrans (F,X) -> ( ( Function-like quasi_total ) ( non empty Relation-like X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) means :: CC0SP1:def 7
( it : ( ( Function-like quasi_total ) ( Relation-like [:X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ,X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) :] : ( ( ) ( ) set ) -defined X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) -valued Function-like quasi_total ) Element of bool [:[:X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ,X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) :] : ( ( ) ( ) set ) ,X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = F : ( ( ) ( ) set ) & it : ( ( Function-like quasi_total ) ( Relation-like [:X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ,X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) :] : ( ( ) ( ) set ) -defined X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) -valued Function-like quasi_total ) Element of bool [:[:X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ,X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) :] : ( ( ) ( ) set ) ,X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) | X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) : ( ( Function-like ) ( Relation-like X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like V139() ) Element of bool [:X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ,COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) :] : ( ( ) ( V139() ) set ) : ( ( ) ( non empty ) set ) ) is bounded );
end;

definition
let X be ( ( non empty ) ( non empty ) set ) ;
let f be ( ( Function-like quasi_total ) ( non empty Relation-like X : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of X : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) ;
func PreNorms f -> ( ( non empty ) ( non empty V176() V177() V178() ) Subset of ( ( ) ( non empty ) set ) ) equals :: CC0SP1:def 8
 { |.(f : ( ( ) ( ) set ) . x : ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) .| : ( ( ) ( V11() real ext-real non negative ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) ) where x is ( ( ) ( ) Element of X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : verum } ;
end;

theorem :: CC0SP1:10
for X being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of X : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) | X : ( ( non empty ) ( non empty ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like V139() ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) :] : ( ( ) ( non empty V139() ) set ) : ( ( ) ( non empty ) set ) ) is bounded holds
PreNorms f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) : ( ( non empty ) ( non empty V176() V177() V178() ) Subset of ( ( ) ( non empty ) set ) ) is bounded_above ;

theorem :: CC0SP1:11
for X being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of X : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) holds
( f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) | X : ( ( non empty ) ( non empty ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like V139() ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) :] : ( ( ) ( non empty V139() ) set ) : ( ( ) ( non empty ) set ) ) is bounded iff PreNorms f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) : ( ( non empty ) ( non empty V176() V177() V178() ) Subset of ( ( ) ( non empty ) set ) ) is bounded_above ) ;

definition
let X be ( ( non empty ) ( non empty ) set ) ;
func ComplexBoundedFunctionsNorm X -> ( ( Function-like quasi_total ) ( non empty Relation-like ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) : ( ( non empty ) ( non empty ) Subset of ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -valued Function-like total quasi_total V139() V140() V141() ) Function of ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) : ( ( non empty ) ( non empty ) Subset of ) , REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) ) means :: CC0SP1:def 9
 for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) : ( ( non empty ) ( non empty ) Subset of ) holds
it : ( ( ) ( ) set ) . x : ( ( ) ( ) set ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) ) = upper_bound (PreNorms (modetrans (x : ( ( ) ( ) set ) ,X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) ) : ( ( non empty ) ( non empty V176() V177() V178() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) ) ;
end;

theorem :: CC0SP1:12
for X being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of X : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) | X : ( ( non empty ) ( non empty ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like V139() ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) :] : ( ( ) ( non empty V139() ) set ) : ( ( ) ( non empty ) set ) ) is bounded holds
modetrans (f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) ,X : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) ;

theorem :: CC0SP1:13
for X being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of X : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) | X : ( ( non empty ) ( non empty ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like V139() ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) :] : ( ( ) ( non empty V139() ) set ) : ( ( ) ( non empty ) set ) ) is bounded holds
(ComplexBoundedFunctionsNorm X : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like ComplexBoundedFunctions b1 : ( ( non empty ) ( non empty ) set ) : ( ( non empty ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -valued Function-like total quasi_total V139() V140() V141() ) Function of ComplexBoundedFunctions b1 : ( ( non empty ) ( non empty ) set ) : ( ( non empty ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) , REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) ) . f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) ) = upper_bound (PreNorms f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) ) : ( ( non empty ) ( non empty V176() V177() V178() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) ) ;

definition
let X be ( ( non empty ) ( non empty ) set ) ;
func C_Normed_Algebra_of_BoundedFunctions X -> ( ( ) ( ) Normed_Complex_AlgebraStr ) equals :: CC0SP1:def 10
 Normed_Complex_AlgebraStr(# (ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(mult_ ((ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(CAlgebra X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( strict ) ( strict ) ComplexAlgebraStr ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:(ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like total quasi_total ) Element of bool [:[:(ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(Add_ ((ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(CAlgebra X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( strict ) ( strict ) ComplexAlgebraStr ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:(ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like total quasi_total ) Element of bool [:[:(ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ ((ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(CAlgebra X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( strict ) ( strict ) ComplexAlgebraStr ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ,(ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like total quasi_total ) Function of [:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ,(ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) : ( ( non empty ) ( non empty ) Subset of ) ) ,(One_ ((ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(CAlgebra X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( strict ) ( strict ) ComplexAlgebraStr ) )) : ( ( ) ( ) Element of ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) : ( ( non empty ) ( non empty ) Subset of ) ) ,(Zero_ ((ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(CAlgebra X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( strict ) ( strict ) ComplexAlgebraStr ) )) : ( ( ) ( ) Element of ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) : ( ( non empty ) ( non empty ) Subset of ) ) ,(ComplexBoundedFunctionsNorm X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) : ( ( non empty ) ( non empty ) Subset of ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -valued Function-like total quasi_total V139() V140() V141() ) Function of ComplexBoundedFunctions X : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebraStr ) : ( ( non empty ) ( non empty ) Subset of ) , REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) ) #) : ( ( strict ) ( strict ) Normed_Complex_AlgebraStr ) ;
end;

registration
let X be ( ( non empty ) ( non empty ) set ) ;
cluster C_Normed_Algebra_of_BoundedFunctions X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) Normed_Complex_AlgebraStr ) -> non empty ;
end;

registration
let X be ( ( non empty ) ( non empty ) set ) ;
cluster C_Normed_Algebra_of_BoundedFunctions X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Normed_Complex_AlgebraStr ) -> unital ;
end;

theorem :: CC0SP1:14
for W being ( ( ) ( ) Normed_Complex_AlgebraStr )
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) st ComplexAlgebraStr(# the carrier of W : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) , the multF of W : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of b1 : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined the carrier of b1 : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[: the carrier of b1 : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , the addF of W : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of b1 : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined the carrier of b1 : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[: the carrier of b1 : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , the Mult of W : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( Function-like quasi_total ) ( Relation-like [:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) , the carrier of b1 : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined the carrier of b1 : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) , the carrier of b1 : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , the OneF of W : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) Element of the carrier of b1 : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) ) , the ZeroF of W : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) Element of the carrier of b1 : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( strict ) ComplexAlgebraStr ) = V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) holds
W : ( ( ) ( ) Normed_Complex_AlgebraStr ) is ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) ;

theorem :: CC0SP1:15
for X being ( ( non empty ) ( non empty ) set ) holds C_Normed_Algebra_of_BoundedFunctions X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty unital ) Normed_Complex_AlgebraStr ) is ( ( non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ) ComplexAlgebra) ;

theorem :: CC0SP1:16
for X being ( ( non empty ) ( non empty ) set )
for F being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds (Mult_ ((ComplexBoundedFunctions X : ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ,(CAlgebra X : ( ( non empty ) ( non empty ) set ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative scalar-unital strict vector-associative ) ComplexAlgebraStr ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ,(ComplexBoundedFunctions b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined ComplexBoundedFunctions b1 : ( ( non empty ) ( non empty ) set ) : ( ( non empty ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) -valued Function-like total quasi_total ) Function of [:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ,(ComplexBoundedFunctions b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) , ComplexBoundedFunctions b1 : ( ( non empty ) ( non empty ) set ) : ( ( non empty ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ) . (1r : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) ,F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) = F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;

theorem :: CC0SP1:17
for X being ( ( non empty ) ( non empty ) set ) holds C_Normed_Algebra_of_BoundedFunctions X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty unital ) Normed_Complex_AlgebraStr ) is ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) ;

theorem :: CC0SP1:18
for X being ( ( non empty ) ( non empty ) set ) holds X : ( ( non empty ) ( non empty ) set ) --> 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V101() ext-real non positive non negative V176() V177() V178() V179() V180() V181() V182() V187() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined RAT : ( ( ) ( non empty V30() V176() V177() V178() V179() V182() ) set ) -valued INT : ( ( ) ( non empty V30() V176() V177() V178() V179() V180() V182() ) set ) -valued NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like constant total quasi_total V139() V140() V141() V142() bounded_above bounded_below bounded ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty RAT : ( ( ) ( non empty V30() V176() V177() V178() V179() V182() ) set ) -valued INT : ( ( ) ( non empty V30() V176() V177() V178() V179() V180() V182() ) set ) -valued V139() V140() V141() V142() ) set ) : ( ( ) ( non empty ) set ) ) = 0. (C_Normed_Algebra_of_BoundedFunctions X : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty unital ) Normed_Complex_AlgebraStr ) : ( ( ) ( V49( C_Normed_Algebra_of_BoundedFunctions b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty unital ) Normed_Complex_AlgebraStr ) ) ) Element of the carrier of (C_Normed_Algebra_of_BoundedFunctions b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty unital ) Normed_Complex_AlgebraStr ) : ( ( ) ( non empty ) set ) ) ;

theorem :: CC0SP1:19
for X being ( ( non empty ) ( non empty ) set )
for x being ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) )
for f being ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of X : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) )
for F being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) & f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) | X : ( ( non empty ) ( non empty ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like V139() ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) :] : ( ( ) ( non empty V139() ) set ) : ( ( ) ( non empty ) set ) ) is bounded holds
|.(f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) .| : ( ( ) ( V11() real ext-real non negative ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) ) <= ||.F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) ) ;

theorem :: CC0SP1:20
for X being ( ( non empty ) ( non empty ) set )
for F being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V101() ext-real non positive non negative V176() V177() V178() V179() V180() V181() V182() V187() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( non empty ) set ) ) ) <= ||.F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) ) ;

theorem :: CC0SP1:21
for X being ( ( non empty ) ( non empty ) set )
for F being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = 0. (C_Normed_Algebra_of_BoundedFunctions X : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty unital ) Normed_Complex_AlgebraStr ) : ( ( ) ( V49( C_Normed_Algebra_of_BoundedFunctions b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty unital ) Normed_Complex_AlgebraStr ) ) ) Element of the carrier of (C_Normed_Algebra_of_BoundedFunctions b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty unital ) Normed_Complex_AlgebraStr ) : ( ( ) ( non empty ) set ) ) holds
0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V101() ext-real non positive non negative V176() V177() V178() V179() V180() V181() V182() V187() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( non empty ) set ) ) ) = ||.F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) ) ;

theorem :: CC0SP1:22
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 COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of X : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) 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 COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) & g : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = G : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) & h : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) 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 (C_Normed_Algebra_of_BoundedFunctions b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty unital ) Normed_Complex_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 COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = (f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) + (g : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) ) ;

theorem :: CC0SP1:23
for X being ( ( non empty ) ( non empty ) set )
for a being ( ( V11() ) ( V11() ) Complex)
for f, g being ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of X : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) )
for F, G being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) & g : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = G : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds
( G : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = a : ( ( V11() ) ( V11() ) Complex) * F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (C_Normed_Algebra_of_BoundedFunctions b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty unital ) Normed_Complex_AlgebraStr ) : ( ( ) ( non empty ) set ) ) iff for x being ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) holds g : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = a : ( ( V11() ) ( V11() ) Complex) * (f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) ) ;

theorem :: CC0SP1:24
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 COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of X : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) 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 COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) & g : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = G : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) & h : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) 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 (C_Normed_Algebra_of_BoundedFunctions b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty unital ) Normed_Complex_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 COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = (f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) * (g : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) ) ;

theorem :: CC0SP1:25
for X being ( ( non empty ) ( non empty ) set )
for a being ( ( V11() ) ( V11() ) Complex)
for F, G being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds
( ( ||.F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V101() ext-real non positive non negative V176() V177() V178() V179() V180() V181() V182() V187() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( non empty ) set ) ) ) implies F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = 0. (C_Normed_Algebra_of_BoundedFunctions X : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty unital ) Normed_Complex_AlgebraStr ) : ( ( ) ( V49( C_Normed_Algebra_of_BoundedFunctions b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty unital ) Normed_Complex_AlgebraStr ) ) ) Element of the carrier of (C_Normed_Algebra_of_BoundedFunctions b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty unital ) Normed_Complex_AlgebraStr ) : ( ( ) ( non empty ) set ) ) ) & ( F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = 0. (C_Normed_Algebra_of_BoundedFunctions X : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty unital ) Normed_Complex_AlgebraStr ) : ( ( ) ( V49( C_Normed_Algebra_of_BoundedFunctions b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty unital ) Normed_Complex_AlgebraStr ) ) ) Element of the carrier of (C_Normed_Algebra_of_BoundedFunctions b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty unital ) Normed_Complex_AlgebraStr ) : ( ( ) ( non empty ) set ) ) implies ||.F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V101() ext-real non positive non negative V176() V177() V178() V179() V180() V181() V182() V187() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( non empty ) set ) ) ) ) & ||.(a : ( ( V11() ) ( V11() ) Complex) * F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of (C_Normed_Algebra_of_BoundedFunctions b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty unital ) Normed_Complex_AlgebraStr ) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) ) = |.a : ( ( V11() ) ( V11() ) Complex) .| : ( ( ) ( V11() real ext-real non negative ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) ) * ||.F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) ) & ||.(F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) + G : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of (C_Normed_Algebra_of_BoundedFunctions b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty unital ) Normed_Complex_AlgebraStr ) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) ) <= ||.F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) ) + ||.G : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) ) ) ;

registration
let X be ( ( non empty ) ( non empty ) set ) ;
cluster C_Normed_Algebra_of_BoundedFunctions X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty unital ) Normed_Complex_AlgebraStr ) -> right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ;
end;

theorem :: CC0SP1:26
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 COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of X : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) )
for F, G, H being ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = F : ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) & g : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = G : ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) & h : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = H : ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) holds
( H : ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) = F : ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) - G : ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of (C_Normed_Algebra_of_BoundedFunctions b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed unital discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) Normed_Complex_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 COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = (f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) - (g : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) ) ;

theorem :: CC0SP1:27
for X being ( ( non empty ) ( non empty ) set )
for seq being ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of (C_Normed_Algebra_of_BoundedFunctions b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed unital discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) Normed_Complex_AlgebraStr ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of ( ( ) ( non empty ) set ) ) st seq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of (C_Normed_Algebra_of_BoundedFunctions b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed unital discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) Normed_Complex_AlgebraStr ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of ( ( ) ( non empty ) set ) ) is CCauchy holds
seq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of (C_Normed_Algebra_of_BoundedFunctions b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed unital discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) Normed_Complex_AlgebraStr ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of ( ( ) ( non empty ) set ) ) is convergent ;

registration
let X be ( ( non empty ) ( non empty ) set ) ;
cluster C_Normed_Algebra_of_BoundedFunctions X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed unital discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) Normed_Complex_AlgebraStr ) -> complete ;
end;

theorem :: CC0SP1:28
for X being ( ( non empty ) ( non empty ) set ) holds C_Normed_Algebra_of_BoundedFunctions X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed unital discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like complete ) Normed_Complex_AlgebraStr ) is ( ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive right_unital discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like vector-associative Banach_Algebra-like ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital V112() left_unital discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like complete vector-associative Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like ) Complex_Banach_Algebra) ;