:: CSSPACE4 semantic presentation

begin

definition
func the_set_of_BoundedComplexSequences -> ( ( ) ( ) Subset of ) means :: CSSPACE4:def 1
 for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in it : ( ( ) ( ) CUNITSTR ) iff ( x : ( ( ) ( ) set ) in the_set_of_ComplexSequences : ( ( non empty ) ( non empty ) set ) & seq_id x : ( ( ) ( ) set ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) :] : ( ( ) ( non empty Relation-like V33() ) set ) : ( ( ) ( non empty ) set ) ) is bounded ) );
end;

registration
cluster the_set_of_BoundedComplexSequences : ( ( ) ( ) Subset of ) -> non empty ;
cluster the_set_of_BoundedComplexSequences : ( ( ) ( ) Subset of ) -> linearly-closed ;
end;

registration
cluster CLSStruct(# the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,(Zero_ (the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,Linear_Space_of_ComplexSequences : ( ( non empty strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) )) : ( ( ) ( ) Element of the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ) ,(Add_ (the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,Linear_Space_of_ComplexSequences : ( ( non empty strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) -defined the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) -valued Function-like V23([:the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ) quasi_total ) Element of bool [:[:the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ,the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ (the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,Linear_Space_of_ComplexSequences : ( ( non empty strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) ,the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) -defined the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) -valued Function-like V23([:COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) ,the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ) quasi_total ) Element of bool [:[:COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) ,the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ,the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) CLSStruct ) -> right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ;
end;

definition
func Complex_linfty_norm -> ( ( Function-like quasi_total ) ( non empty Relation-like the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V23( the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ) quasi_total V33() V34() V35() ) Function of the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) means :: CSSPACE4:def 2
 for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) holds
it : ( ( ) ( ) set ) . x : ( ( ) ( ) set ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) = upper_bound (rng |.(seq_id x : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) :] : ( ( ) ( non empty Relation-like V33() ) set ) : ( ( ) ( non empty ) set ) ) .| : ( ( Function-like ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() V34() V35() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) :] : ( ( ) ( non empty Relation-like V33() V34() V35() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ;
end;

theorem :: CSSPACE4:1
for seq being ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Complex_Sequence) holds
( ( seq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Complex_Sequence) is bounded & upper_bound (rng |.seq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Complex_Sequence) .| : ( ( Function-like ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() V34() V35() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) :] : ( ( ) ( non empty Relation-like V33() V34() V35() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V136() V181() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) ) iff for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V136() V181() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) holds seq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Complex_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V136() V181() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) ) = 0c : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) ) ) ;

registration
cluster CNORMSTR(# the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,(Zero_ (the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,Linear_Space_of_ComplexSequences : ( ( non empty strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) )) : ( ( ) ( ) Element of the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ) ,(Add_ (the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,Linear_Space_of_ComplexSequences : ( ( non empty strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) -defined the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) -valued Function-like V23([:the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ) quasi_total ) Element of bool [:[:the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ,the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ (the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,Linear_Space_of_ComplexSequences : ( ( non empty strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) ,the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) -defined the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) -valued Function-like V23([:COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) ,the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ) quasi_total ) Element of bool [:[:COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) ,the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ,the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,Complex_linfty_norm : ( ( Function-like quasi_total ) ( non empty Relation-like the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V23( the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ) quasi_total V33() V34() V35() ) Function of the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) #) : ( ( strict ) ( non empty strict ) CNORMSTR ) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ;
end;

definition
func Complex_linfty_Space -> ( ( non empty ) ( non empty ) CNORMSTR ) equals :: CSSPACE4:def 3
 CNORMSTR(# the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,(Zero_ (the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,Linear_Space_of_ComplexSequences : ( ( non empty strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) )) : ( ( ) ( ) Element of the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ) ,(Add_ (the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,Linear_Space_of_ComplexSequences : ( ( non empty strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) -defined the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) -valued Function-like V23([:the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ) quasi_total ) Element of bool [:[:the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ,the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ (the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,Linear_Space_of_ComplexSequences : ( ( non empty strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) ,the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) -defined the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) -valued Function-like V23([:COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) ,the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ) quasi_total ) Element of bool [:[:COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) ,the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ,the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,Complex_linfty_norm : ( ( Function-like quasi_total ) ( non empty Relation-like the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V23( the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ) quasi_total V33() V34() V35() ) Function of the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) #) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) CNORMSTR ) ;
end;

theorem :: CSSPACE4:2
( the carrier of Complex_linfty_Space : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( non empty ) set ) = the_set_of_BoundedComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) & ( for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) is ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) iff ( x : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) is ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Complex_Sequence) & seq_id x : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) :] : ( ( ) ( non empty Relation-like V33() ) set ) : ( ( ) ( non empty ) set ) ) is bounded ) ) ) & 0. Complex_linfty_Space : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( V82( Complex_linfty_Space : ( ( non empty ) ( non empty ) CNORMSTR ) ) ) Element of the carrier of Complex_linfty_Space : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) = CZeroseq : ( ( ) ( ) Element of the_set_of_ComplexSequences : ( ( non empty ) ( non empty ) set ) ) & ( for u being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) = seq_id u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) :] : ( ( ) ( non empty Relation-like V33() ) set ) : ( ( ) ( non empty ) set ) ) ) & ( for u, v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of Complex_linfty_Space : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) = (seq_id u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) :] : ( ( ) ( non empty Relation-like V33() ) set ) : ( ( ) ( non empty ) set ) ) + (seq_id v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) :] : ( ( ) ( non empty Relation-like V33() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) :] : ( ( ) ( non empty Relation-like V33() ) set ) : ( ( ) ( non empty ) set ) ) ) & ( for c being ( ( V11() ) ( V11() ) Complex)
for u being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds c : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) * u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of Complex_linfty_Space : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) = c : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) (#) (seq_id u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) :] : ( ( ) ( non empty Relation-like V33() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V33() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) :] : ( ( ) ( non empty Relation-like V33() ) set ) : ( ( ) ( non empty ) set ) ) ) & ( for u being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( - u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of Complex_linfty_Space : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) = - (seq_id u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) :] : ( ( ) ( non empty Relation-like V33() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) :] : ( ( ) ( non empty Relation-like V33() ) set ) : ( ( ) ( non empty ) set ) ) & seq_id (- u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of Complex_linfty_Space : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) :] : ( ( ) ( non empty Relation-like V33() ) set ) : ( ( ) ( non empty ) set ) ) = - (seq_id u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) :] : ( ( ) ( non empty Relation-like V33() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) :] : ( ( ) ( non empty Relation-like V33() ) set ) : ( ( ) ( non empty ) set ) ) ) ) & ( for u, v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) - v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of Complex_linfty_Space : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) = (seq_id u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) :] : ( ( ) ( non empty Relation-like V33() ) set ) : ( ( ) ( non empty ) set ) ) - (seq_id v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) :] : ( ( ) ( non empty Relation-like V33() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) :] : ( ( ) ( non empty Relation-like V33() ) set ) : ( ( ) ( non empty ) set ) ) ) & ( for v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds seq_id v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) :] : ( ( ) ( non empty Relation-like V33() ) set ) : ( ( ) ( non empty ) set ) ) is bounded ) & ( for v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds ||.v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) = upper_bound (rng |.(seq_id v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) :] : ( ( ) ( non empty Relation-like V33() ) set ) : ( ( ) ( non empty ) set ) ) .| : ( ( Function-like ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() V34() V35() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) :] : ( ( ) ( non empty Relation-like V33() V34() V35() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ) ) ;

theorem :: CSSPACE4:3
for x, y being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for c being ( ( V11() ) ( V11() ) Complex) holds
( ( ||.x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V136() V181() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) implies x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = 0. Complex_linfty_Space : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( V82( Complex_linfty_Space : ( ( non empty ) ( non empty ) CNORMSTR ) ) ) Element of the carrier of Complex_linfty_Space : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) ) & ( x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = 0. Complex_linfty_Space : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( V82( Complex_linfty_Space : ( ( non empty ) ( non empty ) CNORMSTR ) ) ) Element of the carrier of Complex_linfty_Space : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) implies ||.x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V136() V181() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) ) & 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V136() V181() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) <= ||.x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) & ||.(x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) + y : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of Complex_linfty_Space : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) <= ||.x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) + ||.y : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) & ||.(c : ( ( V11() ) ( V11() ) Complex) * x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of Complex_linfty_Space : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) = |.c : ( ( V11() ) ( V11() ) Complex) .| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) * ||.x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ) ;

registration
cluster Complex_linfty_Space : ( ( non empty ) ( non empty ) CNORMSTR ) -> non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ;
end;

theorem :: CSSPACE4:4
for vseq being ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of Complex_linfty_Space : ( ( non empty ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) sequence of ( ( ) ( non empty ) set ) ) st vseq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of Complex_linfty_Space : ( ( non empty ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) sequence of ( ( ) ( non empty ) set ) ) is Cauchy_sequence_by_Norm holds
vseq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of Complex_linfty_Space : ( ( non empty ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) sequence of ( ( ) ( non empty ) set ) ) is convergent ;

theorem :: CSSPACE4:5
Complex_linfty_Space : ( ( non empty ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) is ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like complete ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like complete ) ComplexBanachSpace) ;

begin

definition
let X be ( ( non empty ) ( non empty ) set ) ;
let Y be ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) ;
let IT be ( ( Function-like quasi_total ) ( non empty Relation-like X : ( ( non empty ) ( non empty ) set ) -defined the carrier of Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(X : ( ( non empty ) ( non empty ) set ) ) quasi_total ) Function of X : ( ( non empty ) ( non empty ) set ) , the carrier of Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ;
attr IT is bounded means :: CSSPACE4:def 4
 ex K being ( ( ) ( V11() real ext-real ) Real) st
( 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V136() V181() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) <= K : ( ( ) ( V11() real ext-real ) Real) & ( for x being ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) holds ||.(IT : ( ( Function-like quasi_total ) ( Relation-like [:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined X : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) <= K : ( ( ) ( V11() real ext-real ) Real) ) );
end;

theorem :: CSSPACE4:6
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace)
for f being ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total ) Function of X : ( ( non empty ) ( non empty ) set ) , the carrier of Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) st ( for x being ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) holds f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total ) Function of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) = 0. Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( V82(b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) ) ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ) holds
f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total ) Function of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) is bounded ;

registration
let X be ( ( non empty ) ( non empty ) set ) ;
let Y be ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) ;
cluster non empty Relation-like X : ( ( non empty ) ( non empty ) set ) -defined the carrier of Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like V23(X : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded for ( ( ) ( ) Element of bool [:X : ( ( non empty ) ( non empty ) set ) , the carrier of Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

definition
let X be ( ( non empty ) ( non empty ) set ) ;
let Y be ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) ;
func ComplexBoundedFunctions (X,Y) -> ( ( ) ( ) Subset of ) means :: CSSPACE4:def 5
 for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in it : ( ( Function-like quasi_total ) ( non empty Relation-like [:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) -defined X : ( ( non empty ) ( non empty ) set ) -valued Function-like V23([:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) ) quasi_total ) Element of bool [:[:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) iff x : ( ( ) ( ) set ) is ( ( Function-like quasi_total bounded ) ( non empty Relation-like X : ( ( non empty ) ( non empty ) set ) -defined the carrier of Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like V23(X : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of X : ( ( non empty ) ( non empty ) set ) , the carrier of Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) );
end;

registration
let X be ( ( non empty ) ( non empty ) set ) ;
let Y be ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) ;
cluster ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) ) : ( ( ) ( ) Subset of ) -> non empty ;
end;

theorem :: CSSPACE4:7
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) holds ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) ) : ( ( ) ( non empty ) Subset of ) is linearly-closed ;

theorem :: CSSPACE4:8
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) holds CLSStruct(# (ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) )) : ( ( ) ( non empty ) Subset of ) ,(Zero_ ((ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) )) : ( ( ) ( non empty ) Subset of ) ,(ComplexVectSpace (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) )) : ( ( 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 ) CLSStruct ) )) : ( ( ) ( ) Element of ComplexBoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) ) : ( ( ) ( non empty ) Subset of ) ) ,(Add_ ((ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) )) : ( ( ) ( non empty ) Subset of ) ,(ComplexVectSpace (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) )) : ( ( 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 ) CLSStruct ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:(ComplexBoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) )) : ( ( ) ( non empty ) Subset of ) ,(ComplexBoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) -defined ComplexBoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) ) : ( ( ) ( non empty ) Subset of ) -valued Function-like V23([:(ComplexBoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) )) : ( ( ) ( non empty ) Subset of ) ,(ComplexBoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ) quasi_total ) Element of bool [:[:(ComplexBoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) )) : ( ( ) ( non empty ) Subset of ) ,(ComplexBoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ,(ComplexBoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ ((ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) )) : ( ( ) ( non empty ) Subset of ) ,(ComplexVectSpace (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) )) : ( ( 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 ) CLSStruct ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) ,(ComplexBoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) -defined ComplexBoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) ) : ( ( ) ( non empty ) Subset of ) -valued Function-like V23([:COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) ,(ComplexBoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ) quasi_total ) Element of bool [:[:COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) ,(ComplexBoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ,(ComplexBoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) CLSStruct ) is ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of ComplexVectSpace (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) ) : ( ( 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 ) CLSStruct ) ) ;

registration
let X be ( ( non empty ) ( non empty ) set ) ;
let Y be ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) ;
cluster CLSStruct(# (ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(Zero_ ((ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(ComplexVectSpace (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( 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 ) CLSStruct ) )) : ( ( ) ( ) Element of ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) ) : ( ( ) ( non empty ) Subset of ) ) ,(Add_ ((ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(ComplexVectSpace (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( 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 ) CLSStruct ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:(ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) -defined ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) ) : ( ( ) ( non empty ) Subset of ) -valued Function-like V23([:(ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ) quasi_total ) Element of bool [:[:(ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ,(ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ ((ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(ComplexVectSpace (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( 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 ) CLSStruct ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) ,(ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) -defined ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) ) : ( ( ) ( non empty ) Subset of ) -valued Function-like V23([:COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) ,(ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ) quasi_total ) Element of bool [:[:COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) ,(ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ,(ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) CLSStruct ) -> right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ;
end;

definition
let X be ( ( non empty ) ( non empty ) set ) ;
let Y be ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) ;
func C_VectorSpace_of_BoundedFunctions (X,Y) -> ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) equals :: CSSPACE4:def 6
 CLSStruct(# (ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(Zero_ ((ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(ComplexVectSpace (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( 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 ) CLSStruct ) )) : ( ( ) ( ) Element of ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) ) : ( ( ) ( non empty ) Subset of ) ) ,(Add_ ((ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(ComplexVectSpace (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( 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 ) CLSStruct ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:(ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) -defined ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) ) : ( ( ) ( non empty ) Subset of ) -valued Function-like V23([:(ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ) quasi_total ) Element of bool [:[:(ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ,(ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ ((ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(ComplexVectSpace (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( 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 ) CLSStruct ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) ,(ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) -defined ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) ) : ( ( ) ( non empty ) Subset of ) -valued Function-like V23([:COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) ,(ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ) quasi_total ) Element of bool [:[:COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) ,(ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ,(ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) ;
end;

registration
let X be ( ( non empty ) ( non empty ) set ) ;
let Y be ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) ;
cluster C_VectorSpace_of_BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) ) : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) -> non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ;
end;

theorem :: CSSPACE4:9
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace)
for f, g, h being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) )
for f9, g9, h9 being ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of X : ( ( non empty ) ( non empty ) set ) , the carrier of Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) st f9 : ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) = f : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & g9 : ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) = g : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & h9 : ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) = h : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( h : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) = f : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + g : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (C_VectorSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) )) : ( ( 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 strict vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) iff for x being ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) holds h9 : ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) = (f9 : ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) + (g9 : ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: CSSPACE4:10
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace)
for f, h being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) )
for f9, h9 being ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of X : ( ( non empty ) ( non empty ) set ) , the carrier of Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) st f9 : ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) = f : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & h9 : ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) = h : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
for c being ( ( V11() ) ( V11() ) Complex) holds
( h : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) = c : ( ( V11() ) ( V11() ) Complex) * f : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (C_VectorSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) )) : ( ( 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 strict vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) iff for x being ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) holds h9 : ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) = c : ( ( V11() ) ( V11() ) Complex) * (f9 : ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: CSSPACE4:11
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) holds 0. (C_VectorSpace_of_BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) )) : ( ( 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 strict vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( V82( C_VectorSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) ) : ( ( 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 strict vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) ) ) Element of the carrier of (C_VectorSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) )) : ( ( 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 strict vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) = X : ( ( non empty ) ( non empty ) set ) --> (0. Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) ) : ( ( ) ( V82(b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) ) ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like constant V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;

definition
let X be ( ( non empty ) ( non empty ) set ) ;
let Y be ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) ;
let f be ( ( ) ( ) set ) ;
assume f : ( ( ) ( ) set ) in ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) ) : ( ( ) ( non empty ) Subset of ) ;
func modetrans (f,X,Y) -> ( ( Function-like quasi_total bounded ) ( non empty Relation-like X : ( ( non empty ) ( non empty ) set ) -defined the carrier of Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like V23(X : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of X : ( ( non empty ) ( non empty ) set ) , the carrier of Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) equals :: CSSPACE4:def 7
f : ( ( Function-like quasi_total ) ( non empty Relation-like [:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) -defined X : ( ( non empty ) ( non empty ) set ) -valued Function-like V23([:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) ) quasi_total ) Element of bool [:[:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

definition
let X be ( ( non empty ) ( non empty ) set ) ;
let Y be ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) ;
let u be ( ( Function-like quasi_total ) ( non empty Relation-like X : ( ( non empty ) ( non empty ) set ) -defined the carrier of Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(X : ( ( non empty ) ( non empty ) set ) ) quasi_total ) Function of X : ( ( non empty ) ( non empty ) set ) , the carrier of Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ;
func PreNorms u -> ( ( non empty ) ( non empty V45() V46() V47() ) Subset of ( ( ) ( non empty ) set ) ) equals :: CSSPACE4:def 8
 { ||.(u : ( ( Function-like quasi_total ) ( non empty Relation-like [:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) -defined X : ( ( non empty ) ( non empty ) set ) -valued Function-like V23([:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) ) quasi_total ) Element of bool [:[:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) . t : ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) where t is ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) : verum } ;
end;

theorem :: CSSPACE4:12
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace)
for g being ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of X : ( ( non empty ) ( non empty ) set ) , the carrier of Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) holds PreNorms g : ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( non empty ) ( non empty V45() V46() V47() ) Subset of ( ( ) ( non empty ) set ) ) is bounded_above ;

theorem :: CSSPACE4:13
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace)
for g being ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total ) Function of X : ( ( non empty ) ( non empty ) set ) , the carrier of Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) holds
( g : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total ) Function of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) is bounded iff PreNorms g : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total ) Function of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( non empty ) ( non empty V45() V46() V47() ) Subset of ( ( ) ( non empty ) set ) ) is bounded_above ) ;

definition
let X be ( ( non empty ) ( non empty ) set ) ;
let Y be ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) ;
func ComplexBoundedFunctionsNorm (X,Y) -> ( ( Function-like quasi_total ) ( non empty Relation-like ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) ) : ( ( ) ( non empty ) Subset of ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V23( ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) ) : ( ( ) ( non empty ) Subset of ) ) quasi_total V33() V34() V35() ) Function of ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) ) : ( ( ) ( non empty ) Subset of ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) means :: CSSPACE4:def 9
 for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) ) : ( ( ) ( non empty ) Subset of ) holds
it : ( ( Function-like quasi_total ) ( non empty Relation-like [:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) -defined X : ( ( non empty ) ( non empty ) set ) -valued Function-like V23([:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) ) quasi_total ) Element of bool [:[:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) set ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) = upper_bound (PreNorms (modetrans (x : ( ( ) ( ) set ) ,X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( Function-like quasi_total bounded ) ( non empty Relation-like X : ( ( non empty ) ( non empty ) set ) -defined the carrier of Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like V23(X : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of X : ( ( non empty ) ( non empty ) set ) , the carrier of Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty V45() V46() V47() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ;
end;

theorem :: CSSPACE4:14
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace)
for f being ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of X : ( ( non empty ) ( non empty ) set ) , the carrier of Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) holds modetrans (f : ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ,X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) ) : ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) = f : ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ;

theorem :: CSSPACE4:15
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace)
for f being ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of X : ( ( non empty ) ( non empty ) set ) , the carrier of Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) holds (ComplexBoundedFunctionsNorm (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) )) : ( ( Function-like quasi_total ) ( non empty Relation-like ComplexBoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) ) : ( ( ) ( non empty ) Subset of ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V23( ComplexBoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) ) : ( ( ) ( non empty ) Subset of ) ) quasi_total V33() V34() V35() ) Function of ComplexBoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) ) : ( ( ) ( non empty ) Subset of ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) . f : ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) = upper_bound (PreNorms f : ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty V45() V46() V47() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ;

definition
let X be ( ( non empty ) ( non empty ) set ) ;
let Y be ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) ;
func C_NormSpace_of_BoundedFunctions (X,Y) -> ( ( non empty ) ( non empty ) CNORMSTR ) equals :: CSSPACE4:def 10
 CNORMSTR(# (ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(Zero_ ((ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(ComplexVectSpace (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( 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 ) CLSStruct ) )) : ( ( ) ( ) Element of ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) ) : ( ( ) ( non empty ) Subset of ) ) ,(Add_ ((ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(ComplexVectSpace (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( 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 ) CLSStruct ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:(ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) -defined ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) ) : ( ( ) ( non empty ) Subset of ) -valued Function-like V23([:(ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ) quasi_total ) Element of bool [:[:(ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ,(ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ ((ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(ComplexVectSpace (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( 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 ) CLSStruct ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) ,(ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) -defined ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) ) : ( ( ) ( non empty ) Subset of ) -valued Function-like V23([:COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) ,(ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ) quasi_total ) Element of bool [:[:COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) ,(ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ,(ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,(ComplexBoundedFunctionsNorm (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) ) : ( ( ) ( non empty ) Subset of ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V23( ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) ) : ( ( ) ( non empty ) Subset of ) ) quasi_total V33() V34() V35() ) Function of ComplexBoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) ) : ( ( ) ( non empty ) Subset of ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) #) : ( ( strict ) ( non empty strict ) CNORMSTR ) ;
end;

theorem :: CSSPACE4:16
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) holds X : ( ( non empty ) ( non empty ) set ) --> (0. Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) ) : ( ( ) ( V82(b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) ) ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like constant V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) = 0. (C_NormSpace_of_BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) )) : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( V82( C_NormSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) ) : ( ( non empty ) ( non empty ) CNORMSTR ) ) ) Element of the carrier of (C_NormSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) )) : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) ;

theorem :: CSSPACE4:17
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace)
for f being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for g being ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of X : ( ( non empty ) ( non empty ) set ) , the carrier of Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) st g : ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) = f : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds
for t being ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) holds ||.(g : ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) . t : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) <= ||.f : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ;

theorem :: CSSPACE4:18
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace)
for f being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V136() V181() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) <= ||.f : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ;

theorem :: CSSPACE4:19
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace)
for f being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st f : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = 0. (C_NormSpace_of_BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) )) : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( V82( C_NormSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) ) : ( ( non empty ) ( non empty ) CNORMSTR ) ) ) Element of the carrier of (C_NormSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) )) : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) holds
0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V136() V181() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) = ||.f : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ;

theorem :: CSSPACE4:20
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace)
for f, g, h being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for f9, g9, h9 being ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of X : ( ( non empty ) ( non empty ) set ) , the carrier of Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) st f9 : ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) = f : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) & g9 : ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) = g : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) & h9 : ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) = h : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds
( h : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = f : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) + g : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (C_NormSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) )) : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) iff for x being ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) holds h9 : ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) = (f9 : ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) + (g9 : ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: CSSPACE4:21
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace)
for f, h being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for f9, h9 being ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of X : ( ( non empty ) ( non empty ) set ) , the carrier of Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) st f9 : ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) = f : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) & h9 : ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) = h : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds
for c being ( ( V11() ) ( V11() ) Complex) holds
( h : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = c : ( ( V11() ) ( V11() ) Complex) * f : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (C_NormSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) )) : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) iff for x being ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) holds h9 : ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) = c : ( ( V11() ) ( V11() ) Complex) * (f9 : ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: CSSPACE4:22
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace)
for f, g being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for c being ( ( V11() ) ( V11() ) Complex) holds
( ( ||.f : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V136() V181() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) implies f : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = 0. (C_NormSpace_of_BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) )) : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( V82( C_NormSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) ) : ( ( non empty ) ( non empty ) CNORMSTR ) ) ) Element of the carrier of (C_NormSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) )) : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) ) & ( f : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = 0. (C_NormSpace_of_BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) )) : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( V82( C_NormSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) ) : ( ( non empty ) ( non empty ) CNORMSTR ) ) ) Element of the carrier of (C_NormSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) )) : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) implies ||.f : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V136() V181() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) ) & ||.(c : ( ( V11() ) ( V11() ) Complex) * f : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of (C_NormSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) )) : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) = |.c : ( ( V11() ) ( V11() ) Complex) .| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) * ||.f : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) & ||.(f : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) + g : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of (C_NormSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) )) : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) <= ||.f : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) + ||.g : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ) ;

theorem :: CSSPACE4:23
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) holds
( C_NormSpace_of_BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) ) : ( ( non empty ) ( non empty ) CNORMSTR ) is reflexive & C_NormSpace_of_BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) ) : ( ( non empty ) ( non empty ) CNORMSTR ) is discerning & C_NormSpace_of_BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) ) : ( ( non empty ) ( non empty ) CNORMSTR ) is ComplexNormSpace-like ) ;

theorem :: CSSPACE4:24
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) holds C_NormSpace_of_BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) ) : ( ( non empty ) ( non empty ) CNORMSTR ) is ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) ;

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

theorem :: CSSPACE4:25
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace)
for f, g, h being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for f9, g9, h9 being ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of X : ( ( non empty ) ( non empty ) set ) , the carrier of Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) st f9 : ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) = f : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) & g9 : ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) = g : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) & h9 : ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) = h : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds
( h : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = f : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) - g : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (C_NormSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) )) : ( ( non empty ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) iff for x being ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) holds h9 : ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) = (f9 : ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) - (g9 : ( ( Function-like quasi_total bounded ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total bounded ) Function of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: CSSPACE4:26
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) st Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) is complete holds
for seq being ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of (C_NormSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) )) : ( ( non empty ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) 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 V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of (C_NormSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) )) : ( ( non empty ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) 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 V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of (C_NormSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) )) : ( ( non empty ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) sequence of ( ( ) ( non empty ) set ) ) is convergent ;

theorem :: CSSPACE4:27
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like complete ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like complete ) ComplexBanachSpace) holds C_NormSpace_of_BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like complete ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like complete ) ComplexBanachSpace) ) : ( ( non empty ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) CNORMSTR ) is ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like complete ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like complete ) ComplexBanachSpace) ;

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

begin

theorem :: CSSPACE4:28
for seq1, seq2 being ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Complex_Sequence) st seq1 : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Complex_Sequence) is bounded & seq2 : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Complex_Sequence) is bounded holds
seq1 : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Complex_Sequence) + seq2 : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Complex_Sequence) : ( ( Function-like ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) :] : ( ( ) ( non empty Relation-like V33() ) set ) : ( ( ) ( non empty ) set ) ) is bounded ;

theorem :: CSSPACE4:29
for c being ( ( V11() ) ( V11() ) Complex)
for seq being ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Complex_Sequence) st seq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Complex_Sequence) is bounded holds
c : ( ( V11() ) ( V11() ) Complex) (#) seq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Complex_Sequence) : ( ( Function-like ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) :] : ( ( ) ( non empty Relation-like V33() ) set ) : ( ( ) ( non empty ) set ) ) is bounded ;

theorem :: CSSPACE4:30
for seq being ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Complex_Sequence) holds
( seq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Complex_Sequence) is bounded iff |.seq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Complex_Sequence) .| : ( ( Function-like ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() V34() V35() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) :] : ( ( ) ( non empty Relation-like V33() V34() V35() ) set ) : ( ( ) ( non empty ) set ) ) is bounded ) ;

theorem :: CSSPACE4:31
for seq1, seq2, seq3 being ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Complex_Sequence) holds
( seq1 : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Complex_Sequence) = seq2 : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Complex_Sequence) - seq3 : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Complex_Sequence) : ( ( Function-like ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) :] : ( ( ) ( non empty Relation-like V33() ) set ) : ( ( ) ( non empty ) set ) ) iff for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V136() V181() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) holds seq1 : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Complex_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V136() V181() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) ) = (seq2 : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Complex_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V136() V181() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) ) - (seq3 : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() ) Complex_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V136() V181() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) ) ) ;