:: LOPBAN_3 semantic presentation begin theorem Th1: :: LOPBAN_3:1 for X being non empty right_complementable add-associative right_zeroed NORMSTR for seq being sequence of X st ( for n being Element of NAT holds seq . n = 0. X ) holds for m being Element of NAT holds (Partial_Sums seq) . m = 0. X proof let X be non empty right_complementable add-associative right_zeroed NORMSTR ; ::_thesis: for seq being sequence of X st ( for n being Element of NAT holds seq . n = 0. X ) holds for m being Element of NAT holds (Partial_Sums seq) . m = 0. X let seq be sequence of X; ::_thesis: ( ( for n being Element of NAT holds seq . n = 0. X ) implies for m being Element of NAT holds (Partial_Sums seq) . m = 0. X ) assume A1: for n being Element of NAT holds seq . n = 0. X ; ::_thesis: for m being Element of NAT holds (Partial_Sums seq) . m = 0. X let m be Element of NAT ; ::_thesis: (Partial_Sums seq) . m = 0. X defpred S1[ Element of NAT ] means seq . $1 = (Partial_Sums seq) . $1; A2: 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 A3: S1[k] ; ::_thesis: S1[k + 1] thus seq . (k + 1) = (0. X) + (seq . (k + 1)) by RLVECT_1:4 .= ((Partial_Sums seq) . k) + (seq . (k + 1)) by A1, A3 .= (Partial_Sums seq) . (k + 1) by BHSP_4:def_1 ; ::_thesis: verum end; A4: S1[ 0 ] by BHSP_4:def_1; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2); then seq = Partial_Sums seq by FUNCT_2:63; hence (Partial_Sums seq) . m = 0. X by A1; ::_thesis: verum end; definition let X be RealNormSpace; let seq be sequence of X; attrseq is summable means :Def1: :: LOPBAN_3:def 1 Partial_Sums seq is convergent ; end; :: deftheorem Def1 defines summable LOPBAN_3:def_1_:_ for X being RealNormSpace for seq being sequence of X holds ( seq is summable iff Partial_Sums seq is convergent ); registration let X be RealNormSpace; clusterV4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) summable for Element of K32(K33(NAT, the carrier of X)); existence ex b1 being sequence of X st b1 is summable proof reconsider C = NAT --> (0. X) as sequence of X ; take C ; ::_thesis: C is summable take 0. X ; :: according to NORMSP_1:def_6,LOPBAN_3:def_1 ::_thesis: for b1 being Element of REAL holds ( b1 <= 0 or ex b2 being Element of NAT st for b3 being Element of NAT holds ( not b2 <= b3 or not b1 <= ||.(((Partial_Sums C) . b3) - (0. X)).|| ) ) let p be Real; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not p <= ||.(((Partial_Sums C) . b2) - (0. X)).|| ) ) assume A1: 0 < p ; ::_thesis: ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not p <= ||.(((Partial_Sums C) . b2) - (0. X)).|| ) take 0 ; ::_thesis: for b1 being Element of NAT holds ( not 0 <= b1 or not p <= ||.(((Partial_Sums C) . b1) - (0. X)).|| ) let m be Element of NAT ; ::_thesis: ( not 0 <= m or not p <= ||.(((Partial_Sums C) . m) - (0. X)).|| ) assume 0 <= m ; ::_thesis: not p <= ||.(((Partial_Sums C) . m) - (0. X)).|| for n being Element of NAT holds C . n = 0. X by FUNCOP_1:7; then ||.(((Partial_Sums C) . m) - (0. X)).|| = ||.((0. X) - (0. X)).|| by Th1 .= 0 by NORMSP_1:6 ; hence not p <= ||.(((Partial_Sums C) . m) - (0. X)).|| by A1; ::_thesis: verum end; end; definition let X be RealNormSpace; let seq be sequence of X; func Sum seq -> Element of X equals :: LOPBAN_3:def 2 lim (Partial_Sums seq); correctness coherence lim (Partial_Sums seq) is Element of X; ; end; :: deftheorem defines Sum LOPBAN_3:def_2_:_ for X being RealNormSpace for seq being sequence of X holds Sum seq = lim (Partial_Sums seq); definition let X be RealNormSpace; let seq be sequence of X; attrseq is norm_summable means :Def3: :: LOPBAN_3:def 3 ||.seq.|| is summable ; end; :: deftheorem Def3 defines norm_summable LOPBAN_3:def_3_:_ for X being RealNormSpace for seq being sequence of X holds ( seq is norm_summable iff ||.seq.|| is summable ); theorem Th2: :: LOPBAN_3:2 for X being RealNormSpace for seq being sequence of X for m being Element of NAT holds 0 <= ||.seq.|| . m proof let X be RealNormSpace; ::_thesis: for seq being sequence of X for m being Element of NAT holds 0 <= ||.seq.|| . m let seq be sequence of X; ::_thesis: for m being Element of NAT holds 0 <= ||.seq.|| . m let m be Element of NAT ; ::_thesis: 0 <= ||.seq.|| . m ||.seq.|| . m = ||.(seq . m).|| by NORMSP_0:def_4; hence 0 <= ||.seq.|| . m ; ::_thesis: verum end; theorem Th3: :: LOPBAN_3:3 for X being RealNormSpace for x, y, z being Element of X holds ||.(x - y).|| = ||.((x - z) + (z - y)).|| proof let X be RealNormSpace; ::_thesis: for x, y, z being Element of X holds ||.(x - y).|| = ||.((x - z) + (z - y)).|| let x, y, z be Element of X; ::_thesis: ||.(x - y).|| = ||.((x - z) + (z - y)).|| thus ||.(x - y).|| = ||.((x - (0. X)) - y).|| by RLVECT_1:13 .= ||.((x - (z - z)) - y).|| by RLVECT_1:5 .= ||.(((x - z) + z) - y).|| by RLVECT_1:29 .= ||.((x - z) + (z - y)).|| by RLVECT_1:def_3 ; ::_thesis: verum end; theorem Th4: :: LOPBAN_3:4 for X being RealNormSpace for seq being sequence of X st seq is convergent holds for s being Real st 0 < s holds ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((seq . m) - (seq . n)).|| < s proof let X be RealNormSpace; ::_thesis: for seq being sequence of X st seq is convergent holds for s being Real st 0 < s holds ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((seq . m) - (seq . n)).|| < s let seq be sequence of X; ::_thesis: ( seq is convergent implies for s being Real st 0 < s holds ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((seq . m) - (seq . n)).|| < s ) assume seq is convergent ; ::_thesis: for s being Real st 0 < s holds ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((seq . m) - (seq . n)).|| < s then consider g1 being Element of X such that A1: for s being Real st 0 < s holds ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((seq . m) - g1).|| < s by NORMSP_1:def_6; let s be Real; ::_thesis: ( 0 < s implies ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((seq . m) - (seq . n)).|| < s ) assume 0 < s ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((seq . m) - (seq . n)).|| < s then consider n being Element of NAT such that A2: for m being Element of NAT st n <= m holds ||.((seq . m) - g1).|| < s / 2 by A1, XREAL_1:215; now__::_thesis:_for_m_being_Element_of_NAT_st_n_<=_m_holds_ ||.((seq_._m)_-_(seq_._n)).||_<_s let m be Element of NAT ; ::_thesis: ( n <= m implies ||.((seq . m) - (seq . n)).|| < s ) assume n <= m ; ::_thesis: ||.((seq . m) - (seq . n)).|| < s then A3: ||.((seq . m) - g1).|| < s / 2 by A2; A4: ( ||.(((seq . m) - g1) + (g1 - (seq . n))).|| <= ||.((seq . m) - g1).|| + ||.(g1 - (seq . n)).|| & ||.(((seq . m) - g1) + (g1 - (seq . n))).|| = ||.((seq . m) - (seq . n)).|| ) by Th3, NORMSP_1:def_1; ||.((seq . n) - g1).|| < s / 2 by A2; then ||.(g1 - (seq . n)).|| < s / 2 by NORMSP_1:7; then ||.((seq . m) - g1).|| + ||.(g1 - (seq . n)).|| < (s / 2) + (s / 2) by A3, XREAL_1:8; hence ||.((seq . m) - (seq . n)).|| < s by A4, XXREAL_0:2; ::_thesis: verum end; hence ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((seq . m) - (seq . n)).|| < s ; ::_thesis: verum end; theorem Th5: :: LOPBAN_3:5 for X being RealNormSpace for seq being sequence of X holds ( seq is Cauchy_sequence_by_Norm iff for p being Real st p > 0 holds ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((seq . m) - (seq . n)).|| < p ) proof let X be RealNormSpace; ::_thesis: for seq being sequence of X holds ( seq is Cauchy_sequence_by_Norm iff for p being Real st p > 0 holds ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((seq . m) - (seq . n)).|| < p ) let seq be sequence of X; ::_thesis: ( seq is Cauchy_sequence_by_Norm iff for p being Real st p > 0 holds ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((seq . m) - (seq . n)).|| < p ) A1: now__::_thesis:_(_(_for_p_being_Real_st_p_>_0_holds_ ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ ||.((seq_._m)_-_(seq_._n)).||_<_p_)_implies_seq_is_Cauchy_sequence_by_Norm_) assume A2: for p being Real st p > 0 holds ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((seq . m) - (seq . n)).|| < p ; ::_thesis: seq is Cauchy_sequence_by_Norm now__::_thesis:_for_s_being_Real_st_0_<_s_holds_ ex_k_being_Element_of_NAT_st_ for_m,_n_being_Element_of_NAT_st_k_<=_m_&_k_<=_n_holds_ ||.((seq_._m)_-_(seq_._n)).||_<_s let s be Real; ::_thesis: ( 0 < s implies ex k being Element of NAT st for m, n being Element of NAT st k <= m & k <= n holds ||.((seq . m) - (seq . n)).|| < s ) assume 0 < s ; ::_thesis: ex k being Element of NAT st for m, n being Element of NAT st k <= m & k <= n holds ||.((seq . m) - (seq . n)).|| < s then consider k being Element of NAT such that A3: for m being Element of NAT st k <= m holds ||.((seq . m) - (seq . k)).|| < s / 2 by A2, XREAL_1:215; now__::_thesis:_for_m,_n_being_Element_of_NAT_st_k_<=_m_&_k_<=_n_holds_ ||.((seq_._m)_-_(seq_._n)).||_<_s let m, n be Element of NAT ; ::_thesis: ( k <= m & k <= n implies ||.((seq . m) - (seq . n)).|| < s ) assume that A4: k <= m and A5: k <= n ; ::_thesis: ||.((seq . m) - (seq . n)).|| < s ||.((seq . n) - (seq . k)).|| < s / 2 by A3, A5; then A6: ||.((seq . k) - (seq . n)).|| < s / 2 by NORMSP_1:7; ||.((seq . m) - (seq . k)).|| < s / 2 by A3, A4; then A7: ||.((seq . m) - (seq . k)).|| + ||.((seq . k) - (seq . n)).|| < (s / 2) + (s / 2) by A6, XREAL_1:8; ( ||.(((seq . m) - (seq . k)) + ((seq . k) - (seq . n))).|| <= ||.((seq . m) - (seq . k)).|| + ||.((seq . k) - (seq . n)).|| & ||.(((seq . m) - (seq . k)) + ((seq . k) - (seq . n))).|| = ||.((seq . m) - (seq . n)).|| ) by Th3, NORMSP_1:def_1; hence ||.((seq . m) - (seq . n)).|| < s by A7, XXREAL_0:2; ::_thesis: verum end; hence ex k being Element of NAT st for m, n being Element of NAT st k <= m & k <= n holds ||.((seq . m) - (seq . n)).|| < s ; ::_thesis: verum end; hence seq is Cauchy_sequence_by_Norm by RSSPACE3:8; ::_thesis: verum end; now__::_thesis:_(_seq_is_Cauchy_sequence_by_Norm_implies_for_p_being_Real_st_p_>_0_holds_ ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ ||.((seq_._m)_-_(seq_._n)).||_<_p_) assume A8: seq is Cauchy_sequence_by_Norm ; ::_thesis: for p being Real st p > 0 holds ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((seq . m) - (seq . n)).|| < p thus for p being Real st p > 0 holds ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((seq . m) - (seq . n)).|| < p ::_thesis: verum proof let p be Real; ::_thesis: ( p > 0 implies ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((seq . m) - (seq . n)).|| < p ) assume p > 0 ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((seq . m) - (seq . n)).|| < p then consider n being Element of NAT such that A9: for m, k being Element of NAT st n <= m & n <= k holds ||.((seq . m) - (seq . k)).|| < p by A8, RSSPACE3:8; for m being Element of NAT st n <= m holds ||.((seq . m) - (seq . n)).|| < p by A9; hence ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((seq . m) - (seq . n)).|| < p ; ::_thesis: verum end; end; hence ( seq is Cauchy_sequence_by_Norm iff for p being Real st p > 0 holds ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((seq . m) - (seq . n)).|| < p ) by A1; ::_thesis: verum end; theorem Th6: :: LOPBAN_3:6 for X being RealNormSpace for seq being sequence of X st ( for n being Element of NAT holds seq . n = 0. X ) holds for m being Element of NAT holds (Partial_Sums ||.seq.||) . m = 0 proof let X be RealNormSpace; ::_thesis: for seq being sequence of X st ( for n being Element of NAT holds seq . n = 0. X ) holds for m being Element of NAT holds (Partial_Sums ||.seq.||) . m = 0 let seq be sequence of X; ::_thesis: ( ( for n being Element of NAT holds seq . n = 0. X ) implies for m being Element of NAT holds (Partial_Sums ||.seq.||) . m = 0 ) assume A1: for n being Element of NAT holds seq . n = 0. X ; ::_thesis: for m being Element of NAT holds (Partial_Sums ||.seq.||) . m = 0 let m be Element of NAT ; ::_thesis: (Partial_Sums ||.seq.||) . m = 0 defpred S1[ Element of NAT ] means ||.seq.|| . $1 = (Partial_Sums ||.seq.||) . $1; A2: 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 A3: S1[k] ; ::_thesis: S1[k + 1] thus ||.seq.|| . (k + 1) = ||.(0. X).|| + (||.seq.|| . (k + 1)) .= ||.(seq . k).|| + (||.seq.|| . (k + 1)) by A1 .= ((Partial_Sums ||.seq.||) . k) + (||.seq.|| . (k + 1)) by A3, NORMSP_0:def_4 .= (Partial_Sums ||.seq.||) . (k + 1) by SERIES_1:def_1 ; ::_thesis: verum end; A4: S1[ 0 ] by SERIES_1:def_1; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2); hence (Partial_Sums ||.seq.||) . m = ||.seq.|| . m .= ||.(seq . m).|| by NORMSP_0:def_4 .= ||.(0. X).|| by A1 .= 0 ; ::_thesis: verum end; theorem Th7: :: LOPBAN_3:7 for X being RealNormSpace for seq, seq1 being sequence of X st seq1 is subsequence of seq & seq is convergent holds seq1 is convergent proof let X be RealNormSpace; ::_thesis: for seq, seq1 being sequence of X st seq1 is subsequence of seq & seq is convergent holds seq1 is convergent let seq, seq1 be sequence of X; ::_thesis: ( seq1 is subsequence of seq & seq is convergent implies seq1 is convergent ) assume that A1: seq1 is subsequence of seq and A2: seq is convergent ; ::_thesis: seq1 is convergent consider g1 being Element of X such that A3: for p being Real st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((seq . m) - g1).|| < p by A2, NORMSP_1:def_6; take g1 ; :: according to NORMSP_1:def_6 ::_thesis: for b1 being Element of REAL holds ( b1 <= 0 or ex b2 being Element of NAT st for b3 being Element of NAT holds ( not b2 <= b3 or not b1 <= ||.((seq1 . b3) - g1).|| ) ) let p be Real; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not p <= ||.((seq1 . b2) - g1).|| ) ) assume 0 < p ; ::_thesis: ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not p <= ||.((seq1 . b2) - g1).|| ) then consider n1 being Element of NAT such that A4: for m being Element of NAT st n1 <= m holds ||.((seq . m) - g1).|| < p by A3; take n = n1; ::_thesis: for b1 being Element of NAT holds ( not n <= b1 or not p <= ||.((seq1 . b1) - g1).|| ) let m be Element of NAT ; ::_thesis: ( not n <= m or not p <= ||.((seq1 . m) - g1).|| ) assume A5: n <= m ; ::_thesis: not p <= ||.((seq1 . m) - g1).|| consider Nseq being increasing sequence of NAT such that A6: seq1 = seq * Nseq by A1, VALUED_0:def_17; m <= Nseq . m by SEQM_3:14; then A7: n <= Nseq . m by A5, XXREAL_0:2; seq1 . m = seq . (Nseq . m) by A6, FUNCT_2:15; hence not p <= ||.((seq1 . m) - g1).|| by A4, A7; ::_thesis: verum end; theorem Th8: :: LOPBAN_3:8 for X being RealNormSpace for seq, seq1 being sequence of X st seq1 is subsequence of seq & seq is convergent holds lim seq1 = lim seq proof let X be RealNormSpace; ::_thesis: for seq, seq1 being sequence of X st seq1 is subsequence of seq & seq is convergent holds lim seq1 = lim seq let seq, seq1 be sequence of X; ::_thesis: ( seq1 is subsequence of seq & seq is convergent implies lim seq1 = lim seq ) assume that A1: seq1 is subsequence of seq and A2: seq is convergent ; ::_thesis: lim seq1 = lim seq consider Nseq being increasing sequence of NAT such that A3: seq1 = seq * Nseq by A1, VALUED_0:def_17; A4: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_ ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ ||.((seq1_._m)_-_(lim_seq)).||_<_p let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((seq1 . m) - (lim seq)).|| < p ) assume 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((seq1 . m) - (lim seq)).|| < p then consider n1 being Element of NAT such that A5: for m being Element of NAT st n1 <= m holds ||.((seq . m) - (lim seq)).|| < p by A2, NORMSP_1:def_7; take n = n1; ::_thesis: for m being Element of NAT st n <= m holds ||.((seq1 . m) - (lim seq)).|| < p let m be Element of NAT ; ::_thesis: ( n <= m implies ||.((seq1 . m) - (lim seq)).|| < p ) assume A6: n <= m ; ::_thesis: ||.((seq1 . m) - (lim seq)).|| < p m <= Nseq . m by SEQM_3:14; then A7: n <= Nseq . m by A6, XXREAL_0:2; seq1 . m = seq . (Nseq . m) by A3, FUNCT_2:15; hence ||.((seq1 . m) - (lim seq)).|| < p by A5, A7; ::_thesis: verum end; seq1 is convergent by A1, A2, Th7; hence lim seq1 = lim seq by A4, NORMSP_1:def_7; ::_thesis: verum end; theorem :: LOPBAN_3:9 for X being RealNormSpace for seq, seq1 being sequence of X for k being Element of NAT st seq is convergent holds ( seq ^\ k is convergent & lim (seq ^\ k) = lim seq ) by Th7, Th8; theorem Th10: :: LOPBAN_3:10 for X being RealNormSpace for seq, seq1 being sequence of X st seq is convergent & ex k being Element of NAT st seq = seq1 ^\ k holds seq1 is convergent proof let X be RealNormSpace; ::_thesis: for seq, seq1 being sequence of X st seq is convergent & ex k being Element of NAT st seq = seq1 ^\ k holds seq1 is convergent let seq, seq1 be sequence of X; ::_thesis: ( seq is convergent & ex k being Element of NAT st seq = seq1 ^\ k implies seq1 is convergent ) assume that A1: seq is convergent and A2: ex k being Element of NAT st seq = seq1 ^\ k ; ::_thesis: seq1 is convergent consider k being Element of NAT such that A3: seq = seq1 ^\ k by A2; consider g1 being Element of X such that A4: for p being Real st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((seq . m) - g1).|| < p by A1, NORMSP_1:def_6; take g1 ; :: according to NORMSP_1:def_6 ::_thesis: for b1 being Element of REAL holds ( b1 <= 0 or ex b2 being Element of NAT st for b3 being Element of NAT holds ( not b2 <= b3 or not b1 <= ||.((seq1 . b3) - g1).|| ) ) let p be Real; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not p <= ||.((seq1 . b2) - g1).|| ) ) assume 0 < p ; ::_thesis: ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not p <= ||.((seq1 . b2) - g1).|| ) then consider n1 being Element of NAT such that A5: for m being Element of NAT st n1 <= m holds ||.((seq . m) - g1).|| < p by A4; take n = n1 + k; ::_thesis: for b1 being Element of NAT holds ( not n <= b1 or not p <= ||.((seq1 . b1) - g1).|| ) let m be Element of NAT ; ::_thesis: ( not n <= m or not p <= ||.((seq1 . m) - g1).|| ) assume A6: n <= m ; ::_thesis: not p <= ||.((seq1 . m) - g1).|| then consider l being Nat such that A7: m = (n1 + k) + l by NAT_1:10; reconsider l = l as Element of NAT by ORDINAL1:def_12; m - k = ((n1 + l) + k) + (- k) by A7; then reconsider m1 = m - k as Element of NAT ; now__::_thesis:_n1_<=_m1 assume not n1 <= m1 ; ::_thesis: contradiction then m1 + k < n1 + k by XREAL_1:6; hence contradiction by A6; ::_thesis: verum end; then ( m1 + k = m & ||.((seq . m1) - g1).|| < p ) by A5; hence not p <= ||.((seq1 . m) - g1).|| by A3, NAT_1:def_3; ::_thesis: verum end; theorem Th11: :: LOPBAN_3:11 for X being RealNormSpace for seq, seq1 being sequence of X st seq is convergent & ex k being Element of NAT st seq = seq1 ^\ k holds lim seq1 = lim seq proof let X be RealNormSpace; ::_thesis: for seq, seq1 being sequence of X st seq is convergent & ex k being Element of NAT st seq = seq1 ^\ k holds lim seq1 = lim seq let seq, seq1 be sequence of X; ::_thesis: ( seq is convergent & ex k being Element of NAT st seq = seq1 ^\ k implies lim seq1 = lim seq ) assume that A1: seq is convergent and A2: ex k being Element of NAT st seq = seq1 ^\ k ; ::_thesis: lim seq1 = lim seq consider k being Element of NAT such that A3: seq = seq1 ^\ k by A2; A4: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_ ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ ||.((seq1_._m)_-_(lim_seq)).||_<_p let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((seq1 . m) - (lim seq)).|| < p ) assume 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((seq1 . m) - (lim seq)).|| < p then consider n1 being Element of NAT such that A5: for m being Element of NAT st n1 <= m holds ||.((seq . m) - (lim seq)).|| < p by A1, NORMSP_1:def_7; take n = n1 + k; ::_thesis: for m being Element of NAT st n <= m holds ||.((seq1 . m) - (lim seq)).|| < p let m be Element of NAT ; ::_thesis: ( n <= m implies ||.((seq1 . m) - (lim seq)).|| < p ) assume A6: n <= m ; ::_thesis: ||.((seq1 . m) - (lim seq)).|| < p then consider l being Nat such that A7: m = (n1 + k) + l by NAT_1:10; reconsider l = l as Element of NAT by ORDINAL1:def_12; m - k = ((n1 + l) + k) + (- k) by A7; then reconsider m1 = m - k as Element of NAT ; now__::_thesis:_n1_<=_m1 assume not n1 <= m1 ; ::_thesis: contradiction then m1 + k < n1 + k by XREAL_1:6; hence contradiction by A6; ::_thesis: verum end; then ( m1 + k = m & ||.((seq . m1) - (lim seq)).|| < p ) by A5; hence ||.((seq1 . m) - (lim seq)).|| < p by A3, NAT_1:def_3; ::_thesis: verum end; seq1 is convergent by A1, A2, Th10; hence lim seq1 = lim seq by A4, NORMSP_1:def_7; ::_thesis: verum end; theorem Th12: :: LOPBAN_3:12 for X being RealNormSpace for seq being sequence of X st seq is constant holds seq is convergent proof let X be RealNormSpace; ::_thesis: for seq being sequence of X st seq is constant holds seq is convergent let seq be sequence of X; ::_thesis: ( seq is constant implies seq is convergent ) assume seq is constant ; ::_thesis: seq is convergent then consider r being Element of X such that A1: for n being Nat holds seq . n = r by VALUED_0:def_18; take g = r; :: according to NORMSP_1:def_6 ::_thesis: for b1 being Element of REAL holds ( b1 <= 0 or ex b2 being Element of NAT st for b3 being Element of NAT holds ( not b2 <= b3 or not b1 <= ||.((seq . b3) - g).|| ) ) let p be Real; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not p <= ||.((seq . b2) - g).|| ) ) assume A2: 0 < p ; ::_thesis: ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not p <= ||.((seq . b2) - g).|| ) take n = 0 ; ::_thesis: for b1 being Element of NAT holds ( not n <= b1 or not p <= ||.((seq . b1) - g).|| ) let m be Element of NAT ; ::_thesis: ( not n <= m or not p <= ||.((seq . m) - g).|| ) assume n <= m ; ::_thesis: not p <= ||.((seq . m) - g).|| ||.((seq . m) - g).|| = ||.(r - g).|| by A1 .= ||.(0. X).|| by RLVECT_1:15 .= 0 ; hence not p <= ||.((seq . m) - g).|| by A2; ::_thesis: verum end; theorem Th13: :: LOPBAN_3:13 for X being RealNormSpace for seq being sequence of X st ( for n being Element of NAT holds seq . n = 0. X ) holds seq is norm_summable proof let X be RealNormSpace; ::_thesis: for seq being sequence of X st ( for n being Element of NAT holds seq . n = 0. X ) holds seq is norm_summable let seq be sequence of X; ::_thesis: ( ( for n being Element of NAT holds seq . n = 0. X ) implies seq is norm_summable ) assume A1: for n being Element of NAT holds seq . n = 0. X ; ::_thesis: seq is norm_summable take 0 ; :: according to SEQ_2:def_6,SERIES_1:def_2,LOPBAN_3:def_3 ::_thesis: for b1 being set holds ( b1 <= 0 or ex b2 being Element of NAT st for b3 being Element of NAT holds ( not b2 <= b3 or not b1 <= abs (((Partial_Sums ||.seq.||) . b3) - 0) ) ) let p be real number ; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not p <= abs (((Partial_Sums ||.seq.||) . b2) - 0) ) ) assume A2: 0 < p ; ::_thesis: ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not p <= abs (((Partial_Sums ||.seq.||) . b2) - 0) ) take 0 ; ::_thesis: for b1 being Element of NAT holds ( not 0 <= b1 or not p <= abs (((Partial_Sums ||.seq.||) . b1) - 0) ) let m be Element of NAT ; ::_thesis: ( not 0 <= m or not p <= abs (((Partial_Sums ||.seq.||) . m) - 0) ) assume 0 <= m ; ::_thesis: not p <= abs (((Partial_Sums ||.seq.||) . m) - 0) abs (((Partial_Sums ||.seq.||) . m) - 0) = abs (0 - 0) by A1, Th6 .= 0 by ABSVALUE:def_1 ; hence not p <= abs (((Partial_Sums ||.seq.||) . m) - 0) by A2; ::_thesis: verum end; registration let X be RealNormSpace; clusterV4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) norm_summable for Element of K32(K33(NAT, the carrier of X)); existence ex b1 being sequence of X st b1 is norm_summable proof reconsider C = NAT --> (0. X) as sequence of X ; take C ; ::_thesis: C is norm_summable for n being Element of NAT holds C . n = 0. X by FUNCOP_1:7; hence C is norm_summable by Th13; ::_thesis: verum end; end; theorem Th14: :: LOPBAN_3:14 for X being RealNormSpace for s being sequence of X st s is summable holds ( s is convergent & lim s = 0. X ) proof let X be RealNormSpace; ::_thesis: for s being sequence of X st s is summable holds ( s is convergent & lim s = 0. X ) let s be sequence of X; ::_thesis: ( s is summable implies ( s is convergent & lim s = 0. X ) ) assume s is summable ; ::_thesis: ( s is convergent & lim s = 0. X ) then A1: Partial_Sums s is convergent by Def1; then A2: (Partial_Sums s) ^\ 1 is convergent by Th7; lim ((Partial_Sums s) ^\ 1) = lim (Partial_Sums s) by A1, Th8; then A3: lim (((Partial_Sums s) ^\ 1) - (Partial_Sums s)) = (lim (Partial_Sums s)) - (lim (Partial_Sums s)) by A1, A2, NORMSP_1:26 .= 0. X by RLVECT_1:15 ; now__::_thesis:_for_n_being_Element_of_NAT_holds_(((Partial_Sums_s)_^\_1)_._n)_-_((Partial_Sums_s)_._n)_=_(s_^\_1)_._n let n be Element of NAT ; ::_thesis: (((Partial_Sums s) ^\ 1) . n) - ((Partial_Sums s) . n) = (s ^\ 1) . n (Partial_Sums s) . (n + 1) = ((Partial_Sums s) . n) + (s . (n + 1)) by BHSP_4:def_1; then (Partial_Sums s) . (n + 1) = ((Partial_Sums s) . n) + ((s ^\ 1) . n) by NAT_1:def_3; then ((Partial_Sums s) ^\ 1) . n = ((s ^\ 1) . n) + ((Partial_Sums s) . n) by NAT_1:def_3; then (((Partial_Sums s) ^\ 1) . n) - ((Partial_Sums s) . n) = ((s ^\ 1) . n) + (((Partial_Sums s) . n) - ((Partial_Sums s) . n)) by RLVECT_1:def_3; then (((Partial_Sums s) ^\ 1) . n) - ((Partial_Sums s) . n) = ((s ^\ 1) . n) + (0. X) by RLVECT_1:15; hence (((Partial_Sums s) ^\ 1) . n) - ((Partial_Sums s) . n) = (s ^\ 1) . n by RLVECT_1:4; ::_thesis: verum end; then A4: s ^\ 1 = ((Partial_Sums s) ^\ 1) - (Partial_Sums s) by NORMSP_1:def_3; then s ^\ 1 is convergent by A1, A2, NORMSP_1:20; hence ( s is convergent & lim s = 0. X ) by A3, A4, Th10, Th11; ::_thesis: verum end; theorem Th15: :: LOPBAN_3:15 for X being RealNormSpace for s1, s2 being sequence of X holds (Partial_Sums s1) + (Partial_Sums s2) = Partial_Sums (s1 + s2) proof let X be RealNormSpace; ::_thesis: for s1, s2 being sequence of X holds (Partial_Sums s1) + (Partial_Sums s2) = Partial_Sums (s1 + s2) let s1, s2 be sequence of X; ::_thesis: (Partial_Sums s1) + (Partial_Sums s2) = Partial_Sums (s1 + s2) A1: now__::_thesis:_for_n_being_Element_of_NAT_holds_((Partial_Sums_s1)_+_(Partial_Sums_s2))_._(n_+_1)_=_(((Partial_Sums_s1)_+_(Partial_Sums_s2))_._n)_+_((s1_+_s2)_._(n_+_1)) let n be Element of NAT ; ::_thesis: ((Partial_Sums s1) + (Partial_Sums s2)) . (n + 1) = (((Partial_Sums s1) + (Partial_Sums s2)) . n) + ((s1 + s2) . (n + 1)) thus ((Partial_Sums s1) + (Partial_Sums s2)) . (n + 1) = ((Partial_Sums s1) . (n + 1)) + ((Partial_Sums s2) . (n + 1)) by NORMSP_1:def_2 .= (((Partial_Sums s1) . n) + (s1 . (n + 1))) + ((Partial_Sums s2) . (n + 1)) by BHSP_4:def_1 .= (((Partial_Sums s1) . n) + (s1 . (n + 1))) + ((s2 . (n + 1)) + ((Partial_Sums s2) . n)) by BHSP_4:def_1 .= ((((Partial_Sums s1) . n) + (s1 . (n + 1))) + (s2 . (n + 1))) + ((Partial_Sums s2) . n) by RLVECT_1:def_3 .= (((Partial_Sums s1) . n) + ((s1 . (n + 1)) + (s2 . (n + 1)))) + ((Partial_Sums s2) . n) by RLVECT_1:def_3 .= (((Partial_Sums s1) . n) + ((s1 + s2) . (n + 1))) + ((Partial_Sums s2) . n) by NORMSP_1:def_2 .= (((Partial_Sums s1) . n) + ((Partial_Sums s2) . n)) + ((s1 + s2) . (n + 1)) by RLVECT_1:def_3 .= (((Partial_Sums s1) + (Partial_Sums s2)) . n) + ((s1 + s2) . (n + 1)) by NORMSP_1:def_2 ; ::_thesis: verum end; ((Partial_Sums s1) + (Partial_Sums s2)) . 0 = ((Partial_Sums s1) . 0) + ((Partial_Sums s2) . 0) by NORMSP_1:def_2 .= (s1 . 0) + ((Partial_Sums s2) . 0) by BHSP_4:def_1 .= (s1 . 0) + (s2 . 0) by BHSP_4:def_1 .= (s1 + s2) . 0 by NORMSP_1:def_2 ; hence (Partial_Sums s1) + (Partial_Sums s2) = Partial_Sums (s1 + s2) by A1, BHSP_4:def_1; ::_thesis: verum end; theorem Th16: :: LOPBAN_3:16 for X being RealNormSpace for s1, s2 being sequence of X holds (Partial_Sums s1) - (Partial_Sums s2) = Partial_Sums (s1 - s2) proof let X be RealNormSpace; ::_thesis: for s1, s2 being sequence of X holds (Partial_Sums s1) - (Partial_Sums s2) = Partial_Sums (s1 - s2) let s1, s2 be sequence of X; ::_thesis: (Partial_Sums s1) - (Partial_Sums s2) = Partial_Sums (s1 - s2) A1: now__::_thesis:_for_n_being_Element_of_NAT_holds_((Partial_Sums_s1)_-_(Partial_Sums_s2))_._(n_+_1)_=_(((Partial_Sums_s1)_-_(Partial_Sums_s2))_._n)_+_((s1_-_s2)_._(n_+_1)) let n be Element of NAT ; ::_thesis: ((Partial_Sums s1) - (Partial_Sums s2)) . (n + 1) = (((Partial_Sums s1) - (Partial_Sums s2)) . n) + ((s1 - s2) . (n + 1)) thus ((Partial_Sums s1) - (Partial_Sums s2)) . (n + 1) = ((Partial_Sums s1) . (n + 1)) - ((Partial_Sums s2) . (n + 1)) by NORMSP_1:def_3 .= (((Partial_Sums s1) . n) + (s1 . (n + 1))) - ((Partial_Sums s2) . (n + 1)) by BHSP_4:def_1 .= (((Partial_Sums s1) . n) + (s1 . (n + 1))) - ((s2 . (n + 1)) + ((Partial_Sums s2) . n)) by BHSP_4:def_1 .= ((((Partial_Sums s1) . n) + (s1 . (n + 1))) - (s2 . (n + 1))) - ((Partial_Sums s2) . n) by RLVECT_1:27 .= (((Partial_Sums s1) . n) + ((s1 . (n + 1)) - (s2 . (n + 1)))) - ((Partial_Sums s2) . n) by RLVECT_1:def_3 .= (((s1 - s2) . (n + 1)) + ((Partial_Sums s1) . n)) - ((Partial_Sums s2) . n) by NORMSP_1:def_3 .= ((s1 - s2) . (n + 1)) + (((Partial_Sums s1) . n) - ((Partial_Sums s2) . n)) by RLVECT_1:def_3 .= (((Partial_Sums s1) - (Partial_Sums s2)) . n) + ((s1 - s2) . (n + 1)) by NORMSP_1:def_3 ; ::_thesis: verum end; ((Partial_Sums s1) - (Partial_Sums s2)) . 0 = ((Partial_Sums s1) . 0) - ((Partial_Sums s2) . 0) by NORMSP_1:def_3 .= (s1 . 0) - ((Partial_Sums s2) . 0) by BHSP_4:def_1 .= (s1 . 0) - (s2 . 0) by BHSP_4:def_1 .= (s1 - s2) . 0 by NORMSP_1:def_3 ; hence (Partial_Sums s1) - (Partial_Sums s2) = Partial_Sums (s1 - s2) by A1, BHSP_4:def_1; ::_thesis: verum end; registration let X be RealNormSpace; let seq be norm_summable sequence of X; cluster||.seq.|| -> summable for Real_Sequence; coherence for b1 being Real_Sequence st b1 = ||.seq.|| holds b1 is summable by Def3; end; registration let X be RealNormSpace; cluster Function-like V30( NAT , the carrier of X) summable -> convergent for Element of K32(K33(NAT, the carrier of X)); coherence for b1 being sequence of X st b1 is summable holds b1 is convergent by Th14; end; theorem Th17: :: LOPBAN_3:17 for X being RealNormSpace 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 RealNormSpace; ::_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 A2: (Partial_Sums seq1) + (Partial_Sums seq2) is convergent by NORMSP_1:19; A3: (Partial_Sums seq1) + (Partial_Sums seq2) = Partial_Sums (seq1 + seq2) by Th15; Sum (seq1 + seq2) = lim ((Partial_Sums seq1) + (Partial_Sums seq2)) by Th15 .= (lim (Partial_Sums seq1)) + (lim (Partial_Sums seq2)) by A1, NORMSP_1:25 ; hence ( seq1 + seq2 is summable & Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) ) by A2, A3, Def1; ::_thesis: verum end; theorem Th18: :: LOPBAN_3:18 for X being RealNormSpace 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 RealNormSpace; ::_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 A2: (Partial_Sums seq1) - (Partial_Sums seq2) is convergent by NORMSP_1:20; A3: (Partial_Sums seq1) - (Partial_Sums seq2) = Partial_Sums (seq1 - seq2) by Th16; Sum (seq1 - seq2) = lim ((Partial_Sums seq1) - (Partial_Sums seq2)) by Th16 .= (lim (Partial_Sums seq1)) - (lim (Partial_Sums seq2)) by A1, NORMSP_1:26 ; hence ( seq1 - seq2 is summable & Sum (seq1 - seq2) = (Sum seq1) - (Sum seq2) ) by A2, A3, Def1; ::_thesis: verum end; registration let X be RealNormSpace; let seq1, seq2 be summable sequence of X; clusterseq1 + seq2 -> summable ; coherence seq1 + seq2 is summable by Th17; clusterseq1 - seq2 -> summable ; coherence seq1 - seq2 is summable by Th18; end; theorem Th19: :: LOPBAN_3:19 for X being RealNormSpace for seq being sequence of X for z being Real holds Partial_Sums (z * seq) = z * (Partial_Sums seq) proof let X be RealNormSpace; ::_thesis: for seq being sequence of X for z being Real holds Partial_Sums (z * seq) = z * (Partial_Sums seq) let seq be sequence of X; ::_thesis: for z being Real holds Partial_Sums (z * seq) = z * (Partial_Sums seq) let z be Real; ::_thesis: Partial_Sums (z * seq) = z * (Partial_Sums seq) defpred S1[ Element of NAT ] means (Partial_Sums (z * seq)) . $1 = (z * (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] ) assume A2: S1[n] ; ::_thesis: S1[n + 1] (Partial_Sums (z * seq)) . (n + 1) = ((Partial_Sums (z * seq)) . n) + ((z * seq) . (n + 1)) by BHSP_4:def_1 .= (z * ((Partial_Sums seq) . n)) + ((z * seq) . (n + 1)) by A2, NORMSP_1:def_5 .= (z * ((Partial_Sums seq) . n)) + (z * (seq . (n + 1))) by NORMSP_1:def_5 .= z * (((Partial_Sums seq) . n) + (seq . (n + 1))) by RLVECT_1:def_5 .= z * ((Partial_Sums seq) . (n + 1)) by BHSP_4:def_1 .= (z * (Partial_Sums seq)) . (n + 1) by NORMSP_1:def_5 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums (z * seq)) . 0 = (z * seq) . 0 by BHSP_4:def_1 .= z * (seq . 0) by NORMSP_1:def_5 .= z * ((Partial_Sums seq) . 0) by BHSP_4:def_1 .= (z * (Partial_Sums seq)) . 0 by NORMSP_1:def_5 ; then A3: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1); hence Partial_Sums (z * seq) = z * (Partial_Sums seq) by FUNCT_2:63; ::_thesis: verum end; theorem Th20: :: LOPBAN_3:20 for X being RealNormSpace for seq being summable sequence of X for z being Real holds ( z * seq is summable & Sum (z * seq) = z * (Sum seq) ) proof let X be RealNormSpace; ::_thesis: for seq being summable sequence of X for z being Real holds ( z * seq is summable & Sum (z * seq) = z * (Sum seq) ) let seq be summable sequence of X; ::_thesis: for z being Real holds ( z * seq is summable & Sum (z * seq) = z * (Sum seq) ) let z be Real; ::_thesis: ( z * seq is summable & Sum (z * seq) = z * (Sum seq) ) A1: Partial_Sums (z * seq) = z * (Partial_Sums seq) by Th19; A2: Partial_Sums seq is convergent by Def1; then A3: z * (Partial_Sums seq) is convergent by NORMSP_1:22; Sum (z * seq) = lim (z * (Partial_Sums seq)) by Th19 .= z * (Sum seq) by A2, NORMSP_1:28 ; hence ( z * seq is summable & Sum (z * seq) = z * (Sum seq) ) by A3, A1, Def1; ::_thesis: verum end; registration let X be RealNormSpace; let z be Real; let seq be summable sequence of X; clusterz * seq -> summable ; coherence z * seq is summable by Th20; end; theorem Th21: :: LOPBAN_3:21 for X being RealNormSpace for s, s1 being sequence of X st ( for n being Element of NAT holds s1 . n = s . 0 ) holds Partial_Sums (s ^\ 1) = ((Partial_Sums s) ^\ 1) - s1 proof let X be RealNormSpace; ::_thesis: for s, s1 being sequence of X st ( for n being Element of NAT holds s1 . n = s . 0 ) holds Partial_Sums (s ^\ 1) = ((Partial_Sums s) ^\ 1) - s1 let s, s1 be sequence of X; ::_thesis: ( ( for n being Element of NAT holds s1 . n = s . 0 ) implies Partial_Sums (s ^\ 1) = ((Partial_Sums s) ^\ 1) - s1 ) assume A1: for n being Element of NAT holds s1 . n = s . 0 ; ::_thesis: Partial_Sums (s ^\ 1) = ((Partial_Sums s) ^\ 1) - s1 A2: now__::_thesis:_for_k_being_Element_of_NAT_holds_(((Partial_Sums_s)_^\_1)_-_s1)_._(k_+_1)_=_((((Partial_Sums_s)_^\_1)_-_s1)_._k)_+_((s_^\_1)_._(k_+_1)) let k be Element of NAT ; ::_thesis: (((Partial_Sums s) ^\ 1) - s1) . (k + 1) = ((((Partial_Sums s) ^\ 1) - s1) . k) + ((s ^\ 1) . (k + 1)) thus (((Partial_Sums s) ^\ 1) - s1) . (k + 1) = (((Partial_Sums s) ^\ 1) . (k + 1)) - (s1 . (k + 1)) by NORMSP_1:def_3 .= (((Partial_Sums s) ^\ 1) . (k + 1)) - (s . 0) by A1 .= ((Partial_Sums s) . ((k + 1) + 1)) - (s . 0) by NAT_1:def_3 .= ((s . ((k + 1) + 1)) + ((Partial_Sums s) . (k + 1))) - (s . 0) by BHSP_4:def_1 .= ((s . ((k + 1) + 1)) + ((Partial_Sums s) . (k + 1))) - (s1 . k) by A1 .= (s . ((k + 1) + 1)) + (((Partial_Sums s) . (k + 1)) - (s1 . k)) by RLVECT_1:def_3 .= (s . ((k + 1) + 1)) + ((((Partial_Sums s) ^\ 1) . k) - (s1 . k)) by NAT_1:def_3 .= (s . ((k + 1) + 1)) + ((((Partial_Sums s) ^\ 1) - s1) . k) by NORMSP_1:def_3 .= ((((Partial_Sums s) ^\ 1) - s1) . k) + ((s ^\ 1) . (k + 1)) by NAT_1:def_3 ; ::_thesis: verum end; (((Partial_Sums s) ^\ 1) - s1) . 0 = (((Partial_Sums s) ^\ 1) . 0) - (s1 . 0) by NORMSP_1:def_3 .= (((Partial_Sums s) ^\ 1) . 0) - (s . 0) by A1 .= ((Partial_Sums s) . (0 + 1)) - (s . 0) by NAT_1:def_3 .= (((Partial_Sums s) . 0) + (s . (0 + 1))) - (s . 0) by BHSP_4:def_1 .= ((s . (0 + 1)) + (s . 0)) - (s . 0) by BHSP_4:def_1 .= (s . (0 + 1)) + ((s . 0) - (s . 0)) by RLVECT_1:def_3 .= (s . (0 + 1)) + (0. X) by RLVECT_1:15 .= s . (0 + 1) by RLVECT_1:4 .= (s ^\ 1) . 0 by NAT_1:def_3 ; hence Partial_Sums (s ^\ 1) = ((Partial_Sums s) ^\ 1) - s1 by A2, BHSP_4:def_1; ::_thesis: verum end; theorem Th22: :: LOPBAN_3:22 for X being RealNormSpace for s being sequence of X st s is summable holds for n being Element of NAT holds s ^\ n is summable proof let X be RealNormSpace; ::_thesis: for s being sequence of X st s is summable holds for n being Element of NAT holds s ^\ n is summable let s be sequence of X; ::_thesis: ( s is summable implies for n being Element of NAT holds s ^\ n is summable ) defpred S1[ Element of NAT ] means s ^\ $1 is summable ; A1: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) reconsider s1 = NAT --> ((s ^\ n) . 0) as sequence of X ; for k being Element of NAT holds s1 . k = (s ^\ n) . 0 by FUNCOP_1:7; then A2: Partial_Sums ((s ^\ n) ^\ 1) = ((Partial_Sums (s ^\ n)) ^\ 1) - s1 by Th21; assume s ^\ n is summable ; ::_thesis: S1[n + 1] then Partial_Sums (s ^\ n) is convergent by Def1; then A3: (Partial_Sums (s ^\ n)) ^\ 1 is convergent by Th7; s1 is convergent by Th12; then ( s ^\ (n + 1) = (s ^\ n) ^\ 1 & Partial_Sums ((s ^\ n) ^\ 1) is convergent ) by A3, A2, NAT_1:48, NORMSP_1:20; hence S1[n + 1] by Def1; ::_thesis: verum end; assume s is summable ; ::_thesis: for n being Element of NAT holds s ^\ n is summable then A4: S1[ 0 ] by NAT_1:47; thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A1); ::_thesis: verum end; registration let X be RealNormSpace; let seq be summable sequence of X; let n be Element of NAT ; clusterseq ^\ n -> summable for sequence of X; coherence for b1 being sequence of X st b1 = seq ^\ n holds b1 is summable by Th22; end; theorem Th23: :: LOPBAN_3:23 for X being RealNormSpace for seq being sequence of X holds ( Partial_Sums ||.seq.|| is bounded_above iff seq is norm_summable ) proof let X be RealNormSpace; ::_thesis: for seq being sequence of X holds ( Partial_Sums ||.seq.|| is bounded_above iff seq is norm_summable ) let seq be sequence of X; ::_thesis: ( Partial_Sums ||.seq.|| is bounded_above iff seq is norm_summable ) for n being Element of NAT holds 0 <= ||.seq.|| . n by Th2; then ( Partial_Sums ||.seq.|| is bounded_above iff ||.seq.|| is summable ) by SERIES_1:17; hence ( Partial_Sums ||.seq.|| is bounded_above iff seq is norm_summable ) by Def3; ::_thesis: verum end; registration let X be RealNormSpace; let seq be norm_summable sequence of X; cluster Partial_Sums ||.seq.|| -> bounded_above for Real_Sequence; coherence for b1 being Real_Sequence st b1 = Partial_Sums ||.seq.|| holds b1 is bounded_above by Th23; end; theorem Th24: :: LOPBAN_3:24 for X being RealBanachSpace for seq being sequence of X holds ( seq is summable iff for p being Real st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| < p ) proof let X be RealBanachSpace; ::_thesis: for seq being sequence of X holds ( seq is summable iff for p being Real st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| < p ) let seq be sequence of X; ::_thesis: ( seq is summable iff for p being Real st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| < p ) A1: now__::_thesis:_(_(_for_p_being_Real_st_0_<_p_holds_ ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ ||.(((Partial_Sums_seq)_._m)_-_((Partial_Sums_seq)_._n)).||_<_p_)_implies_seq_is_summable_) assume for p being Real st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| < p ; ::_thesis: seq is summable then Partial_Sums seq is Cauchy_sequence_by_Norm by Th5; then Partial_Sums seq is convergent by LOPBAN_1:def_15; hence seq is summable by Def1; ::_thesis: verum end; now__::_thesis:_(_seq_is_summable_implies_for_p_being_Real_st_0_<_p_holds_ ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ ||.(((Partial_Sums_seq)_._m)_-_((Partial_Sums_seq)_._n)).||_<_p_) assume seq is summable ; ::_thesis: for p being Real st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| < p then Partial_Sums seq is convergent by Def1; hence for p being Real st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| < p by Th4; ::_thesis: verum end; hence ( seq is summable iff for p being Real st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| < p ) by A1; ::_thesis: verum end; theorem Th25: :: LOPBAN_3:25 for X being RealNormSpace for s being sequence of X for n, m being Element of NAT st n <= m holds ||.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).|| <= abs (((Partial_Sums ||.s.||) . m) - ((Partial_Sums ||.s.||) . n)) proof let X be RealNormSpace; ::_thesis: for s being sequence of X for n, m being Element of NAT st n <= m holds ||.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).|| <= abs (((Partial_Sums ||.s.||) . m) - ((Partial_Sums ||.s.||) . n)) let s be sequence of X; ::_thesis: for n, m being Element of NAT st n <= m holds ||.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).|| <= abs (((Partial_Sums ||.s.||) . m) - ((Partial_Sums ||.s.||) . n)) set s1 = Partial_Sums s; set s2 = Partial_Sums ||.s.||; let n, m be Element of NAT ; ::_thesis: ( n <= m implies ||.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).|| <= abs (((Partial_Sums ||.s.||) . m) - ((Partial_Sums ||.s.||) . n)) ) assume n <= m ; ::_thesis: ||.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).|| <= abs (((Partial_Sums ||.s.||) . m) - ((Partial_Sums ||.s.||) . n)) then reconsider k = m - n as Element of NAT by INT_1:5; defpred S1[ Element of NAT ] means ||.(((Partial_Sums s) . (n + $1)) - ((Partial_Sums s) . n)).|| <= abs (((Partial_Sums ||.s.||) . (n + $1)) - ((Partial_Sums ||.s.||) . n)); A1: n + k = m ; now__::_thesis:_for_k_being_Element_of_NAT_holds_||.s.||_._k_>=_0 let k be Element of NAT ; ::_thesis: ||.s.|| . k >= 0 ||.(s . k).|| >= 0 ; hence ||.s.|| . k >= 0 by NORMSP_0:def_4; ::_thesis: verum end; then A2: Partial_Sums ||.s.|| is non-decreasing by SERIES_1:16; A3: 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] ) A4: abs (((Partial_Sums ||.s.||) . (n + (k + 1))) - ((Partial_Sums ||.s.||) . n)) = abs ((((Partial_Sums ||.s.||) . (n + k)) + (||.s.|| . ((n + k) + 1))) - ((Partial_Sums ||.s.||) . n)) by SERIES_1:def_1 .= abs ((((Partial_Sums ||.s.||) . (n + k)) + ||.(s . ((n + k) + 1)).||) - ((Partial_Sums ||.s.||) . n)) by NORMSP_0:def_4 .= abs (||.(s . ((n + k) + 1)).|| + (((Partial_Sums ||.s.||) . (n + k)) - ((Partial_Sums ||.s.||) . n))) ; ||.(((Partial_Sums s) . (n + (k + 1))) - ((Partial_Sums s) . n)).|| = ||.(((s . ((n + k) + 1)) + ((Partial_Sums s) . (n + k))) - ((Partial_Sums s) . n)).|| by BHSP_4:def_1 .= ||.((s . ((n + k) + 1)) + (((Partial_Sums s) . (n + k)) - ((Partial_Sums s) . n))).|| by RLVECT_1:def_3 ; then A5: ||.(((Partial_Sums s) . (n + (k + 1))) - ((Partial_Sums s) . n)).|| <= ||.(s . ((n + k) + 1)).|| + ||.(((Partial_Sums s) . (n + k)) - ((Partial_Sums s) . n)).|| by NORMSP_1:def_1; (Partial_Sums ||.s.||) . (n + k) >= (Partial_Sums ||.s.||) . n by A2, SEQM_3:5; then A6: ((Partial_Sums ||.s.||) . (n + k)) - ((Partial_Sums ||.s.||) . n) >= 0 by XREAL_1:48; assume ||.(((Partial_Sums s) . (n + k)) - ((Partial_Sums s) . n)).|| <= abs (((Partial_Sums ||.s.||) . (n + k)) - ((Partial_Sums ||.s.||) . n)) ; ::_thesis: S1[k + 1] then ||.(s . ((n + k) + 1)).|| + ||.(((Partial_Sums s) . (n + k)) - ((Partial_Sums s) . n)).|| <= ||.(s . ((n + k) + 1)).|| + (abs (((Partial_Sums ||.s.||) . (n + k)) - ((Partial_Sums ||.s.||) . n))) by XREAL_1:7; then ||.(((Partial_Sums s) . (n + (k + 1))) - ((Partial_Sums s) . n)).|| <= ||.(s . ((n + k) + 1)).|| + (abs (((Partial_Sums ||.s.||) . (n + k)) - ((Partial_Sums ||.s.||) . n))) by A5, XXREAL_0:2; then ||.(((Partial_Sums s) . (n + (k + 1))) - ((Partial_Sums s) . n)).|| <= ||.(s . ((n + k) + 1)).|| + (((Partial_Sums ||.s.||) . (n + k)) - ((Partial_Sums ||.s.||) . n)) by A6, ABSVALUE:def_1; hence S1[k + 1] by A4, ABSVALUE:def_1; ::_thesis: verum end; ||.(((Partial_Sums s) . (n + 0)) - ((Partial_Sums s) . n)).|| = ||.(0. X).|| by RLVECT_1:15 .= 0 ; then A7: S1[ 0 ] by COMPLEX1:46; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A7, A3); hence ||.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).|| <= abs (((Partial_Sums ||.s.||) . m) - ((Partial_Sums ||.s.||) . n)) by A1; ::_thesis: verum end; theorem Th26: :: LOPBAN_3:26 for X being RealBanachSpace for seq being sequence of X st seq is norm_summable holds seq is summable proof let X be RealBanachSpace; ::_thesis: for seq being sequence of X st seq is norm_summable holds seq is summable let seq be sequence of X; ::_thesis: ( seq is norm_summable implies seq is summable ) assume seq is norm_summable ; ::_thesis: seq is summable then A1: Partial_Sums ||.seq.|| is convergent by SERIES_1:def_2; now__::_thesis:_for_p_being_Real_st_0_<_p_holds_ ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ ||.(((Partial_Sums_seq)_._m)_-_((Partial_Sums_seq)_._n)).||_<_p let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| < p ) assume 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| < p then consider n being Element of NAT such that A2: for m being Element of NAT st n <= m holds abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)) < p by A1, SEQ_4:41; take n = n; ::_thesis: for m being Element of NAT st n <= m holds ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| < p let m be Element of NAT ; ::_thesis: ( n <= m implies ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| < p ) assume A3: n <= m ; ::_thesis: ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| < p then A4: ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)) by Th25; abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)) < p by A2, A3; hence ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| < p by A4, XXREAL_0:2; ::_thesis: verum end; hence seq is summable by Th24; ::_thesis: verum end; theorem :: LOPBAN_3:27 for X being RealNormSpace for rseq1 being Real_Sequence for seq2 being sequence of X st rseq1 is summable & ex m being Element of NAT st for n being Element of NAT st m <= n holds ||.(seq2 . n).|| <= rseq1 . n holds seq2 is norm_summable proof let X be RealNormSpace; ::_thesis: for rseq1 being Real_Sequence for seq2 being sequence of X st rseq1 is summable & ex m being Element of NAT st for n being Element of NAT st m <= n holds ||.(seq2 . n).|| <= rseq1 . n holds seq2 is norm_summable let rseq1 be Real_Sequence; ::_thesis: for seq2 being sequence of X st rseq1 is summable & ex m being Element of NAT st for n being Element of NAT st m <= n holds ||.(seq2 . n).|| <= rseq1 . n holds seq2 is norm_summable let seq2 be sequence of X; ::_thesis: ( rseq1 is summable & ex m being Element of NAT st for n being Element of NAT st m <= n holds ||.(seq2 . n).|| <= rseq1 . n implies seq2 is norm_summable ) assume that A1: rseq1 is summable and A2: ex m being Element of NAT st for n being Element of NAT st m <= n holds ||.(seq2 . n).|| <= rseq1 . n ; ::_thesis: seq2 is norm_summable consider m being Element of NAT such that A3: for n being Element of NAT st m <= n holds ||.(seq2 . n).|| <= rseq1 . n by A2; A4: now__::_thesis:_for_n_being_Element_of_NAT_holds_0_<=_||.seq2.||_._n let n be Element of NAT ; ::_thesis: 0 <= ||.seq2.|| . n ||.(seq2 . n).|| = ||.seq2.|| . n by NORMSP_0:def_4; hence 0 <= ||.seq2.|| . n ; ::_thesis: verum end; now__::_thesis:_for_n_being_Element_of_NAT_st_m_<=_n_holds_ ||.seq2.||_._n_<=_rseq1_._n let n be Element of NAT ; ::_thesis: ( m <= n implies ||.seq2.|| . n <= rseq1 . n ) assume m <= n ; ::_thesis: ||.seq2.|| . n <= rseq1 . n then ||.(seq2 . n).|| <= rseq1 . n by A3; hence ||.seq2.|| . n <= rseq1 . n by NORMSP_0:def_4; ::_thesis: verum end; hence ||.seq2.|| is summable by A1, A4, SERIES_1:19; :: according to LOPBAN_3:def_3 ::_thesis: verum end; theorem :: LOPBAN_3:28 for X being RealNormSpace for seq1, seq2 being sequence of X st ( for n being Element of NAT holds ( 0 <= ||.seq1.|| . n & ||.seq1.|| . n <= ||.seq2.|| . n ) ) & seq2 is norm_summable holds ( seq1 is norm_summable & Sum ||.seq1.|| <= Sum ||.seq2.|| ) proof let X be RealNormSpace; ::_thesis: for seq1, seq2 being sequence of X st ( for n being Element of NAT holds ( 0 <= ||.seq1.|| . n & ||.seq1.|| . n <= ||.seq2.|| . n ) ) & seq2 is norm_summable holds ( seq1 is norm_summable & Sum ||.seq1.|| <= Sum ||.seq2.|| ) let seq1, seq2 be sequence of X; ::_thesis: ( ( for n being Element of NAT holds ( 0 <= ||.seq1.|| . n & ||.seq1.|| . n <= ||.seq2.|| . n ) ) & seq2 is norm_summable implies ( seq1 is norm_summable & Sum ||.seq1.|| <= Sum ||.seq2.|| ) ) assume ( ( for n being Element of NAT holds ( 0 <= ||.seq1.|| . n & ||.seq1.|| . n <= ||.seq2.|| . n ) ) & seq2 is norm_summable ) ; ::_thesis: ( seq1 is norm_summable & Sum ||.seq1.|| <= Sum ||.seq2.|| ) hence ( ||.seq1.|| is summable & Sum ||.seq1.|| <= Sum ||.seq2.|| ) by SERIES_1:20; :: according to LOPBAN_3:def_3 ::_thesis: verum end; theorem :: LOPBAN_3:29 for X being RealNormSpace for seq being sequence of X st ( for n being Element of NAT holds ||.seq.|| . n > 0 ) & 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 norm_summable by SERIES_1:27; theorem :: LOPBAN_3:30 for X being RealNormSpace for seq being sequence of X for rseq1 being Real_Sequence st ( for n being Element of NAT holds rseq1 . n = n -root (||.seq.|| . n) ) & rseq1 is convergent & lim rseq1 < 1 holds seq is norm_summable proof let X be RealNormSpace; ::_thesis: for seq being sequence of X for rseq1 being Real_Sequence st ( for n being Element of NAT holds rseq1 . n = n -root (||.seq.|| . n) ) & rseq1 is convergent & lim rseq1 < 1 holds seq is norm_summable let seq be sequence of X; ::_thesis: for rseq1 being Real_Sequence st ( for n being Element of NAT holds rseq1 . n = n -root (||.seq.|| . n) ) & rseq1 is convergent & lim rseq1 < 1 holds seq is norm_summable let rseq1 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds rseq1 . n = n -root (||.seq.|| . n) ) & rseq1 is convergent & lim rseq1 < 1 implies seq is norm_summable ) assume A1: ( ( for n being Element of NAT holds rseq1 . n = n -root (||.seq.|| . n) ) & rseq1 is convergent & lim rseq1 < 1 ) ; ::_thesis: seq is norm_summable for n being Element of NAT holds ||.seq.|| . n >= 0 by Th2; hence ||.seq.|| is summable by A1, SERIES_1:28; :: according to LOPBAN_3:def_3 ::_thesis: verum end; theorem :: LOPBAN_3:31 for X being RealNormSpace for seq being sequence of X for rseq1 being Real_Sequence st ( for n being Element of NAT holds rseq1 . n = n -root (||.seq.|| . n) ) & ex m being Element of NAT st for n being Element of NAT st m <= n holds rseq1 . n >= 1 holds not ||.seq.|| is summable proof let X be RealNormSpace; ::_thesis: for seq being sequence of X for rseq1 being Real_Sequence st ( for n being Element of NAT holds rseq1 . n = n -root (||.seq.|| . n) ) & ex m being Element of NAT st for n being Element of NAT st m <= n holds rseq1 . n >= 1 holds not ||.seq.|| is summable let seq be sequence of X; ::_thesis: for rseq1 being Real_Sequence st ( for n being Element of NAT holds rseq1 . n = n -root (||.seq.|| . n) ) & ex m being Element of NAT st for n being Element of NAT st m <= n holds rseq1 . n >= 1 holds not ||.seq.|| is summable let rseq1 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds rseq1 . n = n -root (||.seq.|| . n) ) & ex m being Element of NAT st for n being Element of NAT st m <= n holds rseq1 . n >= 1 implies not ||.seq.|| is summable ) assume A1: ( ( for n being Element of NAT holds rseq1 . n = n -root (||.seq.|| . n) ) & ex m being Element of NAT st for n being Element of NAT st m <= n holds rseq1 . n >= 1 ) ; ::_thesis: not ||.seq.|| is summable for n being Element of NAT holds ||.seq.|| . n >= 0 by Th2; hence not ||.seq.|| is summable by A1, SERIES_1:29; ::_thesis: verum end; theorem :: LOPBAN_3:32 for X being RealNormSpace for seq being sequence of X for rseq1 being Real_Sequence st ( for n being Element of NAT holds rseq1 . n = n -root (||.seq.|| . n) ) & rseq1 is convergent & lim rseq1 > 1 holds not seq is norm_summable proof let X be RealNormSpace; ::_thesis: for seq being sequence of X for rseq1 being Real_Sequence st ( for n being Element of NAT holds rseq1 . n = n -root (||.seq.|| . n) ) & rseq1 is convergent & lim rseq1 > 1 holds not seq is norm_summable let seq be sequence of X; ::_thesis: for rseq1 being Real_Sequence st ( for n being Element of NAT holds rseq1 . n = n -root (||.seq.|| . n) ) & rseq1 is convergent & lim rseq1 > 1 holds not seq is norm_summable let rseq1 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds rseq1 . n = n -root (||.seq.|| . n) ) & rseq1 is convergent & lim rseq1 > 1 implies not seq is norm_summable ) assume A1: ( ( for n being Element of NAT holds rseq1 . n = n -root (||.seq.|| . n) ) & rseq1 is convergent & lim rseq1 > 1 ) ; ::_thesis: not seq is norm_summable for n being Element of NAT holds ||.seq.|| . n >= 0 by Th2; hence not ||.seq.|| is summable by A1, SERIES_1:30; :: according to LOPBAN_3:def_3 ::_thesis: verum end; theorem :: LOPBAN_3:33 for X being RealNormSpace for seq being sequence of X for rseq1 being Real_Sequence st ||.seq.|| is non-increasing & ( for n being Element of NAT holds rseq1 . n = (2 to_power n) * (||.seq.|| . (2 to_power n)) ) holds ( seq is norm_summable iff rseq1 is summable ) proof let X be RealNormSpace; ::_thesis: for seq being sequence of X for rseq1 being Real_Sequence st ||.seq.|| is non-increasing & ( for n being Element of NAT holds rseq1 . n = (2 to_power n) * (||.seq.|| . (2 to_power n)) ) holds ( seq is norm_summable iff rseq1 is summable ) let seq be sequence of X; ::_thesis: for rseq1 being Real_Sequence st ||.seq.|| is non-increasing & ( for n being Element of NAT holds rseq1 . n = (2 to_power n) * (||.seq.|| . (2 to_power n)) ) holds ( seq is norm_summable iff rseq1 is summable ) let rseq1 be Real_Sequence; ::_thesis: ( ||.seq.|| is non-increasing & ( for n being Element of NAT holds rseq1 . n = (2 to_power n) * (||.seq.|| . (2 to_power n)) ) implies ( seq is norm_summable iff rseq1 is summable ) ) assume ( ||.seq.|| is non-increasing & ( for n being Element of NAT holds rseq1 . n = (2 to_power n) * (||.seq.|| . (2 to_power n)) ) ) ; ::_thesis: ( seq is norm_summable iff rseq1 is summable ) then for n being Element of NAT holds ( ||.seq.|| is non-increasing & ||.seq.|| . n >= 0 & rseq1 . n = (2 to_power n) * (||.seq.|| . (2 to_power n)) ) by Th2; then ( ||.seq.|| is summable iff rseq1 is summable ) by SERIES_1:31; hence ( seq is norm_summable iff rseq1 is summable ) by Def3; ::_thesis: verum end; theorem :: LOPBAN_3:34 for X being RealNormSpace for seq being sequence of X for p being Real st p > 1 & ( for n being Element of NAT st n >= 1 holds ||.seq.|| . n = 1 / (n to_power p) ) holds seq is norm_summable proof let X be RealNormSpace; ::_thesis: for seq being sequence of X for p being Real st p > 1 & ( for n being Element of NAT st n >= 1 holds ||.seq.|| . n = 1 / (n to_power p) ) holds seq is norm_summable let seq be sequence of X; ::_thesis: for p being Real st p > 1 & ( for n being Element of NAT st n >= 1 holds ||.seq.|| . n = 1 / (n to_power p) ) holds seq is norm_summable let p be Real; ::_thesis: ( p > 1 & ( for n being Element of NAT st n >= 1 holds ||.seq.|| . n = 1 / (n to_power p) ) implies seq is norm_summable ) assume ( p > 1 & ( for n being Element of NAT st n >= 1 holds ||.seq.|| . n = 1 / (n to_power p) ) ) ; ::_thesis: seq is norm_summable then ||.seq.|| is summable by SERIES_1:32; hence seq is norm_summable by Def3; ::_thesis: verum end; theorem :: LOPBAN_3:35 for X being RealNormSpace for seq being sequence of X for p being Real st p <= 1 & ( for n being Element of NAT st n >= 1 holds ||.seq.|| . n = 1 / (n to_power p) ) holds not seq is norm_summable by SERIES_1:33; theorem :: LOPBAN_3:36 for X being RealNormSpace for seq being sequence of X for rseq1 being Real_Sequence st ( for n being Element of NAT holds ( seq . n <> 0. X & rseq1 . n = (||.seq.|| . (n + 1)) / (||.seq.|| . n) ) ) & rseq1 is convergent & lim rseq1 < 1 holds seq is norm_summable proof let X be RealNormSpace; ::_thesis: for seq being sequence of X for rseq1 being Real_Sequence st ( for n being Element of NAT holds ( seq . n <> 0. X & rseq1 . n = (||.seq.|| . (n + 1)) / (||.seq.|| . n) ) ) & rseq1 is convergent & lim rseq1 < 1 holds seq is norm_summable let seq be sequence of X; ::_thesis: for rseq1 being Real_Sequence st ( for n being Element of NAT holds ( seq . n <> 0. X & rseq1 . n = (||.seq.|| . (n + 1)) / (||.seq.|| . n) ) ) & rseq1 is convergent & lim rseq1 < 1 holds seq is norm_summable let rseq1 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds ( seq . n <> 0. X & rseq1 . n = (||.seq.|| . (n + 1)) / (||.seq.|| . n) ) ) & rseq1 is convergent & lim rseq1 < 1 implies seq is norm_summable ) assume that A1: for n being Element of NAT holds ( seq . n <> 0. X & rseq1 . n = (||.seq.|| . (n + 1)) / (||.seq.|| . n) ) and A2: ( rseq1 is convergent & lim rseq1 < 1 ) ; ::_thesis: seq is norm_summable now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_||.seq.||_._n_<>_0_&_rseq1_._n_=_((abs_||.seq.||)_._(n_+_1))_/_((abs_||.seq.||)_._n)_) let n be Element of NAT ; ::_thesis: ( ||.seq.|| . n <> 0 & rseq1 . n = ((abs ||.seq.||) . (n + 1)) / ((abs ||.seq.||) . n) ) A3: 0 <= ||.seq.|| . n by Th2; A4: 0 <= ||.seq.|| . (n + 1) by Th2; A5: (abs ||.seq.||) . (n + 1) = abs (||.seq.|| . (n + 1)) by SEQ_1:12 .= ||.seq.|| . (n + 1) by A4, ABSVALUE:def_1 ; A6: ( seq . n <> 0. X & ||.seq.|| . n = ||.(seq . n).|| ) by A1, NORMSP_0:def_4; (abs ||.seq.||) . n = abs (||.seq.|| . n) by SEQ_1:12 .= ||.seq.|| . n by A3, ABSVALUE:def_1 ; hence ( ||.seq.|| . n <> 0 & rseq1 . n = ((abs ||.seq.||) . (n + 1)) / ((abs ||.seq.||) . n) ) by A1, A5, A6, NORMSP_0:def_5; ::_thesis: verum end; then ||.seq.|| is absolutely_summable by A2, SERIES_1:37; then A7: abs ||.seq.|| is summable by SERIES_1:def_4; now__::_thesis:_for_n_being_Element_of_NAT_holds_(abs_||.seq.||)_._n_=_||.seq.||_._n let n be Element of NAT ; ::_thesis: (abs ||.seq.||) . n = ||.seq.|| . n A8: 0 <= ||.seq.|| . n by Th2; thus (abs ||.seq.||) . n = abs (||.seq.|| . n) by SEQ_1:12 .= ||.seq.|| . n by A8, ABSVALUE:def_1 ; ::_thesis: verum end; then abs ||.seq.|| = ||.seq.|| by FUNCT_2:63; hence seq is norm_summable by A7, Def3; ::_thesis: verum end; theorem :: LOPBAN_3:37 for X being RealNormSpace 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 norm_summable proof let X be RealNormSpace; ::_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 norm_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 norm_summable ) assume that A1: for n being Element of NAT holds seq . n <> 0. X and A2: ex m being Element of NAT st for n being Element of NAT st n >= m holds (||.seq.|| . (n + 1)) / (||.seq.|| . n) >= 1 ; ::_thesis: not seq is norm_summable consider m being Element of NAT such that A3: for n being Element of NAT st n >= m holds (||.seq.|| . (n + 1)) / (||.seq.|| . n) >= 1 by A2; A4: now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_m_holds_ ((abs_||.seq.||)_._(n_+_1))_/_((abs_||.seq.||)_._n)_>=_1 let n be Element of NAT ; ::_thesis: ( n >= m implies ((abs ||.seq.||) . (n + 1)) / ((abs ||.seq.||) . n) >= 1 ) assume A5: n >= m ; ::_thesis: ((abs ||.seq.||) . (n + 1)) / ((abs ||.seq.||) . n) >= 1 A6: 0 <= ||.seq.|| . n by Th2; A7: 0 <= ||.seq.|| . (n + 1) by Th2; A8: (abs ||.seq.||) . (n + 1) = abs (||.seq.|| . (n + 1)) by SEQ_1:12 .= ||.seq.|| . (n + 1) by A7, ABSVALUE:def_1 ; (abs ||.seq.||) . n = abs (||.seq.|| . n) by SEQ_1:12 .= ||.seq.|| . n by A6, ABSVALUE:def_1 ; hence ((abs ||.seq.||) . (n + 1)) / ((abs ||.seq.||) . n) >= 1 by A3, A5, A8; ::_thesis: verum end; now__::_thesis:_for_n_being_Element_of_NAT_holds_||.seq.||_._n_<>_0 let n be Element of NAT ; ::_thesis: ||.seq.|| . n <> 0 seq . n <> 0. X by A1; then ||.(seq . n).|| <> 0 by NORMSP_0:def_5; hence ||.seq.|| . n <> 0 by NORMSP_0:def_4; ::_thesis: verum end; hence not ||.seq.|| is summable by A4, SERIES_1:39; :: according to LOPBAN_3:def_3 ::_thesis: verum end; registration let X be RealBanachSpace; cluster Function-like V30( NAT , the carrier of X) norm_summable -> summable for Element of K32(K33(NAT, the carrier of X)); coherence for b1 being sequence of X st b1 is norm_summable holds b1 is summable by Th26; end; begin theorem Th38: :: LOPBAN_3:38 for X being Banach_Algebra for x, y, z being Element of X for a, b being Real holds ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. X) = x & ex t being Element of X st x + t = 0. X & (x * y) * z = x * (y * z) & 1 * x = x & 0 * x = 0. X & a * (0. X) = 0. X & (- 1) * x = - x & x * (1. X) = x & (1. X) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) & a * (x * y) = x * (a * y) & (0. X) * x = 0. X & x * (0. X) = 0. X & x * (y - z) = (x * y) - (x * z) & (y - z) * x = (y * x) - (z * x) & (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete ) proof let X be Banach_Algebra; ::_thesis: for x, y, z being Element of X for a, b being Real holds ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. X) = x & ex t being Element of X st x + t = 0. X & (x * y) * z = x * (y * z) & 1 * x = x & 0 * x = 0. X & a * (0. X) = 0. X & (- 1) * x = - x & x * (1. X) = x & (1. X) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) & a * (x * y) = x * (a * y) & (0. X) * x = 0. X & x * (0. X) = 0. X & x * (y - z) = (x * y) - (x * z) & (y - z) * x = (y * x) - (z * x) & (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete ) let x, y, z be Element of X; ::_thesis: for a, b being Real holds ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. X) = x & ex t being Element of X st x + t = 0. X & (x * y) * z = x * (y * z) & 1 * x = x & 0 * x = 0. X & a * (0. X) = 0. X & (- 1) * x = - x & x * (1. X) = x & (1. X) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) & a * (x * y) = x * (a * y) & (0. X) * x = 0. X & x * (0. X) = 0. X & x * (y - z) = (x * y) - (x * z) & (y - z) * x = (y * x) - (z * x) & (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete ) let a, b be Real; ::_thesis: ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. X) = x & ex t being Element of X st x + t = 0. X & (x * y) * z = x * (y * z) & 1 * x = x & 0 * x = 0. X & a * (0. X) = 0. X & (- 1) * x = - x & x * (1. X) = x & (1. X) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) & a * (x * y) = x * (a * y) & (0. X) * x = 0. X & x * (0. X) = 0. X & x * (y - z) = (x * y) - (x * z) & (y - z) * x = (y * x) - (z * x) & (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete ) thus x + y = y + x ; ::_thesis: ( (x + y) + z = x + (y + z) & x + (0. X) = x & ex t being Element of X st x + t = 0. X & (x * y) * z = x * (y * z) & 1 * x = x & 0 * x = 0. X & a * (0. X) = 0. X & (- 1) * x = - x & x * (1. X) = x & (1. X) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) & a * (x * y) = x * (a * y) & (0. X) * x = 0. X & x * (0. X) = 0. X & x * (y - z) = (x * y) - (x * z) & (y - z) * x = (y * x) - (z * x) & (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete ) thus (x + y) + z = x + (y + z) by RLVECT_1:def_3; ::_thesis: ( x + (0. X) = x & ex t being Element of X st x + t = 0. X & (x * y) * z = x * (y * z) & 1 * x = x & 0 * x = 0. X & a * (0. X) = 0. X & (- 1) * x = - x & x * (1. X) = x & (1. X) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) & a * (x * y) = x * (a * y) & (0. X) * x = 0. X & x * (0. X) = 0. X & x * (y - z) = (x * y) - (x * z) & (y - z) * x = (y * x) - (z * x) & (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete ) thus x + (0. X) = x by RLVECT_1:def_4; ::_thesis: ( ex t being Element of X st x + t = 0. X & (x * y) * z = x * (y * z) & 1 * x = x & 0 * x = 0. X & a * (0. X) = 0. X & (- 1) * x = - x & x * (1. X) = x & (1. X) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) & a * (x * y) = x * (a * y) & (0. X) * x = 0. X & x * (0. X) = 0. X & x * (y - z) = (x * y) - (x * z) & (y - z) * x = (y * x) - (z * x) & (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete ) thus ex t being Element of X st x + t = 0. X by ALGSTR_0:def_11; ::_thesis: ( (x * y) * z = x * (y * z) & 1 * x = x & 0 * x = 0. X & a * (0. X) = 0. X & (- 1) * x = - x & x * (1. X) = x & (1. X) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) & a * (x * y) = x * (a * y) & (0. X) * x = 0. X & x * (0. X) = 0. X & x * (y - z) = (x * y) - (x * z) & (y - z) * x = (y * x) - (z * x) & (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete ) thus (x * y) * z = x * (y * z) by GROUP_1:def_3; ::_thesis: ( 1 * x = x & 0 * x = 0. X & a * (0. X) = 0. X & (- 1) * x = - x & x * (1. X) = x & (1. X) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) & a * (x * y) = x * (a * y) & (0. X) * x = 0. X & x * (0. X) = 0. X & x * (y - z) = (x * y) - (x * z) & (y - z) * x = (y * x) - (z * x) & (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete ) thus 1 * x = x by RLVECT_1:def_8; ::_thesis: ( 0 * x = 0. X & a * (0. X) = 0. X & (- 1) * x = - x & x * (1. X) = x & (1. X) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) & a * (x * y) = x * (a * y) & (0. X) * x = 0. X & x * (0. X) = 0. X & x * (y - z) = (x * y) - (x * z) & (y - z) * x = (y * x) - (z * x) & (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete ) thus 0 * x = 0. X by RLVECT_1:10; ::_thesis: ( a * (0. X) = 0. X & (- 1) * x = - x & x * (1. X) = x & (1. X) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) & a * (x * y) = x * (a * y) & (0. X) * x = 0. X & x * (0. X) = 0. X & x * (y - z) = (x * y) - (x * z) & (y - z) * x = (y * x) - (z * x) & (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete ) thus a * (0. X) = 0. X by RLVECT_1:10; ::_thesis: ( (- 1) * x = - x & x * (1. X) = x & (1. X) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) & a * (x * y) = x * (a * y) & (0. X) * x = 0. X & x * (0. X) = 0. X & x * (y - z) = (x * y) - (x * z) & (y - z) * x = (y * x) - (z * x) & (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete ) thus (- 1) * x = - x by RLVECT_1:16; ::_thesis: ( x * (1. X) = x & (1. X) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) & a * (x * y) = x * (a * y) & (0. X) * x = 0. X & x * (0. X) = 0. X & x * (y - z) = (x * y) - (x * z) & (y - z) * x = (y * x) - (z * x) & (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete ) thus ( x * (1. X) = x & (1. X) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) ) by FUNCSDOM:def_9, RLVECT_1:def_5, RLVECT_1:def_6, RLVECT_1:def_7, VECTSP_1:def_2, VECTSP_1:def_3, VECTSP_1:def_4, VECTSP_1:def_8; ::_thesis: ( (a * b) * (x * y) = (a * x) * (b * y) & a * (x * y) = x * (a * y) & (0. X) * x = 0. X & x * (0. X) = 0. X & x * (y - z) = (x * y) - (x * z) & (y - z) * x = (y * x) - (z * x) & (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete ) thus (a * b) * (x * y) = a * (b * (x * y)) by RLVECT_1:def_7 .= a * (x * (b * y)) by LOPBAN_2:def_11 .= (a * x) * (b * y) by FUNCSDOM:def_9 ; ::_thesis: ( a * (x * y) = x * (a * y) & (0. X) * x = 0. X & x * (0. X) = 0. X & x * (y - z) = (x * y) - (x * z) & (y - z) * x = (y * x) - (z * x) & (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete ) thus a * (x * y) = x * (a * y) by LOPBAN_2:def_11; ::_thesis: ( (0. X) * x = 0. X & x * (0. X) = 0. X & x * (y - z) = (x * y) - (x * z) & (y - z) * x = (y * x) - (z * x) & (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete ) A1: (x * (y - z)) + (x * z) = x * ((y - z) + z) by VECTSP_1:def_2 .= x * (y - (z - z)) by RLVECT_1:29 .= x * (y - (0. X)) by RLVECT_1:15 .= x * y by RLVECT_1:13 ; x * (0. X) = x * ((0. X) + (0. X)) by RLVECT_1:def_4 .= (x * (0. X)) + (x * (0. X)) by VECTSP_1:def_2 ; then 0. X = ((x * (0. X)) + (x * (0. X))) - (x * (0. X)) by RLVECT_1:15; then 0. X = (x * (0. X)) + ((x * (0. X)) - (x * (0. X))) by RLVECT_1:def_3; then A2: 0. X = (x * (0. X)) + (0. X) by RLVECT_1:15; (0. X) * x = ((0. X) + (0. X)) * x by RLVECT_1:def_4 .= ((0. X) * x) + ((0. X) * x) by VECTSP_1:def_3 ; then 0. X = (((0. X) * x) + ((0. X) * x)) - ((0. X) * x) by RLVECT_1:15; then 0. X = ((0. X) * x) + (((0. X) * x) - ((0. X) * x)) by RLVECT_1:def_3; then 0. X = ((0. X) * x) + (0. X) by RLVECT_1:15; hence ( (0. X) * x = 0. X & x * (0. X) = 0. X ) by A2, RLVECT_1:def_4; ::_thesis: ( x * (y - z) = (x * y) - (x * z) & (y - z) * x = (y * x) - (z * x) & (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete ) thus x * (y - z) = (x * (y - z)) + (0. X) by RLVECT_1:4 .= (x * (y - z)) + ((x * z) - (x * z)) by RLVECT_1:15 .= (x * y) - (x * z) by A1, RLVECT_1:def_3 ; ::_thesis: ( (y - z) * x = (y * x) - (z * x) & (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete ) A3: ((y - z) * x) + (z * x) = ((y - z) + z) * x by VECTSP_1:def_3 .= (y - (z - z)) * x by RLVECT_1:29 .= (y - (0. X)) * x by RLVECT_1:15 .= y * x by RLVECT_1:13 ; thus (y - z) * x = ((y - z) * x) + (0. X) by RLVECT_1:4 .= ((y - z) * x) + ((z * x) - (z * x)) by RLVECT_1:15 .= (y * x) - (z * x) by A3, RLVECT_1:def_3 ; ::_thesis: ( (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete ) thus (x + y) - z = x + (y - z) by RLVECT_1:def_3; ::_thesis: ( (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete ) thus (x - y) + z = x - (y - z) by RLVECT_1:29; ::_thesis: ( (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete ) thus (x - y) - z = x - (y + z) by RLVECT_1:27; ::_thesis: ( x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete ) thus (x - z) + (z + y) = ((x - z) + z) + y by RLVECT_1:def_3 .= (x - (z - z)) + y by RLVECT_1:29 .= (x - (0. X)) + y by RLVECT_1:15 .= x + y by RLVECT_1:13 ; ::_thesis: ( x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete ) thus (x - z) + (z - y) = ((x - z) + z) - y by RLVECT_1:def_3 .= (x - (z - z)) - y by RLVECT_1:29 .= (x - (0. X)) - y by RLVECT_1:15 .= x - y by RLVECT_1:13 ; ::_thesis: ( x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete ) thus (x - y) + y = x - (y - y) by RLVECT_1:29 .= x - (0. X) by RLVECT_1:15 .= x by RLVECT_1:13 ; ::_thesis: ( x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete ) thus y - (y - x) = (y - y) + x by RLVECT_1:29 .= (0. X) + x by RLVECT_1:15 .= x by RLVECT_1:4 ; ::_thesis: ( ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete ) thus ( ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| ) by LOPBAN_2:def_9, NORMSP_0:def_5, NORMSP_1:def_1; ::_thesis: ( ||.(1. X).|| = 1 & X is complete ) thus ( ||.(1. X).|| = 1 & X is complete ) by LOPBAN_2:def_10; ::_thesis: verum end; registration cluster non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V133() V134() RealNormSpace-like V150() associative right-distributive right_unital Banach_Algebra-like -> well-unital for Normed_AlgebraStr ; coherence for b1 being Banach_Algebra holds b1 is well-unital proof let X be Banach_Algebra; ::_thesis: X is well-unital let x be Element of X; :: according to VECTSP_1:def_6 ::_thesis: ( x * (1. X) = x & (1. X) * x = x ) thus ( x * (1. X) = x & (1. X) * x = x ) by Th38; ::_thesis: verum end; end; definition let X be non empty associative well-unital multLoopStr ; let v be Element of X; redefine attr v is invertible means :Def4: :: LOPBAN_3:def 4 ex w being Element of X st ( v * w = 1. X & w * v = 1. X ); compatibility ( v is invertible iff ex w being Element of X st ( v * w = 1. X & w * v = 1. X ) ) proof thus ( v is invertible implies ex w being Element of X st ( v * w = 1. X & w * v = 1. X ) ) ::_thesis: ( ex w being Element of X st ( v * w = 1. X & w * v = 1. X ) implies v is invertible ) proof assume A1: v is invertible ; ::_thesis: ex w being Element of X st ( v * w = 1. X & w * v = 1. X ) then consider y being Element of X such that A2: v * y = 1. X by ALGSTR_0:def_28; take y ; ::_thesis: ( v * y = 1. X & y * v = 1. X ) thus v * y = 1. X by A2; ::_thesis: y * v = 1. X consider x being Element of X such that A3: x * v = 1. X by A1, ALGSTR_0:def_27; x = x * (1. X) by VECTSP_1:def_6 .= (1. X) * y by A2, A3, GROUP_1:def_3 .= y by VECTSP_1:def_6 ; hence y * v = 1. X by A3; ::_thesis: verum end; given w being Element of X such that A4: ( v * w = 1. X & w * v = 1. X ) ; ::_thesis: v is invertible thus ( v is right_invertible & v is left_invertible ) by A4, ALGSTR_0:def_27, ALGSTR_0:def_28; :: according to ALGSTR_0:def_29 ::_thesis: verum end; end; :: deftheorem Def4 defines invertible LOPBAN_3:def_4_:_ for X being non empty associative well-unital multLoopStr for v being Element of X holds ( v is invertible iff ex w being Element of X st ( v * w = 1. X & w * v = 1. X ) ); definition let X be non empty Normed_AlgebraStr ; let S be sequence of X; let a be Element of X; funca * S -> sequence of X means :: LOPBAN_3:def 5 for n being Element of NAT holds it . n = a * (S . n); existence ex b1 being sequence of X st for n being Element of NAT holds b1 . n = a * (S . n) proof deffunc H1( Element of NAT ) -> Element of the carrier of X = a * (S . $1); ex S being sequence of X st for n being Element of NAT holds S . n = H1(n) from FUNCT_2:sch_4(); hence ex b1 being sequence of X st for n being Element of NAT holds b1 . n = a * (S . n) ; ::_thesis: verum end; uniqueness for b1, b2 being sequence of X st ( for n being Element of NAT holds b1 . n = a * (S . n) ) & ( for n being Element of NAT holds b2 . n = a * (S . n) ) holds b1 = b2 proof let S1, S2 be sequence of X; ::_thesis: ( ( for n being Element of NAT holds S1 . n = a * (S . n) ) & ( for n being Element of NAT holds S2 . n = a * (S . n) ) implies S1 = S2 ) assume that A1: for n being Element of NAT holds S1 . n = a * (S . n) and A2: for n being Element of NAT holds S2 . n = a * (S . n) ; ::_thesis: S1 = S2 for n being Element of NAT holds S1 . n = S2 . n proof let n be Element of NAT ; ::_thesis: S1 . n = S2 . n S1 . n = a * (S . n) by A1; hence S1 . n = S2 . n by A2; ::_thesis: verum end; hence S1 = S2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem defines * LOPBAN_3:def_5_:_ for X being non empty Normed_AlgebraStr for S being sequence of X for a being Element of X for b4 being sequence of X holds ( b4 = a * S iff for n being Element of NAT holds b4 . n = a * (S . n) ); definition let X be non empty Normed_AlgebraStr ; let S be sequence of X; let a be Element of X; funcS * a -> sequence of X means :: LOPBAN_3:def 6 for n being Element of NAT holds it . n = (S . n) * a; existence ex b1 being sequence of X st for n being Element of NAT holds b1 . n = (S . n) * a proof deffunc H1( Element of NAT ) -> Element of the carrier of X = (S . $1) * a; ex S being sequence of X st for n being Element of NAT holds S . n = H1(n) from FUNCT_2:sch_4(); hence ex b1 being sequence of X st for n being Element of NAT holds b1 . n = (S . n) * a ; ::_thesis: verum end; uniqueness for b1, b2 being sequence of X st ( for n being Element of NAT holds b1 . n = (S . n) * a ) & ( for n being Element of NAT holds b2 . n = (S . n) * a ) holds b1 = b2 proof let S1, S2 be sequence of X; ::_thesis: ( ( for n being Element of NAT holds S1 . n = (S . n) * a ) & ( for n being Element of NAT holds S2 . n = (S . n) * a ) implies S1 = S2 ) assume that A1: for n being Element of NAT holds S1 . n = (S . n) * a and A2: for n being Element of NAT holds S2 . n = (S . n) * a ; ::_thesis: S1 = S2 for n being Element of NAT holds S1 . n = S2 . n proof let n be Element of NAT ; ::_thesis: S1 . n = S2 . n S1 . n = (S . n) * a by A1; hence S1 . n = S2 . n by A2; ::_thesis: verum end; hence S1 = S2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem defines * LOPBAN_3:def_6_:_ for X being non empty Normed_AlgebraStr for S being sequence of X for a being Element of X for b4 being sequence of X holds ( b4 = S * a iff for n being Element of NAT holds b4 . n = (S . n) * a ); definition let X be non empty Normed_AlgebraStr ; let seq1, seq2 be sequence of X; funcseq1 * seq2 -> sequence of X means :: LOPBAN_3:def 7 for n being Element of NAT holds it . n = (seq1 . n) * (seq2 . n); existence ex b1 being sequence of X st for n being Element of NAT holds b1 . n = (seq1 . n) * (seq2 . n) proof deffunc H1( Element of NAT ) -> Element of the carrier of X = (seq1 . $1) * (seq2 . $1); ex S being sequence of X st for n being Element of NAT holds S . n = H1(n) from FUNCT_2:sch_4(); hence ex b1 being sequence of X st for n being Element of NAT holds b1 . n = (seq1 . n) * (seq2 . n) ; ::_thesis: verum end; uniqueness for b1, b2 being sequence of X st ( for n being Element of NAT holds b1 . n = (seq1 . n) * (seq2 . n) ) & ( for n being Element of NAT holds b2 . n = (seq1 . n) * (seq2 . n) ) holds b1 = b2 proof let S1, S2 be sequence of X; ::_thesis: ( ( for n being Element of NAT holds S1 . n = (seq1 . n) * (seq2 . n) ) & ( for n being Element of NAT holds S2 . n = (seq1 . n) * (seq2 . n) ) implies S1 = S2 ) assume that A1: for n being Element of NAT holds S1 . n = (seq1 . n) * (seq2 . n) and A2: for n being Element of NAT holds S2 . n = (seq1 . n) * (seq2 . n) ; ::_thesis: S1 = S2 for n being Element of NAT holds S1 . n = S2 . n proof let n be Element of NAT ; ::_thesis: S1 . n = S2 . n S1 . n = (seq1 . n) * (seq2 . n) by A1; hence S1 . n = S2 . n by A2; ::_thesis: verum end; hence S1 = S2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem defines * LOPBAN_3:def_7_:_ for X being non empty Normed_AlgebraStr for seq1, seq2, b4 being sequence of X holds ( b4 = seq1 * seq2 iff for n being Element of NAT holds b4 . n = (seq1 . n) * (seq2 . n) ); notation let X be non empty associative well-unital multLoopStr ; let x be Element of X; synonym x " for / x; end; definition let X be non empty associative well-unital multLoopStr ; let x be Element of X; assume B1: x is invertible ; redefine func / x means :Def8: :: LOPBAN_3:def 8 ( x * it = 1. X & it * x = 1. X ); compatibility for b1 being Element of the carrier of X holds ( b1 = x " iff ( x * b1 = 1. X & b1 * x = 1. X ) ) proof let y be Element of X; ::_thesis: ( y = x " iff ( x * y = 1. X & y * x = 1. X ) ) consider x1 being Element of X such that A1: x * x1 = 1. X by B1, ALGSTR_0:def_28; A2: x is right_mult-cancelable proof let y, z be Element of X; :: according to ALGSTR_0:def_21 ::_thesis: ( not y * x = z * x or y = z ) assume A3: y * x = z * x ; ::_thesis: y = z thus y = y * (1. X) by VECTSP_1:def_6 .= (z * x) * x1 by A1, A3, GROUP_1:def_3 .= z * (1. X) by A1, GROUP_1:def_3 .= z by VECTSP_1:def_6 ; ::_thesis: verum end; thus ( y = x " implies ( x * y = 1. X & y * x = 1. X ) ) ::_thesis: ( x * y = 1. X & y * x = 1. X implies y = x " ) proof assume A4: y = x " ; ::_thesis: ( x * y = 1. X & y * x = 1. X ) y = y * (1. X) by VECTSP_1:def_6 .= (y * x) * x1 by A1, GROUP_1:def_3 .= (1. X) * x1 by B1, A2, A4, ALGSTR_0:def_30 .= x1 by VECTSP_1:def_6 ; hence x * y = 1. X by A1; ::_thesis: y * x = 1. X thus y * x = 1. X by B1, A2, A4, ALGSTR_0:def_30; ::_thesis: verum end; thus ( x * y = 1. X & y * x = 1. X implies y = x " ) by B1, A2, ALGSTR_0:def_30; ::_thesis: verum end; end; :: deftheorem Def8 defines " LOPBAN_3:def_8_:_ for X being non empty associative well-unital multLoopStr for x being Element of X st x is invertible holds for b3 being Element of the carrier of X holds ( b3 = x " iff ( x * b3 = 1. X & b3 * x = 1. X ) ); definition let X be Banach_Algebra; let z be Element of X; funcz GeoSeq -> sequence of X means :Def9: :: LOPBAN_3:def 9 ( it . 0 = 1. X & ( for n being Element of NAT holds it . (n + 1) = (it . n) * z ) ); existence ex b1 being sequence of X st ( b1 . 0 = 1. X & ( for n being Element of NAT holds b1 . (n + 1) = (b1 . n) * z ) ) proof deffunc H1( set , set ) -> set = the multF of X . [$2,z]; consider g being Function such that A1: ( dom g = NAT & g . 0 = 1. X & ( for n being Nat holds g . (n + 1) = H1(n,g . n) ) ) from NAT_1:sch_11(); defpred S1[ Element of NAT ] means g . $1 in the carrier of X; A2: 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 S1[k] ; ::_thesis: S1[k + 1] then reconsider gk = g . k as Element of X ; g . (k + 1) = the multF of X . [gk,z] by A1; hence S1[k + 1] ; ::_thesis: verum end; A3: S1[ 0 ] by A1; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A2); then for n being set st n in NAT holds g . n in the carrier of X ; then reconsider g0 = g as sequence of X by A1, FUNCT_2:3; take g0 ; ::_thesis: ( g0 . 0 = 1. X & ( for n being Element of NAT holds g0 . (n + 1) = (g0 . n) * z ) ) thus ( g0 . 0 = 1. X & ( for n being Element of NAT holds g0 . (n + 1) = (g0 . n) * z ) ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being sequence of X st b1 . 0 = 1. X & ( for n being Element of NAT holds b1 . (n + 1) = (b1 . n) * z ) & b2 . 0 = 1. X & ( for n being Element of NAT holds b2 . (n + 1) = (b2 . n) * z ) holds b1 = b2 proof let seq1, seq2 be sequence of X; ::_thesis: ( seq1 . 0 = 1. X & ( for n being Element of NAT holds seq1 . (n + 1) = (seq1 . n) * z ) & seq2 . 0 = 1. X & ( for n being Element of NAT holds seq2 . (n + 1) = (seq2 . n) * z ) implies seq1 = seq2 ) assume that A4: seq1 . 0 = 1. X and A5: for n being Element of NAT holds seq1 . (n + 1) = (seq1 . n) * z and A6: seq2 . 0 = 1. X and A7: for n being Element of NAT holds seq2 . (n + 1) = (seq2 . n) * z ; ::_thesis: seq1 = seq2 defpred S1[ Element of NAT ] means seq1 . $1 = seq2 . $1; A8: 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 S1[k] ; ::_thesis: S1[k + 1] hence seq1 . (k + 1) = (seq2 . k) * z by A5 .= seq2 . (k + 1) by A7 ; ::_thesis: verum end; A9: S1[ 0 ] by A4, A6; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A9, A8); hence seq1 = seq2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def9 defines GeoSeq LOPBAN_3:def_9_:_ for X being Banach_Algebra for z being Element of X for b3 being sequence of X holds ( b3 = z GeoSeq iff ( b3 . 0 = 1. X & ( for n being Element of NAT holds b3 . (n + 1) = (b3 . n) * z ) ) ); definition let X be Banach_Algebra; let z be Element of X; let n be Element of NAT ; funcz #N n -> Element of X equals :: LOPBAN_3:def 10 (z GeoSeq) . n; correctness coherence (z GeoSeq) . n is Element of X; ; end; :: deftheorem defines #N LOPBAN_3:def_10_:_ for X being Banach_Algebra for z being Element of X for n being Element of NAT holds z #N n = (z GeoSeq) . n; theorem :: LOPBAN_3:39 for X being Banach_Algebra for z being Element of X holds z #N 0 = 1. X by Def9; theorem Th40: :: LOPBAN_3:40 for X being Banach_Algebra for z being Element of X st ||.z.|| < 1 holds ( z GeoSeq is summable & z GeoSeq is norm_summable ) proof let X be Banach_Algebra; ::_thesis: for z being Element of X st ||.z.|| < 1 holds ( z GeoSeq is summable & z GeoSeq is norm_summable ) let z be Element of X; ::_thesis: ( ||.z.|| < 1 implies ( z GeoSeq is summable & z GeoSeq is norm_summable ) ) A1: for n being Element of NAT holds ( 0 <= ||.(z GeoSeq).|| . n & ||.(z GeoSeq).|| . n <= (||.z.|| GeoSeq) . n ) proof defpred S1[ Element of NAT ] means ( 0 <= ||.(z GeoSeq).|| . $1 & ||.(z GeoSeq).|| . $1 <= (||.z.|| GeoSeq) . $1 ); A2: ||.(z GeoSeq).|| . 0 = ||.((z GeoSeq) . 0).|| by NORMSP_0:def_4; A3: 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] ) ||.(((z GeoSeq) . k) * z).|| <= ||.((z GeoSeq) . k).|| * ||.z.|| by LOPBAN_2:def_9; then A4: ||.(((z GeoSeq) . k) * z).|| <= (||.(z GeoSeq).|| . k) * ||.z.|| by NORMSP_0:def_4; assume S1[k] ; ::_thesis: S1[k + 1] then (||.(z GeoSeq).|| . k) * ||.z.|| <= ((||.z.|| GeoSeq) . k) * ||.z.|| by XREAL_1:64; then A5: ||.(((z GeoSeq) . k) * z).|| <= ((||.z.|| GeoSeq) . k) * ||.z.|| by A4, XXREAL_0:2; ||.(z GeoSeq).|| . (k + 1) = ||.((z GeoSeq) . (k + 1)).|| by NORMSP_0:def_4 .= ||.(((z GeoSeq) . k) * z).|| by Def9 ; hence S1[k + 1] by A5, PREPOWER:3; ::_thesis: verum end; ||.((z GeoSeq) . 0).|| = ||.(1. X).|| by Def9 .= 1 by LOPBAN_2:def_10 .= (||.z.|| GeoSeq) . 0 by PREPOWER:3 ; then A6: S1[ 0 ] by A2; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A6, A3); hence for n being Element of NAT holds ( 0 <= ||.(z GeoSeq).|| . n & ||.(z GeoSeq).|| . n <= (||.z.|| GeoSeq) . n ) ; ::_thesis: verum end; assume ||.z.|| < 1 ; ::_thesis: ( z GeoSeq is summable & z GeoSeq is norm_summable ) then abs ||.z.|| < 1 by ABSVALUE:def_1; then ||.z.|| GeoSeq is summable by SERIES_1:24; then ||.(z GeoSeq).|| is summable by A1, SERIES_1:20; then z GeoSeq is norm_summable by Def3; hence ( z GeoSeq is summable & z GeoSeq is norm_summable ) ; ::_thesis: verum end; theorem :: LOPBAN_3:41 for X being Banach_Algebra for x being Point of X st ||.((1. X) - x).|| < 1 holds ( ((1. X) - x) GeoSeq is summable & ((1. X) - x) GeoSeq is norm_summable ) by Th40; Lm1: for X being RealNormSpace for x being Point of X st ( for e being Real st e > 0 holds ||.x.|| < e ) holds x = 0. X proof let X be RealNormSpace; ::_thesis: for x being Point of X st ( for e being Real st e > 0 holds ||.x.|| < e ) holds x = 0. X let x be Point of X; ::_thesis: ( ( for e being Real st e > 0 holds ||.x.|| < e ) implies x = 0. X ) assume A1: for e being Real st e > 0 holds ||.x.|| < e ; ::_thesis: x = 0. X now__::_thesis:_not_x_<>_0._X assume x <> 0. X ; ::_thesis: contradiction then 0 <> ||.x.|| by NORMSP_0:def_5; then 0 < ||.x.|| ; hence contradiction by A1; ::_thesis: verum end; hence x = 0. X ; ::_thesis: verum end; Lm2: for X being RealNormSpace for x, y being Point of X st ( for e being Real st e > 0 holds ||.(x - y).|| < e ) holds x = y proof let X be RealNormSpace; ::_thesis: for x, y being Point of X st ( for e being Real st e > 0 holds ||.(x - y).|| < e ) holds x = y let x, y be Point of X; ::_thesis: ( ( for e being Real st e > 0 holds ||.(x - y).|| < e ) implies x = y ) assume for e being Real st e > 0 holds ||.(x - y).|| < e ; ::_thesis: x = y then x - y = 0. X by Lm1; hence x = y by RLVECT_1:21; ::_thesis: verum end; Lm3: for X being RealNormSpace for x, y being Point of X for seq being Real_Sequence st seq is convergent & lim seq = 0 & ( for n being Element of NAT holds ||.(x - y).|| <= seq . n ) holds x = y proof let X be RealNormSpace; ::_thesis: for x, y being Point of X for seq being Real_Sequence st seq is convergent & lim seq = 0 & ( for n being Element of NAT holds ||.(x - y).|| <= seq . n ) holds x = y let x, y be Point of X; ::_thesis: for seq being Real_Sequence st seq is convergent & lim seq = 0 & ( for n being Element of NAT holds ||.(x - y).|| <= seq . n ) holds x = y let seq be Real_Sequence; ::_thesis: ( seq is convergent & lim seq = 0 & ( for n being Element of NAT holds ||.(x - y).|| <= seq . n ) implies x = y ) assume that A1: ( seq is convergent & lim seq = 0 ) and A2: for n being Element of NAT holds ||.(x - y).|| <= seq . n ; ::_thesis: x = y now__::_thesis:_for_e_being_Real_st_0_<_e_holds_ ||.(x_-_y).||_<_e let e be Real; ::_thesis: ( 0 < e implies ||.(x - y).|| < e ) assume 0 < e ; ::_thesis: ||.(x - y).|| < e then consider n being Element of NAT such that A3: for m being Element of NAT st n <= m holds abs ((seq . m) - 0) < e by A1, SEQ_2:def_7; A4: seq . n <= abs (seq . n) by ABSVALUE:4; A5: ||.(x - y).|| <= seq . n by A2; abs ((seq . n) - 0) < e by A3; then seq . n < e by A4, XXREAL_0:2; hence ||.(x - y).|| < e by A5, XXREAL_0:2; ::_thesis: verum end; hence x = y by Lm2; ::_thesis: verum end; theorem :: LOPBAN_3:42 for X being Banach_Algebra for x being Point of X st ||.((1. X) - x).|| < 1 holds ( x is invertible & x " = Sum (((1. X) - x) GeoSeq) ) proof let X be Banach_Algebra; ::_thesis: for x being Point of X st ||.((1. X) - x).|| < 1 holds ( x is invertible & x " = Sum (((1. X) - x) GeoSeq) ) let x be Point of X; ::_thesis: ( ||.((1. X) - x).|| < 1 implies ( x is invertible & x " = Sum (((1. X) - x) GeoSeq) ) ) assume A1: ||.((1. X) - x).|| < 1 ; ::_thesis: ( x is invertible & x " = Sum (((1. X) - x) GeoSeq) ) set seq = ((1. X) - x) GeoSeq ; A2: ((1. X) - x) GeoSeq is summable by A1, Th40; then A3: ||.((((1. X) - x) GeoSeq) ^\ 1).|| is convergent by LOPBAN_1:41; reconsider y = Sum (((1. X) - x) GeoSeq) as Element of X ; A4: Partial_Sums (((1. X) - x) GeoSeq) is convergent by A2, Def1; then lim ||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).|| = 0 by NORMSP_1:24; then A5: lim (||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).||) = ||.x.|| * 0 by A4, NORMSP_1:24, SEQ_2:8 .= 0 ; lim ((((1. X) - x) GeoSeq) ^\ 1) = 0. X by A2, Th14; then A6: lim ||.((((1. X) - x) GeoSeq) ^\ 1).|| = ||.(0. X).|| by A2, LOPBAN_1:41; A7: ||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).|| is convergent by A4, NORMSP_1:24, SEQ_2:7; then A8: ||.((((1. X) - x) GeoSeq) ^\ 1).|| + (||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).||) is convergent by A3, SEQ_2:5; A9: lim (||.((((1. X) - x) GeoSeq) ^\ 1).|| + (||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).||)) = (lim ||.((((1. X) - x) GeoSeq) ^\ 1).||) + (lim (||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).||)) by A7, A3, SEQ_2:6 .= 0 by A5, A6 ; A10: for n being Element of NAT holds ((1. X) - x) * ((((1. X) - x) GeoSeq) . n) = (((1. X) - x) GeoSeq) . (n + 1) proof defpred S1[ Element of NAT ] means ((1. X) - x) * ((((1. X) - x) GeoSeq) . $1) = (((1. X) - x) GeoSeq) . ($1 + 1); A11: ((1. X) - x) * ((((1. X) - x) GeoSeq) . 0) = ((1. X) - x) * (1. X) by Def9 .= (1. X) - x by Th38 ; A12: 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 A13: S1[k] ; ::_thesis: S1[k + 1] thus ((1. X) - x) * ((((1. X) - x) GeoSeq) . (k + 1)) = ((1. X) - x) * (((((1. X) - x) GeoSeq) . k) * ((1. X) - x)) by Def9 .= (((1. X) - x) * ((((1. X) - x) GeoSeq) . k)) * ((1. X) - x) by Th38 .= (((1. X) - x) GeoSeq) . ((k + 1) + 1) by A13, Def9 ; ::_thesis: verum end; (((1. X) - x) GeoSeq) . (0 + 1) = ((((1. X) - x) GeoSeq) . 0) * ((1. X) - x) by Def9 .= (1. X) * ((1. X) - x) by Def9 .= (1. X) - x by Th38 ; then A14: S1[ 0 ] by A11; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A14, A12); hence for n being Element of NAT holds ((1. X) - x) * ((((1. X) - x) GeoSeq) . n) = (((1. X) - x) GeoSeq) . (n + 1) ; ::_thesis: verum end; A15: for n being Element of NAT holds ((1. X) - x) * ((Partial_Sums (((1. X) - x) GeoSeq)) . n) = (((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . n) - ((((1. X) - x) GeoSeq) . 0) proof defpred S1[ Element of NAT ] means ((1. X) - x) * ((Partial_Sums (((1. X) - x) GeoSeq)) . $1) = (((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . $1) - ((((1. X) - x) GeoSeq) . 0); A16: ((1. X) - x) * ((Partial_Sums (((1. X) - x) GeoSeq)) . 0) = ((1. X) - x) * ((((1. X) - x) GeoSeq) . 0) by BHSP_4:def_1 .= ((1. X) - x) * (1. X) by Def9 .= (1. X) - x by Th38 ; A17: 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 A18: S1[k] ; ::_thesis: S1[k + 1] A19: (((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . (k + 1)) - ((((1. X) - x) GeoSeq) . 0) = ((Partial_Sums (((1. X) - x) GeoSeq)) . ((k + 1) + 1)) - ((((1. X) - x) GeoSeq) . 0) by NAT_1:def_3 .= (((Partial_Sums (((1. X) - x) GeoSeq)) . (k + 1)) + ((((1. X) - x) GeoSeq) . ((k + 1) + 1))) - ((((1. X) - x) GeoSeq) . 0) by BHSP_4:def_1 .= ((((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . k) + ((((1. X) - x) GeoSeq) . ((k + 1) + 1))) + (- ((((1. X) - x) GeoSeq) . 0)) by NAT_1:def_3 .= ((((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . k) - ((((1. X) - x) GeoSeq) . 0)) + ((((1. X) - x) GeoSeq) . ((k + 1) + 1)) by RLVECT_1:def_3 ; ((1. X) - x) * ((Partial_Sums (((1. X) - x) GeoSeq)) . (k + 1)) = ((1. X) - x) * (((Partial_Sums (((1. X) - x) GeoSeq)) . k) + ((((1. X) - x) GeoSeq) . (k + 1))) by BHSP_4:def_1 .= (((1. X) - x) * ((Partial_Sums (((1. X) - x) GeoSeq)) . k)) + (((1. X) - x) * ((((1. X) - x) GeoSeq) . (k + 1))) by Th38 .= ((((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . k) - ((((1. X) - x) GeoSeq) . 0)) + ((((1. X) - x) GeoSeq) . ((k + 1) + 1)) by A10, A18 ; hence S1[k + 1] by A19; ::_thesis: verum end; (((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . 0) - ((((1. X) - x) GeoSeq) . 0) = ((Partial_Sums (((1. X) - x) GeoSeq)) . (0 + 1)) - ((((1. X) - x) GeoSeq) . 0) by NAT_1:def_3 .= (((Partial_Sums (((1. X) - x) GeoSeq)) . 0) + ((((1. X) - x) GeoSeq) . 1)) - ((((1. X) - x) GeoSeq) . 0) by BHSP_4:def_1 .= (((((1. X) - x) GeoSeq) . 0) + ((((1. X) - x) GeoSeq) . 1)) - ((((1. X) - x) GeoSeq) . 0) by BHSP_4:def_1 .= ((((1. X) - x) GeoSeq) . 1) + (((((1. X) - x) GeoSeq) . 0) - ((((1. X) - x) GeoSeq) . 0)) by Th38 .= ((((1. X) - x) GeoSeq) . 1) + (0. X) by RLVECT_1:15 .= (((1. X) - x) GeoSeq) . (0 + 1) by RLVECT_1:4 .= ((((1. X) - x) GeoSeq) . 0) * ((1. X) - x) by Def9 .= (1. X) * ((1. X) - x) by Def9 .= (1. X) - x by Th38 ; then A20: S1[ 0 ] by A16; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A20, A17); hence for n being Element of NAT holds ((1. X) - x) * ((Partial_Sums (((1. X) - x) GeoSeq)) . n) = (((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . n) - ((((1. X) - x) GeoSeq) . 0) ; ::_thesis: verum end; now__::_thesis:_for_n_being_Element_of_NAT_holds_||.((1._X)_-_(x_*_y)).||_<=_(||.((((1._X)_-_x)_GeoSeq)_^\_1).||_+_(||.x.||_(#)_||.((Partial_Sums_(((1._X)_-_x)_GeoSeq))_-_y).||))_._n let n be Element of NAT ; ::_thesis: ||.((1. X) - (x * y)).|| <= (||.((((1. X) - x) GeoSeq) ^\ 1).|| + (||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).||)) . n reconsider yn = (Partial_Sums (((1. X) - x) GeoSeq)) . n as Element of X ; (Partial_Sums (((1. X) - x) GeoSeq)) . (n + 1) = ((Partial_Sums (((1. X) - x) GeoSeq)) . n) + ((((1. X) - x) GeoSeq) . (n + 1)) by BHSP_4:def_1; then A21: (Partial_Sums (((1. X) - x) GeoSeq)) . (n + 1) = ((Partial_Sums (((1. X) - x) GeoSeq)) . n) + (((((1. X) - x) GeoSeq) ^\ 1) . n) by NAT_1:def_3; ((1. X) - ((1. X) - x)) * yn = ((1. X) * yn) - (((1. X) - x) * yn) by Th38 .= yn - (((1. X) - x) * yn) by Th38 .= ((Partial_Sums (((1. X) - x) GeoSeq)) . n) - ((((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . n) - ((((1. X) - x) GeoSeq) . 0)) by A15 .= (((Partial_Sums (((1. X) - x) GeoSeq)) . n) - (((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . n)) + ((((1. X) - x) GeoSeq) . 0) by Th38 ; then ((1. X) - ((1. X) - x)) * yn = (((Partial_Sums (((1. X) - x) GeoSeq)) . n) - (((Partial_Sums (((1. X) - x) GeoSeq)) . n) + (((((1. X) - x) GeoSeq) ^\ 1) . n))) + ((((1. X) - x) GeoSeq) . 0) by A21, NAT_1:def_3 .= ((((Partial_Sums (((1. X) - x) GeoSeq)) . n) - ((Partial_Sums (((1. X) - x) GeoSeq)) . n)) - (((((1. X) - x) GeoSeq) ^\ 1) . n)) + ((((1. X) - x) GeoSeq) . 0) by Th38 .= ((0. X) - (((((1. X) - x) GeoSeq) ^\ 1) . n)) + ((((1. X) - x) GeoSeq) . 0) by RLVECT_1:15 .= (0. X) - ((((((1. X) - x) GeoSeq) ^\ 1) . n) - ((((1. X) - x) GeoSeq) . 0)) by RLVECT_1:29 .= - ((((((1. X) - x) GeoSeq) ^\ 1) . n) - ((((1. X) - x) GeoSeq) . 0)) by RLVECT_1:14 .= ((((1. X) - x) GeoSeq) . 0) - (((((1. X) - x) GeoSeq) ^\ 1) . n) by RLVECT_1:33 .= ((((1. X) - x) GeoSeq) . 0) - ((((1. X) - x) GeoSeq) . (n + 1)) by NAT_1:def_3 .= (1. X) - ((((1. X) - x) GeoSeq) . (n + 1)) by Def9 ; then A22: (1. X) - (x * yn) = (1. X) - ((1. X) - ((((1. X) - x) GeoSeq) . (n + 1))) by Th38 .= (((1. X) - x) GeoSeq) . (n + 1) by Th38 .= ((((1. X) - x) GeoSeq) ^\ 1) . n by NAT_1:def_3 ; ||.(x * (yn - y)).|| <= ||.x.|| * ||.(yn - y).|| by Th38; then A23: (||.((((1. X) - x) GeoSeq) ^\ 1).|| . n) + ||.(x * (yn - y)).|| <= (||.((((1. X) - x) GeoSeq) ^\ 1).|| . n) + (||.x.|| * ||.(yn - y).||) by XREAL_1:7; ( ||.((((((1. X) - x) GeoSeq) ^\ 1) . n) + (x * (yn - y))).|| <= ||.(((((1. X) - x) GeoSeq) ^\ 1) . n).|| + ||.(x * (yn - y)).|| & ||.(((((1. X) - x) GeoSeq) ^\ 1) . n).|| + ||.(x * (yn - y)).|| = (||.((((1. X) - x) GeoSeq) ^\ 1).|| . n) + ||.(x * (yn - y)).|| ) by NORMSP_0:def_4, NORMSP_1:def_1; then A24: ||.((((((1. X) - x) GeoSeq) ^\ 1) . n) + (x * (yn - y))).|| <= (||.((((1. X) - x) GeoSeq) ^\ 1).|| . n) + (||.x.|| * ||.(yn - y).||) by A23, XXREAL_0:2; (1. X) - (x * y) = ((1. X) - (0. X)) - (x * y) by RLVECT_1:13 .= ((1. X) - ((x * yn) - (x * yn))) - (x * y) by RLVECT_1:15 .= (((1. X) - (x * yn)) + (x * yn)) - (x * y) by RLVECT_1:29 .= ((1. X) - (x * yn)) + ((x * yn) - (x * y)) by RLVECT_1:def_3 .= ((1. X) - (x * yn)) + (x * (yn - y)) by Th38 ; then ||.((1. X) - (x * y)).|| <= (||.((((1. X) - x) GeoSeq) ^\ 1).|| . n) + (||.x.|| * ||.(((Partial_Sums (((1. X) - x) GeoSeq)) - y) . n).||) by A22, A24, NORMSP_1:def_4; then ||.((1. X) - (x * y)).|| <= (||.((((1. X) - x) GeoSeq) ^\ 1).|| . n) + (||.x.|| * (||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).|| . n)) by NORMSP_0:def_4; then ||.((1. X) - (x * y)).|| <= (||.((((1. X) - x) GeoSeq) ^\ 1).|| . n) + ((||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).||) . n) by SEQ_1:9; hence ||.((1. X) - (x * y)).|| <= (||.((((1. X) - x) GeoSeq) ^\ 1).|| + (||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).||)) . n by SEQ_1:7; ::_thesis: verum end; then A25: 1. X = x * y by A8, A9, Lm3; A26: for n being Element of NAT holds ((Partial_Sums (((1. X) - x) GeoSeq)) . n) * ((1. X) - x) = (((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . n) - ((((1. X) - x) GeoSeq) . 0) proof defpred S1[ Element of NAT ] means ((Partial_Sums (((1. X) - x) GeoSeq)) . $1) * ((1. X) - x) = (((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . $1) - ((((1. X) - x) GeoSeq) . 0); A27: ((Partial_Sums (((1. X) - x) GeoSeq)) . 0) * ((1. X) - x) = ((((1. X) - x) GeoSeq) . 0) * ((1. X) - x) by BHSP_4:def_1 .= (1. X) * ((1. X) - x) by Def9 .= (1. X) - x by Th38 ; A28: 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 A29: S1[k] ; ::_thesis: S1[k + 1] A30: (((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . (k + 1)) - ((((1. X) - x) GeoSeq) . 0) = ((Partial_Sums (((1. X) - x) GeoSeq)) . ((k + 1) + 1)) - ((((1. X) - x) GeoSeq) . 0) by NAT_1:def_3 .= (((Partial_Sums (((1. X) - x) GeoSeq)) . (k + 1)) + ((((1. X) - x) GeoSeq) . ((k + 1) + 1))) - ((((1. X) - x) GeoSeq) . 0) by BHSP_4:def_1 .= ((((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . k) + ((((1. X) - x) GeoSeq) . ((k + 1) + 1))) + (- ((((1. X) - x) GeoSeq) . 0)) by NAT_1:def_3 .= ((((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . k) - ((((1. X) - x) GeoSeq) . 0)) + ((((1. X) - x) GeoSeq) . ((k + 1) + 1)) by RLVECT_1:def_3 ; ((Partial_Sums (((1. X) - x) GeoSeq)) . (k + 1)) * ((1. X) - x) = (((Partial_Sums (((1. X) - x) GeoSeq)) . k) + ((((1. X) - x) GeoSeq) . (k + 1))) * ((1. X) - x) by BHSP_4:def_1 .= (((Partial_Sums (((1. X) - x) GeoSeq)) . k) * ((1. X) - x)) + (((((1. X) - x) GeoSeq) . (k + 1)) * ((1. X) - x)) by Th38 .= ((((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . k) - ((((1. X) - x) GeoSeq) . 0)) + ((((1. X) - x) GeoSeq) . ((k + 1) + 1)) by A29, Def9 ; hence S1[k + 1] by A30; ::_thesis: verum end; (((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . 0) - ((((1. X) - x) GeoSeq) . 0) = ((Partial_Sums (((1. X) - x) GeoSeq)) . (0 + 1)) - ((((1. X) - x) GeoSeq) . 0) by NAT_1:def_3 .= (((Partial_Sums (((1. X) - x) GeoSeq)) . 0) + ((((1. X) - x) GeoSeq) . 1)) - ((((1. X) - x) GeoSeq) . 0) by BHSP_4:def_1 .= (((((1. X) - x) GeoSeq) . 0) + ((((1. X) - x) GeoSeq) . 1)) - ((((1. X) - x) GeoSeq) . 0) by BHSP_4:def_1 .= ((((1. X) - x) GeoSeq) . 1) + (((((1. X) - x) GeoSeq) . 0) - ((((1. X) - x) GeoSeq) . 0)) by Th38 .= ((((1. X) - x) GeoSeq) . 1) + (0. X) by RLVECT_1:15 .= (((1. X) - x) GeoSeq) . (0 + 1) by RLVECT_1:4 .= ((((1. X) - x) GeoSeq) . 0) * ((1. X) - x) by Def9 .= (1. X) * ((1. X) - x) by Def9 .= (1. X) - x by Th38 ; then A31: S1[ 0 ] by A27; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A31, A28); hence for n being Element of NAT holds ((Partial_Sums (((1. X) - x) GeoSeq)) . n) * ((1. X) - x) = (((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . n) - ((((1. X) - x) GeoSeq) . 0) ; ::_thesis: verum end; now__::_thesis:_for_n_being_Element_of_NAT_holds_||.((1._X)_-_(y_*_x)).||_<=_(||.((((1._X)_-_x)_GeoSeq)_^\_1).||_+_(||.x.||_(#)_||.((Partial_Sums_(((1._X)_-_x)_GeoSeq))_-_y).||))_._n let n be Element of NAT ; ::_thesis: ||.((1. X) - (y * x)).|| <= (||.((((1. X) - x) GeoSeq) ^\ 1).|| + (||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).||)) . n reconsider yn = (Partial_Sums (((1. X) - x) GeoSeq)) . n as Element of X ; (Partial_Sums (((1. X) - x) GeoSeq)) . (n + 1) = ((Partial_Sums (((1. X) - x) GeoSeq)) . n) + ((((1. X) - x) GeoSeq) . (n + 1)) by BHSP_4:def_1; then A32: (Partial_Sums (((1. X) - x) GeoSeq)) . (n + 1) = ((Partial_Sums (((1. X) - x) GeoSeq)) . n) + (((((1. X) - x) GeoSeq) ^\ 1) . n) by NAT_1:def_3; yn * ((1. X) - ((1. X) - x)) = (yn * (1. X)) - (yn * ((1. X) - x)) by Th38 .= yn - (yn * ((1. X) - x)) by Th38 .= ((Partial_Sums (((1. X) - x) GeoSeq)) . n) - ((((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . n) - ((((1. X) - x) GeoSeq) . 0)) by A26 .= (((Partial_Sums (((1. X) - x) GeoSeq)) . n) - (((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . n)) + ((((1. X) - x) GeoSeq) . 0) by Th38 ; then yn * ((1. X) - ((1. X) - x)) = (((Partial_Sums (((1. X) - x) GeoSeq)) . n) - (((Partial_Sums (((1. X) - x) GeoSeq)) . n) + (((((1. X) - x) GeoSeq) ^\ 1) . n))) + ((((1. X) - x) GeoSeq) . 0) by A32, NAT_1:def_3 .= ((((Partial_Sums (((1. X) - x) GeoSeq)) . n) - ((Partial_Sums (((1. X) - x) GeoSeq)) . n)) - (((((1. X) - x) GeoSeq) ^\ 1) . n)) + ((((1. X) - x) GeoSeq) . 0) by Th38 .= ((0. X) - (((((1. X) - x) GeoSeq) ^\ 1) . n)) + ((((1. X) - x) GeoSeq) . 0) by RLVECT_1:15 .= (0. X) - ((((((1. X) - x) GeoSeq) ^\ 1) . n) - ((((1. X) - x) GeoSeq) . 0)) by RLVECT_1:29 .= - ((((((1. X) - x) GeoSeq) ^\ 1) . n) - ((((1. X) - x) GeoSeq) . 0)) by RLVECT_1:14 .= ((((1. X) - x) GeoSeq) . 0) - (((((1. X) - x) GeoSeq) ^\ 1) . n) by RLVECT_1:33 .= ((((1. X) - x) GeoSeq) . 0) - ((((1. X) - x) GeoSeq) . (n + 1)) by NAT_1:def_3 .= (1. X) - ((((1. X) - x) GeoSeq) . (n + 1)) by Def9 ; then A33: (1. X) - (yn * x) = (1. X) - ((1. X) - ((((1. X) - x) GeoSeq) . (n + 1))) by Th38 .= (((1. X) - x) GeoSeq) . (n + 1) by Th38 .= ((((1. X) - x) GeoSeq) ^\ 1) . n by NAT_1:def_3 ; ||.((yn - y) * x).|| <= ||.(yn - y).|| * ||.x.|| by Th38; then A34: (||.((((1. X) - x) GeoSeq) ^\ 1).|| . n) + ||.((yn - y) * x).|| <= (||.((((1. X) - x) GeoSeq) ^\ 1).|| . n) + (||.(yn - y).|| * ||.x.||) by XREAL_1:7; ( ||.((((((1. X) - x) GeoSeq) ^\ 1) . n) + ((yn - y) * x)).|| <= ||.(((((1. X) - x) GeoSeq) ^\ 1) . n).|| + ||.((yn - y) * x).|| & ||.(((((1. X) - x) GeoSeq) ^\ 1) . n).|| + ||.((yn - y) * x).|| = (||.((((1. X) - x) GeoSeq) ^\ 1).|| . n) + ||.((yn - y) * x).|| ) by NORMSP_0:def_4, NORMSP_1:def_1; then A35: ||.((((((1. X) - x) GeoSeq) ^\ 1) . n) + ((yn - y) * x)).|| <= (||.((((1. X) - x) GeoSeq) ^\ 1).|| . n) + (||.(yn - y).|| * ||.x.||) by A34, XXREAL_0:2; (1. X) - (y * x) = ((1. X) - (0. X)) - (y * x) by RLVECT_1:13 .= ((1. X) - ((yn * x) - (yn * x))) - (y * x) by RLVECT_1:15 .= (((1. X) - (yn * x)) + (yn * x)) - (y * x) by RLVECT_1:29 .= ((1. X) - (yn * x)) + ((yn * x) - (y * x)) by RLVECT_1:def_3 .= ((1. X) - (yn * x)) + ((yn - y) * x) by Th38 ; then ||.((1. X) - (y * x)).|| <= (||.((((1. X) - x) GeoSeq) ^\ 1).|| . n) + (||.(((Partial_Sums (((1. X) - x) GeoSeq)) - y) . n).|| * ||.x.||) by A33, A35, NORMSP_1:def_4; then ||.((1. X) - (y * x)).|| <= (||.((((1. X) - x) GeoSeq) ^\ 1).|| . n) + ((||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).|| . n) * ||.x.||) by NORMSP_0:def_4; then ||.((1. X) - (y * x)).|| <= (||.((((1. X) - x) GeoSeq) ^\ 1).|| . n) + ((||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).||) . n) by SEQ_1:9; hence ||.((1. X) - (y * x)).|| <= (||.((((1. X) - x) GeoSeq) ^\ 1).|| + (||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).||)) . n by SEQ_1:7; ::_thesis: verum end; then A36: 1. X = y * x by A8, A9, Lm3; hence x is invertible by A25, Def4; ::_thesis: x " = Sum (((1. X) - x) GeoSeq) hence x " = Sum (((1. X) - x) GeoSeq) by A36, A25, Def8; ::_thesis: verum end;