:: RSSPACE4 semantic presentation 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 let rseq be Real_Sequence; ::_thesis: for K being real number st ( for n being Element of NAT holds rseq . n <= K ) holds upper_bound (rng rseq) <= K let K be real number ; ::_thesis: ( ( for n being Element of NAT holds rseq . n <= K ) implies upper_bound (rng rseq) <= K ) assume A1: for n being Element of NAT holds rseq . n <= K ; ::_thesis: upper_bound (rng rseq) <= K now__::_thesis:_for_s_being_real_number_st_s_in_rng_rseq_holds_ s_<=_K let s be real number ; ::_thesis: ( s in rng rseq implies s <= K ) assume s in rng rseq ; ::_thesis: s <= K then ex n being set st ( n in NAT & rseq . n = s ) by FUNCT_2:11; hence s <= K by A1; ::_thesis: verum end; hence upper_bound (rng rseq) <= K by SEQ_4:45; ::_thesis: verum 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 let rseq be Real_Sequence; ::_thesis: ( rseq is bounded implies for n being Element of NAT holds rseq . n <= upper_bound (rng rseq) ) assume rseq is bounded ; ::_thesis: for n being Element of NAT holds rseq . n <= upper_bound (rng rseq) then rng rseq is real-bounded by MEASURE6:39; then A1: rng rseq is bounded_above by XXREAL_2:def_11; let n be Element of NAT ; ::_thesis: rseq . n <= upper_bound (rng rseq) NAT = dom rseq by FUNCT_2:def_1; then rseq . n in rng rseq by FUNCT_1:3; hence rseq . n <= upper_bound (rng rseq) by A1, SEQ_4:def_1; ::_thesis: verum 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 defpred S1[ set ] means seq_id $1 is bounded ; consider IT being set such that A1: for x being set holds ( x in IT iff ( x in the_set_of_RealSequences & S1[x] ) ) from XBOOLE_0:sch_1(); for x being set st x in IT holds x in the_set_of_RealSequences by A1; then IT is Subset of the_set_of_RealSequences by TARSKI:def_3; hence 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 ) ) by A1, RSSPACE:def_7; ::_thesis: verum 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 let X1, X2 be Subset of Linear_Space_of_RealSequences; ::_thesis: ( ( for x being set holds ( x in X1 iff ( x in the_set_of_RealSequences & seq_id x is bounded ) ) ) & ( for x being set holds ( x in X2 iff ( x in the_set_of_RealSequences & seq_id x is bounded ) ) ) implies X1 = X2 ) assume that A2: for x being set holds ( x in X1 iff ( x in the_set_of_RealSequences & seq_id x is bounded ) ) and A3: for x being set holds ( x in X2 iff ( x in the_set_of_RealSequences & seq_id x is bounded ) ) ; ::_thesis: X1 = X2 thus X1 c= X2 :: according to XBOOLE_0:def_10 ::_thesis: X2 c= X1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X1 or x in X2 ) assume x in X1 ; ::_thesis: x in X2 then ( x in the_set_of_RealSequences & seq_id x is bounded ) by A2; hence x in X2 by A3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X2 or x in X1 ) assume x in X2 ; ::_thesis: x in X1 then ( x in the_set_of_RealSequences & seq_id x is bounded ) by A3; hence x in X1 by A2; ::_thesis: verum 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 seq_id Zeroseq is bounded proof reconsider rseq = seq_id Zeroseq as Real_Sequence ; for n being Nat holds rseq . n = 0 proof let n be Nat; ::_thesis: rseq . n = 0 n in NAT by ORDINAL1:def_12; hence rseq . n = 0 by RSSPACE:def_6; ::_thesis: verum end; then rseq is constant by VALUED_0:def_18; hence seq_id Zeroseq is bounded ; ::_thesis: verum end; hence not the_set_of_BoundedRealSequences is empty by Def1; ::_thesis: verum end; cluster the_set_of_BoundedRealSequences -> linearly-closed ; coherence the_set_of_BoundedRealSequences is linearly-closed proof set W = the_set_of_BoundedRealSequences ; A1: for a being Real for v being VECTOR of Linear_Space_of_RealSequences st v in the_set_of_BoundedRealSequences holds a * v in the_set_of_BoundedRealSequences proof let a be Real; ::_thesis: for v being VECTOR of Linear_Space_of_RealSequences st v in the_set_of_BoundedRealSequences holds a * v in the_set_of_BoundedRealSequences let v be VECTOR of Linear_Space_of_RealSequences; ::_thesis: ( v in the_set_of_BoundedRealSequences implies a * v in the_set_of_BoundedRealSequences ) assume v in the_set_of_BoundedRealSequences ; ::_thesis: a * v in the_set_of_BoundedRealSequences then A2: seq_id v is bounded by Def1; seq_id (a * v) = seq_id (a (#) (seq_id v)) by RSSPACE:3, RSSPACE:def_7 .= a (#) (seq_id v) by RSSPACE:1 ; then seq_id (a * v) is bounded by A2, SEQM_3:37; hence a * v in the_set_of_BoundedRealSequences by Def1, RSSPACE:def_7; ::_thesis: verum end; for v, u being VECTOR of Linear_Space_of_RealSequences st v in the_set_of_BoundedRealSequences & u in the_set_of_BoundedRealSequences holds v + u in the_set_of_BoundedRealSequences proof let v, u be VECTOR of Linear_Space_of_RealSequences; ::_thesis: ( v in the_set_of_BoundedRealSequences & u in the_set_of_BoundedRealSequences implies v + u in the_set_of_BoundedRealSequences ) assume ( v in the_set_of_BoundedRealSequences & u in the_set_of_BoundedRealSequences ) ; ::_thesis: v + u in the_set_of_BoundedRealSequences then A3: ( seq_id v is bounded & seq_id u is bounded ) by Def1; seq_id (v + u) = seq_id ((seq_id v) + (seq_id u)) by RSSPACE:2, RSSPACE:def_7 .= (seq_id v) + (seq_id u) by RSSPACE:1 ; hence v + u in the_set_of_BoundedRealSequences by A3, Def1, RSSPACE:def_7; ::_thesis: verum end; hence the_set_of_BoundedRealSequences is linearly-closed by A1, RLSUB_1:def_1; ::_thesis: verum 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:11; 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:11; 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 ) ; 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))) proof deffunc H1( set ) -> Element of REAL = upper_bound (rng (abs (seq_id $1))); A1: for z being set st z in the_set_of_BoundedRealSequences holds H1(z) in REAL ; ex f being Function of the_set_of_BoundedRealSequences,REAL st for x being set st x in the_set_of_BoundedRealSequences holds f . x = H1(x) from FUNCT_2:sch_2(A1); hence 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))) ; ::_thesis: verum end; 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 let NORM1, NORM2 be Function of the_set_of_BoundedRealSequences,REAL; ::_thesis: ( ( for x being set st x in the_set_of_BoundedRealSequences holds NORM1 . x = upper_bound (rng (abs (seq_id x))) ) & ( for x being set st x in the_set_of_BoundedRealSequences holds NORM2 . x = upper_bound (rng (abs (seq_id x))) ) implies NORM1 = NORM2 ) assume that A2: for x being set st x in the_set_of_BoundedRealSequences holds NORM1 . x = upper_bound (rng (abs (seq_id x))) and A3: for x being set st x in the_set_of_BoundedRealSequences holds NORM2 . x = upper_bound (rng (abs (seq_id x))) ; ::_thesis: NORM1 = NORM2 A4: for z being set st z in the_set_of_BoundedRealSequences holds NORM1 . z = NORM2 . z proof let z be set ; ::_thesis: ( z in the_set_of_BoundedRealSequences implies NORM1 . z = NORM2 . z ) assume A5: z in the_set_of_BoundedRealSequences ; ::_thesis: NORM1 . z = NORM2 . z NORM1 . z = upper_bound (rng (abs (seq_id z))) by A2, A5; hence NORM1 . z = NORM2 . z by A3, A5; ::_thesis: verum end; ( dom NORM1 = the_set_of_BoundedRealSequences & dom NORM2 = the_set_of_BoundedRealSequences ) by FUNCT_2:def_1; hence NORM1 = NORM2 by A4, FUNCT_1:2; ::_thesis: verum 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))) ); Lm5: 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 let rseq be Real_Sequence; ::_thesis: ( ( for n being Nat holds rseq . n = 0 ) implies ( rseq is bounded & upper_bound (rng (abs rseq)) = 0 ) ) assume A1: for n being Nat holds rseq . n = 0 ; ::_thesis: ( rseq is bounded & upper_bound (rng (abs rseq)) = 0 ) A2: for n being Nat holds (abs rseq) . n = 0 proof let n be Nat; ::_thesis: (abs rseq) . n = 0 n in NAT by ORDINAL1:def_12; then A3: (abs rseq) . n = abs (rseq . n) by SEQ_1:12; rseq . n = 0 by A1; hence (abs rseq) . n = 0 by A3, ABSVALUE:2; ::_thesis: verum end; rng (abs rseq) c= {0} proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (abs rseq) or y in {0} ) assume y in rng (abs rseq) ; ::_thesis: y in {0} then ex n being set st ( n in NAT & (abs rseq) . n = y ) by FUNCT_2:11; then y = 0 by A2; hence y in {0} by TARSKI:def_1; ::_thesis: verum end; then A4: rng (abs rseq) = {0} by ZFMISC_1:33; rseq is constant by A1, VALUED_0:def_18; hence ( rseq is bounded & upper_bound (rng (abs rseq)) = 0 ) by A4, SEQ_4:9; ::_thesis: verum end; Lm6: 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 let rseq be Real_Sequence; ::_thesis: ( rseq is bounded & upper_bound (rng (abs rseq)) = 0 implies for n being Nat holds rseq . n = 0 ) assume A1: ( rseq is bounded & upper_bound (rng (abs rseq)) = 0 ) ; ::_thesis: for n being Nat holds rseq . n = 0 let n be Nat; ::_thesis: rseq . n = 0 A2: n in NAT by ORDINAL1:def_12; 0 <= abs (rseq . n) by COMPLEX1:46; then 0 <= (abs rseq) . n by A2, SEQ_1:12; then (abs rseq) . n = 0 by A1, A2, Lm2; then abs (rseq . n) = 0 by A2, SEQ_1:12; hence rseq . n = 0 by ABSVALUE:2; ::_thesis: verum end; theorem :: RSSPACE4:1 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 Lm5, Lm6; 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:2; 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 Th2: :: RSSPACE4:2 ( 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 set l1 = linfty_Space ; A1: 0. linfty_Space = 0. Linear_Space_of_RealSequences by RSSPACE:def_10 .= Zeroseq by RSSPACE:def_7 ; A2: for x being set holds ( x is Element of linfty_Space iff ( x is Real_Sequence & seq_id x is bounded ) ) proof let x be set ; ::_thesis: ( x is Element of linfty_Space iff ( x is Real_Sequence & seq_id x is bounded ) ) ( x in the_set_of_RealSequences iff x is Real_Sequence ) by RSSPACE:def_1; hence ( x is Element of linfty_Space iff ( x is Real_Sequence & seq_id x is bounded ) ) by Def1; ::_thesis: verum end; A3: for u, v being VECTOR of linfty_Space holds u + v = (seq_id u) + (seq_id v) proof let u, v be VECTOR of linfty_Space; ::_thesis: u + v = (seq_id u) + (seq_id v) reconsider u1 = u, v1 = v as VECTOR of Linear_Space_of_RealSequences by Lm3, RLSUB_1:10; set L1 = Linear_Space_of_RealSequences ; set W = the_set_of_BoundedRealSequences ; dom the addF of Linear_Space_of_RealSequences = [: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:] by FUNCT_2:def_1; then A4: dom ( the addF of Linear_Space_of_RealSequences || the_set_of_BoundedRealSequences) = [:the_set_of_BoundedRealSequences,the_set_of_BoundedRealSequences:] by RELAT_1:62; u + v = ( the addF of Linear_Space_of_RealSequences || the_set_of_BoundedRealSequences) . [u,v] by RSSPACE:def_8 .= u1 + v1 by A4, FUNCT_1:47 ; hence u + v = (seq_id u) + (seq_id v) by RSSPACE:2, RSSPACE:def_7; ::_thesis: verum end; A5: for r being Real for u being VECTOR of linfty_Space holds r * u = r (#) (seq_id u) proof let r be Real; ::_thesis: for u being VECTOR of linfty_Space holds r * u = r (#) (seq_id u) let u be VECTOR of linfty_Space; ::_thesis: r * u = r (#) (seq_id u) reconsider u1 = u as VECTOR of Linear_Space_of_RealSequences by Lm3, RLSUB_1:10; set L1 = Linear_Space_of_RealSequences ; set W = the_set_of_BoundedRealSequences ; dom the Mult of Linear_Space_of_RealSequences = [:REAL, the carrier of Linear_Space_of_RealSequences:] by FUNCT_2:def_1; then A6: dom ( the Mult of Linear_Space_of_RealSequences | [:REAL,the_set_of_BoundedRealSequences:]) = [:REAL,the_set_of_BoundedRealSequences:] by RELAT_1:62, ZFMISC_1:96; r * u = ( the Mult of Linear_Space_of_RealSequences | [:REAL,the_set_of_BoundedRealSequences:]) . [r,u] by RSSPACE:def_9 .= r * u1 by A6, FUNCT_1:47 ; hence r * u = r (#) (seq_id u) by RSSPACE:3, RSSPACE:def_7; ::_thesis: verum end; A7: for u being VECTOR of linfty_Space holds u = seq_id u proof let u be VECTOR of linfty_Space; ::_thesis: u = seq_id u u is VECTOR of Linear_Space_of_RealSequences by Lm3, RLSUB_1:10; hence u = seq_id u by RSSPACE:def_2, RSSPACE:def_7; ::_thesis: verum end; A8: for u being VECTOR of linfty_Space holds ( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) proof let u be VECTOR of linfty_Space; ::_thesis: ( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) - u = (- 1) * u by RLVECT_1:16 .= - (seq_id u) by A5 ; hence ( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) by A7; ::_thesis: verum end; for u, v being VECTOR of linfty_Space holds u - v = (seq_id u) - (seq_id v) proof let u, v be VECTOR of linfty_Space; ::_thesis: u - v = (seq_id u) - (seq_id v) thus u - v = (seq_id u) + (seq_id (- v)) by A3 .= (seq_id u) - (seq_id v) by A8 ; ::_thesis: verum end; hence ( 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))) ) ) by A2, A7, A3, A5, A8, A1, Def2; ::_thesis: verum end; theorem Th3: :: RSSPACE4:3 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 let x, y be Point of linfty_Space; ::_thesis: 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.|| ) let a be Real; ::_thesis: ( ( ||.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.|| ) A1: for n being Element of NAT holds (abs (a (#) (seq_id x))) . n = (abs a) * ((abs (seq_id x)) . n) proof let n be Element of NAT ; ::_thesis: (abs (a (#) (seq_id x))) . n = (abs a) * ((abs (seq_id x)) . n) (abs (a (#) (seq_id x))) . n = abs ((a (#) (seq_id x)) . n) by SEQ_1:12 .= abs (a * ((seq_id x) . n)) by SEQ_1:9 .= (abs a) * (abs ((seq_id x) . n)) by COMPLEX1:65 .= (abs a) * ((abs (seq_id x)) . n) by SEQ_1:12 ; hence (abs (a (#) (seq_id x))) . n = (abs a) * ((abs (seq_id x)) . n) ; ::_thesis: verum end; (abs (seq_id x)) . 1 = abs ((seq_id x) . 1) by SEQ_1:12; then A2: 0 <= (abs (seq_id x)) . 1 by COMPLEX1:46; A3: for n being Element of NAT holds (abs (seq_id (x + y))) . n = abs (((seq_id x) . n) + ((seq_id y) . n)) proof let n be Element of NAT ; ::_thesis: (abs (seq_id (x + y))) . n = abs (((seq_id x) . n) + ((seq_id y) . n)) (abs (seq_id (x + y))) . n = (abs (seq_id ((seq_id x) + (seq_id y)))) . n by Th2 .= (abs ((seq_id x) + (seq_id y))) . n by RSSPACE:1 .= abs (((seq_id x) + (seq_id y)) . n) by SEQ_1:12 .= abs (((seq_id x) . n) + ((seq_id y) . n)) by SEQ_1:7 ; hence (abs (seq_id (x + y))) . n = abs (((seq_id x) . n) + ((seq_id y) . n)) ; ::_thesis: verum end; A4: for n being Element of NAT holds (abs (seq_id (x + y))) . n <= ((abs (seq_id x)) . n) + ((abs (seq_id y)) . n) proof let n be Element of NAT ; ::_thesis: (abs (seq_id (x + y))) . n <= ((abs (seq_id x)) . n) + ((abs (seq_id y)) . n) abs (((seq_id x) . n) + ((seq_id y) . n)) <= (abs ((seq_id x) . n)) + (abs ((seq_id y) . n)) by COMPLEX1:56; then (abs (seq_id (x + y))) . n <= (abs ((seq_id x) . n)) + (abs ((seq_id y) . n)) by A3; then (abs (seq_id (x + y))) . n <= ((abs (seq_id x)) . n) + (abs ((seq_id y) . n)) by SEQ_1:12; hence (abs (seq_id (x + y))) . n <= ((abs (seq_id x)) . n) + ((abs (seq_id y)) . n) by SEQ_1:12; ::_thesis: verum end; A5: for n being Element of NAT holds (abs (seq_id (x + y))) . n <= ((abs (seq_id x)) + (abs (seq_id y))) . n proof let n be Element of NAT ; ::_thesis: (abs (seq_id (x + y))) . n <= ((abs (seq_id x)) + (abs (seq_id y))) . n ((abs (seq_id x)) . n) + ((abs (seq_id y)) . n) = ((abs (seq_id x)) + (abs (seq_id y))) . n by SEQ_1:7; hence (abs (seq_id (x + y))) . n <= ((abs (seq_id x)) + (abs (seq_id y))) . n by A4; ::_thesis: verum end; A6: now__::_thesis:_(_x_=_0._linfty_Space_implies_||.x.||_=_0_) assume A7: x = 0. linfty_Space ; ::_thesis: ||.x.|| = 0 A8: for n being Nat holds (seq_id x) . n = 0 proof let n be Nat; ::_thesis: (seq_id x) . n = 0 n in NAT by ORDINAL1:def_12; hence (seq_id x) . n = 0 by A7, Th2, RSSPACE:def_6; ::_thesis: verum end; thus ||.x.|| = upper_bound (rng (abs (seq_id x))) by Th2 .= 0 by A8, Lm5 ; ::_thesis: verum end; seq_id x is bounded by Def1; then A9: 0 <= upper_bound (rng (abs (seq_id x))) by A2, Lm2; seq_id x is bounded by Def1; then rng (abs (seq_id x)) is real-bounded by MEASURE6:39; then A10: rng (abs (seq_id x)) is bounded_above by XXREAL_2:def_11; A11: now__::_thesis:_(_||.x.||_=_0_implies_x_=_0._linfty_Space_) A12: x in the_set_of_RealSequences by Def1; assume A13: ||.x.|| = 0 ; ::_thesis: x = 0. linfty_Space ( ||.x.|| = upper_bound (rng (abs (seq_id x))) & seq_id x is bounded ) by Th2; then for n being Element of NAT holds 0 = (seq_id x) . n by A13, Lm6; hence x = 0. linfty_Space by A12, Th2, RSSPACE:def_6; ::_thesis: verum end; A14: seq_id y is bounded by Def1; A15: seq_id x is bounded by Def1; now__::_thesis:_for_n_being_Element_of_NAT_holds_(abs_(seq_id_(x_+_y)))_._n_<=_(upper_bound_(rng_(abs_(seq_id_x))))_+_(upper_bound_(rng_(abs_(seq_id_y)))) let n be Element of NAT ; ::_thesis: (abs (seq_id (x + y))) . n <= (upper_bound (rng (abs (seq_id x)))) + (upper_bound (rng (abs (seq_id y)))) A16: (abs (seq_id y)) . n <= upper_bound (rng (abs (seq_id y))) by A14, Lm2; ( ((abs (seq_id x)) + (abs (seq_id y))) . n = ((abs (seq_id x)) . n) + ((abs (seq_id y)) . n) & (abs (seq_id x)) . n <= upper_bound (rng (abs (seq_id x))) ) by A15, Lm2, SEQ_1:7; then A17: ((abs (seq_id x)) + (abs (seq_id y))) . n <= (upper_bound (rng (abs (seq_id x)))) + (upper_bound (rng (abs (seq_id y)))) by A16, XREAL_1:7; (abs (seq_id (x + y))) . n <= ((abs (seq_id x)) + (abs (seq_id y))) . n by A5; hence (abs (seq_id (x + y))) . n <= (upper_bound (rng (abs (seq_id x)))) + (upper_bound (rng (abs (seq_id y)))) by A17, XXREAL_0:2; ::_thesis: verum end; then A18: upper_bound (rng (abs (seq_id (x + y)))) <= (upper_bound (rng (abs (seq_id x)))) + (upper_bound (rng (abs (seq_id y)))) by Lm1; A19: ( ||.y.|| = upper_bound (rng (abs (seq_id y))) & upper_bound (rng (abs (seq_id (x + y)))) = ||.(x + y).|| ) by Th2; ||.(a * x).|| = upper_bound (rng (abs (seq_id (a * x)))) by Th2 .= upper_bound (rng (abs (seq_id (a (#) (seq_id x))))) by Th2 .= upper_bound (rng (abs (a (#) (seq_id x)))) by RSSPACE:1 .= upper_bound (rng ((abs a) (#) (abs (seq_id x)))) by A1, SEQ_1:9 .= upper_bound ((abs a) ** (rng (abs (seq_id x)))) by INTEGRA2:17 .= (abs a) * (upper_bound (rng (abs (seq_id x)))) by A10, COMPLEX1:46, INTEGRA2:13 .= (abs a) * ||.x.|| by Th2 ; hence ( ( ||.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.|| ) by A11, A6, A9, A19, A18, Th2; ::_thesis: verum 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 thus ||.(0. linfty_Space).|| = 0 by Th3; :: according to NORMSP_0:def_6 ::_thesis: ( 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 ) thus ( 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 ) by Th3, NORMSP_0:def_5, NORMSP_1:def_1; ::_thesis: verum end; end; theorem :: RSSPACE4:4 for vseq being sequence of linfty_Space st vseq is Cauchy_sequence_by_Norm holds vseq is convergent proof let vseq be sequence of linfty_Space; ::_thesis: ( vseq is Cauchy_sequence_by_Norm implies vseq is convergent ) assume A1: vseq is Cauchy_sequence_by_Norm ; ::_thesis: vseq is convergent defpred S1[ set , set ] means ex i being Element of NAT st ( $1 = i & ex rseqi being Real_Sequence st ( ( for n being Element of NAT holds rseqi . n = (seq_id (vseq . n)) . i ) & rseqi is convergent & $2 = lim rseqi ) ); A2: for x being set st x in NAT holds ex y being set st ( y in REAL & S1[x,y] ) proof let x be set ; ::_thesis: ( x in NAT implies ex y being set st ( y in REAL & S1[x,y] ) ) assume x in NAT ; ::_thesis: ex y being set st ( y in REAL & S1[x,y] ) then reconsider i = x as Element of NAT ; deffunc H1( Nat) -> Element of REAL = (seq_id (vseq . $1)) . i; consider rseqi being Real_Sequence such that A3: for n being Element of NAT holds rseqi . n = H1(n) from SEQ_1:sch_1(); take lim rseqi ; ::_thesis: ( lim rseqi in REAL & S1[x, lim rseqi] ) now__::_thesis:_for_e_being_real_number_st_e_>_0_holds_ ex_k_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_k_<=_m_holds_ abs_((rseqi_._m)_-_(rseqi_._k))_<_e let e be real number ; ::_thesis: ( e > 0 implies ex k being Element of NAT st for m being Element of NAT st k <= m holds abs ((rseqi . m) - (rseqi . k)) < e ) assume A4: e > 0 ; ::_thesis: ex k being Element of NAT st for m being Element of NAT st k <= m holds abs ((rseqi . m) - (rseqi . k)) < e thus ex k being Element of NAT st for m being Element of NAT st k <= m holds abs ((rseqi . m) - (rseqi . k)) < e ::_thesis: verum proof e is Real by XREAL_0:def_1; then consider k being Element of NAT such that A5: for n, m being Element of NAT st n >= k & m >= k holds ||.((vseq . n) - (vseq . m)).|| < e by A1, A4, RSSPACE3:8; take k ; ::_thesis: for m being Element of NAT st k <= m holds abs ((rseqi . m) - (rseqi . k)) < e let m be Element of NAT ; ::_thesis: ( k <= m implies abs ((rseqi . m) - (rseqi . k)) < e ) assume A6: k <= m ; ::_thesis: abs ((rseqi . m) - (rseqi . k)) < e seq_id ((vseq . m) - (vseq . k)) is bounded by Def1; then A7: (abs (seq_id ((vseq . m) - (vseq . k)))) . i <= upper_bound (rng (abs (seq_id ((vseq . m) - (vseq . k))))) by Lm2; seq_id ((vseq . m) - (vseq . k)) = seq_id ((seq_id (vseq . m)) - (seq_id (vseq . k))) by Th2 .= (seq_id (vseq . m)) + (- (seq_id (vseq . k))) by RSSPACE:1 ; then (seq_id ((vseq . m) - (vseq . k))) . i = ((seq_id (vseq . m)) . i) + ((- (seq_id (vseq . k))) . i) by SEQ_1:7 .= ((seq_id (vseq . m)) . i) + (- ((seq_id (vseq . k)) . i)) by SEQ_1:10 .= ((seq_id (vseq . m)) . i) - ((seq_id (vseq . k)) . i) .= (rseqi . m) - ((seq_id (vseq . k)) . i) by A3 .= (rseqi . m) - (rseqi . k) by A3 ; then A8: abs ((rseqi . m) - (rseqi . k)) = (abs (seq_id ((vseq . m) - (vseq . k)))) . i by SEQ_1:12; ||.((vseq . m) - (vseq . k)).|| = upper_bound (rng (abs (seq_id ((vseq . m) - (vseq . k))))) by Th2; then upper_bound (rng (abs (seq_id ((vseq . m) - (vseq . k))))) < e by A5, A6; hence abs ((rseqi . m) - (rseqi . k)) < e by A7, A8, XXREAL_0:2; ::_thesis: verum end; end; then rseqi is convergent by SEQ_4:41; hence ( lim rseqi in REAL & S1[x, lim rseqi] ) by A3; ::_thesis: verum end; consider f being Function of NAT,REAL such that A9: for x being set st x in NAT holds S1[x,f . x] from FUNCT_2:sch_1(A2); reconsider tseq = f as Real_Sequence ; A10: now__::_thesis:_for_i_being_Element_of_NAT_ex_rseqi_being_Real_Sequence_st_ (_(_for_n_being_Element_of_NAT_holds_rseqi_._n_=_(seq_id_(vseq_._n))_._i_)_&_rseqi_is_convergent_&_tseq_._i_=_lim_rseqi_) let i be Element of NAT ; ::_thesis: ex rseqi being Real_Sequence st ( ( for n being Element of NAT holds rseqi . n = (seq_id (vseq . n)) . i ) & rseqi is convergent & tseq . i = lim rseqi ) reconsider x = i as set ; ex i0 being Element of NAT st ( x = i0 & ex rseqi being Real_Sequence st ( ( for n being Element of NAT holds rseqi . n = (seq_id (vseq . n)) . i0 ) & rseqi is convergent & f . x = lim rseqi ) ) by A9; hence ex rseqi being Real_Sequence st ( ( for n being Element of NAT holds rseqi . n = (seq_id (vseq . n)) . i ) & rseqi is convergent & tseq . i = lim rseqi ) ; ::_thesis: verum end; A11: for e being Real st e > 0 holds ex k being Element of NAT st for n being Element of NAT st n >= k holds ( abs ((seq_id tseq) - (seq_id (vseq . n))) is bounded & upper_bound (rng (abs ((seq_id tseq) - (seq_id (vseq . n))))) <= e ) proof let e be Real; ::_thesis: ( e > 0 implies ex k being Element of NAT st for n being Element of NAT st n >= k holds ( abs ((seq_id tseq) - (seq_id (vseq . n))) is bounded & upper_bound (rng (abs ((seq_id tseq) - (seq_id (vseq . n))))) <= e ) ) assume A12: e > 0 ; ::_thesis: ex k being Element of NAT st for n being Element of NAT st n >= k holds ( abs ((seq_id tseq) - (seq_id (vseq . n))) is bounded & upper_bound (rng (abs ((seq_id tseq) - (seq_id (vseq . n))))) <= e ) consider k being Element of NAT such that A13: for n, m being Element of NAT st n >= k & m >= k holds ||.((vseq . n) - (vseq . m)).|| < e by A1, A12, RSSPACE3:8; A14: for m, n being Element of NAT st n >= k & m >= k holds ( abs (seq_id ((vseq . n) - (vseq . m))) is bounded & upper_bound (rng (abs (seq_id ((vseq . n) - (vseq . m))))) < e ) proof let m, n be Element of NAT ; ::_thesis: ( n >= k & m >= k implies ( abs (seq_id ((vseq . n) - (vseq . m))) is bounded & upper_bound (rng (abs (seq_id ((vseq . n) - (vseq . m))))) < e ) ) assume ( n >= k & m >= k ) ; ::_thesis: ( abs (seq_id ((vseq . n) - (vseq . m))) is bounded & upper_bound (rng (abs (seq_id ((vseq . n) - (vseq . m))))) < e ) then A15: ||.((vseq . n) - (vseq . m)).|| < e by A13; seq_id ((vseq . n) - (vseq . m)) is bounded by Def1; hence ( abs (seq_id ((vseq . n) - (vseq . m))) is bounded & upper_bound (rng (abs (seq_id ((vseq . n) - (vseq . m))))) < e ) by A15, Def2; ::_thesis: verum end; A16: for n, i being Element of NAT for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (abs (seq_id ((vseq . m) - (vseq . n)))) . i ) holds ( rseq is convergent & lim rseq = (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i ) proof let n be Element of NAT ; ::_thesis: for i being Element of NAT for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (abs (seq_id ((vseq . m) - (vseq . n)))) . i ) holds ( rseq is convergent & lim rseq = (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i ) A17: for m, k being Element of NAT holds seq_id ((vseq . m) - (vseq . k)) = (seq_id (vseq . m)) - (seq_id (vseq . k)) proof let m, k be Element of NAT ; ::_thesis: seq_id ((vseq . m) - (vseq . k)) = (seq_id (vseq . m)) - (seq_id (vseq . k)) seq_id ((vseq . m) - (vseq . k)) = seq_id ((seq_id (vseq . m)) - (seq_id (vseq . k))) by Th2; hence seq_id ((vseq . m) - (vseq . k)) = (seq_id (vseq . m)) - (seq_id (vseq . k)) by RSSPACE:1; ::_thesis: verum end; now__::_thesis:_for_i_being_Element_of_NAT_ for_rseq_being_Real_Sequence_st_(_for_m_being_Element_of_NAT_holds_rseq_._m_=_(abs_(seq_id_((vseq_._m)_-_(vseq_._n))))_._i_)_holds_ (_rseq_is_convergent_&_lim_rseq_=_(abs_((seq_id_tseq)_-_(seq_id_(vseq_._n))))_._i_) let i be Element of NAT ; ::_thesis: for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (abs (seq_id ((vseq . m) - (vseq . n)))) . i ) holds ( rseq is convergent & lim rseq = (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i ) consider rseqi being Real_Sequence such that A18: for n being Element of NAT holds rseqi . n = (seq_id (vseq . n)) . i and A19: ( rseqi is convergent & tseq . i = lim rseqi ) by A10; now__::_thesis:_for_rseq_being_Real_Sequence_st_(_for_m_being_Element_of_NAT_holds_rseq_._m_=_(abs_(seq_id_((vseq_._m)_-_(vseq_._n))))_._i_)_holds_ (_rseq_is_convergent_&_lim_rseq_=_(abs_((seq_id_tseq)_-_(seq_id_(vseq_._n))))_._i_) let rseq be Real_Sequence; ::_thesis: ( ( for m being Element of NAT holds rseq . m = (abs (seq_id ((vseq . m) - (vseq . n)))) . i ) implies ( rseq is convergent & lim rseq = (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i ) ) assume A20: for m being Element of NAT holds rseq . m = (abs (seq_id ((vseq . m) - (vseq . n)))) . i ; ::_thesis: ( rseq is convergent & lim rseq = (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i ) A21: now__::_thesis:_for_m_being_Element_of_NAT_holds_rseq_._m_=_abs_((rseqi_._m)_-_((seq_id_(vseq_._n))_._i)) let m be Element of NAT ; ::_thesis: rseq . m = abs ((rseqi . m) - ((seq_id (vseq . n)) . i)) A22: seq_id ((vseq . m) - (vseq . n)) = (seq_id (vseq . m)) - (seq_id (vseq . n)) by A17; thus rseq . m = (abs (seq_id ((vseq . m) - (vseq . n)))) . i by A20 .= abs ((seq_id ((vseq . m) - (vseq . n))) . i) by SEQ_1:12 .= abs (((seq_id (vseq . m)) . i) - ((seq_id (vseq . n)) . i)) by A22, RFUNCT_2:1 .= abs ((rseqi . m) - ((seq_id (vseq . n)) . i)) by A18 ; ::_thesis: verum end; abs ((tseq . i) - ((seq_id (vseq . n)) . i)) = abs ((tseq - (seq_id (vseq . n))) . i) by RFUNCT_2:1 .= abs (((seq_id tseq) - (seq_id (vseq . n))) . i) by RSSPACE:1 .= (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i by SEQ_1:12 ; hence ( rseq is convergent & lim rseq = (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i ) by A19, A21, RSSPACE3:1; ::_thesis: verum end; hence for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (abs (seq_id ((vseq . m) - (vseq . n)))) . i ) holds ( rseq is convergent & lim rseq = (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i ) ; ::_thesis: verum end; hence for i being Element of NAT for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (abs (seq_id ((vseq . m) - (vseq . n)))) . i ) holds ( rseq is convergent & lim rseq = (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i ) ; ::_thesis: verum end; for n being Element of NAT st n >= k holds ( abs ((seq_id tseq) - (seq_id (vseq . n))) is bounded & upper_bound (rng (abs ((seq_id tseq) - (seq_id (vseq . n))))) <= e ) proof let n be Element of NAT ; ::_thesis: ( n >= k implies ( abs ((seq_id tseq) - (seq_id (vseq . n))) is bounded & upper_bound (rng (abs ((seq_id tseq) - (seq_id (vseq . n))))) <= e ) ) assume A23: n >= k ; ::_thesis: ( abs ((seq_id tseq) - (seq_id (vseq . n))) is bounded & upper_bound (rng (abs ((seq_id tseq) - (seq_id (vseq . n))))) <= e ) A24: for i being Element of NAT holds (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i <= e proof let i be Element of NAT ; ::_thesis: (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i <= e deffunc H1( Element of NAT ) -> Element of REAL = (abs (seq_id ((vseq . $1) - (vseq . n)))) . i; consider rseq being Real_Sequence such that A25: for m being Element of NAT holds rseq . m = H1(m) from SEQ_1:sch_1(); A26: for m being Element of NAT st m >= k holds rseq . m <= e proof let m be Element of NAT ; ::_thesis: ( m >= k implies rseq . m <= e ) A27: rseq . m = (abs (seq_id ((vseq . m) - (vseq . n)))) . i by A25; assume A28: m >= k ; ::_thesis: rseq . m <= e then abs (seq_id ((vseq . m) - (vseq . n))) is bounded by A14, A23; then A29: (abs (seq_id ((vseq . m) - (vseq . n)))) . i <= upper_bound (rng (abs (seq_id ((vseq . m) - (vseq . n))))) by Lm2; upper_bound (rng (abs (seq_id ((vseq . m) - (vseq . n))))) <= e by A14, A23, A28; hence rseq . m <= e by A29, A27, XXREAL_0:2; ::_thesis: verum end; ( rseq is convergent & lim rseq = (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i ) by A16, A25; hence (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i <= e by A26, RSSPACE2:5; ::_thesis: verum end; A30: 0 + e < 1 + e by XREAL_1:8; now__::_thesis:_for_i_being_Element_of_NAT_holds_abs_(((seq_id_tseq)_-_(seq_id_(vseq_._n)))_._i)_<_e_+_1 let i be Element of NAT ; ::_thesis: abs (((seq_id tseq) - (seq_id (vseq . n))) . i) < e + 1 ( (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i <= e & (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i = abs (((seq_id tseq) - (seq_id (vseq . n))) . i) ) by A24, SEQ_1:12; hence abs (((seq_id tseq) - (seq_id (vseq . n))) . i) < e + 1 by A30, XXREAL_0:2; ::_thesis: verum end; then (seq_id tseq) - (seq_id (vseq . n)) is bounded by A12, SEQ_2:3; hence ( abs ((seq_id tseq) - (seq_id (vseq . n))) is bounded & upper_bound (rng (abs ((seq_id tseq) - (seq_id (vseq . n))))) <= e ) by A24, Lm1; ::_thesis: verum end; hence ex k being Element of NAT st for n being Element of NAT st n >= k holds ( abs ((seq_id tseq) - (seq_id (vseq . n))) is bounded & upper_bound (rng (abs ((seq_id tseq) - (seq_id (vseq . n))))) <= e ) ; ::_thesis: verum end; A31: seq_id tseq is bounded proof consider m being Element of NAT such that A32: for n being Element of NAT st n >= m holds ( abs ((seq_id tseq) - (seq_id (vseq . n))) is bounded & upper_bound (rng (abs ((seq_id tseq) - (seq_id (vseq . n))))) <= 1 ) by A11; A33: abs ((seq_id tseq) - (seq_id (vseq . m))) is bounded by A32; set d = abs (seq_id tseq); set b = abs (seq_id (vseq . m)); set a = abs ((seq_id tseq) - (seq_id (vseq . m))); A34: seq_id (vseq . m) is bounded by Def1; A35: for i being Element of NAT holds (abs (seq_id tseq)) . i <= ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m)))) . i proof let i be Element of NAT ; ::_thesis: (abs (seq_id tseq)) . i <= ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m)))) . i A36: ( (abs (seq_id (vseq . m))) . i = abs ((seq_id (vseq . m)) . i) & (abs (seq_id tseq)) . i = abs ((seq_id tseq) . i) ) by SEQ_1:12; (abs ((seq_id tseq) - (seq_id (vseq . m)))) . i = abs (((seq_id tseq) + (- (seq_id (vseq . m)))) . i) by SEQ_1:12 .= abs (((seq_id tseq) . i) + ((- (seq_id (vseq . m))) . i)) by SEQ_1:7 .= abs (((seq_id tseq) . i) + (- ((seq_id (vseq . m)) . i))) by SEQ_1:10 .= abs (((seq_id tseq) . i) - ((seq_id (vseq . m)) . i)) ; then ((abs (seq_id tseq)) . i) - ((abs (seq_id (vseq . m))) . i) <= (abs ((seq_id tseq) - (seq_id (vseq . m)))) . i by A36, COMPLEX1:59; then (((abs (seq_id tseq)) . i) - ((abs (seq_id (vseq . m))) . i)) + ((abs (seq_id (vseq . m))) . i) <= ((abs ((seq_id tseq) - (seq_id (vseq . m)))) . i) + ((abs (seq_id (vseq . m))) . i) by XREAL_1:6; hence (abs (seq_id tseq)) . i <= ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m)))) . i by SEQ_1:7; ::_thesis: verum end; abs (seq_id tseq) is bounded proof reconsider r = (upper_bound (rng ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m)))))) + 1 as real number ; (abs (seq_id (vseq . m))) . 1 = abs ((seq_id (vseq . m)) . 1) by SEQ_1:12; then A37: 0 <= (abs (seq_id (vseq . m))) . 1 by COMPLEX1:46; A38: (upper_bound (rng ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m)))))) + 0 < (upper_bound (rng ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m)))))) + 1 by XREAL_1:8; A39: now__::_thesis:_for_i_being_Element_of_NAT_holds_abs_((seq_id_tseq)_._i)_<_r let i be Element of NAT ; ::_thesis: abs ((seq_id tseq) . i) < r ( (abs (seq_id tseq)) . i <= ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m)))) . i & ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m)))) . i <= upper_bound (rng ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m))))) ) by A33, A34, A35, Lm2; then A40: (abs (seq_id tseq)) . i <= upper_bound (rng ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m))))) by XXREAL_0:2; (abs (seq_id tseq)) . i = abs ((seq_id tseq) . i) by SEQ_1:12; hence abs ((seq_id tseq) . i) < r by A38, A40, XXREAL_0:2; ::_thesis: verum end; (abs ((seq_id tseq) - (seq_id (vseq . m)))) . 1 = abs (((seq_id tseq) - (seq_id (vseq . m))) . 1) by SEQ_1:12; then ( ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m)))) . 1 = ((abs ((seq_id tseq) - (seq_id (vseq . m)))) . 1) + ((abs (seq_id (vseq . m))) . 1) & 0 <= (abs ((seq_id tseq) - (seq_id (vseq . m)))) . 1 ) by COMPLEX1:46, SEQ_1:7; then 0 <= upper_bound (rng ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m))))) by A33, A34, A37, Lm2; then seq_id tseq is bounded by A39, SEQ_2:3; hence abs (seq_id tseq) is bounded ; ::_thesis: verum end; hence seq_id tseq is bounded by SEQM_3:37; ::_thesis: verum end; A41: tseq in the_set_of_RealSequences by RSSPACE:def_1; then reconsider tv = tseq as Point of linfty_Space by A31, Def1; take tv ; :: according to NORMSP_1:def_6 ::_thesis: for b1 being Element of REAL holds ( b1 <= 0 or ex b2 being Element of NAT st for b3 being Element of NAT holds ( not b2 <= b3 or not b1 <= ||.((vseq . b3) - tv).|| ) ) let e1 be Real; ::_thesis: ( e1 <= 0 or ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not e1 <= ||.((vseq . b2) - tv).|| ) ) assume A42: e1 > 0 ; ::_thesis: ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not e1 <= ||.((vseq . b2) - tv).|| ) set e = e1 / 2; consider m being Element of NAT such that A43: for n being Element of NAT st n >= m holds ( abs ((seq_id tseq) - (seq_id (vseq . n))) is bounded & upper_bound (rng (abs ((seq_id tseq) - (seq_id (vseq . n))))) <= e1 / 2 ) by A11, A42, XREAL_1:215; A44: e1 / 2 < e1 by A42, XREAL_1:216; now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_m_holds_ ||.((vseq_._n)_-_tv).||_<_e1 reconsider u = tseq as VECTOR of linfty_Space by A31, A41, Def1; let n be Element of NAT ; ::_thesis: ( n >= m implies ||.((vseq . n) - tv).|| < e1 ) assume n >= m ; ::_thesis: ||.((vseq . n) - tv).|| < e1 then A45: upper_bound (rng (abs ((seq_id tseq) - (seq_id (vseq . n))))) <= e1 / 2 by A43; reconsider v = vseq . n as VECTOR of linfty_Space ; seq_id (u - v) = u - v by Th2; then upper_bound (rng (abs (seq_id (u - v)))) = upper_bound (rng (abs ((seq_id tseq) - (seq_id (vseq . n))))) by Th2; then A46: the normF of linfty_Space . (u - v) <= e1 / 2 by A45, Def2; ||.((vseq . n) - tv).|| = ||.(- (tv - (vseq . n))).|| by RLVECT_1:33 .= ||.(tv - (vseq . n)).|| by NORMSP_1:2 ; hence ||.((vseq . n) - tv).|| < e1 by A44, A46, XXREAL_0:2; ::_thesis: verum end; hence ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not e1 <= ||.((vseq . b2) - tv).|| ) ; ::_thesis: verum end; begin definition let X be non empty set ; let Y be RealNormSpace; let IT be Function of X, the carrier of Y; attrIT 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 Th5: :: RSSPACE4:5 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 let X be non empty set ; ::_thesis: 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 let Y be RealNormSpace; ::_thesis: 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 let f be Function of X, the carrier of Y; ::_thesis: ( ( for x being Element of X holds f . x = 0. Y ) implies f is bounded ) assume A1: for x being Element of X holds f . x = 0. Y ; ::_thesis: f is bounded A2: now__::_thesis:_for_x_being_Element_of_X_holds_||.(f_._x).||_=_0 let x be Element of X; ::_thesis: ||.(f . x).|| = 0 thus ||.(f . x).|| = ||.(0. Y).|| by A1 .= 0 ; ::_thesis: verum end; take 0 ; :: according to RSSPACE4:def_4 ::_thesis: ( 0 <= 0 & ( for x being Element of X holds ||.(f . x).|| <= 0 ) ) thus ( 0 <= 0 & ( for x being Element of X holds ||.(f . x).|| <= 0 ) ) by A2; ::_thesis: verum end; registration let X be non empty set ; let Y be RealNormSpace; cluster non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total bounded for Element of bool [:X, the carrier of Y:]; existence ex b1 being Function of X, the carrier of Y st b1 is bounded proof set f = X --> (0. Y); reconsider f = X --> (0. Y) as Function of X, the carrier of Y ; take f ; ::_thesis: f is bounded for x being Element of X holds f . x = 0. Y by FUNCOP_1:7; hence f is bounded by Th5; ::_thesis: verum 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 A1: RealVectSpace (X,Y) = RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) by LOPBAN_1:def_4; defpred S1[ set ] means $1 is bounded Function of X, the carrier of Y; consider IT being set such that A2: for x being set holds ( x in IT iff ( x in Funcs (X, the carrier of Y) & S1[x] ) ) from XBOOLE_0:sch_1(); take IT ; ::_thesis: ( IT is Subset of (RealVectSpace (X,Y)) & ( for x being set holds ( x in IT iff x is bounded Function of X, the carrier of Y ) ) ) for x being set st x in IT holds x in Funcs (X, the carrier of Y) by A2; hence IT is Subset of (RealVectSpace (X,Y)) by A1, TARSKI:def_3; ::_thesis: for x being set holds ( x in IT iff x is bounded Function of X, the carrier of Y ) let x be set ; ::_thesis: ( x in IT iff x is bounded Function of X, the carrier of Y ) thus ( x in IT implies x is bounded Function of X, the carrier of Y ) by A2; ::_thesis: ( x is bounded Function of X, the carrier of Y implies x in IT ) assume A3: x is bounded Function of X, the carrier of Y ; ::_thesis: x in IT then x in Funcs (X, the carrier of Y) by FUNCT_2:8; hence x in IT by A2, A3; ::_thesis: verum 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 let X1, X2 be Subset of (RealVectSpace (X,Y)); ::_thesis: ( ( for x being set holds ( x in X1 iff x is bounded Function of X, the carrier of Y ) ) & ( for x being set holds ( x in X2 iff x is bounded Function of X, the carrier of Y ) ) implies X1 = X2 ) assume that A4: for x being set holds ( x in X1 iff x is bounded Function of X, the carrier of Y ) and A5: for x being set holds ( x in X2 iff x is bounded Function of X, the carrier of Y ) ; ::_thesis: X1 = X2 for x being set st x in X2 holds x in X1 proof let x be set ; ::_thesis: ( x in X2 implies x in X1 ) assume x in X2 ; ::_thesis: x in X1 then x is bounded Function of X, the carrier of Y by A5; hence x in X1 by A4; ::_thesis: verum end; then A6: X2 c= X1 by TARSKI:def_3; for x being set st x in X1 holds x in X2 proof let x be set ; ::_thesis: ( x in X1 implies x in X2 ) assume x in X1 ; ::_thesis: x in X2 then x is bounded Function of X, the carrier of Y by A4; hence x in X2 by A5; ::_thesis: verum end; then X1 c= X2 by TARSKI:def_3; hence X1 = X2 by A6, XBOOLE_0:def_10; ::_thesis: verum 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 set f = X --> (0. Y); reconsider f = X --> (0. Y) as Function of X, the carrier of Y ; for x being Element of X holds f . x = 0. Y by FUNCOP_1:7; then f is bounded by Th5; hence not BoundedFunctions (X,Y) is empty by Def5; ::_thesis: verum end; end; theorem Th6: :: RSSPACE4:6 for X being non empty set for Y being RealNormSpace holds BoundedFunctions (X,Y) is linearly-closed proof let X be non empty set ; ::_thesis: for Y being RealNormSpace holds BoundedFunctions (X,Y) is linearly-closed let Y be RealNormSpace; ::_thesis: BoundedFunctions (X,Y) is linearly-closed set W = BoundedFunctions (X,Y); A1: RealVectSpace (X,Y) = RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) by LOPBAN_1:def_4; A2: for v, u being VECTOR of (RealVectSpace (X,Y)) st v in BoundedFunctions (X,Y) & u in BoundedFunctions (X,Y) holds v + u in BoundedFunctions (X,Y) proof let v, u be VECTOR of (RealVectSpace (X,Y)); ::_thesis: ( v in BoundedFunctions (X,Y) & u in BoundedFunctions (X,Y) implies v + u in BoundedFunctions (X,Y) ) assume that A3: v in BoundedFunctions (X,Y) and A4: u in BoundedFunctions (X,Y) ; ::_thesis: v + u in BoundedFunctions (X,Y) reconsider f = v + u as Function of X, the carrier of Y by A1, FUNCT_2:66; f is bounded proof reconsider v1 = v as bounded Function of X, the carrier of Y by A3, Def5; consider K2 being Real such that A5: 0 <= K2 and A6: for x being Element of X holds ||.(v1 . x).|| <= K2 by Def4; reconsider u1 = u as bounded Function of X, the carrier of Y by A4, Def5; consider K1 being Real such that A7: 0 <= K1 and A8: for x being Element of X holds ||.(u1 . x).|| <= K1 by Def4; take K3 = K1 + K2; :: according to RSSPACE4:def_4 ::_thesis: ( 0 <= K3 & ( for x being Element of X holds ||.(f . x).|| <= K3 ) ) now__::_thesis:_for_x_being_Element_of_X_holds_||.(f_._x).||_<=_K3 let x be Element of X; ::_thesis: ||.(f . x).|| <= K3 ( ||.(u1 . x).|| <= K1 & ||.(v1 . x).|| <= K2 ) by A8, A6; then A9: ||.(u1 . x).|| + ||.(v1 . x).|| <= K1 + K2 by XREAL_1:7; ( ||.(f . x).|| = ||.((v1 . x) + (u1 . x)).|| & ||.((u1 . x) + (v1 . x)).|| <= ||.(u1 . x).|| + ||.(v1 . x).|| ) by LOPBAN_1:11, NORMSP_1:def_1; hence ||.(f . x).|| <= K3 by A9, XXREAL_0:2; ::_thesis: verum end; hence ( 0 <= K3 & ( for x being Element of X holds ||.(f . x).|| <= K3 ) ) by A7, A5; ::_thesis: verum end; hence v + u in BoundedFunctions (X,Y) by Def5; ::_thesis: verum end; for a being Real for v being VECTOR of (RealVectSpace (X,Y)) st v in BoundedFunctions (X,Y) holds a * v in BoundedFunctions (X,Y) proof let a be Real; ::_thesis: for v being VECTOR of (RealVectSpace (X,Y)) st v in BoundedFunctions (X,Y) holds a * v in BoundedFunctions (X,Y) let v be VECTOR of (RealVectSpace (X,Y)); ::_thesis: ( v in BoundedFunctions (X,Y) implies a * v in BoundedFunctions (X,Y) ) assume A10: v in BoundedFunctions (X,Y) ; ::_thesis: a * v in BoundedFunctions (X,Y) reconsider f = a * v as Function of X, the carrier of Y by A1, FUNCT_2:66; f is bounded proof reconsider v1 = v as bounded Function of X, the carrier of Y by A10, Def5; consider K being Real such that A11: 0 <= K and A12: for x being Element of X holds ||.(v1 . x).|| <= K by Def4; take (abs a) * K ; :: according to RSSPACE4:def_4 ::_thesis: ( 0 <= (abs a) * K & ( for x being Element of X holds ||.(f . x).|| <= (abs a) * K ) ) A13: now__::_thesis:_for_x_being_Element_of_X_holds_||.(f_._x).||_<=_(abs_a)_*_K let x be Element of X; ::_thesis: ||.(f . x).|| <= (abs a) * K A14: 0 <= abs a by COMPLEX1:46; ( ||.(f . x).|| = ||.(a * (v1 . x)).|| & ||.(a * (v1 . x)).|| = (abs a) * ||.(v1 . x).|| ) by LOPBAN_1:12, NORMSP_1:def_1; hence ||.(f . x).|| <= (abs a) * K by A12, A14, XREAL_1:64; ::_thesis: verum end; 0 <= abs a by COMPLEX1:46; hence ( 0 <= (abs a) * K & ( for x being Element of X holds ||.(f . x).|| <= (abs a) * K ) ) by A11, A13; ::_thesis: verum end; hence a * v in BoundedFunctions (X,Y) by Def5; ::_thesis: verum end; hence BoundedFunctions (X,Y) is linearly-closed by A2, RLSUB_1:def_1; ::_thesis: verum end; theorem :: RSSPACE4:7 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 Th6, RSSPACE:11; 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 Th6, RSSPACE:11; 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 Th8: :: RSSPACE4:8 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 let X be non empty set ; ::_thesis: 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) ) let Y be RealNormSpace; ::_thesis: 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) ) let f, g, h be VECTOR of (R_VectorSpace_of_BoundedFunctions (X,Y)); ::_thesis: 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) ) A1: R_VectorSpace_of_BoundedFunctions (X,Y) is Subspace of RealVectSpace (X,Y) by Th6, RSSPACE:11; then reconsider f1 = f as VECTOR of (RealVectSpace (X,Y)) by RLSUB_1:10; reconsider h1 = h as VECTOR of (RealVectSpace (X,Y)) by A1, RLSUB_1:10; reconsider g1 = g as VECTOR of (RealVectSpace (X,Y)) by A1, RLSUB_1:10; let f9, g9, h9 be bounded Function of X, the carrier of Y; ::_thesis: ( f9 = f & g9 = g & h9 = h implies ( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) ) ) assume A2: ( f9 = f & g9 = g & h9 = h ) ; ::_thesis: ( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) ) A3: now__::_thesis:_(_h_=_f_+_g_implies_for_x_being_Element_of_X_holds_h9_._x_=_(f9_._x)_+_(g9_._x)_) assume A4: h = f + g ; ::_thesis: for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) let x be Element of X; ::_thesis: h9 . x = (f9 . x) + (g9 . x) h1 = f1 + g1 by A1, A4, RLSUB_1:13; hence h9 . x = (f9 . x) + (g9 . x) by A2, LOPBAN_1:11; ::_thesis: verum end; now__::_thesis:_(_(_for_x_being_Element_of_X_holds_h9_._x_=_(f9_._x)_+_(g9_._x)_)_implies_h_=_f_+_g_) assume for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) ; ::_thesis: h = f + g then h1 = f1 + g1 by A2, LOPBAN_1:11; hence h = f + g by A1, RLSUB_1:13; ::_thesis: verum end; hence ( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) ) by A3; ::_thesis: verum end; theorem Th9: :: RSSPACE4:9 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 let X be non empty set ; ::_thesis: 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) ) let Y be RealNormSpace; ::_thesis: 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) ) let f, h be VECTOR of (R_VectorSpace_of_BoundedFunctions (X,Y)); ::_thesis: 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) ) let f9, h9 be bounded Function of X, the carrier of Y; ::_thesis: ( f9 = f & h9 = h implies for a being Real holds ( h = a * f iff for x being Element of X holds h9 . x = a * (f9 . x) ) ) assume A1: ( f9 = f & h9 = h ) ; ::_thesis: for a being Real holds ( h = a * f iff for x being Element of X holds h9 . x = a * (f9 . x) ) let a be Real; ::_thesis: ( h = a * f iff for x being Element of X holds h9 . x = a * (f9 . x) ) A2: R_VectorSpace_of_BoundedFunctions (X,Y) is Subspace of RealVectSpace (X,Y) by Th6, RSSPACE:11; then reconsider f1 = f, h1 = h as VECTOR of (RealVectSpace (X,Y)) by RLSUB_1:10; A3: now__::_thesis:_(_h_=_a_*_f_implies_for_x_being_Element_of_X_holds_h9_._x_=_a_*_(f9_._x)_) assume A4: h = a * f ; ::_thesis: for x being Element of X holds h9 . x = a * (f9 . x) let x be Element of X; ::_thesis: h9 . x = a * (f9 . x) h1 = a * f1 by A2, A4, RLSUB_1:14; hence h9 . x = a * (f9 . x) by A1, LOPBAN_1:12; ::_thesis: verum end; now__::_thesis:_(_(_for_x_being_Element_of_X_holds_h9_._x_=_a_*_(f9_._x)_)_implies_h_=_a_*_f_) assume for x being Element of X holds h9 . x = a * (f9 . x) ; ::_thesis: h = a * f then h1 = a * f1 by A1, LOPBAN_1:12; hence h = a * f by A2, RLSUB_1:14; ::_thesis: verum end; hence ( h = a * f iff for x being Element of X holds h9 . x = a * (f9 . x) ) by A3; ::_thesis: verum end; theorem Th10: :: RSSPACE4:10 for X being non empty set for Y being RealNormSpace holds 0. (R_VectorSpace_of_BoundedFunctions (X,Y)) = X --> (0. Y) proof let X be non empty set ; ::_thesis: for Y being RealNormSpace holds 0. (R_VectorSpace_of_BoundedFunctions (X,Y)) = X --> (0. Y) let Y be RealNormSpace; ::_thesis: 0. (R_VectorSpace_of_BoundedFunctions (X,Y)) = X --> (0. Y) ( R_VectorSpace_of_BoundedFunctions (X,Y) is Subspace of RealVectSpace (X,Y) & 0. (RealVectSpace (X,Y)) = X --> (0. Y) ) by Th6, LOPBAN_1:13, RSSPACE:11; hence 0. (R_VectorSpace_of_BoundedFunctions (X,Y)) = X --> (0. Y) by RLSUB_1:11; ::_thesis: verum 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 set x = the Element of X; A1: now__::_thesis:_for_x_being_set_st_x_in__{__||.(u_._t).||_where_t_is_Element_of_X_:_verum__}__holds_ x_in_REAL let x be set ; ::_thesis: ( x in { ||.(u . t).|| where t is Element of X : verum } implies x in REAL ) now__::_thesis:_(_x_in__{__||.(u_._t).||_where_t_is_Element_of_X_:_verum__}__implies_x_in_REAL_) assume x in { ||.(u . t).|| where t is Element of X : verum } ; ::_thesis: x in REAL then ex t being Element of X st x = ||.(u . t).|| ; hence x in REAL ; ::_thesis: verum end; hence ( x in { ||.(u . t).|| where t is Element of X : verum } implies x in REAL ) ; ::_thesis: verum end; ||.(u . the Element of X).|| in { ||.(u . t).|| where t is Element of X : verum } ; hence { ||.(u . t).|| where t is Element of X : verum } is non empty Subset of REAL by A1, TARSKI:def_3; ::_thesis: verum 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 Th11: :: RSSPACE4:11 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 let X be non empty set ; ::_thesis: for Y being RealNormSpace for g being bounded Function of X, the carrier of Y holds PreNorms g is bounded_above let Y be RealNormSpace; ::_thesis: for g being bounded Function of X, the carrier of Y holds PreNorms g is bounded_above let g be bounded Function of X, the carrier of Y; ::_thesis: PreNorms g is bounded_above consider K being Real such that 0 <= K and A1: for x being Element of X holds ||.(g . x).|| <= K by Def4; take K ; :: according to XXREAL_2:def_10 ::_thesis: K is UpperBound of PreNorms g let r be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not r in PreNorms g or r <= K ) assume r in PreNorms g ; ::_thesis: r <= K then ex t being Element of X st r = ||.(g . t).|| ; hence r <= K by A1; ::_thesis: verum end; theorem :: RSSPACE4:12 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 let X be non empty set ; ::_thesis: for Y being RealNormSpace for g being Function of X, the carrier of Y holds ( g is bounded iff PreNorms g is bounded_above ) let Y be RealNormSpace; ::_thesis: for g being Function of X, the carrier of Y holds ( g is bounded iff PreNorms g is bounded_above ) let g be Function of X, the carrier of Y; ::_thesis: ( g is bounded iff PreNorms g is bounded_above ) now__::_thesis:_(_PreNorms_g_is_bounded_above_implies_ex_K_being_Real_st_g_is_bounded_) reconsider K = upper_bound (PreNorms g) as Real ; assume A1: PreNorms g is bounded_above ; ::_thesis: ex K being Real st g is bounded A2: 0 <= K proof consider r0 being set such that A3: r0 in PreNorms g by XBOOLE_0:def_1; reconsider r0 = r0 as Real by A3; now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_g_holds_ 0_<=_r let r be Real; ::_thesis: ( r in PreNorms g implies 0 <= r ) assume r in PreNorms g ; ::_thesis: 0 <= r then ex t being Element of X st r = ||.(g . t).|| ; hence 0 <= r ; ::_thesis: verum end; then 0 <= r0 by A3; hence 0 <= K by A1, A3, SEQ_4:def_1; ::_thesis: verum end; take K = K; ::_thesis: g is bounded now__::_thesis:_for_t_being_Element_of_X_holds_||.(g_._t).||_<=_K let t be Element of X; ::_thesis: ||.(g . t).|| <= K ||.(g . t).|| in PreNorms g ; hence ||.(g . t).|| <= K by A1, SEQ_4:def_1; ::_thesis: verum end; hence g is bounded by A2, Def4; ::_thesis: verum end; hence ( g is bounded iff PreNorms g is bounded_above ) by Th11; ::_thesis: verum 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))) proof deffunc H1( set ) -> Element of REAL = upper_bound (PreNorms (modetrans ($1,X,Y))); A1: for z being set st z in BoundedFunctions (X,Y) holds H1(z) in REAL ; ex f being Function of (BoundedFunctions (X,Y)),REAL st for x being set st x in BoundedFunctions (X,Y) holds f . x = H1(x) from FUNCT_2:sch_2(A1); hence 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))) ; ::_thesis: verum end; 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 let NORM1, NORM2 be Function of (BoundedFunctions (X,Y)),REAL; ::_thesis: ( ( for x being set st x in BoundedFunctions (X,Y) holds NORM1 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) & ( for x being set st x in BoundedFunctions (X,Y) holds NORM2 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) implies NORM1 = NORM2 ) assume that A2: for x being set st x in BoundedFunctions (X,Y) holds NORM1 . x = upper_bound (PreNorms (modetrans (x,X,Y))) and A3: for x being set st x in BoundedFunctions (X,Y) holds NORM2 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ; ::_thesis: NORM1 = NORM2 A4: for z being set st z in BoundedFunctions (X,Y) holds NORM1 . z = NORM2 . z proof let z be set ; ::_thesis: ( z in BoundedFunctions (X,Y) implies NORM1 . z = NORM2 . z ) assume A5: z in BoundedFunctions (X,Y) ; ::_thesis: NORM1 . z = NORM2 . z NORM1 . z = upper_bound (PreNorms (modetrans (z,X,Y))) by A2, A5; hence NORM1 . z = NORM2 . z by A3, A5; ::_thesis: verum end; ( dom NORM1 = BoundedFunctions (X,Y) & dom NORM2 = BoundedFunctions (X,Y) ) by FUNCT_2:def_1; hence NORM1 = NORM2 by A4, FUNCT_1:2; ::_thesis: verum 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 Th13: :: RSSPACE4:13 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 let X be non empty set ; ::_thesis: for Y being RealNormSpace for f being bounded Function of X, the carrier of Y holds modetrans (f,X,Y) = f let Y be RealNormSpace; ::_thesis: for f being bounded Function of X, the carrier of Y holds modetrans (f,X,Y) = f let f be bounded Function of X, the carrier of Y; ::_thesis: modetrans (f,X,Y) = f f in BoundedFunctions (X,Y) by Def5; hence modetrans (f,X,Y) = f by Def7; ::_thesis: verum end; theorem Th14: :: RSSPACE4:14 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 let X be non empty set ; ::_thesis: for Y being RealNormSpace for f being bounded Function of X, the carrier of Y holds (BoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms f) let Y be RealNormSpace; ::_thesis: for f being bounded Function of X, the carrier of Y holds (BoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms f) let f be bounded Function of X, the carrier of Y; ::_thesis: (BoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms f) reconsider f9 = f as set ; f in BoundedFunctions (X,Y) by Def5; hence (BoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms (modetrans (f9,X,Y))) by Def9 .= upper_bound (PreNorms f) by Th13 ; ::_thesis: verum 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 Th15: :: RSSPACE4:15 for X being non empty set for Y being RealNormSpace holds X --> (0. Y) = 0. (R_NormSpace_of_BoundedFunctions (X,Y)) proof let X be non empty set ; ::_thesis: for Y being RealNormSpace holds X --> (0. Y) = 0. (R_NormSpace_of_BoundedFunctions (X,Y)) let Y be RealNormSpace; ::_thesis: X --> (0. Y) = 0. (R_NormSpace_of_BoundedFunctions (X,Y)) X --> (0. Y) = 0. (R_VectorSpace_of_BoundedFunctions (X,Y)) by Th10 .= 0. (R_NormSpace_of_BoundedFunctions (X,Y)) ; hence X --> (0. Y) = 0. (R_NormSpace_of_BoundedFunctions (X,Y)) ; ::_thesis: verum end; theorem Th16: :: RSSPACE4:16 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 let X be non empty set ; ::_thesis: 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.|| let Y be RealNormSpace; ::_thesis: 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.|| let f be Point of (R_NormSpace_of_BoundedFunctions (X,Y)); ::_thesis: 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.|| let g be bounded Function of X, the carrier of Y; ::_thesis: ( g = f implies for t being Element of X holds ||.(g . t).|| <= ||.f.|| ) assume A1: g = f ; ::_thesis: for t being Element of X holds ||.(g . t).|| <= ||.f.|| A2: ( not PreNorms g is empty & PreNorms g is bounded_above ) by Th11; now__::_thesis:_for_t_being_Element_of_X_holds_||.(g_._t).||_<=_||.f.|| let t be Element of X; ::_thesis: ||.(g . t).|| <= ||.f.|| ||.(g . t).|| in PreNorms g ; then ||.(g . t).|| <= upper_bound (PreNorms g) by A2, SEQ_4:def_1; hence ||.(g . t).|| <= ||.f.|| by A1, Th14; ::_thesis: verum end; hence for t being Element of X holds ||.(g . t).|| <= ||.f.|| ; ::_thesis: verum end; theorem :: RSSPACE4:17 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 let X be non empty set ; ::_thesis: for Y being RealNormSpace for f being Point of (R_NormSpace_of_BoundedFunctions (X,Y)) holds 0 <= ||.f.|| let Y be RealNormSpace; ::_thesis: for f being Point of (R_NormSpace_of_BoundedFunctions (X,Y)) holds 0 <= ||.f.|| let f be Point of (R_NormSpace_of_BoundedFunctions (X,Y)); ::_thesis: 0 <= ||.f.|| reconsider g = f as bounded Function of X, the carrier of Y by Def5; consider r0 being set such that A1: r0 in PreNorms g by XBOOLE_0:def_1; reconsider r0 = r0 as Real by A1; A2: ( not PreNorms g is empty & PreNorms g is bounded_above ) by Th11; now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_g_holds_ 0_<=_r let r be Real; ::_thesis: ( r in PreNorms g implies 0 <= r ) assume r in PreNorms g ; ::_thesis: 0 <= r then ex t being Element of X st r = ||.(g . t).|| ; hence 0 <= r ; ::_thesis: verum end; then 0 <= r0 by A1; then 0 <= upper_bound (PreNorms g) by A2, A1, SEQ_4:def_1; hence 0 <= ||.f.|| by Th14; ::_thesis: verum end; theorem Th18: :: RSSPACE4:18 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 let X be non empty set ; ::_thesis: 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.|| let Y be RealNormSpace; ::_thesis: for f being Point of (R_NormSpace_of_BoundedFunctions (X,Y)) st f = 0. (R_NormSpace_of_BoundedFunctions (X,Y)) holds 0 = ||.f.|| let f be Point of (R_NormSpace_of_BoundedFunctions (X,Y)); ::_thesis: ( f = 0. (R_NormSpace_of_BoundedFunctions (X,Y)) implies 0 = ||.f.|| ) assume A1: f = 0. (R_NormSpace_of_BoundedFunctions (X,Y)) ; ::_thesis: 0 = ||.f.|| thus ||.f.|| = 0 ::_thesis: verum proof reconsider g = f as bounded Function of X, the carrier of Y by Def5; set z = X --> (0. Y); reconsider z = X --> (0. Y) as Function of X, the carrier of Y ; consider r0 being set such that A2: r0 in PreNorms g by XBOOLE_0:def_1; reconsider r0 = r0 as Real by A2; A3: ( ( for s being real number st s in PreNorms g holds s <= 0 ) implies upper_bound (PreNorms g) <= 0 ) by SEQ_4:45; A4: ( not PreNorms g is empty & PreNorms g is bounded_above ) by Th11; A5: z = g by A1, Th15; A6: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_g_holds_ (_0_<=_r_&_r_<=_0_) let r be Real; ::_thesis: ( r in PreNorms g implies ( 0 <= r & r <= 0 ) ) assume r in PreNorms g ; ::_thesis: ( 0 <= r & r <= 0 ) then consider t being Element of X such that A7: r = ||.(g . t).|| ; ||.(g . t).|| = ||.(0. Y).|| by A5, FUNCOP_1:7 .= 0 ; hence ( 0 <= r & r <= 0 ) by A7; ::_thesis: verum end; then 0 <= r0 by A2; then upper_bound (PreNorms g) = 0 by A6, A4, A2, A3, SEQ_4:def_1; hence ||.f.|| = 0 by Th14; ::_thesis: verum end; end; theorem Th19: :: RSSPACE4:19 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 let X be non empty set ; ::_thesis: 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) ) let Y be RealNormSpace; ::_thesis: 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) ) let f, g, h be Point of (R_NormSpace_of_BoundedFunctions (X,Y)); ::_thesis: 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) ) reconsider f1 = f, g1 = g, h1 = h as VECTOR of (R_VectorSpace_of_BoundedFunctions (X,Y)) ; A1: ( h = f + g iff h1 = f1 + g1 ) ; let f9, g9, h9 be bounded Function of X, the carrier of Y; ::_thesis: ( f9 = f & g9 = g & h9 = h implies ( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) ) ) assume ( f9 = f & g9 = g & h9 = h ) ; ::_thesis: ( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) ) hence ( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) ) by A1, Th8; ::_thesis: verum end; theorem Th20: :: RSSPACE4:20 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 let X be non empty set ; ::_thesis: 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) ) let Y be RealNormSpace; ::_thesis: 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) ) let f, h be Point of (R_NormSpace_of_BoundedFunctions (X,Y)); ::_thesis: 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) ) let f9, h9 be bounded Function of X, the carrier of Y; ::_thesis: ( f9 = f & h9 = h implies for a being Real holds ( h = a * f iff for x being Element of X holds h9 . x = a * (f9 . x) ) ) assume A1: ( f9 = f & h9 = h ) ; ::_thesis: for a being Real holds ( h = a * f iff for x being Element of X holds h9 . x = a * (f9 . x) ) reconsider h1 = h as VECTOR of (R_VectorSpace_of_BoundedFunctions (X,Y)) ; reconsider f1 = f as VECTOR of (R_VectorSpace_of_BoundedFunctions (X,Y)) ; let a be Real; ::_thesis: ( h = a * f iff for x being Element of X holds h9 . x = a * (f9 . x) ) ( h = a * f iff h1 = a * f1 ) ; hence ( h = a * f iff for x being Element of X holds h9 . x = a * (f9 . x) ) by A1, Th9; ::_thesis: verum end; theorem Th21: :: RSSPACE4:21 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 let X be non empty set ; ::_thesis: 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.|| ) let Y be RealNormSpace; ::_thesis: 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.|| ) let f, g be Point of (R_NormSpace_of_BoundedFunctions (X,Y)); ::_thesis: 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.|| ) let a be Real; ::_thesis: ( ( ||.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.|| ) A1: now__::_thesis:_(_f_=_0._(R_NormSpace_of_BoundedFunctions_(X,Y))_implies_||.f.||_=_0_) assume A2: f = 0. (R_NormSpace_of_BoundedFunctions (X,Y)) ; ::_thesis: ||.f.|| = 0 thus ||.f.|| = 0 ::_thesis: verum proof reconsider g = f as bounded Function of X, the carrier of Y by Def5; set z = X --> (0. Y); reconsider z = X --> (0. Y) as Function of X, the carrier of Y ; consider r0 being set such that A3: r0 in PreNorms g by XBOOLE_0:def_1; reconsider r0 = r0 as Real by A3; A4: ( ( for s being real number st s in PreNorms g holds s <= 0 ) implies upper_bound (PreNorms g) <= 0 ) by SEQ_4:45; A5: ( not PreNorms g is empty & PreNorms g is bounded_above ) by Th11; A6: z = g by A2, Th15; A7: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_g_holds_ (_0_<=_r_&_r_<=_0_) let r be Real; ::_thesis: ( r in PreNorms g implies ( 0 <= r & r <= 0 ) ) assume r in PreNorms g ; ::_thesis: ( 0 <= r & r <= 0 ) then consider t being Element of X such that A8: r = ||.(g . t).|| ; ||.(g . t).|| = ||.(0. Y).|| by A6, FUNCOP_1:7 .= 0 ; hence ( 0 <= r & r <= 0 ) by A8; ::_thesis: verum end; then 0 <= r0 by A3; then upper_bound (PreNorms g) = 0 by A7, A5, A3, A4, SEQ_4:def_1; hence ||.f.|| = 0 by Th14; ::_thesis: verum end; end; A9: ||.(f + g).|| <= ||.f.|| + ||.g.|| proof reconsider f1 = f, g1 = g, h1 = f + g as bounded Function of X, the carrier of Y by Def5; A10: now__::_thesis:_for_t_being_Element_of_X_holds_||.(h1_._t).||_<=_||.f.||_+_||.g.|| let t be Element of X; ::_thesis: ||.(h1 . t).|| <= ||.f.|| + ||.g.|| ( ||.(f1 . t).|| <= ||.f.|| & ||.(g1 . t).|| <= ||.g.|| ) by Th16; then A11: ||.(f1 . t).|| + ||.(g1 . t).|| <= ||.f.|| + ||.g.|| by XREAL_1:7; ( ||.(h1 . t).|| = ||.((f1 . t) + (g1 . t)).|| & ||.((f1 . t) + (g1 . t)).|| <= ||.(f1 . t).|| + ||.(g1 . t).|| ) by Th19, NORMSP_1:def_1; hence ||.(h1 . t).|| <= ||.f.|| + ||.g.|| by A11, XXREAL_0:2; ::_thesis: verum end; A12: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_h1_holds_ r_<=_||.f.||_+_||.g.|| let r be Real; ::_thesis: ( r in PreNorms h1 implies r <= ||.f.|| + ||.g.|| ) assume r in PreNorms h1 ; ::_thesis: r <= ||.f.|| + ||.g.|| then ex t being Element of X st r = ||.(h1 . t).|| ; hence r <= ||.f.|| + ||.g.|| by A10; ::_thesis: verum end; ( ( for s being real number st s in PreNorms h1 holds s <= ||.f.|| + ||.g.|| ) implies upper_bound (PreNorms h1) <= ||.f.|| + ||.g.|| ) by SEQ_4:45; hence ||.(f + g).|| <= ||.f.|| + ||.g.|| by A12, Th14; ::_thesis: verum end; A13: ||.(a * f).|| = (abs a) * ||.f.|| proof reconsider f1 = f, h1 = a * f as bounded Function of X, the carrier of Y by Def5; A14: ( ( for s being real number st s in PreNorms h1 holds s <= (abs a) * ||.f.|| ) implies upper_bound (PreNorms h1) <= (abs a) * ||.f.|| ) by SEQ_4:45; A15: now__::_thesis:_for_t_being_Element_of_X_holds_||.(h1_._t).||_<=_(abs_a)_*_||.f.|| let t be Element of X; ::_thesis: ||.(h1 . t).|| <= (abs a) * ||.f.|| A16: 0 <= abs a by COMPLEX1:46; ( ||.(h1 . t).|| = ||.(a * (f1 . t)).|| & ||.(a * (f1 . t)).|| = (abs a) * ||.(f1 . t).|| ) by Th20, NORMSP_1:def_1; hence ||.(h1 . t).|| <= (abs a) * ||.f.|| by A16, Th16, XREAL_1:64; ::_thesis: verum end; A17: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_h1_holds_ r_<=_(abs_a)_*_||.f.|| let r be Real; ::_thesis: ( r in PreNorms h1 implies r <= (abs a) * ||.f.|| ) assume r in PreNorms h1 ; ::_thesis: r <= (abs a) * ||.f.|| then ex t being Element of X st r = ||.(h1 . t).|| ; hence r <= (abs a) * ||.f.|| by A15; ::_thesis: verum end; A18: now__::_thesis:_(_(_a_<>_0_&_(abs_a)_*_||.f.||_<=_||.(a_*_f).||_)_or_(_a_=_0_&_(abs_a)_*_||.f.||_=_||.(a_*_f).||_)_) percases ( a <> 0 or a = 0 ) ; caseA19: a <> 0 ; ::_thesis: (abs a) * ||.f.|| <= ||.(a * f).|| A20: now__::_thesis:_for_t_being_Element_of_X_holds_||.(f1_._t).||_<=_((abs_a)_")_*_||.(a_*_f).|| let t be Element of X; ::_thesis: ||.(f1 . t).|| <= ((abs a) ") * ||.(a * f).|| A21: abs (a ") = abs (1 * (a ")) .= abs (1 / a) by XCMPLX_0:def_9 .= 1 / (abs a) by ABSVALUE:7 .= 1 * ((abs a) ") by XCMPLX_0:def_9 .= (abs a) " ; h1 . t = a * (f1 . t) by Th20; then A22: (a ") * (h1 . t) = ((a ") * a) * (f1 . t) by RLVECT_1:def_7 .= 1 * (f1 . t) by A19, XCMPLX_0:def_7 .= f1 . t by RLVECT_1:def_8 ; ( ||.((a ") * (h1 . t)).|| = (abs (a ")) * ||.(h1 . t).|| & 0 <= abs (a ") ) by COMPLEX1:46, NORMSP_1:def_1; hence ||.(f1 . t).|| <= ((abs a) ") * ||.(a * f).|| by A22, A21, Th16, XREAL_1:64; ::_thesis: verum end; A23: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_f1_holds_ r_<=_((abs_a)_")_*_||.(a_*_f).|| let r be Real; ::_thesis: ( r in PreNorms f1 implies r <= ((abs a) ") * ||.(a * f).|| ) assume r in PreNorms f1 ; ::_thesis: r <= ((abs a) ") * ||.(a * f).|| then ex t being Element of X st r = ||.(f1 . t).|| ; hence r <= ((abs a) ") * ||.(a * f).|| by A20; ::_thesis: verum end; A24: ( ( for s being real number st s in PreNorms f1 holds s <= ((abs a) ") * ||.(a * f).|| ) implies upper_bound (PreNorms f1) <= ((abs a) ") * ||.(a * f).|| ) by SEQ_4:45; ( (BoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms f1) & 0 <= abs a ) by Th14, COMPLEX1:46; then (abs a) * ||.f.|| <= (abs a) * (((abs a) ") * ||.(a * f).||) by A23, A24, XREAL_1:64; then A25: (abs a) * ||.f.|| <= ((abs a) * ((abs a) ")) * ||.(a * f).|| ; abs a <> 0 by A19, COMPLEX1:47; then (abs a) * ||.f.|| <= 1 * ||.(a * f).|| by A25, XCMPLX_0:def_7; hence (abs a) * ||.f.|| <= ||.(a * f).|| ; ::_thesis: verum end; caseA26: a = 0 ; ::_thesis: (abs a) * ||.f.|| = ||.(a * f).|| reconsider fz = f as VECTOR of (R_VectorSpace_of_BoundedFunctions (X,Y)) ; A27: a * f = a * fz .= 0. (R_VectorSpace_of_BoundedFunctions (X,Y)) by A26, RLVECT_1:10 .= 0. (R_NormSpace_of_BoundedFunctions (X,Y)) ; thus (abs a) * ||.f.|| = 0 * ||.f.|| by A26, ABSVALUE:2 .= ||.(a * f).|| by A27, Th18 ; ::_thesis: verum end; end; end; (BoundedFunctionsNorm (X,Y)) . (a * f) = upper_bound (PreNorms h1) by Th14; hence ||.(a * f).|| = (abs a) * ||.f.|| by A17, A14, A18, XXREAL_0:1; ::_thesis: verum end; now__::_thesis:_(_||.f.||_=_0_implies_f_=_0._(R_NormSpace_of_BoundedFunctions_(X,Y))_) reconsider g = f as bounded Function of X, the carrier of Y by Def5; set z = X --> (0. Y); reconsider z = X --> (0. Y) as Function of X, the carrier of Y ; assume A28: ||.f.|| = 0 ; ::_thesis: f = 0. (R_NormSpace_of_BoundedFunctions (X,Y)) now__::_thesis:_for_t_being_Element_of_X_holds_g_._t_=_z_._t let t be Element of X; ::_thesis: g . t = z . t ||.(g . t).|| <= ||.f.|| by Th16; then ||.(g . t).|| = 0 by A28; hence g . t = 0. Y by NORMSP_0:def_5 .= z . t by FUNCOP_1:7 ; ::_thesis: verum end; then g = z by FUNCT_2:63; hence f = 0. (R_NormSpace_of_BoundedFunctions (X,Y)) by Th15; ::_thesis: verum end; hence ( ( ||.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.|| ) by A1, A13, A9; ::_thesis: verum end; theorem Th22: :: RSSPACE4:22 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 let X be non empty set ; ::_thesis: 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 ) let Y be RealNormSpace; ::_thesis: ( 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 ) thus ||.(0. (R_NormSpace_of_BoundedFunctions (X,Y))).|| = 0 by Th21; :: according to NORMSP_0:def_6 ::_thesis: ( R_NormSpace_of_BoundedFunctions (X,Y) is discerning & R_NormSpace_of_BoundedFunctions (X,Y) is RealNormSpace-like ) for x, y being Point of (R_NormSpace_of_BoundedFunctions (X,Y)) for a being Real holds ( ( ||.x.|| = 0 implies x = 0. (R_NormSpace_of_BoundedFunctions (X,Y)) ) & ( x = 0. (R_NormSpace_of_BoundedFunctions (X,Y)) implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) by Th21; hence ( R_NormSpace_of_BoundedFunctions (X,Y) is discerning & R_NormSpace_of_BoundedFunctions (X,Y) is RealNormSpace-like ) by NORMSP_0:def_5, NORMSP_1:def_1; ::_thesis: verum end; theorem Th23: :: RSSPACE4:23 for X being non empty set for Y being RealNormSpace holds R_NormSpace_of_BoundedFunctions (X,Y) is RealNormSpace proof let X be non empty set ; ::_thesis: for Y being RealNormSpace holds R_NormSpace_of_BoundedFunctions (X,Y) is RealNormSpace let Y be RealNormSpace; ::_thesis: R_NormSpace_of_BoundedFunctions (X,Y) is RealNormSpace 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 ; hence R_NormSpace_of_BoundedFunctions (X,Y) is RealNormSpace by Th22, RSSPACE3:2; ::_thesis: verum 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 Th23; end; theorem Th24: :: RSSPACE4:24 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 let X be non empty set ; ::_thesis: 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) ) let Y be RealNormSpace; ::_thesis: 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) ) let f, g, h be Point of (R_NormSpace_of_BoundedFunctions (X,Y)); ::_thesis: 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) ) let f9, g9, h9 be bounded Function of X, the carrier of Y; ::_thesis: ( f9 = f & g9 = g & h9 = h implies ( h = f - g iff for x being Element of X holds h9 . x = (f9 . x) - (g9 . x) ) ) assume A1: ( f9 = f & g9 = g & h9 = h ) ; ::_thesis: ( h = f - g iff for x being Element of X holds h9 . x = (f9 . x) - (g9 . x) ) A2: now__::_thesis:_(_(_for_x_being_Element_of_X_holds_h9_._x_=_(f9_._x)_-_(g9_._x)_)_implies_f_-_g_=_h_) assume A3: for x being Element of X holds h9 . x = (f9 . x) - (g9 . x) ; ::_thesis: f - g = h now__::_thesis:_for_x_being_Element_of_X_holds_(h9_._x)_+_(g9_._x)_=_f9_._x let x be Element of X; ::_thesis: (h9 . x) + (g9 . x) = f9 . x h9 . x = (f9 . x) - (g9 . x) by A3; then (h9 . x) + (g9 . x) = (f9 . x) - ((g9 . x) - (g9 . x)) by RLVECT_1:29; then (h9 . x) + (g9 . x) = (f9 . x) - (0. Y) by RLVECT_1:15; hence (h9 . x) + (g9 . x) = f9 . x by RLVECT_1:13; ::_thesis: verum end; then f = h + g by A1, Th19; then f - g = h + (g - g) by RLVECT_1:def_3; then f - g = h + (0. (R_NormSpace_of_BoundedFunctions (X,Y))) by RLVECT_1:15; hence f - g = h by RLVECT_1:4; ::_thesis: verum end; now__::_thesis:_(_h_=_f_-_g_implies_for_x_being_Element_of_X_holds_h9_._x_=_(f9_._x)_-_(g9_._x)_) assume h = f - g ; ::_thesis: for x being Element of X holds h9 . x = (f9 . x) - (g9 . x) then h + g = f - (g - g) by RLVECT_1:29; then h + g = f - (0. (R_NormSpace_of_BoundedFunctions (X,Y))) by RLVECT_1:15; then A4: h + g = f by RLVECT_1:13; now__::_thesis:_for_x_being_Element_of_X_holds_(f9_._x)_-_(g9_._x)_=_h9_._x let x be Element of X; ::_thesis: (f9 . x) - (g9 . x) = h9 . x f9 . x = (h9 . x) + (g9 . x) by A1, A4, Th19; then (f9 . x) - (g9 . x) = (h9 . x) + ((g9 . x) - (g9 . x)) by RLVECT_1:def_3; then (f9 . x) - (g9 . x) = (h9 . x) + (0. Y) by RLVECT_1:15; hence (f9 . x) - (g9 . x) = h9 . x by RLVECT_1:4; ::_thesis: verum end; hence for x being Element of X holds h9 . x = (f9 . x) - (g9 . x) ; ::_thesis: verum end; hence ( h = f - g iff for x being Element of X holds h9 . x = (f9 . x) - (g9 . x) ) by A2; ::_thesis: verum end; Lm7: 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 let e be Real; ::_thesis: 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 let seq be Real_Sequence; ::_thesis: ( seq is convergent & ex k being Element of NAT st for i being Element of NAT st k <= i holds seq . i <= e implies lim seq <= e ) assume that A1: seq is convergent and A2: ex k being Element of NAT st for i being Element of NAT st k <= i holds seq . i <= e ; ::_thesis: lim seq <= e consider k being Element of NAT such that A3: for i being Element of NAT st k <= i holds seq . i <= e by A2; reconsider cseq = NAT --> e as Real_Sequence ; A4: lim cseq = cseq . 0 by SEQ_4:26 .= e by FUNCOP_1:7 ; A5: now__::_thesis:_for_i_being_Element_of_NAT_holds_(seq_^\_k)_._i_<=_cseq_._i let i be Element of NAT ; ::_thesis: (seq ^\ k) . i <= cseq . i ( (seq ^\ k) . i = seq . (k + i) & seq . (k + i) <= e ) by A3, NAT_1:11, NAT_1:def_3; hence (seq ^\ k) . i <= cseq . i by FUNCOP_1:7; ::_thesis: verum end; lim (seq ^\ k) = lim seq by A1, SEQ_4:20; hence lim seq <= e by A1, A5, A4, SEQ_2:18; ::_thesis: verum end; theorem Th25: :: RSSPACE4:25 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 Cauchy_sequence_by_Norm holds seq is convergent proof let X be non empty set ; ::_thesis: for Y being RealNormSpace st Y is complete holds for seq being sequence of (R_NormSpace_of_BoundedFunctions (X,Y)) st seq is Cauchy_sequence_by_Norm holds seq is convergent let Y be RealNormSpace; ::_thesis: ( Y is complete implies for seq being sequence of (R_NormSpace_of_BoundedFunctions (X,Y)) st seq is Cauchy_sequence_by_Norm holds seq is convergent ) assume A1: Y is complete ; ::_thesis: for seq being sequence of (R_NormSpace_of_BoundedFunctions (X,Y)) st seq is Cauchy_sequence_by_Norm holds seq is convergent let vseq be sequence of (R_NormSpace_of_BoundedFunctions (X,Y)); ::_thesis: ( vseq is Cauchy_sequence_by_Norm implies vseq is convergent ) assume A2: vseq is Cauchy_sequence_by_Norm ; ::_thesis: vseq is convergent defpred S1[ set , set ] means ex xseq being sequence of Y st ( ( for n being Element of NAT holds xseq . n = (modetrans ((vseq . n),X,Y)) . $1 ) & xseq is convergent & $2 = lim xseq ); A3: for x being Element of X ex y being Element of Y st S1[x,y] proof let x be Element of X; ::_thesis: ex y being Element of Y st S1[x,y] deffunc H1( Element of NAT ) -> Element of the carrier of Y = (modetrans ((vseq . $1),X,Y)) . x; consider xseq being sequence of Y such that A4: for n being Element of NAT holds xseq . n = H1(n) from FUNCT_2:sch_4(); take lim xseq ; ::_thesis: S1[x, lim xseq] A5: for m, k being Element of NAT holds ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| proof let m, k be Element of NAT ; ::_thesis: ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| vseq . k is bounded Function of X, the carrier of Y by Def5; then A6: modetrans ((vseq . k),X,Y) = vseq . k by Th13; reconsider h1 = (vseq . m) - (vseq . k) as bounded Function of X, the carrier of Y by Def5; vseq . m is bounded Function of X, the carrier of Y by Def5; then A7: modetrans ((vseq . m),X,Y) = vseq . m by Th13; ( xseq . m = (modetrans ((vseq . m),X,Y)) . x & xseq . k = (modetrans ((vseq . k),X,Y)) . x ) by A4; then (xseq . m) - (xseq . k) = h1 . x by A7, A6, Th24; hence ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| by Th16; ::_thesis: verum end; now__::_thesis:_for_e_being_Real_st_e_>_0_holds_ ex_k_being_Element_of_NAT_st_ for_n,_m_being_Element_of_NAT_st_n_>=_k_&_m_>=_k_holds_ ||.((xseq_._n)_-_(xseq_._m)).||_<_e let e be Real; ::_thesis: ( e > 0 implies ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.((xseq . n) - (xseq . m)).|| < e ) assume A8: e > 0 ; ::_thesis: ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.((xseq . n) - (xseq . m)).|| < e thus ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.((xseq . n) - (xseq . m)).|| < e ::_thesis: verum proof consider k being Element of NAT such that A9: for n, m being Element of NAT st n >= k & m >= k holds ||.((vseq . n) - (vseq . m)).|| < e by A2, A8, RSSPACE3:8; take k ; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds ||.((xseq . n) - (xseq . m)).|| < e thus for n, m being Element of NAT st n >= k & m >= k holds ||.((xseq . n) - (xseq . m)).|| < e ::_thesis: verum proof let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies ||.((xseq . n) - (xseq . m)).|| < e ) assume ( n >= k & m >= k ) ; ::_thesis: ||.((xseq . n) - (xseq . m)).|| < e then A10: ||.((vseq . n) - (vseq . m)).|| < e by A9; ||.((xseq . n) - (xseq . m)).|| <= ||.((vseq . n) - (vseq . m)).|| by A5; hence ||.((xseq . n) - (xseq . m)).|| < e by A10, XXREAL_0:2; ::_thesis: verum end; end; end; then xseq is Cauchy_sequence_by_Norm by RSSPACE3:8; then xseq is convergent by A1, LOPBAN_1:def_15; hence S1[x, lim xseq] by A4; ::_thesis: verum end; consider f being Function of X, the carrier of Y such that A11: for x being Element of X holds S1[x,f . x] from FUNCT_2:sch_3(A3); reconsider tseq = f as Function of X, the carrier of Y ; now__::_thesis:_for_e1_being_real_number_st_e1_>_0_holds_ ex_k_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_m_>=_k_holds_ abs_((||.vseq.||_._m)_-_(||.vseq.||_._k))_<_e1 let e1 be real number ; ::_thesis: ( e1 > 0 implies ex k being Element of NAT st for m being Element of NAT st m >= k holds abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1 ) assume A12: e1 > 0 ; ::_thesis: ex k being Element of NAT st for m being Element of NAT st m >= k holds abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1 reconsider e = e1 as Real by XREAL_0:def_1; consider k being Element of NAT such that A13: for n, m being Element of NAT st n >= k & m >= k holds ||.((vseq . n) - (vseq . m)).|| < e by A2, A12, RSSPACE3:8; take k = k; ::_thesis: for m being Element of NAT st m >= k holds abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1 now__::_thesis:_for_m_being_Element_of_NAT_st_m_>=_k_holds_ abs_((||.vseq.||_._m)_-_(||.vseq.||_._k))_<_e1 let m be Element of NAT ; ::_thesis: ( m >= k implies abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1 ) assume m >= k ; ::_thesis: abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1 then A14: ( ||.(vseq . m).|| = ||.vseq.|| . m & ||.((vseq . m) - (vseq . k)).|| < e ) by A13, NORMSP_0:def_4; ( abs (||.(vseq . m).|| - ||.(vseq . k).||) <= ||.((vseq . m) - (vseq . k)).|| & ||.(vseq . k).|| = ||.vseq.|| . k ) by NORMSP_0:def_4, NORMSP_1:9; hence abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1 by A14, XXREAL_0:2; ::_thesis: verum end; hence for m being Element of NAT st m >= k holds abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1 ; ::_thesis: verum end; then A15: ||.vseq.|| is convergent by SEQ_4:41; A16: tseq is bounded proof take lim ||.vseq.|| ; :: according to RSSPACE4:def_4 ::_thesis: ( 0 <= lim ||.vseq.|| & ( for x being Element of X holds ||.(tseq . x).|| <= lim ||.vseq.|| ) ) A17: now__::_thesis:_for_x_being_Element_of_X_holds_||.(tseq_._x).||_<=_lim_||.vseq.|| let x be Element of X; ::_thesis: ||.(tseq . x).|| <= lim ||.vseq.|| consider xseq being sequence of Y such that A18: for n being Element of NAT holds xseq . n = (modetrans ((vseq . n),X,Y)) . x and A19: ( xseq is convergent & tseq . x = lim xseq ) by A11; A20: for m being Element of NAT holds ||.(xseq . m).|| <= ||.(vseq . m).|| proof let m be Element of NAT ; ::_thesis: ||.(xseq . m).|| <= ||.(vseq . m).|| ( vseq . m is bounded Function of X, the carrier of Y & xseq . m = (modetrans ((vseq . m),X,Y)) . x ) by A18, Def5; hence ||.(xseq . m).|| <= ||.(vseq . m).|| by Th13, Th16; ::_thesis: verum end; A21: for n being Element of NAT holds ||.xseq.|| . n <= ||.vseq.|| . n proof let n be Element of NAT ; ::_thesis: ||.xseq.|| . n <= ||.vseq.|| . n ( ||.xseq.|| . n = ||.(xseq . n).|| & ||.(xseq . n).|| <= ||.(vseq . n).|| ) by A20, NORMSP_0:def_4; hence ||.xseq.|| . n <= ||.vseq.|| . n by NORMSP_0:def_4; ::_thesis: verum end; ( ||.xseq.|| is convergent & ||.(tseq . x).|| = lim ||.xseq.|| ) by A19, LOPBAN_1:41; hence ||.(tseq . x).|| <= lim ||.vseq.|| by A15, A21, SEQ_2:18; ::_thesis: verum end; now__::_thesis:_for_n_being_Element_of_NAT_holds_||.vseq.||_._n_>=_0 let n be Element of NAT ; ::_thesis: ||.vseq.|| . n >= 0 ||.(vseq . n).|| >= 0 ; hence ||.vseq.|| . n >= 0 by NORMSP_0:def_4; ::_thesis: verum end; hence ( 0 <= lim ||.vseq.|| & ( for x being Element of X holds ||.(tseq . x).|| <= lim ||.vseq.|| ) ) by A15, A17, SEQ_2:17; ::_thesis: verum end; A22: for e being Real st e > 0 holds ex k being Element of NAT st for n being Element of NAT st n >= k holds for x being Element of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e proof let e be Real; ::_thesis: ( e > 0 implies ex k being Element of NAT st for n being Element of NAT st n >= k holds for x being Element of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e ) assume e > 0 ; ::_thesis: ex k being Element of NAT st for n being Element of NAT st n >= k holds for x being Element of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e then consider k being Element of NAT such that A23: for n, m being Element of NAT st n >= k & m >= k holds ||.((vseq . n) - (vseq . m)).|| < e by A2, RSSPACE3:8; take k ; ::_thesis: for n being Element of NAT st n >= k holds for x being Element of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_k_holds_ for_x_being_Element_of_X_holds_||.(((modetrans_((vseq_._n),X,Y))_._x)_-_(tseq_._x)).||_<=_e let n be Element of NAT ; ::_thesis: ( n >= k implies for x being Element of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e ) assume A24: n >= k ; ::_thesis: for x being Element of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e now__::_thesis:_for_x_being_Element_of_X_holds_||.(((modetrans_((vseq_._n),X,Y))_._x)_-_(tseq_._x)).||_<=_e let x be Element of X; ::_thesis: ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e consider xseq being sequence of Y such that A25: for n being Element of NAT holds xseq . n = (modetrans ((vseq . n),X,Y)) . x and A26: ( xseq is convergent & tseq . x = lim xseq ) by A11; A27: for m, k being Element of NAT holds ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| proof let m, k be Element of NAT ; ::_thesis: ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| vseq . k is bounded Function of X, the carrier of Y by Def5; then A28: modetrans ((vseq . k),X,Y) = vseq . k by Th13; reconsider h1 = (vseq . m) - (vseq . k) as bounded Function of X, the carrier of Y by Def5; vseq . m is bounded Function of X, the carrier of Y by Def5; then A29: modetrans ((vseq . m),X,Y) = vseq . m by Th13; ( xseq . m = (modetrans ((vseq . m),X,Y)) . x & xseq . k = (modetrans ((vseq . k),X,Y)) . x ) by A25; then (xseq . m) - (xseq . k) = h1 . x by A29, A28, Th24; hence ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| by Th16; ::_thesis: verum end; A30: for m being Element of NAT st m >= k holds ||.((xseq . n) - (xseq . m)).|| <= e proof let m be Element of NAT ; ::_thesis: ( m >= k implies ||.((xseq . n) - (xseq . m)).|| <= e ) assume m >= k ; ::_thesis: ||.((xseq . n) - (xseq . m)).|| <= e then A31: ||.((vseq . n) - (vseq . m)).|| < e by A23, A24; ||.((xseq . n) - (xseq . m)).|| <= ||.((vseq . n) - (vseq . m)).|| by A27; hence ||.((xseq . n) - (xseq . m)).|| <= e by A31, XXREAL_0:2; ::_thesis: verum end; ||.((xseq . n) - (tseq . x)).|| <= e proof deffunc H1( Element of NAT ) -> Element of REAL = ||.((xseq . $1) - (xseq . n)).||; consider rseq being Real_Sequence such that A32: for m being Element of NAT holds rseq . m = H1(m) from SEQ_1:sch_1(); now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_ rseq_._x_=_||.(xseq_-_(xseq_._n)).||_._x let x be set ; ::_thesis: ( x in NAT implies rseq . x = ||.(xseq - (xseq . n)).|| . x ) assume x in NAT ; ::_thesis: rseq . x = ||.(xseq - (xseq . n)).|| . x then reconsider k = x as Element of NAT ; thus rseq . x = ||.((xseq . k) - (xseq . n)).|| by A32 .= ||.((xseq - (xseq . n)) . k).|| by NORMSP_1:def_4 .= ||.(xseq - (xseq . n)).|| . x by NORMSP_0:def_4 ; ::_thesis: verum end; then A33: rseq = ||.(xseq - (xseq . n)).|| by FUNCT_2:12; A34: ( xseq - (xseq . n) is convergent & lim (xseq - (xseq . n)) = (tseq . x) - (xseq . n) ) by A26, NORMSP_1:21, NORMSP_1:27; then A35: lim rseq = ||.((tseq . x) - (xseq . n)).|| by A33, LOPBAN_1:20; for m being Element of NAT st m >= k holds rseq . m <= e proof let m be Element of NAT ; ::_thesis: ( m >= k implies rseq . m <= e ) assume A36: m >= k ; ::_thesis: rseq . m <= e rseq . m = ||.((xseq . m) - (xseq . n)).|| by A32 .= ||.((xseq . n) - (xseq . m)).|| by NORMSP_1:7 ; hence rseq . m <= e by A30, A36; ::_thesis: verum end; then lim rseq <= e by A34, A33, Lm7, LOPBAN_1:20; hence ||.((xseq . n) - (tseq . x)).|| <= e by A35, NORMSP_1:7; ::_thesis: verum end; hence ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e by A25; ::_thesis: verum end; hence for x being Element of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e ; ::_thesis: verum end; hence for n being Element of NAT st n >= k holds for x being Element of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e ; ::_thesis: verum end; reconsider tseq = tseq as bounded Function of X, the carrier of Y by A16; reconsider tv = tseq as Point of (R_NormSpace_of_BoundedFunctions (X,Y)) by Def5; A37: for e being Real st e > 0 holds ex k being Element of NAT st for n being Element of NAT st n >= k holds ||.((vseq . n) - tv).|| <= e proof let e be Real; ::_thesis: ( e > 0 implies ex k being Element of NAT st for n being Element of NAT st n >= k holds ||.((vseq . n) - tv).|| <= e ) assume e > 0 ; ::_thesis: ex k being Element of NAT st for n being Element of NAT st n >= k holds ||.((vseq . n) - tv).|| <= e then consider k being Element of NAT such that A38: for n being Element of NAT st n >= k holds for x being Element of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e by A22; now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_k_holds_ ||.((vseq_._n)_-_tv).||_<=_e set g1 = tseq; let n be Element of NAT ; ::_thesis: ( n >= k implies ||.((vseq . n) - tv).|| <= e ) assume A39: n >= k ; ::_thesis: ||.((vseq . n) - tv).|| <= e reconsider h1 = (vseq . n) - tv as bounded Function of X, the carrier of Y by Def5; set f1 = modetrans ((vseq . n),X,Y); A40: now__::_thesis:_for_t_being_Element_of_X_holds_||.(h1_._t).||_<=_e let t be Element of X; ::_thesis: ||.(h1 . t).|| <= e vseq . n is bounded Function of X, the carrier of Y by Def5; then modetrans ((vseq . n),X,Y) = vseq . n by Th13; then ||.(h1 . t).|| = ||.(((modetrans ((vseq . n),X,Y)) . t) - (tseq . t)).|| by Th24; hence ||.(h1 . t).|| <= e by A38, A39; ::_thesis: verum end; A41: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_h1_holds_ r_<=_e let r be Real; ::_thesis: ( r in PreNorms h1 implies r <= e ) assume r in PreNorms h1 ; ::_thesis: r <= e then ex t being Element of X st r = ||.(h1 . t).|| ; hence r <= e by A40; ::_thesis: verum end; ( ( for s being real number st s in PreNorms h1 holds s <= e ) implies upper_bound (PreNorms h1) <= e ) by SEQ_4:45; hence ||.((vseq . n) - tv).|| <= e by A41, Th14; ::_thesis: verum end; hence ex k being Element of NAT st for n being Element of NAT st n >= k holds ||.((vseq . n) - tv).|| <= e ; ::_thesis: verum end; for e being Real st e > 0 holds ex m being Element of NAT st for n being Element of NAT st n >= m holds ||.((vseq . n) - tv).|| < e proof let e be Real; ::_thesis: ( e > 0 implies ex m being Element of NAT st for n being Element of NAT st n >= m holds ||.((vseq . n) - tv).|| < e ) assume A42: e > 0 ; ::_thesis: ex m being Element of NAT st for n being Element of NAT st n >= m holds ||.((vseq . n) - tv).|| < e consider m being Element of NAT such that A43: for n being Element of NAT st n >= m holds ||.((vseq . n) - tv).|| <= e / 2 by A37, A42, XREAL_1:215; A44: e / 2 < e by A42, XREAL_1:216; now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_m_holds_ ||.((vseq_._n)_-_tv).||_<_e let n be Element of NAT ; ::_thesis: ( n >= m implies ||.((vseq . n) - tv).|| < e ) assume n >= m ; ::_thesis: ||.((vseq . n) - tv).|| < e then ||.((vseq . n) - tv).|| <= e / 2 by A43; hence ||.((vseq . n) - tv).|| < e by A44, XXREAL_0:2; ::_thesis: verum end; hence ex m being Element of NAT st for n being Element of NAT st n >= m holds ||.((vseq . n) - tv).|| < e ; ::_thesis: verum end; hence vseq is convergent by NORMSP_1:def_6; ::_thesis: verum end; theorem Th26: :: RSSPACE4:26 for X being non empty set for Y being RealBanachSpace holds R_NormSpace_of_BoundedFunctions (X,Y) is RealBanachSpace proof let X be non empty set ; ::_thesis: for Y being RealBanachSpace holds R_NormSpace_of_BoundedFunctions (X,Y) is RealBanachSpace let Y be RealBanachSpace; ::_thesis: R_NormSpace_of_BoundedFunctions (X,Y) is RealBanachSpace for seq being sequence of (R_NormSpace_of_BoundedFunctions (X,Y)) st seq is Cauchy_sequence_by_Norm holds seq is convergent by Th25; hence R_NormSpace_of_BoundedFunctions (X,Y) is RealBanachSpace by LOPBAN_1:def_15; ::_thesis: verum 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 Th26; end;