:: Banach Space of Bounded Real Sequences
:: by Yasumasa Suzuki
::
:: Received January 6, 2004
:: Copyright (c) 2004-2011 Association of Mizar Users


begin

Lm1: for rseq being Real_Sequence
for K being real number st ( for n being Element of NAT holds rseq . n <= K ) holds
upper_bound (rng rseq) <= K
proof end;

Lm2: for rseq being Real_Sequence st rseq is bounded holds
for n being Element of NAT holds rseq . n <= upper_bound (rng rseq)
proof end;

definition
func the_set_of_BoundedRealSequences -> Subset of Linear_Space_of_RealSequences means :Def1: :: RSSPACE4:def 1
 for x being set holds
( x in it iff ( x in the_set_of_RealSequences & seq_id x is bounded ) );
existence
ex b1 being Subset of Linear_Space_of_RealSequences st
for x being set holds
( x in b1 iff ( x in the_set_of_RealSequences & seq_id x is bounded ) )
proof end;
uniqueness
for b1, b2 being Subset of Linear_Space_of_RealSequences st ( for x being set holds
( x in b1 iff ( x in the_set_of_RealSequences & seq_id x is bounded ) ) ) & ( for x being set holds
( x in b2 iff ( x in the_set_of_RealSequences & seq_id x is bounded ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines the_set_of_BoundedRealSequences RSSPACE4:def 1 :
for b1 being Subset of Linear_Space_of_RealSequences holds
( b1 = the_set_of_BoundedRealSequences iff for x being set holds
( x in b1 iff ( x in the_set_of_RealSequences & seq_id x is bounded ) ) );

registration
cluster the_set_of_BoundedRealSequences -> non empty ;
coherence
not the_set_of_BoundedRealSequences is empty
proof end;
cluster the_set_of_BoundedRealSequences -> linearly-closed ;
coherence
the_set_of_BoundedRealSequences is linearly-closed
proof end;
end;

Lm3: RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is Subspace of Linear_Space_of_RealSequences
by RSSPACE:13;

registration
cluster RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
( RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is Abelian & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is add-associative & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is right_zeroed & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is right_complementable & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is vector-distributive & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is scalar-distributive & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is scalar-associative & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is scalar-unital ) by RSSPACE:13;
end;

Lm4: ( RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is Abelian & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is add-associative & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is right_zeroed & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is right_complementable & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is vector-distributive & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is scalar-distributive & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is scalar-associative & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is scalar-unital )
;

Lm5: ex NORM being Function of the_set_of_BoundedRealSequences,REAL st
for x being set st x in the_set_of_BoundedRealSequences holds
NORM . x = upper_bound (rng (abs (seq_id x)))
proof end;

definition
func linfty_norm -> Function of the_set_of_BoundedRealSequences,REAL means :Def2: :: RSSPACE4:def 2
 for x being set st x in the_set_of_BoundedRealSequences holds
it . x = upper_bound (rng (abs (seq_id x)));
existence
ex b1 being Function of the_set_of_BoundedRealSequences,REAL st
for x being set st x in the_set_of_BoundedRealSequences holds
b1 . x = upper_bound (rng (abs (seq_id x))) by Lm5;
uniqueness
for b1, b2 being Function of the_set_of_BoundedRealSequences,REAL st ( for x being set st x in the_set_of_BoundedRealSequences holds
b1 . x = upper_bound (rng (abs (seq_id x))) ) & ( for x being set st x in the_set_of_BoundedRealSequences holds
b2 . x = upper_bound (rng (abs (seq_id x))) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines linfty_norm RSSPACE4:def 2 :
for b1 being Function of the_set_of_BoundedRealSequences,REAL holds
( b1 = linfty_norm iff for x being set st x in the_set_of_BoundedRealSequences holds
b1 . x = upper_bound (rng (abs (seq_id x))) );

Lm6: for rseq being Real_Sequence st ( for n being Nat holds rseq . n = 0 ) holds
( rseq is bounded & upper_bound (rng (abs rseq)) = 0 )
proof end;

Lm7: for rseq being Real_Sequence st rseq is bounded & upper_bound (rng (abs rseq)) = 0 holds
for n being Nat holds rseq . n = 0
proof end;

theorem :: RSSPACE4:1
canceled;

theorem :: RSSPACE4:2
for rseq being Real_Sequence holds
( ( rseq is bounded & upper_bound (rng (abs rseq)) = 0 ) iff for n being Nat holds rseq . n = 0 ) by Lm6, Lm7;

registration
cluster NORMSTR(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),linfty_norm #) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
( NORMSTR(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),linfty_norm #) is Abelian & NORMSTR(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),linfty_norm #) is add-associative & NORMSTR(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),linfty_norm #) is right_zeroed & NORMSTR(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),linfty_norm #) is right_complementable & NORMSTR(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),linfty_norm #) is vector-distributive & NORMSTR(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),linfty_norm #) is scalar-distributive & NORMSTR(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),linfty_norm #) is scalar-associative & NORMSTR(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),linfty_norm #) is scalar-unital ) by Lm4, RSSPACE3:4;
end;

definition
func linfty_Space -> non empty NORMSTR equals :: RSSPACE4:def 3
 NORMSTR(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),linfty_norm #);
coherence
NORMSTR(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),linfty_norm #) is non empty NORMSTR ;
end;

:: deftheorem defines linfty_Space RSSPACE4:def 3 :
linfty_Space = NORMSTR(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),linfty_norm #);

theorem Th3: :: RSSPACE4:3
( the carrier of linfty_Space = the_set_of_BoundedRealSequences & ( for x being set holds
( x is VECTOR of linfty_Space iff ( x is Real_Sequence & seq_id x is bounded ) ) ) & 0. linfty_Space = Zeroseq & ( for u being VECTOR of linfty_Space holds u = seq_id u ) & ( for u, v being VECTOR of linfty_Space holds u + v = (seq_id u) + (seq_id v) ) & ( for r being Real
for u being VECTOR of linfty_Space holds r * u = r (#) (seq_id u) ) & ( for u being VECTOR of linfty_Space holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) ) & ( for u, v being VECTOR of linfty_Space holds u - v = (seq_id u) - (seq_id v) ) & ( for v being VECTOR of linfty_Space holds seq_id v is bounded ) & ( for v being VECTOR of linfty_Space holds ||.v.|| = upper_bound (rng (abs (seq_id v))) ) )
proof end;

theorem Th4: :: RSSPACE4:4
for x, y being Point of linfty_Space
for a being Real holds
( ( ||.x.|| = 0 implies x = 0. linfty_Space ) & ( x = 0. linfty_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = (abs a) * ||.x.|| )
proof end;

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

theorem :: RSSPACE4:5
for vseq being sequence of linfty_Space st vseq is CCauchy holds
vseq is convergent
proof end;

begin

definition
let X be non empty set ;
let Y be RealNormSpace;
let IT be Function of X, the carrier of Y;
attr IT is bounded means :Def4: :: RSSPACE4:def 4
 ex K being Real st
( 0 <= K & ( for x being Element of X holds ||.(IT . x).|| <= K ) );
end;

:: deftheorem Def4 defines bounded RSSPACE4:def 4 :
for X being non empty set
for Y being RealNormSpace
for IT being Function of X, the carrier of Y holds
( IT is bounded iff ex K being Real st
( 0 <= K & ( for x being Element of X holds ||.(IT . x).|| <= K ) ) );

theorem Th6: :: RSSPACE4:6
for X being non empty set
for Y being RealNormSpace
for f being Function of X, the carrier of Y st ( for x being Element of X holds f . x = 0. Y ) holds
f is bounded
proof end;

registration
let X be non empty set ;
let Y be RealNormSpace;
cluster Relation-like Function-like non empty V14(X) quasi_total bounded Element of bool [:X, the carrier of Y:];
existence
ex b1 being Function of X, the carrier of Y st b1 is bounded
proof end;
end;

definition
let X be non empty set ;
let Y be RealNormSpace;
func BoundedFunctions (X,Y) -> Subset of (RealVectSpace (X,Y)) means :Def5: :: RSSPACE4:def 5
 for x being set holds
( x in it iff x is bounded Function of X, the carrier of Y );
existence
ex b1 being Subset of (RealVectSpace (X,Y)) st
for x being set holds
( x in b1 iff x is bounded Function of X, the carrier of Y )
proof end;
uniqueness
for b1, b2 being Subset of (RealVectSpace (X,Y)) st ( for x being set holds
( x in b1 iff x is bounded Function of X, the carrier of Y ) ) & ( for x being set holds
( x in b2 iff x is bounded Function of X, the carrier of Y ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines BoundedFunctions RSSPACE4:def 5 :
for X being non empty set
for Y being RealNormSpace
for b3 being Subset of (RealVectSpace (X,Y)) holds
( b3 = BoundedFunctions (X,Y) iff for x being set holds
( x in b3 iff x is bounded Function of X, the carrier of Y ) );

registration
let X be non empty set ;
let Y be RealNormSpace;
cluster BoundedFunctions (X,Y) -> non empty ;
coherence
not BoundedFunctions (X,Y) is empty
proof end;
end;

theorem Th7: :: RSSPACE4:7
for X being non empty set
for Y being RealNormSpace holds BoundedFunctions (X,Y) is linearly-closed
proof end;

theorem :: RSSPACE4:8
for X being non empty set
for Y being RealNormSpace holds RLSStruct(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #) is Subspace of RealVectSpace (X,Y) by Th7, RSSPACE:13;

registration
let X be non empty set ;
let Y be RealNormSpace;
cluster RLSStruct(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
( RLSStruct(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #) is Abelian & RLSStruct(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #) is add-associative & RLSStruct(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #) is right_zeroed & RLSStruct(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #) is right_complementable & RLSStruct(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #) is vector-distributive & RLSStruct(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #) is scalar-distributive & RLSStruct(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #) is scalar-associative & RLSStruct(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #) is scalar-unital ) by Th7, RSSPACE:13;
end;

definition
let X be non empty set ;
let Y be RealNormSpace;
func R_VectorSpace_of_BoundedFunctions (X,Y) -> RealLinearSpace equals :: RSSPACE4:def 6
 RLSStruct(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #);
coherence
RLSStruct(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #) is RealLinearSpace ;
end;

:: deftheorem defines R_VectorSpace_of_BoundedFunctions RSSPACE4:def 6 :
for X being non empty set
for Y being RealNormSpace holds R_VectorSpace_of_BoundedFunctions (X,Y) = RLSStruct(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #);

registration
let X be non empty set ;
let Y be RealNormSpace;
cluster R_VectorSpace_of_BoundedFunctions (X,Y) -> strict ;
coherence
R_VectorSpace_of_BoundedFunctions (X,Y) is strict ;
end;

theorem :: RSSPACE4:9
canceled;

theorem Th10: :: RSSPACE4:10
for X being non empty set
for Y being RealNormSpace
for f, g, h being VECTOR of (R_VectorSpace_of_BoundedFunctions (X,Y))
for f9, g9, h9 being bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds
( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) )
proof end;

theorem Th11: :: RSSPACE4:11
for X being non empty set
for Y being RealNormSpace
for f, h being VECTOR of (R_VectorSpace_of_BoundedFunctions (X,Y))
for f9, h9 being bounded Function of X, the carrier of Y st f9 = f & h9 = h holds
for a being Real holds
( h = a * f iff for x being Element of X holds h9 . x = a * (f9 . x) )
proof end;

theorem Th12: :: RSSPACE4:12
for X being non empty set
for Y being RealNormSpace holds 0. (R_VectorSpace_of_BoundedFunctions (X,Y)) = X --> (0. Y)
proof end;

definition
let X be non empty set ;
let Y be RealNormSpace;
let f be set ;
assume A1: f in BoundedFunctions (X,Y) ;
func modetrans (f,X,Y) -> bounded Function of X, the carrier of Y equals :Def7: :: RSSPACE4:def 7
f;
coherence
f is bounded Function of X, the carrier of Y by A1, Def5;
end;

:: deftheorem Def7 defines modetrans RSSPACE4:def 7 :
for X being non empty set
for Y being RealNormSpace
for f being set st f in BoundedFunctions (X,Y) holds
modetrans (f,X,Y) = f;

definition
let X be non empty set ;
let Y be RealNormSpace;
let u be Function of X, the carrier of Y;
func PreNorms u -> non empty Subset of REAL equals :: RSSPACE4:def 8
 { ||.(u . t).|| where t is Element of X : verum } ;
coherence
{ ||.(u . t).|| where t is Element of X : verum } is non empty Subset of REAL
proof end;
end;

:: deftheorem defines PreNorms RSSPACE4:def 8 :
for X being non empty set
for Y being RealNormSpace
for u being Function of X, the carrier of Y holds PreNorms u = { ||.(u . t).|| where t is Element of X : verum } ;

theorem Th13: :: RSSPACE4:13
for X being non empty set
for Y being RealNormSpace
for g being bounded Function of X, the carrier of Y holds PreNorms g is bounded_above
proof end;

theorem :: RSSPACE4:14
for X being non empty set
for Y being RealNormSpace
for g being Function of X, the carrier of Y holds
( g is bounded iff PreNorms g is bounded_above )
proof end;

theorem Th15: :: RSSPACE4:15
for X being non empty set
for Y being RealNormSpace ex NORM being Function of (BoundedFunctions (X,Y)),REAL st
for f being set st f in BoundedFunctions (X,Y) holds
NORM . f = upper_bound (PreNorms (modetrans (f,X,Y)))
proof end;

definition
let X be non empty set ;
let Y be RealNormSpace;
func BoundedFunctionsNorm (X,Y) -> Function of (BoundedFunctions (X,Y)),REAL means :Def9: :: RSSPACE4:def 9
 for x being set st x in BoundedFunctions (X,Y) holds
it . x = upper_bound (PreNorms (modetrans (x,X,Y)));
existence
ex b1 being Function of (BoundedFunctions (X,Y)),REAL st
for x being set st x in BoundedFunctions (X,Y) holds
b1 . x = upper_bound (PreNorms (modetrans (x,X,Y))) by Th15;
uniqueness
for b1, b2 being Function of (BoundedFunctions (X,Y)),REAL st ( for x being set st x in BoundedFunctions (X,Y) holds
b1 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) & ( for x being set st x in BoundedFunctions (X,Y) holds
b2 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines BoundedFunctionsNorm RSSPACE4:def 9 :
for X being non empty set
for Y being RealNormSpace
for b3 being Function of (BoundedFunctions (X,Y)),REAL holds
( b3 = BoundedFunctionsNorm (X,Y) iff for x being set st x in BoundedFunctions (X,Y) holds
b3 . x = upper_bound (PreNorms (modetrans (x,X,Y))) );

theorem Th16: :: RSSPACE4:16
for X being non empty set
for Y being RealNormSpace
for f being bounded Function of X, the carrier of Y holds modetrans (f,X,Y) = f
proof end;

theorem Th17: :: RSSPACE4:17
for X being non empty set
for Y being RealNormSpace
for f being bounded Function of X, the carrier of Y holds (BoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms f)
proof end;

definition
let X be non empty set ;
let Y be RealNormSpace;
func R_NormSpace_of_BoundedFunctions (X,Y) -> non empty NORMSTR equals :: RSSPACE4:def 10
 NORMSTR(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(BoundedFunctionsNorm (X,Y)) #);
coherence
NORMSTR(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(BoundedFunctionsNorm (X,Y)) #) is non empty NORMSTR ;
end;

:: deftheorem defines R_NormSpace_of_BoundedFunctions RSSPACE4:def 10 :
for X being non empty set
for Y being RealNormSpace holds R_NormSpace_of_BoundedFunctions (X,Y) = NORMSTR(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(BoundedFunctionsNorm (X,Y)) #);

theorem Th18: :: RSSPACE4:18
for X being non empty set
for Y being RealNormSpace holds X --> (0. Y) = 0. (R_NormSpace_of_BoundedFunctions (X,Y))
proof end;

theorem Th19: :: RSSPACE4:19
for X being non empty set
for Y being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedFunctions (X,Y))
for g being bounded Function of X, the carrier of Y st g = f holds
for t being Element of X holds ||.(g . t).|| <= ||.f.||
proof end;

theorem :: RSSPACE4:20
for X being non empty set
for Y being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedFunctions (X,Y)) holds 0 <= ||.f.||
proof end;

theorem Th21: :: RSSPACE4:21
for X being non empty set
for Y being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedFunctions (X,Y)) st f = 0. (R_NormSpace_of_BoundedFunctions (X,Y)) holds
0 = ||.f.||
proof end;

theorem Th22: :: RSSPACE4:22
for X being non empty set
for Y being RealNormSpace
for f, g, h being Point of (R_NormSpace_of_BoundedFunctions (X,Y))
for f9, g9, h9 being bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds
( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) )
proof end;

theorem Th23: :: RSSPACE4:23
for X being non empty set
for Y being RealNormSpace
for f, h being Point of (R_NormSpace_of_BoundedFunctions (X,Y))
for f9, h9 being bounded Function of X, the carrier of Y st f9 = f & h9 = h holds
for a being Real holds
( h = a * f iff for x being Element of X holds h9 . x = a * (f9 . x) )
proof end;

theorem Th24: :: RSSPACE4:24
for X being non empty set
for Y being RealNormSpace
for f, g being Point of (R_NormSpace_of_BoundedFunctions (X,Y))
for a being Real holds
( ( ||.f.|| = 0 implies f = 0. (R_NormSpace_of_BoundedFunctions (X,Y)) ) & ( f = 0. (R_NormSpace_of_BoundedFunctions (X,Y)) implies ||.f.|| = 0 ) & ||.(a * f).|| = (abs a) * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )
proof end;

theorem Th25: :: RSSPACE4:25
for X being non empty set
for Y being RealNormSpace holds
( R_NormSpace_of_BoundedFunctions (X,Y) is reflexive & R_NormSpace_of_BoundedFunctions (X,Y) is discerning & R_NormSpace_of_BoundedFunctions (X,Y) is RealNormSpace-like )
proof end;

theorem Th26: :: RSSPACE4:26
for X being non empty set
for Y being RealNormSpace holds R_NormSpace_of_BoundedFunctions (X,Y) is RealNormSpace
proof end;

registration
let X be non empty set ;
let Y be RealNormSpace;
cluster R_NormSpace_of_BoundedFunctions (X,Y) -> non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ;
coherence
( R_NormSpace_of_BoundedFunctions (X,Y) is reflexive & R_NormSpace_of_BoundedFunctions (X,Y) is discerning & R_NormSpace_of_BoundedFunctions (X,Y) is RealNormSpace-like & R_NormSpace_of_BoundedFunctions (X,Y) is vector-distributive & R_NormSpace_of_BoundedFunctions (X,Y) is scalar-distributive & R_NormSpace_of_BoundedFunctions (X,Y) is scalar-associative & R_NormSpace_of_BoundedFunctions (X,Y) is scalar-unital & R_NormSpace_of_BoundedFunctions (X,Y) is Abelian & R_NormSpace_of_BoundedFunctions (X,Y) is add-associative & R_NormSpace_of_BoundedFunctions (X,Y) is right_zeroed & R_NormSpace_of_BoundedFunctions (X,Y) is right_complementable ) by Th26;
end;

theorem Th27: :: RSSPACE4:27
for X being non empty set
for Y being RealNormSpace
for f, g, h being Point of (R_NormSpace_of_BoundedFunctions (X,Y))
for f9, g9, h9 being bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds
( h = f - g iff for x being Element of X holds h9 . x = (f9 . x) - (g9 . x) )
proof end;

Lm8: for e being Real
for seq being Real_Sequence st seq is convergent & ex k being Element of NAT st
for i being Element of NAT st k <= i holds
seq . i <= e holds
lim seq <= e
proof end;

theorem Th28: :: RSSPACE4:28
for X being non empty set
for Y being RealNormSpace st Y is complete holds
for seq being sequence of (R_NormSpace_of_BoundedFunctions (X,Y)) st seq is CCauchy holds
seq is convergent
proof end;

theorem Th29: :: RSSPACE4:29
for X being non empty set
for Y being RealBanachSpace holds R_NormSpace_of_BoundedFunctions (X,Y) is RealBanachSpace
proof end;

registration
let X be non empty set ;
let Y be RealBanachSpace;
cluster R_NormSpace_of_BoundedFunctions (X,Y) -> non empty complete ;
coherence
R_NormSpace_of_BoundedFunctions (X,Y) is complete by Th29;
end;