:: RSSPACE4 semantic presentation

begin

definition
func the_set_of_BoundedRealSequences -> ( ( ) ( ) Subset of ) means :: RSSPACE4:def 1
 for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in it : ( ( ) ( ) NORMSTR ) iff ( x : ( ( ) ( ) set ) in the_set_of_RealSequences : ( ( 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 V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V105() V106() V107() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) :] : ( ( ) ( non empty Relation-like V105() V106() V107() ) set ) : ( ( ) ( non empty ) set ) ) is bounded ) );
end;

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

registration
cluster RLSStruct(# the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,(Zero_ (the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() ) RLSStruct ) )) : ( ( ) ( ) Element of the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ) ,(Add_ (the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() ) RLSStruct ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) -defined the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) -valued Function-like V23([:the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ) quasi_total ) Element of bool [:[:the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ,the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ (the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() ) RLSStruct ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ,the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) -defined the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) -valued Function-like V23([:REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ,the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ) quasi_total ) Element of bool [:[:REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ,the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ,the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) RLSStruct ) -> right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
end;

definition
func linfty_norm -> ( ( Function-like quasi_total ) ( non empty Relation-like the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) -defined REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) -valued Function-like V23( the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ) quasi_total V105() V106() V107() ) Function of the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) , REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ) means :: RSSPACE4:def 2
 for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) holds
it : ( ( ) ( ) set ) . x : ( ( ) ( ) set ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ) = upper_bound (rng (abs (seq_id x : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V105() V106() V107() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) :] : ( ( ) ( non empty Relation-like V105() V106() V107() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V105() V106() V107() bounded_below ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) :] : ( ( ) ( non empty Relation-like V105() V106() V107() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V115() V116() V117() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ) ;
end;

theorem :: RSSPACE4:1
for rseq being ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V105() V106() V107() ) Real_Sequence) holds
( ( rseq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V105() V106() V107() ) Real_Sequence) is bounded & upper_bound (rng (abs rseq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V105() V106() V107() ) Real_Sequence) ) : ( ( Function-like ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V105() V106() V107() bounded_below ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) :] : ( ( ) ( non empty Relation-like V105() V106() V107() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V115() V116() V117() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ) ) iff for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real ) Nat) holds rseq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V105() V106() V107() ) Real_Sequence) . n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real ) Nat) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;

registration
cluster NORMSTR(# the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,(Zero_ (the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() ) RLSStruct ) )) : ( ( ) ( ) Element of the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ) ,(Add_ (the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() ) RLSStruct ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) -defined the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) -valued Function-like V23([:the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ) quasi_total ) Element of bool [:[:the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ,the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ (the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() ) RLSStruct ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ,the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) -defined the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) -valued Function-like V23([:REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ,the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ) quasi_total ) Element of bool [:[:REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ,the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ,the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,linfty_norm : ( ( Function-like quasi_total ) ( non empty Relation-like the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) -defined REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) -valued Function-like V23( the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ) quasi_total V105() V106() V107() ) Function of the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) , REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ) #) : ( ( strict ) ( non empty strict ) NORMSTR ) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ;
end;

definition
func linfty_Space -> ( ( non empty ) ( non empty ) NORMSTR ) equals :: RSSPACE4:def 3
 NORMSTR(# the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,(Zero_ (the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() ) RLSStruct ) )) : ( ( ) ( ) Element of the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ) ,(Add_ (the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() ) RLSStruct ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) -defined the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) -valued Function-like V23([:the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ) quasi_total ) Element of bool [:[:the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ,the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ (the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() ) RLSStruct ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ,the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) -defined the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) -valued Function-like V23([:REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ,the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ) quasi_total ) Element of bool [:[:REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ,the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ,the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,linfty_norm : ( ( Function-like quasi_total ) ( non empty Relation-like the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) -defined REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) -valued Function-like V23( the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ) quasi_total V105() V106() V107() ) Function of the_set_of_BoundedRealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) , REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ) #) : ( ( strict ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() strict ) NORMSTR ) ;
end;

theorem :: RSSPACE4:2
( the carrier of linfty_Space : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) = the_set_of_BoundedRealSequences : ( ( ) ( 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 V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V105() V106() V107() ) Real_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 V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V105() V106() V107() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) :] : ( ( ) ( non empty Relation-like V105() V106() V107() ) set ) : ( ( ) ( non empty ) set ) ) is bounded ) ) ) & 0. linfty_Space : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( V49( linfty_Space : ( ( non empty ) ( non empty ) NORMSTR ) ) ) Element of the carrier of linfty_Space : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) = Zeroseq : ( ( ) ( ) Element of the_set_of_RealSequences : ( ( 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 V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V105() V106() V107() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) :] : ( ( ) ( non empty Relation-like V105() V106() V107() ) 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 linfty_Space : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( 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 V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V105() V106() V107() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) :] : ( ( ) ( non empty Relation-like V105() V106() V107() ) 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 V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V105() V106() V107() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) :] : ( ( ) ( non empty Relation-like V105() V106() V107() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V105() V106() V107() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) :] : ( ( ) ( non empty Relation-like V105() V106() V107() ) set ) : ( ( ) ( non empty ) set ) ) ) & ( for r being ( ( ) ( V11() real ext-real ) Real)
for u being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds r : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) * u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of linfty_Space : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) = r : ( ( ) ( ) 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 V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V105() V106() V107() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) :] : ( ( ) ( non empty Relation-like V105() V106() V107() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) -valued Function-like V105() V106() V107() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) :] : ( ( ) ( non empty Relation-like V105() V106() V107() ) set ) : ( ( ) ( non empty ) set ) ) ) & ( for u being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( - u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of linfty_Space : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( 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 V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V105() V106() V107() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) :] : ( ( ) ( non empty Relation-like V105() V106() V107() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V105() V106() V107() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) :] : ( ( ) ( non empty Relation-like V105() V106() V107() ) set ) : ( ( ) ( non empty ) set ) ) & seq_id (- u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of linfty_Space : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V105() V106() V107() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) :] : ( ( ) ( non empty Relation-like V105() V106() V107() ) 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 V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V105() V106() V107() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) :] : ( ( ) ( non empty Relation-like V105() V106() V107() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V105() V106() V107() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) :] : ( ( ) ( non empty Relation-like V105() V106() V107() ) 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 linfty_Space : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( 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 V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V105() V106() V107() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) :] : ( ( ) ( non empty Relation-like V105() V106() V107() ) 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 V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V105() V106() V107() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) :] : ( ( ) ( non empty Relation-like V105() V106() V107() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V105() V106() V107() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) :] : ( ( ) ( non empty Relation-like V105() V106() V107() ) 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 V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V105() V106() V107() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) :] : ( ( ) ( non empty Relation-like V105() V106() V107() ) 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 V30() V115() V116() V117() V121() ) set ) ) = upper_bound (rng (abs (seq_id v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V105() V106() V107() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) :] : ( ( ) ( non empty Relation-like V105() V106() V107() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V105() V106() V107() bounded_below ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) :] : ( ( ) ( non empty Relation-like V105() V106() V107() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V115() V116() V117() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ) ) ) ;

theorem :: RSSPACE4:3
for x, y being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for a being ( ( ) ( V11() real ext-real ) Real) holds
( ( ||.x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ) implies x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = 0. linfty_Space : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( V49( linfty_Space : ( ( non empty ) ( non empty ) NORMSTR ) ) ) Element of the carrier of linfty_Space : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) ) & ( x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = 0. linfty_Space : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( V49( linfty_Space : ( ( non empty ) ( non empty ) NORMSTR ) ) ) Element of the carrier of linfty_Space : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) implies ||.x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ) ) & 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ) <= ||.x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ) & ||.(x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) + y : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of linfty_Space : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ) <= ||.x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ) + ||.y : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ) & ||.(a : ( ( ) ( V11() real ext-real ) Real) * x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of linfty_Space : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ) = (abs a : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ) * ||.x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ) ) ;

registration
cluster linfty_Space : ( ( non empty ) ( non empty ) NORMSTR ) -> non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ;
end;

theorem :: RSSPACE4:4
for vseq being ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of linfty_Space : ( ( non empty ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) 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 V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of linfty_Space : ( ( non empty ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) 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 V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of linfty_Space : ( ( non empty ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) sequence of ( ( ) ( non empty ) set ) ) is convergent ;

begin

definition
let X be ( ( non empty ) ( non empty ) set ) ;
let Y be ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) ;
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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ;
attr IT is bounded means :: RSSPACE4:def 4
 ex K being ( ( ) ( V11() real ext-real ) Real) st
( 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) 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 V30() V115() V116() V117() V121() ) set ) ) <= K : ( ( ) ( V11() real ext-real ) Real) ) );
end;

theorem :: RSSPACE4:5
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace)
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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) = 0. Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( V49(b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) ) ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) ;
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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) ;
func BoundedFunctions (X,Y) -> ( ( ) ( ) Subset of ) means :: RSSPACE4: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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) ;
cluster BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) ) : ( ( ) ( ) Subset of ) -> non empty ;
end;

theorem :: RSSPACE4:6
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) holds BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) ) : ( ( ) ( non empty ) Subset of ) is linearly-closed ;

theorem :: RSSPACE4:7
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) holds RLSStruct(# (BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) )) : ( ( ) ( non empty ) Subset of ) ,(Zero_ ((BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) )) : ( ( ) ( non empty ) Subset of ) ,(RealVectSpace (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) )) : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() ) RLSStruct ) )) : ( ( ) ( ) Element of BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) ) : ( ( ) ( non empty ) Subset of ) ) ,(Add_ ((BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) )) : ( ( ) ( non empty ) Subset of ) ,(RealVectSpace (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) )) : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() ) RLSStruct ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:(BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) )) : ( ( ) ( non empty ) Subset of ) ,(BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) -defined BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) ) : ( ( ) ( non empty ) Subset of ) -valued Function-like V23([:(BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) )) : ( ( ) ( non empty ) Subset of ) ,(BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ) quasi_total ) Element of bool [:[:(BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) )) : ( ( ) ( non empty ) Subset of ) ,(BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ,(BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ ((BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) )) : ( ( ) ( non empty ) Subset of ) ,(RealVectSpace (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) )) : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() ) RLSStruct ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ,(BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) -defined BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) ) : ( ( ) ( non empty ) Subset of ) -valued Function-like V23([:REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ,(BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ) quasi_total ) Element of bool [:[:REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ,(BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ,(BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) RLSStruct ) is ( ( ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() ) Subspace of RealVectSpace (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) ) : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() ) RLSStruct ) ) ;

registration
let X be ( ( non empty ) ( non empty ) set ) ;
let Y be ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) ;
cluster RLSStruct(# (BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(Zero_ ((BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(RealVectSpace (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() ) RLSStruct ) )) : ( ( ) ( ) Element of BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) ) : ( ( ) ( non empty ) Subset of ) ) ,(Add_ ((BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(RealVectSpace (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() ) RLSStruct ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:(BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) -defined BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) ) : ( ( ) ( non empty ) Subset of ) -valued Function-like V23([:(BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ) quasi_total ) Element of bool [:[:(BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ,(BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ ((BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(RealVectSpace (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() ) RLSStruct ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ,(BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) -defined BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) ) : ( ( ) ( non empty ) Subset of ) -valued Function-like V23([:REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ,(BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ) quasi_total ) Element of bool [:[:REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ,(BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ,(BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) RLSStruct ) -> right_complementable strict Abelian add-associative right_zeroed 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) ;
func R_VectorSpace_of_BoundedFunctions (X,Y) -> ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() ) RealLinearSpace) equals :: RSSPACE4:def 6
 RLSStruct(# (BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(Zero_ ((BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(RealVectSpace (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() ) RLSStruct ) )) : ( ( ) ( ) Element of BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) ) : ( ( ) ( non empty ) Subset of ) ) ,(Add_ ((BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(RealVectSpace (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() ) RLSStruct ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:(BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) -defined BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) ) : ( ( ) ( non empty ) Subset of ) -valued Function-like V23([:(BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ) quasi_total ) Element of bool [:[:(BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ,(BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ ((BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(RealVectSpace (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() ) RLSStruct ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ,(BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) -defined BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) ) : ( ( ) ( non empty ) Subset of ) -valued Function-like V23([:REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ,(BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ) quasi_total ) Element of bool [:[:REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ,(BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ,(BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() ) RLSStruct ) ;
end;

registration
let X be ( ( non empty ) ( non empty ) set ) ;
let Y be ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) ;
cluster R_VectorSpace_of_BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) ) : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() ) RealLinearSpace) -> non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
end;

theorem :: RSSPACE4:8
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace)
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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 (R_VectorSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) )) : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() ) RealLinearSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: RSSPACE4:9
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace)
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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) = h : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
for a being ( ( ) ( V11() real ext-real ) Real) holds
( h : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) = a : ( ( ) ( V11() real ext-real ) Real) * f : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (R_VectorSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) )) : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() ) RealLinearSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) = a : ( ( ) ( V11() real ext-real ) Real) * (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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: RSSPACE4:10
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) holds 0. (R_VectorSpace_of_BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) )) : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() ) RealLinearSpace) : ( ( ) ( V49( R_VectorSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) ) : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() ) RealLinearSpace) ) ) Element of the carrier of (R_VectorSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) )) : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) = X : ( ( non empty ) ( non empty ) set ) --> (0. Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) ) : ( ( ) ( V49(b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) ) ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) ;
let f be ( ( ) ( ) set ) ;
assume f : ( ( ) ( ) set ) in BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) ) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) equals :: RSSPACE4: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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) ;
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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ;
func PreNorms u -> ( ( non empty ) ( non empty V115() V116() V117() ) Subset of ( ( ) ( non empty ) set ) ) equals :: RSSPACE4: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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real non negative ) Element of REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ) where t is ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) : verum } ;
end;

theorem :: RSSPACE4:11
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace)
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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( non empty ) ( non empty V115() V116() V117() ) Subset of ( ( ) ( non empty ) set ) ) is bounded_above ;

theorem :: RSSPACE4:12
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace)
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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( non empty ) ( non empty V115() V116() V117() ) 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) ;
func BoundedFunctionsNorm (X,Y) -> ( ( Function-like quasi_total ) ( non empty Relation-like BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) ) : ( ( ) ( non empty ) Subset of ) -defined REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) -valued Function-like V23( BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) ) : ( ( ) ( non empty ) Subset of ) ) quasi_total V105() V106() V107() ) Function of BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) ) : ( ( ) ( non empty ) Subset of ) , REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ) means :: RSSPACE4:def 9
 for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) ) : ( ( ) ( 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 V30() V115() V116() V117() V121() ) set ) ) = upper_bound (PreNorms (modetrans (x : ( ( ) ( ) set ) ,X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty V115() V116() V117() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ) ;
end;

theorem :: RSSPACE4:13
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace)
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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ,X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) ) : ( ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ;

theorem :: RSSPACE4:14
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace)
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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) holds (BoundedFunctionsNorm (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) )) : ( ( Function-like quasi_total ) ( non empty Relation-like BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) ) : ( ( ) ( non empty ) Subset of ) -defined REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) -valued Function-like V23( BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) ) : ( ( ) ( non empty ) Subset of ) ) quasi_total V105() V106() V107() ) Function of BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) ) : ( ( ) ( non empty ) Subset of ) , REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty V115() V116() V117() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ) ;

definition
let X be ( ( non empty ) ( non empty ) set ) ;
let Y be ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) ;
func R_NormSpace_of_BoundedFunctions (X,Y) -> ( ( non empty ) ( non empty ) NORMSTR ) equals :: RSSPACE4:def 10
 NORMSTR(# (BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(Zero_ ((BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(RealVectSpace (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() ) RLSStruct ) )) : ( ( ) ( ) Element of BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) ) : ( ( ) ( non empty ) Subset of ) ) ,(Add_ ((BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(RealVectSpace (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() ) RLSStruct ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:(BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) -defined BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) ) : ( ( ) ( non empty ) Subset of ) -valued Function-like V23([:(BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ) quasi_total ) Element of bool [:[:(BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ,(BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ ((BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(RealVectSpace (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() ) RLSStruct ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like [:REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ,(BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) -defined BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) ) : ( ( ) ( non empty ) Subset of ) -valued Function-like V23([:REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ,(BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ) quasi_total ) Element of bool [:[:REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ,(BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) ,(BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,(BoundedFunctionsNorm (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) ) : ( ( ) ( non empty ) Subset of ) -defined REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) -valued Function-like V23( BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) ) : ( ( ) ( non empty ) Subset of ) ) quasi_total V105() V106() V107() ) Function of BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) ) : ( ( ) ( non empty ) Subset of ) , REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ) #) : ( ( strict ) ( non empty strict ) NORMSTR ) ;
end;

theorem :: RSSPACE4:15
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) holds X : ( ( non empty ) ( non empty ) set ) --> (0. Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) ) : ( ( ) ( V49(b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) ) ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) = 0. (R_NormSpace_of_BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) )) : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( V49( R_NormSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) ) : ( ( non empty ) ( non empty ) NORMSTR ) ) ) Element of the carrier of (R_NormSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) )) : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RSSPACE4:16
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace)
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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real non negative ) Element of REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ) <= ||.f : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ) ;

theorem :: RSSPACE4:17
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace)
for f being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ) <= ||.f : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ) ;

theorem :: RSSPACE4:18
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace)
for f being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st f : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = 0. (R_NormSpace_of_BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) )) : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( V49( R_NormSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) ) : ( ( non empty ) ( non empty ) NORMSTR ) ) ) Element of the carrier of (R_NormSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) )) : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) holds
0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ) = ||.f : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ) ;

theorem :: RSSPACE4:19
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace)
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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 (R_NormSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) )) : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: RSSPACE4:20
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace)
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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) = h : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds
for a being ( ( ) ( V11() real ext-real ) Real) holds
( h : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = a : ( ( ) ( V11() real ext-real ) Real) * f : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (R_NormSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) )) : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) = a : ( ( ) ( V11() real ext-real ) Real) * (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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: RSSPACE4:21
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace)
for f, g being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for a being ( ( ) ( V11() real ext-real ) Real) holds
( ( ||.f : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ) implies f : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = 0. (R_NormSpace_of_BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) )) : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( V49( R_NormSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) ) : ( ( non empty ) ( non empty ) NORMSTR ) ) ) Element of the carrier of (R_NormSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) )) : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) ) & ( f : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = 0. (R_NormSpace_of_BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) )) : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( V49( R_NormSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) ) : ( ( non empty ) ( non empty ) NORMSTR ) ) ) Element of the carrier of (R_NormSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) )) : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) implies ||.f : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ) ) & ||.(a : ( ( ) ( V11() real ext-real ) Real) * f : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of (R_NormSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) )) : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ) = (abs a : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ) * ||.f : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ) & ||.(f : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) + g : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of (R_NormSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) )) : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ) <= ||.f : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ) + ||.g : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) ) ) ;

theorem :: RSSPACE4:22
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) holds
( R_NormSpace_of_BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) ) : ( ( non empty ) ( non empty ) NORMSTR ) is reflexive & R_NormSpace_of_BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) ) : ( ( non empty ) ( non empty ) NORMSTR ) is discerning & R_NormSpace_of_BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) ) : ( ( non empty ) ( non empty ) NORMSTR ) is RealNormSpace-like ) ;

theorem :: RSSPACE4:23
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) holds R_NormSpace_of_BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) ) : ( ( non empty ) ( non empty ) NORMSTR ) is ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) ;

registration
let X be ( ( non empty ) ( non empty ) set ) ;
let Y be ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) ;
cluster R_NormSpace_of_BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) ) : ( ( non empty ) ( non empty ) NORMSTR ) -> non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ;
end;

theorem :: RSSPACE4:24
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace)
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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 (R_NormSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) )) : ( ( non empty ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: RSSPACE4:25
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) st Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) is complete holds
for seq being ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of (R_NormSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) )) : ( ( non empty ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) 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 V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of (R_NormSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) )) : ( ( non empty ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) 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 V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of (R_NormSpace_of_BoundedFunctions (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) RealNormSpace) )) : ( ( non empty ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() ) Element of bool REAL : ( ( ) ( non empty V30() V115() V116() V117() V121() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) sequence of ( ( ) ( non empty ) set ) ) is convergent ;

theorem :: RSSPACE4:26
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like complete ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like complete ) RealBanachSpace) holds R_NormSpace_of_BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like complete ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like complete ) RealBanachSpace) ) : ( ( non empty ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) is ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like complete ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like complete ) RealBanachSpace) ;

registration
let X be ( ( non empty ) ( non empty ) set ) ;
let Y be ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like complete ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like complete ) RealBanachSpace) ;
cluster R_NormSpace_of_BoundedFunctions (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like complete ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like complete ) NORMSTR ) ) : ( ( non empty ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like ) NORMSTR ) -> non empty complete ;
end;