:: Banach Space of Bounded Real Sequences :: by Yasumasa Suzuki :: :: Received January 6, 2004 :: Copyright (c) 2004-2012 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SEQ_1, XREAL_0, ORDINAL1, SUBSET_1, FUNCT_1, XXREAL_0, ORDINAL2, RELAT_1, XXREAL_2, RSSPACE, TARSKI, XBOOLE_0, NAT_1, CARD_1, RLSUB_1, REAL_1, RLVECT_1, VALUED_1, ARYTM_3, ALGSTR_0, COMPLEX1, SEQ_4, NORMSP_1, STRUCT_0, SUPINF_2, ARYTM_1, ZFMISC_1, REALSET1, PRE_TOPC, MEMBER_1, RSSPACE3, SEQ_2, FUNCOP_1, FUNCSDOM, FUNCT_2, LOPBAN_1, REWRITE1, RSSPACE4, METRIC_1, RELAT_2, NORMSP_0; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MCART_1, RELAT_1, PRE_TOPC, DOMAIN_1, FUNCOP_1, REALSET1, XXREAL_0, XXREAL_2, COMPLEX1, REAL_1, ORDINAL1, NAT_1, STRUCT_0, ALGSTR_0, XREAL_0, NUMBERS, FUNCT_1, RELSET_1, FUNCT_2, INTEGRA2, RLVECT_1, NORMSP_0, NORMSP_1, VALUED_1, SEQ_1, SEQ_2, SEQ_4, RLSUB_1, PARTFUN1, RSSPACE, RSSPACE3, LOPBAN_1; constructors REAL_1, COMPLEX1, REALSET1, RLSUB_1, INTEGRA2, RSSPACE3, LOPBAN_1, SEQ_1, RVSUM_1, SEQ_4, RELSET_1, BINOP_2, SEQ_2, SERIES_1, COMSEQ_2, BINOP_1; registrations SUBSET_1, RELAT_1, ORDINAL1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, REALSET1, STRUCT_0, RLVECT_1, RFUNCT_1, SEQ_2, NORMSP_1, RSSPACE3, VALUED_0, RSSPACE, VALUED_1, FUNCOP_1, SEQ_4, NORMSP_0, RELSET_1; requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM; definitions TARSKI, XBOOLE_0, NORMSP_1, RLVECT_1, BINOP_1, REALSET1, STRUCT_0, ALGSTR_0, VALUED_1, NORMSP_0, XXREAL_2; theorems RELAT_1, TARSKI, ABSVALUE, ZFMISC_1, XBOOLE_0, NAT_1, FUNCOP_1, SEQ_1, SEQ_2, SEQM_3, SEQ_4, FUNCT_1, FUNCT_2, RLVECT_1, RLSUB_1, NORMSP_1, XREAL_0, XCMPLX_0, INTEGRA2, RSSPACE, RSSPACE3, RFUNCT_2, RSSPACE2, LOPBAN_1, COMPLEX1, XREAL_1, XXREAL_0, XXREAL_2, VALUED_0, ORDINAL1, MEASURE6, NORMSP_0; schemes SEQ_1, FUNCT_2, XBOOLE_0; begin :: The Banach Space of Bounded Real Sequences Lm1: for rseq be Real_Sequence for K be real number st (for n be Element of NAT holds rseq.n <= K) holds upper_bound rng rseq <= K proof let rseq be Real_Sequence; let K be real number such that A1: for n be Element of NAT holds rseq.n <= K; now let s be real number; assume s in rng rseq; then ex n be set st n in NAT & rseq.n=s by FUNCT_2:11; hence s <=K by A1; end; hence thesis by SEQ_4:45; end; Lm2: for rseq be Real_Sequence st rseq is bounded holds for n be Element of NAT holds rseq.n <= upper_bound rng rseq proof let rseq be Real_Sequence; assume rseq is bounded; 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; NAT = dom rseq by FUNCT_2:def 1; then rseq.n in rng rseq by FUNCT_1:3; hence thesis by A1,SEQ_4:def 1; end; definition func the_set_of_BoundedRealSequences -> Subset of Linear_Space_of_RealSequences means :Def1: for x being set holds x in it iff x in the_set_of_RealSequences & seq_id x is bounded; existence proof defpred P[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 & P[x] from XBOOLE_0:sch 1; for x be 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 thesis by A1,RSSPACE:def 7; end; uniqueness proof let X1,X2 be Subset of Linear_Space_of_RealSequences; 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; thus X1 c= X2 proof let x be set; assume x in X1; then x in the_set_of_RealSequences & seq_id(x) is bounded by A2; hence thesis by A3; end; let x be set; assume x in X2; then x in the_set_of_RealSequences & seq_id(x) is bounded by A3; hence thesis by A2; end; end; registration cluster the_set_of_BoundedRealSequences -> non empty; coherence 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; n in NAT by ORDINAL1:def 12; hence thesis by RSSPACE:def 6; end; then rseq is constant by VALUED_0:def 18; hence thesis; end; hence thesis by Def1; end; cluster the_set_of_BoundedRealSequences -> linearly-closed; coherence proof set W = the_set_of_BoundedRealSequences; A1: for a be Real for v be VECTOR of Linear_Space_of_RealSequences st v in W holds a * v in W proof let a be Real; let v be VECTOR of Linear_Space_of_RealSequences; assume v in W; then A2: seq_id v is bounded by Def1; seq_id(a*v) =seq_id(a(#)seq_id(v)) by RSSPACE:3,def 7 .=a(#)seq_id(v) by RSSPACE:1; then seq_id(a*v) is bounded by A2,SEQM_3:37; hence thesis by Def1,RSSPACE:def 7; end; for v,u be 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; assume v in W & u in W; 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,def 7 .=seq_id v+seq_id u by RSSPACE:1; hence thesis by A3,Def1,RSSPACE:def 7; end; hence thesis by A1,RLSUB_1:def 1; 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) #) -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital; coherence 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 add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital; definition func linfty_norm -> Function of the_set_of_BoundedRealSequences, REAL means :Def2: for x be set st x in the_set_of_BoundedRealSequences holds it.x = upper_bound rng abs seq_id x; existence proof deffunc F(set) = upper_bound rng abs seq_id($1); A1: for z be set st z in the_set_of_BoundedRealSequences holds F(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 = F(x) from FUNCT_2 :sch 2(A1); hence thesis; end; uniqueness proof let NORM1,NORM2 be Function of the_set_of_BoundedRealSequences, REAL such that A2: for x be set st x in the_set_of_BoundedRealSequences holds NORM1.x = upper_bound rng abs seq_id x and A3: for x be set st x in the_set_of_BoundedRealSequences holds NORM2.x = upper_bound rng abs seq_id x; A4: for z be set st z in the_set_of_BoundedRealSequences holds NORM1.z = NORM2 . z proof let z be set such that A5: z in the_set_of_BoundedRealSequences; NORM1.z = upper_bound rng abs seq_id(z) by A2,A5; hence thesis by A3,A5; end; dom NORM1 = the_set_of_BoundedRealSequences & dom NORM2 = the_set_of_BoundedRealSequences by FUNCT_2:def 1; hence thesis by A4,FUNCT_1:2; end; end; Lm5: for rseq be Real_Sequence st (for n be Nat holds rseq.n=0) holds rseq is bounded & upper_bound rng abs rseq = 0 proof let rseq be Real_Sequence such that A1: for n be Nat holds rseq.n=0; A2: for n be Nat holds (abs rseq).n=0 proof let n be Nat; 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 thesis by A3,ABSVALUE:2; end; rng abs rseq c= {0} proof let y be set; assume y in rng abs rseq; then ex n be set st n in NAT & abs(rseq).n=y by FUNCT_2:11; then y=0 by A2; hence thesis by TARSKI:def 1; end; then A4: rng abs rseq = {0} by ZFMISC_1:33; rseq is constant by A1,VALUED_0:def 18; hence thesis by A4,SEQ_4:9; end; Lm6: for rseq be Real_Sequence st rseq is bounded & upper_bound rng abs rseq = 0 holds for n be Nat holds rseq.n = 0 proof let rseq be Real_Sequence such that A1: rseq is bounded & upper_bound rng abs rseq = 0; let n be Nat; 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 thesis by ABSVALUE:2; end; theorem for rseq be Real_Sequence holds rseq is bounded & upper_bound rng abs rseq = 0 iff for n be 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 #) -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital; coherence by Lm4,RSSPACE3:2; end; definition func linfty_Space -> non empty NORMSTR equals 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; end; theorem Th2: the carrier of linfty_Space = the_set_of_BoundedRealSequences & ( for x be set holds x is VECTOR of linfty_Space iff x is Real_Sequence & seq_id x is bounded ) & 0.linfty_Space = Zeroseq & ( for u be VECTOR of linfty_Space holds u = seq_id u ) & ( for u,v be VECTOR of linfty_Space holds u+v =seq_id(u) +seq_id(v) ) & ( for r be Real for u be VECTOR of linfty_Space holds r*u =r(#) seq_id(u) ) & ( for u be VECTOR of linfty_Space holds -u = -seq_id u & seq_id(- u) = -seq_id u ) & ( for u,v be VECTOR of linfty_Space holds u-v =seq_id(u)- seq_id(v) ) & ( for v be VECTOR of linfty_Space holds seq_id v is bounded ) & for v be VECTOR of linfty_Space holds ||.v.|| = upper_bound rng abs seq_id v proof set l1 =linfty_Space; A1: 0.l1 = 0.Linear_Space_of_RealSequences by RSSPACE:def 10 .= Zeroseq by RSSPACE:def 7; A2: for x be set holds x is Element of l1 iff x is Real_Sequence & seq_id x is bounded proof let x be set; x in the_set_of_RealSequences iff x is Real_Sequence by RSSPACE:def 1; hence thesis by Def1; end; A3: for u,v be VECTOR of l1 holds u+v =seq_id u+seq_id v proof let u,v be VECTOR of l1; 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 L1) = [:the carrier of L1,the carrier of L1:] by FUNCT_2:def 1; then A4: dom ((the addF of Linear_Space_of_RealSequences)||W) =[:W,W:] by RELAT_1:62 ; u+v =((the addF of Linear_Space_of_RealSequences)||W).[u,v] by RSSPACE:def 8 .=u1+v1 by A4,FUNCT_1:47; hence thesis by RSSPACE:2,def 7; end; A5: for r be Real for u be VECTOR of l1 holds r*u =r(#)seq_id u proof let r be Real; let u be VECTOR of l1; 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 L1) = [:REAL,the carrier of L1:] by FUNCT_2:def 1; then A6: dom ((the Mult of Linear_Space_of_RealSequences) | [:REAL,W:]) =[: REAL,W:] by RELAT_1:62,ZFMISC_1:96; r*u =((the Mult of Linear_Space_of_RealSequences)|[:REAL,W:]).[r,u] by RSSPACE:def 9 .=r*u1 by A6,FUNCT_1:47; hence thesis by RSSPACE:3,def 7; end; A7: for u be VECTOR of l1 holds u = seq_id u proof let u be VECTOR of l1; u is VECTOR of Linear_Space_of_RealSequences by Lm3,RLSUB_1:10; hence thesis by RSSPACE:def 2,def 7; end; A8: for u be VECTOR of l1 holds -u =-seq_id u & seq_id(-u)=-seq_id u proof let u be VECTOR of l1; -u = (-1)*u by RLVECT_1:16 .= -seq_id u by A5; hence thesis by A7; end; for u,v be VECTOR of l1 holds u-v =seq_id u-seq_id v proof let u,v be VECTOR of l1; thus u-v = seq_id u+seq_id(-v) by A3 .= seq_id u-seq_id v by A8; end; hence thesis by A2,A7,A3,A5,A8,A1,Def2; end; theorem Th3: for x, y being Point of linfty_Space, a be Real holds ( ||.x.|| = 0 iff x = 0.linfty_Space ) & 0 <= ||.x.|| & ||.x+y.|| <= ||.x.|| + ||.y.|| & ||. a*x .|| = abs(a) * ||.x.|| proof let x, y be Point of linfty_Space; let a be Real; A1: for n be Element of NAT holds (abs(a(#)seq_id x)).n =(abs a)*(abs( seq_id x).n) proof let n be Element of NAT; (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 thesis; 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 be 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; (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 thesis; end; A4: for n be 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; 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 thesis by SEQ_1:12; 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; (abs seq_id x).n + (abs seq_id y).n =((abs seq_id x) + (abs seq_id y) ).n by SEQ_1:7; hence thesis by A4; end; A6: now assume A7: x=0.linfty_Space; A8: for n be Nat holds (seq_id x).n=0 proof let n be Nat; n in NAT by ORDINAL1:def 12; hence thesis by A7,Th2,RSSPACE:def 6; end; thus ||.x.|| = upper_bound rng abs seq_id x by Th2 .= 0 by A8,Lm5; 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 A12: x in the_set_of_RealSequences by Def1; assume A13: ||.x.|| = 0; ||.x.|| = upper_bound rng abs seq_id x & seq_id x is bounded by Th2; then for n be Element of NAT holds 0 = (seq_id x).n by A13,Lm6; hence x=0.linfty_Space by A12,Th2,RSSPACE:def 6; end; A14: seq_id y is bounded by Def1; A15: seq_id x is bounded by Def1; now let n be Element of NAT; 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; 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 thesis by A11,A6,A9,A19,A18,Th2; end; registration cluster linfty_Space -> reflexive discerning RealNormSpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable; coherence proof thus ||.0.linfty_Space.|| = 0 by Th3; thus thesis by Th3,NORMSP_0:def 5,NORMSP_1:def 1; end; end; theorem for vseq be sequence of linfty_Space st vseq is Cauchy_sequence_by_Norm holds vseq is convergent proof let vseq be sequence of linfty_Space such that A1: vseq is Cauchy_sequence_by_Norm; defpred P[set,set] means ex i be Element of NAT st $1=i & ex rseqi be Real_Sequence st (for n be Element of NAT holds rseqi.n=(seq_id(vseq.n)).i) & rseqi is convergent & $2 = lim rseqi; A2: for x be set st x in NAT ex y be set st y in REAL & P[x,y] proof let x be set; assume x in NAT; then reconsider i=x as Element of NAT; deffunc F(Nat) = (seq_id(vseq.$1)).i; consider rseqi be Real_Sequence such that A3: for n be Element of NAT holds rseqi.n = F(n) from SEQ_1:sch 1; take lim rseqi; now let e be real number such that A4: e > 0; thus ex k be Element of NAT st for m be Element of NAT st k <= m holds abs(rseqi.m -rseqi.k) < e proof e is Real by XREAL_0:def 1; then consider k be Element of NAT such that A5: for n, m be Element of NAT st n >= k & m >= k holds ||.(vseq.n ) - (vseq.m).|| < e by A1,A4,RSSPACE3:8; take k; let m be Element of NAT such that A6: k<=m; 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 thesis by A7,A8,XXREAL_0:2; end; end; then rseqi is convergent by SEQ_4:41; hence thesis by A3; end; consider f be Function of NAT,REAL such that A9: for x be set st x in NAT holds P[x,f.x] from FUNCT_2:sch 1(A2); reconsider tseq=f as Real_Sequence; A10: now let i be Element of NAT; reconsider x=i as set; ex i0 be Element of NAT st x=i0 & ex rseqi be Real_Sequence st ( for n be Element of NAT holds rseqi.n=(seq_id(vseq.n)).i0 ) & rseqi is convergent & f.x=lim rseqi by A9; hence ex rseqi be Real_Sequence st ( for n be Element of NAT holds rseqi.n= (seq_id(vseq.n)).i ) & rseqi is convergent & tseq.i=lim rseqi; end; A11: for e be Real st e >0 ex k be Element of NAT st for n be 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 such that A12: e > 0; consider k be Element of NAT such that A13: for n, m be Element of NAT st n >= k & m >= k holds ||.(vseq.n) - (vseq.m).|| < e by A1,A12,RSSPACE3:8; A14: for m,n be 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; assume n >= k & m >= k; then A15: ||.(vseq.n) - (vseq.m).|| < e by A13; seq_id((vseq.n) - (vseq.m)) is bounded by Def1; hence thesis by A15,Def2; end; A16: for n be Element of NAT for i be Element of NAT holds for rseq be Real_Sequence st ( for m be 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; A17: for m,k be 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; seq_id((vseq.m) - (vseq.k)) = seq_id(seq_id(vseq.m)-seq_id(vseq.k )) by Th2; hence thesis by RSSPACE:1; end; now let i be Element of NAT; consider rseqi be Real_Sequence such that A18: for n be Element of NAT holds rseqi.n=(seq_id(vseq.n)).i and A19: rseqi is convergent & tseq.i=lim rseqi by A10; now let rseq be Real_Sequence such that A20: for m be Element of NAT holds rseq.m=abs(seq_id(vseq.m-vseq .n)).i; A21: now let m be Element of NAT; 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; 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; end; hence for rseq be Real_Sequence st ( for m be 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; end; hence thesis; end; for n be 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 such that A23: n >= k; A24: for i be Element of NAT holds abs((seq_id tseq -seq_id(vseq.n))).i <= e proof let i be Element of NAT; deffunc F(Element of NAT)= abs(seq_id((vseq.$1) - (vseq.n))).i; consider rseq be Real_Sequence such that A25: for m be Element of NAT holds rseq.m = F(m) from SEQ_1:sch 1; A26: for m be Element of NAT st m >= k holds rseq.m <= e proof let m be Element of NAT; A27: rseq.m = abs(seq_id((vseq.m) - (vseq.n))).i by A25; assume A28: m >= k; 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 thesis by A29,A27,XXREAL_0:2; end; rseq is convergent & lim rseq = abs(seq_id tseq-seq_id(vseq.n)).i by A16,A25; hence thesis by A26,RSSPACE2:5; end; A30: 0 + e < 1 + e by XREAL_1:8; now let i be Element of NAT; 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) = 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 be Element of NAT holds d.i <= (a+b).i proof let i be Element of NAT; A36: b.i=abs((seq_id(vseq.m)).i) & d.i=abs((seq_id tseq).i) by SEQ_1:12; a.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 d.i-b.i <= a.i by A36,COMPLEX1:59; then d.i-b.i+b.i<= a.i + b.i by XREAL_1:6; hence thesis by SEQ_1:7; end; d is bounded proof reconsider r=upper_bound rng (a+b)+1 as real number; b.1=abs( (seq_id(vseq.m)).1 ) by SEQ_1:12; then A37: 0<= b.1 by COMPLEX1:46; A38: upper_bound( rng(a+b) ) +0 < upper_bound( rng(a+b) )+1 by XREAL_1:8; A39: now let i be Element of NAT; d.i <= (a+b).i & (a+b).i <= upper_bound rng (a+b) by A33,A34,A35,Lm2; then A40: d.i <= upper_bound rng (a+b) by XXREAL_0:2; d.i=abs((seq_id tseq).i) by SEQ_1:12; hence abs((seq_id tseq).i) 0; set e=e1/2; consider m be Element of NAT such that A43: for n be 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)) <= e by A11,A42,XREAL_1:215; A44: e < e1 by A42,XREAL_1:216; now reconsider u=tseq as VECTOR of linfty_Space by A31,A41,Def1; let n be Element of NAT; assume n >= m; then A45: upper_bound rng( abs(seq_id tseq-seq_id(vseq.n))) <= e 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) <= e 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; end; hence thesis; end; begin definition let X be non empty set; let Y be RealNormSpace; let IT be Function of X, the carrier of Y; attr IT is bounded means :Def4: ex K being Real st 0 <= K & for x being Element of X holds ||. IT.x .|| <= K; end; theorem Th5: for X be non empty set for Y be RealNormSpace holds for f be Function of X,the carrier of Y st (for x be Element of X holds f.x=0.Y) holds f is bounded proof let X be non empty set; let Y be RealNormSpace; let f be Function of X,the carrier of Y such that A1: for x be Element of X holds f.x=0.Y; A2: now let x be Element of X; thus ||. f.x .|| = ||. 0.Y .|| by A1 .=0; end; take 0; thus thesis by A2; end; registration let X be non empty set; let Y be RealNormSpace; cluster bounded for Function of X,the carrier of Y; existence proof set f=X --> 0.Y; reconsider f as Function of X,the carrier of Y; take f; for x be Element of X holds f.x =0.Y by FUNCOP_1:7; hence thesis by Th5; end; end; definition let X be non empty set; let Y be RealNormSpace; func BoundedFunctions(X,Y) -> Subset of RealVectSpace(X,Y) means :Def5: for x being set holds x in it iff x is bounded Function of X,the carrier of Y; existence 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 P[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) & P[x] from XBOOLE_0:sch 1; take IT; for x be 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; let x be set; thus x in IT implies x is bounded Function of X,the carrier of Y by A2; assume A3: x is bounded Function of X,the carrier of Y; then x in Funcs(X,the carrier of Y) by FUNCT_2:8; hence thesis by A2,A3; end; uniqueness proof let X1,X2 be Subset of RealVectSpace(X,Y); 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; for x being set st x in X2 holds x in X1 proof let x be set; assume x in X2; then x is bounded Function of X,the carrier of Y by A5; hence thesis by A4; 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; assume x in X1; then x is bounded Function of X,the carrier of Y by A4; hence thesis by A5; end; then X1 c= X2 by TARSKI:def 3; hence thesis by A6,XBOOLE_0:def 10; end; end; registration let X be non empty set; let Y be RealNormSpace; cluster BoundedFunctions(X,Y) -> non empty; coherence proof set f=X --> 0.Y; reconsider f as Function of X,the carrier of Y; for x be Element of X holds f.x =0.Y by FUNCOP_1:7; then f is bounded by Th5; hence thesis by Def5; end; end; theorem Th6: for X be non empty set for Y be RealNormSpace holds BoundedFunctions(X,Y) is linearly-closed proof let X be non empty set; let Y be RealNormSpace; 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 be VECTOR of RealVectSpace(X,Y) st v in W & u in W holds v + u in W proof let v,u be VECTOR of RealVectSpace(X,Y) such that A3: v in W and A4: u in W; 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 be Real such that A5: 0 <= K2 and A6: for x be 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 be Real such that A7: 0 <= K1 and A8: for x be Element of X holds ||. u1.x .|| <= K1 by Def4; take K3=K1+K2; now let x be Element of X; ||. 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; end; hence thesis by A7,A5; end; hence thesis by Def5; end; for a be Real for v be VECTOR of RealVectSpace(X,Y) st v in W holds a * v in W proof let a be Real; let v be VECTOR of RealVectSpace(X,Y) such that A10: v in W; 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 be Real such that A11: 0 <= K and A12: for x be Element of X holds ||. v1.x .|| <= K by Def4; take abs(a)*K; A13: now let x be Element of X; 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; end; 0 <=abs(a) by COMPLEX1:46; hence thesis by A11,A13; end; hence thesis by Def5; end; hence thesis by A2,RLSUB_1:def 1; end; theorem for X be non empty set for Y be 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)) #) -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital; coherence 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 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; end; registration let X be non empty set; let Y be RealNormSpace; cluster R_VectorSpace_of_BoundedFunctions(X,Y) -> strict; coherence; end; theorem Th8: for X be non empty set for Y be RealNormSpace for f,g,h be VECTOR of R_VectorSpace_of_BoundedFunctions(X,Y) for f9,g9,h9 be bounded Function of X,the carrier of Y st f9=f & g9=g & h9=h holds (h = f+g iff for x be Element of X holds h9.x = f9.x + g9.x ) proof let X be non empty set; let Y be RealNormSpace; let f,g,h be VECTOR of R_VectorSpace_of_BoundedFunctions(X,Y); 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 such that A2: f9=f & g9=g & h9=h; A3: now assume A4: h = f+g; let x be Element of X; h1=f1+g1 by A1,A4,RLSUB_1:13; hence h9.x=f9.x+g9.x by A2,LOPBAN_1:11; end; now assume for x be Element of X holds h9.x=f9.x+g9.x; then h1=f1+g1 by A2,LOPBAN_1:11; hence h =f+g by A1,RLSUB_1:13; end; hence thesis by A3; end; theorem Th9: for X be non empty set for Y be RealNormSpace for f,h be VECTOR of R_VectorSpace_of_BoundedFunctions(X,Y) for f9,h9 be bounded Function of X, the carrier of Y st f9=f & h9=h for a be Real holds h = a*f iff for x be Element of X holds h9.x = a*f9.x proof let X be non empty set; let Y be RealNormSpace; let f,h be VECTOR of R_VectorSpace_of_BoundedFunctions(X,Y); let f9,h9 be bounded Function of X,the carrier of Y such that A1: f9=f & h9=h; let a be Real; 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 assume A4: h = a*f; let x be Element of X; h1=a*f1 by A2,A4,RLSUB_1:14; hence h9.x=a*f9.x by A1,LOPBAN_1:12; end; now assume for x be Element of X holds h9.x=a*f9.x; then h1=a*f1 by A1,LOPBAN_1:12; hence h =a*f by A2,RLSUB_1:14; end; hence thesis by A3; end; theorem Th10: for X be non empty set for Y be RealNormSpace holds 0. R_VectorSpace_of_BoundedFunctions(X,Y) =(X -->0.Y) proof let X be non empty set; let Y be RealNormSpace; 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 thesis by RLSUB_1:11; end; definition let X be non empty set; let Y be RealNormSpace; let f be set such that A1: f in BoundedFunctions(X,Y); func modetrans(f,X,Y) -> bounded Function of X,the carrier of Y equals :Def7 : f; coherence by A1,Def5; end; 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 {||.u.t.|| where t is Element of X : not contradiction }; coherence proof set x = the Element of X; A1: now let x be set; now assume x in {||.u.t.|| where t is Element of X : not contradiction }; then ex t be Element of X st x=||.u.t.||; hence x in REAL; end; hence x in {||.u.t.|| where t is Element of X : not contradiction } implies x in REAL; end; ||.u.x.|| in {||.u.t.|| where t is Element of X : not contradiction }; hence thesis by A1,TARSKI:def 3; end; end; theorem Th11: for X be non empty set for Y be RealNormSpace for g be bounded Function of X,the carrier of Y holds PreNorms(g) is bounded_above proof let X be non empty set; let Y be RealNormSpace; let g be bounded Function of X,the carrier of Y; consider K be Real such that 0 <= K and A1: for x be Element of X holds ||. g.x .|| <= K by Def4; take K; let r be ext-real number; assume r in PreNorms(g); then ex t be Element of X st r=||.g.t.||; hence r <=K by A1; end; theorem for X be non empty set for Y be RealNormSpace for g be Function of X, the carrier of Y holds g is bounded iff PreNorms(g) is bounded_above proof let X be non empty set; let Y be RealNormSpace; let g be Function of X,the carrier of Y; now reconsider K=upper_bound PreNorms(g) as Real; assume A1: PreNorms(g) is bounded_above; A2: 0 <= K proof consider r0 be set such that A3: r0 in PreNorms(g) by XBOOLE_0:def 1; reconsider r0 as Real by A3; now let r be Real; assume r in PreNorms(g); then ex t be Element of X st r=||.g.t.||; hence 0 <= r; end; then 0 <= r0 by A3; hence thesis by A1,A3,SEQ_4:def 1; end; take K; now let t be Element of X; ||.g.t.|| in PreNorms(g); hence ||.g.t.|| <= K by A1,SEQ_4:def 1; end; hence g is bounded by A2,Def4; end; hence thesis by Th11; end; definition let X be non empty set; let Y be RealNormSpace; func BoundedFunctionsNorm(X,Y) -> Function of BoundedFunctions(X,Y), REAL means :Def9: for x be set st x in BoundedFunctions(X,Y) holds it.x = upper_bound PreNorms(modetrans(x,X,Y)); existence proof deffunc F(set) = upper_bound PreNorms(modetrans($1,X,Y)); A1: for z be set st z in BoundedFunctions(X,Y) holds F(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 = F(x) from FUNCT_2:sch 2(A1); hence thesis; end; uniqueness proof let NORM1,NORM2 be Function of BoundedFunctions(X,Y), REAL such that A2: for x be set st x in BoundedFunctions(X,Y) holds NORM1.x = upper_bound PreNorms(modetrans(x,X,Y)) and A3: for x be set st x in BoundedFunctions(X,Y) holds NORM2.x = upper_bound PreNorms(modetrans(x,X,Y)); A4: for z be set st z in BoundedFunctions(X,Y) holds NORM1.z = NORM2.z proof let z be set such that A5: z in BoundedFunctions(X,Y); NORM1.z = upper_bound PreNorms(modetrans(z,X,Y)) by A2,A5; hence thesis by A3,A5; end; dom NORM1 = BoundedFunctions(X,Y) & dom NORM2 = BoundedFunctions(X,Y) by FUNCT_2:def 1; hence thesis by A4,FUNCT_1:2; end; end; theorem Th13: for X be non empty set for Y be RealNormSpace for f be bounded Function of X,the carrier of Y holds modetrans(f,X,Y)=f proof let X be non empty set; let Y be RealNormSpace; let f be bounded Function of X,the carrier of Y; f in BoundedFunctions(X,Y) by Def5; hence thesis by Def7; end; theorem Th14: for X be non empty set for Y be RealNormSpace for f be bounded Function of X,the carrier of Y holds BoundedFunctionsNorm(X,Y).f = upper_bound PreNorms (f) proof let X be non empty set; let Y be RealNormSpace; let f be bounded Function of X,the carrier of Y; 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; end; definition let X be non empty set; let Y be RealNormSpace; func R_NormSpace_of_BoundedFunctions(X,Y) -> non empty NORMSTR equals 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; end; theorem Th15: for X be non empty set for Y be RealNormSpace holds (X --> 0.Y) = 0.R_NormSpace_of_BoundedFunctions(X,Y) proof let X be non empty set; let Y be RealNormSpace; (X --> 0.Y) =0.R_VectorSpace_of_BoundedFunctions(X,Y) by Th10 .=0.R_NormSpace_of_BoundedFunctions(X,Y); hence thesis; end; theorem Th16: for X be non empty set for Y be RealNormSpace for f being Point of R_NormSpace_of_BoundedFunctions(X,Y) for g be bounded Function of X,the carrier of Y st g=f holds for t be Element of X holds ||.g.t.|| <= ||.f.|| proof let X be non empty set; let Y be RealNormSpace; let f being Point of R_NormSpace_of_BoundedFunctions(X,Y); let g be bounded Function of X,the carrier of Y such that A1: g=f; A2: PreNorms(g) is non empty bounded_above by Th11; now let t be Element of X; ||.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; end; hence thesis; end; theorem for X be non empty set for Y be RealNormSpace for f being Point of R_NormSpace_of_BoundedFunctions(X,Y) holds 0 <= ||.f.|| proof let X be non empty set; let Y be RealNormSpace; let f being Point of R_NormSpace_of_BoundedFunctions(X,Y); reconsider g=f as bounded Function of X,the carrier of Y by Def5; consider r0 be set such that A1: r0 in PreNorms(g) by XBOOLE_0:def 1; reconsider r0 as Real by A1; A2: PreNorms(g) is non empty bounded_above by Th11; now let r be Real; assume r in PreNorms(g); then ex t be Element of X st r=||.g.t.||; hence 0 <= r; end; then 0 <= r0 by A1; then 0 <=upper_bound PreNorms(g) by A2,A1,SEQ_4:def 1; hence thesis by Th14; end; theorem Th18: for X be non empty set for Y be 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; let Y be RealNormSpace; let f being Point of R_NormSpace_of_BoundedFunctions(X,Y) such that A1: f = 0.R_NormSpace_of_BoundedFunctions(X,Y); thus ||.f.|| = 0 proof reconsider g=f as bounded Function of X, the carrier of Y by Def5; set z = X --> 0.Y; reconsider z as Function of X, the carrier of Y; consider r0 be set such that A2: r0 in PreNorms(g) by XBOOLE_0:def 1; reconsider r0 as Real by A2; A3: (for s be real number st s in PreNorms(g) holds s <= 0) implies upper_bound PreNorms(g) <= 0 by SEQ_4:45; A4: PreNorms(g) is non empty bounded_above by Th11; A5: z=g by A1,Th15; A6: now let r be Real; assume r in PreNorms(g); then consider t be 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; end; then 0 <= r0 by A2; then upper_bound PreNorms(g) = 0 by A6,A4,A2,A3,SEQ_4:def 1; hence thesis by Th14; end; end; theorem Th19: for X be non empty set for Y be RealNormSpace for f,g,h be Point of R_NormSpace_of_BoundedFunctions(X,Y) for f9,g9,h9 be bounded Function of X, the carrier of Y st f9=f & g9=g & h9=h holds (h = f+g iff for x be Element of X holds h9.x = f9.x + g9.x ) proof let X be non empty set; let Y be RealNormSpace; let f,g,h be Point of R_NormSpace_of_BoundedFunctions(X,Y); 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; assume f9=f & g9=g & h9=h; hence thesis by A1,Th8; end; theorem Th20: for X be non empty set for Y be RealNormSpace for f,h be Point of R_NormSpace_of_BoundedFunctions(X,Y) for f9,h9 be bounded Function of X,the carrier of Y st f9=f & h9=h for a be Real holds h = a*f iff for x be Element of X holds h9.x = a*f9.x proof let X be non empty set; let Y be RealNormSpace; let f,h be Point of R_NormSpace_of_BoundedFunctions(X,Y); let f9,h9 be bounded Function of X,the carrier of Y such that A1: f9=f & h9=h; 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; h=a*f iff h1=a*f1; hence thesis by A1,Th9; end; theorem Th21: for X be non empty set for Y be RealNormSpace for f, g being Point of R_NormSpace_of_BoundedFunctions(X,Y) for a be Real holds ( ||.f.|| = 0 iff f = 0.R_NormSpace_of_BoundedFunctions(X,Y) ) & ||.a*f.|| = abs(a) * ||.f.|| & ||.f+g.|| <= ||.f.|| + ||.g.|| proof let X be non empty set; let Y be RealNormSpace; let f, g being Point of R_NormSpace_of_BoundedFunctions(X,Y); let a be Real; A1: now assume A2: f = 0.R_NormSpace_of_BoundedFunctions(X,Y); thus ||.f.|| = 0 proof reconsider g=f as bounded Function of X,the carrier of Y by Def5; set z = X --> 0.Y; reconsider z as Function of X, the carrier of Y; consider r0 be set such that A3: r0 in PreNorms(g) by XBOOLE_0:def 1; reconsider r0 as Real by A3; A4: (for s be real number st s in PreNorms(g) holds s <= 0) implies upper_bound PreNorms(g) <= 0 by SEQ_4:45; A5: PreNorms(g) is non empty bounded_above by Th11; A6: z=g by A2,Th15; A7: now let r be Real; assume r in PreNorms(g); then consider t be 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; end; then 0<=r0 by A3; then upper_bound PreNorms(g) = 0 by A7,A5,A3,A4,SEQ_4:def 1; hence thesis by Th14; 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 let t be Element of X; ||.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; end; A12: now let r be Real; assume r in PreNorms(h1); then ex t be Element of X st r=||.h1.t.||; hence r <= ||.f.|| + ||.g.|| by A10; end; (for s be real number st s in PreNorms(h1) holds s <= ||.f.|| + ||.g .||) implies upper_bound PreNorms(h1) <= ||.f.|| + ||.g.|| by SEQ_4:45; hence thesis by A12,Th14; 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 be 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 let t be Element of X; 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; end; A17: now let r be Real; assume r in PreNorms(h1); then ex t be Element of X st r=||.h1.t.||; hence r <= abs(a)*||.f.|| by A15; end; A18: now per cases; case A19: a <> 0; A20: now let t be Element of X; 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; end; A23: now let r be Real; assume r in PreNorms(f1); then ex t be Element of X st r=||.f1.t.||; hence r <= abs(a)"*||.a*f.|| by A20; end; A24: ( for s be 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.||; end; case A26: a=0; 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; end; end; BoundedFunctionsNorm(X,Y).(a*f) = upper_bound PreNorms(h1) by Th14; hence thesis by A17,A14,A18,XXREAL_0:1; end; now reconsider g=f as bounded Function of X,the carrier of Y by Def5; set z = X --> 0.Y; reconsider z as Function of X, the carrier of Y; assume A28: ||.f.|| = 0; now let t be Element of X; ||.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; end; then g=z by FUNCT_2:63; hence f=0.R_NormSpace_of_BoundedFunctions(X,Y) by Th15; end; hence thesis by A1,A13,A9; end; theorem Th22: for X be non empty set for Y be RealNormSpace holds R_NormSpace_of_BoundedFunctions(X,Y) is reflexive discerning RealNormSpace-like proof let X be non empty set; let Y be RealNormSpace; thus ||.0.R_NormSpace_of_BoundedFunctions(X,Y).|| = 0 by Th21; for x, y being Point of R_NormSpace_of_BoundedFunctions(X,Y) for a be Real holds ( ||.x.|| = 0 iff x = 0.R_NormSpace_of_BoundedFunctions(X,Y) ) & ||. a*x.|| = abs(a) * ||.x.|| & ||.x+y.|| <= ||.x.|| + ||.y.|| by Th21; hence thesis by NORMSP_0:def 5,NORMSP_1:def 1; end; theorem Th23: for X be non empty set for Y be RealNormSpace holds R_NormSpace_of_BoundedFunctions(X,Y) is RealNormSpace proof let X be non empty set; let Y be 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 thesis by Th22,RSSPACE3:2; end; registration let X be non empty set; let Y be RealNormSpace; cluster R_NormSpace_of_BoundedFunctions(X,Y) -> reflexive discerning RealNormSpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable; coherence by Th23; end; theorem Th24: for X be non empty set for Y be RealNormSpace for f,g,h be Point of R_NormSpace_of_BoundedFunctions(X,Y) for f9,g9,h9 be bounded Function of X, the carrier of Y st f9=f & g9=g & h9=h holds (h = f-g iff for x be Element of X holds h9.x = f9.x - g9.x ) proof let X be non empty set; let Y be RealNormSpace; let f,g,h be Point of R_NormSpace_of_BoundedFunctions(X,Y); let f9,g9,h9 be bounded Function of X,the carrier of Y such that A1: f9=f & g9=g & h9=h; A2: now assume A3: for x be Element of X holds h9.x = f9.x - g9.x; now let x be Element of 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; 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; end; now assume h=f-g; 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 let x be Element of 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; end; hence for x be Element of X holds h9.x = f9.x - g9.x; end; hence thesis by A2; end; Lm7: for e be Real, seq be Real_Sequence st ( seq is convergent & ex k be Element of NAT st for i be Element of NAT st k <= i holds seq.i <=e ) holds lim seq <=e proof let e be Real; let seq be Real_Sequence such that A1: seq is convergent and A2: ex k be Element of NAT st for i be Element of NAT st k <= i holds seq.i <=e; consider k be Element of NAT such that A3: for i be 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 let i be Element of NAT; (seq ^\k).i = seq.(k+i) & seq.(k+i) <=e by A3,NAT_1:11,def 3; hence (seq ^\k) .i <= cseq.i by FUNCOP_1:7; end; lim (seq ^\k)=lim seq by A1,SEQ_4:20; hence thesis by A1,A5,A4,SEQ_2:18; end; theorem Th25: for X be non empty set for Y be RealNormSpace st Y is complete for seq be 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; let Y be RealNormSpace such that A1: Y is complete; let vseq be sequence of R_NormSpace_of_BoundedFunctions(X,Y) such that A2: vseq is Cauchy_sequence_by_Norm; defpred P[set, set] means ex xseq be sequence of Y st (for n be Element of NAT holds xseq.n=modetrans((vseq.n),X,Y).$1) & xseq is convergent & $2= lim xseq; A3: for x be Element of X ex y be Element of Y st P[x,y] proof let x be Element of X; deffunc F(Element of NAT) = modetrans((vseq.$1),X,Y).x; consider xseq be sequence of Y such that A4: for n be Element of NAT holds xseq.n = F(n) from FUNCT_2:sch 4; take lim xseq; A5: for m,k be Element of NAT holds ||.xseq.m-xseq.k.|| <= ||.vseq.m - vseq.k.|| proof let m,k be Element of NAT; 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 thesis by Th16; end; now let e be Real such that A8: e > 0; thus ex k be Element of NAT st for n, m be Element of NAT st n >= k & m >= k holds ||.xseq.n -xseq.m.|| < e proof consider k be Element of NAT such that A9: for n, m be Element of NAT st n >= k & m >= k holds ||.(vseq. n) - (vseq.m).|| < e by A2,A8,RSSPACE3:8; take k; thus for n, m be Element of NAT st n >= k & m >= k holds ||.xseq.n- xseq.m.|| < e proof let n,m be Element of NAT; assume n >=k & m >= k; then A10: ||.(vseq.n) - (vseq.m).|| < e by A9; ||.xseq.n-xseq.m.|| <= ||.(vseq.n) - (vseq.m).|| by A5; hence thesis by A10,XXREAL_0:2; end; end; end; then xseq is Cauchy_sequence_by_Norm by RSSPACE3:8; then xseq is convergent by A1,LOPBAN_1:def 15; hence thesis by A4; end; consider f be Function of X,the carrier of Y such that A11: for x be Element of X holds P[x,f.x] from FUNCT_2:sch 3(A3); reconsider tseq=f as Function of X,the carrier of Y; now let e1 be real number such that A12: e1 >0; reconsider e =e1 as Real by XREAL_0:def 1; consider k be Element of NAT such that A13: for n, m be Element of NAT st n >= k & m >= k holds ||.(vseq.n) - (vseq.m).|| < e by A2,A12,RSSPACE3:8; take k; now let m be Element of NAT; assume m >= k; then A14: ||.vseq.m.||= ||.vseq.||.m & ||.(vseq.m) - (vseq.k).|| = k holds abs(||.vseq.||.m - ||.vseq.|| .k ) < e1; end; then A15: ||.vseq.|| is convergent by SEQ_4:41; A16: tseq is bounded proof take lim (||.vseq.|| ); A17: now let x be Element of X; consider xseq be sequence of Y such that A18: for n be 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 be Element of NAT holds ||.xseq.m.|| <= ||.vseq.m.|| proof let m be Element of NAT; vseq.m is bounded Function of X,the carrier of Y & xseq.m = modetrans((vseq.m ),X,Y).x by A18,Def5; hence thesis by Th13,Th16; end; A21: for n be Element of NAT holds ||.xseq.||.n <=(||.vseq.||).n proof let n be Element of NAT; ||.xseq.||.n = ||.(xseq.n).|| & ||.(xseq.n).|| <= ||.vseq.n.|| by A20, NORMSP_0:def 4; hence thesis by NORMSP_0:def 4; end; ||.xseq.|| is convergent & ||.tseq.x.|| = lim ||.xseq.|| by A19, LOPBAN_1:41; hence ||.tseq.x.|| <= lim (||.vseq.|| ) by A15,A21,SEQ_2:18; end; now let n be Element of NAT; ||.vseq.n.|| >=0; hence ||.vseq.||.n >=0 by NORMSP_0:def 4; end; hence thesis by A15,A17,SEQ_2:17; end; A22: for e be Real st e > 0 ex k be Element of NAT st for n be Element of NAT st n >= k holds for x be Element of X holds ||.modetrans((vseq.n),X,Y).x - tseq.x.|| <= e proof let e be Real; assume e > 0; then consider k be Element of NAT such that A23: for n, m be Element of NAT st n >= k & m >= k holds ||.(vseq.n) - (vseq.m).|| < e by A2,RSSPACE3:8; take k; now let n be Element of NAT such that A24: n >= k; now let x be Element of X; consider xseq be sequence of Y such that A25: for n be 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 be Element of NAT holds ||.xseq.m-xseq.k.|| <= ||.vseq.m - vseq.k.|| proof let m,k be Element of NAT; 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 thesis by Th16; end; A30: for m be Element of NAT st m >=k holds ||.xseq.n-xseq.m.|| <= e proof let m be Element of NAT; assume m >=k; then A31: ||.vseq.n - vseq.m.|| = k holds rseq.m <= e proof let m be Element of NAT such that A36: m >=k; rseq.m = ||.xseq.m-xseq.n.|| by A32 .= ||.xseq.n-xseq.m.|| by NORMSP_1:7; hence thesis by A30,A36; end; then lim rseq <= e by A34,A33,Lm7,LOPBAN_1:20; hence thesis by A35,NORMSP_1:7; end; hence ||.modetrans((vseq.n),X,Y).x - tseq.x.|| <= e by A25; end; hence for x be Element of X holds ||.modetrans((vseq.n),X,Y).x - tseq.x .|| <= e; end; hence thesis; end; reconsider 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 be Real st e > 0 ex k be Element of NAT st for n be Element of NAT st n >= k holds ||.vseq.n - tv.|| <= e proof let e be Real; assume e > 0; then consider k be Element of NAT such that A38: for n be Element of NAT st n >= k holds for x be Element of X holds ||.modetrans((vseq.n),X,Y).x - tseq.x.|| <= e by A22; now set g1=tseq; let n be Element of NAT such that A39: n >= k; 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 let t be Element of X; 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.||= ||.f1.t-g1.t.|| by Th24; hence ||.h1.t.|| <=e by A38,A39; end; A41: now let r be Real; assume r in PreNorms(h1); then ex t be Element of X st r=||.h1.t.||; hence r <=e by A40; end; (for s be 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; end; hence thesis; end; for e be Real st e > 0 ex m be Element of NAT st for n be Element of NAT st n >= m holds ||.(vseq.n) - tv.|| < e proof let e be Real such that A42: e > 0; consider m be Element of NAT such that A43: for n be Element of NAT st n >= m holds ||.(vseq.n) - tv.|| <= e/ 2 by A37,A42,XREAL_1:215; A44: e/2= m; then ||.(vseq.n) - tv.|| <= e/2 by A43; hence ||.(vseq.n) - tv.|| < e by A44,XXREAL_0:2; end; hence thesis; end; hence thesis by NORMSP_1:def 6; end; theorem Th26: for X be non empty set for Y be RealBanachSpace holds R_NormSpace_of_BoundedFunctions(X,Y) is RealBanachSpace proof let X be non empty set; let Y be RealBanachSpace; for seq be sequence of R_NormSpace_of_BoundedFunctions(X,Y) st seq is Cauchy_sequence_by_Norm holds seq is convergent by Th25; hence thesis by LOPBAN_1:def 15; end; registration let X be non empty set; let Y be RealBanachSpace; cluster R_NormSpace_of_BoundedFunctions (X,Y) -> complete; coherence by Th26; end;