:: C0SP2 semantic presentation

begin

definition
let X be ( ( ) ( ) 1-sorted ) ;
let y be ( ( real ) ( V11() real ext-real ) number ) ;
func X --> y -> ( ( Function-like quasi_total ) ( Relation-like the carrier of X : ( ( ) ( ) Normed_AlgebraStr ) : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( ) set ) ) equals :: C0SP2:def 1
 the carrier of X : ( ( ) ( ) Normed_AlgebraStr ) : ( ( ) ( ) set ) --> y : ( ( ) ( ) VectSpStr over X : ( ( ) ( ) Normed_AlgebraStr ) ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of X : ( ( ) ( ) Normed_AlgebraStr ) : ( ( ) ( ) set ) -defined {y : ( ( ) ( ) VectSpStr over X : ( ( ) ( ) Normed_AlgebraStr ) ) } : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of bool [: the carrier of X : ( ( ) ( ) Normed_AlgebraStr ) : ( ( ) ( ) set ) ,{y : ( ( ) ( ) VectSpStr over X : ( ( ) ( ) Normed_AlgebraStr ) ) } : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

registration
let X be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
let y be ( ( real ) ( V11() real ext-real ) number ) ;
cluster X : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) --> y : ( ( real ) ( V11() real ext-real ) set ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( ) set ) ) -> Function-like quasi_total continuous ;
end;

theorem :: C0SP2:1
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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) 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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) is continuous iff for x being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for V being ( ( ) ( V185() V186() V187() ) 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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) in V : ( ( ) ( V185() V186() V187() ) Subset of ( ( ) ( non empty ) set ) ) & V : ( ( ) ( V185() V186() V187() ) 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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) .: W : ( ( ) ( ) Subset of ) : ( ( ) ( V185() V186() V187() ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) c= V : ( ( ) ( V185() V186() V187() ) Subset of ( ( ) ( non empty ) set ) ) ) ) ;

definition
let X be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
func ContinuousFunctions X -> ( ( ) ( ) Subset of ) equals :: C0SP2:def 2
 { 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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() continuous ) RealMap of ( ( ) ( non empty ) set ) ) where f is ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() continuous ) RealMap of ( ( ) ( ) set ) ) : verum } ;
end;

registration
let X be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
cluster ContinuousFunctions 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 ContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset of ) -> multiplicatively-closed additively-linearly-closed ;
end;

definition
let X be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
func R_Algebra_of_ContinuousFunctions X -> ( ( ) ( ) AlgebraStr ) equals :: C0SP2:def 3
 AlgebraStr(# (ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) ,(mult_ ((ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) ,(RAlgebra the carrier of X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative ) AlgebraStr ) )) : ( ( Function-like quasi_total ) ( Relation-like [:(ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) ,(ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) :] : ( ( ) ( ) set ) -defined ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ) -valued Function-like quasi_total ) Element of bool [:[:(ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) ,(ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) :] : ( ( ) ( ) set ) ,(ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(Add_ ((ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) ,(RAlgebra the carrier of X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative ) AlgebraStr ) )) : ( ( Function-like quasi_total ) ( Relation-like [:(ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) ,(ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) :] : ( ( ) ( ) set ) -defined ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ) -valued Function-like quasi_total ) Element of bool [:[:(ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) ,(ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) :] : ( ( ) ( ) set ) ,(ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ ((ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) ,(RAlgebra the carrier of X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative ) AlgebraStr ) )) : ( ( Function-like quasi_total ) ( Relation-like [:REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ,(ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) :] : ( ( ) ( ) set ) -defined ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ) -valued Function-like quasi_total ) Element of bool [:[:REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ,(ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) :] : ( ( ) ( ) set ) ,(ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(One_ ((ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) ,(RAlgebra the carrier of X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative ) AlgebraStr ) )) : ( ( ) ( ) Element of ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ) ) ,(Zero_ ((ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) ,(RAlgebra the carrier of X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative ) AlgebraStr ) )) : ( ( ) ( ) Element of ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ) ) #) : ( ( strict ) ( strict ) AlgebraStr ) ;
end;

theorem :: C0SP2:2
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds R_Algebra_of_ContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) AlgebraStr ) is ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital vector-associative ) Subalgebra of RAlgebra 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 vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative ) AlgebraStr ) ) ;

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

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

theorem :: C0SP2:3
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for F, G, H being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) )
for f, g, h being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap 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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) = F : ( ( ) ( right_complementable ) 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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) = G : ( ( ) ( right_complementable ) 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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) = H : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( H : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) = F : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + G : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of (R_Algebra_of_ContinuousFunctions 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 unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative ) AlgebraStr ) : ( ( ) ( 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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) 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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) 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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) ) ;

theorem :: C0SP2:4
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for F, G, H being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) )
for f, g, h being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) )
for a being ( ( ) ( V11() real ext-real ) Real) 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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) = F : ( ( ) ( right_complementable ) 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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) = G : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( G : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) = a : ( ( ) ( V11() real ext-real ) Real) * F : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of (R_Algebra_of_ContinuousFunctions 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 unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative ) 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 b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) = a : ( ( ) ( V11() real ext-real ) Real) * (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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) ) ;

theorem :: C0SP2:5
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for F, G, H being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) )
for f, g, h being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap 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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) = F : ( ( ) ( right_complementable ) 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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) = G : ( ( ) ( right_complementable ) 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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) = H : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( H : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) = F : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) * G : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of (R_Algebra_of_ContinuousFunctions 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 unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative ) AlgebraStr ) : ( ( ) ( 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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) 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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) 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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) ) ;

theorem :: C0SP2:6
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds 0. (R_Algebra_of_ContinuousFunctions 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 unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative ) AlgebraStr ) : ( ( ) ( V49( R_Algebra_of_ContinuousFunctions 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 unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative ) AlgebraStr ) ) right_complementable ) Element of the carrier of (R_Algebra_of_ContinuousFunctions 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 unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative ) AlgebraStr ) : ( ( ) ( 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 V11() real ext-real non positive non negative V117() V185() V186() V187() V188() V189() V190() V191() V197() bounded_below V268() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) 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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() continuous ) RealMap of ( ( ) ( non empty ) set ) ) ;

theorem :: C0SP2:7
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds 1_ (R_Algebra_of_ContinuousFunctions 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 unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative ) AlgebraStr ) : ( ( ) ( right_complementable ) Element of the carrier of (R_Algebra_of_ContinuousFunctions 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 unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative ) AlgebraStr ) : ( ( ) ( non empty ) set ) ) = X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) --> 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V117() V185() V186() V187() V188() V189() V190() V197() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) 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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() continuous ) RealMap of ( ( ) ( non empty ) set ) ) ;

theorem :: C0SP2:8
for A being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative associative commutative right-distributive right_unital vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital vector-associative ) Algebra)
for A1, A2 being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital vector-associative ) Subalgebra of A : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative associative commutative right-distributive right_unital vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital vector-associative ) Algebra) ) st the carrier of A1 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital vector-associative ) Subalgebra of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative associative commutative right-distributive right_unital vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital vector-associative ) Algebra) ) : ( ( ) ( non empty ) set ) c= the carrier of A2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital vector-associative ) Subalgebra of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative associative commutative right-distributive right_unital vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital vector-associative ) Algebra) ) : ( ( ) ( non empty ) set ) holds
A1 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital vector-associative ) Subalgebra of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative associative commutative right-distributive right_unital vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital vector-associative ) Algebra) ) is ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital vector-associative ) Subalgebra of A2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital vector-associative ) Subalgebra of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative associative commutative right-distributive right_unital vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital vector-associative ) Algebra) ) ) ;

theorem :: C0SP2:9
for X being ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) holds R_Algebra_of_ContinuousFunctions X : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative ) AlgebraStr ) is ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital vector-associative ) Subalgebra of R_Algebra_of_BoundedFunctions the carrier of X : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative associative commutative right-distributive right_unital vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital vector-associative ) AlgebraStr ) ) ;

definition
let X be ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) ;
func ContinuousFunctionsNorm X -> ( ( Function-like quasi_total ) ( non empty Relation-like ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) Function of ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ) , REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) equals :: C0SP2:def 4
(BoundedFunctionsNorm the carrier of X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like BoundedFunctions the carrier of X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) Element of bool the carrier of (RAlgebra the carrier of X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative ) AlgebraStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) Element of bool [:(BoundedFunctions the carrier of X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty ) Element of bool the carrier of (RAlgebra the carrier of X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative ) AlgebraStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) :] : ( ( ) ( non empty V152() V153() V154() ) set ) : ( ( ) ( non empty ) set ) ) | (ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) : ( ( Function-like ) ( Relation-like BoundedFunctions the carrier of X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) Element of bool the carrier of (RAlgebra the carrier of X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative ) AlgebraStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like V152() V153() V154() ) Element of bool [:(BoundedFunctions the carrier of X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty ) Element of bool the carrier of (RAlgebra the carrier of X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative ) AlgebraStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) :] : ( ( ) ( non empty V152() V153() V154() ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

definition
let X be ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) ;
func R_Normed_Algebra_of_ContinuousFunctions X -> ( ( ) ( ) Normed_AlgebraStr ) equals :: C0SP2:def 5
 Normed_AlgebraStr(# (ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) ,(mult_ ((ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) ,(RAlgebra the carrier of X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative ) AlgebraStr ) )) : ( ( Function-like quasi_total ) ( Relation-like [:(ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) ,(ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) :] : ( ( ) ( ) set ) -defined ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ) -valued Function-like quasi_total ) Element of bool [:[:(ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) ,(ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) :] : ( ( ) ( ) set ) ,(ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(Add_ ((ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) ,(RAlgebra the carrier of X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative ) AlgebraStr ) )) : ( ( Function-like quasi_total ) ( Relation-like [:(ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) ,(ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) :] : ( ( ) ( ) set ) -defined ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ) -valued Function-like quasi_total ) Element of bool [:[:(ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) ,(ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) :] : ( ( ) ( ) set ) ,(ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ ((ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) ,(RAlgebra the carrier of X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative ) AlgebraStr ) )) : ( ( Function-like quasi_total ) ( Relation-like [:REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ,(ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) :] : ( ( ) ( ) set ) -defined ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ) -valued Function-like quasi_total ) Element of bool [:[:REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ,(ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) :] : ( ( ) ( ) set ) ,(ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(One_ ((ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) ,(RAlgebra the carrier of X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative ) AlgebraStr ) )) : ( ( ) ( ) Element of ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ) ) ,(Zero_ ((ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) ,(RAlgebra the carrier of X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative ) AlgebraStr ) )) : ( ( ) ( ) Element of ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ) ) ,(ContinuousFunctionsNorm X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) Function of ContinuousFunctions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ) , REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) #) : ( ( strict ) ( strict ) Normed_AlgebraStr ) ;
end;

registration
let X be ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) ;
cluster R_Normed_Algebra_of_ContinuousFunctions X : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopStruct ) : ( ( ) ( ) Normed_AlgebraStr ) -> non empty strict ;
end;

registration
let X be ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) ;
cluster R_Normed_Algebra_of_ContinuousFunctions X : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopStruct ) : ( ( ) ( non empty strict ) Normed_AlgebraStr ) -> unital ;
end;

theorem :: C0SP2:10
for W being ( ( ) ( ) Normed_AlgebraStr )
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative associative commutative right-distributive right_unital vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital vector-associative ) Algebra) st AlgebraStr(# the carrier of W : ( ( ) ( ) Normed_AlgebraStr ) : ( ( ) ( ) set ) , the multF of W : ( ( ) ( ) Normed_AlgebraStr ) : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of b1 : ( ( ) ( ) Normed_AlgebraStr ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( ) ( ) Normed_AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined the carrier of b1 : ( ( ) ( ) Normed_AlgebraStr ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[: the carrier of b1 : ( ( ) ( ) Normed_AlgebraStr ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( ) ( ) Normed_AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( ) ( ) Normed_AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , the addF of W : ( ( ) ( ) Normed_AlgebraStr ) : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of b1 : ( ( ) ( ) Normed_AlgebraStr ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( ) ( ) Normed_AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined the carrier of b1 : ( ( ) ( ) Normed_AlgebraStr ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[: the carrier of b1 : ( ( ) ( ) Normed_AlgebraStr ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( ) ( ) Normed_AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( ) ( ) Normed_AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , the Mult of W : ( ( ) ( ) Normed_AlgebraStr ) : ( ( Function-like quasi_total ) ( Relation-like [:REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) , the carrier of b1 : ( ( ) ( ) Normed_AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined the carrier of b1 : ( ( ) ( ) Normed_AlgebraStr ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[:REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) , the carrier of b1 : ( ( ) ( ) Normed_AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( ) ( ) Normed_AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , the OneF of W : ( ( ) ( ) Normed_AlgebraStr ) : ( ( ) ( ) Element of the carrier of b1 : ( ( ) ( ) Normed_AlgebraStr ) : ( ( ) ( ) set ) ) , the ZeroF of W : ( ( ) ( ) Normed_AlgebraStr ) : ( ( ) ( ) Element of the carrier of b1 : ( ( ) ( ) Normed_AlgebraStr ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( strict ) AlgebraStr ) = V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative associative commutative right-distributive right_unital vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital vector-associative ) Algebra) holds
W : ( ( ) ( ) Normed_AlgebraStr ) is ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative associative commutative right-distributive right_unital vector-associative ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital vector-associative ) Algebra) ;

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

theorem :: C0SP2:11
for X being ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace)
for F being ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) holds (Mult_ ((ContinuousFunctions X : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) ) : ( ( ) ( non empty add-closed having-inverse additively-closed multiplicatively-closed additively-linearly-closed ) Subset of ) ,(RAlgebra the carrier of X : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative ) AlgebraStr ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ,(ContinuousFunctions b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) ) : ( ( ) ( non empty add-closed having-inverse additively-closed multiplicatively-closed additively-linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined ContinuousFunctions b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) : ( ( ) ( non empty add-closed having-inverse additively-closed multiplicatively-closed additively-linearly-closed ) Subset of ) -valued Function-like total quasi_total ) Element of bool [:[:REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ,(ContinuousFunctions b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) ) : ( ( ) ( non empty add-closed having-inverse additively-closed multiplicatively-closed additively-linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(ContinuousFunctions b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) ) : ( ( ) ( non empty add-closed having-inverse additively-closed multiplicatively-closed additively-linearly-closed ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . (1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V117() V185() V186() V187() V188() V189() V190() V197() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ,F : ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) = F : ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) ;

registration
let X be ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) ;
cluster R_Normed_Algebra_of_ContinuousFunctions X : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopStruct ) : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital vector-associative strict ) Normed_AlgebraStr ) -> vector-distributive scalar-distributive scalar-associative scalar-unital ;
end;

theorem :: C0SP2:12
for X being ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) holds X : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) --> 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V117() V185() V186() V187() V188() V189() V190() V191() V197() bounded_below V268() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) 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 pseudocompact compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() V206( the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) : ( ( ) ( non empty ) set ) ) V207( the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous bounded ) RealMap of ( ( ) ( non empty ) set ) ) = 0. (R_Normed_Algebra_of_ContinuousFunctions X : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) ) : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital unital associative commutative right-distributive right_unital well-unital left_unital vector-associative strict ) Normed_AlgebraStr ) : ( ( ) ( V49( R_Normed_Algebra_of_ContinuousFunctions b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital unital associative commutative right-distributive right_unital well-unital left_unital vector-associative strict ) Normed_AlgebraStr ) ) right_complementable ) Element of the carrier of (R_Normed_Algebra_of_ContinuousFunctions b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) ) : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital unital associative commutative right-distributive right_unital well-unital left_unital vector-associative strict ) Normed_AlgebraStr ) : ( ( ) ( non empty ) set ) ) ;

theorem :: C0SP2:13
for X being ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace)
for F being ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) holds 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V117() V185() V186() V187() V188() V189() V190() V191() V197() bounded_below V268() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) <= ||.F : ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) ;

theorem :: C0SP2:14
for X being ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace)
for F being ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) st F : ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) = 0. (R_Normed_Algebra_of_ContinuousFunctions X : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) ) : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital unital associative commutative right-distributive right_unital well-unital left_unital vector-associative strict ) Normed_AlgebraStr ) : ( ( ) ( V49( R_Normed_Algebra_of_ContinuousFunctions b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital unital associative commutative right-distributive right_unital well-unital left_unital vector-associative strict ) Normed_AlgebraStr ) ) right_complementable ) Element of the carrier of (R_Normed_Algebra_of_ContinuousFunctions b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) ) : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital unital associative commutative right-distributive right_unital well-unital left_unital vector-associative strict ) Normed_AlgebraStr ) : ( ( ) ( non empty ) set ) ) holds
0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V117() V185() V186() V187() V188() V189() V190() V191() V197() bounded_below V268() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) = ||.F : ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) ;

theorem :: C0SP2:15
for X being ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace)
for F, G, H being ( ( ) ( right_complementable ) Point 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 compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap 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 pseudocompact compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) = F : ( ( ) ( right_complementable ) 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 pseudocompact compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) = G : ( ( ) ( right_complementable ) 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 pseudocompact compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) = H : ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) holds
( H : ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) = F : ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) + G : ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of (R_Normed_Algebra_of_ContinuousFunctions b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) ) : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital unital associative commutative right-distributive right_unital well-unital left_unital vector-associative strict ) Normed_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 pseudocompact compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) = (f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) + (g : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) ) ;

theorem :: C0SP2:16
for a being ( ( ) ( V11() real ext-real ) Real)
for X being ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace)
for F, G being ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) )
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 pseudocompact compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap 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 pseudocompact compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) = F : ( ( ) ( right_complementable ) 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 pseudocompact compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) = G : ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) holds
( G : ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) = a : ( ( ) ( V11() real ext-real ) Real) * F : ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of (R_Normed_Algebra_of_ContinuousFunctions b2 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) ) : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital unital associative commutative right-distributive right_unital well-unital left_unital vector-associative strict ) Normed_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 pseudocompact compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) = a : ( ( ) ( V11() real ext-real ) Real) * (f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b2 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) ) ;

theorem :: C0SP2:17
for X being ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace)
for F, G, H being ( ( ) ( right_complementable ) Point 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 compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap 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 pseudocompact compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) = F : ( ( ) ( right_complementable ) 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 pseudocompact compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) = G : ( ( ) ( right_complementable ) 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 pseudocompact compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) = H : ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) holds
( H : ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) = F : ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) * G : ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of (R_Normed_Algebra_of_ContinuousFunctions b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) ) : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital unital associative commutative right-distributive right_unital well-unital left_unital vector-associative strict ) Normed_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 pseudocompact compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) = (f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) * (g : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) ) ;

theorem :: C0SP2:18
for a being ( ( ) ( V11() real ext-real ) Real)
for X being ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace)
for F, G being ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) holds
( ( ||.F : ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V117() V185() V186() V187() V188() V189() V190() V191() V197() bounded_below V268() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) implies F : ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) = 0. (R_Normed_Algebra_of_ContinuousFunctions X : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) ) : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital unital associative commutative right-distributive right_unital well-unital left_unital vector-associative strict ) Normed_AlgebraStr ) : ( ( ) ( V49( R_Normed_Algebra_of_ContinuousFunctions b2 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital unital associative commutative right-distributive right_unital well-unital left_unital vector-associative strict ) Normed_AlgebraStr ) ) right_complementable ) Element of the carrier of (R_Normed_Algebra_of_ContinuousFunctions b2 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) ) : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital unital associative commutative right-distributive right_unital well-unital left_unital vector-associative strict ) Normed_AlgebraStr ) : ( ( ) ( non empty ) set ) ) ) & ( F : ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) = 0. (R_Normed_Algebra_of_ContinuousFunctions X : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) ) : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital unital associative commutative right-distributive right_unital well-unital left_unital vector-associative strict ) Normed_AlgebraStr ) : ( ( ) ( V49( R_Normed_Algebra_of_ContinuousFunctions b2 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital unital associative commutative right-distributive right_unital well-unital left_unital vector-associative strict ) Normed_AlgebraStr ) ) right_complementable ) Element of the carrier of (R_Normed_Algebra_of_ContinuousFunctions b2 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) ) : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital unital associative commutative right-distributive right_unital well-unital left_unital vector-associative strict ) Normed_AlgebraStr ) : ( ( ) ( non empty ) set ) ) implies ||.F : ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V117() V185() V186() V187() V188() V189() V190() V191() V197() bounded_below V268() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) & ||.(a : ( ( ) ( V11() real ext-real ) Real) * F : ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of (R_Normed_Algebra_of_ContinuousFunctions b2 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) ) : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital unital associative commutative right-distributive right_unital well-unital left_unital vector-associative strict ) Normed_AlgebraStr ) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) = (abs a : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) * ||.F : ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) & ||.(F : ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) + G : ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of (R_Normed_Algebra_of_ContinuousFunctions b2 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) ) : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital unital associative commutative right-distributive right_unital well-unital left_unital vector-associative strict ) Normed_AlgebraStr ) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) <= ||.F : ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) + ||.G : ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) ) ;

registration
let X be ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) ;
cluster R_Normed_Algebra_of_ContinuousFunctions X : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopStruct ) : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital unital associative commutative right-distributive right_unital well-unital left_unital vector-associative strict ) Normed_AlgebraStr ) -> discerning reflexive RealNormSpace-like ;
end;

theorem :: C0SP2:19
for X being ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace)
for F, G, H being ( ( ) ( right_complementable ) Point 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 compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap 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 pseudocompact compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) = F : ( ( ) ( right_complementable ) 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 pseudocompact compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) = G : ( ( ) ( right_complementable ) 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 pseudocompact compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) = H : ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) holds
( H : ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) = F : ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) - G : ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of (R_Normed_Algebra_of_ContinuousFunctions b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) ) : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like unital associative commutative right-distributive right_unital well-unital left_unital vector-associative strict ) Normed_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 pseudocompact compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) = (f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) - (g : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) ) ;

theorem :: C0SP2:20
for X being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like complete ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like complete ) RealBanachSpace)
for Y being ( ( ) ( ) Subset of )
for seq being ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like complete ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( 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 V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like complete ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like complete ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( 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 V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like complete ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of ( ( ) ( non empty ) set ) ) is Cauchy_sequence_by_Norm holds
( seq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like complete ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( 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 V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like complete ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like complete ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) ) in Y : ( ( ) ( ) Subset of ) ) ;

theorem :: C0SP2:21
for X being ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace)
for Y being ( ( ) ( ) Subset of ) st Y : ( ( ) ( ) Subset of ) = ContinuousFunctions X : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) : ( ( ) ( non empty add-closed having-inverse additively-closed multiplicatively-closed additively-linearly-closed ) Subset of ) holds
Y : ( ( ) ( ) Subset of ) is closed ;

theorem :: C0SP2:22
for X being ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace)
for seq being ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of (R_Normed_Algebra_of_ContinuousFunctions b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) ) : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like unital associative commutative right-distributive right_unital well-unital left_unital vector-associative strict ) Normed_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 V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of (R_Normed_Algebra_of_ContinuousFunctions b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) ) : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like unital associative commutative right-distributive right_unital well-unital left_unital vector-associative strict ) Normed_AlgebraStr ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of ( ( ) ( non empty ) set ) ) is Cauchy_sequence_by_Norm holds
seq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of (R_Normed_Algebra_of_ContinuousFunctions b1 : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopSpace) ) : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like unital associative commutative right-distributive right_unital well-unital left_unital vector-associative strict ) Normed_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 pseudocompact compact ) TopSpace) ;
cluster R_Normed_Algebra_of_ContinuousFunctions X : ( ( non empty TopSpace-like compact ) ( non empty TopSpace-like pseudocompact compact ) TopStruct ) : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like unital associative commutative right-distributive right_unital well-unital left_unital vector-associative strict ) Normed_AlgebraStr ) -> complete ;
end;

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

begin

theorem :: C0SP2:23
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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) 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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap 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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) 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() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) Element of bool [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) :] : ( ( ) ( non empty V152() V153() V154() ) 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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) 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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: C0SP2:24
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for a being ( ( ) ( V11() real ext-real ) Real)
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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) holds support (a : ( ( ) ( V11() real ext-real ) Real) (#) 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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) 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() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) Element of bool [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) :] : ( ( ) ( non empty V152() V153() V154() ) 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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ;

theorem :: C0SP2:25
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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) 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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap 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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) 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() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) Element of bool [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) :] : ( ( ) ( non empty V152() V153() V154() ) 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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) 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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

begin

definition
let X be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
func C_0_Functions X -> ( ( non empty ) ( non empty ) Subset of ) equals :: C0SP2:def 6
 { 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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) where f is ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( ) 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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) 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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) RealMap of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) holds
Cl A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) is ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) ) ) } ;
end;

theorem :: C0SP2:26
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds C_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 :: C0SP2:27
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 ) = C_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 additively-linearly-closed ;

theorem :: C0SP2:28
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds C_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 C_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( non empty ) ( non empty ) Subset of ) -> non empty linearly-closed ;
end;

definition
let X be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
func R_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 ) RealLinearSpace) equals :: C0SP2:def 7
 RLSStruct(# (C_0_Functions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(Zero_ ((C_0_Functions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(RealVectSpace the carrier of X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) )) : ( ( ) ( ) Element of C_0_Functions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) Subset of ) ) ,(Add_ ((C_0_Functions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(RealVectSpace the carrier of X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:(C_0_Functions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(C_0_Functions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined C_0_Functions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like total quasi_total ) Element of bool [:[:(C_0_Functions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(C_0_Functions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(C_0_Functions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ ((C_0_Functions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(RealVectSpace the carrier of X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ,(C_0_Functions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined C_0_Functions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like total quasi_total ) Element of bool [:[:REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ,(C_0_Functions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(C_0_Functions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RLSStruct ) ;
end;

theorem :: C0SP2:29
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds R_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 ) RealLinearSpace) is ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of RealVectSpace the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ) ;

theorem :: C0SP2:30
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in C_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) holds
x : ( ( ) ( ) set ) in BoundedFunctions the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( non empty ) ( non empty add-closed having-inverse additively-closed multiplicatively-closed additively-linearly-closed ) Element of bool the carrier of (RAlgebra 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 vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative ) AlgebraStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

definition
let X be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
func C_0_FunctionsNorm X -> ( ( Function-like quasi_total ) ( non empty Relation-like C_0_Functions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) Subset of ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) Function of C_0_Functions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) Subset of ) , REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) equals :: C0SP2:def 8
(BoundedFunctionsNorm the carrier of X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like BoundedFunctions the carrier of X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) Element of bool the carrier of (RAlgebra the carrier of X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative ) AlgebraStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) Element of bool [:(BoundedFunctions the carrier of X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty ) Element of bool the carrier of (RAlgebra the carrier of X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative ) AlgebraStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) :] : ( ( ) ( non empty V152() V153() V154() ) set ) : ( ( ) ( non empty ) set ) ) | (C_0_Functions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) Subset of ) : ( ( Function-like ) ( Relation-like BoundedFunctions the carrier of X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) Element of bool the carrier of (RAlgebra the carrier of X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative ) AlgebraStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like V152() V153() V154() ) Element of bool [:(BoundedFunctions the carrier of X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty ) Element of bool the carrier of (RAlgebra the carrier of X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital well-unital left_unital strict vector-associative ) AlgebraStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) :] : ( ( ) ( non empty V152() V153() V154() ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

definition
let X be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
func R_Normed_Space_of_C_0_Functions X -> ( ( non empty ) ( non empty ) NORMSTR ) equals :: C0SP2:def 9
 NORMSTR(# (C_0_Functions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(Zero_ ((C_0_Functions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(RealVectSpace the carrier of X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) )) : ( ( ) ( ) Element of C_0_Functions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) Subset of ) ) ,(Add_ ((C_0_Functions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(RealVectSpace the carrier of X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:(C_0_Functions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(C_0_Functions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined C_0_Functions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like total quasi_total ) Element of bool [:[:(C_0_Functions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(C_0_Functions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(C_0_Functions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ ((C_0_Functions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(RealVectSpace the carrier of X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ,(C_0_Functions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined C_0_Functions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like total quasi_total ) Element of bool [:[:REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ,(C_0_Functions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(C_0_Functions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(C_0_FunctionsNorm X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like C_0_Functions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) Subset of ) -defined REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() ) Function of C_0_Functions X : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V117() V185() V186() V187() V188() V189() V190() V197() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) Subset of ) , REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) #) : ( ( strict ) ( strict ) NORMSTR ) ;
end;

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

theorem :: C0SP2:31
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in C_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( non empty ) ( non empty linearly-closed ) Subset of ) holds
x : ( ( ) ( ) set ) in ContinuousFunctions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty add-closed having-inverse additively-closed multiplicatively-closed additively-linearly-closed ) Subset of ) ;

theorem :: C0SP2:32
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds 0. (R_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 ) RealLinearSpace) : ( ( ) ( V49( R_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 ) RealLinearSpace) ) right_complementable ) Element of the carrier of (R_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 ) RealLinearSpace) : ( ( ) ( 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 V11() real ext-real non positive non negative V117() V185() V186() V187() V188() V189() V190() V191() V197() bounded_below V268() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) 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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() continuous ) RealMap of ( ( ) ( non empty ) set ) ) ;

theorem :: C0SP2:33
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds 0. (R_Normed_Space_of_C_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( non empty ) ( non empty strict ) NORMSTR ) : ( ( ) ( V49( R_Normed_Space_of_C_0_Functions b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( non empty ) ( non empty strict ) NORMSTR ) ) ) Element of the carrier of (R_Normed_Space_of_C_0_Functions b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( non empty ) ( non empty strict ) NORMSTR ) : ( ( ) ( 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 V11() real ext-real non positive non negative V117() V185() V186() V187() V188() V189() V190() V191() V197() bounded_below V268() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) 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 REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) -valued Function-like total quasi_total V152() V153() V154() continuous ) RealMap of ( ( ) ( non empty ) set ) ) ;

theorem :: C0SP2:34
for a being ( ( ) ( V11() real ext-real ) Real)
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 ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V117() V185() V186() V187() V188() V189() V190() V191() V197() bounded_below V268() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) implies F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = 0. (R_Normed_Space_of_C_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( non empty ) ( non empty strict ) NORMSTR ) : ( ( ) ( V49( R_Normed_Space_of_C_0_Functions b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( non empty ) ( non empty strict ) NORMSTR ) ) ) Element of the carrier of (R_Normed_Space_of_C_0_Functions b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( non empty ) ( non empty strict ) NORMSTR ) : ( ( ) ( non empty ) set ) ) ) & ( F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = 0. (R_Normed_Space_of_C_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( non empty ) ( non empty strict ) NORMSTR ) : ( ( ) ( V49( R_Normed_Space_of_C_0_Functions b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( non empty ) ( non empty strict ) NORMSTR ) ) ) Element of the carrier of (R_Normed_Space_of_C_0_Functions b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( non empty ) ( non empty strict ) NORMSTR ) : ( ( ) ( non empty ) set ) ) implies ||.F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V117() V185() V186() V187() V188() V189() V190() V191() V197() bounded_below V268() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V185() V186() V187() V188() V189() V190() V191() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) : ( ( ) ( non empty ) set ) ) ) ) & ||.(a : ( ( ) ( V11() real ext-real ) Real) * F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of (R_Normed_Space_of_C_0_Functions b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( non empty ) ( non empty strict ) NORMSTR ) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) = (abs a : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) * ||.F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) & ||.(F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) + G : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of (R_Normed_Space_of_C_0_Functions b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( non empty ) ( non empty strict ) NORMSTR ) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) <= ||.F : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) + ||.G : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V185() V186() V187() V191() non bounded_below non bounded_above V268() ) set ) ) ) ;

theorem :: C0SP2:35
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds R_Normed_Space_of_C_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( non empty ) ( non empty strict ) NORMSTR ) is RealNormSpace-like ;

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

theorem :: C0SP2:36
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds R_Normed_Space_of_C_0_Functions X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( non empty ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive strict RealNormSpace-like ) NORMSTR ) is ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) RealNormSpace) ;