:: CLVECT_3 semantic presentation begin deffunc H1( ComplexUnitarySpace) -> Element of the U1 of \$1 = 0. \$1; theorem Th1: :: CLVECT_3:1 for X being ComplexUnitarySpace for seq1, seq2 being sequence of X holds (Partial_Sums seq1) + (Partial_Sums seq2) = Partial_Sums (seq1 + seq2) proof let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X holds (Partial_Sums seq1) + (Partial_Sums seq2) = Partial_Sums (seq1 + seq2) let seq1, seq2 be sequence of X; ::_thesis: (Partial_Sums seq1) + (Partial_Sums seq2) = Partial_Sums (seq1 + seq2) set PSseq1 = Partial_Sums seq1; set PSseq2 = Partial_Sums seq2; A1: now__::_thesis:_for_n_being_Element_of_NAT_holds_((Partial_Sums_seq1)_+_(Partial_Sums_seq2))_._(n_+_1)_=_(((Partial_Sums_seq1)_+_(Partial_Sums_seq2))_._n)_+_((seq1_+_seq2)_._(n_+_1)) let n be Element of NAT ; ::_thesis: ((Partial_Sums seq1) + (Partial_Sums seq2)) . (n + 1) = (((Partial_Sums seq1) + (Partial_Sums seq2)) . n) + ((seq1 + seq2) . (n + 1)) thus ((Partial_Sums seq1) + (Partial_Sums seq2)) . (n + 1) = ((Partial_Sums seq1) . (n + 1)) + ((Partial_Sums seq2) . (n + 1)) by NORMSP_1:def_2 .= (((Partial_Sums seq1) . n) + (seq1 . (n + 1))) + ((Partial_Sums seq2) . (n + 1)) by BHSP_4:def_1 .= (((Partial_Sums seq1) . n) + (seq1 . (n + 1))) + ((seq2 . (n + 1)) + ((Partial_Sums seq2) . n)) by BHSP_4:def_1 .= ((((Partial_Sums seq1) . n) + (seq1 . (n + 1))) + (seq2 . (n + 1))) + ((Partial_Sums seq2) . n) by RLVECT_1:def_3 .= (((Partial_Sums seq1) . n) + ((seq1 . (n + 1)) + (seq2 . (n + 1)))) + ((Partial_Sums seq2) . n) by RLVECT_1:def_3 .= (((Partial_Sums seq1) . n) + ((seq1 + seq2) . (n + 1))) + ((Partial_Sums seq2) . n) by NORMSP_1:def_2 .= (((Partial_Sums seq1) . n) + ((Partial_Sums seq2) . n)) + ((seq1 + seq2) . (n + 1)) by RLVECT_1:def_3 .= (((Partial_Sums seq1) + (Partial_Sums seq2)) . n) + ((seq1 + seq2) . (n + 1)) by NORMSP_1:def_2 ; ::_thesis: verum end; ((Partial_Sums seq1) + (Partial_Sums seq2)) . 0 = ((Partial_Sums seq1) . 0) + ((Partial_Sums seq2) . 0) by NORMSP_1:def_2 .= (seq1 . 0) + ((Partial_Sums seq2) . 0) by BHSP_4:def_1 .= (seq1 . 0) + (seq2 . 0) by BHSP_4:def_1 .= (seq1 + seq2) . 0 by NORMSP_1:def_2 ; hence (Partial_Sums seq1) + (Partial_Sums seq2) = Partial_Sums (seq1 + seq2) by A1, BHSP_4:def_1; ::_thesis: verum end; theorem Th2: :: CLVECT_3:2 for X being ComplexUnitarySpace for seq1, seq2 being sequence of X holds (Partial_Sums seq1) - (Partial_Sums seq2) = Partial_Sums (seq1 - seq2) proof let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X holds (Partial_Sums seq1) - (Partial_Sums seq2) = Partial_Sums (seq1 - seq2) let seq1, seq2 be sequence of X; ::_thesis: (Partial_Sums seq1) - (Partial_Sums seq2) = Partial_Sums (seq1 - seq2) set PSseq1 = Partial_Sums seq1; set PSseq2 = Partial_Sums seq2; A1: now__::_thesis:_for_n_being_Element_of_NAT_holds_((Partial_Sums_seq1)_-_(Partial_Sums_seq2))_._(n_+_1)_=_(((Partial_Sums_seq1)_-_(Partial_Sums_seq2))_._n)_+_((seq1_-_seq2)_._(n_+_1)) let n be Element of NAT ; ::_thesis: ((Partial_Sums seq1) - (Partial_Sums seq2)) . (n + 1) = (((Partial_Sums seq1) - (Partial_Sums seq2)) . n) + ((seq1 - seq2) . (n + 1)) thus ((Partial_Sums seq1) - (Partial_Sums seq2)) . (n + 1) = ((Partial_Sums seq1) . (n + 1)) - ((Partial_Sums seq2) . (n + 1)) by NORMSP_1:def_3 .= (((Partial_Sums seq1) . n) + (seq1 . (n + 1))) - ((Partial_Sums seq2) . (n + 1)) by BHSP_4:def_1 .= (((Partial_Sums seq1) . n) + (seq1 . (n + 1))) - ((seq2 . (n + 1)) + ((Partial_Sums seq2) . n)) by BHSP_4:def_1 .= ((((Partial_Sums seq1) . n) + (seq1 . (n + 1))) - (seq2 . (n + 1))) - ((Partial_Sums seq2) . n) by RLVECT_1:27 .= (((Partial_Sums seq1) . n) + ((seq1 . (n + 1)) - (seq2 . (n + 1)))) - ((Partial_Sums seq2) . n) by RLVECT_1:def_3 .= (((Partial_Sums seq1) . n) - ((Partial_Sums seq2) . n)) + ((seq1 . (n + 1)) - (seq2 . (n + 1))) by RLVECT_1:def_3 .= (((Partial_Sums seq1) - (Partial_Sums seq2)) . n) + ((seq1 . (n + 1)) - (seq2 . (n + 1))) by NORMSP_1:def_3 .= (((Partial_Sums seq1) - (Partial_Sums seq2)) . n) + ((seq1 - seq2) . (n + 1)) by NORMSP_1:def_3 ; ::_thesis: verum end; ((Partial_Sums seq1) - (Partial_Sums seq2)) . 0 = ((Partial_Sums seq1) . 0) - ((Partial_Sums seq2) . 0) by NORMSP_1:def_3 .= (seq1 . 0) - ((Partial_Sums seq2) . 0) by BHSP_4:def_1 .= (seq1 . 0) - (seq2 . 0) by BHSP_4:def_1 .= (seq1 - seq2) . 0 by NORMSP_1:def_3 ; hence (Partial_Sums seq1) - (Partial_Sums seq2) = Partial_Sums (seq1 - seq2) by A1, BHSP_4:def_1; ::_thesis: verum end; theorem Th3: :: CLVECT_3:3 for X being ComplexUnitarySpace for seq being sequence of X for z being Complex holds Partial_Sums (z * seq) = z * (Partial_Sums seq) proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X for z being Complex holds Partial_Sums (z * seq) = z * (Partial_Sums seq) let seq be sequence of X; ::_thesis: for z being Complex holds Partial_Sums (z * seq) = z * (Partial_Sums seq) let z be Complex; ::_thesis: Partial_Sums (z * seq) = z * (Partial_Sums seq) set PSseq = Partial_Sums seq; A1: now__::_thesis:_for_n_being_Element_of_NAT_holds_(z_*_(Partial_Sums_seq))_._(n_+_1)_=_((z_*_(Partial_Sums_seq))_._n)_+_((z_*_seq)_._(n_+_1)) let n be Element of NAT ; ::_thesis: (z * (Partial_Sums seq)) . (n + 1) = ((z * (Partial_Sums seq)) . n) + ((z * seq) . (n + 1)) thus (z * (Partial_Sums seq)) . (n + 1) = z * ((Partial_Sums seq) . (n + 1)) by CLVECT_1:def_14 .= z * (((Partial_Sums seq) . n) + (seq . (n + 1))) by BHSP_4:def_1 .= (z * ((Partial_Sums seq) . n)) + (z * (seq . (n + 1))) by CLVECT_1:def_2 .= ((z * (Partial_Sums seq)) . n) + (z * (seq . (n + 1))) by CLVECT_1:def_14 .= ((z * (Partial_Sums seq)) . n) + ((z * seq) . (n + 1)) by CLVECT_1:def_14 ; ::_thesis: verum end; (z * (Partial_Sums seq)) . 0 = z * ((Partial_Sums seq) . 0) by CLVECT_1:def_14 .= z * (seq . 0) by BHSP_4:def_1 .= (z * seq) . 0 by CLVECT_1:def_14 ; hence Partial_Sums (z * seq) = z * (Partial_Sums seq) by A1, BHSP_4:def_1; ::_thesis: verum end; theorem :: CLVECT_3:4 for X being ComplexUnitarySpace for seq being sequence of X holds Partial_Sums (- seq) = - (Partial_Sums seq) proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X holds Partial_Sums (- seq) = - (Partial_Sums seq) let seq be sequence of X; ::_thesis: Partial_Sums (- seq) = - (Partial_Sums seq) Partial_Sums ((- 1r) * seq) = (- 1r) * (Partial_Sums seq) by Th3; then Partial_Sums (- seq) = (- 1r) * (Partial_Sums seq) by CSSPACE:70; hence Partial_Sums (- seq) = - (Partial_Sums seq) by CSSPACE:70; ::_thesis: verum end; theorem :: CLVECT_3:5 for X being ComplexUnitarySpace for seq1, seq2 being sequence of X for z1, z2 being Complex holds (z1 * (Partial_Sums seq1)) + (z2 * (Partial_Sums seq2)) = Partial_Sums ((z1 * seq1) + (z2 * seq2)) proof let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X for z1, z2 being Complex holds (z1 * (Partial_Sums seq1)) + (z2 * (Partial_Sums seq2)) = Partial_Sums ((z1 * seq1) + (z2 * seq2)) let seq1, seq2 be sequence of X; ::_thesis: for z1, z2 being Complex holds (z1 * (Partial_Sums seq1)) + (z2 * (Partial_Sums seq2)) = Partial_Sums ((z1 * seq1) + (z2 * seq2)) let z1, z2 be Complex; ::_thesis: (z1 * (Partial_Sums seq1)) + (z2 * (Partial_Sums seq2)) = Partial_Sums ((z1 * seq1) + (z2 * seq2)) thus (z1 * (Partial_Sums seq1)) + (z2 * (Partial_Sums seq2)) = (Partial_Sums (z1 * seq1)) + (z2 * (Partial_Sums seq2)) by Th3 .= (Partial_Sums (z1 * seq1)) + (Partial_Sums (z2 * seq2)) by Th3 .= Partial_Sums ((z1 * seq1) + (z2 * seq2)) by Th1 ; ::_thesis: verum end; definition let X be ComplexUnitarySpace; let seq be sequence of X; attrseq is summable means :Def1: :: CLVECT_3:def 1 Partial_Sums seq is convergent ; func Sum seq -> Point of X equals :: CLVECT_3:def 2 lim (Partial_Sums seq); correctness coherence lim (Partial_Sums seq) is Point of X; ; end; :: deftheorem Def1 defines summable CLVECT_3:def_1_:_ for X being ComplexUnitarySpace for seq being sequence of X holds ( seq is summable iff Partial_Sums seq is convergent ); :: deftheorem defines Sum CLVECT_3:def_2_:_ for X being ComplexUnitarySpace for seq being sequence of X holds Sum seq = lim (Partial_Sums seq); theorem :: CLVECT_3:6 for X being ComplexUnitarySpace for seq1, seq2 being sequence of X st seq1 is summable & seq2 is summable holds ( seq1 + seq2 is summable & Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) ) proof let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X st seq1 is summable & seq2 is summable holds ( seq1 + seq2 is summable & Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) ) let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is summable & seq2 is summable implies ( seq1 + seq2 is summable & Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) ) ) assume ( seq1 is summable & seq2 is summable ) ; ::_thesis: ( seq1 + seq2 is summable & Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) ) then A1: ( Partial_Sums seq1 is convergent & Partial_Sums seq2 is convergent ) by Def1; then (Partial_Sums seq1) + (Partial_Sums seq2) is convergent by CLVECT_2:3; then Partial_Sums (seq1 + seq2) is convergent by Th1; hence seq1 + seq2 is summable by Def1; ::_thesis: Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) thus Sum (seq1 + seq2) = lim ((Partial_Sums seq1) + (Partial_Sums seq2)) by Th1 .= (Sum seq1) + (Sum seq2) by A1, CLVECT_2:13 ; ::_thesis: verum end; theorem :: CLVECT_3:7 for X being ComplexUnitarySpace for seq1, seq2 being sequence of X st seq1 is summable & seq2 is summable holds ( seq1 - seq2 is summable & Sum (seq1 - seq2) = (Sum seq1) - (Sum seq2) ) proof let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X st seq1 is summable & seq2 is summable holds ( seq1 - seq2 is summable & Sum (seq1 - seq2) = (Sum seq1) - (Sum seq2) ) let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is summable & seq2 is summable implies ( seq1 - seq2 is summable & Sum (seq1 - seq2) = (Sum seq1) - (Sum seq2) ) ) assume ( seq1 is summable & seq2 is summable ) ; ::_thesis: ( seq1 - seq2 is summable & Sum (seq1 - seq2) = (Sum seq1) - (Sum seq2) ) then A1: ( Partial_Sums seq1 is convergent & Partial_Sums seq2 is convergent ) by Def1; then (Partial_Sums seq1) - (Partial_Sums seq2) is convergent by CLVECT_2:4; then Partial_Sums (seq1 - seq2) is convergent by Th2; hence seq1 - seq2 is summable by Def1; ::_thesis: Sum (seq1 - seq2) = (Sum seq1) - (Sum seq2) thus Sum (seq1 - seq2) = lim ((Partial_Sums seq1) - (Partial_Sums seq2)) by Th2 .= (Sum seq1) - (Sum seq2) by A1, CLVECT_2:14 ; ::_thesis: verum end; theorem :: CLVECT_3:8 for X being ComplexUnitarySpace for seq being sequence of X for z being Complex st seq is summable holds ( z * seq is summable & Sum (z * seq) = z * (Sum seq) ) proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X for z being Complex st seq is summable holds ( z * seq is summable & Sum (z * seq) = z * (Sum seq) ) let seq be sequence of X; ::_thesis: for z being Complex st seq is summable holds ( z * seq is summable & Sum (z * seq) = z * (Sum seq) ) let z be Complex; ::_thesis: ( seq is summable implies ( z * seq is summable & Sum (z * seq) = z * (Sum seq) ) ) assume seq is summable ; ::_thesis: ( z * seq is summable & Sum (z * seq) = z * (Sum seq) ) then A1: Partial_Sums seq is convergent by Def1; then z * (Partial_Sums seq) is convergent by CLVECT_2:5; then Partial_Sums (z * seq) is convergent by Th3; hence z * seq is summable by Def1; ::_thesis: Sum (z * seq) = z * (Sum seq) thus Sum (z * seq) = lim (z * (Partial_Sums seq)) by Th3 .= z * (Sum seq) by A1, CLVECT_2:15 ; ::_thesis: verum end; theorem Th9: :: CLVECT_3:9 for X being ComplexUnitarySpace for seq being sequence of X st seq is summable holds ( seq is convergent & lim seq = 0. X ) proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X st seq is summable holds ( seq is convergent & lim seq = 0. X ) let seq be sequence of X; ::_thesis: ( seq is summable implies ( seq is convergent & lim seq = 0. X ) ) set PSseq = Partial_Sums seq; now__::_thesis:_for_n_being_Element_of_NAT_holds_((Partial_Sums_seq)_^\_1)_._n_=_((Partial_Sums_seq)_._n)_+_((seq_^\_1)_._n) let n be Element of NAT ; ::_thesis: ((Partial_Sums seq) ^\ 1) . n = ((Partial_Sums seq) . n) + ((seq ^\ 1) . n) (Partial_Sums seq) . (n + 1) = ((Partial_Sums seq) . n) + (seq . (n + 1)) by BHSP_4:def_1 .= ((Partial_Sums seq) . n) + ((seq ^\ 1) . n) by NAT_1:def_3 ; hence ((Partial_Sums seq) ^\ 1) . n = ((Partial_Sums seq) . n) + ((seq ^\ 1) . n) by NAT_1:def_3; ::_thesis: verum end; then A1: (Partial_Sums seq) ^\ 1 = (Partial_Sums seq) + (seq ^\ 1) by NORMSP_1:def_2; now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq_^\_1)_+_((Partial_Sums_seq)_-_(Partial_Sums_seq)))_._n_=_(seq_^\_1)_._n let n be Element of NAT ; ::_thesis: ((seq ^\ 1) + ((Partial_Sums seq) - (Partial_Sums seq))) . n = (seq ^\ 1) . n thus ((seq ^\ 1) + ((Partial_Sums seq) - (Partial_Sums seq))) . n = ((seq ^\ 1) . n) + (((Partial_Sums seq) - (Partial_Sums seq)) . n) by NORMSP_1:def_2 .= ((seq ^\ 1) . n) + (((Partial_Sums seq) . n) - ((Partial_Sums seq) . n)) by NORMSP_1:def_3 .= ((seq ^\ 1) . n) + H1(X) by RLVECT_1:15 .= (seq ^\ 1) . n by RLVECT_1:4 ; ::_thesis: verum end; then (seq ^\ 1) + ((Partial_Sums seq) - (Partial_Sums seq)) = seq ^\ 1 by FUNCT_2:63; then A2: seq ^\ 1 = ((Partial_Sums seq) ^\ 1) - (Partial_Sums seq) by A1, CSSPACE:76; assume seq is summable ; ::_thesis: ( seq is convergent & lim seq = 0. X ) then A3: Partial_Sums seq is convergent by Def1; then A4: (Partial_Sums seq) ^\ 1 is convergent by CLVECT_2:90; then A5: seq ^\ 1 is convergent by A3, A2, CLVECT_2:4; hence seq is convergent by CLVECT_2:91; ::_thesis: lim seq = 0. X lim ((Partial_Sums seq) ^\ 1) = lim (Partial_Sums seq) by A3, CLVECT_2:90; then lim (((Partial_Sums seq) ^\ 1) - (Partial_Sums seq)) = (lim (Partial_Sums seq)) - (lim (Partial_Sums seq)) by A3, A4, CLVECT_2:14 .= H1(X) by RLVECT_1:15 ; hence lim seq = 0. X by A2, A5, CLVECT_2:84, CLVECT_2:91; ::_thesis: verum end; theorem Th10: :: CLVECT_3:10 for X being ComplexHilbertSpace for seq being sequence of X holds ( seq is summable iff for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r ) proof let X be ComplexHilbertSpace; ::_thesis: for seq being sequence of X holds ( seq is summable iff for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r ) let seq be sequence of X; ::_thesis: ( seq is summable iff for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r ) set PSseq = Partial_Sums seq; thus ( seq is summable implies for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r ) ::_thesis: ( ( for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r ) implies seq is summable ) proof assume seq is summable ; ::_thesis: for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r then Partial_Sums seq is convergent by Def1; then Partial_Sums seq is Cauchy by CLVECT_2:65; hence for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r by CLVECT_2:58; ::_thesis: verum end; thus ( ( for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r ) implies seq is summable ) ::_thesis: verum proof assume for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r ; ::_thesis: seq is summable then Partial_Sums seq is Cauchy by CLVECT_2:58; then Partial_Sums seq is convergent by CLVECT_2:def_11; hence seq is summable by Def1; ::_thesis: verum end; end; theorem :: CLVECT_3:11 for X being ComplexUnitarySpace for seq being sequence of X st seq is summable holds Partial_Sums seq is bounded proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X st seq is summable holds Partial_Sums seq is bounded let seq be sequence of X; ::_thesis: ( seq is summable implies Partial_Sums seq is bounded ) assume seq is summable ; ::_thesis: Partial_Sums seq is bounded then Partial_Sums seq is convergent by Def1; hence Partial_Sums seq is bounded by CLVECT_2:80; ::_thesis: verum end; theorem Th12: :: CLVECT_3:12 for X being ComplexUnitarySpace for seq1, seq being sequence of X st ( for n being Element of NAT holds seq1 . n = seq . 0 ) holds Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1 proof let X be ComplexUnitarySpace; ::_thesis: for seq1, seq being sequence of X st ( for n being Element of NAT holds seq1 . n = seq . 0 ) holds Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1 let seq1, seq be sequence of X; ::_thesis: ( ( for n being Element of NAT holds seq1 . n = seq . 0 ) implies Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1 ) assume A1: for n being Element of NAT holds seq1 . n = seq . 0 ; ::_thesis: Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1 A2: now__::_thesis:_for_n_being_Element_of_NAT_holds_(((Partial_Sums_seq)_^\_1)_-_seq1)_._(n_+_1)_=_((((Partial_Sums_seq)_^\_1)_-_seq1)_._n)_+_((seq_^\_1)_._(n_+_1)) let n be Element of NAT ; ::_thesis: (((Partial_Sums seq) ^\ 1) - seq1) . (n + 1) = ((((Partial_Sums seq) ^\ 1) - seq1) . n) + ((seq ^\ 1) . (n + 1)) thus (((Partial_Sums seq) ^\ 1) - seq1) . (n + 1) = (((Partial_Sums seq) ^\ 1) . (n + 1)) - (seq1 . (n + 1)) by NORMSP_1:def_3 .= (((Partial_Sums seq) ^\ 1) . (n + 1)) - (seq . 0) by A1 .= ((Partial_Sums seq) . ((n + 1) + 1)) - (seq . 0) by NAT_1:def_3 .= ((seq . ((n + 1) + 1)) + ((Partial_Sums seq) . (n + 1))) - (seq . 0) by BHSP_4:def_1 .= ((seq . ((n + 1) + 1)) + ((Partial_Sums seq) . (n + 1))) - (seq1 . n) by A1 .= (seq . ((n + 1) + 1)) + (((Partial_Sums seq) . (n + 1)) - (seq1 . n)) by RLVECT_1:def_3 .= (seq . ((n + 1) + 1)) + ((((Partial_Sums seq) ^\ 1) . n) - (seq1 . n)) by NAT_1:def_3 .= (seq . ((n + 1) + 1)) + ((((Partial_Sums seq) ^\ 1) - seq1) . n) by NORMSP_1:def_3 .= ((((Partial_Sums seq) ^\ 1) - seq1) . n) + ((seq ^\ 1) . (n + 1)) by NAT_1:def_3 ; ::_thesis: verum end; (((Partial_Sums seq) ^\ 1) - seq1) . 0 = (((Partial_Sums seq) ^\ 1) . 0) - (seq1 . 0) by NORMSP_1:def_3 .= (((Partial_Sums seq) ^\ 1) . 0) - (seq . 0) by A1 .= ((Partial_Sums seq) . (0 + 1)) - (seq . 0) by NAT_1:def_3 .= (((Partial_Sums seq) . 0) + (seq . (0 + 1))) - (seq . 0) by BHSP_4:def_1 .= ((seq . (0 + 1)) + (seq . 0)) - (seq . 0) by BHSP_4:def_1 .= (seq . (0 + 1)) + ((seq . 0) - (seq . 0)) by RLVECT_1:def_3 .= (seq . (0 + 1)) + H1(X) by RLVECT_1:15 .= seq . (0 + 1) by RLVECT_1:4 .= (seq ^\ 1) . 0 by NAT_1:def_3 ; hence Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1 by A2, BHSP_4:def_1; ::_thesis: verum end; theorem Th13: :: CLVECT_3:13 for X being ComplexUnitarySpace for seq being sequence of X st seq is summable holds for k being Element of NAT holds seq ^\ k is summable proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X st seq is summable holds for k being Element of NAT holds seq ^\ k is summable let seq be sequence of X; ::_thesis: ( seq is summable implies for k being Element of NAT holds seq ^\ k is summable ) defpred S1[ Element of NAT ] means seq ^\ \$1 is summable ; A1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) reconsider seq1 = NAT --> ((seq ^\ k) . 0) as sequence of X ; assume seq ^\ k is summable ; ::_thesis: S1[k + 1] then Partial_Sums (seq ^\ k) is convergent by Def1; then A2: (Partial_Sums (seq ^\ k)) ^\ 1 is convergent by CLVECT_2:90; for m being Element of NAT holds seq1 . m = (seq ^\ k) . 0 by FUNCOP_1:7; then ( seq1 is convergent & Partial_Sums ((seq ^\ k) ^\ 1) = ((Partial_Sums (seq ^\ k)) ^\ 1) - seq1 ) by Th12, CLVECT_2:1; then ( seq ^\ (k + 1) = (seq ^\ k) ^\ 1 & Partial_Sums ((seq ^\ k) ^\ 1) is convergent ) by A2, CLVECT_2:4, NAT_1:48; hence S1[k + 1] by Def1; ::_thesis: verum end; assume seq is summable ; ::_thesis: for k being Element of NAT holds seq ^\ k is summable then A3: S1[ 0 ] by NAT_1:47; thus for k being Element of NAT holds S1[k] from NAT_1:sch_1(A3, A1); ::_thesis: verum end; theorem :: CLVECT_3:14 for X being ComplexUnitarySpace for seq being sequence of X st ex k being Element of NAT st seq ^\ k is summable holds seq is summable proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X st ex k being Element of NAT st seq ^\ k is summable holds seq is summable let seq be sequence of X; ::_thesis: ( ex k being Element of NAT st seq ^\ k is summable implies seq is summable ) given k being Element of NAT such that A1: seq ^\ k is summable ; ::_thesis: seq is summable (seq ^\ k) ^\ 1 is summable by A1, Th13; then A2: Partial_Sums ((seq ^\ k) ^\ 1) is convergent by Def1; reconsider seq1 = NAT --> ((Partial_Sums seq) . k) as sequence of X ; defpred S1[ Element of NAT ] means ((Partial_Sums seq) ^\ (k + 1)) . \$1 = ((Partial_Sums (seq ^\ (k + 1))) . \$1) + (seq1 . \$1); A3: (Partial_Sums (seq ^\ (k + 1))) . 0 = (seq ^\ (k + 1)) . 0 by BHSP_4:def_1 .= seq . (0 + (k + 1)) by NAT_1:def_3 .= seq . (k + 1) ; A4: now__::_thesis:_for_m_being_Element_of_NAT_st_S1[m]_holds_ S1[m_+_1] let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] ) assume A5: S1[m] ; ::_thesis: S1[m + 1] ((Partial_Sums (seq ^\ (k + 1))) . (m + 1)) + (seq1 . (m + 1)) = (seq1 . (m + 1)) + (((Partial_Sums (seq ^\ (k + 1))) . m) + ((seq ^\ (k + 1)) . (m + 1))) by BHSP_4:def_1 .= ((seq1 . (m + 1)) + ((Partial_Sums (seq ^\ (k + 1))) . m)) + ((seq ^\ (k + 1)) . (m + 1)) by RLVECT_1:def_3 .= (((Partial_Sums seq) . k) + ((Partial_Sums (seq ^\ (k + 1))) . m)) + ((seq ^\ (k + 1)) . (m + 1)) by FUNCOP_1:7 .= (((Partial_Sums seq) ^\ (k + 1)) . m) + ((seq ^\ (k + 1)) . (m + 1)) by A5, FUNCOP_1:7 .= ((Partial_Sums seq) . (m + (k + 1))) + ((seq ^\ (k + 1)) . (m + 1)) by NAT_1:def_3 .= ((Partial_Sums seq) . (m + (k + 1))) + (seq . ((m + 1) + (k + 1))) by NAT_1:def_3 .= (Partial_Sums seq) . ((m + (k + 1)) + 1) by BHSP_4:def_1 .= (Partial_Sums seq) . ((m + 1) + (k + 1)) .= ((Partial_Sums seq) ^\ (k + 1)) . (m + 1) by NAT_1:def_3 ; hence S1[m + 1] ; ::_thesis: verum end; ((Partial_Sums seq) ^\ (k + 1)) . 0 = (Partial_Sums seq) . (0 + (k + 1)) by NAT_1:def_3 .= ((Partial_Sums seq) . k) + (seq . (k + 1)) by BHSP_4:def_1 .= ((Partial_Sums (seq ^\ (k + 1))) . 0) + (seq1 . 0) by A3, FUNCOP_1:7 ; then A6: S1[ 0 ] ; for m being Element of NAT holds S1[m] from NAT_1:sch_1(A6, A4); then A7: (Partial_Sums seq) ^\ (k + 1) = (Partial_Sums (seq ^\ (k + 1))) + seq1 by NORMSP_1:def_2 .= (Partial_Sums ((seq ^\ k) ^\ 1)) + seq1 by NAT_1:48 ; seq1 is convergent by CLVECT_2:1; then (Partial_Sums seq) ^\ (k + 1) is convergent by A2, A7, CLVECT_2:3; then Partial_Sums seq is convergent by CLVECT_2:91; hence seq is summable by Def1; ::_thesis: verum end; definition let X be ComplexUnitarySpace; let seq be sequence of X; let n be Element of NAT ; func Sum (seq,n) -> Point of X equals :: CLVECT_3:def 3 (Partial_Sums seq) . n; correctness coherence (Partial_Sums seq) . n is Point of X; ; end; :: deftheorem defines Sum CLVECT_3:def_3_:_ for X being ComplexUnitarySpace for seq being sequence of X for n being Element of NAT holds Sum (seq,n) = (Partial_Sums seq) . n; theorem :: CLVECT_3:15 for X being ComplexUnitarySpace for seq being sequence of X holds Sum (seq,0) = seq . 0 by BHSP_4:def_1; theorem Th16: :: CLVECT_3:16 for X being ComplexUnitarySpace for seq being sequence of X holds Sum (seq,1) = (Sum (seq,0)) + (seq . 1) proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X holds Sum (seq,1) = (Sum (seq,0)) + (seq . 1) let seq be sequence of X; ::_thesis: Sum (seq,1) = (Sum (seq,0)) + (seq . 1) (Partial_Sums seq) . 1 = ((Partial_Sums seq) . 0) + (seq . (0 + 1)) by BHSP_4:def_1 .= ((Partial_Sums seq) . 0) + (seq . 1) ; hence Sum (seq,1) = (Sum (seq,0)) + (seq . 1) ; ::_thesis: verum end; theorem Th17: :: CLVECT_3:17 for X being ComplexUnitarySpace for seq being sequence of X holds Sum (seq,1) = (seq . 0) + (seq . 1) proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X holds Sum (seq,1) = (seq . 0) + (seq . 1) let seq be sequence of X; ::_thesis: Sum (seq,1) = (seq . 0) + (seq . 1) thus Sum (seq,1) = (Sum (seq,0)) + (seq . 1) by Th16 .= (seq . 0) + (seq . 1) by BHSP_4:def_1 ; ::_thesis: verum end; theorem :: CLVECT_3:18 for X being ComplexUnitarySpace for seq being sequence of X for n being Element of NAT holds Sum (seq,(n + 1)) = (Sum (seq,n)) + (seq . (n + 1)) by BHSP_4:def_1; theorem Th19: :: CLVECT_3:19 for X being ComplexUnitarySpace for seq being sequence of X for n being Element of NAT holds seq . (n + 1) = (Sum (seq,(n + 1))) - (Sum (seq,n)) proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X for n being Element of NAT holds seq . (n + 1) = (Sum (seq,(n + 1))) - (Sum (seq,n)) let seq be sequence of X; ::_thesis: for n being Element of NAT holds seq . (n + 1) = (Sum (seq,(n + 1))) - (Sum (seq,n)) let n be Element of NAT ; ::_thesis: seq . (n + 1) = (Sum (seq,(n + 1))) - (Sum (seq,n)) thus (Sum (seq,(n + 1))) - (Sum (seq,n)) = ((seq . (n + 1)) + (Sum (seq,n))) - (Sum (seq,n)) by BHSP_4:def_1 .= (seq . (n + 1)) + ((Sum (seq,n)) - (Sum (seq,n))) by RLVECT_1:def_3 .= (seq . (n + 1)) + (0. X) by RLVECT_1:15 .= seq . (n + 1) by RLVECT_1:4 ; ::_thesis: verum end; theorem :: CLVECT_3:20 for X being ComplexUnitarySpace for seq being sequence of X holds seq . 1 = (Sum (seq,1)) - (Sum (seq,0)) proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X holds seq . 1 = (Sum (seq,1)) - (Sum (seq,0)) let seq be sequence of X; ::_thesis: seq . 1 = (Sum (seq,1)) - (Sum (seq,0)) seq . (0 + 1) = (Sum (seq,(0 + 1))) - (Sum (seq,0)) by Th19; hence seq . 1 = (Sum (seq,1)) - (Sum (seq,0)) ; ::_thesis: verum end; definition let X be ComplexUnitarySpace; let seq be sequence of X; let n, m be Element of NAT ; func Sum (seq,n,m) -> Point of X equals :: CLVECT_3:def 4 (Sum (seq,n)) - (Sum (seq,m)); correctness coherence (Sum (seq,n)) - (Sum (seq,m)) is Point of X; ; end; :: deftheorem defines Sum CLVECT_3:def_4_:_ for X being ComplexUnitarySpace for seq being sequence of X for n, m being Element of NAT holds Sum (seq,n,m) = (Sum (seq,n)) - (Sum (seq,m)); theorem :: CLVECT_3:21 for X being ComplexUnitarySpace for seq being sequence of X holds Sum (seq,1,0) = seq . 1 proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X holds Sum (seq,1,0) = seq . 1 let seq be sequence of X; ::_thesis: Sum (seq,1,0) = seq . 1 Sum (seq,1,0) = ((seq . 0) + (seq . 1)) - (Sum (seq,0)) by Th17 .= ((seq . 1) + (seq . 0)) - (seq . 0) by BHSP_4:def_1 .= (seq . 1) + ((seq . 0) - (seq . 0)) by RLVECT_1:def_3 .= (seq . 1) + H1(X) by RLVECT_1:15 ; hence Sum (seq,1,0) = seq . 1 by RLVECT_1:4; ::_thesis: verum end; theorem :: CLVECT_3:22 for X being ComplexUnitarySpace for seq being sequence of X for n being Element of NAT holds Sum (seq,(n + 1),n) = seq . (n + 1) by Th19; theorem Th23: :: CLVECT_3:23 for X being ComplexHilbertSpace for seq being sequence of X holds ( seq is summable iff for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.((Sum (seq,n)) - (Sum (seq,m))).|| < r ) proof let X be ComplexHilbertSpace; ::_thesis: for seq being sequence of X holds ( seq is summable iff for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.((Sum (seq,n)) - (Sum (seq,m))).|| < r ) let seq be sequence of X; ::_thesis: ( seq is summable iff for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.((Sum (seq,n)) - (Sum (seq,m))).|| < r ) thus ( seq is summable implies for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.((Sum (seq,n)) - (Sum (seq,m))).|| < r ) ::_thesis: ( ( for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.((Sum (seq,n)) - (Sum (seq,m))).|| < r ) implies seq is summable ) proof assume A1: seq is summable ; ::_thesis: for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.((Sum (seq,n)) - (Sum (seq,m))).|| < r now__::_thesis:_for_r_being_Real_st_r_>_0_holds_ ex_k_being_Element_of_NAT_st_ for_n,_m_being_Element_of_NAT_st_n_>=_k_&_m_>=_k_holds_ ||.((Sum_(seq,n))_-_(Sum_(seq,m))).||_<_r let r be Real; ::_thesis: ( r > 0 implies ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.((Sum (seq,n)) - (Sum (seq,m))).|| < r ) assume r > 0 ; ::_thesis: ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.((Sum (seq,n)) - (Sum (seq,m))).|| < r then consider k being Element of NAT such that A2: for n, m being Element of NAT st n >= k & m >= k holds ||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r by A1, Th10; take k = k; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds ||.((Sum (seq,n)) - (Sum (seq,m))).|| < r let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies ||.((Sum (seq,n)) - (Sum (seq,m))).|| < r ) assume ( n >= k & m >= k ) ; ::_thesis: ||.((Sum (seq,n)) - (Sum (seq,m))).|| < r hence ||.((Sum (seq,n)) - (Sum (seq,m))).|| < r by A2; ::_thesis: verum end; hence for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.((Sum (seq,n)) - (Sum (seq,m))).|| < r ; ::_thesis: verum end; thus ( ( for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.((Sum (seq,n)) - (Sum (seq,m))).|| < r ) implies seq is summable ) ::_thesis: verum proof assume A3: for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.((Sum (seq,n)) - (Sum (seq,m))).|| < r ; ::_thesis: seq is summable now__::_thesis:_for_r_being_Real_st_r_>_0_holds_ ex_k_being_Element_of_NAT_st_ for_n,_m_being_Element_of_NAT_st_n_>=_k_&_m_>=_k_holds_ ||.(((Partial_Sums_seq)_._n)_-_((Partial_Sums_seq)_._m)).||_<_r let r be Real; ::_thesis: ( r > 0 implies ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r ) assume r > 0 ; ::_thesis: ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r then consider k being Element of NAT such that A4: for n, m being Element of NAT st n >= k & m >= k holds ||.((Sum (seq,n)) - (Sum (seq,m))).|| < r by A3; take k = k; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds ||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies ||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r ) assume ( n >= k & m >= k ) ; ::_thesis: ||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r then ||.((Sum (seq,n)) - (Sum (seq,m))).|| < r by A4; hence ||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r ; ::_thesis: verum end; hence seq is summable by Th10; ::_thesis: verum end; end; theorem :: CLVECT_3:24 for X being ComplexHilbertSpace for seq being sequence of X holds ( seq is summable iff for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.(Sum (seq,n,m)).|| < r ) proof let X be ComplexHilbertSpace; ::_thesis: for seq being sequence of X holds ( seq is summable iff for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.(Sum (seq,n,m)).|| < r ) let seq be sequence of X; ::_thesis: ( seq is summable iff for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.(Sum (seq,n,m)).|| < r ) thus ( seq is summable implies for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.(Sum (seq,n,m)).|| < r ) ::_thesis: ( ( for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.(Sum (seq,n,m)).|| < r ) implies seq is summable ) proof assume A1: seq is summable ; ::_thesis: for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.(Sum (seq,n,m)).|| < r now__::_thesis:_for_r_being_Real_st_r_>_0_holds_ ex_k_being_Element_of_NAT_st_ for_n,_m_being_Element_of_NAT_st_n_>=_k_&_m_>=_k_holds_ ||.(Sum_(seq,n,m)).||_<_r let r be Real; ::_thesis: ( r > 0 implies ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.(Sum (seq,n,m)).|| < r ) assume r > 0 ; ::_thesis: ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.(Sum (seq,n,m)).|| < r then consider k being Element of NAT such that A2: for n, m being Element of NAT st n >= k & m >= k holds ||.((Sum (seq,n)) - (Sum (seq,m))).|| < r by A1, Th23; take k = k; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds ||.(Sum (seq,n,m)).|| < r let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies ||.(Sum (seq,n,m)).|| < r ) assume ( n >= k & m >= k ) ; ::_thesis: ||.(Sum (seq,n,m)).|| < r hence ||.(Sum (seq,n,m)).|| < r by A2; ::_thesis: verum end; hence for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.(Sum (seq,n,m)).|| < r ; ::_thesis: verum end; thus ( ( for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.(Sum (seq,n,m)).|| < r ) implies seq is summable ) ::_thesis: verum proof assume A3: for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.(Sum (seq,n,m)).|| < r ; ::_thesis: seq is summable now__::_thesis:_for_r_being_Real_st_r_>_0_holds_ ex_k_being_Element_of_NAT_st_ for_n,_m_being_Element_of_NAT_st_n_>=_k_&_m_>=_k_holds_ ||.((Sum_(seq,n))_-_(Sum_(seq,m))).||_<_r let r be Real; ::_thesis: ( r > 0 implies ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.((Sum (seq,n)) - (Sum (seq,m))).|| < r ) assume r > 0 ; ::_thesis: ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.((Sum (seq,n)) - (Sum (seq,m))).|| < r then consider k being Element of NAT such that A4: for n, m being Element of NAT st n >= k & m >= k holds ||.(Sum (seq,n,m)).|| < r by A3; take k = k; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds ||.((Sum (seq,n)) - (Sum (seq,m))).|| < r let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies ||.((Sum (seq,n)) - (Sum (seq,m))).|| < r ) assume ( n >= k & m >= k ) ; ::_thesis: ||.((Sum (seq,n)) - (Sum (seq,m))).|| < r then ||.(Sum (seq,n,m)).|| < r by A4; hence ||.((Sum (seq,n)) - (Sum (seq,m))).|| < r ; ::_thesis: verum end; hence seq is summable by Th23; ::_thesis: verum end; end; definition let Cseq be Complex_Sequence; let n be Element of NAT ; func Sum (Cseq,n) -> Complex equals :: CLVECT_3:def 5 (Partial_Sums Cseq) . n; correctness coherence (Partial_Sums Cseq) . n is Complex; ; end; :: deftheorem defines Sum CLVECT_3:def_5_:_ for Cseq being Complex_Sequence for n being Element of NAT holds Sum (Cseq,n) = (Partial_Sums Cseq) . n; definition let Cseq be Complex_Sequence; let n, m be Element of NAT ; func Sum (Cseq,n,m) -> Complex equals :: CLVECT_3:def 6 (Sum (Cseq,n)) - (Sum (Cseq,m)); correctness coherence (Sum (Cseq,n)) - (Sum (Cseq,m)) is Complex; ; end; :: deftheorem defines Sum CLVECT_3:def_6_:_ for Cseq being Complex_Sequence for n, m being Element of NAT holds Sum (Cseq,n,m) = (Sum (Cseq,n)) - (Sum (Cseq,m)); definition let X be ComplexUnitarySpace; let seq be sequence of X; attrseq is absolutely_summable means :Def7: :: CLVECT_3:def 7 ||.seq.|| is summable ; end; :: deftheorem Def7 defines absolutely_summable CLVECT_3:def_7_:_ for X being ComplexUnitarySpace for seq being sequence of X holds ( seq is absolutely_summable iff ||.seq.|| is summable ); theorem :: CLVECT_3:25 for X being ComplexUnitarySpace for seq1, seq2 being sequence of X st seq1 is absolutely_summable & seq2 is absolutely_summable holds seq1 + seq2 is absolutely_summable proof let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X st seq1 is absolutely_summable & seq2 is absolutely_summable holds seq1 + seq2 is absolutely_summable let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is absolutely_summable & seq2 is absolutely_summable implies seq1 + seq2 is absolutely_summable ) A1: for n being Element of NAT holds ( ||.(seq1 + seq2).|| . n >= 0 & ||.(seq1 + seq2).|| . n <= (||.seq1.|| + ||.seq2.||) . n ) proof let n be Element of NAT ; ::_thesis: ( ||.(seq1 + seq2).|| . n >= 0 & ||.(seq1 + seq2).|| . n <= (||.seq1.|| + ||.seq2.||) . n ) ||.(seq1 + seq2).|| . n = ||.((seq1 + seq2) . n).|| by CLVECT_2:def_3; hence ||.(seq1 + seq2).|| . n >= 0 by CSSPACE:44; ::_thesis: ||.(seq1 + seq2).|| . n <= (||.seq1.|| + ||.seq2.||) . n ||.(seq1 + seq2).|| . n = ||.((seq1 + seq2) . n).|| by CLVECT_2:def_3 .= ||.((seq1 . n) + (seq2 . n)).|| by NORMSP_1:def_2 ; then ||.(seq1 + seq2).|| . n <= ||.(seq1 . n).|| + ||.(seq2 . n).|| by CSSPACE:46; then ||.(seq1 + seq2).|| . n <= (||.seq1.|| . n) + ||.(seq2 . n).|| by CLVECT_2:def_3; then ||.(seq1 + seq2).|| . n <= (||.seq1.|| . n) + (||.seq2.|| . n) by CLVECT_2:def_3; hence ||.(seq1 + seq2).|| . n <= (||.seq1.|| + ||.seq2.||) . n by SEQ_1:7; ::_thesis: verum end; assume ( seq1 is absolutely_summable & seq2 is absolutely_summable ) ; ::_thesis: seq1 + seq2 is absolutely_summable then ( ||.seq1.|| is summable & ||.seq2.|| is summable ) by Def7; then ||.seq1.|| + ||.seq2.|| is summable by SERIES_1:7; then ||.(seq1 + seq2).|| is summable by A1, SERIES_1:20; hence seq1 + seq2 is absolutely_summable by Def7; ::_thesis: verum end; theorem :: CLVECT_3:26 for X being ComplexUnitarySpace for seq being sequence of X for z being Complex st seq is absolutely_summable holds z * seq is absolutely_summable proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X for z being Complex st seq is absolutely_summable holds z * seq is absolutely_summable let seq be sequence of X; ::_thesis: for z being Complex st seq is absolutely_summable holds z * seq is absolutely_summable let z be Complex; ::_thesis: ( seq is absolutely_summable implies z * seq is absolutely_summable ) A1: for n being Element of NAT holds ( ||.(z * seq).|| . n >= 0 & ||.(z * seq).|| . n <= (|.z.| (#) ||.seq.||) . n ) proof let n be Element of NAT ; ::_thesis: ( ||.(z * seq).|| . n >= 0 & ||.(z * seq).|| . n <= (|.z.| (#) ||.seq.||) . n ) ||.(z * seq).|| . n = ||.((z * seq) . n).|| by CLVECT_2:def_3; hence ||.(z * seq).|| . n >= 0 by CSSPACE:44; ::_thesis: ||.(z * seq).|| . n <= (|.z.| (#) ||.seq.||) . n ||.(z * seq).|| . n = ||.((z * seq) . n).|| by CLVECT_2:def_3 .= ||.(z * (seq . n)).|| by CLVECT_1:def_14 .= |.z.| * ||.(seq . n).|| by CSSPACE:43 .= |.z.| * (||.seq.|| . n) by CLVECT_2:def_3 .= (|.z.| (#) ||.seq.||) . n by SEQ_1:9 ; hence ||.(z * seq).|| . n <= (|.z.| (#) ||.seq.||) . n ; ::_thesis: verum end; assume seq is absolutely_summable ; ::_thesis: z * seq is absolutely_summable then ||.seq.|| is summable by Def7; then |.z.| (#) ||.seq.|| is summable by SERIES_1:10; then ||.(z * seq).|| is summable by A1, SERIES_1:20; hence z * seq is absolutely_summable by Def7; ::_thesis: verum end; theorem :: CLVECT_3:27 for X being ComplexUnitarySpace for seq being sequence of X for Rseq being Real_Sequence st ( for n being Element of NAT holds ||.seq.|| . n <= Rseq . n ) & Rseq is summable holds seq is absolutely_summable proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X for Rseq being Real_Sequence st ( for n being Element of NAT holds ||.seq.|| . n <= Rseq . n ) & Rseq is summable holds seq is absolutely_summable let seq be sequence of X; ::_thesis: for Rseq being Real_Sequence st ( for n being Element of NAT holds ||.seq.|| . n <= Rseq . n ) & Rseq is summable holds seq is absolutely_summable let Rseq be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds ||.seq.|| . n <= Rseq . n ) & Rseq is summable implies seq is absolutely_summable ) A1: for n being Element of NAT holds ||.seq.|| . n >= 0 proof let n be Element of NAT ; ::_thesis: ||.seq.|| . n >= 0 ||.seq.|| . n = ||.(seq . n).|| by CLVECT_2:def_3; hence ||.seq.|| . n >= 0 by CSSPACE:44; ::_thesis: verum end; assume ( ( for n being Element of NAT holds ||.seq.|| . n <= Rseq . n ) & Rseq is summable ) ; ::_thesis: seq is absolutely_summable then ||.seq.|| is summable by A1, SERIES_1:20; hence seq is absolutely_summable by Def7; ::_thesis: verum end; theorem :: CLVECT_3:28 for X being ComplexUnitarySpace for seq being sequence of X for Rseq being Real_Sequence st ( for n being Element of NAT holds ( seq . n <> 0. X & Rseq . n = ||.(seq . (n + 1)).|| / ||.(seq . n).|| ) ) & Rseq is convergent & lim Rseq < 1 holds seq is absolutely_summable proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X for Rseq being Real_Sequence st ( for n being Element of NAT holds ( seq . n <> 0. X & Rseq . n = ||.(seq . (n + 1)).|| / ||.(seq . n).|| ) ) & Rseq is convergent & lim Rseq < 1 holds seq is absolutely_summable let seq be sequence of X; ::_thesis: for Rseq being Real_Sequence st ( for n being Element of NAT holds ( seq . n <> 0. X & Rseq . n = ||.(seq . (n + 1)).|| / ||.(seq . n).|| ) ) & Rseq is convergent & lim Rseq < 1 holds seq is absolutely_summable let Rseq be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds ( seq . n <> 0. X & Rseq . n = ||.(seq . (n + 1)).|| / ||.(seq . n).|| ) ) & Rseq is convergent & lim Rseq < 1 implies seq is absolutely_summable ) assume that A1: for n being Element of NAT holds ( seq . n <> H1(X) & Rseq . n = ||.(seq . (n + 1)).|| / ||.(seq . n).|| ) and A2: ( Rseq is convergent & lim Rseq < 1 ) ; ::_thesis: seq is absolutely_summable for n being Element of NAT holds ( ||.seq.|| . n > 0 & Rseq . n = (||.seq.|| . (n + 1)) / (||.seq.|| . n) ) proof let n be Element of NAT ; ::_thesis: ( ||.seq.|| . n > 0 & Rseq . n = (||.seq.|| . (n + 1)) / (||.seq.|| . n) ) seq . n <> H1(X) by A1; then A3: ||.(seq . n).|| <> 0 by CSSPACE:42; ||.(seq . n).|| >= 0 by CSSPACE:44; hence ||.seq.|| . n > 0 by A3, CLVECT_2:def_3; ::_thesis: Rseq . n = (||.seq.|| . (n + 1)) / (||.seq.|| . n) Rseq . n = ||.(seq . (n + 1)).|| / ||.(seq . n).|| by A1 .= (||.seq.|| . (n + 1)) / ||.(seq . n).|| by CLVECT_2:def_3 ; hence Rseq . n = (||.seq.|| . (n + 1)) / (||.seq.|| . n) by CLVECT_2:def_3; ::_thesis: verum end; then ||.seq.|| is summable by A2, SERIES_1:26; hence seq is absolutely_summable by Def7; ::_thesis: verum end; theorem Th29: :: CLVECT_3:29 for X being ComplexUnitarySpace for seq being sequence of X for r being Real st r > 0 & ex m being Element of NAT st for n being Element of NAT st n >= m holds ||.(seq . n).|| >= r & seq is convergent holds lim seq <> 0. X proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X for r being Real st r > 0 & ex m being Element of NAT st for n being Element of NAT st n >= m holds ||.(seq . n).|| >= r & seq is convergent holds lim seq <> 0. X let seq be sequence of X; ::_thesis: for r being Real st r > 0 & ex m being Element of NAT st for n being Element of NAT st n >= m holds ||.(seq . n).|| >= r & seq is convergent holds lim seq <> 0. X let r be Real; ::_thesis: ( r > 0 & ex m being Element of NAT st for n being Element of NAT st n >= m holds ||.(seq . n).|| >= r & seq is convergent implies lim seq <> 0. X ) assume A1: r > 0 ; ::_thesis: ( for m being Element of NAT ex n being Element of NAT st ( n >= m & not ||.(seq . n).|| >= r ) or not seq is convergent or lim seq <> 0. X ) given m being Element of NAT such that A2: for n being Element of NAT st n >= m holds ||.(seq . n).|| >= r ; ::_thesis: ( not seq is convergent or lim seq <> 0. X ) now__::_thesis:_(_not_seq_is_convergent_or_lim_seq_<>_0._X_) percases ( not seq is convergent or seq is convergent ) ; suppose not seq is convergent ; ::_thesis: ( not seq is convergent or lim seq <> 0. X ) hence ( not seq is convergent or lim seq <> 0. X ) ; ::_thesis: verum end; supposeA3: seq is convergent ; ::_thesis: ( not seq is convergent or lim seq <> 0. X ) now__::_thesis:_not_lim_seq_=_H1(X) assume lim seq = H1(X) ; ::_thesis: contradiction then consider k being Element of NAT such that A4: for n being Element of NAT st n >= k holds ||.((seq . n) - H1(X)).|| < r by A1, A3, CLVECT_2:19; now__::_thesis:_for_n_being_Element_of_NAT_holds_not_n_>=_m_+_k let n be Element of NAT ; ::_thesis: not n >= m + k assume A5: n >= m + k ; ::_thesis: contradiction m + k >= k by NAT_1:11; then n >= k by A5, XXREAL_0:2; then ||.((seq . n) - H1(X)).|| < r by A4; then A6: ||.(seq . n).|| < r by RLVECT_1:13; m + k >= m by NAT_1:11; then n >= m by A5, XXREAL_0:2; hence contradiction by A2, A6; ::_thesis: verum end; hence contradiction ; ::_thesis: verum end; hence ( not seq is convergent or lim seq <> 0. X ) ; ::_thesis: verum end; end; end; hence ( not seq is convergent or lim seq <> 0. X ) ; ::_thesis: verum end; theorem Th30: :: CLVECT_3:30 for X being ComplexUnitarySpace for seq being sequence of X st ( for n being Element of NAT holds seq . n <> 0. X ) & ex m being Element of NAT st for n being Element of NAT st n >= m holds ||.(seq . (n + 1)).|| / ||.(seq . n).|| >= 1 holds not seq is summable proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X st ( for n being Element of NAT holds seq . n <> 0. X ) & ex m being Element of NAT st for n being Element of NAT st n >= m holds ||.(seq . (n + 1)).|| / ||.(seq . n).|| >= 1 holds not seq is summable let seq be sequence of X; ::_thesis: ( ( for n being Element of NAT holds seq . n <> 0. X ) & ex m being Element of NAT st for n being Element of NAT st n >= m holds ||.(seq . (n + 1)).|| / ||.(seq . n).|| >= 1 implies not seq is summable ) assume A1: for n being Element of NAT holds seq . n <> H1(X) ; ::_thesis: ( for m being Element of NAT ex n being Element of NAT st ( n >= m & not ||.(seq . (n + 1)).|| / ||.(seq . n).|| >= 1 ) or not seq is summable ) given m being Element of NAT such that A2: for n being Element of NAT st n >= m holds ||.(seq . (n + 1)).|| / ||.(seq . n).|| >= 1 ; ::_thesis: not seq is summable A3: now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_m_holds_ ||.(seq_._n).||_>=_||.(seq_._m).|| defpred S1[ Element of NAT ] means ||.(seq . (m + \$1)).|| >= ||.(seq . m).||; let n be Element of NAT ; ::_thesis: ( n >= m implies ||.(seq . n).|| >= ||.(seq . m).|| ) A4: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A5: ||.(seq . (m + k)).|| >= ||.(seq . m).|| ; ::_thesis: S1[k + 1] seq . (m + k) <> H1(X) by A1; then A6: ||.(seq . (m + k)).|| <> 0 by CSSPACE:42; ( ||.(seq . ((m + k) + 1)).|| / ||.(seq . (m + k)).|| >= 1 & ||.(seq . (m + k)).|| >= 0 ) by A2, CSSPACE:44, NAT_1:11; then ||.(seq . ((m + k) + 1)).|| >= ||.(seq . (m + k)).|| by A6, XREAL_1:191; hence S1[k + 1] by A5, XXREAL_0:2; ::_thesis: verum end; A7: S1[ 0 ] ; A8: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A7, A4); assume n >= m ; ::_thesis: ||.(seq . n).|| >= ||.(seq . m).|| then consider k being Nat such that A9: n = m + k by NAT_1:10; k in NAT by ORDINAL1:def_12; hence ||.(seq . n).|| >= ||.(seq . m).|| by A8, A9; ::_thesis: verum end; seq . m <> H1(X) by A1; then ||.(seq . m).|| <> 0 by CSSPACE:42; then ||.(seq . m).|| > 0 by CSSPACE:44; then ( not seq is convergent or lim seq <> H1(X) ) by A3, Th29; hence not seq is summable by Th9; ::_thesis: verum end; theorem :: CLVECT_3:31 for X being ComplexUnitarySpace for seq being sequence of X for Rseq being Real_Sequence st ( for n being Element of NAT holds seq . n <> 0. X ) & ( for n being Element of NAT holds Rseq . n = ||.(seq . (n + 1)).|| / ||.(seq . n).|| ) & Rseq is convergent & lim Rseq > 1 holds not seq is summable proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X for Rseq being Real_Sequence st ( for n being Element of NAT holds seq . n <> 0. X ) & ( for n being Element of NAT holds Rseq . n = ||.(seq . (n + 1)).|| / ||.(seq . n).|| ) & Rseq is convergent & lim Rseq > 1 holds not seq is summable let seq be sequence of X; ::_thesis: for Rseq being Real_Sequence st ( for n being Element of NAT holds seq . n <> 0. X ) & ( for n being Element of NAT holds Rseq . n = ||.(seq . (n + 1)).|| / ||.(seq . n).|| ) & Rseq is convergent & lim Rseq > 1 holds not seq is summable let Rseq be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds seq . n <> 0. X ) & ( for n being Element of NAT holds Rseq . n = ||.(seq . (n + 1)).|| / ||.(seq . n).|| ) & Rseq is convergent & lim Rseq > 1 implies not seq is summable ) assume that A1: for n being Element of NAT holds seq . n <> H1(X) and A2: for n being Element of NAT holds Rseq . n = ||.(seq . (n + 1)).|| / ||.(seq . n).|| and A3: Rseq is convergent and A4: lim Rseq > 1 ; ::_thesis: not seq is summable (lim Rseq) - 1 > 0 by A4, XREAL_1:50; then consider m being Element of NAT such that A5: for n being Element of NAT st n >= m holds abs ((Rseq . n) - (lim Rseq)) < (lim Rseq) - 1 by A3, SEQ_2:def_7; now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_m_+_1_holds_ ||.(seq_._(n_+_1)).||_/_||.(seq_._n).||_>=_1 let n be Element of NAT ; ::_thesis: ( n >= m + 1 implies ||.(seq . (n + 1)).|| / ||.(seq . n).|| >= 1 ) A6: m + 1 >= m by NAT_1:11; A7: Rseq . n = ||.(seq . (n + 1)).|| / ||.(seq . n).|| by A2; assume n >= m + 1 ; ::_thesis: ||.(seq . (n + 1)).|| / ||.(seq . n).|| >= 1 then n >= m by A6, XXREAL_0:2; then abs ((||.(seq . (n + 1)).|| / ||.(seq . n).||) - (lim Rseq)) < (lim Rseq) - 1 by A5, A7; then - ((lim Rseq) - 1) < (||.(seq . (n + 1)).|| / ||.(seq . n).||) - (lim Rseq) by SEQ_2:1; then (1 - (lim Rseq)) + (lim Rseq) < ((||.(seq . (n + 1)).|| / ||.(seq . n).||) - (lim Rseq)) + (lim Rseq) by XREAL_1:6; hence ||.(seq . (n + 1)).|| / ||.(seq . n).|| >= 1 ; ::_thesis: verum end; hence not seq is summable by A1, Th30; ::_thesis: verum end; theorem :: CLVECT_3:32 for X being ComplexUnitarySpace for seq being sequence of X for Rseq being Real_Sequence st ( for n being Element of NAT holds Rseq . n = n -root ||.(seq . n).|| ) & Rseq is convergent & lim Rseq < 1 holds seq is absolutely_summable proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X for Rseq being Real_Sequence st ( for n being Element of NAT holds Rseq . n = n -root ||.(seq . n).|| ) & Rseq is convergent & lim Rseq < 1 holds seq is absolutely_summable let seq be sequence of X; ::_thesis: for Rseq being Real_Sequence st ( for n being Element of NAT holds Rseq . n = n -root ||.(seq . n).|| ) & Rseq is convergent & lim Rseq < 1 holds seq is absolutely_summable let Rseq be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds Rseq . n = n -root ||.(seq . n).|| ) & Rseq is convergent & lim Rseq < 1 implies seq is absolutely_summable ) assume that A1: for n being Element of NAT holds Rseq . n = n -root ||.(seq . n).|| and A2: ( Rseq is convergent & lim Rseq < 1 ) ; ::_thesis: seq is absolutely_summable for n being Element of NAT holds ( ||.seq.|| . n >= 0 & Rseq . n = n -root (||.seq.|| . n) ) proof let n be Element of NAT ; ::_thesis: ( ||.seq.|| . n >= 0 & Rseq . n = n -root (||.seq.|| . n) ) ||.seq.|| . n = ||.(seq . n).|| by CLVECT_2:def_3; hence ||.seq.|| . n >= 0 by CSSPACE:44; ::_thesis: Rseq . n = n -root (||.seq.|| . n) Rseq . n = n -root ||.(seq . n).|| by A1; hence Rseq . n = n -root (||.seq.|| . n) by CLVECT_2:def_3; ::_thesis: verum end; then ||.seq.|| is summable by A2, SERIES_1:28; hence seq is absolutely_summable by Def7; ::_thesis: verum end; theorem :: CLVECT_3:33 for X being ComplexUnitarySpace for seq being sequence of X for Rseq being Real_Sequence st ( for n being Element of NAT holds Rseq . n = n -root (||.seq.|| . n) ) & ex m being Element of NAT st for n being Element of NAT st n >= m holds Rseq . n >= 1 holds not seq is summable proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X for Rseq being Real_Sequence st ( for n being Element of NAT holds Rseq . n = n -root (||.seq.|| . n) ) & ex m being Element of NAT st for n being Element of NAT st n >= m holds Rseq . n >= 1 holds not seq is summable let seq be sequence of X; ::_thesis: for Rseq being Real_Sequence st ( for n being Element of NAT holds Rseq . n = n -root (||.seq.|| . n) ) & ex m being Element of NAT st for n being Element of NAT st n >= m holds Rseq . n >= 1 holds not seq is summable let Rseq be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds Rseq . n = n -root (||.seq.|| . n) ) & ex m being Element of NAT st for n being Element of NAT st n >= m holds Rseq . n >= 1 implies not seq is summable ) assume A1: for n being Element of NAT holds Rseq . n = n -root (||.seq.|| . n) ; ::_thesis: ( for m being Element of NAT ex n being Element of NAT st ( n >= m & not Rseq . n >= 1 ) or not seq is summable ) given m being Element of NAT such that A2: for n being Element of NAT st n >= m holds Rseq . n >= 1 ; ::_thesis: not seq is summable now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_m_+_1_holds_ ||.(seq_._n).||_>=_1 let n be Element of NAT ; ::_thesis: ( n >= m + 1 implies ||.(seq . n).|| >= 1 ) assume A3: n >= m + 1 ; ::_thesis: ||.(seq . n).|| >= 1 m + 1 >= 1 by NAT_1:11; then A4: n >= 1 by A3, XXREAL_0:2; m + 1 >= m by NAT_1:11; then A5: n >= m by A3, XXREAL_0:2; Rseq . n = n -root (||.seq.|| . n) by A1 .= n -root ||.(seq . n).|| by CLVECT_2:def_3 ; then ( ||.(seq . n).|| >= 0 & (n -root ||.(seq . n).||) |^ n >= 1 ) by A2, A5, CSSPACE:44, PREPOWER:11; hence ||.(seq . n).|| >= 1 by A4, POWER:4; ::_thesis: verum end; then ( not seq is convergent or lim seq <> H1(X) ) by Th29; hence not seq is summable by Th9; ::_thesis: verum end; theorem :: CLVECT_3:34 for X being ComplexUnitarySpace for seq being sequence of X for Rseq being Real_Sequence st ( for n being Element of NAT holds Rseq . n = n -root (||.seq.|| . n) ) & Rseq is convergent & lim Rseq > 1 holds not seq is summable proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X for Rseq being Real_Sequence st ( for n being Element of NAT holds Rseq . n = n -root (||.seq.|| . n) ) & Rseq is convergent & lim Rseq > 1 holds not seq is summable let seq be sequence of X; ::_thesis: for Rseq being Real_Sequence st ( for n being Element of NAT holds Rseq . n = n -root (||.seq.|| . n) ) & Rseq is convergent & lim Rseq > 1 holds not seq is summable let Rseq be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds Rseq . n = n -root (||.seq.|| . n) ) & Rseq is convergent & lim Rseq > 1 implies not seq is summable ) assume that A1: for n being Element of NAT holds Rseq . n = n -root (||.seq.|| . n) and A2: Rseq is convergent and A3: lim Rseq > 1 ; ::_thesis: not seq is summable (lim Rseq) - 1 > 0 by A3, XREAL_1:50; then consider m being Element of NAT such that A4: for n being Element of NAT st n >= m holds abs ((Rseq . n) - (lim Rseq)) < (lim Rseq) - 1 by A2, SEQ_2:def_7; now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_m_+_1_holds_ ||.(seq_._n).||_>=_1 let n be Element of NAT ; ::_thesis: ( n >= m + 1 implies ||.(seq . n).|| >= 1 ) assume A5: n >= m + 1 ; ::_thesis: ||.(seq . n).|| >= 1 A6: Rseq . n = n -root (||.seq.|| . n) by A1 .= n -root ||.(seq . n).|| by CLVECT_2:def_3 ; m + 1 >= m by NAT_1:11; then n >= m by A5, XXREAL_0:2; then abs ((n -root ||.(seq . n).||) - (lim Rseq)) < (lim Rseq) - 1 by A4, A6; then - ((lim Rseq) - 1) < (n -root ||.(seq . n).||) - (lim Rseq) by SEQ_2:1; then (1 - (lim Rseq)) + (lim Rseq) < ((n -root ||.(seq . n).||) - (lim Rseq)) + (lim Rseq) by XREAL_1:6; then A7: ( ||.(seq . n).|| >= 0 & (n -root ||.(seq . n).||) |^ n >= 1 ) by CSSPACE:44, PREPOWER:11; m + 1 >= 1 by NAT_1:11; then n >= 1 by A5, XXREAL_0:2; hence ||.(seq . n).|| >= 1 by A7, POWER:4; ::_thesis: verum end; then ( not seq is convergent or lim seq <> H1(X) ) by Th29; hence not seq is summable by Th9; ::_thesis: verum end; theorem Th35: :: CLVECT_3:35 for X being ComplexUnitarySpace for seq being sequence of X holds Partial_Sums ||.seq.|| is non-decreasing proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X holds Partial_Sums ||.seq.|| is non-decreasing let seq be sequence of X; ::_thesis: Partial_Sums ||.seq.|| is non-decreasing now__::_thesis:_for_n_being_Element_of_NAT_holds_(Partial_Sums_||.seq.||)_._n_<=_(Partial_Sums_||.seq.||)_._(n_+_1) let n be Element of NAT ; ::_thesis: (Partial_Sums ||.seq.||) . n <= (Partial_Sums ||.seq.||) . (n + 1) ||.(seq . (n + 1)).|| >= 0 by CSSPACE:44; then ||.seq.|| . (n + 1) >= 0 by CLVECT_2:def_3; then 0 + ((Partial_Sums ||.seq.||) . n) <= (||.seq.|| . (n + 1)) + ((Partial_Sums ||.seq.||) . n) by XREAL_1:6; hence (Partial_Sums ||.seq.||) . n <= (Partial_Sums ||.seq.||) . (n + 1) by SERIES_1:def_1; ::_thesis: verum end; hence Partial_Sums ||.seq.|| is non-decreasing by SEQM_3:def_8; ::_thesis: verum end; theorem :: CLVECT_3:36 for X being ComplexUnitarySpace for seq being sequence of X for n being Element of NAT holds (Partial_Sums ||.seq.||) . n >= 0 proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X for n being Element of NAT holds (Partial_Sums ||.seq.||) . n >= 0 let seq be sequence of X; ::_thesis: for n being Element of NAT holds (Partial_Sums ||.seq.||) . n >= 0 let n be Element of NAT ; ::_thesis: (Partial_Sums ||.seq.||) . n >= 0 ||.(seq . 0).|| >= 0 by CSSPACE:44; then ||.seq.|| . 0 >= 0 by CLVECT_2:def_3; then (Partial_Sums ||.seq.||) . 0 >= 0 by SERIES_1:def_1; hence (Partial_Sums ||.seq.||) . n >= 0 by Th35, SEQM_3:11; ::_thesis: verum end; theorem Th37: :: CLVECT_3:37 for X being ComplexUnitarySpace for seq being sequence of X for n being Element of NAT holds ||.((Partial_Sums seq) . n).|| <= (Partial_Sums ||.seq.||) . n proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X for n being Element of NAT holds ||.((Partial_Sums seq) . n).|| <= (Partial_Sums ||.seq.||) . n let seq be sequence of X; ::_thesis: for n being Element of NAT holds ||.((Partial_Sums seq) . n).|| <= (Partial_Sums ||.seq.||) . n defpred S1[ Element of NAT ] means ||.((Partial_Sums seq) . \$1).|| <= (Partial_Sums ||.seq.||) . \$1; A1: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_ S1[n_+_1] let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) (Partial_Sums seq) . (n + 1) = ((Partial_Sums seq) . n) + (seq . (n + 1)) by BHSP_4:def_1; then A2: ||.((Partial_Sums seq) . (n + 1)).|| <= ||.((Partial_Sums seq) . n).|| + ||.(seq . (n + 1)).|| by CSSPACE:46; assume S1[n] ; ::_thesis: S1[n + 1] then ||.((Partial_Sums seq) . n).|| + ||.(seq . (n + 1)).|| <= ((Partial_Sums ||.seq.||) . n) + ||.(seq . (n + 1)).|| by XREAL_1:6; then ||.((Partial_Sums seq) . (n + 1)).|| <= ((Partial_Sums ||.seq.||) . n) + ||.(seq . (n + 1)).|| by A2, XXREAL_0:2; then ||.((Partial_Sums seq) . (n + 1)).|| <= ((Partial_Sums ||.seq.||) . n) + (||.seq.|| . (n + 1)) by CLVECT_2:def_3; hence S1[n + 1] by SERIES_1:def_1; ::_thesis: verum end; (Partial_Sums ||.seq.||) . 0 = ||.seq.|| . 0 by SERIES_1:def_1 .= ||.(seq . 0).|| by CLVECT_2:def_3 ; then A3: S1[ 0 ] by BHSP_4:def_1; thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1); ::_thesis: verum end; theorem :: CLVECT_3:38 for X being ComplexUnitarySpace for seq being sequence of X for n being Element of NAT holds ||.(Sum (seq,n)).|| <= Sum (||.seq.||,n) proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X for n being Element of NAT holds ||.(Sum (seq,n)).|| <= Sum (||.seq.||,n) let seq be sequence of X; ::_thesis: for n being Element of NAT holds ||.(Sum (seq,n)).|| <= Sum (||.seq.||,n) let n be Element of NAT ; ::_thesis: ||.(Sum (seq,n)).|| <= Sum (||.seq.||,n) ||.((Partial_Sums seq) . n).|| <= (Partial_Sums ||.seq.||) . n by Th37; hence ||.(Sum (seq,n)).|| <= Sum (||.seq.||,n) by SERIES_1:def_5; ::_thesis: verum end; theorem Th39: :: CLVECT_3:39 for X being ComplexUnitarySpace for seq being sequence of X for n, m being Element of NAT holds ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)) proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X for n, m being Element of NAT holds ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)) let seq be sequence of X; ::_thesis: for n, m being Element of NAT holds ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)) let n, m be Element of NAT ; ::_thesis: ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)) A1: now__::_thesis:_(_n_>=_m_implies_||.(((Partial_Sums_seq)_._m)_-_((Partial_Sums_seq)_._n)).||_<=_abs_(((Partial_Sums_||.seq.||)_._m)_-_((Partial_Sums_||.seq.||)_._n))_) reconsider d = n, t = m as Integer ; set PSseq9 = Partial_Sums ||.seq.||; set PSseq = Partial_Sums seq; defpred S1[ Element of NAT ] means ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + \$1))).|| <= abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . (m + \$1))); A2: Partial_Sums ||.seq.|| is non-decreasing by Th35; A3: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ S1[k_+_1] let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) A4: ||.(seq . ((m + k) + 1)).|| >= 0 by CSSPACE:44; A5: abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . (m + (k + 1)))) = abs (- (((Partial_Sums ||.seq.||) . (m + (k + 1))) - ((Partial_Sums ||.seq.||) . m))) .= abs (((Partial_Sums ||.seq.||) . ((m + k) + 1)) - ((Partial_Sums ||.seq.||) . m)) by COMPLEX1:52 .= abs ((((Partial_Sums ||.seq.||) . (m + k)) + (||.seq.|| . ((m + k) + 1))) - ((Partial_Sums ||.seq.||) . m)) by SERIES_1:def_1 .= abs ((||.(seq . ((m + k) + 1)).|| + ((Partial_Sums ||.seq.||) . (m + k))) - ((Partial_Sums ||.seq.||) . m)) by CLVECT_2:def_3 .= abs ((((Partial_Sums ||.seq.||) . (m + k)) - ((Partial_Sums ||.seq.||) . m)) + ||.(seq . ((m + k) + 1)).||) ; ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + (k + 1)))).|| = ||.(((Partial_Sums seq) . m) - (((Partial_Sums seq) . (m + k)) + (seq . ((m + k) + 1)))).|| by BHSP_4:def_1 .= ||.((((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + k))) - (seq . ((m + k) + 1))).|| by RLVECT_1:27 .= ||.((((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + k))) + (- (seq . ((m + k) + 1)))).|| ; then ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + (k + 1)))).|| <= ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + k))).|| + ||.(- (seq . ((m + k) + 1))).|| by CSSPACE:46; then A6: ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + (k + 1)))).|| <= ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + k))).|| + ||.(seq . ((m + k) + 1)).|| by CSSPACE:47; (Partial_Sums ||.seq.||) . (m + k) >= (Partial_Sums ||.seq.||) . m by A2, SEQM_3:5; then A7: ((Partial_Sums ||.seq.||) . (m + k)) - ((Partial_Sums ||.seq.||) . m) >= 0 by XREAL_1:48; assume S1[k] ; ::_thesis: S1[k + 1] then ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + k))).|| + ||.(seq . ((m + k) + 1)).|| <= (abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . (m + k)))) + ||.(seq . ((m + k) + 1)).|| by XREAL_1:6; then ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + (k + 1)))).|| <= (abs (- (((Partial_Sums ||.seq.||) . (m + k)) - ((Partial_Sums ||.seq.||) . m)))) + ||.(seq . ((m + k) + 1)).|| by A6, XXREAL_0:2; then ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + (k + 1)))).|| <= (abs (((Partial_Sums ||.seq.||) . (m + k)) - ((Partial_Sums ||.seq.||) . m))) + ||.(seq . ((m + k) + 1)).|| by COMPLEX1:52; then ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + (k + 1)))).|| <= (((Partial_Sums ||.seq.||) . (m + k)) - ((Partial_Sums ||.seq.||) . m)) + ||.(seq . ((m + k) + 1)).|| by A7, ABSVALUE:def_1; hence S1[k + 1] by A7, A4, A5, ABSVALUE:def_1; ::_thesis: verum end; assume n >= m ; ::_thesis: ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)) then reconsider k = d - t as Element of NAT by INT_1:5; A8: m + k = n ; ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + 0))).|| = ||.H1(X).|| by RLVECT_1:15 .= 0 by CSSPACE:42 ; then A9: S1[ 0 ] by COMPLEX1:46; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A9, A3); hence ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)) by A8; ::_thesis: verum end; now__::_thesis:_(_n_<=_m_implies_||.(((Partial_Sums_seq)_._m)_-_((Partial_Sums_seq)_._n)).||_<=_abs_(((Partial_Sums_||.seq.||)_._m)_-_((Partial_Sums_||.seq.||)_._n))_) reconsider d = n, t = m as Integer ; set PSseq9 = Partial_Sums ||.seq.||; set PSseq = Partial_Sums seq; defpred S1[ Element of NAT ] means ||.(((Partial_Sums seq) . (n + \$1)) - ((Partial_Sums seq) . n)).|| <= abs (((Partial_Sums ||.seq.||) . (n + \$1)) - ((Partial_Sums ||.seq.||) . n)); A10: Partial_Sums ||.seq.|| is non-decreasing by Th35; A11: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ S1[k_+_1] let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) A12: abs (((Partial_Sums ||.seq.||) . (n + (k + 1))) - ((Partial_Sums ||.seq.||) . n)) = abs ((((Partial_Sums ||.seq.||) . (n + k)) + (||.seq.|| . ((n + k) + 1))) - ((Partial_Sums ||.seq.||) . n)) by SERIES_1:def_1 .= abs ((||.(seq . ((n + k) + 1)).|| + ((Partial_Sums ||.seq.||) . (n + k))) - ((Partial_Sums ||.seq.||) . n)) by CLVECT_2:def_3 .= abs (||.(seq . ((n + k) + 1)).|| + (((Partial_Sums ||.seq.||) . (n + k)) - ((Partial_Sums ||.seq.||) . n))) ; ||.(((Partial_Sums seq) . (n + (k + 1))) - ((Partial_Sums seq) . n)).|| = ||.(((seq . ((n + k) + 1)) + ((Partial_Sums seq) . (n + k))) - ((Partial_Sums seq) . n)).|| by BHSP_4:def_1 .= ||.((seq . ((n + k) + 1)) + (((Partial_Sums seq) . (n + k)) - ((Partial_Sums seq) . n))).|| by RLVECT_1:def_3 ; then A13: ||.(((Partial_Sums seq) . (n + (k + 1))) - ((Partial_Sums seq) . n)).|| <= ||.(seq . ((n + k) + 1)).|| + ||.(((Partial_Sums seq) . (n + k)) - ((Partial_Sums seq) . n)).|| by CSSPACE:46; (Partial_Sums ||.seq.||) . (n + k) >= (Partial_Sums ||.seq.||) . n by A10, SEQM_3:5; then A14: ((Partial_Sums ||.seq.||) . (n + k)) - ((Partial_Sums ||.seq.||) . n) >= 0 by XREAL_1:48; assume S1[k] ; ::_thesis: S1[k + 1] then ||.(seq . ((n + k) + 1)).|| + ||.(((Partial_Sums seq) . (n + k)) - ((Partial_Sums seq) . n)).|| <= ||.(seq . ((n + k) + 1)).|| + (abs (((Partial_Sums ||.seq.||) . (n + k)) - ((Partial_Sums ||.seq.||) . n))) by XREAL_1:7; then ||.(((Partial_Sums seq) . (n + (k + 1))) - ((Partial_Sums seq) . n)).|| <= ||.(seq . ((n + k) + 1)).|| + (abs (((Partial_Sums ||.seq.||) . (n + k)) - ((Partial_Sums ||.seq.||) . n))) by A13, XXREAL_0:2; then A15: ||.(((Partial_Sums seq) . (n + (k + 1))) - ((Partial_Sums seq) . n)).|| <= ||.(seq . ((n + k) + 1)).|| + (((Partial_Sums ||.seq.||) . (n + k)) - ((Partial_Sums ||.seq.||) . n)) by A14, ABSVALUE:def_1; ||.(seq . ((n + k) + 1)).|| >= 0 by CSSPACE:44; hence S1[k + 1] by A14, A15, A12, ABSVALUE:def_1; ::_thesis: verum end; assume n <= m ; ::_thesis: ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)) then reconsider k = t - d as Element of NAT by INT_1:5; A16: n + k = m ; ||.(((Partial_Sums seq) . (n + 0)) - ((Partial_Sums seq) . n)).|| = ||.H1(X).|| by RLVECT_1:15 .= 0 by CSSPACE:42 ; then A17: S1[ 0 ] by COMPLEX1:46; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A17, A11); hence ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)) by A16; ::_thesis: verum end; hence ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)) by A1; ::_thesis: verum end; theorem Th40: :: CLVECT_3:40 for X being ComplexUnitarySpace for seq being sequence of X for n, m being Element of NAT holds ||.((Sum (seq,m)) - (Sum (seq,n))).|| <= abs ((Sum (||.seq.||,m)) - (Sum (||.seq.||,n))) proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X for n, m being Element of NAT holds ||.((Sum (seq,m)) - (Sum (seq,n))).|| <= abs ((Sum (||.seq.||,m)) - (Sum (||.seq.||,n))) let seq be sequence of X; ::_thesis: for n, m being Element of NAT holds ||.((Sum (seq,m)) - (Sum (seq,n))).|| <= abs ((Sum (||.seq.||,m)) - (Sum (||.seq.||,n))) let n, m be Element of NAT ; ::_thesis: ||.((Sum (seq,m)) - (Sum (seq,n))).|| <= abs ((Sum (||.seq.||,m)) - (Sum (||.seq.||,n))) ||.((Sum (seq,m)) - ((Partial_Sums seq) . n)).|| <= abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)) by Th39; then ||.((Sum (seq,m)) - (Sum (seq,n))).|| <= abs ((Sum (||.seq.||,m)) - ((Partial_Sums ||.seq.||) . n)) by SERIES_1:def_5; hence ||.((Sum (seq,m)) - (Sum (seq,n))).|| <= abs ((Sum (||.seq.||,m)) - (Sum (||.seq.||,n))) by SERIES_1:def_5; ::_thesis: verum end; theorem :: CLVECT_3:41 for X being ComplexUnitarySpace for seq being sequence of X for n, m being Element of NAT holds ||.(Sum (seq,m,n)).|| <= abs (Sum (||.seq.||,m,n)) proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X for n, m being Element of NAT holds ||.(Sum (seq,m,n)).|| <= abs (Sum (||.seq.||,m,n)) let seq be sequence of X; ::_thesis: for n, m being Element of NAT holds ||.(Sum (seq,m,n)).|| <= abs (Sum (||.seq.||,m,n)) let n, m be Element of NAT ; ::_thesis: ||.(Sum (seq,m,n)).|| <= abs (Sum (||.seq.||,m,n)) ||.((Sum (seq,m)) - (Sum (seq,n))).|| <= abs ((Sum (||.seq.||,m)) - (Sum (||.seq.||,n))) by Th40; hence ||.(Sum (seq,m,n)).|| <= abs (Sum (||.seq.||,m,n)) by SERIES_1:def_6; ::_thesis: verum end; theorem :: CLVECT_3:42 for X being ComplexHilbertSpace for seq being sequence of X st seq is absolutely_summable holds seq is summable proof let X be ComplexHilbertSpace; ::_thesis: for seq being sequence of X st seq is absolutely_summable holds seq is summable let seq be sequence of X; ::_thesis: ( seq is absolutely_summable implies seq is summable ) assume A1: seq is absolutely_summable ; ::_thesis: seq is summable A2: ||.seq.|| is summable by A1, Def7; now__::_thesis:_for_r_being_Real_st_r_>_0_holds_ ex_k_being_Element_of_NAT_st_ for_n,_m_being_Element_of_NAT_st_n_>=_k_&_m_>=_k_holds_ ||.(((Partial_Sums_seq)_._n)_-_((Partial_Sums_seq)_._m)).||_<_r let r be Real; ::_thesis: ( r > 0 implies ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r ) assume r > 0 ; ::_thesis: ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r then r / 2 > 0 ; then consider k being Element of NAT such that A3: for m being Element of NAT st m >= k holds abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . k)) < r / 2 by A2, SERIES_1:21; take k = k; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds ||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r now__::_thesis:_for_m,_n_being_Element_of_NAT_st_m_>=_k_&_n_>=_k_holds_ ||.(((Partial_Sums_seq)_._n)_-_((Partial_Sums_seq)_._m)).||_<_r let m, n be Element of NAT ; ::_thesis: ( m >= k & n >= k implies ||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r ) A4: ||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| <= abs (((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . m)) by Th39; assume ( m >= k & n >= k ) ; ::_thesis: ||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r then ( abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . k)) < r / 2 & abs (((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . k)) < r / 2 ) by A3; then A5: (abs (((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . k))) + (abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . k))) < (r / 2) + (r / 2) by XREAL_1:8; abs (((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . m)) = abs ((((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . k)) - (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . k))) ; then abs (((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . m)) <= (abs (((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . k))) + (abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . k))) by COMPLEX1:57; then abs (((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . m)) < r by A5, XXREAL_0:2; hence ||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r by A4, XXREAL_0:2; ::_thesis: verum end; hence for n, m being Element of NAT st n >= k & m >= k holds ||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r ; ::_thesis: verum end; hence seq is summable by Th10; ::_thesis: verum end; definition let X be ComplexUnitarySpace; let seq be sequence of X; let Cseq be Complex_Sequence; funcCseq * seq -> sequence of X means :Def8: :: CLVECT_3:def 8 for n being Element of NAT holds it . n = (Cseq . n) * (seq . n); existence ex b1 being sequence of X st for n being Element of NAT holds b1 . n = (Cseq . n) * (seq . n) proof deffunc H2( Element of NAT ) -> Element of the U1 of X = (Cseq . \$1) * (seq . \$1); thus ex M being sequence of X st for n being Element of NAT holds M . n = H2(n) from FUNCT_2:sch_4(); ::_thesis: verum end; uniqueness for b1, b2 being sequence of X st ( for n being Element of NAT holds b1 . n = (Cseq . n) * (seq . n) ) & ( for n being Element of NAT holds b2 . n = (Cseq . n) * (seq . n) ) holds b1 = b2 proof let seq1, seq2 be sequence of X; ::_thesis: ( ( for n being Element of NAT holds seq1 . n = (Cseq . n) * (seq . n) ) & ( for n being Element of NAT holds seq2 . n = (Cseq . n) * (seq . n) ) implies seq1 = seq2 ) assume that A1: for n being Element of NAT holds seq1 . n = (Cseq . n) * (seq . n) and A2: for n being Element of NAT holds seq2 . n = (Cseq . n) * (seq . n) ; ::_thesis: seq1 = seq2 now__::_thesis:_for_n_being_Element_of_NAT_holds_seq1_._n_=_seq2_._n let n be Element of NAT ; ::_thesis: seq1 . n = seq2 . n seq1 . n = (Cseq . n) * (seq . n) by A1; hence seq1 . n = seq2 . n by A2; ::_thesis: verum end; hence seq1 = seq2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def8 defines * CLVECT_3:def_8_:_ for X being ComplexUnitarySpace for seq being sequence of X for Cseq being Complex_Sequence for b4 being sequence of X holds ( b4 = Cseq * seq iff for n being Element of NAT holds b4 . n = (Cseq . n) * (seq . n) ); theorem :: CLVECT_3:43 for X being ComplexUnitarySpace for seq1, seq2 being sequence of X for Cseq being Complex_Sequence holds Cseq * (seq1 + seq2) = (Cseq * seq1) + (Cseq * seq2) proof let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X for Cseq being Complex_Sequence holds Cseq * (seq1 + seq2) = (Cseq * seq1) + (Cseq * seq2) let seq1, seq2 be sequence of X; ::_thesis: for Cseq being Complex_Sequence holds Cseq * (seq1 + seq2) = (Cseq * seq1) + (Cseq * seq2) let Cseq be Complex_Sequence; ::_thesis: Cseq * (seq1 + seq2) = (Cseq * seq1) + (Cseq * seq2) now__::_thesis:_for_n_being_Element_of_NAT_holds_(Cseq_*_(seq1_+_seq2))_._n_=_((Cseq_*_seq1)_+_(Cseq_*_seq2))_._n let n be Element of NAT ; ::_thesis: (Cseq * (seq1 + seq2)) . n = ((Cseq * seq1) + (Cseq * seq2)) . n thus (Cseq * (seq1 + seq2)) . n = (Cseq . n) * ((seq1 + seq2) . n) by Def8 .= (Cseq . n) * ((seq1 . n) + (seq2 . n)) by NORMSP_1:def_2 .= ((Cseq . n) * (seq1 . n)) + ((Cseq . n) * (seq2 . n)) by CLVECT_1:def_2 .= ((Cseq * seq1) . n) + ((Cseq . n) * (seq2 . n)) by Def8 .= ((Cseq * seq1) . n) + ((Cseq * seq2) . n) by Def8 .= ((Cseq * seq1) + (Cseq * seq2)) . n by NORMSP_1:def_2 ; ::_thesis: verum end; hence Cseq * (seq1 + seq2) = (Cseq * seq1) + (Cseq * seq2) by FUNCT_2:63; ::_thesis: verum end; theorem :: CLVECT_3:44 for X being ComplexUnitarySpace for seq being sequence of X for Cseq1, Cseq2 being Complex_Sequence holds (Cseq1 + Cseq2) * seq = (Cseq1 * seq) + (Cseq2 * seq) proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X for Cseq1, Cseq2 being Complex_Sequence holds (Cseq1 + Cseq2) * seq = (Cseq1 * seq) + (Cseq2 * seq) let seq be sequence of X; ::_thesis: for Cseq1, Cseq2 being Complex_Sequence holds (Cseq1 + Cseq2) * seq = (Cseq1 * seq) + (Cseq2 * seq) let Cseq1, Cseq2 be Complex_Sequence; ::_thesis: (Cseq1 + Cseq2) * seq = (Cseq1 * seq) + (Cseq2 * seq) now__::_thesis:_for_n_being_Element_of_NAT_holds_((Cseq1_+_Cseq2)_*_seq)_._n_=_((Cseq1_*_seq)_+_(Cseq2_*_seq))_._n let n be Element of NAT ; ::_thesis: ((Cseq1 + Cseq2) * seq) . n = ((Cseq1 * seq) + (Cseq2 * seq)) . n thus ((Cseq1 + Cseq2) * seq) . n = ((Cseq1 + Cseq2) . n) * (seq . n) by Def8 .= ((Cseq1 . n) + (Cseq2 . n)) * (seq . n) by VALUED_1:1 .= ((Cseq1 . n) * (seq . n)) + ((Cseq2 . n) * (seq . n)) by CLVECT_1:def_3 .= ((Cseq1 * seq) . n) + ((Cseq2 . n) * (seq . n)) by Def8 .= ((Cseq1 * seq) . n) + ((Cseq2 * seq) . n) by Def8 .= ((Cseq1 * seq) + (Cseq2 * seq)) . n by NORMSP_1:def_2 ; ::_thesis: verum end; hence (Cseq1 + Cseq2) * seq = (Cseq1 * seq) + (Cseq2 * seq) by FUNCT_2:63; ::_thesis: verum end; theorem :: CLVECT_3:45 for X being ComplexUnitarySpace for seq being sequence of X for Cseq1, Cseq2 being Complex_Sequence holds (Cseq1 (#) Cseq2) * seq = Cseq1 * (Cseq2 * seq) proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X for Cseq1, Cseq2 being Complex_Sequence holds (Cseq1 (#) Cseq2) * seq = Cseq1 * (Cseq2 * seq) let seq be sequence of X; ::_thesis: for Cseq1, Cseq2 being Complex_Sequence holds (Cseq1 (#) Cseq2) * seq = Cseq1 * (Cseq2 * seq) let Cseq1, Cseq2 be Complex_Sequence; ::_thesis: (Cseq1 (#) Cseq2) * seq = Cseq1 * (Cseq2 * seq) now__::_thesis:_for_n_being_Element_of_NAT_holds_((Cseq1_(#)_Cseq2)_*_seq)_._n_=_(Cseq1_*_(Cseq2_*_seq))_._n let n be Element of NAT ; ::_thesis: ((Cseq1 (#) Cseq2) * seq) . n = (Cseq1 * (Cseq2 * seq)) . n thus ((Cseq1 (#) Cseq2) * seq) . n = ((Cseq1 (#) Cseq2) . n) * (seq . n) by Def8 .= ((Cseq1 . n) * (Cseq2 . n)) * (seq . n) by VALUED_1:5 .= (Cseq1 . n) * ((Cseq2 . n) * (seq . n)) by CLVECT_1:def_4 .= (Cseq1 . n) * ((Cseq2 * seq) . n) by Def8 .= (Cseq1 * (Cseq2 * seq)) . n by Def8 ; ::_thesis: verum end; hence (Cseq1 (#) Cseq2) * seq = Cseq1 * (Cseq2 * seq) by FUNCT_2:63; ::_thesis: verum end; theorem Th46: :: CLVECT_3:46 for X being ComplexUnitarySpace for seq being sequence of X for Cseq being Complex_Sequence for z being Complex holds (z (#) Cseq) * seq = z * (Cseq * seq) proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X for Cseq being Complex_Sequence for z being Complex holds (z (#) Cseq) * seq = z * (Cseq * seq) let seq be sequence of X; ::_thesis: for Cseq being Complex_Sequence for z being Complex holds (z (#) Cseq) * seq = z * (Cseq * seq) let Cseq be Complex_Sequence; ::_thesis: for z being Complex holds (z (#) Cseq) * seq = z * (Cseq * seq) let z be Complex; ::_thesis: (z (#) Cseq) * seq = z * (Cseq * seq) now__::_thesis:_for_n_being_Element_of_NAT_holds_((z_(#)_Cseq)_*_seq)_._n_=_(z_*_(Cseq_*_seq))_._n let n be Element of NAT ; ::_thesis: ((z (#) Cseq) * seq) . n = (z * (Cseq * seq)) . n thus ((z (#) Cseq) * seq) . n = ((z (#) Cseq) . n) * (seq . n) by Def8 .= (z * (Cseq . n)) * (seq . n) by VALUED_1:6 .= z * ((Cseq . n) * (seq . n)) by CLVECT_1:def_4 .= z * ((Cseq * seq) . n) by Def8 .= (z * (Cseq * seq)) . n by CLVECT_1:def_14 ; ::_thesis: verum end; hence (z (#) Cseq) * seq = z * (Cseq * seq) by FUNCT_2:63; ::_thesis: verum end; theorem :: CLVECT_3:47 for X being ComplexUnitarySpace for seq being sequence of X for Cseq being Complex_Sequence holds Cseq * (- seq) = (- Cseq) * seq proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X for Cseq being Complex_Sequence holds Cseq * (- seq) = (- Cseq) * seq let seq be sequence of X; ::_thesis: for Cseq being Complex_Sequence holds Cseq * (- seq) = (- Cseq) * seq let Cseq be Complex_Sequence; ::_thesis: Cseq * (- seq) = (- Cseq) * seq now__::_thesis:_for_n_being_Element_of_NAT_holds_(Cseq_*_(-_seq))_._n_=_((-_Cseq)_*_seq)_._n let n be Element of NAT ; ::_thesis: (Cseq * (- seq)) . n = ((- Cseq) * seq) . n thus (Cseq * (- seq)) . n = (Cseq . n) * ((- seq) . n) by Def8 .= (Cseq . n) * (- (seq . n)) by BHSP_1:44 .= (- (Cseq . n)) * (seq . n) by CLVECT_1:6 .= ((- Cseq) . n) * (seq . n) by VALUED_1:8 .= ((- Cseq) * seq) . n by Def8 ; ::_thesis: verum end; hence Cseq * (- seq) = (- Cseq) * seq by FUNCT_2:63; ::_thesis: verum end; theorem Th48: :: CLVECT_3:48 for X being ComplexUnitarySpace for seq being sequence of X for Cseq being Complex_Sequence st Cseq is convergent & seq is convergent holds Cseq * seq is convergent proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X for Cseq being Complex_Sequence st Cseq is convergent & seq is convergent holds Cseq * seq is convergent let seq be sequence of X; ::_thesis: for Cseq being Complex_Sequence st Cseq is convergent & seq is convergent holds Cseq * seq is convergent let Cseq be Complex_Sequence; ::_thesis: ( Cseq is convergent & seq is convergent implies Cseq * seq is convergent ) assume that A1: Cseq is convergent and A2: seq is convergent ; ::_thesis: Cseq * seq is convergent consider p being Element of COMPLEX such that A3: for r being Real st r > 0 holds ex m being Element of NAT st for n being Element of NAT st n >= m holds |.((Cseq . n) - p).| < r by A1, COMSEQ_2:def_5; consider g being Point of X such that A4: for r being Real st r > 0 holds ex m being Element of NAT st for n being Element of NAT st n >= m holds ||.((seq . n) - g).|| < r by A2, CLVECT_2:9; now__::_thesis:_ex_h_being_Element_of_the_U1_of_X_st_ for_r_being_Real_st_r_>_0_holds_ ex_m_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_n_>=_m_holds_ ||.(((Cseq_*_seq)_._n)_-_h).||_<_r take h = p * g; ::_thesis: for r being Real st r > 0 holds ex m being Element of NAT st for n being Element of NAT st n >= m holds ||.(((Cseq * seq) . n) - h).|| < r let r be Real; ::_thesis: ( r > 0 implies ex m being Element of NAT st for n being Element of NAT st n >= m holds ||.(((Cseq * seq) . n) - h).|| < r ) Cseq is bounded by A1; then consider b being Real such that A5: b > 0 and A6: for n being Element of NAT holds |.(Cseq . n).| < b by COMSEQ_2:8; A7: b + ||.g.|| > 0 + 0 by A5, CSSPACE:44, XREAL_1:8; assume A8: r > 0 ; ::_thesis: ex m being Element of NAT st for n being Element of NAT st n >= m holds ||.(((Cseq * seq) . n) - h).|| < r then consider m1 being Element of NAT such that A9: for n being Element of NAT st n >= m1 holds |.((Cseq . n) - p).| < r / (b + ||.g.||) by A3, A7; consider m2 being Element of NAT such that A10: for n being Element of NAT st n >= m2 holds ||.((seq . n) - g).|| < r / (b + ||.g.||) by A4, A7, A8; take m = m1 + m2; ::_thesis: for n being Element of NAT st n >= m holds ||.(((Cseq * seq) . n) - h).|| < r let n be Element of NAT ; ::_thesis: ( n >= m implies ||.(((Cseq * seq) . n) - h).|| < r ) assume A11: n >= m ; ::_thesis: ||.(((Cseq * seq) . n) - h).|| < r m1 + m2 >= m1 by NAT_1:12; then n >= m1 by A11, XXREAL_0:2; then ( ||.g.|| >= 0 & |.((Cseq . n) - p).| <= r / (b + ||.g.||) ) by A9, CSSPACE:44; then A12: ||.g.|| * |.((Cseq . n) - p).| <= ||.g.|| * (r / (b + ||.g.||)) by XREAL_1:64; A13: ( |.(Cseq . n).| >= 0 & ||.((seq . n) - g).|| >= 0 ) by COMPLEX1:46, CSSPACE:44; m >= m2 by NAT_1:12; then n >= m2 by A11, XXREAL_0:2; then A14: ||.((seq . n) - g).|| < r / (b + ||.g.||) by A10; |.(Cseq . n).| < b by A6; then |.(Cseq . n).| * ||.((seq . n) - g).|| < b * (r / (b + ||.g.||)) by A14, A13, XREAL_1:96; then (|.(Cseq . n).| * ||.((seq . n) - g).||) + (||.g.|| * |.((Cseq . n) - p).|) < (b * (r / (b + ||.g.||))) + (||.g.|| * (r / (b + ||.g.||))) by A12, XREAL_1:8; then (|.(Cseq . n).| * ||.((seq . n) - g).||) + (||.g.|| * |.((Cseq . n) - p).|) < ((b * r) / (b + ||.g.||)) + (||.g.|| * (r / (b + ||.g.||))) by XCMPLX_1:74; then (|.(Cseq . n).| * ||.((seq . n) - g).||) + (||.g.|| * |.((Cseq . n) - p).|) < ((b * r) / (b + ||.g.||)) + ((||.g.|| * r) / (b + ||.g.||)) by XCMPLX_1:74; then (|.(Cseq . n).| * ||.((seq . n) - g).||) + (||.g.|| * |.((Cseq . n) - p).|) < ((b * r) + (||.g.|| * r)) / (b + ||.g.||) by XCMPLX_1:62; then (|.(Cseq . n).| * ||.((seq . n) - g).||) + (||.g.|| * |.((Cseq . n) - p).|) < ((b + ||.g.||) * r) / (b + ||.g.||) ; then A15: (|.(Cseq . n).| * ||.((seq . n) - g).||) + (||.g.|| * |.((Cseq . n) - p).|) < r by A7, XCMPLX_1:89; ||.(((Cseq * seq) . n) - (p * g)).|| = ||.(((Cseq . n) * (seq . n)) - (p * g)).|| by Def8 .= ||.((((Cseq . n) * (seq . n)) - (p * g)) + H1(X)).|| by RLVECT_1:4 .= ||.((((Cseq . n) * (seq . n)) - (p * g)) + (((Cseq . n) * g) - ((Cseq . n) * g))).|| by RLVECT_1:15 .= ||.(((Cseq . n) * (seq . n)) - ((p * g) - (((Cseq . n) * g) - ((Cseq . n) * g)))).|| by RLVECT_1:29 .= ||.(((Cseq . n) * (seq . n)) - (((Cseq . n) * g) + ((p * g) - ((Cseq . n) * g)))).|| by RLVECT_1:29 .= ||.((((Cseq . n) * (seq . n)) - ((Cseq . n) * g)) - ((p * g) - ((Cseq . n) * g))).|| by RLVECT_1:27 .= ||.((((Cseq . n) * (seq . n)) - ((Cseq . n) * g)) + (((Cseq . n) * g) - (p * g))).|| by RLVECT_1:33 ; then ||.(((Cseq * seq) . n) - (p * g)).|| <= ||.(((Cseq . n) * (seq . n)) - ((Cseq . n) * g)).|| + ||.(((Cseq . n) * g) - (p * g)).|| by CSSPACE:46; then ||.(((Cseq * seq) . n) - (p * g)).|| <= ||.((Cseq . n) * ((seq . n) - g)).|| + ||.(((Cseq . n) * g) - (p * g)).|| by CLVECT_1:9; then ||.(((Cseq * seq) . n) - (p * g)).|| <= ||.((Cseq . n) * ((seq . n) - g)).|| + ||.(((Cseq . n) - p) * g).|| by CLVECT_1:10; then ||.(((Cseq * seq) . n) - (p * g)).|| <= (|.(Cseq . n).| * ||.((seq . n) - g).||) + ||.(((Cseq . n) - p) * g).|| by CSSPACE:43; then ||.(((Cseq * seq) . n) - (p * g)).|| <= (|.(Cseq . n).| * ||.((seq . n) - g).||) + (||.g.|| * |.((Cseq . n) - p).|) by CSSPACE:43; hence ||.(((Cseq * seq) . n) - h).|| < r by A15, XXREAL_0:2; ::_thesis: verum end; hence Cseq * seq is convergent by CLVECT_2:9; ::_thesis: verum end; theorem :: CLVECT_3:49 for X being ComplexUnitarySpace for seq being sequence of X for Cseq being Complex_Sequence st Cseq is bounded & seq is bounded holds Cseq * seq is bounded proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X for Cseq being Complex_Sequence st Cseq is bounded & seq is bounded holds Cseq * seq is bounded let seq be sequence of X; ::_thesis: for Cseq being Complex_Sequence st Cseq is bounded & seq is bounded holds Cseq * seq is bounded let Cseq be Complex_Sequence; ::_thesis: ( Cseq is bounded & seq is bounded implies Cseq * seq is bounded ) assume that A1: Cseq is bounded and A2: seq is bounded ; ::_thesis: Cseq * seq is bounded consider M1 being Real such that A3: M1 > 0 and A4: for n being Element of NAT holds |.(Cseq . n).| < M1 by A1, COMSEQ_2:8; consider M2 being Real such that A5: M2 > 0 and A6: for n being Element of NAT holds ||.(seq . n).|| <= M2 by A2, CLVECT_2:def_10; now__::_thesis:_ex_M_being_Element_of_REAL_st_ (_M_>_0_&_(_for_n_being_Element_of_NAT_holds_||.((Cseq_*_seq)_._n).||_<=_M_)_) set M = M1 * M2; take M = M1 * M2; ::_thesis: ( M > 0 & ( for n being Element of NAT holds ||.((Cseq * seq) . n).|| <= M ) ) now__::_thesis:_for_n_being_Element_of_NAT_holds_||.((Cseq_*_seq)_._n).||_<=_M let n be Element of NAT ; ::_thesis: ||.((Cseq * seq) . n).|| <= M |.(Cseq . n).| >= 0 by COMPLEX1:46; then A7: |.(Cseq . n).| * ||.(seq . n).|| <= |.(Cseq . n).| * M2 by A6, XREAL_1:64; |.(Cseq . n).| <= M1 by A4; then A8: |.(Cseq . n).| * M2 <= M1 * M2 by A5, XREAL_1:64; ||.((Cseq * seq) . n).|| = ||.((Cseq . n) * (seq . n)).|| by Def8 .= |.(Cseq . n).| * ||.(seq . n).|| by CSSPACE:43 ; hence ||.((Cseq * seq) . n).|| <= M by A7, A8, XXREAL_0:2; ::_thesis: verum end; hence ( M > 0 & ( for n being Element of NAT holds ||.((Cseq * seq) . n).|| <= M ) ) by A3, A5; ::_thesis: verum end; hence Cseq * seq is bounded by CLVECT_2:def_10; ::_thesis: verum end; theorem :: CLVECT_3:50 for X being ComplexUnitarySpace for seq being sequence of X for Cseq being Complex_Sequence st Cseq is convergent & seq is convergent holds ( Cseq * seq is convergent & lim (Cseq * seq) = (lim Cseq) * (lim seq) ) proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X for Cseq being Complex_Sequence st Cseq is convergent & seq is convergent holds ( Cseq * seq is convergent & lim (Cseq * seq) = (lim Cseq) * (lim seq) ) let seq be sequence of X; ::_thesis: for Cseq being Complex_Sequence st Cseq is convergent & seq is convergent holds ( Cseq * seq is convergent & lim (Cseq * seq) = (lim Cseq) * (lim seq) ) let Cseq be Complex_Sequence; ::_thesis: ( Cseq is convergent & seq is convergent implies ( Cseq * seq is convergent & lim (Cseq * seq) = (lim Cseq) * (lim seq) ) ) assume that A1: Cseq is convergent and A2: seq is convergent ; ::_thesis: ( Cseq * seq is convergent & lim (Cseq * seq) = (lim Cseq) * (lim seq) ) Cseq is bounded by A1; then consider b being Real such that A3: b > 0 and A4: for n being Element of NAT holds |.(Cseq . n).| < b by COMSEQ_2:8; A5: b + ||.(lim seq).|| > 0 + 0 by A3, CSSPACE:44, XREAL_1:8; A6: ||.(lim seq).|| >= 0 by CSSPACE:44; A7: now__::_thesis:_for_r_being_Real_st_r_>_0_holds_ ex_m_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_n_>=_m_holds_ dist_(((Cseq_*_seq)_._n),((lim_Cseq)_*_(lim_seq)))_<_r let r be Real; ::_thesis: ( r > 0 implies ex m being Element of NAT st for n being Element of NAT st n >= m holds dist (((Cseq * seq) . n),((lim Cseq) * (lim seq))) < r ) assume r > 0 ; ::_thesis: ex m being Element of NAT st for n being Element of NAT st n >= m holds dist (((Cseq * seq) . n),((lim Cseq) * (lim seq))) < r then A8: r / (b + ||.(lim seq).||) > 0 by A5; then consider m1 being Element of NAT such that A9: for n being Element of NAT st n >= m1 holds |.((Cseq . n) - (lim Cseq)).| < r / (b + ||.(lim seq).||) by A1, COMSEQ_2:def_6; consider m2 being Element of NAT such that A10: for n being Element of NAT st n >= m2 holds dist ((seq . n),(lim seq)) < r / (b + ||.(lim seq).||) by A2, A8, CLVECT_2:def_2; take m = m1 + m2; ::_thesis: for n being Element of NAT st n >= m holds dist (((Cseq * seq) . n),((lim Cseq) * (lim seq))) < r let n be Element of NAT ; ::_thesis: ( n >= m implies dist (((Cseq * seq) . n),((lim Cseq) * (lim seq))) < r ) assume A11: n >= m ; ::_thesis: dist (((Cseq * seq) . n),((lim Cseq) * (lim seq))) < r m1 + m2 >= m1 by NAT_1:12; then n >= m1 by A11, XXREAL_0:2; then |.((Cseq . n) - (lim Cseq)).| <= r / (b + ||.(lim seq).||) by A9; then A12: ||.(lim seq).|| * |.((Cseq . n) - (lim Cseq)).| <= ||.(lim seq).|| * (r / (b + ||.(lim seq).||)) by A6, XREAL_1:64; A13: ||.((seq . n) - (lim seq)).|| >= 0 by CSSPACE:44; m >= m2 by NAT_1:12; then n >= m2 by A11, XXREAL_0:2; then dist ((seq . n),(lim seq)) < r / (b + ||.(lim seq).||) by A10; then A14: ||.((seq . n) - (lim seq)).|| < r / (b + ||.(lim seq).||) by CSSPACE:def_16; ( |.(Cseq . n).| < b & |.(Cseq . n).| >= 0 ) by A4, COMPLEX1:46; then |.(Cseq . n).| * ||.((seq . n) - (lim seq)).|| < b * (r / (b + ||.(lim seq).||)) by A14, A13, XREAL_1:96; then (|.(Cseq . n).| * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * |.((Cseq . n) - (lim Cseq)).|) < (b * (r / (b + ||.(lim seq).||))) + (||.(lim seq).|| * (r / (b + ||.(lim seq).||))) by A12, XREAL_1:8; then (|.(Cseq . n).| * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * |.((Cseq . n) - (lim Cseq)).|) < ((b * r) / (b + ||.(lim seq).||)) + (||.(lim seq).|| * (r / (b + ||.(lim seq).||))) by XCMPLX_1:74; then (|.(Cseq . n).| * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * |.((Cseq . n) - (lim Cseq)).|) < ((b * r) / (b + ||.(lim seq).||)) + ((||.(lim seq).|| * r) / (b + ||.(lim seq).||)) by XCMPLX_1:74; then (|.(Cseq . n).| * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * |.((Cseq . n) - (lim Cseq)).|) < ((b * r) + (||.(lim seq).|| * r)) / (b + ||.(lim seq).||) by XCMPLX_1:62; then (|.(Cseq . n).| * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * |.((Cseq . n) - (lim Cseq)).|) < ((b + ||.(lim seq).||) * r) / (b + ||.(lim seq).||) ; then A15: (|.(Cseq . n).| * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * |.((Cseq . n) - (lim Cseq)).|) < r by A5, XCMPLX_1:89; ||.(((Cseq * seq) . n) - ((lim Cseq) * (lim seq))).|| = ||.(((Cseq . n) * (seq . n)) - ((lim Cseq) * (lim seq))).|| by Def8 .= ||.((((Cseq . n) * (seq . n)) - ((lim Cseq) * (lim seq))) + H1(X)).|| by RLVECT_1:4 .= ||.((((Cseq . n) * (seq . n)) - ((lim Cseq) * (lim seq))) + (((Cseq . n) * (lim seq)) - ((Cseq . n) * (lim seq)))).|| by RLVECT_1:15 .= ||.(((Cseq . n) * (seq . n)) - (((lim Cseq) * (lim seq)) - (((Cseq . n) * (lim seq)) - ((Cseq . n) * (lim seq))))).|| by RLVECT_1:29 .= ||.(((Cseq . n) * (seq . n)) - (((Cseq . n) * (lim seq)) + (((lim Cseq) * (lim seq)) - ((Cseq . n) * (lim seq))))).|| by RLVECT_1:29 .= ||.((((Cseq . n) * (seq . n)) - ((Cseq . n) * (lim seq))) - (((lim Cseq) * (lim seq)) - ((Cseq . n) * (lim seq)))).|| by RLVECT_1:27 .= ||.((((Cseq . n) * (seq . n)) - ((Cseq . n) * (lim seq))) + (((Cseq . n) * (lim seq)) - ((lim Cseq) * (lim seq)))).|| by RLVECT_1:33 ; then ||.(((Cseq * seq) . n) - ((lim Cseq) * (lim seq))).|| <= ||.(((Cseq . n) * (seq . n)) - ((Cseq . n) * (lim seq))).|| + ||.(((Cseq . n) * (lim seq)) - ((lim Cseq) * (lim seq))).|| by CSSPACE:46; then ||.(((Cseq * seq) . n) - ((lim Cseq) * (lim seq))).|| <= ||.((Cseq . n) * ((seq . n) - (lim seq))).|| + ||.(((Cseq . n) * (lim seq)) - ((lim Cseq) * (lim seq))).|| by CLVECT_1:9; then ||.(((Cseq * seq) . n) - ((lim Cseq) * (lim seq))).|| <= ||.((Cseq . n) * ((seq . n) - (lim seq))).|| + ||.(((Cseq . n) - (lim Cseq)) * (lim seq)).|| by CLVECT_1:10; then ||.(((Cseq * seq) . n) - ((lim Cseq) * (lim seq))).|| <= (|.(Cseq . n).| * ||.((seq . n) - (lim seq)).||) + ||.(((Cseq . n) - (lim Cseq)) * (lim seq)).|| by CSSPACE:43; then ||.(((Cseq * seq) . n) - ((lim Cseq) * (lim seq))).|| <= (|.(Cseq . n).| * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * |.((Cseq . n) - (lim Cseq)).|) by CSSPACE:43; then ||.(((Cseq * seq) . n) - ((lim Cseq) * (lim seq))).|| < r by A15, XXREAL_0:2; hence dist (((Cseq * seq) . n),((lim Cseq) * (lim seq))) < r by CSSPACE:def_16; ::_thesis: verum end; Cseq * seq is convergent by A1, A2, Th48; hence ( Cseq * seq is convergent & lim (Cseq * seq) = (lim Cseq) * (lim seq) ) by A7, CLVECT_2:def_2; ::_thesis: verum end; definition let Cseq be Complex_Sequence; attrCseq is Cauchy means :Def9: :: CLVECT_3:def 9 for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds |.((Cseq . n) - (Cseq . m)).| < r; end; :: deftheorem Def9 defines Cauchy CLVECT_3:def_9_:_ for Cseq being Complex_Sequence holds ( Cseq is Cauchy iff for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds |.((Cseq . n) - (Cseq . m)).| < r ); theorem :: CLVECT_3:51 for Cseq being Complex_Sequence for X being ComplexHilbertSpace for seq being sequence of X st seq is Cauchy & Cseq is Cauchy holds Cseq * seq is Cauchy proof let Cseq be Complex_Sequence; ::_thesis: for X being ComplexHilbertSpace for seq being sequence of X st seq is Cauchy & Cseq is Cauchy holds Cseq * seq is Cauchy let X be ComplexHilbertSpace; ::_thesis: for seq being sequence of X st seq is Cauchy & Cseq is Cauchy holds Cseq * seq is Cauchy let seq be sequence of X; ::_thesis: ( seq is Cauchy & Cseq is Cauchy implies Cseq * seq is Cauchy ) assume that A1: seq is Cauchy and A2: Cseq is Cauchy ; ::_thesis: Cseq * seq is Cauchy now__::_thesis:_for_r_being_Real_st_r_>_0_holds_ ex_k_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_n_>=_k_holds_ |.((Cseq_._n)_-_(Cseq_._k)).|_<_r let r be Real; ::_thesis: ( r > 0 implies ex k being Element of NAT st for n being Element of NAT st n >= k holds |.((Cseq . n) - (Cseq . k)).| < r ) assume r > 0 ; ::_thesis: ex k being Element of NAT st for n being Element of NAT st n >= k holds |.((Cseq . n) - (Cseq . k)).| < r then consider k being Element of NAT such that A3: for n, m being Element of NAT st n >= k & m >= k holds |.((Cseq . n) - (Cseq . m)).| < r by A2, Def9; take k = k; ::_thesis: for n being Element of NAT st n >= k holds |.((Cseq . n) - (Cseq . k)).| < r thus for n being Element of NAT st n >= k holds |.((Cseq . n) - (Cseq . k)).| < r by A3; ::_thesis: verum end; then A4: Cseq is convergent by COMSEQ_3:46; seq is convergent by A1, CLVECT_2:def_11; hence Cseq * seq is Cauchy by A4, Th48, CLVECT_2:65; ::_thesis: verum end; theorem Th52: :: CLVECT_3:52 for X being ComplexUnitarySpace for seq being sequence of X for Cseq being Complex_Sequence for n being Element of NAT holds (Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n = ((Partial_Sums (Cseq * seq)) . (n + 1)) - ((Cseq * (Partial_Sums seq)) . (n + 1)) proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X for Cseq being Complex_Sequence for n being Element of NAT holds (Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n = ((Partial_Sums (Cseq * seq)) . (n + 1)) - ((Cseq * (Partial_Sums seq)) . (n + 1)) let seq be sequence of X; ::_thesis: for Cseq being Complex_Sequence for n being Element of NAT holds (Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n = ((Partial_Sums (Cseq * seq)) . (n + 1)) - ((Cseq * (Partial_Sums seq)) . (n + 1)) let Cseq be Complex_Sequence; ::_thesis: for n being Element of NAT holds (Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n = ((Partial_Sums (Cseq * seq)) . (n + 1)) - ((Cseq * (Partial_Sums seq)) . (n + 1)) defpred S1[ Element of NAT ] means (Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . \$1 = ((Partial_Sums (Cseq * seq)) . (\$1 + 1)) - ((Cseq * (Partial_Sums seq)) . (\$1 + 1)); A1: (Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . 0 = ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq)) . 0 by BHSP_4:def_1 .= ((Cseq - (Cseq ^\ 1)) . 0) * ((Partial_Sums seq) . 0) by Def8 .= ((Cseq + (- (Cseq ^\ 1))) . 0) * (seq . 0) by BHSP_4:def_1 .= ((Cseq . 0) + ((- (Cseq ^\ 1)) . 0)) * (seq . 0) by VALUED_1:1 .= ((Cseq . 0) + (- ((Cseq ^\ 1) . 0))) * (seq . 0) by VALUED_1:8 .= ((Cseq . 0) - ((Cseq ^\ 1) . 0)) * (seq . 0) .= ((Cseq . 0) - (Cseq . (0 + 1))) * (seq . 0) by NAT_1:def_3 .= ((Cseq . 0) * (seq . 0)) - ((Cseq . 1) * (seq . 0)) by CLVECT_1:10 ; A2: (Cseq * (Partial_Sums seq)) . (0 + 1) = (Cseq . (0 + 1)) * ((Partial_Sums seq) . (0 + 1)) by Def8 .= (Cseq . (0 + 1)) * (((Partial_Sums seq) . 0) + (seq . (0 + 1))) by BHSP_4:def_1 .= (Cseq . 1) * ((seq . 0) + (seq . 1)) by BHSP_4:def_1 .= ((Cseq . 1) * (seq . 0)) + ((Cseq . 1) * (seq . 1)) by CLVECT_1:def_2 ; A3: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_ S1[n_+_1] let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume S1[n] ; ::_thesis: S1[n + 1] then ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + ((Cseq * (Partial_Sums seq)) . (n + 1)) = ((Partial_Sums (Cseq * seq)) . (n + 1)) - (((Cseq * (Partial_Sums seq)) . (n + 1)) - ((Cseq * (Partial_Sums seq)) . (n + 1))) by RLVECT_1:29; then A4: ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + ((Cseq * (Partial_Sums seq)) . (n + 1)) = ((Partial_Sums (Cseq * seq)) . (n + 1)) - H1(X) by RLVECT_1:15; (Partial_Sums (Cseq * seq)) . ((n + 1) + 1) = ((Partial_Sums (Cseq * seq)) . (n + 1)) + ((Cseq * seq) . ((n + 1) + 1)) by BHSP_4:def_1 .= (((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + ((Cseq * (Partial_Sums seq)) . (n + 1))) + ((Cseq * seq) . ((n + 1) + 1)) by A4, RLVECT_1:13 .= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + (((Cseq * (Partial_Sums seq)) . (n + 1)) + ((Cseq * seq) . ((n + 1) + 1))) by RLVECT_1:def_3 .= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + (((Cseq . (n + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Cseq * seq) . ((n + 1) + 1))) by Def8 .= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + (((((Cseq . (n + 1)) - (Cseq . ((n + 1) + 1))) + (Cseq . ((n + 1) + 1))) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by Def8 .= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + (((((Cseq . (n + 1)) - (Cseq . ((n + 1) + 1))) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1)))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by CLVECT_1:def_3 .= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + (((((Cseq . (n + 1)) - ((Cseq ^\ 1) . (n + 1))) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1)))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by NAT_1:def_3 .= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + (((((Cseq . (n + 1)) + (- ((Cseq ^\ 1) . (n + 1)))) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1)))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) .= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + (((((Cseq . (n + 1)) + ((- (Cseq ^\ 1)) . (n + 1))) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1)))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by VALUED_1:8 .= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + (((((Cseq - (Cseq ^\ 1)) . (n + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1)))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by VALUED_1:1 .= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + ((((Cseq - (Cseq ^\ 1)) . (n + 1)) * ((Partial_Sums seq) . (n + 1))) + (((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1))))) by RLVECT_1:def_3 .= (((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + (((Cseq - (Cseq ^\ 1)) . (n + 1)) * ((Partial_Sums seq) . (n + 1)))) + (((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by RLVECT_1:def_3 .= (((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + (((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq)) . (n + 1))) + (((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by Def8 .= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . (n + 1)) + (((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by BHSP_4:def_1 .= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . (n + 1)) + ((Cseq . ((n + 1) + 1)) * (((Partial_Sums seq) . (n + 1)) + (seq . ((n + 1) + 1)))) by CLVECT_1:def_2 .= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . (n + 1)) + ((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . ((n + 1) + 1))) by BHSP_4:def_1 .= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . (n + 1)) + ((Cseq * (Partial_Sums seq)) . ((n + 1) + 1)) by Def8 ; then ((Partial_Sums (Cseq * seq)) . ((n + 1) + 1)) - ((Cseq * (Partial_Sums seq)) . ((n + 1) + 1)) = ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . (n + 1)) + (((Cseq * (Partial_Sums seq)) . ((n + 1) + 1)) - ((Cseq * (Partial_Sums seq)) . ((n + 1) + 1))) by RLVECT_1:def_3; then ((Partial_Sums (Cseq * seq)) . ((n + 1) + 1)) - ((Cseq * (Partial_Sums seq)) . ((n + 1) + 1)) = ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . (n + 1)) + H1(X) by RLVECT_1:15; hence S1[n + 1] by RLVECT_1:4; ::_thesis: verum end; (Partial_Sums (Cseq * seq)) . (0 + 1) = ((Partial_Sums (Cseq * seq)) . 0) + ((Cseq * seq) . (0 + 1)) by BHSP_4:def_1 .= ((Cseq * seq) . 0) + ((Cseq * seq) . 1) by BHSP_4:def_1 .= ((Cseq . 0) * (seq . 0)) + ((Cseq * seq) . 1) by Def8 .= ((Cseq . 0) * (seq . 0)) + ((Cseq . 1) * (seq . 1)) by Def8 ; then (Partial_Sums (Cseq * seq)) . (0 + 1) = (((Cseq . 0) * (seq . 0)) + H1(X)) + ((Cseq . 1) * (seq . 1)) by RLVECT_1:4 .= (((Cseq . 0) * (seq . 0)) + (((Cseq . 1) * (seq . 0)) - ((Cseq . 1) * (seq . 0)))) + ((Cseq . 1) * (seq . 1)) by RLVECT_1:15 .= ((((Cseq . 0) * (seq . 0)) + (- ((Cseq . 1) * (seq . 0)))) + ((Cseq . 1) * (seq . 0))) + ((Cseq . 1) * (seq . 1)) by RLVECT_1:def_3 .= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . 0) + ((Cseq * (Partial_Sums seq)) . (0 + 1)) by A1, A2, RLVECT_1:def_3 ; then ((Partial_Sums (Cseq * seq)) . (0 + 1)) - ((Cseq * (Partial_Sums seq)) . (0 + 1)) = ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . 0) + (((Cseq * (Partial_Sums seq)) . (0 + 1)) - ((Cseq * (Partial_Sums seq)) . (0 + 1))) by RLVECT_1:def_3; then ((Partial_Sums (Cseq * seq)) . (0 + 1)) - ((Cseq * (Partial_Sums seq)) . (0 + 1)) = ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . 0) + H1(X) by RLVECT_1:15; then A5: S1[ 0 ] by RLVECT_1:4; thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A5, A3); ::_thesis: verum end; theorem Th53: :: CLVECT_3:53 for X being ComplexUnitarySpace for seq being sequence of X for Cseq being Complex_Sequence for n being Element of NAT holds (Partial_Sums (Cseq * seq)) . (n + 1) = ((Cseq * (Partial_Sums seq)) . (n + 1)) - ((Partial_Sums (((Cseq ^\ 1) - Cseq) * (Partial_Sums seq))) . n) proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X for Cseq being Complex_Sequence for n being Element of NAT holds (Partial_Sums (Cseq * seq)) . (n + 1) = ((Cseq * (Partial_Sums seq)) . (n + 1)) - ((Partial_Sums (((Cseq ^\ 1) - Cseq) * (Partial_Sums seq))) . n) let seq be sequence of X; ::_thesis: for Cseq being Complex_Sequence for n being Element of NAT holds (Partial_Sums (Cseq * seq)) . (n + 1) = ((Cseq * (Partial_Sums seq)) . (n + 1)) - ((Partial_Sums (((Cseq ^\ 1) - Cseq) * (Partial_Sums seq))) . n) let Cseq be Complex_Sequence; ::_thesis: for n being Element of NAT holds (Partial_Sums (Cseq * seq)) . (n + 1) = ((Cseq * (Partial_Sums seq)) . (n + 1)) - ((Partial_Sums (((Cseq ^\ 1) - Cseq) * (Partial_Sums seq))) . n) let n be Element of NAT ; ::_thesis: (Partial_Sums (Cseq * seq)) . (n + 1) = ((Cseq * (Partial_Sums seq)) . (n + 1)) - ((Partial_Sums (((Cseq ^\ 1) - Cseq) * (Partial_Sums seq))) . n) ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + ((Cseq * (Partial_Sums seq)) . (n + 1)) = (((Partial_Sums (Cseq * seq)) . (n + 1)) - ((Cseq * (Partial_Sums seq)) . (n + 1))) + ((Cseq * (Partial_Sums seq)) . (n + 1)) by Th52; then ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + ((Cseq * (Partial_Sums seq)) . (n + 1)) = ((Partial_Sums (Cseq * seq)) . (n + 1)) - (((Cseq * (Partial_Sums seq)) . (n + 1)) - ((Cseq * (Partial_Sums seq)) . (n + 1))) by RLVECT_1:29; then ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + ((Cseq * (Partial_Sums seq)) . (n + 1)) = ((Partial_Sums (Cseq * seq)) . (n + 1)) - H1(X) by RLVECT_1:15; then (Partial_Sums (Cseq * seq)) . (n + 1) = ((Cseq * (Partial_Sums seq)) . (n + 1)) + ((Partial_Sums ((Cseq + (- (Cseq ^\ 1))) * (Partial_Sums seq))) . n) by RLVECT_1:13; then (Partial_Sums (Cseq * seq)) . (n + 1) = ((Cseq * (Partial_Sums seq)) . (n + 1)) + ((Partial_Sums ((((- 1r) (#) (Cseq ^\ 1)) - (- Cseq)) * (Partial_Sums seq))) . n) by COMSEQ_1:11; then (Partial_Sums (Cseq * seq)) . (n + 1) = ((Cseq * (Partial_Sums seq)) . (n + 1)) + ((Partial_Sums ((((- 1r) (#) (Cseq ^\ 1)) - ((- 1r) (#) Cseq)) * (Partial_Sums seq))) . n) by COMSEQ_1:11; then (Partial_Sums (Cseq * seq)) . (n + 1) = ((Cseq * (Partial_Sums seq)) . (n + 1)) + ((Partial_Sums (((- 1r) (#) ((Cseq ^\ 1) - Cseq)) * (Partial_Sums seq))) . n) by COMSEQ_1:18; then (Partial_Sums (Cseq * seq)) . (n + 1) = ((Cseq * (Partial_Sums seq)) . (n + 1)) + ((Partial_Sums ((- 1r) * (((Cseq ^\ 1) - Cseq) * (Partial_Sums seq)))) . n) by Th46; then (Partial_Sums (Cseq * seq)) . (n + 1) = ((Cseq * (Partial_Sums seq)) . (n + 1)) + (((- 1r) * (Partial_Sums (((Cseq ^\ 1) - Cseq) * (Partial_Sums seq)))) . n) by Th3; then (Partial_Sums (Cseq * seq)) . (n + 1) = ((Cseq * (Partial_Sums seq)) . (n + 1)) + ((- 1r) * ((Partial_Sums (((Cseq ^\ 1) - Cseq) * (Partial_Sums seq))) . n)) by CLVECT_1:def_14; hence (Partial_Sums (Cseq * seq)) . (n + 1) = ((Cseq * (Partial_Sums seq)) . (n + 1)) - ((Partial_Sums (((Cseq ^\ 1) - Cseq) * (Partial_Sums seq))) . n) by CLVECT_1:3; ::_thesis: verum end; theorem :: CLVECT_3:54 for X being ComplexUnitarySpace for seq being sequence of X for Cseq being Complex_Sequence for n being Element of NAT holds Sum ((Cseq * seq),(n + 1)) = ((Cseq * (Partial_Sums seq)) . (n + 1)) - (Sum ((((Cseq ^\ 1) - Cseq) * (Partial_Sums seq)),n)) by Th53;