:: CSSPACE4 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_BoundedComplexSequences -> Subset of Linear_Space_of_ComplexSequences means :Def1: :: CSSPACE4:def 1 for x being set holds ( x in it iff ( x in the_set_of_ComplexSequences & seq_id x is bounded ) ); existence ex b1 being Subset of Linear_Space_of_ComplexSequences st for x being set holds ( x in b1 iff ( x in the_set_of_ComplexSequences & 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_ComplexSequences & S1[x] ) ) from XBOOLE_0:sch_1(); for x being set st x in IT holds x in the_set_of_ComplexSequences by A1; then IT is Subset of the_set_of_ComplexSequences by TARSKI:def_3; hence ex b1 being Subset of Linear_Space_of_ComplexSequences st for x being set holds ( x in b1 iff ( x in the_set_of_ComplexSequences & seq_id x is bounded ) ) by A1, CSSPACE:def_7; ::_thesis: verum end; uniqueness for b1, b2 being Subset of Linear_Space_of_ComplexSequences st ( for x being set holds ( x in b1 iff ( x in the_set_of_ComplexSequences & seq_id x is bounded ) ) ) & ( for x being set holds ( x in b2 iff ( x in the_set_of_ComplexSequences & seq_id x is bounded ) ) ) holds b1 = b2 proof let X1, X2 be Subset of Linear_Space_of_ComplexSequences; ::_thesis: ( ( for x being set holds ( x in X1 iff ( x in the_set_of_ComplexSequences & seq_id x is bounded ) ) ) & ( for x being set holds ( x in X2 iff ( x in the_set_of_ComplexSequences & 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_ComplexSequences & seq_id x is bounded ) ) and A3: for x being set holds ( x in X2 iff ( x in the_set_of_ComplexSequences & 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_ComplexSequences & 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_ComplexSequences & seq_id x is bounded ) by A3; hence x in X1 by A2; ::_thesis: verum end; end; :: deftheorem Def1 defines the_set_of_BoundedComplexSequences CSSPACE4:def_1_:_ for b1 being Subset of Linear_Space_of_ComplexSequences holds ( b1 = the_set_of_BoundedComplexSequences iff for x being set holds ( x in b1 iff ( x in the_set_of_ComplexSequences & seq_id x is bounded ) ) ); Lm3: for seq1, seq2 being Complex_Sequence st seq1 is bounded & seq2 is bounded holds seq1 + seq2 is bounded proof let seq1, seq2 be Complex_Sequence; ::_thesis: ( seq1 is bounded & seq2 is bounded implies seq1 + seq2 is bounded ) assume that A1: seq1 is bounded and A2: seq2 is bounded ; ::_thesis: seq1 + seq2 is bounded consider r2 being Real such that 0 < r2 and A3: for n being Element of NAT holds |.(seq2 . n).| < r2 by A2, COMSEQ_2:8; consider r1 being Real such that 0 < r1 and A4: for n being Element of NAT holds |.(seq1 . n).| < r1 by A1, COMSEQ_2:8; for n being Element of NAT holds |.((seq1 + seq2) . n).| < r1 + r2 proof let n be Element of NAT ; ::_thesis: |.((seq1 + seq2) . n).| < r1 + r2 |.((seq1 + seq2) . n).| = |.((seq1 . n) + (seq2 . n)).| by VALUED_1:1; then A5: |.((seq1 + seq2) . n).| <= |.(seq1 . n).| + |.(seq2 . n).| by COMPLEX1:56; |.(seq1 . n).| < r1 by A4; then |.(seq1 . n).| + |.(seq2 . n).| < r1 + r2 by A3, XREAL_1:8; hence |.((seq1 + seq2) . n).| < r1 + r2 by A5, XXREAL_0:2; ::_thesis: verum end; hence seq1 + seq2 is bounded by COMSEQ_2:def_4; ::_thesis: verum end; Lm4: for c being Complex for seq being Complex_Sequence st seq is bounded holds c (#) seq is bounded proof let c be Complex; ::_thesis: for seq being Complex_Sequence st seq is bounded holds c (#) seq is bounded let seq be Complex_Sequence; ::_thesis: ( seq is bounded implies c (#) seq is bounded ) assume seq is bounded ; ::_thesis: c (#) seq is bounded then consider r being Real such that 0 < r and A1: for n being Element of NAT holds |.(seq . n).| < r by COMSEQ_2:8; ex r1 being Real st for n being Element of NAT holds |.((c (#) seq) . n).| < r1 proof now__::_thesis:_(_(_c_=_0c_&_ex_r1_being_Element_of_NAT_ex_r1_being_Real_st_ for_n_being_Element_of_NAT_holds_|.((c_(#)_seq)_._n).|_<_r1_)_or_(_c_<>_0c_&_ex_r1_being_Element_of_REAL_ex_r1_being_Real_st_ for_n_being_Element_of_NAT_holds_|.((c_(#)_seq)_._n).|_<_r1_)_) percases ( c = 0c or c <> 0c ) ; caseA2: c = 0c ; ::_thesis: ex r1 being Element of NAT ex r1 being Real st for n being Element of NAT holds |.((c (#) seq) . n).| < r1 take r1 = 1; ::_thesis: ex r1 being Real st for n being Element of NAT holds |.((c (#) seq) . n).| < r1 for n being Element of NAT holds |.((c (#) seq) . n).| < 1 proof let n be Element of NAT ; ::_thesis: |.((c (#) seq) . n).| < 1 (c (#) seq) . n = c * (seq . n) by VALUED_1:6 .= 0 by A2 ; hence |.((c (#) seq) . n).| < 1 by COMPLEX1:44; ::_thesis: verum end; hence ex r1 being Real st for n being Element of NAT holds |.((c (#) seq) . n).| < r1 ; ::_thesis: verum end; caseA3: c <> 0c ; ::_thesis: ex r1 being Element of REAL ex r1 being Real st for n being Element of NAT holds |.((c (#) seq) . n).| < r1 take r1 = |.c.| * r; ::_thesis: ex r1 being Real st for n being Element of NAT holds |.((c (#) seq) . n).| < r1 for n being Element of NAT holds |.((c (#) seq) . n).| < |.c.| * r proof let n be Element of NAT ; ::_thesis: |.((c (#) seq) . n).| < |.c.| * r A4: |.((c (#) seq) . n).| = |.(c * (seq . n)).| by VALUED_1:6 .= |.c.| * |.(seq . n).| by COMPLEX1:65 ; |.c.| > 0 by A3, COMPLEX1:47; hence |.((c (#) seq) . n).| < |.c.| * r by A1, A4, XREAL_1:68; ::_thesis: verum end; hence ex r1 being Real st for n being Element of NAT holds |.((c (#) seq) . n).| < r1 ; ::_thesis: verum end; end; end; hence ex r1 being Real st for n being Element of NAT holds |.((c (#) seq) . n).| < r1 ; ::_thesis: verum end; hence c (#) seq is bounded by COMSEQ_2:def_4; ::_thesis: verum end; registration cluster the_set_of_BoundedComplexSequences -> non empty ; coherence not the_set_of_BoundedComplexSequences is empty proof seq_id CZeroseq is bounded proof reconsider seq = seq_id CZeroseq as Complex_Sequence ; for n being Element of NAT holds |.(seq . n).| < 1 by COMPLEX1:44, CSSPACE:def_6; hence seq_id CZeroseq is bounded by COMSEQ_2:8; ::_thesis: verum end; hence not the_set_of_BoundedComplexSequences is empty by Def1; ::_thesis: verum end; cluster the_set_of_BoundedComplexSequences -> linearly-closed ; coherence the_set_of_BoundedComplexSequences is linearly-closed proof set W = the_set_of_BoundedComplexSequences ; A1: for c being Complex for v being VECTOR of Linear_Space_of_ComplexSequences st v in the_set_of_BoundedComplexSequences holds c * v in the_set_of_BoundedComplexSequences proof let c be Complex; ::_thesis: for v being VECTOR of Linear_Space_of_ComplexSequences st v in the_set_of_BoundedComplexSequences holds c * v in the_set_of_BoundedComplexSequences let v be VECTOR of Linear_Space_of_ComplexSequences; ::_thesis: ( v in the_set_of_BoundedComplexSequences implies c * v in the_set_of_BoundedComplexSequences ) assume v in the_set_of_BoundedComplexSequences ; ::_thesis: c * v in the_set_of_BoundedComplexSequences then A2: seq_id v is bounded by Def1; seq_id (c * v) = seq_id (c (#) (seq_id v)) by CSSPACE:3, CSSPACE:def_7 .= c (#) (seq_id v) by CSSPACE:1 ; then seq_id (c * v) is bounded by A2, Lm4; hence c * v in the_set_of_BoundedComplexSequences by Def1, CSSPACE:def_7; ::_thesis: verum end; for v, u being VECTOR of Linear_Space_of_ComplexSequences st v in the_set_of_BoundedComplexSequences & u in the_set_of_BoundedComplexSequences holds v + u in the_set_of_BoundedComplexSequences proof let v, u be VECTOR of Linear_Space_of_ComplexSequences; ::_thesis: ( v in the_set_of_BoundedComplexSequences & u in the_set_of_BoundedComplexSequences implies v + u in the_set_of_BoundedComplexSequences ) assume ( v in the_set_of_BoundedComplexSequences & u in the_set_of_BoundedComplexSequences ) ; ::_thesis: v + u in the_set_of_BoundedComplexSequences 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 CSSPACE:2, CSSPACE:def_7 .= (seq_id v) + (seq_id u) by CSSPACE:1 ; then seq_id (v + u) is bounded by A3, Lm3; hence v + u in the_set_of_BoundedComplexSequences by Def1, CSSPACE:def_7; ::_thesis: verum end; hence the_set_of_BoundedComplexSequences is linearly-closed by A1, CLVECT_1:def_7; ::_thesis: verum end; end; Lm5: CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is Subspace of Linear_Space_of_ComplexSequences by CSSPACE:11; registration cluster CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ; coherence ( CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is Abelian & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is add-associative & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is right_zeroed & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is right_complementable & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is vector-distributive & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is scalar-distributive & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is scalar-associative & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is scalar-unital ) by CSSPACE:11; end; Lm6: ( CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is Abelian & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is add-associative & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is right_zeroed & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is right_complementable & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is vector-distributive & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is scalar-distributive & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is scalar-associative & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is scalar-unital ) ; definition func Complex_linfty_norm -> Function of the_set_of_BoundedComplexSequences,REAL means :Def2: :: CSSPACE4:def 2 for x being set st x in the_set_of_BoundedComplexSequences holds it . x = upper_bound (rng |.(seq_id x).|); existence ex b1 being Function of the_set_of_BoundedComplexSequences,REAL st for x being set st x in the_set_of_BoundedComplexSequences holds b1 . x = upper_bound (rng |.(seq_id x).|) proof deffunc H1( set ) -> Element of REAL = upper_bound (rng |.(seq_id $1).|); A1: for z being set st z in the_set_of_BoundedComplexSequences holds H1(z) in REAL ; ex f being Function of the_set_of_BoundedComplexSequences,REAL st for x being set st x in the_set_of_BoundedComplexSequences holds f . x = H1(x) from FUNCT_2:sch_2(A1); hence ex b1 being Function of the_set_of_BoundedComplexSequences,REAL st for x being set st x in the_set_of_BoundedComplexSequences holds b1 . x = upper_bound (rng |.(seq_id x).|) ; ::_thesis: verum end; uniqueness for b1, b2 being Function of the_set_of_BoundedComplexSequences,REAL st ( for x being set st x in the_set_of_BoundedComplexSequences holds b1 . x = upper_bound (rng |.(seq_id x).|) ) & ( for x being set st x in the_set_of_BoundedComplexSequences holds b2 . x = upper_bound (rng |.(seq_id x).|) ) holds b1 = b2 proof let NORM1, NORM2 be Function of the_set_of_BoundedComplexSequences,REAL; ::_thesis: ( ( for x being set st x in the_set_of_BoundedComplexSequences holds NORM1 . x = upper_bound (rng |.(seq_id x).|) ) & ( for x being set st x in the_set_of_BoundedComplexSequences holds NORM2 . x = upper_bound (rng |.(seq_id x).|) ) implies NORM1 = NORM2 ) assume that A2: for x being set st x in the_set_of_BoundedComplexSequences holds NORM1 . x = upper_bound (rng |.(seq_id x).|) and A3: for x being set st x in the_set_of_BoundedComplexSequences holds NORM2 . x = upper_bound (rng |.(seq_id x).|) ; ::_thesis: NORM1 = NORM2 A4: for z being set st z in the_set_of_BoundedComplexSequences holds NORM1 . z = NORM2 . z proof let z be set ; ::_thesis: ( z in the_set_of_BoundedComplexSequences implies NORM1 . z = NORM2 . z ) assume A5: z in the_set_of_BoundedComplexSequences ; ::_thesis: NORM1 . z = NORM2 . z NORM1 . z = upper_bound (rng |.(seq_id z).|) by A2, A5; hence NORM1 . z = NORM2 . z by A3, A5; ::_thesis: verum end; ( dom NORM1 = the_set_of_BoundedComplexSequences & dom NORM2 = the_set_of_BoundedComplexSequences ) by FUNCT_2:def_1; hence NORM1 = NORM2 by A4, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def2 defines Complex_linfty_norm CSSPACE4:def_2_:_ for b1 being Function of the_set_of_BoundedComplexSequences,REAL holds ( b1 = Complex_linfty_norm iff for x being set st x in the_set_of_BoundedComplexSequences holds b1 . x = upper_bound (rng |.(seq_id x).|) ); Lm7: for seq being Complex_Sequence st ( for n being Element of NAT holds seq . n = 0c ) holds ( seq is bounded & upper_bound (rng |.seq.|) = 0 ) proof let seq be Complex_Sequence; ::_thesis: ( ( for n being Element of NAT holds seq . n = 0c ) implies ( seq is bounded & upper_bound (rng |.seq.|) = 0 ) ) assume A1: for n being Element of NAT holds seq . n = 0c ; ::_thesis: ( seq is bounded & upper_bound (rng |.seq.|) = 0 ) for n being Element of NAT holds |.(seq . n).| < 1 by A1, COMPLEX1:44; hence seq is bounded by COMSEQ_2:def_4; ::_thesis: upper_bound (rng |.seq.|) = 0 rng |.seq.| c= {0} proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng |.seq.| or y in {0} ) assume y in rng |.seq.| ; ::_thesis: y in {0} then consider n being set such that A2: n in NAT and A3: |.seq.| . n = y by FUNCT_2:11; reconsider n = n as Element of NAT by A2; |.seq.| . n = |.(seq . n).| by VALUED_1:18 .= |.0c.| by A1 ; hence y in {0} by A3, COMPLEX1:44, TARSKI:def_1; ::_thesis: verum end; then rng |.seq.| = {0} by ZFMISC_1:33; hence upper_bound (rng |.seq.|) = 0 by SEQ_4:9; ::_thesis: verum end; Lm8: for seq being Complex_Sequence st seq is bounded holds |.seq.| is bounded proof let seq be Complex_Sequence; ::_thesis: ( seq is bounded implies |.seq.| is bounded ) A1: 0 <= |.(seq . 0).| by COMPLEX1:46; assume seq is bounded ; ::_thesis: |.seq.| is bounded then consider r being Real such that A2: for n being Element of NAT holds |.(seq . n).| < r by COMSEQ_2:def_4; A3: for n being Element of NAT holds abs (|.seq.| . n) < r proof let n be Element of NAT ; ::_thesis: abs (|.seq.| . n) < r |.seq.| . n = |.(seq . n).| by VALUED_1:18; hence abs (|.seq.| . n) < r by A2; ::_thesis: verum end; |.(seq . 0).| < r by A2; hence |.seq.| is bounded by A1, A3, SEQ_2:3; ::_thesis: verum end; Lm9: for seq being Complex_Sequence st |.seq.| is bounded holds seq is bounded proof let seq be Complex_Sequence; ::_thesis: ( |.seq.| is bounded implies seq is bounded ) assume |.seq.| is bounded ; ::_thesis: seq is bounded then consider r being real number such that 0 < r and A1: for n being Element of NAT holds abs (|.seq.| . n) < r by SEQ_2:3; reconsider r = r as Real by XREAL_0:def_1; for n being Element of NAT holds |.(seq . n).| < r proof let n be Element of NAT ; ::_thesis: |.(seq . n).| < r |.seq.| . n = |.(seq . n).| by VALUED_1:18; then abs (|.seq.| . n) = |.(seq . n).| ; hence |.(seq . n).| < r by A1; ::_thesis: verum end; hence seq is bounded by COMSEQ_2:def_4; ::_thesis: verum end; Lm10: for seq being Complex_Sequence st seq is bounded & upper_bound (rng |.seq.|) = 0 holds for n being Element of NAT holds seq . n = 0c proof let seq be Complex_Sequence; ::_thesis: ( seq is bounded & upper_bound (rng |.seq.|) = 0 implies for n being Element of NAT holds seq . n = 0c ) assume that A1: seq is bounded and A2: upper_bound (rng |.seq.|) = 0 ; ::_thesis: for n being Element of NAT holds seq . n = 0c let n be Element of NAT ; ::_thesis: seq . n = 0c 0 <= |.(seq . n).| by COMPLEX1:46; then A3: 0 <= |.seq.| . n by VALUED_1:18; |.seq.| is bounded by A1, Lm8; then |.seq.| . n = 0 by A2, A3, Lm2; then |.(seq . n).| = 0 by VALUED_1:18; hence seq . n = 0c by COMPLEX1:45; ::_thesis: verum end; theorem :: CSSPACE4:1 for seq being Complex_Sequence holds ( ( seq is bounded & upper_bound (rng |.seq.|) = 0 ) iff for n being Element of NAT holds seq . n = 0c ) by Lm7, Lm10; registration cluster CNORMSTR(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),Complex_linfty_norm #) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ; coherence ( CNORMSTR(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),Complex_linfty_norm #) is Abelian & CNORMSTR(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),Complex_linfty_norm #) is add-associative & CNORMSTR(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),Complex_linfty_norm #) is right_zeroed & CNORMSTR(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),Complex_linfty_norm #) is right_complementable & CNORMSTR(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),Complex_linfty_norm #) is vector-distributive & CNORMSTR(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),Complex_linfty_norm #) is scalar-distributive & CNORMSTR(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),Complex_linfty_norm #) is scalar-associative & CNORMSTR(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),Complex_linfty_norm #) is scalar-unital ) by Lm6, CSSPACE3:2; end; definition func Complex_linfty_Space -> non empty CNORMSTR equals :: CSSPACE4:def 3 CNORMSTR(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),Complex_linfty_norm #); coherence CNORMSTR(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),Complex_linfty_norm #) is non empty CNORMSTR ; end; :: deftheorem defines Complex_linfty_Space CSSPACE4:def_3_:_ Complex_linfty_Space = CNORMSTR(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),Complex_linfty_norm #); theorem Th2: :: CSSPACE4:2 ( the carrier of Complex_linfty_Space = the_set_of_BoundedComplexSequences & ( for x being set holds ( x is VECTOR of Complex_linfty_Space iff ( x is Complex_Sequence & seq_id x is bounded ) ) ) & 0. Complex_linfty_Space = CZeroseq & ( for u being VECTOR of Complex_linfty_Space holds u = seq_id u ) & ( for u, v being VECTOR of Complex_linfty_Space holds u + v = (seq_id u) + (seq_id v) ) & ( for c being Complex for u being VECTOR of Complex_linfty_Space holds c * u = c (#) (seq_id u) ) & ( for u being VECTOR of Complex_linfty_Space holds ( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) ) & ( for u, v being VECTOR of Complex_linfty_Space holds u - v = (seq_id u) - (seq_id v) ) & ( for v being VECTOR of Complex_linfty_Space holds seq_id v is bounded ) & ( for v being VECTOR of Complex_linfty_Space holds ||.v.|| = upper_bound (rng |.(seq_id v).|) ) ) proof set l1 = Complex_linfty_Space ; A1: for x being set holds ( x is Element of Complex_linfty_Space iff ( x is Complex_Sequence & seq_id x is bounded ) ) proof let x be set ; ::_thesis: ( x is Element of Complex_linfty_Space iff ( x is Complex_Sequence & seq_id x is bounded ) ) ( x in the_set_of_ComplexSequences iff x is Complex_Sequence ) by CSSPACE:def_1; hence ( x is Element of Complex_linfty_Space iff ( x is Complex_Sequence & seq_id x is bounded ) ) by Def1; ::_thesis: verum end; A2: for u, v being VECTOR of Complex_linfty_Space holds u + v = (seq_id u) + (seq_id v) proof let u, v be VECTOR of Complex_linfty_Space; ::_thesis: u + v = (seq_id u) + (seq_id v) reconsider u1 = u, v1 = v as VECTOR of Linear_Space_of_ComplexSequences by Lm5, CLVECT_1:29; set L1 = Linear_Space_of_ComplexSequences ; set W = the_set_of_BoundedComplexSequences ; dom the addF of Linear_Space_of_ComplexSequences = [: the carrier of Linear_Space_of_ComplexSequences, the carrier of Linear_Space_of_ComplexSequences:] by FUNCT_2:def_1; then A3: dom ( the addF of Linear_Space_of_ComplexSequences || the_set_of_BoundedComplexSequences) = [:the_set_of_BoundedComplexSequences,the_set_of_BoundedComplexSequences:] by RELAT_1:62; u + v = ( the addF of Linear_Space_of_ComplexSequences || the_set_of_BoundedComplexSequences) . [u,v] by CSSPACE:def_8 .= u1 + v1 by A3, FUNCT_1:47 ; hence u + v = (seq_id u) + (seq_id v) by CSSPACE:2, CSSPACE:def_7; ::_thesis: verum end; A4: for c being Complex for u being VECTOR of Complex_linfty_Space holds c * u = c (#) (seq_id u) proof let c be Complex; ::_thesis: for u being VECTOR of Complex_linfty_Space holds c * u = c (#) (seq_id u) let u be VECTOR of Complex_linfty_Space; ::_thesis: c * u = c (#) (seq_id u) reconsider u1 = u as VECTOR of Linear_Space_of_ComplexSequences by Lm5, CLVECT_1:29; set L1 = Linear_Space_of_ComplexSequences ; set W = the_set_of_BoundedComplexSequences ; reconsider c = c as Element of COMPLEX by XCMPLX_0:def_2; dom the Mult of Linear_Space_of_ComplexSequences = [:COMPLEX, the carrier of Linear_Space_of_ComplexSequences:] by FUNCT_2:def_1; then A5: dom ( the Mult of Linear_Space_of_ComplexSequences | [:COMPLEX,the_set_of_BoundedComplexSequences:]) = [:COMPLEX,the_set_of_BoundedComplexSequences:] by RELAT_1:62, ZFMISC_1:96; c * u = the Mult of Complex_linfty_Space . [c,u] by CLVECT_1:def_1 .= ( the Mult of Linear_Space_of_ComplexSequences | [:COMPLEX,the_set_of_BoundedComplexSequences:]) . [c,u] by CSSPACE:def_9 .= the Mult of Linear_Space_of_ComplexSequences . [c,u] by A5, FUNCT_1:47 .= c * u1 by CLVECT_1:def_1 ; hence c * u = c (#) (seq_id u) by CSSPACE:3, CSSPACE:def_7; ::_thesis: verum end; A6: for u being VECTOR of Complex_linfty_Space holds u = seq_id u proof let u be VECTOR of Complex_linfty_Space; ::_thesis: u = seq_id u u is VECTOR of Linear_Space_of_ComplexSequences by Lm5, CLVECT_1:29; hence u = seq_id u by CSSPACE:def_2, CSSPACE:def_7; ::_thesis: verum end; A7: for u being VECTOR of Complex_linfty_Space holds ( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) proof let u be VECTOR of Complex_linfty_Space; ::_thesis: ( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) - u = (- 1r) * u by CLVECT_1:3 .= (- 1r) (#) (seq_id u) by A4 .= - (seq_id u) by COMSEQ_1:11 ; hence ( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) by A6; ::_thesis: verum end; A8: for u, v being VECTOR of Complex_linfty_Space holds u - v = (seq_id u) - (seq_id v) proof let u, v be VECTOR of Complex_linfty_Space; ::_thesis: u - v = (seq_id u) - (seq_id v) thus u - v = (seq_id u) + (seq_id (- v)) by A2 .= (seq_id u) - (seq_id v) by A7 ; ::_thesis: verum end; A9: for v being VECTOR of Complex_linfty_Space holds ||.v.|| = upper_bound (rng |.(seq_id v).|) by Def2; 0. Complex_linfty_Space = 0. Linear_Space_of_ComplexSequences by CSSPACE:def_10 .= CZeroseq by CSSPACE:def_7 ; hence ( the carrier of Complex_linfty_Space = the_set_of_BoundedComplexSequences & ( for x being set holds ( x is VECTOR of Complex_linfty_Space iff ( x is Complex_Sequence & seq_id x is bounded ) ) ) & 0. Complex_linfty_Space = CZeroseq & ( for u being VECTOR of Complex_linfty_Space holds u = seq_id u ) & ( for u, v being VECTOR of Complex_linfty_Space holds u + v = (seq_id u) + (seq_id v) ) & ( for c being Complex for u being VECTOR of Complex_linfty_Space holds c * u = c (#) (seq_id u) ) & ( for u being VECTOR of Complex_linfty_Space holds ( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) ) & ( for u, v being VECTOR of Complex_linfty_Space holds u - v = (seq_id u) - (seq_id v) ) & ( for v being VECTOR of Complex_linfty_Space holds seq_id v is bounded ) & ( for v being VECTOR of Complex_linfty_Space holds ||.v.|| = upper_bound (rng |.(seq_id v).|) ) ) by A1, A6, A2, A4, A7, A8, A9; ::_thesis: verum end; theorem Th3: :: CSSPACE4:3 for x, y being Point of Complex_linfty_Space for c being Complex holds ( ( ||.x.|| = 0 implies x = 0. Complex_linfty_Space ) & ( x = 0. Complex_linfty_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(c * x).|| = |.c.| * ||.x.|| ) proof let x, y be Point of Complex_linfty_Space; ::_thesis: for c being Complex holds ( ( ||.x.|| = 0 implies x = 0. Complex_linfty_Space ) & ( x = 0. Complex_linfty_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(c * x).|| = |.c.| * ||.x.|| ) let c be Complex; ::_thesis: ( ( ||.x.|| = 0 implies x = 0. Complex_linfty_Space ) & ( x = 0. Complex_linfty_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(c * x).|| = |.c.| * ||.x.|| ) A1: for n being Element of NAT holds |.(c (#) (seq_id x)).| . n = |.c.| * (|.(seq_id x).| . n) proof let n be Element of NAT ; ::_thesis: |.(c (#) (seq_id x)).| . n = |.c.| * (|.(seq_id x).| . n) |.(c (#) (seq_id x)).| . n = |.((c (#) (seq_id x)) . n).| by VALUED_1:18 .= |.(c * ((seq_id x) . n)).| by VALUED_1:6 .= |.c.| * |.((seq_id x) . n).| by COMPLEX1:65 .= |.c.| * (|.(seq_id x).| . n) by VALUED_1:18 ; hence |.(c (#) (seq_id x)).| . n = |.c.| * (|.(seq_id x).| . n) ; ::_thesis: verum end; |.(seq_id x).| . 1 = |.((seq_id x) . 1).| by VALUED_1:18; then A2: 0 <= |.(seq_id x).| . 1 by COMPLEX1:46; A3: for n being Element of NAT holds |.(seq_id (x + y)).| . n = |.(((seq_id x) . n) + ((seq_id y) . n)).| proof let n be Element of NAT ; ::_thesis: |.(seq_id (x + y)).| . n = |.(((seq_id x) . n) + ((seq_id y) . n)).| |.(seq_id (x + y)).| . n = |.(seq_id ((seq_id x) + (seq_id y))).| . n by Th2 .= |.((seq_id x) + (seq_id y)).| . n by CSSPACE:1 .= |.(((seq_id x) + (seq_id y)) . n).| by VALUED_1:18 .= |.(((seq_id x) . n) + ((seq_id y) . n)).| by VALUED_1:1 ; hence |.(seq_id (x + y)).| . n = |.(((seq_id x) . n) + ((seq_id y) . n)).| ; ::_thesis: verum end; A4: for n being Element of NAT holds |.(seq_id (x + y)).| . n <= (|.(seq_id x).| . n) + (|.(seq_id y).| . n) proof let n be Element of NAT ; ::_thesis: |.(seq_id (x + y)).| . n <= (|.(seq_id x).| . n) + (|.(seq_id y).| . n) |.(((seq_id x) . n) + ((seq_id y) . n)).| <= |.((seq_id x) . n).| + |.((seq_id y) . n).| by COMPLEX1:56; then |.(seq_id (x + y)).| . n <= |.((seq_id x) . n).| + |.((seq_id y) . n).| by A3; then |.(seq_id (x + y)).| . n <= (|.(seq_id x).| . n) + |.((seq_id y) . n).| by VALUED_1:18; hence |.(seq_id (x + y)).| . n <= (|.(seq_id x).| . n) + (|.(seq_id y).| . n) by VALUED_1:18; ::_thesis: verum end; A5: for n being Element of NAT holds |.(seq_id (x + y)).| . n <= (|.(seq_id x).| + |.(seq_id y).|) . n proof let n be Element of NAT ; ::_thesis: |.(seq_id (x + y)).| . n <= (|.(seq_id x).| + |.(seq_id y).|) . n (|.(seq_id x).| . n) + (|.(seq_id y).| . n) = (|.(seq_id x).| + |.(seq_id y).|) . n by SEQ_1:7; hence |.(seq_id (x + y)).| . n <= (|.(seq_id x).| + |.(seq_id y).|) . n by A4; ::_thesis: verum end; A6: now__::_thesis:_(_||.x.||_=_0_implies_x_=_0._Complex_linfty_Space_) A7: x in the_set_of_ComplexSequences by Def1; assume A8: ||.x.|| = 0 ; ::_thesis: x = 0. Complex_linfty_Space ( ||.x.|| = upper_bound (rng |.(seq_id x).|) & seq_id x is bounded ) by Th2; then for n being Element of NAT holds 0c = (seq_id x) . n by A8, Lm10; hence x = 0. Complex_linfty_Space by A7, Th2, CSSPACE:def_6; ::_thesis: verum end; seq_id x is bounded by Def1; then |.(seq_id x).| is bounded by Lm8; then A9: 0 <= upper_bound (rng |.(seq_id x).|) by A2, Lm2; seq_id y is bounded by Def1; then A10: |.(seq_id y).| is bounded by Lm8; seq_id x is bounded by Def1; then |.(seq_id x).| is bounded by Lm8; then rng |.(seq_id x).| is real-bounded by MEASURE6:39; then A11: rng |.(seq_id x).| is bounded_above by XXREAL_2:def_11; A12: now__::_thesis:_(_x_=_0._Complex_linfty_Space_implies_||.x.||_=_0_) assume x = 0. Complex_linfty_Space ; ::_thesis: ||.x.|| = 0 then A13: for n being Element of NAT holds (seq_id x) . n = 0c by Th2, CSSPACE:def_6; thus ||.x.|| = upper_bound (rng |.(seq_id x).|) by Th2 .= 0 by A13, Lm7 ; ::_thesis: verum end; seq_id x is bounded by Def1; then A14: |.(seq_id x).| is bounded by Lm8; now__::_thesis:_for_n_being_Element_of_NAT_holds_|.(seq_id_(x_+_y)).|_._n_<=_(upper_bound_(rng_|.(seq_id_x).|))_+_(upper_bound_(rng_|.(seq_id_y).|)) let n be Element of NAT ; ::_thesis: |.(seq_id (x + y)).| . n <= (upper_bound (rng |.(seq_id x).|)) + (upper_bound (rng |.(seq_id y).|)) A15: |.(seq_id y).| . n <= upper_bound (rng |.(seq_id y).|) by A10, Lm2; ( (|.(seq_id x).| + |.(seq_id y).|) . n = (|.(seq_id x).| . n) + (|.(seq_id y).| . n) & |.(seq_id x).| . n <= upper_bound (rng |.(seq_id x).|) ) by A14, Lm2, SEQ_1:7; then A16: (|.(seq_id x).| + |.(seq_id y).|) . n <= (upper_bound (rng |.(seq_id x).|)) + (upper_bound (rng |.(seq_id y).|)) by A15, XREAL_1:7; |.(seq_id (x + y)).| . n <= (|.(seq_id x).| + |.(seq_id y).|) . n by A5; hence |.(seq_id (x + y)).| . n <= (upper_bound (rng |.(seq_id x).|)) + (upper_bound (rng |.(seq_id y).|)) by A16, XXREAL_0:2; ::_thesis: verum end; then A17: upper_bound (rng |.(seq_id (x + y)).|) <= (upper_bound (rng |.(seq_id x).|)) + (upper_bound (rng |.(seq_id y).|)) by Lm1; A18: ( ||.y.|| = upper_bound (rng |.(seq_id y).|) & upper_bound (rng |.(seq_id (x + y)).|) = ||.(x + y).|| ) by Th2; ||.(c * x).|| = upper_bound (rng |.(seq_id (c * x)).|) by Th2 .= upper_bound (rng |.(seq_id (c (#) (seq_id x))).|) by Th2 .= upper_bound (rng |.(c (#) (seq_id x)).|) by CSSPACE:1 .= upper_bound (rng (|.c.| (#) |.(seq_id x).|)) by A1, SEQ_1:9 .= upper_bound (|.c.| ** (rng |.(seq_id x).|)) by INTEGRA2:17 .= |.c.| * (upper_bound (rng |.(seq_id x).|)) by A11, COMPLEX1:46, INTEGRA2:13 .= |.c.| * ||.x.|| by Th2 ; hence ( ( ||.x.|| = 0 implies x = 0. Complex_linfty_Space ) & ( x = 0. Complex_linfty_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(c * x).|| = |.c.| * ||.x.|| ) by A6, A12, A9, A18, A17, Th2; ::_thesis: verum end; registration cluster Complex_linfty_Space -> non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ; coherence ( Complex_linfty_Space is reflexive & Complex_linfty_Space is discerning & Complex_linfty_Space is ComplexNormSpace-like & Complex_linfty_Space is vector-distributive & Complex_linfty_Space is scalar-distributive & Complex_linfty_Space is scalar-associative & Complex_linfty_Space is scalar-unital & Complex_linfty_Space is Abelian & Complex_linfty_Space is add-associative & Complex_linfty_Space is right_zeroed & Complex_linfty_Space is right_complementable ) proof thus Complex_linfty_Space is reflexive ::_thesis: ( Complex_linfty_Space is discerning & Complex_linfty_Space is ComplexNormSpace-like & Complex_linfty_Space is vector-distributive & Complex_linfty_Space is scalar-distributive & Complex_linfty_Space is scalar-associative & Complex_linfty_Space is scalar-unital & Complex_linfty_Space is Abelian & Complex_linfty_Space is add-associative & Complex_linfty_Space is right_zeroed & Complex_linfty_Space is right_complementable ) proof thus ||.(0. Complex_linfty_Space).|| = 0 by Th3; :: according to NORMSP_0:def_6 ::_thesis: verum end; thus ( Complex_linfty_Space is discerning & Complex_linfty_Space is ComplexNormSpace-like & Complex_linfty_Space is vector-distributive & Complex_linfty_Space is scalar-distributive & Complex_linfty_Space is scalar-associative & Complex_linfty_Space is scalar-unital & Complex_linfty_Space is Abelian & Complex_linfty_Space is add-associative & Complex_linfty_Space is right_zeroed & Complex_linfty_Space is right_complementable ) by Th3, CLVECT_1:def_13, NORMSP_0:def_5; ::_thesis: verum end; end; Lm11: for seq1, seq2, seq3 being Complex_Sequence holds ( seq1 = seq2 - seq3 iff for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) ) proof let seq1, seq2, seq3 be Complex_Sequence; ::_thesis: ( seq1 = seq2 - seq3 iff for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) ) A1: ( ( for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) ) implies seq1 = seq2 - seq3 ) proof assume A2: for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) ; ::_thesis: seq1 = seq2 - seq3 for x being set st x in NAT holds seq1 . x = (seq2 - seq3) . x proof let x be set ; ::_thesis: ( x in NAT implies seq1 . x = (seq2 - seq3) . x ) assume x in NAT ; ::_thesis: seq1 . x = (seq2 - seq3) . x then reconsider x = x as Element of NAT ; seq1 . x = (seq2 . x) - (seq3 . x) by A2 .= (seq2 . x) + (- (seq3 . x)) .= (seq2 . x) + ((- seq3) . x) by VALUED_1:8 .= (seq2 + (- seq3)) . x by VALUED_1:1 ; hence seq1 . x = (seq2 - seq3) . x ; ::_thesis: verum end; hence seq1 = seq2 - seq3 by FUNCT_2:12; ::_thesis: verum end; ( seq1 = seq2 - seq3 implies for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) ) proof assume A3: seq1 = seq2 - seq3 ; ::_thesis: for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) now__::_thesis:_for_n_being_Element_of_NAT_holds_seq1_._n_=_(seq2_._n)_-_(seq3_._n) let n be Element of NAT ; ::_thesis: seq1 . n = (seq2 . n) - (seq3 . n) seq1 . n = (seq2 . n) + ((- seq3) . n) by A3, VALUED_1:1 .= (seq2 . n) + (- (seq3 . n)) by VALUED_1:8 ; hence seq1 . n = (seq2 . n) - (seq3 . n) ; ::_thesis: verum end; hence for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) ; ::_thesis: verum end; hence ( seq1 = seq2 - seq3 iff for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) ) by A1; ::_thesis: verum end; theorem Th4: :: CSSPACE4:4 for vseq being sequence of Complex_linfty_Space st vseq is Cauchy_sequence_by_Norm holds vseq is convergent proof let vseq be sequence of Complex_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 cseqi being Complex_Sequence st ( ( for n being Element of NAT holds cseqi . n = (seq_id (vseq . n)) . i ) & cseqi is convergent & $2 = lim cseqi ) ); A2: for x being set st x in NAT holds ex y being set st ( y in COMPLEX & S1[x,y] ) proof let x be set ; ::_thesis: ( x in NAT implies ex y being set st ( y in COMPLEX & S1[x,y] ) ) assume x in NAT ; ::_thesis: ex y being set st ( y in COMPLEX & S1[x,y] ) then reconsider i = x as Element of NAT ; deffunc H1( Element of NAT ) -> Element of COMPLEX = (seq_id (vseq . $1)) . i; consider cseqi being Complex_Sequence such that A3: for n being Element of NAT holds cseqi . n = H1(n) from COMSEQ_1:sch_1(); take lim cseqi ; ::_thesis: ( lim cseqi in COMPLEX & S1[x, lim cseqi] ) now__::_thesis:_for_e_being_Real_st_e_>_0_holds_ ex_k_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_k_<=_m_holds_ |.((cseqi_._m)_-_(cseqi_._k)).|_<_e let e be Real; ::_thesis: ( e > 0 implies ex k being Element of NAT st for m being Element of NAT st k <= m holds |.((cseqi . m) - (cseqi . k)).| < e ) assume A4: e > 0 ; ::_thesis: ex k being Element of NAT st for m being Element of NAT st k <= m holds |.((cseqi . m) - (cseqi . k)).| < e thus ex k being Element of NAT st for m being Element of NAT st k <= m holds |.((cseqi . m) - (cseqi . k)).| < e ::_thesis: verum proof 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, CSSPACE3:8; take k ; ::_thesis: for m being Element of NAT st k <= m holds |.((cseqi . m) - (cseqi . k)).| < e let m be Element of NAT ; ::_thesis: ( k <= m implies |.((cseqi . m) - (cseqi . k)).| < e ) assume A6: k <= m ; ::_thesis: |.((cseqi . m) - (cseqi . k)).| < e 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 CSSPACE:1 ; then (seq_id ((vseq . m) - (vseq . k))) . i = ((seq_id (vseq . m)) . i) + ((- (seq_id (vseq . k))) . i) by VALUED_1:1 .= ((seq_id (vseq . m)) . i) + (- ((seq_id (vseq . k)) . i)) by VALUED_1:8 .= ((seq_id (vseq . m)) . i) - ((seq_id (vseq . k)) . i) .= (cseqi . m) - ((seq_id (vseq . k)) . i) by A3 .= (cseqi . m) - (cseqi . k) by A3 ; then A7: |.((cseqi . m) - (cseqi . k)).| = |.(seq_id ((vseq . m) - (vseq . k))).| . i by VALUED_1:18; seq_id ((vseq . m) - (vseq . k)) is bounded by Def1; then |.(seq_id ((vseq . m) - (vseq . k))).| is bounded by Lm8; then A8: |.(seq_id ((vseq . m) - (vseq . k))).| . i <= upper_bound (rng |.(seq_id ((vseq . m) - (vseq . k))).|) by Lm2; ||.((vseq . m) - (vseq . k)).|| = upper_bound (rng |.(seq_id ((vseq . m) - (vseq . k))).|) by Th2; then upper_bound (rng |.(seq_id ((vseq . m) - (vseq . k))).|) < e by A5, A6; hence |.((cseqi . m) - (cseqi . k)).| < e by A8, A7, XXREAL_0:2; ::_thesis: verum end; end; then cseqi is convergent by COMSEQ_3:46; hence ( lim cseqi in COMPLEX & S1[x, lim cseqi] ) by A3; ::_thesis: verum end; consider f being Function of NAT,COMPLEX 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 Complex_Sequence ; A10: now__::_thesis:_for_i_being_Element_of_NAT_ex_cseqi_being_Complex_Sequence_st_ (_(_for_n_being_Element_of_NAT_holds_cseqi_._n_=_(seq_id_(vseq_._n))_._i_)_&_cseqi_is_convergent_&_tseq_._i_=_lim_cseqi_) let i be Element of NAT ; ::_thesis: ex cseqi being Complex_Sequence st ( ( for n being Element of NAT holds cseqi . n = (seq_id (vseq . n)) . i ) & cseqi is convergent & tseq . i = lim cseqi ) reconsider x = i as set ; ex i0 being Element of NAT st ( x = i0 & ex cseqi being Complex_Sequence st ( ( for n being Element of NAT holds cseqi . n = (seq_id (vseq . n)) . i0 ) & cseqi is convergent & f . x = lim cseqi ) ) by A9; hence ex cseqi being Complex_Sequence st ( ( for n being Element of NAT holds cseqi . n = (seq_id (vseq . n)) . i ) & cseqi is convergent & tseq . i = lim cseqi ) ; ::_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 ( |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded & upper_bound (rng |.((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 ( |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded & upper_bound (rng |.((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 ( |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded & upper_bound (rng |.((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, CSSPACE3:8; A14: for m, n being Element of NAT st n >= k & m >= k holds ( |.(seq_id ((vseq . n) - (vseq . m))).| is bounded & upper_bound (rng |.(seq_id ((vseq . n) - (vseq . m))).|) < e ) proof let m, n be Element of NAT ; ::_thesis: ( n >= k & m >= k implies ( |.(seq_id ((vseq . n) - (vseq . m))).| is bounded & upper_bound (rng |.(seq_id ((vseq . n) - (vseq . m))).|) < e ) ) assume ( n >= k & m >= k ) ; ::_thesis: ( |.(seq_id ((vseq . n) - (vseq . m))).| is bounded & upper_bound (rng |.(seq_id ((vseq . n) - (vseq . m))).|) < e ) then ||.((vseq . n) - (vseq . m)).|| < e by A13; then A15: the normF of Complex_linfty_Space . ((vseq . n) - (vseq . m)) < e ; seq_id ((vseq . n) - (vseq . m)) is bounded by Def1; hence ( |.(seq_id ((vseq . n) - (vseq . m))).| is bounded & upper_bound (rng |.(seq_id ((vseq . n) - (vseq . m))).|) < e ) by A15, Def2, Lm8; ::_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 = |.(seq_id ((vseq . m) - (vseq . n))).| . i ) holds ( rseq is convergent & lim rseq = |.((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 = |.(seq_id ((vseq . m) - (vseq . n))).| . i ) holds ( rseq is convergent & lim rseq = |.((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 CSSPACE: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_=_|.(seq_id_((vseq_._m)_-_(vseq_._n))).|_._i_)_holds_ (_rseq_is_convergent_&_lim_rseq_=_|.((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 = |.(seq_id ((vseq . m) - (vseq . n))).| . i ) holds ( rseq is convergent & lim rseq = |.((seq_id tseq) - (seq_id (vseq . n))).| . i ) consider cseqi being Complex_Sequence such that A18: for n being Element of NAT holds cseqi . n = (seq_id (vseq . n)) . i and A19: ( cseqi is convergent & tseq . i = lim cseqi ) by A10; now__::_thesis:_for_rseq_being_Real_Sequence_st_(_for_m_being_Element_of_NAT_holds_rseq_._m_=_|.(seq_id_((vseq_._m)_-_(vseq_._n))).|_._i_)_holds_ (_rseq_is_convergent_&_lim_rseq_=_|.((seq_id_tseq)_-_(seq_id_(vseq_._n))).|_._i_) let rseq be Real_Sequence; ::_thesis: ( ( for m being Element of NAT holds rseq . m = |.(seq_id ((vseq . m) - (vseq . n))).| . i ) implies ( rseq is convergent & lim rseq = |.((seq_id tseq) - (seq_id (vseq . n))).| . i ) ) assume A20: for m being Element of NAT holds rseq . m = |.(seq_id ((vseq . m) - (vseq . n))).| . i ; ::_thesis: ( rseq is convergent & lim rseq = |.((seq_id tseq) - (seq_id (vseq . n))).| . i ) A21: now__::_thesis:_for_m_being_Element_of_NAT_holds_rseq_._m_=_|.((cseqi_._m)_-_((seq_id_(vseq_._n))_._i)).| let m be Element of NAT ; ::_thesis: rseq . m = |.((cseqi . 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 = |.(seq_id ((vseq . m) - (vseq . n))).| . i by A20 .= |.((seq_id ((vseq . m) - (vseq . n))) . i).| by VALUED_1:18 .= |.(((seq_id (vseq . m)) . i) - ((seq_id (vseq . n)) . i)).| by A22, Lm11 .= |.((cseqi . m) - ((seq_id (vseq . n)) . i)).| by A18 ; ::_thesis: verum end; |.((tseq . i) - ((seq_id (vseq . n)) . i)).| = |.((tseq - (seq_id (vseq . n))) . i).| by Lm11 .= |.(((seq_id tseq) - (seq_id (vseq . n))) . i).| by CSSPACE:1 .= |.((seq_id tseq) - (seq_id (vseq . n))).| . i by VALUED_1:18 ; hence ( rseq is convergent & lim rseq = |.((seq_id tseq) - (seq_id (vseq . n))).| . i ) by A19, A21, CSSPACE3:1; ::_thesis: verum end; hence for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = |.(seq_id ((vseq . m) - (vseq . n))).| . i ) holds ( rseq is convergent & lim rseq = |.((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 = |.(seq_id ((vseq . m) - (vseq . n))).| . i ) holds ( rseq is convergent & lim rseq = |.((seq_id tseq) - (seq_id (vseq . n))).| . i ) ; ::_thesis: verum end; for n being Element of NAT st n >= k holds ( |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded & upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e ) proof let n be Element of NAT ; ::_thesis: ( n >= k implies ( |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded & upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e ) ) assume A23: n >= k ; ::_thesis: ( |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded & upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e ) A24: for i being Element of NAT holds |.((seq_id tseq) - (seq_id (vseq . n))).| . i <= e proof let i be Element of NAT ; ::_thesis: |.((seq_id tseq) - (seq_id (vseq . n))).| . i <= e deffunc H1( Element of NAT ) -> Element of REAL = |.(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 = |.(seq_id ((vseq . m) - (vseq . n))).| . i by A25; assume A28: m >= k ; ::_thesis: rseq . m <= e then |.(seq_id ((vseq . m) - (vseq . n))).| is bounded by A14, A23; then A29: |.(seq_id ((vseq . m) - (vseq . n))).| . i <= upper_bound (rng |.(seq_id ((vseq . m) - (vseq . n))).|) by Lm2; upper_bound (rng |.(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 = |.((seq_id tseq) - (seq_id (vseq . n))).| . i ) by A16, A25; hence |.((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_|.(((seq_id_tseq)_-_(seq_id_(vseq_._n)))_._i).|_<_e_+_1 let i be Element of NAT ; ::_thesis: |.(((seq_id tseq) - (seq_id (vseq . n))) . i).| < e + 1 |.((seq_id tseq) - (seq_id (vseq . n))).| . i <= e by A24; then |.(((seq_id tseq) - (seq_id (vseq . n))) . i).| <= e by VALUED_1:18; hence |.(((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, COMSEQ_2:8; hence ( |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded & upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e ) by A24, Lm1, Lm8; ::_thesis: verum end; hence ex k being Element of NAT st for n being Element of NAT st n >= k holds ( |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded & upper_bound (rng |.((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 ( |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded & upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= 1 ) by A11; A33: |.((seq_id tseq) - (seq_id (vseq . m))).| is bounded by A32; set d = |.(seq_id tseq).|; set b = |.(seq_id (vseq . m)).|; set a = |.((seq_id tseq) - (seq_id (vseq . m))).|; seq_id (vseq . m) is bounded by Def1; then A34: |.(seq_id (vseq . m)).| is bounded by Lm8; A35: for i being Element of NAT holds |.(seq_id tseq).| . i <= (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|) . i proof let i be Element of NAT ; ::_thesis: |.(seq_id tseq).| . i <= (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|) . i A36: ( |.(seq_id (vseq . m)).| . i = |.((seq_id (vseq . m)) . i).| & |.(seq_id tseq).| . i = |.((seq_id tseq) . i).| ) by VALUED_1:18; |.((seq_id tseq) - (seq_id (vseq . m))).| . i = |.(((seq_id tseq) + (- (seq_id (vseq . m)))) . i).| by VALUED_1:18 .= |.(((seq_id tseq) . i) + ((- (seq_id (vseq . m))) . i)).| by VALUED_1:1 .= |.(((seq_id tseq) . i) + (- ((seq_id (vseq . m)) . i))).| by VALUED_1:8 .= |.(((seq_id tseq) . i) - ((seq_id (vseq . m)) . i)).| ; then (|.(seq_id tseq).| . i) - (|.(seq_id (vseq . m)).| . i) <= |.((seq_id tseq) - (seq_id (vseq . m))).| . i by A36, COMPLEX1:59; then ((|.(seq_id tseq).| . i) - (|.(seq_id (vseq . m)).| . i)) + (|.(seq_id (vseq . m)).| . i) <= (|.((seq_id tseq) - (seq_id (vseq . m))).| . i) + (|.(seq_id (vseq . m)).| . i) by XREAL_1:6; hence |.(seq_id tseq).| . i <= (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|) . i by SEQ_1:7; ::_thesis: verum end; |.(seq_id tseq).| is bounded proof reconsider r = (upper_bound (rng (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|))) + 1 as real number ; |.(seq_id (vseq . m)).| . 1 = |.((seq_id (vseq . m)) . 1).| by VALUED_1:18; then A37: 0 <= |.(seq_id (vseq . m)).| . 1 by COMPLEX1:46; A38: (upper_bound (rng (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|))) + 0 < (upper_bound (rng (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|))) + 1 by XREAL_1:8; A39: now__::_thesis:_for_i_being_Element_of_NAT_holds_|.((seq_id_tseq)_._i).|_<_r let i be Element of NAT ; ::_thesis: |.((seq_id tseq) . i).| < r ( |.(seq_id tseq).| . i <= (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|) . i & (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|) . i <= upper_bound (rng (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|)) ) by A33, A34, A35, Lm2; then A40: |.(seq_id tseq).| . i <= upper_bound (rng (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|)) by XXREAL_0:2; |.(seq_id tseq).| . i = |.((seq_id tseq) . i).| by VALUED_1:18; hence |.((seq_id tseq) . i).| < r by A38, A40, XXREAL_0:2; ::_thesis: verum end; |.((seq_id tseq) - (seq_id (vseq . m))).| . 1 = |.(((seq_id tseq) - (seq_id (vseq . m))) . 1).| by VALUED_1:18; then ( (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|) . 1 = (|.((seq_id tseq) - (seq_id (vseq . m))).| . 1) + (|.(seq_id (vseq . m)).| . 1) & 0 <= |.((seq_id tseq) - (seq_id (vseq . m))).| . 1 ) by COMPLEX1:46, SEQ_1:7; then 0 <= upper_bound (rng (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|)) by A33, A34, A37, Lm2; then seq_id tseq is bounded by A39, COMSEQ_2:8; hence |.(seq_id tseq).| is bounded by Lm8; ::_thesis: verum end; hence seq_id tseq is bounded by Lm9; ::_thesis: verum end; A41: tseq in the_set_of_ComplexSequences by CSSPACE:def_1; then reconsider tv = tseq as Point of Complex_linfty_Space by A31, Def1; ex tv being Point of Complex_linfty_Space st for e1 being Real st e1 > 0 holds ex m being Element of NAT st for n being Element of NAT st n >= m holds ||.((vseq . n) - tv).|| < e1 proof take tv ; ::_thesis: for e1 being Real st e1 > 0 holds ex m being Element of NAT st for n being Element of NAT st n >= m holds ||.((vseq . n) - tv).|| < e1 let e1 be Real; ::_thesis: ( e1 > 0 implies ex m being Element of NAT st for n being Element of NAT st n >= m holds ||.((vseq . n) - tv).|| < e1 ) assume A42: e1 > 0 ; ::_thesis: ex m being Element of NAT st for n being Element of NAT st n >= m holds ||.((vseq . n) - tv).|| < e1 set e = e1 / 2; consider m being Element of NAT such that A43: for n being Element of NAT st n >= m holds ( |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded & upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e1 / 2 ) by A11, A42; 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 Complex_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 |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e1 / 2 by A43; reconsider v = vseq . n as VECTOR of Complex_linfty_Space ; seq_id (u - v) = u - v by Th2; then upper_bound (rng |.(seq_id (u - v)).|) = upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) by Th2; then A46: the normF of Complex_linfty_Space . (u - v) <= e1 / 2 by A45, Def2; ||.((vseq . n) - tv).|| = ||.(- (tv - (vseq . n))).|| by RLVECT_1:33 .= ||.(tv - (vseq . n)).|| by CLVECT_1:103 ; then ||.((vseq . n) - tv).|| <= e1 / 2 by A46; hence ||.((vseq . n) - tv).|| < e1 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).|| < e1 ; ::_thesis: verum end; hence vseq is convergent by CLVECT_1:def_15; ::_thesis: verum end; theorem :: CSSPACE4:5 Complex_linfty_Space is ComplexBanachSpace by Th4, CLOPBAN1:def_13; begin definition let X be non empty set ; let Y be ComplexNormSpace; let IT be Function of X, the carrier of Y; attrIT is bounded means :Def4: :: CSSPACE4:def 4 ex K being Real st ( 0 <= K & ( for x being Element of X holds ||.(IT . x).|| <= K ) ); end; :: deftheorem Def4 defines bounded CSSPACE4:def_4_:_ for X being non empty set for Y being ComplexNormSpace for IT being Function of X, the carrier of Y holds ( IT is bounded iff ex K being Real st ( 0 <= K & ( for x being Element of X holds ||.(IT . x).|| <= K ) ) ); theorem Th6: :: CSSPACE4:6 for X being non empty set for Y being ComplexNormSpace 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 ComplexNormSpace 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 ComplexNormSpace; ::_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 CSSPACE4: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 ComplexNormSpace; 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 Th6; ::_thesis: verum end; end; definition let X be non empty set ; let Y be ComplexNormSpace; func ComplexBoundedFunctions (X,Y) -> Subset of (ComplexVectSpace (X,Y)) means :Def5: :: CSSPACE4: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 (ComplexVectSpace (X,Y)) st for x being set holds ( x in b1 iff x is bounded Function of X, the carrier of Y ) proof defpred S1[ set ] means $1 is bounded Function of X, the carrier of Y; consider IT being set such that A1: 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 (ComplexVectSpace (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 A1; hence IT is Subset of (ComplexVectSpace (X,Y)) by 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 A1; ::_thesis: ( x is bounded Function of X, the carrier of Y implies x in IT ) assume A2: 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 A1, A2; ::_thesis: verum end; uniqueness for b1, b2 being Subset of (ComplexVectSpace (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 (ComplexVectSpace (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 A3: for x being set holds ( x in X1 iff x is bounded Function of X, the carrier of Y ) and A4: 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 A4; hence x in X1 by A3; ::_thesis: verum end; then A5: 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 A3; hence x in X2 by A4; ::_thesis: verum end; then X1 c= X2 by TARSKI:def_3; hence X1 = X2 by A5, XBOOLE_0:def_10; ::_thesis: verum end; end; :: deftheorem Def5 defines ComplexBoundedFunctions CSSPACE4:def_5_:_ for X being non empty set for Y being ComplexNormSpace for b3 being Subset of (ComplexVectSpace (X,Y)) holds ( b3 = ComplexBoundedFunctions (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 ComplexNormSpace; cluster ComplexBoundedFunctions (X,Y) -> non empty ; coherence not ComplexBoundedFunctions (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 Th6; hence not ComplexBoundedFunctions (X,Y) is empty by Def5; ::_thesis: verum end; end; theorem Th7: :: CSSPACE4:7 for X being non empty set for Y being ComplexNormSpace holds ComplexBoundedFunctions (X,Y) is linearly-closed proof let X be non empty set ; ::_thesis: for Y being ComplexNormSpace holds ComplexBoundedFunctions (X,Y) is linearly-closed let Y be ComplexNormSpace; ::_thesis: ComplexBoundedFunctions (X,Y) is linearly-closed set W = ComplexBoundedFunctions (X,Y); A1: for v, u being VECTOR of (ComplexVectSpace (X,Y)) st v in ComplexBoundedFunctions (X,Y) & u in ComplexBoundedFunctions (X,Y) holds v + u in ComplexBoundedFunctions (X,Y) proof let v, u be VECTOR of (ComplexVectSpace (X,Y)); ::_thesis: ( v in ComplexBoundedFunctions (X,Y) & u in ComplexBoundedFunctions (X,Y) implies v + u in ComplexBoundedFunctions (X,Y) ) assume that A2: v in ComplexBoundedFunctions (X,Y) and A3: u in ComplexBoundedFunctions (X,Y) ; ::_thesis: v + u in ComplexBoundedFunctions (X,Y) reconsider f = v + u as Function of X, the carrier of Y by FUNCT_2:66; f is bounded proof reconsider v1 = v as bounded Function of X, the carrier of Y by A2, Def5; consider K2 being Real such that A4: 0 <= K2 and A5: 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 A3, Def5; consider K1 being Real such that A6: 0 <= K1 and A7: for x being Element of X holds ||.(u1 . x).|| <= K1 by Def4; take K3 = K1 + K2; :: according to CSSPACE4: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 A7, A5; then A8: ||.(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 CLOPBAN1:11, CLVECT_1:def_13; hence ||.(f . x).|| <= K3 by A8, XXREAL_0:2; ::_thesis: verum end; hence ( 0 <= K3 & ( for x being Element of X holds ||.(f . x).|| <= K3 ) ) by A6, A4; ::_thesis: verum end; hence v + u in ComplexBoundedFunctions (X,Y) by Def5; ::_thesis: verum end; for c being Complex for v being VECTOR of (ComplexVectSpace (X,Y)) st v in ComplexBoundedFunctions (X,Y) holds c * v in ComplexBoundedFunctions (X,Y) proof let c be Complex; ::_thesis: for v being VECTOR of (ComplexVectSpace (X,Y)) st v in ComplexBoundedFunctions (X,Y) holds c * v in ComplexBoundedFunctions (X,Y) let v be VECTOR of (ComplexVectSpace (X,Y)); ::_thesis: ( v in ComplexBoundedFunctions (X,Y) implies c * v in ComplexBoundedFunctions (X,Y) ) assume A9: v in ComplexBoundedFunctions (X,Y) ; ::_thesis: c * v in ComplexBoundedFunctions (X,Y) reconsider f = c * v as Function of X, the carrier of Y by FUNCT_2:66; f is bounded proof reconsider v1 = v as bounded Function of X, the carrier of Y by A9, Def5; consider K being Real such that A10: 0 <= K and A11: for x being Element of X holds ||.(v1 . x).|| <= K by Def4; take |.c.| * K ; :: according to CSSPACE4:def_4 ::_thesis: ( 0 <= |.c.| * K & ( for x being Element of X holds ||.(f . x).|| <= |.c.| * K ) ) A12: now__::_thesis:_for_x_being_Element_of_X_holds_||.(f_._x).||_<=_|.c.|_*_K let x be Element of X; ::_thesis: ||.(f . x).|| <= |.c.| * K A13: 0 <= |.c.| by COMPLEX1:46; ( ||.(f . x).|| = ||.(c * (v1 . x)).|| & ||.(c * (v1 . x)).|| = |.c.| * ||.(v1 . x).|| ) by CLOPBAN1:12, CLVECT_1:def_13; hence ||.(f . x).|| <= |.c.| * K by A11, A13, XREAL_1:64; ::_thesis: verum end; 0 <= |.c.| by COMPLEX1:46; hence ( 0 <= |.c.| * K & ( for x being Element of X holds ||.(f . x).|| <= |.c.| * K ) ) by A10, A12; ::_thesis: verum end; hence c * v in ComplexBoundedFunctions (X,Y) by Def5; ::_thesis: verum end; hence ComplexBoundedFunctions (X,Y) is linearly-closed by A1, CLVECT_1:def_7; ::_thesis: verum end; theorem :: CSSPACE4:8 for X being non empty set for Y being ComplexNormSpace holds CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #) is Subspace of ComplexVectSpace (X,Y) by Th7, CSSPACE:11; registration let X be non empty set ; let Y be ComplexNormSpace; cluster CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ; coherence ( CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #) is Abelian & CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #) is add-associative & CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #) is right_zeroed & CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #) is right_complementable & CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #) is vector-distributive & CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #) is scalar-distributive & CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #) is scalar-associative & CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #) is scalar-unital ) by Th7, CSSPACE:11; end; definition let X be non empty set ; let Y be ComplexNormSpace; func C_VectorSpace_of_BoundedFunctions (X,Y) -> ComplexLinearSpace equals :: CSSPACE4:def 6 CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #); coherence CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #) is ComplexLinearSpace ; end; :: deftheorem defines C_VectorSpace_of_BoundedFunctions CSSPACE4:def_6_:_ for X being non empty set for Y being ComplexNormSpace holds C_VectorSpace_of_BoundedFunctions (X,Y) = CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #); registration let X be non empty set ; let Y be ComplexNormSpace; cluster C_VectorSpace_of_BoundedFunctions (X,Y) -> strict ; coherence C_VectorSpace_of_BoundedFunctions (X,Y) is strict ; end; theorem Th9: :: CSSPACE4:9 for X being non empty set for Y being ComplexNormSpace for f, g, h being VECTOR of (C_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 ComplexNormSpace for f, g, h being VECTOR of (C_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 ComplexNormSpace; ::_thesis: for f, g, h being VECTOR of (C_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 (C_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: C_VectorSpace_of_BoundedFunctions (X,Y) is Subspace of ComplexVectSpace (X,Y) by Th7, CSSPACE:11; then reconsider f1 = f as VECTOR of (ComplexVectSpace (X,Y)) by CLVECT_1:29; reconsider h1 = h as VECTOR of (ComplexVectSpace (X,Y)) by A1, CLVECT_1:29; reconsider g1 = g as VECTOR of (ComplexVectSpace (X,Y)) by A1, CLVECT_1:29; 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, CLVECT_1:32; hence h9 . x = (f9 . x) + (g9 . x) by A2, CLOPBAN1: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, CLOPBAN1:11; hence h = f + g by A1, CLVECT_1:32; ::_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 Th10: :: CSSPACE4:10 for X being non empty set for Y being ComplexNormSpace for f, h being VECTOR of (C_VectorSpace_of_BoundedFunctions (X,Y)) for f9, h9 being bounded Function of X, the carrier of Y st f9 = f & h9 = h holds for c being Complex holds ( h = c * f iff for x being Element of X holds h9 . x = c * (f9 . x) ) proof let X be non empty set ; ::_thesis: for Y being ComplexNormSpace for f, h being VECTOR of (C_VectorSpace_of_BoundedFunctions (X,Y)) for f9, h9 being bounded Function of X, the carrier of Y st f9 = f & h9 = h holds for c being Complex holds ( h = c * f iff for x being Element of X holds h9 . x = c * (f9 . x) ) let Y be ComplexNormSpace; ::_thesis: for f, h being VECTOR of (C_VectorSpace_of_BoundedFunctions (X,Y)) for f9, h9 being bounded Function of X, the carrier of Y st f9 = f & h9 = h holds for c being Complex holds ( h = c * f iff for x being Element of X holds h9 . x = c * (f9 . x) ) let f, h be VECTOR of (C_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 c being Complex holds ( h = c * f iff for x being Element of X holds h9 . x = c * (f9 . x) ) let f9, h9 be bounded Function of X, the carrier of Y; ::_thesis: ( f9 = f & h9 = h implies for c being Complex holds ( h = c * f iff for x being Element of X holds h9 . x = c * (f9 . x) ) ) assume A1: ( f9 = f & h9 = h ) ; ::_thesis: for c being Complex holds ( h = c * f iff for x being Element of X holds h9 . x = c * (f9 . x) ) let c be Complex; ::_thesis: ( h = c * f iff for x being Element of X holds h9 . x = c * (f9 . x) ) A2: C_VectorSpace_of_BoundedFunctions (X,Y) is Subspace of ComplexVectSpace (X,Y) by Th7, CSSPACE:11; then reconsider f1 = f, h1 = h as VECTOR of (ComplexVectSpace (X,Y)) by CLVECT_1:29; A3: now__::_thesis:_(_h_=_c_*_f_implies_for_x_being_Element_of_X_holds_h9_._x_=_c_*_(f9_._x)_) assume A4: h = c * f ; ::_thesis: for x being Element of X holds h9 . x = c * (f9 . x) let x be Element of X; ::_thesis: h9 . x = c * (f9 . x) h1 = c * f1 by A2, A4, CLVECT_1:33; hence h9 . x = c * (f9 . x) by A1, CLOPBAN1:12; ::_thesis: verum end; now__::_thesis:_(_(_for_x_being_Element_of_X_holds_h9_._x_=_c_*_(f9_._x)_)_implies_h_=_c_*_f_) assume for x being Element of X holds h9 . x = c * (f9 . x) ; ::_thesis: h = c * f then h1 = c * f1 by A1, CLOPBAN1:12; hence h = c * f by A2, CLVECT_1:33; ::_thesis: verum end; hence ( h = c * f iff for x being Element of X holds h9 . x = c * (f9 . x) ) by A3; ::_thesis: verum end; theorem Th11: :: CSSPACE4:11 for X being non empty set for Y being ComplexNormSpace holds 0. (C_VectorSpace_of_BoundedFunctions (X,Y)) = X --> (0. Y) proof let X be non empty set ; ::_thesis: for Y being ComplexNormSpace holds 0. (C_VectorSpace_of_BoundedFunctions (X,Y)) = X --> (0. Y) let Y be ComplexNormSpace; ::_thesis: 0. (C_VectorSpace_of_BoundedFunctions (X,Y)) = X --> (0. Y) ( C_VectorSpace_of_BoundedFunctions (X,Y) is Subspace of ComplexVectSpace (X,Y) & 0. (ComplexVectSpace (X,Y)) = X --> (0. Y) ) by Th7, CSSPACE:11, LOPBAN_1:def_3; hence 0. (C_VectorSpace_of_BoundedFunctions (X,Y)) = X --> (0. Y) by CLVECT_1:30; ::_thesis: verum end; definition let X be non empty set ; let Y be ComplexNormSpace; let f be set ; assume A1: f in ComplexBoundedFunctions (X,Y) ; func modetrans (f,X,Y) -> bounded Function of X, the carrier of Y equals :Def7: :: CSSPACE4:def 7 f; coherence f is bounded Function of X, the carrier of Y by A1, Def5; end; :: deftheorem Def7 defines modetrans CSSPACE4:def_7_:_ for X being non empty set for Y being ComplexNormSpace for f being set st f in ComplexBoundedFunctions (X,Y) holds modetrans (f,X,Y) = f; definition let X be non empty set ; let Y be ComplexNormSpace; let u be Function of X, the carrier of Y; func PreNorms u -> non empty Subset of REAL equals :: CSSPACE4: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 CSSPACE4:def_8_:_ for X being non empty set for Y being ComplexNormSpace for u being Function of X, the carrier of Y holds PreNorms u = { ||.(u . t).|| where t is Element of X : verum } ; theorem Th12: :: CSSPACE4:12 for X being non empty set for Y being ComplexNormSpace 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 ComplexNormSpace for g being bounded Function of X, the carrier of Y holds PreNorms g is bounded_above let Y be ComplexNormSpace; ::_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 :: CSSPACE4:13 for X being non empty set for Y being ComplexNormSpace 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 ComplexNormSpace for g being Function of X, the carrier of Y holds ( g is bounded iff PreNorms g is bounded_above ) let Y be ComplexNormSpace; ::_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 by CLVECT_1:105; ::_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 Th12; ::_thesis: verum end; definition let X be non empty set ; let Y be ComplexNormSpace; func ComplexBoundedFunctionsNorm (X,Y) -> Function of (ComplexBoundedFunctions (X,Y)),REAL means :Def9: :: CSSPACE4:def 9 for x being set st x in ComplexBoundedFunctions (X,Y) holds it . x = upper_bound (PreNorms (modetrans (x,X,Y))); existence ex b1 being Function of (ComplexBoundedFunctions (X,Y)),REAL st for x being set st x in ComplexBoundedFunctions (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 ComplexBoundedFunctions (X,Y) holds H1(z) in REAL ; ex f being Function of (ComplexBoundedFunctions (X,Y)),REAL st for x being set st x in ComplexBoundedFunctions (X,Y) holds f . x = H1(x) from FUNCT_2:sch_2(A1); hence ex b1 being Function of (ComplexBoundedFunctions (X,Y)),REAL st for x being set st x in ComplexBoundedFunctions (X,Y) holds b1 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ; ::_thesis: verum end; uniqueness for b1, b2 being Function of (ComplexBoundedFunctions (X,Y)),REAL st ( for x being set st x in ComplexBoundedFunctions (X,Y) holds b1 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) & ( for x being set st x in ComplexBoundedFunctions (X,Y) holds b2 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) holds b1 = b2 proof let NORM1, NORM2 be Function of (ComplexBoundedFunctions (X,Y)),REAL; ::_thesis: ( ( for x being set st x in ComplexBoundedFunctions (X,Y) holds NORM1 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) & ( for x being set st x in ComplexBoundedFunctions (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 ComplexBoundedFunctions (X,Y) holds NORM1 . x = upper_bound (PreNorms (modetrans (x,X,Y))) and A3: for x being set st x in ComplexBoundedFunctions (X,Y) holds NORM2 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ; ::_thesis: NORM1 = NORM2 A4: for z being set st z in ComplexBoundedFunctions (X,Y) holds NORM1 . z = NORM2 . z proof let z be set ; ::_thesis: ( z in ComplexBoundedFunctions (X,Y) implies NORM1 . z = NORM2 . z ) assume A5: z in ComplexBoundedFunctions (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 = ComplexBoundedFunctions (X,Y) & dom NORM2 = ComplexBoundedFunctions (X,Y) ) by FUNCT_2:def_1; hence NORM1 = NORM2 by A4, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def9 defines ComplexBoundedFunctionsNorm CSSPACE4:def_9_:_ for X being non empty set for Y being ComplexNormSpace for b3 being Function of (ComplexBoundedFunctions (X,Y)),REAL holds ( b3 = ComplexBoundedFunctionsNorm (X,Y) iff for x being set st x in ComplexBoundedFunctions (X,Y) holds b3 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ); theorem Th14: :: CSSPACE4:14 for X being non empty set for Y being ComplexNormSpace 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 ComplexNormSpace for f being bounded Function of X, the carrier of Y holds modetrans (f,X,Y) = f let Y be ComplexNormSpace; ::_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 ComplexBoundedFunctions (X,Y) by Def5; hence modetrans (f,X,Y) = f by Def7; ::_thesis: verum end; theorem Th15: :: CSSPACE4:15 for X being non empty set for Y being ComplexNormSpace for f being bounded Function of X, the carrier of Y holds (ComplexBoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms f) proof let X be non empty set ; ::_thesis: for Y being ComplexNormSpace for f being bounded Function of X, the carrier of Y holds (ComplexBoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms f) let Y be ComplexNormSpace; ::_thesis: for f being bounded Function of X, the carrier of Y holds (ComplexBoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms f) let f be bounded Function of X, the carrier of Y; ::_thesis: (ComplexBoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms f) reconsider f9 = f as set ; f in ComplexBoundedFunctions (X,Y) by Def5; hence (ComplexBoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms (modetrans (f9,X,Y))) by Def9 .= upper_bound (PreNorms f) by Th14 ; ::_thesis: verum end; definition let X be non empty set ; let Y be ComplexNormSpace; func C_NormSpace_of_BoundedFunctions (X,Y) -> non empty CNORMSTR equals :: CSSPACE4:def 10 CNORMSTR(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(ComplexBoundedFunctionsNorm (X,Y)) #); coherence CNORMSTR(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(ComplexBoundedFunctionsNorm (X,Y)) #) is non empty CNORMSTR ; end; :: deftheorem defines C_NormSpace_of_BoundedFunctions CSSPACE4:def_10_:_ for X being non empty set for Y being ComplexNormSpace holds C_NormSpace_of_BoundedFunctions (X,Y) = CNORMSTR(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(ComplexBoundedFunctionsNorm (X,Y)) #); theorem Th16: :: CSSPACE4:16 for X being non empty set for Y being ComplexNormSpace holds X --> (0. Y) = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) proof let X be non empty set ; ::_thesis: for Y being ComplexNormSpace holds X --> (0. Y) = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) let Y be ComplexNormSpace; ::_thesis: X --> (0. Y) = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) X --> (0. Y) = 0. (C_VectorSpace_of_BoundedFunctions (X,Y)) by Th11 .= 0. (C_NormSpace_of_BoundedFunctions (X,Y)) ; hence X --> (0. Y) = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) ; ::_thesis: verum end; theorem Th17: :: CSSPACE4:17 for X being non empty set for Y being ComplexNormSpace for f being Point of (C_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 ComplexNormSpace for f being Point of (C_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 ComplexNormSpace; ::_thesis: for f being Point of (C_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 (C_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 Th12; 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; then ||.(g . t).|| <= (ComplexBoundedFunctionsNorm (X,Y)) . g by Th15; hence ||.(g . t).|| <= ||.f.|| by A1; ::_thesis: verum end; hence for t being Element of X holds ||.(g . t).|| <= ||.f.|| ; ::_thesis: verum end; theorem :: CSSPACE4:18 for X being non empty set for Y being ComplexNormSpace for f being Point of (C_NormSpace_of_BoundedFunctions (X,Y)) holds 0 <= ||.f.|| proof let X be non empty set ; ::_thesis: for Y being ComplexNormSpace for f being Point of (C_NormSpace_of_BoundedFunctions (X,Y)) holds 0 <= ||.f.|| let Y be ComplexNormSpace; ::_thesis: for f being Point of (C_NormSpace_of_BoundedFunctions (X,Y)) holds 0 <= ||.f.|| let f be Point of (C_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 Th12; A3: (ComplexBoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms g) by Th15; 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 by CLVECT_1:105; ::_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 A3; ::_thesis: verum end; theorem Th19: :: CSSPACE4:19 for X being non empty set for Y being ComplexNormSpace for f being Point of (C_NormSpace_of_BoundedFunctions (X,Y)) st f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) holds 0 = ||.f.|| proof let X be non empty set ; ::_thesis: for Y being ComplexNormSpace for f being Point of (C_NormSpace_of_BoundedFunctions (X,Y)) st f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) holds 0 = ||.f.|| let Y be ComplexNormSpace; ::_thesis: for f being Point of (C_NormSpace_of_BoundedFunctions (X,Y)) st f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) holds 0 = ||.f.|| let f be Point of (C_NormSpace_of_BoundedFunctions (X,Y)); ::_thesis: ( f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) implies 0 = ||.f.|| ) assume A1: f = 0. (C_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 Th12; A5: z = g by A1, Th16; 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; then (ComplexBoundedFunctionsNorm (X,Y)) . f = 0 by Th15; hence ||.f.|| = 0 ; ::_thesis: verum end; end; theorem Th20: :: CSSPACE4:20 for X being non empty set for Y being ComplexNormSpace for f, g, h being Point of (C_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 ComplexNormSpace for f, g, h being Point of (C_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 ComplexNormSpace; ::_thesis: for f, g, h being Point of (C_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 (C_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 (C_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, Th9; ::_thesis: verum end; theorem Th21: :: CSSPACE4:21 for X being non empty set for Y being ComplexNormSpace for f, h being Point of (C_NormSpace_of_BoundedFunctions (X,Y)) for f9, h9 being bounded Function of X, the carrier of Y st f9 = f & h9 = h holds for c being Complex holds ( h = c * f iff for x being Element of X holds h9 . x = c * (f9 . x) ) proof let X be non empty set ; ::_thesis: for Y being ComplexNormSpace for f, h being Point of (C_NormSpace_of_BoundedFunctions (X,Y)) for f9, h9 being bounded Function of X, the carrier of Y st f9 = f & h9 = h holds for c being Complex holds ( h = c * f iff for x being Element of X holds h9 . x = c * (f9 . x) ) let Y be ComplexNormSpace; ::_thesis: for f, h being Point of (C_NormSpace_of_BoundedFunctions (X,Y)) for f9, h9 being bounded Function of X, the carrier of Y st f9 = f & h9 = h holds for c being Complex holds ( h = c * f iff for x being Element of X holds h9 . x = c * (f9 . x) ) let f, h be Point of (C_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 c being Complex holds ( h = c * f iff for x being Element of X holds h9 . x = c * (f9 . x) ) let f9, h9 be bounded Function of X, the carrier of Y; ::_thesis: ( f9 = f & h9 = h implies for c being Complex holds ( h = c * f iff for x being Element of X holds h9 . x = c * (f9 . x) ) ) assume A1: ( f9 = f & h9 = h ) ; ::_thesis: for c being Complex holds ( h = c * f iff for x being Element of X holds h9 . x = c * (f9 . x) ) reconsider h1 = h as VECTOR of (C_VectorSpace_of_BoundedFunctions (X,Y)) ; reconsider f1 = f as VECTOR of (C_VectorSpace_of_BoundedFunctions (X,Y)) ; let c be Complex; ::_thesis: ( h = c * f iff for x being Element of X holds h9 . x = c * (f9 . x) ) A2: now__::_thesis:_(_h1_=_c_*_f1_implies_h_=_c_*_f_) assume h1 = c * f1 ; ::_thesis: h = c * f hence h = (Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) . [c,f1] by CLVECT_1:def_1 .= c * f by CLVECT_1:def_1 ; ::_thesis: verum end; now__::_thesis:_(_h_=_c_*_f_implies_h1_=_c_*_f1_) assume h = c * f ; ::_thesis: h1 = c * f1 hence h1 = (Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) . [c,f] by CLVECT_1:def_1 .= c * f1 by CLVECT_1:def_1 ; ::_thesis: verum end; hence ( h = c * f iff for x being Element of X holds h9 . x = c * (f9 . x) ) by A1, A2, Th10; ::_thesis: verum end; theorem Th22: :: CSSPACE4:22 for X being non empty set for Y being ComplexNormSpace for f, g being Point of (C_NormSpace_of_BoundedFunctions (X,Y)) for c being Complex holds ( ( ||.f.|| = 0 implies f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) ) & ( f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) implies ||.f.|| = 0 ) & ||.(c * f).|| = |.c.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| ) proof let X be non empty set ; ::_thesis: for Y being ComplexNormSpace for f, g being Point of (C_NormSpace_of_BoundedFunctions (X,Y)) for c being Complex holds ( ( ||.f.|| = 0 implies f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) ) & ( f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) implies ||.f.|| = 0 ) & ||.(c * f).|| = |.c.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| ) let Y be ComplexNormSpace; ::_thesis: for f, g being Point of (C_NormSpace_of_BoundedFunctions (X,Y)) for c being Complex holds ( ( ||.f.|| = 0 implies f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) ) & ( f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) implies ||.f.|| = 0 ) & ||.(c * f).|| = |.c.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| ) let f, g be Point of (C_NormSpace_of_BoundedFunctions (X,Y)); ::_thesis: for c being Complex holds ( ( ||.f.|| = 0 implies f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) ) & ( f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) implies ||.f.|| = 0 ) & ||.(c * f).|| = |.c.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| ) let c be Complex; ::_thesis: ( ( ||.f.|| = 0 implies f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) ) & ( f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) implies ||.f.|| = 0 ) & ||.(c * f).|| = |.c.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| ) A1: now__::_thesis:_(_f_=_0._(C_NormSpace_of_BoundedFunctions_(X,Y))_implies_||.f.||_=_0_) assume A2: f = 0. (C_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 Th12; A6: z = g by A2, Th16; 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; then (ComplexBoundedFunctionsNorm (X,Y)) . f = 0 by Th15; hence ||.f.|| = 0 ; ::_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: ( ( 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; A11: 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 Th17; then A12: ||.(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 Th20, CLVECT_1:def_13; hence ||.(h1 . t).|| <= ||.f.|| + ||.g.|| by A12, XXREAL_0:2; ::_thesis: verum end; A13: 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 A11; ::_thesis: verum end; (ComplexBoundedFunctionsNorm (X,Y)) . (f + g) = upper_bound (PreNorms h1) by Th15; hence ||.(f + g).|| <= ||.f.|| + ||.g.|| by A13, A10; ::_thesis: verum end; A14: ||.(c * f).|| = |.c.| * ||.f.|| proof reconsider f1 = f, h1 = c * f as bounded Function of X, the carrier of Y by Def5; A15: ( ( for s being real number st s in PreNorms h1 holds s <= |.c.| * ||.f.|| ) implies upper_bound (PreNorms h1) <= |.c.| * ||.f.|| ) by SEQ_4:45; A16: now__::_thesis:_for_t_being_Element_of_X_holds_||.(h1_._t).||_<=_|.c.|_*_||.f.|| let t be Element of X; ::_thesis: ||.(h1 . t).|| <= |.c.| * ||.f.|| A17: 0 <= |.c.| by COMPLEX1:46; ( ||.(h1 . t).|| = ||.(c * (f1 . t)).|| & ||.(c * (f1 . t)).|| = |.c.| * ||.(f1 . t).|| ) by Th21, CLVECT_1:def_13; hence ||.(h1 . t).|| <= |.c.| * ||.f.|| by A17, Th17, XREAL_1:64; ::_thesis: verum end; A18: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_h1_holds_ r_<=_|.c.|_*_||.f.|| let r be Real; ::_thesis: ( r in PreNorms h1 implies r <= |.c.| * ||.f.|| ) assume r in PreNorms h1 ; ::_thesis: r <= |.c.| * ||.f.|| then ex t being Element of X st r = ||.(h1 . t).|| ; hence r <= |.c.| * ||.f.|| by A16; ::_thesis: verum end; A19: now__::_thesis:_(_(_c_<>_0c_&_|.c.|_*_||.f.||_<=_||.(c_*_f).||_)_or_(_c_=_0c_&_||.(c_*_f).||_=_|.c.|_*_||.f.||_)_) percases ( c <> 0c or c = 0c ) ; caseA20: c <> 0c ; ::_thesis: |.c.| * ||.f.|| <= ||.(c * f).|| A21: now__::_thesis:_for_t_being_Element_of_X_holds_||.(f1_._t).||_<=_(|.c.|_")_*_||.(c_*_f).|| let t be Element of X; ::_thesis: ||.(f1 . t).|| <= (|.c.| ") * ||.(c * f).|| A22: |.(c ").| = |.(1r / c).| by COMPLEX1:def_4, XCMPLX_1:215 .= 1 / |.c.| by COMPLEX1:48, COMPLEX1:67 .= 1 * (|.c.| ") by XCMPLX_0:def_9 .= |.c.| " ; h1 . t = c * (f1 . t) by Th21; then A23: (c ") * (h1 . t) = ((c ") * c) * (f1 . t) by CLVECT_1:def_4 .= 1r * (f1 . t) by A20, COMPLEX1:def_4, XCMPLX_0:def_7 .= f1 . t by CLVECT_1:def_5 ; ( ||.((c ") * (h1 . t)).|| = |.(c ").| * ||.(h1 . t).|| & 0 <= |.(c ").| ) by CLVECT_1:def_13, COMPLEX1:46; hence ||.(f1 . t).|| <= (|.c.| ") * ||.(c * f).|| by A23, A22, Th17, XREAL_1:64; ::_thesis: verum end; A24: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_f1_holds_ r_<=_(|.c.|_")_*_||.(c_*_f).|| let r be Real; ::_thesis: ( r in PreNorms f1 implies r <= (|.c.| ") * ||.(c * f).|| ) assume r in PreNorms f1 ; ::_thesis: r <= (|.c.| ") * ||.(c * f).|| then ex t being Element of X st r = ||.(f1 . t).|| ; hence r <= (|.c.| ") * ||.(c * f).|| by A21; ::_thesis: verum end; A25: ( ( for s being real number st s in PreNorms f1 holds s <= (|.c.| ") * ||.(c * f).|| ) implies upper_bound (PreNorms f1) <= (|.c.| ") * ||.(c * f).|| ) by SEQ_4:45; A26: 0 <= |.c.| by COMPLEX1:46; (ComplexBoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms f1) by Th15; then ||.f.|| <= (|.c.| ") * ||.(c * f).|| by A24, A25; then |.c.| * ||.f.|| <= |.c.| * ((|.c.| ") * ||.(c * f).||) by A26, XREAL_1:64; then A27: |.c.| * ||.f.|| <= (|.c.| * (|.c.| ")) * ||.(c * f).|| ; |.c.| <> 0 by A20, COMPLEX1:47; then |.c.| * ||.f.|| <= 1 * ||.(c * f).|| by A27, XCMPLX_0:def_7; hence |.c.| * ||.f.|| <= ||.(c * f).|| ; ::_thesis: verum end; caseA28: c = 0c ; ::_thesis: ||.(c * f).|| = |.c.| * ||.f.|| reconsider fz = f as VECTOR of (C_VectorSpace_of_BoundedFunctions (X,Y)) ; c * f = (Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) . [c,f] by CLVECT_1:def_1 .= c * fz by CLVECT_1:def_1 .= 0. (C_VectorSpace_of_BoundedFunctions (X,Y)) by A28, CLVECT_1:1 .= 0. (C_NormSpace_of_BoundedFunctions (X,Y)) ; hence ||.(c * f).|| = |.c.| * ||.f.|| by A28, Th19, COMPLEX1:44; ::_thesis: verum end; end; end; (ComplexBoundedFunctionsNorm (X,Y)) . (c * f) = upper_bound (PreNorms h1) by Th15; then ||.(c * f).|| <= |.c.| * ||.f.|| by A18, A15; hence ||.(c * f).|| = |.c.| * ||.f.|| by A19, XXREAL_0:1; ::_thesis: verum end; now__::_thesis:_(_||.f.||_=_0_implies_f_=_0._(C_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 A29: ||.f.|| = 0 ; ::_thesis: f = 0. (C_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 Th17; then ||.(g . t).|| = 0 by A29, CLVECT_1:105; 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. (C_NormSpace_of_BoundedFunctions (X,Y)) by Th16; ::_thesis: verum end; hence ( ( ||.f.|| = 0 implies f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) ) & ( f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) implies ||.f.|| = 0 ) & ||.(c * f).|| = |.c.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| ) by A1, A14, A9; ::_thesis: verum end; theorem Th23: :: CSSPACE4:23 for X being non empty set for Y being ComplexNormSpace holds ( C_NormSpace_of_BoundedFunctions (X,Y) is reflexive & C_NormSpace_of_BoundedFunctions (X,Y) is discerning & C_NormSpace_of_BoundedFunctions (X,Y) is ComplexNormSpace-like ) proof let X be non empty set ; ::_thesis: for Y being ComplexNormSpace holds ( C_NormSpace_of_BoundedFunctions (X,Y) is reflexive & C_NormSpace_of_BoundedFunctions (X,Y) is discerning & C_NormSpace_of_BoundedFunctions (X,Y) is ComplexNormSpace-like ) let Y be ComplexNormSpace; ::_thesis: ( C_NormSpace_of_BoundedFunctions (X,Y) is reflexive & C_NormSpace_of_BoundedFunctions (X,Y) is discerning & C_NormSpace_of_BoundedFunctions (X,Y) is ComplexNormSpace-like ) thus ||.(0. (C_NormSpace_of_BoundedFunctions (X,Y))).|| = 0 by Th22; :: according to NORMSP_0:def_6 ::_thesis: ( C_NormSpace_of_BoundedFunctions (X,Y) is discerning & C_NormSpace_of_BoundedFunctions (X,Y) is ComplexNormSpace-like ) for x, y being Point of (C_NormSpace_of_BoundedFunctions (X,Y)) for c being Complex holds ( ( ||.x.|| = 0 implies x = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) ) & ( x = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) implies ||.x.|| = 0 ) & ||.(c * x).|| = |.c.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) by Th22; hence ( C_NormSpace_of_BoundedFunctions (X,Y) is discerning & C_NormSpace_of_BoundedFunctions (X,Y) is ComplexNormSpace-like ) by CLVECT_1:def_13, NORMSP_0:def_5; ::_thesis: verum end; theorem Th24: :: CSSPACE4:24 for X being non empty set for Y being ComplexNormSpace holds C_NormSpace_of_BoundedFunctions (X,Y) is ComplexNormSpace proof let X be non empty set ; ::_thesis: for Y being ComplexNormSpace holds C_NormSpace_of_BoundedFunctions (X,Y) is ComplexNormSpace let Y be ComplexNormSpace; ::_thesis: C_NormSpace_of_BoundedFunctions (X,Y) is ComplexNormSpace CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #) is ComplexLinearSpace ; hence C_NormSpace_of_BoundedFunctions (X,Y) is ComplexNormSpace by Th23, CSSPACE3:2; ::_thesis: verum end; registration let X be non empty set ; let Y be ComplexNormSpace; cluster C_NormSpace_of_BoundedFunctions (X,Y) -> non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ; coherence ( C_NormSpace_of_BoundedFunctions (X,Y) is reflexive & C_NormSpace_of_BoundedFunctions (X,Y) is discerning & C_NormSpace_of_BoundedFunctions (X,Y) is ComplexNormSpace-like & C_NormSpace_of_BoundedFunctions (X,Y) is vector-distributive & C_NormSpace_of_BoundedFunctions (X,Y) is scalar-distributive & C_NormSpace_of_BoundedFunctions (X,Y) is scalar-associative & C_NormSpace_of_BoundedFunctions (X,Y) is scalar-unital & C_NormSpace_of_BoundedFunctions (X,Y) is Abelian & C_NormSpace_of_BoundedFunctions (X,Y) is add-associative & C_NormSpace_of_BoundedFunctions (X,Y) is right_zeroed & C_NormSpace_of_BoundedFunctions (X,Y) is right_complementable ) by Th24; end; theorem Th25: :: CSSPACE4:25 for X being non empty set for Y being ComplexNormSpace for f, g, h being Point of (C_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 ComplexNormSpace for f, g, h being Point of (C_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 ComplexNormSpace; ::_thesis: for f, g, h being Point of (C_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 (C_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, Th20; then f - g = h + (g - g) by RLVECT_1:def_3; then f - g = h + (0. (C_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. (C_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, Th20; 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; Lm12: 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 Th26: :: CSSPACE4:26 for X being non empty set for Y being ComplexNormSpace st Y is complete holds for seq being sequence of (C_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 ComplexNormSpace st Y is complete holds for seq being sequence of (C_NormSpace_of_BoundedFunctions (X,Y)) st seq is Cauchy_sequence_by_Norm holds seq is convergent let Y be ComplexNormSpace; ::_thesis: ( Y is complete implies for seq being sequence of (C_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 (C_NormSpace_of_BoundedFunctions (X,Y)) st seq is Cauchy_sequence_by_Norm holds seq is convergent let vseq be sequence of (C_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 Th14; 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 Th14; ( 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, Th25; hence ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| by Th17; ::_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, CSSPACE3: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 CSSPACE3:8; then xseq is convergent by A1, CLOPBAN1:def_13; 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, CSSPACE3: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 CLVECT_1:110, NORMSP_0:def_4; 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 CSSPACE4: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 Th14, Th17; ::_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, CLOPBAN1:40; 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 by CLVECT_1:105; 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, CSSPACE3: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 Th14; 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 Th14; ( 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, Th25; hence ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| by Th17; ::_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, CLVECT_1:115, CLVECT_1:121; then A35: lim rseq = ||.((tseq . x) - (xseq . n)).|| by A33, CLOPBAN1:19; 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 CLVECT_1:108 ; hence rseq . m <= e by A30, A36; ::_thesis: verum end; then lim rseq <= e by A34, A33, Lm12, CLOPBAN1:19; hence ||.((xseq . n) - (tseq . x)).|| <= e by A35, CLVECT_1:108; ::_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 (C_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 Th14; then ||.(h1 . t).|| = ||.(((modetrans ((vseq . n),X,Y)) . t) - (tseq . t)).|| by Th25; 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; A42: ( ( for s being real number st s in PreNorms h1 holds s <= e ) implies upper_bound (PreNorms h1) <= e ) by SEQ_4:45; (ComplexBoundedFunctionsNorm (X,Y)) . ((vseq . n) - tv) = upper_bound (PreNorms h1) by Th15; hence ||.((vseq . n) - tv).|| <= e by A41, A42; ::_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 A43: 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 A44: for n being Element of NAT st n >= m holds ||.((vseq . n) - tv).|| <= e / 2 by A37, A43; A45: e / 2 < e by A43, 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 A44; hence ||.((vseq . n) - tv).|| < e by A45, 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 CLVECT_1:def_15; ::_thesis: verum end; theorem Th27: :: CSSPACE4:27 for X being non empty set for Y being ComplexBanachSpace holds C_NormSpace_of_BoundedFunctions (X,Y) is ComplexBanachSpace proof let X be non empty set ; ::_thesis: for Y being ComplexBanachSpace holds C_NormSpace_of_BoundedFunctions (X,Y) is ComplexBanachSpace let Y be ComplexBanachSpace; ::_thesis: C_NormSpace_of_BoundedFunctions (X,Y) is ComplexBanachSpace for seq being sequence of (C_NormSpace_of_BoundedFunctions (X,Y)) st seq is Cauchy_sequence_by_Norm holds seq is convergent by Th26; hence C_NormSpace_of_BoundedFunctions (X,Y) is ComplexBanachSpace by CLOPBAN1:def_13; ::_thesis: verum end; registration let X be non empty set ; let Y be ComplexBanachSpace; cluster C_NormSpace_of_BoundedFunctions (X,Y) -> non empty complete ; coherence C_NormSpace_of_BoundedFunctions (X,Y) is complete by Th27; end; begin theorem :: CSSPACE4:28 for seq1, seq2 being Complex_Sequence st seq1 is bounded & seq2 is bounded holds seq1 + seq2 is bounded by Lm3; theorem :: CSSPACE4:29 for c being Complex for seq being Complex_Sequence st seq is bounded holds c (#) seq is bounded by Lm4; theorem :: CSSPACE4:30 for seq being Complex_Sequence holds ( seq is bounded iff |.seq.| is bounded ) by Lm8, Lm9; theorem :: CSSPACE4:31 for seq1, seq2, seq3 being Complex_Sequence holds ( seq1 = seq2 - seq3 iff for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) ) by Lm11;