:: CC0SP2 semantic presentation

begin

definition
let X be ( ( ) ( ) TopStruct ) ;
let f be ( ( Function-like quasi_total ) ( Relation-like the carrier of X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) ;
attr f is continuous means :: CC0SP2:def 1
 for Y being ( ( ) ( V176() ) Subset of ( ( ) ( non empty ) set ) ) st Y : ( ( ) ( V176() ) Subset of ( ( ) ( non empty ) set ) ) is closed holds
f : ( ( ) ( ) VectSpStr over X : ( ( ) ( ) Normed_Complex_AlgebraStr ) ) " Y : ( ( ) ( V176() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of X : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) is closed ;
end;

definition
let X be ( ( ) ( ) 1-sorted ) ;
let y be ( ( complex ) ( complex ) number ) ;
func X --> y -> ( ( Function-like quasi_total ) ( Relation-like the carrier of X : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of X : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) equals :: CC0SP2:def 2
 the carrier of X : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) --> y : ( ( ) ( ) VectSpStr over X : ( ( ) ( ) Normed_Complex_AlgebraStr ) ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of X : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) -defined {y : ( ( ) ( ) VectSpStr over X : ( ( ) ( ) Normed_Complex_AlgebraStr ) ) } : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of bool [: the carrier of X : ( ( ) ( ) Normed_Complex_AlgebraStr ) : ( ( ) ( ) set ) ,{y : ( ( ) ( ) VectSpStr over X : ( ( ) ( ) Normed_Complex_AlgebraStr ) ) } : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: CC0SP2:1
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for y being ( ( complex ) ( complex ) number )
for f being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) --> y : ( ( complex ) ( complex ) number ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) holds
f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) is continuous ;

registration
let X be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let y be ( ( complex ) ( complex ) number ) ;
cluster X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) --> y : ( ( complex ) ( complex ) set ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) -> Function-like quasi_total continuous ;
end;

registration
let X be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
cluster non empty Relation-like the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() continuous for ( ( ) ( ) Element of bool [: the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) :] : ( ( ) ( non empty V139() ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: CC0SP2:2
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) holds
( f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) is continuous iff for Y being ( ( ) ( V176() ) Subset of ( ( ) ( non empty ) set ) ) st Y : ( ( ) ( V176() ) Subset of ( ( ) ( non empty ) set ) ) is open holds
f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) " Y : ( ( ) ( V176() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is open ) ;

theorem :: CC0SP2:3
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) holds
( f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) is continuous iff for x being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for V being ( ( ) ( V176() ) Subset of ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) in V : ( ( ) ( V176() ) Subset of ( ( ) ( non empty ) set ) ) & V : ( ( ) ( V176() ) Subset of ( ( ) ( non empty ) set ) ) is open holds
ex W being ( ( ) ( ) Subset of ) st
( x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( ) Subset of ) & W : ( ( ) ( ) Subset of ) is open & f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) .: W : ( ( ) ( ) Subset of ) : ( ( ) ( V176() ) Element of bool COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) : ( ( ) ( non empty ) set ) ) c= V : ( ( ) ( V176() ) Subset of ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: CC0SP2:4
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f, g being ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() continuous ) Function of the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) holds f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() continuous ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) + g : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() continuous ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined Function-like total V139() ) set ) is ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() continuous ) Function of the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) ;

theorem :: CC0SP2:5
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for a being ( ( complex ) ( complex ) number )
for f being ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() continuous ) Function of the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) holds a : ( ( complex ) ( complex ) number ) (#) f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() continuous ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) : ( ( Function-like ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Element of bool [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) :] : ( ( ) ( non empty V139() ) set ) : ( ( ) ( non empty ) set ) ) is ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() continuous ) Function of the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) ;

theorem :: CC0SP2:6
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f, g being ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() continuous ) Function of the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) holds f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() continuous ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) - g : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() continuous ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) : ( ( Function-like ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Element of bool [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) :] : ( ( ) ( non empty V139() ) set ) : ( ( ) ( non empty ) set ) ) is ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() continuous ) Function of the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) ;

theorem :: CC0SP2:7
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f, g being ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() continuous ) Function of the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) holds f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() continuous ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) (#) g : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() continuous ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) : ( ( Function-like ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Element of bool [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) :] : ( ( ) ( non empty V139() ) set ) : ( ( ) ( non empty ) set ) ) is ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() continuous ) Function of the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) ;

theorem :: CC0SP2:8
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() continuous ) Function of the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) holds
( |.f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() continuous ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) .| : ( ( Function-like ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) -valued Function-like total quasi_total V139() V140() V141() ) Element of bool [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) :] : ( ( ) ( non empty V139() V140() V141() ) set ) : ( ( ) ( non empty ) set ) ) is ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) -valued Function-like total quasi_total V139() V140() V141() ) Function of the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) ) & |.f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() continuous ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) .| : ( ( Function-like ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) -valued Function-like total quasi_total V139() V140() V141() ) Element of bool [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) :] : ( ( ) ( non empty V139() V140() V141() ) set ) : ( ( ) ( non empty ) set ) ) is continuous ) ;

definition
let X be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
func CContinuousFunctions X -> ( ( ) ( ) Subset of ) equals :: CC0SP2:def 3
 { f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() continuous ) Function of the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) where f is ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() continuous ) Function of the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) : verum } ;
end;

registration
let X be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
cluster CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( ) Subset of ) -> non empty ;
end;

registration
let X be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
cluster CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset of ) -> multiplicatively-closed Cadditively-linearly-closed ;
end;

definition
let X be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
func C_Algebra_of_ContinuousFunctions 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 :: CC0SP2:def 4
 ComplexAlgebraStr(# (CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ,(mult_ ((CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ,(CAlgebra the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( 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 [:(CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ,(CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) -valued Function-like total quasi_total ) Element of bool [:[:(CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ,(CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(Add_ ((CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ,(CAlgebra the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( 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 [:(CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ,(CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) -valued Function-like total quasi_total ) Element of bool [:[:(CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ,(CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ ((CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ,(CAlgebra the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( 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 ) ,(CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) -valued Function-like total quasi_total ) Element of bool [:[:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ,(CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(One_ ((CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ,(CAlgebra the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( 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 ) )) : ( ( ) ( ) Element of CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ) ,(Zero_ ((CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ,(CAlgebra the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( 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 ) )) : ( ( ) ( ) Element of CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ) #) : ( ( strict ) ( strict ) ComplexAlgebraStr ) ;
end;

theorem :: CC0SP2:9
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds C_Algebra_of_ContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( 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 the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( 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 TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
cluster C_Algebra_of_ContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( 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 strict vector-associative ;
end;

registration
let X be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
cluster C_Algebra_of_ContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( 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 strict 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 :: CC0SP2:10
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for F, G, H being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) )
for f, g, h being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = F : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & g : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = G : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & h : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = H : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( H : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) = F : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + G : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (C_Algebra_of_ContinuousFunctions b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( 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 strict vector-associative ) ComplexAlgebra) : ( ( ) ( non empty ) set ) ) iff for x being ( ( ) ( ) Element of the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) holds h : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = (f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) + (g : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) ) ;

theorem :: CC0SP2:11
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for F, G being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) )
for f, g being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) )
for a being ( ( complex ) ( complex ) Complex) st f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = F : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & g : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = G : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( G : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) = a : ( ( complex ) ( complex ) Complex) * F : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (C_Algebra_of_ContinuousFunctions b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( 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 strict vector-associative ) ComplexAlgebra) : ( ( ) ( non empty ) set ) ) iff for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds g : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = a : ( ( complex ) ( complex ) Complex) * (f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) : ( ( ) ( complex ) set ) ) ;

theorem :: CC0SP2:12
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for F, G, H being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) )
for f, g, h being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = F : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & g : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = G : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & h : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = H : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( H : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) = F : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) * G : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (C_Algebra_of_ContinuousFunctions b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( 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 strict vector-associative ) ComplexAlgebra) : ( ( ) ( non empty ) set ) ) iff for x being ( ( ) ( ) Element of the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) holds h : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = (f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) * (g : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) ) ;

theorem :: CC0SP2:13
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds 0. (C_Algebra_of_ContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( 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 strict vector-associative ) ComplexAlgebra) : ( ( ) ( zero ) Element of the carrier of (C_Algebra_of_ContinuousFunctions b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( 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 strict vector-associative ) ComplexAlgebra) : ( ( ) ( non empty ) set ) ) = X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) --> 0c : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V176() V177() V178() V179() V180() V181() V182() bounded_below V197() ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() continuous ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) ;

theorem :: CC0SP2:14
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds 1_ (C_Algebra_of_ContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( 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 strict vector-associative ) ComplexAlgebra) : ( ( ) ( ) Element of the carrier of (C_Algebra_of_ContinuousFunctions b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( 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 strict vector-associative ) ComplexAlgebra) : ( ( ) ( non empty ) set ) ) = X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) --> 1r : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() continuous ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) ;

theorem :: CC0SP2:15
for A 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 A1, A2 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 A : ( ( 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 the carrier of A1 : ( ( ) ( 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 ) c= the carrier of A2 : ( ( ) ( 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 ) holds
A1 : ( ( ) ( 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) ) 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 A2 : ( ( ) ( 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) ) ) ;

theorem :: CC0SP2:16
for X being ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) holds C_Algebra_of_ContinuousFunctions X : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( 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 strict 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 C_Algebra_of_BoundedFunctions the carrier of X : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( 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 ) ComplexAlgebraStr ) ) ;

definition
let X be ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) ;
func CContinuousFunctionsNorm X -> ( ( Function-like quasi_total ) ( non empty Relation-like CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) -valued Function-like total quasi_total V139() V140() V141() ) Function of CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) , REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) ) equals :: CC0SP2:def 5
(ComplexBoundedFunctionsNorm the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like ComplexBoundedFunctions the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) : ( ( non empty ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Element of bool the carrier of (CAlgebra the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( 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 ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) -valued Function-like total quasi_total V139() V140() V141() ) Element of bool [:(ComplexBoundedFunctions the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( non empty ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Element of bool the carrier of (CAlgebra the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( 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 ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) :] : ( ( ) ( non empty V139() V140() V141() ) set ) : ( ( ) ( non empty ) set ) ) | (CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) : ( ( Function-like ) ( Relation-like ComplexBoundedFunctions the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) : ( ( non empty ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Element of bool the carrier of (CAlgebra the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( 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 ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) -valued Function-like V139() V140() V141() ) Element of bool [:(ComplexBoundedFunctions the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( non empty ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Element of bool the carrier of (CAlgebra the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( 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 ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) :] : ( ( ) ( non empty V139() V140() V141() ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

definition
let X be ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) ;
func C_Normed_Algebra_of_ContinuousFunctions X -> ( ( ) ( ) Normed_Complex_AlgebraStr ) equals :: CC0SP2:def 6
 Normed_Complex_AlgebraStr(# (CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ,(mult_ ((CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ,(CAlgebra the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( 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 [:(CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ,(CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) -valued Function-like total quasi_total ) Element of bool [:[:(CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ,(CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(Add_ ((CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ,(CAlgebra the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( 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 [:(CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ,(CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) -valued Function-like total quasi_total ) Element of bool [:[:(CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ,(CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ ((CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ,(CAlgebra the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( 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 ) ,(CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) -valued Function-like total quasi_total ) Element of bool [:[:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ,(CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(One_ ((CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ,(CAlgebra the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( 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 ) )) : ( ( ) ( ) Element of CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ) ,(Zero_ ((CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ,(CAlgebra the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( 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 ) )) : ( ( ) ( ) Element of CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ) ,(CContinuousFunctionsNorm X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) -valued Function-like total quasi_total V139() V140() V141() ) Function of CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) , REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) ) #) : ( ( strict ) ( strict ) Normed_Complex_AlgebraStr ) ;
end;

registration
let X be ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) ;
cluster C_Normed_Algebra_of_ContinuousFunctions X : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopStruct ) : ( ( ) ( ) Normed_Complex_AlgebraStr ) -> non empty strict ;
end;

registration
let X be ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) ;
cluster C_Normed_Algebra_of_ContinuousFunctions X : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopStruct ) : ( ( ) ( non empty strict ) Normed_Complex_AlgebraStr ) -> unital ;
end;

theorem :: CC0SP2:17
for X being ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) holds C_Normed_Algebra_of_ContinuousFunctions X : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty unital strict ) 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) ;

registration
let X be ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) ;
cluster C_Normed_Algebra_of_ContinuousFunctions X : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopStruct ) : ( ( ) ( non empty unital strict ) Normed_Complex_AlgebraStr ) -> right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ;
end;

theorem :: CC0SP2:18
for X being ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace)
for F being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds (Mult_ ((CContinuousFunctions X : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ,(CAlgebra the carrier of X : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( 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 ) ,(CContinuousFunctions b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined CContinuousFunctions b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) -valued Function-like total quasi_total ) Element of bool [:[:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ,(CContinuousFunctions b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(CContinuousFunctions b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) ) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . (1r : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) ,F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) = F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;

registration
let X be ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) ;
cluster C_Normed_Algebra_of_ContinuousFunctions X : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopStruct ) : ( ( ) ( 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 strict ) Normed_Complex_AlgebraStr ) -> vector-distributive scalar-distributive scalar-associative scalar-unital ;
end;

theorem :: CC0SP2:19
for X being ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) holds C_Normed_Algebra_of_ContinuousFunctions X : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( 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 strict ) 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 :: CC0SP2:20
for X being ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) holds X : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) --> 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real V101() ext-real non positive non negative V176() V177() V178() V179() V180() V181() V182() V187() bounded_below V197() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V176() V177() V178() V179() V180() V181() V182() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() continuous ) Function of the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = 0. (C_Normed_Algebra_of_ContinuousFunctions X : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) ) : ( ( ) ( 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 strict ) Normed_Complex_AlgebraStr ) : ( ( ) ( zero ) Element of the carrier of (C_Normed_Algebra_of_ContinuousFunctions b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) ) : ( ( ) ( 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 strict ) Normed_Complex_AlgebraStr ) : ( ( ) ( non empty ) set ) ) ;

theorem :: CC0SP2:21
for X being ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace)
for F being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real V101() ext-real non positive non negative V176() V177() V178() V179() V180() V181() V182() V187() bounded_below V197() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V176() V177() V178() V179() V180() V181() V182() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) : ( ( ) ( non empty ) set ) ) ) <= ||.F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) ) ;

theorem :: CC0SP2:22
for X being ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace)
for f, g, h being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of X : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( 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 the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( 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 the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( 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 the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( 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_ContinuousFunctions b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) ) : ( ( ) ( 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 strict ) Normed_Complex_AlgebraStr ) : ( ( ) ( non empty ) set ) ) iff for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds h : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = (f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) + (g : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) ) ;

theorem :: CC0SP2:23
for a being ( ( complex ) ( complex ) Complex)
for X being ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace)
for f, g being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b2 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of X : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( 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 the carrier of b2 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b2 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( 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 the carrier of b2 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b2 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = G : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds
( G : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = a : ( ( complex ) ( complex ) Complex) * F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (C_Normed_Algebra_of_ContinuousFunctions b2 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) ) : ( ( ) ( 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 strict ) Normed_Complex_AlgebraStr ) : ( ( ) ( non empty ) set ) ) iff for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds g : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b2 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b2 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = a : ( ( complex ) ( complex ) Complex) * (f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b2 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b2 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) : ( ( ) ( complex ) set ) ) ;

theorem :: CC0SP2:24
for X being ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace)
for f, g, h being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of X : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( 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 the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( 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 the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( 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 the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( 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_ContinuousFunctions b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) ) : ( ( ) ( 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 strict ) Normed_Complex_AlgebraStr ) : ( ( ) ( non empty ) set ) ) iff for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds h : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = (f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) * (g : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) ) ;

theorem :: CC0SP2:25
for X being ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) holds ||.(0. (C_Normed_Algebra_of_ContinuousFunctions X : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) ) : ( ( ) ( 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 strict ) Normed_Complex_AlgebraStr ) ) : ( ( ) ( zero ) Element of the carrier of (C_Normed_Algebra_of_ContinuousFunctions b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) ) : ( ( ) ( 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 strict ) Normed_Complex_AlgebraStr ) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real V101() ext-real non positive non negative V176() V177() V178() V179() V180() V181() V182() V187() bounded_below V197() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V176() V177() V178() V179() V180() V181() V182() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: CC0SP2:26
for X being ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace)
for F being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st ||.F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real V101() ext-real non positive non negative V176() V177() V178() V179() V180() V181() V182() V187() bounded_below V197() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V176() V177() V178() V179() V180() V181() V182() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) : ( ( ) ( non empty ) set ) ) ) holds
F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = 0. (C_Normed_Algebra_of_ContinuousFunctions X : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) ) : ( ( ) ( 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 strict ) Normed_Complex_AlgebraStr ) : ( ( ) ( zero ) Element of the carrier of (C_Normed_Algebra_of_ContinuousFunctions b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) ) : ( ( ) ( 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 strict ) Normed_Complex_AlgebraStr ) : ( ( ) ( non empty ) set ) ) ;

theorem :: CC0SP2:27
for a being ( ( complex ) ( complex ) Complex)
for X being ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace)
for F being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds ||.(a : ( ( complex ) ( complex ) Complex) * F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of (C_Normed_Algebra_of_ContinuousFunctions b2 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) ) : ( ( ) ( 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 strict ) Normed_Complex_AlgebraStr ) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) ) = (abs a : ( ( complex ) ( complex ) Complex) ) : ( ( ) ( complex real ext-real non negative ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) ) * ||.F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) ) ;

theorem :: CC0SP2:28
for X being ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace)
for F, G being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds ||.(F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) + G : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of (C_Normed_Algebra_of_ContinuousFunctions b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) ) : ( ( ) ( 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 strict ) Normed_Complex_AlgebraStr ) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) ) <= ||.F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) ) + ||.G : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) ) ;

registration
let X be ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) ;
cluster C_Normed_Algebra_of_ContinuousFunctions X : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopStruct ) : ( ( ) ( 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 strict ) Normed_Complex_AlgebraStr ) -> discerning reflexive ComplexNormSpace-like ;
end;

theorem :: CC0SP2:29
for X being ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace)
for f, g, h being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of X : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( 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 the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( 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 the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( 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 the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( 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_ContinuousFunctions b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) ) : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like vector-associative strict ) Normed_Complex_AlgebraStr ) : ( ( ) ( non empty ) set ) ) iff for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds h : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) = (f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) - (g : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) ) ;

theorem :: CC0SP2:30
for X being ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like complete ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like complete ) ComplexBanachSpace)
for Y being ( ( ) ( ) Subset of )
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() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like complete ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like complete ) ComplexBanachSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of ( ( ) ( non empty ) set ) ) st Y : ( ( ) ( ) Subset of ) is closed & rng seq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V176() V177() V178() V179() V180() V181() V182() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like complete ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like complete ) ComplexBanachSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like complete ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like complete ) ComplexBanachSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) c= Y : ( ( ) ( ) Subset of ) & seq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V176() V177() V178() V179() V180() V181() V182() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like complete ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like complete ) ComplexBanachSpace) : ( ( ) ( 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() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like complete ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like complete ) ComplexBanachSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of ( ( ) ( non empty ) set ) ) is convergent & lim seq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V176() V177() V178() V179() V180() V181() V182() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like complete ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like complete ) ComplexBanachSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like complete ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like complete ) ComplexBanachSpace) : ( ( ) ( non empty ) set ) ) in Y : ( ( ) ( ) Subset of ) ) ;

theorem :: CC0SP2:31
for X being ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace)
for Y being ( ( ) ( ) Subset of ) st Y : ( ( ) ( ) Subset of ) = CContinuousFunctions X : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) holds
Y : ( ( ) ( ) Subset of ) is closed ;

theorem :: CC0SP2:32
for X being ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace)
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() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of (C_Normed_Algebra_of_ContinuousFunctions b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) ) : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like vector-associative strict ) 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() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of (C_Normed_Algebra_of_ContinuousFunctions b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) ) : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like vector-associative strict ) 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() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of (C_Normed_Algebra_of_ContinuousFunctions b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) ) : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like vector-associative strict ) 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 TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) ;
cluster C_Normed_Algebra_of_ContinuousFunctions X : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopStruct ) : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like vector-associative strict ) Normed_Complex_AlgebraStr ) -> complete ;
end;

registration
let X be ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopSpace) ;
cluster C_Normed_Algebra_of_ContinuousFunctions X : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like V300() compact ) TopStruct ) : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like complete vector-associative strict ) Normed_Complex_AlgebraStr ) -> Banach_Algebra-like ;
end;

theorem :: CC0SP2:33
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f, g being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) holds support (f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) + g : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined Function-like total V139() ) set ) : ( ( ) ( ) set ) c= (support f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) ) : ( ( ) ( ) set ) \/ (support g : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: CC0SP2:34
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for a being ( ( complex ) ( complex ) Complex)
for f being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) holds support (a : ( ( complex ) ( complex ) Complex) (#) f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) ) : ( ( Function-like ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Element of bool [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) :] : ( ( ) ( non empty V139() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) c= support f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) : ( ( ) ( ) set ) ;

theorem :: CC0SP2:35
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f, g being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) holds support (f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) (#) g : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) ) : ( ( Function-like ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Element of bool [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) :] : ( ( ) ( non empty V139() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) c= (support f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) ) : ( ( ) ( ) set ) \/ (support g : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

definition
let X be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
func CC_0_Functions X -> ( ( non empty ) ( non empty ) Subset of ) equals :: CC0SP2:def 7
 { f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) where f is ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) : ( f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) is continuous & ex Y being ( ( non empty ) ( non empty ) Subset of ) st
( Y : ( ( non empty ) ( non empty ) Subset of ) is compact & ( for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) = support f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() ) Function of the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) : ( ( ) ( ) set ) holds
Cl A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) ) ) } ;
end;

theorem :: CC0SP2:36
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( non empty ) ( non empty ) Subset of ) is ( ( non empty ) ( non empty ) Subset of ) ;

theorem :: CC0SP2:37
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for W being ( ( non empty ) ( non empty ) Subset of ) st W : ( ( non empty ) ( non empty ) Subset of ) = CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( non empty ) ( non empty ) Subset of ) holds
W : ( ( non empty ) ( non empty ) Subset of ) is Cadditively-linearly-closed ;

theorem :: CC0SP2:38
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( non empty ) ( non empty ) Subset of ) is add-closed ;

theorem :: CC0SP2:39
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( non empty ) ( non empty ) Subset of ) is linearly-closed ;

registration
let X be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
cluster CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( non empty ) ( non empty ) Subset of ) -> non empty linearly-closed ;
end;

theorem :: CC0SP2:40
for V being ( ( 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)
for V1 being ( ( ) ( ) Subset of ) st V1 : ( ( ) ( ) Subset of ) is linearly-closed & not V1 : ( ( ) ( ) Subset of ) is empty holds
CLSStruct(# V1 : ( ( ) ( ) Subset of ) ,(Zero_ (V1 : ( ( ) ( ) Subset of ) ,V : ( ( 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) )) : ( ( ) ( ) Element of b2 : ( ( ) ( ) Subset of ) ) ,(Add_ (V1 : ( ( ) ( ) Subset of ) ,V : ( ( 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) )) : ( ( Function-like quasi_total ) ( Relation-like [:b2 : ( ( ) ( ) Subset of ) ,b2 : ( ( ) ( ) Subset of ) :] : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) Subset of ) -valued Function-like quasi_total ) Element of bool [:[:b2 : ( ( ) ( ) Subset of ) ,b2 : ( ( ) ( ) Subset of ) :] : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) Subset of ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ (V1 : ( ( ) ( ) Subset of ) ,V : ( ( 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) )) : ( ( Function-like quasi_total ) ( Relation-like [:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ,b2 : ( ( ) ( ) Subset of ) :] : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) Subset of ) -valued Function-like quasi_total ) Element of bool [:[:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ,b2 : ( ( ) ( ) Subset of ) :] : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) Subset of ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) CLSStruct ) is ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of V : ( ( 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 :: CC0SP2:41
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds CLSStruct(# (CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) ,(Zero_ ((CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) ,(ComplexVectSpace the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( non empty strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) )) : ( ( ) ( ) Element of CC_0_Functions b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) ) ,(Add_ ((CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) ,(ComplexVectSpace the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( non empty strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:(CC_0_Functions b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) ,(CC_0_Functions b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined CC_0_Functions b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) -valued Function-like total quasi_total ) Element of bool [:[:(CC_0_Functions b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) ,(CC_0_Functions b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(CC_0_Functions b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ ((CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) ,(ComplexVectSpace the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( non empty strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ,(CC_0_Functions b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined CC_0_Functions b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) -valued Function-like total quasi_total ) Element of bool [:[:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ,(CC_0_Functions b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(CC_0_Functions b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) CLSStruct ) is ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of ComplexVectSpace the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( non empty strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) ) ;

definition
let X be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
func C_VectorSpace_of_C_0_Functions X -> ( ( 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) equals :: CC0SP2:def 8
 CLSStruct(# (CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) ,(Zero_ ((CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) ,(ComplexVectSpace the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( non empty strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) )) : ( ( ) ( ) Element of CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) ) ,(Add_ ((CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) ,(ComplexVectSpace the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( non empty strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:(CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) ,(CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) -valued Function-like total quasi_total ) Element of bool [:[:(CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) ,(CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ ((CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) ,(ComplexVectSpace the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( non empty strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ,(CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) -valued Function-like total quasi_total ) Element of bool [:[:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ,(CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) CLSStruct ) ;
end;

theorem :: CC0SP2:42
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) holds
x : ( ( ) ( ) set ) in ComplexBoundedFunctions the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( non empty ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Element of bool the carrier of (CAlgebra the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( 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 ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

definition
let X be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
func CC_0_FunctionsNorm X -> ( ( Function-like quasi_total ) ( non empty Relation-like CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) -valued Function-like total quasi_total V139() V140() V141() ) Function of CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) , REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) ) equals :: CC0SP2:def 9
(ComplexBoundedFunctionsNorm the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like ComplexBoundedFunctions the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) : ( ( non empty ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Element of bool the carrier of (CAlgebra the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( 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 ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) -valued Function-like total quasi_total V139() V140() V141() ) Element of bool [:(ComplexBoundedFunctions the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( non empty ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Element of bool the carrier of (CAlgebra the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( 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 ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) :] : ( ( ) ( non empty V139() V140() V141() ) set ) : ( ( ) ( non empty ) set ) ) | (CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) : ( ( Function-like ) ( Relation-like ComplexBoundedFunctions the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) : ( ( non empty ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Element of bool the carrier of (CAlgebra the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( 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 ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) -valued Function-like V139() V140() V141() ) Element of bool [:(ComplexBoundedFunctions the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( non empty ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Element of bool the carrier of (CAlgebra the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( 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 ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) :] : ( ( ) ( non empty V139() V140() V141() ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

definition
let X be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
func C_Normed_Space_of_C_0_Functions X -> ( ( ) ( ) CNORMSTR ) equals :: CC0SP2:def 10
 CNORMSTR(# (CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) ,(Zero_ ((CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) ,(ComplexVectSpace the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( non empty strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) )) : ( ( ) ( ) Element of CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) ) ,(Add_ ((CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) ,(ComplexVectSpace the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( non empty strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:(CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) ,(CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) -valued Function-like total quasi_total ) Element of bool [:[:(CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) ,(CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ ((CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) ,(ComplexVectSpace the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( non empty strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ,(CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) -valued Function-like total quasi_total ) Element of bool [:[:COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ,(CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(CC_0_FunctionsNorm X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) -valued Function-like total quasi_total V139() V140() V141() ) Function of CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) , REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) ) #) : ( ( strict ) ( strict ) CNORMSTR ) ;
end;

registration
let X be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
cluster C_Normed_Space_of_C_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( ) CNORMSTR ) -> non empty strict ;
end;

theorem :: CC0SP2:43
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in CC_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) holds
x : ( ( ) ( ) set ) in CContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty multiplicatively-closed Cadditively-linearly-closed ) Subset of ) ;

theorem :: CC0SP2:44
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds 0. (C_VectorSpace_of_C_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( 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) : ( ( ) ( zero ) Element of the carrier of (C_VectorSpace_of_C_0_Functions b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( 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) : ( ( ) ( non empty ) set ) ) = X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) --> 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real V101() ext-real non positive non negative V176() V177() V178() V179() V180() V181() V182() V187() bounded_below V197() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V176() V177() V178() V179() V180() V181() V182() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() continuous ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) ;

theorem :: CC0SP2:45
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds 0. (C_Normed_Space_of_C_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty strict ) CNORMSTR ) : ( ( ) ( zero ) Element of the carrier of (C_Normed_Space_of_C_0_Functions b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty strict ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) = X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) --> 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real V101() ext-real non positive non negative V176() V177() V178() V179() V180() V181() V182() V187() bounded_below V197() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V176() V177() V178() V179() V180() V181() V182() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) -valued Function-like total quasi_total V139() continuous ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V30() V176() V182() ) set ) ) ;

theorem :: CC0SP2:46
for a being ( ( complex ) ( complex ) Complex)
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for F, G being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds
( ( ||.F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real V101() ext-real non positive non negative V176() V177() V178() V179() V180() V181() V182() V187() bounded_below V197() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V176() V177() V178() V179() V180() V181() V182() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) : ( ( ) ( non empty ) set ) ) ) implies F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = 0. (C_Normed_Space_of_C_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty strict ) CNORMSTR ) : ( ( ) ( zero ) Element of the carrier of (C_Normed_Space_of_C_0_Functions b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty strict ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) ) & ( F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = 0. (C_Normed_Space_of_C_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty strict ) CNORMSTR ) : ( ( ) ( zero ) Element of the carrier of (C_Normed_Space_of_C_0_Functions b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty strict ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) implies ||.F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real V101() ext-real non positive non negative V176() V177() V178() V179() V180() V181() V182() V187() bounded_below V197() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V176() V177() V178() V179() V180() V181() V182() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) : ( ( ) ( non empty ) set ) ) ) ) & ||.(a : ( ( complex ) ( complex ) Complex) * F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of (C_Normed_Space_of_C_0_Functions b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty strict ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) ) = (abs a : ( ( complex ) ( complex ) Complex) ) : ( ( ) ( complex real ext-real non negative ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) ) * ||.F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) ) & ||.(F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) + G : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of (C_Normed_Space_of_C_0_Functions b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty strict ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) ) <= ||.F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) ) + ||.G : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() ) set ) ) ) ;

registration
let X be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
cluster C_Normed_Space_of_C_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty strict ) CNORMSTR ) -> right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ;
end;

theorem :: CC0SP2:47
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds C_Normed_Space_of_C_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital strict ComplexNormSpace-like ) CNORMSTR ) is ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) ;