:: LOPBAN_4 semantic presentation begin definition let X be non empty multMagma ; let x, y be Element of X; predx,y are_commutative means :Def1: :: LOPBAN_4:def 1 x * y = y * x; reflexivity for x being Element of X holds x * x = x * x ; symmetry for x, y being Element of X st x * y = y * x holds y * x = x * y ; end; :: deftheorem Def1 defines are_commutative LOPBAN_4:def_1_:_ for X being non empty multMagma for x, y being Element of X holds ( x,y are_commutative iff x * y = y * x ); Lm1: for X being Banach_Algebra for z being Element of X for n being Element of NAT holds ( z * (z #N n) = z #N (n + 1) & (z #N n) * z = z #N (n + 1) & z * (z #N n) = (z #N n) * z ) proof let X be Banach_Algebra; ::_thesis: for z being Element of X for n being Element of NAT holds ( z * (z #N n) = z #N (n + 1) & (z #N n) * z = z #N (n + 1) & z * (z #N n) = (z #N n) * z ) let z be Element of X; ::_thesis: for n being Element of NAT holds ( z * (z #N n) = z #N (n + 1) & (z #N n) * z = z #N (n + 1) & z * (z #N n) = (z #N n) * z ) let n be Element of NAT ; ::_thesis: ( z * (z #N n) = z #N (n + 1) & (z #N n) * z = z #N (n + 1) & z * (z #N n) = (z #N n) * z ) defpred S1[ Element of NAT ] means z * (z #N $1) = z #N ($1 + 1); A1: z #N (0 + 1) = ((z GeoSeq) . 0) * z by LOPBAN_3:def_9 .= (1. X) * z by LOPBAN_3:def_9 .= z by LOPBAN_3:38 ; 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 z * (z #N (k + 1)) = z * (((z GeoSeq) . k) * z) by LOPBAN_3:def_9 .= (z * (z #N k)) * z by LOPBAN_3:38 .= z #N ((k + 1) + 1) by A3, LOPBAN_3:def_9 ; ::_thesis: verum end; z * (z #N 0) = z * (1. X) by LOPBAN_3:def_9 .= z by LOPBAN_3:38 ; then A4: S1[ 0 ] by A1; A5: for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2); now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_z_*_(z_#N_n)_=_z_#N_(n_+_1)_&_(z_#N_n)_*_z_=_z_#N_(n_+_1)_&_z_*_(z_#N_n)_=_(z_#N_n)_*_z_) let n be Element of NAT ; ::_thesis: ( z * (z #N n) = z #N (n + 1) & (z #N n) * z = z #N (n + 1) & z * (z #N n) = (z #N n) * z ) thus z * (z #N n) = z #N (n + 1) by A5; ::_thesis: ( (z #N n) * z = z #N (n + 1) & z * (z #N n) = (z #N n) * z ) thus (z #N n) * z = z #N (n + 1) by LOPBAN_3:def_9; ::_thesis: z * (z #N n) = (z #N n) * z hence z * (z #N n) = (z #N n) * z by A5; ::_thesis: verum end; hence ( z * (z #N n) = z #N (n + 1) & (z #N n) * z = z #N (n + 1) & z * (z #N n) = (z #N n) * z ) ; ::_thesis: verum end; Lm2: for X being Banach_Algebra for n being Element of NAT for z, w being Element of X st z,w are_commutative holds ( w * (z #N n) = (z #N n) * w & z * (w #N n) = (w #N n) * z ) proof let X be Banach_Algebra; ::_thesis: for n being Element of NAT for z, w being Element of X st z,w are_commutative holds ( w * (z #N n) = (z #N n) * w & z * (w #N n) = (w #N n) * z ) let n be Element of NAT ; ::_thesis: for z, w being Element of X st z,w are_commutative holds ( w * (z #N n) = (z #N n) * w & z * (w #N n) = (w #N n) * z ) let z, w be Element of X; ::_thesis: ( z,w are_commutative implies ( w * (z #N n) = (z #N n) * w & z * (w #N n) = (w #N n) * z ) ) assume A1: z,w are_commutative ; ::_thesis: ( w * (z #N n) = (z #N n) * w & z * (w #N n) = (w #N n) * z ) defpred S1[ Element of NAT ] means ( w * (z #N $1) = (z #N $1) * w & z * (w #N $1) = (w #N $1) * z ); 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] A4: z * (w #N (k + 1)) = z * ((w #N k) * w) by Lm1 .= (z * (w #N k)) * w by LOPBAN_3:38 .= (w #N k) * (z * w) by A3, LOPBAN_3:38 .= (w #N k) * (w * z) by A1, Def1 .= ((w #N k) * w) * z by LOPBAN_3:38 .= (w #N (k + 1)) * z by Lm1 ; w * (z #N (k + 1)) = w * ((z #N k) * z) by Lm1 .= (w * (z #N k)) * z by LOPBAN_3:38 .= (z #N k) * (w * z) by A3, LOPBAN_3:38 .= (z #N k) * (z * w) by A1, Def1 .= ((z #N k) * z) * w by LOPBAN_3:38 .= (z #N (k + 1)) * w by Lm1 ; hence S1[k + 1] by A4; ::_thesis: verum end; A5: w #N 0 = 1. X by LOPBAN_3:def_9; then A6: z * (w #N 0) = z by LOPBAN_3:38 .= (w #N 0) * z by A5, LOPBAN_3:38 ; A7: z #N 0 = 1. X by LOPBAN_3:def_9; then w * (z #N 0) = w by LOPBAN_3:38 .= (z #N 0) * w by A7, LOPBAN_3:38 ; then A8: S1[ 0 ] by A6; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A8, A2); hence ( w * (z #N n) = (z #N n) * w & z * (w #N n) = (w #N n) * z ) ; ::_thesis: verum end; theorem Th1: :: LOPBAN_4:1 for X being Banach_Algebra for seq1, seq2 being sequence of X st seq1 is convergent & seq2 is convergent & lim (seq1 - seq2) = 0. X holds lim seq1 = lim seq2 proof let X be Banach_Algebra; ::_thesis: for seq1, seq2 being sequence of X st seq1 is convergent & seq2 is convergent & lim (seq1 - seq2) = 0. X holds lim seq1 = lim seq2 let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is convergent & seq2 is convergent & lim (seq1 - seq2) = 0. X implies lim seq1 = lim seq2 ) assume that A1: seq1 is convergent and A2: seq2 is convergent and A3: lim (seq1 - seq2) = 0. X ; ::_thesis: lim seq1 = lim seq2 (lim seq1) - (lim seq2) = 0. X by A1, A2, A3, NORMSP_1:26; then ((lim seq1) - (lim seq2)) + (lim seq2) = lim seq2 by LOPBAN_3:38; then (lim seq1) - ((lim seq2) - (lim seq2)) = lim seq2 by LOPBAN_3:38; then (lim seq1) - (0. X) = lim seq2 by RLVECT_1:15; hence lim seq1 = lim seq2 by RLVECT_1:13; ::_thesis: verum end; theorem Th2: :: LOPBAN_4:2 for X being Banach_Algebra for s being sequence of X for z being Element of X st ( for n being Element of NAT holds s . n = z ) holds lim s = z proof let X be Banach_Algebra; ::_thesis: for s being sequence of X for z being Element of X st ( for n being Element of NAT holds s . n = z ) holds lim s = z let s be sequence of X; ::_thesis: for z being Element of X st ( for n being Element of NAT holds s . n = z ) holds lim s = z let z be Element of X; ::_thesis: ( ( for n being Element of NAT holds s . n = z ) implies lim s = z ) assume A1: for n being Element of NAT holds s . n = z ; ::_thesis: lim s = z A2: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_ ex_k_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_k_<=_n_holds_ ||.((s_._n)_-_z).||_<_p let p be Real; ::_thesis: ( 0 < p implies ex k being Element of NAT st for n being Element of NAT st k <= n holds ||.((s . n) - z).|| < p ) assume A3: 0 < p ; ::_thesis: ex k being Element of NAT st for n being Element of NAT st k <= n holds ||.((s . n) - z).|| < p take k = 0 ; ::_thesis: for n being Element of NAT st k <= n holds ||.((s . n) - z).|| < p let n be Element of NAT ; ::_thesis: ( k <= n implies ||.((s . n) - z).|| < p ) assume k <= n ; ::_thesis: ||.((s . n) - z).|| < p s . n = z by A1; hence ||.((s . n) - z).|| < p by A3, NORMSP_1:6; ::_thesis: verum end; then s is convergent by NORMSP_1:def_6; hence lim s = z by A2, NORMSP_1:def_7; ::_thesis: verum end; theorem Th3: :: LOPBAN_4:3 for X being Banach_Algebra for s, s9 being sequence of X st s is convergent & s9 is convergent holds s * s9 is convergent proof let X be Banach_Algebra; ::_thesis: for s, s9 being sequence of X st s is convergent & s9 is convergent holds s * s9 is convergent let s, s9 be sequence of X; ::_thesis: ( s is convergent & s9 is convergent implies s * s9 is convergent ) assume that A1: s is convergent and A2: s9 is convergent ; ::_thesis: s * s9 is convergent consider g1 being Point 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 ||.((s . m) - g1).|| < p by A1, NORMSP_1:def_6; ||.s.|| is bounded by A1, NORMSP_1:23, SEQ_2:13; then consider R being real number such that A4: for n being Element of NAT holds ||.s.|| . n < R by SEQ_2:def_3; A5: now__::_thesis:_for_n_being_Element_of_NAT_holds_||.(s_._n).||_<_R let n be Element of NAT ; ::_thesis: ||.(s . n).|| < R ||.(s . n).|| = ||.s.|| . n by NORMSP_0:def_4; hence ||.(s . n).|| < R by A4; ::_thesis: verum end; ||.(s . 1).|| = ||.s.|| . 1 by NORMSP_0:def_4; then 0 <= ||.s.|| . 1 by NORMSP_1:4; then A6: 0 < R by A4; consider g2 being Point of X such that A7: 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 ||.((s9 . m) - g2).|| < p by A2, NORMSP_1:def_6; take g = g1 * g2; :: 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 <= ||.(((s * s9) . 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 <= ||.(((s * s9) . b2) - g).|| ) ) reconsider R = R as Real by XREAL_0:def_1; A8: 0 + 0 < ||.g2.|| + R by A6, NORMSP_1:4, XREAL_1:8; assume A9: 0 < p ; ::_thesis: ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not p <= ||.(((s * s9) . b2) - g).|| ) then consider n1 being Element of NAT such that A10: for m being Element of NAT st n1 <= m holds ||.((s . m) - g1).|| < p / (||.g2.|| + R) by A3, A8, XREAL_1:139; consider n2 being Element of NAT such that A11: for m being Element of NAT st n2 <= m holds ||.((s9 . m) - g2).|| < p / (||.g2.|| + R) by A7, A8, A9, XREAL_1:139; take n = n1 + n2; ::_thesis: for b1 being Element of NAT holds ( not n <= b1 or not p <= ||.(((s * s9) . b1) - g).|| ) let m be Element of NAT ; ::_thesis: ( not n <= m or not p <= ||.(((s * s9) . m) - g).|| ) assume A12: n <= m ; ::_thesis: not p <= ||.(((s * s9) . m) - g).|| n2 <= n by NAT_1:12; then n2 <= m by A12, XXREAL_0:2; then A13: ||.((s9 . m) - g2).|| < p / (||.g2.|| + R) by A11; A14: 0 <= ||.(s . m).|| by NORMSP_1:4; A15: ||.((s . m) * ((s9 . m) - g2)).|| <= ||.(s . m).|| * ||.((s9 . m) - g2).|| by LOPBAN_3:38; A16: 0 <= ||.((s9 . m) - g2).|| by NORMSP_1:4; n1 <= n1 + n2 by NAT_1:12; then n1 <= m by A12, XXREAL_0:2; then A17: ||.((s . m) - g1).|| <= p / (||.g2.|| + R) by A10; ||.(((s * s9) . m) - g).|| = ||.(((s . m) * (s9 . m)) - (g1 * g2)).|| by LOPBAN_3:def_7 .= ||.((((s . m) * (s9 . m)) - ((s . m) * g2)) + (((s . m) * g2) - (g1 * g2))).|| by LOPBAN_3:38 .= ||.(((s . m) * ((s9 . m) - g2)) + (((s . m) * g2) - (g1 * g2))).|| by LOPBAN_3:38 .= ||.(((s . m) * ((s9 . m) - g2)) + (((s . m) - g1) * g2)).|| by LOPBAN_3:38 ; then A18: ||.(((s * s9) . m) - g).|| <= ||.((s . m) * ((s9 . m) - g2)).|| + ||.(((s . m) - g1) * g2).|| by NORMSP_1:def_1; ||.(s . m).|| < R by A5; then ||.(s . m).|| * ||.((s9 . m) - g2).|| < R * (p / (||.g2.|| + R)) by A14, A16, A13, XREAL_1:96; then A19: ||.((s . m) * ((s9 . m) - g2)).|| < R * (p / (||.g2.|| + R)) by A15, XXREAL_0:2; A20: ||.(((s . m) - g1) * g2).|| <= ||.g2.|| * ||.((s . m) - g1).|| by LOPBAN_3:38; 0 <= ||.g2.|| by NORMSP_1:4; then ||.g2.|| * ||.((s . m) - g1).|| <= ||.g2.|| * (p / (||.g2.|| + R)) by A17, XREAL_1:64; then A21: ||.(((s . m) - g1) * g2).|| <= ||.g2.|| * (p / (||.g2.|| + R)) by A20, XXREAL_0:2; (R * (p / (||.g2.|| + R))) + (||.g2.|| * (p / (||.g2.|| + R))) = (p / (||.g2.|| + R)) * (||.g2.|| + R) .= p by A8, XCMPLX_1:87 ; then ||.((s . m) * ((s9 . m) - g2)).|| + ||.(((s . m) - g1) * g2).|| < p by A19, A21, XREAL_1:8; hence ||.(((s * s9) . m) - g).|| < p by A18, XXREAL_0:2; ::_thesis: verum end; theorem Th4: :: LOPBAN_4:4 for X being Banach_Algebra for z being Element of X for s being sequence of X st s is convergent holds z * s is convergent proof let X be Banach_Algebra; ::_thesis: for z being Element of X for s being sequence of X st s is convergent holds z * s is convergent let z be Element of X; ::_thesis: for s being sequence of X st s is convergent holds z * s is convergent let s be sequence of X; ::_thesis: ( s is convergent implies z * s is convergent ) A1: 0 <= ||.z.|| by NORMSP_1:4; assume s is convergent ; ::_thesis: z * s is convergent then consider g1 being Point of X such that A2: 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 ||.((s . m) - g1).|| < p by NORMSP_1:def_6; take g = z * 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 <= ||.(((z * s) . 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 <= ||.(((z * s) . b2) - g).|| ) ) A3: 0 + 0 < ||.z.|| + 1 by NORMSP_1:4, XREAL_1:8; assume A4: 0 < p ; ::_thesis: ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not p <= ||.(((z * s) . b2) - g).|| ) then consider n being Element of NAT such that A5: for m being Element of NAT st n <= m holds ||.((s . m) - g1).|| < p / (||.z.|| + 1) by A2, A3, XREAL_1:139; take n ; ::_thesis: for b1 being Element of NAT holds ( not n <= b1 or not p <= ||.(((z * s) . b1) - g).|| ) let m be Element of NAT ; ::_thesis: ( not n <= m or not p <= ||.(((z * s) . m) - g).|| ) assume n <= m ; ::_thesis: not p <= ||.(((z * s) . m) - g).|| then A6: ||.((s . m) - g1).|| < p / (||.z.|| + 1) by A5; A7: ||.(z * ((s . m) - g1)).|| <= ||.z.|| * ||.((s . m) - g1).|| by LOPBAN_3:38; A8: 0 + ||.z.|| < ||.z.|| + 1 by XREAL_1:8; 0 < p / (||.z.|| + 1) by A3, A4, XREAL_1:139; then A9: ||.z.|| * (p / (||.z.|| + 1)) < (||.z.|| + 1) * (p / (||.z.|| + 1)) by A1, A8, XREAL_1:97; A10: ||.(((z * s) . m) - g).|| = ||.((z * (s . m)) - (z * g1)).|| by LOPBAN_3:def_5 .= ||.(z * ((s . m) - g1)).|| by LOPBAN_3:38 ; 0 <= ||.((s . m) - g1).|| by NORMSP_1:4; then ||.z.|| * ||.((s . m) - g1).|| <= ||.z.|| * (p / (||.z.|| + 1)) by A1, A6, XREAL_1:66; then A11: ||.(z * ((s . m) - g1)).|| <= ||.z.|| * (p / (||.z.|| + 1)) by A7, XXREAL_0:2; (||.z.|| + 1) * (p / (||.z.|| + 1)) = p by A3, XCMPLX_1:87; hence ||.(((z * s) . m) - g).|| < p by A10, A11, A9, XXREAL_0:2; ::_thesis: verum end; theorem Th5: :: LOPBAN_4:5 for X being Banach_Algebra for z being Element of X for s being sequence of X st s is convergent holds s * z is convergent proof let X be Banach_Algebra; ::_thesis: for z being Element of X for s being sequence of X st s is convergent holds s * z is convergent let z be Element of X; ::_thesis: for s being sequence of X st s is convergent holds s * z is convergent let s be sequence of X; ::_thesis: ( s is convergent implies s * z is convergent ) A1: 0 <= ||.z.|| by NORMSP_1:4; assume s is convergent ; ::_thesis: s * z is convergent then consider g1 being Point of X such that A2: 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 ||.((s . m) - g1).|| < p by NORMSP_1:def_6; take g = g1 * z; :: 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 <= ||.(((s * z) . 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 <= ||.(((s * z) . b2) - g).|| ) ) A3: 0 + 0 < ||.z.|| + 1 by NORMSP_1:4, XREAL_1:8; assume A4: 0 < p ; ::_thesis: ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not p <= ||.(((s * z) . b2) - g).|| ) then consider n being Element of NAT such that A5: for m being Element of NAT st n <= m holds ||.((s . m) - g1).|| < p / (||.z.|| + 1) by A2, A3, XREAL_1:139; take n ; ::_thesis: for b1 being Element of NAT holds ( not n <= b1 or not p <= ||.(((s * z) . b1) - g).|| ) let m be Element of NAT ; ::_thesis: ( not n <= m or not p <= ||.(((s * z) . m) - g).|| ) assume n <= m ; ::_thesis: not p <= ||.(((s * z) . m) - g).|| then A6: ||.((s . m) - g1).|| < p / (||.z.|| + 1) by A5; A7: ||.(((s . m) - g1) * z).|| <= ||.((s . m) - g1).|| * ||.z.|| by LOPBAN_3:38; A8: 0 + ||.z.|| < ||.z.|| + 1 by XREAL_1:8; 0 < p / (||.z.|| + 1) by A3, A4, XREAL_1:139; then A9: (p / (||.z.|| + 1)) * ||.z.|| < (p / (||.z.|| + 1)) * (||.z.|| + 1) by A1, A8, XREAL_1:97; A10: ||.(((s * z) . m) - g).|| = ||.(((s . m) * z) - (g1 * z)).|| by LOPBAN_3:def_6 .= ||.(((s . m) - g1) * z).|| by LOPBAN_3:38 ; 0 <= ||.((s . m) - g1).|| by NORMSP_1:4; then ||.((s . m) - g1).|| * ||.z.|| <= (p / (||.z.|| + 1)) * ||.z.|| by A1, A6, XREAL_1:66; then A11: ||.(((s . m) - g1) * z).|| <= (p / (||.z.|| + 1)) * ||.z.|| by A7, XXREAL_0:2; (p / (||.z.|| + 1)) * (||.z.|| + 1) = p by A3, XCMPLX_1:87; hence ||.(((s * z) . m) - g).|| < p by A10, A11, A9, XXREAL_0:2; ::_thesis: verum end; theorem Th6: :: LOPBAN_4:6 for X being Banach_Algebra for z being Element of X for s being sequence of X st s is convergent holds lim (z * s) = z * (lim s) proof let X be Banach_Algebra; ::_thesis: for z being Element of X for s being sequence of X st s is convergent holds lim (z * s) = z * (lim s) let z be Element of X; ::_thesis: for s being sequence of X st s is convergent holds lim (z * s) = z * (lim s) let s be sequence of X; ::_thesis: ( s is convergent implies lim (z * s) = z * (lim s) ) assume A1: s is convergent ; ::_thesis: lim (z * s) = z * (lim s) set g1 = lim s; set g = z * (lim s); A2: 0 + 0 < ||.z.|| + 1 by NORMSP_1:4, XREAL_1:8; A3: 0 <= ||.z.|| by NORMSP_1:4; 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_ ||.(((z_*_s)_._m)_-_(z_*_(lim_s))).||_<_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 ||.(((z * s) . m) - (z * (lim s))).|| < p ) assume 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.(((z * s) . m) - (z * (lim s))).|| < p then A5: 0 < p / (||.z.|| + 1) by A2, XREAL_1:139; then consider n being Element of NAT such that A6: for m being Element of NAT st n <= m holds ||.((s . m) - (lim s)).|| < p / (||.z.|| + 1) by A1, NORMSP_1:def_7; take n = n; ::_thesis: for m being Element of NAT st n <= m holds ||.(((z * s) . m) - (z * (lim s))).|| < p let m be Element of NAT ; ::_thesis: ( n <= m implies ||.(((z * s) . m) - (z * (lim s))).|| < p ) assume n <= m ; ::_thesis: ||.(((z * s) . m) - (z * (lim s))).|| < p then A7: ||.((s . m) - (lim s)).|| < p / (||.z.|| + 1) by A6; 0 <= ||.((s . m) - (lim s)).|| by NORMSP_1:4; then A8: ||.z.|| * ||.((s . m) - (lim s)).|| <= ||.z.|| * (p / (||.z.|| + 1)) by A3, A7, XREAL_1:66; ||.(z * ((s . m) - (lim s))).|| <= ||.z.|| * ||.((s . m) - (lim s)).|| by LOPBAN_3:38; then A9: ||.(z * ((s . m) - (lim s))).|| <= ||.z.|| * (p / (||.z.|| + 1)) by A8, XXREAL_0:2; A10: ||.(((z * s) . m) - (z * (lim s))).|| = ||.((z * (s . m)) - (z * (lim s))).|| by LOPBAN_3:def_5 .= ||.(z * ((s . m) - (lim s))).|| by LOPBAN_3:38 ; 0 + ||.z.|| < ||.z.|| + 1 by XREAL_1:8; then A11: ||.z.|| * (p / (||.z.|| + 1)) < (||.z.|| + 1) * (p / (||.z.|| + 1)) by A3, A5, XREAL_1:97; (||.z.|| + 1) * (p / (||.z.|| + 1)) = p by A2, XCMPLX_1:87; hence ||.(((z * s) . m) - (z * (lim s))).|| < p by A10, A9, A11, XXREAL_0:2; ::_thesis: verum end; z * s is convergent by A1, Th4; hence lim (z * s) = z * (lim s) by A4, NORMSP_1:def_7; ::_thesis: verum end; theorem Th7: :: LOPBAN_4:7 for X being Banach_Algebra for z being Element of X for s being sequence of X st s is convergent holds lim (s * z) = (lim s) * z proof let X be Banach_Algebra; ::_thesis: for z being Element of X for s being sequence of X st s is convergent holds lim (s * z) = (lim s) * z let z be Element of X; ::_thesis: for s being sequence of X st s is convergent holds lim (s * z) = (lim s) * z let s be sequence of X; ::_thesis: ( s is convergent implies lim (s * z) = (lim s) * z ) assume A1: s is convergent ; ::_thesis: lim (s * z) = (lim s) * z set g1 = lim s; set g = (lim s) * z; A2: 0 + 0 < ||.z.|| + 1 by NORMSP_1:4, XREAL_1:8; A3: 0 <= ||.z.|| by NORMSP_1:4; 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_ ||.(((s_*_z)_._m)_-_((lim_s)_*_z)).||_<_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 ||.(((s * z) . m) - ((lim s) * z)).|| < p ) assume 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.(((s * z) . m) - ((lim s) * z)).|| < p then A5: 0 < p / (||.z.|| + 1) by A2, XREAL_1:139; then consider n being Element of NAT such that A6: for m being Element of NAT st n <= m holds ||.((s . m) - (lim s)).|| < p / (||.z.|| + 1) by A1, NORMSP_1:def_7; take n = n; ::_thesis: for m being Element of NAT st n <= m holds ||.(((s * z) . m) - ((lim s) * z)).|| < p let m be Element of NAT ; ::_thesis: ( n <= m implies ||.(((s * z) . m) - ((lim s) * z)).|| < p ) assume n <= m ; ::_thesis: ||.(((s * z) . m) - ((lim s) * z)).|| < p then A7: ||.((s . m) - (lim s)).|| < p / (||.z.|| + 1) by A6; 0 <= ||.((s . m) - (lim s)).|| by NORMSP_1:4; then A8: ||.((s . m) - (lim s)).|| * ||.z.|| <= (p / (||.z.|| + 1)) * ||.z.|| by A3, A7, XREAL_1:66; ||.(((s . m) - (lim s)) * z).|| <= ||.((s . m) - (lim s)).|| * ||.z.|| by LOPBAN_3:38; then A9: ||.(((s . m) - (lim s)) * z).|| <= (p / (||.z.|| + 1)) * ||.z.|| by A8, XXREAL_0:2; A10: ||.(((s * z) . m) - ((lim s) * z)).|| = ||.(((s . m) * z) - ((lim s) * z)).|| by LOPBAN_3:def_6 .= ||.(((s . m) - (lim s)) * z).|| by LOPBAN_3:38 ; 0 + ||.z.|| < ||.z.|| + 1 by XREAL_1:8; then A11: (p / (||.z.|| + 1)) * ||.z.|| < (p / (||.z.|| + 1)) * (||.z.|| + 1) by A3, A5, XREAL_1:97; (p / (||.z.|| + 1)) * (||.z.|| + 1) = p by A2, XCMPLX_1:87; hence ||.(((s * z) . m) - ((lim s) * z)).|| < p by A10, A9, A11, XXREAL_0:2; ::_thesis: verum end; s * z is convergent by A1, Th5; hence lim (s * z) = (lim s) * z by A4, NORMSP_1:def_7; ::_thesis: verum end; theorem Th8: :: LOPBAN_4:8 for X being Banach_Algebra for s, s9 being sequence of X st s is convergent & s9 is convergent holds lim (s * s9) = (lim s) * (lim s9) proof let X be Banach_Algebra; ::_thesis: for s, s9 being sequence of X st s is convergent & s9 is convergent holds lim (s * s9) = (lim s) * (lim s9) let s, s9 be sequence of X; ::_thesis: ( s is convergent & s9 is convergent implies lim (s * s9) = (lim s) * (lim s9) ) assume that A1: s is convergent and A2: s9 is convergent ; ::_thesis: lim (s * s9) = (lim s) * (lim s9) ||.s.|| is bounded by A1, NORMSP_1:23, SEQ_2:13; then consider R being real number such that A3: for n being Element of NAT holds ||.s.|| . n < R by SEQ_2:def_3; set g2 = lim s9; set g1 = lim s; set g = (lim s) * (lim s9); A4: now__::_thesis:_for_n_being_Element_of_NAT_holds_||.(s_._n).||_<_R let n be Element of NAT ; ::_thesis: ||.(s . n).|| < R ||.(s . n).|| = ||.s.|| . n by NORMSP_0:def_4; hence ||.(s . n).|| < R by A3; ::_thesis: verum end; ||.(s . 1).|| = ||.s.|| . 1 by NORMSP_0:def_4; then 0 <= ||.s.|| . 1 by NORMSP_1:4; then A5: 0 < R by A3; reconsider R = R as Real by XREAL_0:def_1; A6: 0 + 0 < ||.(lim s9).|| + R by A5, NORMSP_1:4, XREAL_1:8; A7: 0 <= ||.(lim s9).|| by NORMSP_1:4; A8: 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_ ||.(((s_*_s9)_._m)_-_((lim_s)_*_(lim_s9))).||_<_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 ||.(((s * s9) . m) - ((lim s) * (lim s9))).|| < p ) assume 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.(((s * s9) . m) - ((lim s) * (lim s9))).|| < p then A9: 0 < p / (||.(lim s9).|| + R) by A6, XREAL_1:139; then consider n1 being Element of NAT such that A10: for m being Element of NAT st n1 <= m holds ||.((s . m) - (lim s)).|| < p / (||.(lim s9).|| + R) by A1, NORMSP_1:def_7; consider n2 being Element of NAT such that A11: for m being Element of NAT st n2 <= m holds ||.((s9 . m) - (lim s9)).|| < p / (||.(lim s9).|| + R) by A2, A9, NORMSP_1:def_7; take n = n1 + n2; ::_thesis: for m being Element of NAT st n <= m holds ||.(((s * s9) . m) - ((lim s) * (lim s9))).|| < p let m be Element of NAT ; ::_thesis: ( n <= m implies ||.(((s * s9) . m) - ((lim s) * (lim s9))).|| < p ) assume A12: n <= m ; ::_thesis: ||.(((s * s9) . m) - ((lim s) * (lim s9))).|| < p n1 <= n1 + n2 by NAT_1:12; then n1 <= m by A12, XXREAL_0:2; then ||.((s . m) - (lim s)).|| <= p / (||.(lim s9).|| + R) by A10; then A13: ||.(lim s9).|| * ||.((s . m) - (lim s)).|| <= ||.(lim s9).|| * (p / (||.(lim s9).|| + R)) by A7, XREAL_1:64; ||.(((s . m) - (lim s)) * (lim s9)).|| <= ||.(lim s9).|| * ||.((s . m) - (lim s)).|| by LOPBAN_3:38; then A14: ||.(((s . m) - (lim s)) * (lim s9)).|| <= ||.(lim s9).|| * (p / (||.(lim s9).|| + R)) by A13, XXREAL_0:2; A15: 0 <= ||.(s . m).|| by NORMSP_1:4; ||.(((s * s9) . m) - ((lim s) * (lim s9))).|| = ||.(((s . m) * (s9 . m)) - ((lim s) * (lim s9))).|| by LOPBAN_3:def_7 .= ||.((((s . m) * (s9 . m)) - ((s . m) * (lim s9))) + (((s . m) * (lim s9)) - ((lim s) * (lim s9)))).|| by LOPBAN_3:38 .= ||.(((s . m) * ((s9 . m) - (lim s9))) + (((s . m) * (lim s9)) - ((lim s) * (lim s9)))).|| by LOPBAN_3:38 .= ||.(((s . m) * ((s9 . m) - (lim s9))) + (((s . m) - (lim s)) * (lim s9))).|| by LOPBAN_3:38 ; then A16: ||.(((s * s9) . m) - ((lim s) * (lim s9))).|| <= ||.((s . m) * ((s9 . m) - (lim s9))).|| + ||.(((s . m) - (lim s)) * (lim s9)).|| by NORMSP_1:def_1; A17: ||.((s . m) * ((s9 . m) - (lim s9))).|| <= ||.(s . m).|| * ||.((s9 . m) - (lim s9)).|| by LOPBAN_3:38; n2 <= n by NAT_1:12; then n2 <= m by A12, XXREAL_0:2; then A18: ||.((s9 . m) - (lim s9)).|| < p / (||.(lim s9).|| + R) by A11; A19: 0 <= ||.((s9 . m) - (lim s9)).|| by NORMSP_1:4; ||.(s . m).|| < R by A4; then ||.(s . m).|| * ||.((s9 . m) - (lim s9)).|| < R * (p / (||.(lim s9).|| + R)) by A15, A19, A18, XREAL_1:96; then A20: ||.((s . m) * ((s9 . m) - (lim s9))).|| < R * (p / (||.(lim s9).|| + R)) by A17, XXREAL_0:2; (R * (p / (||.(lim s9).|| + R))) + (||.(lim s9).|| * (p / (||.(lim s9).|| + R))) = (p / (||.(lim s9).|| + R)) * (||.(lim s9).|| + R) .= p by A6, XCMPLX_1:87 ; then ||.((s . m) * ((s9 . m) - (lim s9))).|| + ||.(((s . m) - (lim s)) * (lim s9)).|| < p by A20, A14, XREAL_1:8; hence ||.(((s * s9) . m) - ((lim s) * (lim s9))).|| < p by A16, XXREAL_0:2; ::_thesis: verum end; s * s9 is convergent by A1, A2, Th3; hence lim (s * s9) = (lim s) * (lim s9) by A8, NORMSP_1:def_7; ::_thesis: verum end; theorem Th9: :: LOPBAN_4:9 for X being Banach_Algebra for z being Element of X for seq being sequence of X holds ( Partial_Sums (z * seq) = z * (Partial_Sums seq) & Partial_Sums (seq * z) = (Partial_Sums seq) * z ) proof let X be Banach_Algebra; ::_thesis: for z being Element of X for seq being sequence of X holds ( Partial_Sums (z * seq) = z * (Partial_Sums seq) & Partial_Sums (seq * z) = (Partial_Sums seq) * z ) let z be Element of X; ::_thesis: for seq being sequence of X holds ( Partial_Sums (z * seq) = z * (Partial_Sums seq) & Partial_Sums (seq * z) = (Partial_Sums seq) * z ) let seq be sequence of X; ::_thesis: ( Partial_Sums (z * seq) = z * (Partial_Sums seq) & Partial_Sums (seq * z) = (Partial_Sums seq) * z ) A1: Partial_Sums (seq * z) = (Partial_Sums seq) * z proof defpred S1[ Element of NAT ] means (Partial_Sums (seq * z)) . $1 = ((Partial_Sums seq) * z) . $1; A2: 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 A3: S1[n] ; ::_thesis: S1[n + 1] (Partial_Sums (seq * z)) . (n + 1) = ((Partial_Sums (seq * z)) . n) + ((seq * z) . (n + 1)) by BHSP_4:def_1 .= (((Partial_Sums seq) . n) * z) + ((seq * z) . (n + 1)) by A3, LOPBAN_3:def_6 .= (((Partial_Sums seq) . n) * z) + ((seq . (n + 1)) * z) by LOPBAN_3:def_6 .= (((Partial_Sums seq) . n) + (seq . (n + 1))) * z by LOPBAN_3:38 .= ((Partial_Sums seq) . (n + 1)) * z by BHSP_4:def_1 .= ((Partial_Sums seq) * z) . (n + 1) by LOPBAN_3:def_6 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums (seq * z)) . 0 = (seq * z) . 0 by BHSP_4:def_1 .= (seq . 0) * z by LOPBAN_3:def_6 .= ((Partial_Sums seq) . 0) * z by BHSP_4:def_1 .= ((Partial_Sums seq) * z) . 0 by LOPBAN_3:def_6 ; then A4: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2); hence Partial_Sums (seq * z) = (Partial_Sums seq) * z by FUNCT_2:63; ::_thesis: verum end; Partial_Sums (z * seq) = z * (Partial_Sums seq) proof defpred S1[ Element of NAT ] means (Partial_Sums (z * seq)) . $1 = (z * (Partial_Sums seq)) . $1; A5: 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 A6: 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 A6, LOPBAN_3:def_5 .= (z * ((Partial_Sums seq) . n)) + (z * (seq . (n + 1))) by LOPBAN_3:def_5 .= z * (((Partial_Sums seq) . n) + (seq . (n + 1))) by LOPBAN_3:38 .= z * ((Partial_Sums seq) . (n + 1)) by BHSP_4:def_1 .= (z * (Partial_Sums seq)) . (n + 1) by LOPBAN_3: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 LOPBAN_3:def_5 .= z * ((Partial_Sums seq) . 0) by BHSP_4:def_1 .= (z * (Partial_Sums seq)) . 0 by LOPBAN_3:def_5 ; then A7: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A7, A5); hence Partial_Sums (z * seq) = z * (Partial_Sums seq) by FUNCT_2:63; ::_thesis: verum end; hence ( Partial_Sums (z * seq) = z * (Partial_Sums seq) & Partial_Sums (seq * z) = (Partial_Sums seq) * z ) by A1; ::_thesis: verum end; theorem Th10: :: LOPBAN_4:10 for X being Banach_Algebra for k being Element of NAT for seq being sequence of X holds ||.((Partial_Sums seq) . k).|| <= (Partial_Sums ||.seq.||) . k proof let X be Banach_Algebra; ::_thesis: for k being Element of NAT for seq being sequence of X holds ||.((Partial_Sums seq) . k).|| <= (Partial_Sums ||.seq.||) . k let k be Element of NAT ; ::_thesis: for seq being sequence of X holds ||.((Partial_Sums seq) . k).|| <= (Partial_Sums ||.seq.||) . k let seq be sequence of X; ::_thesis: ||.((Partial_Sums seq) . k).|| <= (Partial_Sums ||.seq.||) . k defpred S1[ Element of NAT ] means ||.((Partial_Sums seq) . $1).|| <= (Partial_Sums ||.seq.||) . $1; A1: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ S1[k_+_1] let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume S1[k] ; ::_thesis: S1[k + 1] then A2: ||.((Partial_Sums seq) . k).|| + ||.(seq . (k + 1)).|| <= ((Partial_Sums ||.seq.||) . k) + ||.(seq . (k + 1)).|| by XREAL_1:6; A3: ||.(((Partial_Sums seq) . k) + (seq . (k + 1))).|| <= ||.((Partial_Sums seq) . k).|| + ||.(seq . (k + 1)).|| by NORMSP_1:def_1; ||.((Partial_Sums seq) . (k + 1)).|| = ||.(((Partial_Sums seq) . k) + (seq . (k + 1))).|| by BHSP_4:def_1; then ||.((Partial_Sums seq) . (k + 1)).|| <= ((Partial_Sums ||.seq.||) . k) + ||.(seq . (k + 1)).|| by A3, A2, XXREAL_0:2; then ||.((Partial_Sums seq) . (k + 1)).|| <= ((Partial_Sums ||.seq.||) . k) + (||.seq.|| . (k + 1)) by NORMSP_0:def_4; hence S1[k + 1] by SERIES_1:def_1; ::_thesis: verum end; (Partial_Sums ||.seq.||) . 0 = ||.seq.|| . 0 by SERIES_1:def_1 .= ||.(seq . 0).|| by NORMSP_0:def_4 ; then A4: S1[ 0 ] by BHSP_4:def_1; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A4, A1); hence ||.((Partial_Sums seq) . k).|| <= (Partial_Sums ||.seq.||) . k ; ::_thesis: verum end; theorem Th11: :: LOPBAN_4:11 for X being Banach_Algebra for m being Element of NAT for seq1, seq2 being sequence of X st ( for n being Element of NAT st n <= m holds seq1 . n = seq2 . n ) holds (Partial_Sums seq1) . m = (Partial_Sums seq2) . m proof let X be Banach_Algebra; ::_thesis: for m being Element of NAT for seq1, seq2 being sequence of X st ( for n being Element of NAT st n <= m holds seq1 . n = seq2 . n ) holds (Partial_Sums seq1) . m = (Partial_Sums seq2) . m let m be Element of NAT ; ::_thesis: for seq1, seq2 being sequence of X st ( for n being Element of NAT st n <= m holds seq1 . n = seq2 . n ) holds (Partial_Sums seq1) . m = (Partial_Sums seq2) . m let seq1, seq2 be sequence of X; ::_thesis: ( ( for n being Element of NAT st n <= m holds seq1 . n = seq2 . n ) implies (Partial_Sums seq1) . m = (Partial_Sums seq2) . m ) defpred S1[ Element of NAT ] means ( $1 <= m implies (Partial_Sums seq1) . $1 = (Partial_Sums seq2) . $1 ); assume A1: for n being Element of NAT st n <= m holds seq1 . n = seq2 . n ; ::_thesis: (Partial_Sums seq1) . m = (Partial_Sums seq2) . m 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] assume A4: k + 1 <= m ; ::_thesis: (Partial_Sums seq1) . (k + 1) = (Partial_Sums seq2) . (k + 1) k < k + 1 by XREAL_1:29; hence (Partial_Sums seq1) . (k + 1) = ((Partial_Sums seq2) . k) + (seq1 . (k + 1)) by A3, A4, BHSP_4:def_1, XXREAL_0:2 .= ((Partial_Sums seq2) . k) + (seq2 . (k + 1)) by A1, A4 .= (Partial_Sums seq2) . (k + 1) by BHSP_4:def_1 ; ::_thesis: verum end; A5: S1[ 0 ] proof assume 0 <= m ; ::_thesis: (Partial_Sums seq1) . 0 = (Partial_Sums seq2) . 0 thus (Partial_Sums seq1) . 0 = seq1 . 0 by BHSP_4:def_1 .= seq2 . 0 by A1 .= (Partial_Sums seq2) . 0 by BHSP_4:def_1 ; ::_thesis: verum end; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A5, A2); hence (Partial_Sums seq1) . m = (Partial_Sums seq2) . m ; ::_thesis: verum end; theorem Th12: :: LOPBAN_4:12 for X being Banach_Algebra for seq being sequence of X for rseq being Real_Sequence st ( for n being Element of NAT holds ||.(seq . n).|| <= rseq . n ) & rseq is convergent & lim rseq = 0 holds ( seq is convergent & lim seq = 0. X ) proof let X be Banach_Algebra; ::_thesis: for seq being sequence of X for rseq being Real_Sequence st ( for n being Element of NAT holds ||.(seq . n).|| <= rseq . n ) & rseq is convergent & lim rseq = 0 holds ( seq is convergent & lim seq = 0. X ) let seq be sequence of X; ::_thesis: for rseq being Real_Sequence st ( for n being Element of NAT holds ||.(seq . n).|| <= rseq . n ) & rseq is convergent & lim rseq = 0 holds ( seq is convergent & lim seq = 0. X ) let rseq be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds ||.(seq . n).|| <= rseq . n ) & rseq is convergent & lim rseq = 0 implies ( seq is convergent & lim seq = 0. X ) ) assume that A1: for n being Element of NAT holds ||.(seq . n).|| <= rseq . n and A2: rseq is convergent and A3: lim rseq = 0 ; ::_thesis: ( seq is convergent & lim seq = 0. X ) now__::_thesis:_for_p_being_real_number_st_0_<_p_holds_ ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ ||.((seq_._m)_-_(0._X)).||_<_p let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((seq . m) - (0. X)).|| < p ) assume 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((seq . m) - (0. X)).|| < p then consider n being Element of NAT such that A4: for m being Element of NAT st n <= m holds abs ((rseq . m) - 0) < p by A2, A3, SEQ_2:def_7; now__::_thesis:_for_m_being_Element_of_NAT_st_n_<=_m_holds_ ||.((seq_._m)_-_(0._X)).||_<_p let m be Element of NAT ; ::_thesis: ( n <= m implies ||.((seq . m) - (0. X)).|| < p ) assume n <= m ; ::_thesis: ||.((seq . m) - (0. X)).|| < p then A5: abs ((rseq . m) - 0) < p by A4; A6: ||.((seq . m) - (0. X)).|| = ||.(seq . m).|| by RLVECT_1:13; A7: rseq . m <= abs (rseq . m) by ABSVALUE:4; ||.(seq . m).|| <= rseq . m by A1; then ||.((seq . m) - (0. X)).|| <= abs (rseq . m) by A6, A7, XXREAL_0:2; hence ||.((seq . m) - (0. X)).|| < p by A5, 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) - (0. X)).|| < p ; ::_thesis: verum end; then A8: 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) - (0. X)).|| < p ; hence seq is convergent by NORMSP_1:def_6; ::_thesis: lim seq = 0. X hence lim seq = 0. X by A8, NORMSP_1:def_7; ::_thesis: verum end; definition let X be Banach_Algebra; let z be Element of X; funcz rExpSeq -> sequence of X means :Def2: :: LOPBAN_4:def 2 for n being Element of NAT holds it . n = (1 / (n !)) * (z #N n); existence ex b1 being sequence of X st for n being Element of NAT holds b1 . n = (1 / (n !)) * (z #N n) proof deffunc H1( Element of NAT ) -> Element of the carrier of X = (1 / ($1 !)) * (z #N $1); thus ex s being sequence of X st for n being Element of NAT holds s . n = H1(n) from FUNCT_2:sch_4(); ::_thesis: verum end; uniqueness for b1, b2 being sequence of X st ( for n being Element of NAT holds b1 . n = (1 / (n !)) * (z #N n) ) & ( for n being Element of NAT holds b2 . n = (1 / (n !)) * (z #N n) ) holds b1 = b2 proof let S1, S2 be sequence of X; ::_thesis: ( ( for n being Element of NAT holds S1 . n = (1 / (n !)) * (z #N n) ) & ( for n being Element of NAT holds S2 . n = (1 / (n !)) * (z #N n) ) implies S1 = S2 ) assume that A1: for n being Element of NAT holds S1 . n = (1 / (n !)) * (z #N n) and A2: for n being Element of NAT holds S2 . n = (1 / (n !)) * (z #N 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 = (1 / (n !)) * (z #N 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 Def2 defines rExpSeq LOPBAN_4:def_2_:_ for X being Banach_Algebra for z being Element of X for b3 being sequence of X holds ( b3 = z rExpSeq iff for n being Element of NAT holds b3 . n = (1 / (n !)) * (z #N n) ); scheme :: LOPBAN_4:sch 1 ExNormSpaceCASE{ F1() -> Banach_Algebra, F2( Element of NAT , Element of NAT ) -> Point of F1() } : for k being Element of NAT ex seq being sequence of F1() st for n being Element of NAT holds ( ( n <= k implies seq . n = F2(k,n) ) & ( n > k implies seq . n = 0. F1() ) ) proof let k be Element of NAT ; ::_thesis: ex seq being sequence of F1() st for n being Element of NAT holds ( ( n <= k implies seq . n = F2(k,n) ) & ( n > k implies seq . n = 0. F1() ) ) defpred S1[ set , set ] means ex n being Element of NAT st ( n = $1 & ( n <= k implies $2 = F2(k,n) ) & ( n > k implies $2 = 0. F1() ) ); A1: now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_ ex_y_being_set_st_S1[x,y] let x be set ; ::_thesis: ( x in NAT implies ex y being set st S1[x,y] ) assume x in NAT ; ::_thesis: ex y being set st S1[x,y] then consider n being Element of NAT such that A2: n = x ; reconsider chk = CHK (n,k) as Element of REAL by XREAL_0:def_1; A3: now__::_thesis:_(_n_>_k_implies_chk_*_F2(k,n)_=_0._F1()_) assume n > k ; ::_thesis: chk * F2(k,n) = 0. F1() hence chk * F2(k,n) = 0 * F2(k,n) by SIN_COS:def_1 .= 0. F1() by RLVECT_1:10 ; ::_thesis: verum end; reconsider y = chk * F2(k,n) as set ; take y = y; ::_thesis: S1[x,y] now__::_thesis:_(_n_<=_k_implies_chk_*_F2(k,n)_=_F2(k,n)_) assume n <= k ; ::_thesis: chk * F2(k,n) = F2(k,n) hence chk * F2(k,n) = 1 * F2(k,n) by SIN_COS:def_1 .= F2(k,n) by RLVECT_1:def_8 ; ::_thesis: verum end; hence S1[x,y] by A2, A3; ::_thesis: verum end; consider f being Function such that A4: dom f = NAT and A5: for x being set st x in NAT holds S1[x,f . x] from CLASSES1:sch_1(A1); now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_ f_._x_in_the_carrier_of_F1() let x be set ; ::_thesis: ( x in NAT implies f . x in the carrier of F1() ) assume x in NAT ; ::_thesis: f . x in the carrier of F1() then ex n being Element of NAT st ( n = x & ( n <= k implies f . x = F2(k,n) ) & ( n > k implies f . x = 0. F1() ) ) by A5; hence f . x in the carrier of F1() ; ::_thesis: verum end; then reconsider f = f as sequence of F1() by A4, FUNCT_2:3; take seq = f; ::_thesis: for n being Element of NAT holds ( ( n <= k implies seq . n = F2(k,n) ) & ( n > k implies seq . n = 0. F1() ) ) let n be Element of NAT ; ::_thesis: ( ( n <= k implies seq . n = F2(k,n) ) & ( n > k implies seq . n = 0. F1() ) ) ex l being Element of NAT st ( l = n & ( l <= k implies seq . n = F2(k,l) ) & ( l > k implies seq . n = 0. F1() ) ) by A5; hence ( ( n <= k implies seq . n = F2(k,n) ) & ( n > k implies seq . n = 0. F1() ) ) ; ::_thesis: verum end; theorem Th13: :: LOPBAN_4:13 ( ( for k being Element of NAT st 0 < k holds ((k -' 1) !) * k = k ! ) & ( for m, k being Element of NAT st k <= m holds ((m -' k) !) * ((m + 1) - k) = ((m + 1) -' k) ! ) ) proof A1: now__::_thesis:_for_k_being_Element_of_NAT_st_0_<_k_holds_ k_!_=_((k_-'_1)_!)_*_k let k be Element of NAT ; ::_thesis: ( 0 < k implies k ! = ((k -' 1) !) * k ) assume 0 < k ; ::_thesis: k ! = ((k -' 1) !) * k then 0 + 1 <= k by INT_1:7; then (k -' 1) + 1 = (k - 1) + 1 by XREAL_1:233 .= k ; hence k ! = ((k -' 1) !) * k by NEWTON:15; ::_thesis: verum end; now__::_thesis:_for_m,_k_being_Element_of_NAT_st_k_<=_m_holds_ ((m_+_1)_-'_k)_!_=_((m_-'_k)_!)_*_((m_+_1)_-_k) let m, k be Element of NAT ; ::_thesis: ( k <= m implies ((m + 1) -' k) ! = ((m -' k) !) * ((m + 1) - k) ) assume A2: k <= m ; ::_thesis: ((m + 1) -' k) ! = ((m -' k) !) * ((m + 1) - k) m <= m + 1 by XREAL_1:29; then (m + 1) -' k = (m + 1) - k by A2, XREAL_1:233, XXREAL_0:2 .= (m - k) + 1 .= (m -' k) + 1 by A2, XREAL_1:233 ; hence ((m + 1) -' k) ! = ((m -' k) !) * ((m -' k) + 1) by NEWTON:15 .= ((m -' k) !) * ((m - k) + 1) by A2, XREAL_1:233 .= ((m -' k) !) * ((m + 1) - k) ; ::_thesis: verum end; hence ( ( for k being Element of NAT st 0 < k holds ((k -' 1) !) * k = k ! ) & ( for m, k being Element of NAT st k <= m holds ((m -' k) !) * ((m + 1) - k) = ((m + 1) -' k) ! ) ) by A1; ::_thesis: verum end; definition let n be Element of NAT ; func Coef n -> Real_Sequence means :Def3: :: LOPBAN_4:def 3 for k being Element of NAT holds ( ( k <= n implies it . k = (n !) / ((k !) * ((n -' k) !)) ) & ( k > n implies it . k = 0 ) ); existence ex b1 being Real_Sequence st for k being Element of NAT holds ( ( k <= n implies b1 . k = (n !) / ((k !) * ((n -' k) !)) ) & ( k > n implies b1 . k = 0 ) ) proof deffunc H1( Element of NAT , Element of NAT ) -> Element of REAL = ($1 !) / (($2 !) * (($1 -' $2) !)); for n being Element of NAT ex seq being Real_Sequence st for k being Element of NAT holds ( ( k <= n implies seq . k = H1(n,k) ) & ( k > n implies seq . k = 0 ) ) from SIN_COS:sch_2(); hence ex b1 being Real_Sequence st for k being Element of NAT holds ( ( k <= n implies b1 . k = (n !) / ((k !) * ((n -' k) !)) ) & ( k > n implies b1 . k = 0 ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Real_Sequence st ( for k being Element of NAT holds ( ( k <= n implies b1 . k = (n !) / ((k !) * ((n -' k) !)) ) & ( k > n implies b1 . k = 0 ) ) ) & ( for k being Element of NAT holds ( ( k <= n implies b2 . k = (n !) / ((k !) * ((n -' k) !)) ) & ( k > n implies b2 . k = 0 ) ) ) holds b1 = b2 proof let seq1, seq2 be Real_Sequence; ::_thesis: ( ( for k being Element of NAT holds ( ( k <= n implies seq1 . k = (n !) / ((k !) * ((n -' k) !)) ) & ( k > n implies seq1 . k = 0 ) ) ) & ( for k being Element of NAT holds ( ( k <= n implies seq2 . k = (n !) / ((k !) * ((n -' k) !)) ) & ( k > n implies seq2 . k = 0 ) ) ) implies seq1 = seq2 ) assume that A1: for k being Element of NAT holds ( ( k <= n implies seq1 . k = (n !) / ((k !) * ((n -' k) !)) ) & ( k > n implies seq1 . k = 0 ) ) and A2: for k being Element of NAT holds ( ( k <= n implies seq2 . k = (n !) / ((k !) * ((n -' k) !)) ) & ( k > n implies seq2 . k = 0 ) ) ; ::_thesis: seq1 = seq2 now__::_thesis:_for_k_being_Element_of_NAT_holds_seq1_._k_=_seq2_._k let k be Element of NAT ; ::_thesis: seq1 . b1 = seq2 . b1 percases ( k <= n or k > n ) ; supposeA3: k <= n ; ::_thesis: seq1 . b1 = seq2 . b1 hence seq1 . k = (n !) / ((k !) * ((n -' k) !)) by A1 .= seq2 . k by A2, A3 ; ::_thesis: verum end; supposeA4: k > n ; ::_thesis: seq1 . b1 = seq2 . b1 hence seq1 . k = 0 by A1 .= seq2 . k by A2, A4 ; ::_thesis: verum end; end; end; hence seq1 = seq2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def3 defines Coef LOPBAN_4:def_3_:_ for n being Element of NAT for b2 being Real_Sequence holds ( b2 = Coef n iff for k being Element of NAT holds ( ( k <= n implies b2 . k = (n !) / ((k !) * ((n -' k) !)) ) & ( k > n implies b2 . k = 0 ) ) ); definition let n be Element of NAT ; func Coef_e n -> Real_Sequence means :Def4: :: LOPBAN_4:def 4 for k being Element of NAT holds ( ( k <= n implies it . k = 1 / ((k !) * ((n -' k) !)) ) & ( k > n implies it . k = 0 ) ); existence ex b1 being Real_Sequence st for k being Element of NAT holds ( ( k <= n implies b1 . k = 1 / ((k !) * ((n -' k) !)) ) & ( k > n implies b1 . k = 0 ) ) proof deffunc H1( Element of NAT , Element of NAT ) -> Element of REAL = 1 / (($2 !) * (($1 -' $2) !)); for n being Element of NAT ex seq being Real_Sequence st for k being Element of NAT holds ( ( k <= n implies seq . k = H1(n,k) ) & ( k > n implies seq . k = 0 ) ) from SIN_COS:sch_2(); hence ex b1 being Real_Sequence st for k being Element of NAT holds ( ( k <= n implies b1 . k = 1 / ((k !) * ((n -' k) !)) ) & ( k > n implies b1 . k = 0 ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Real_Sequence st ( for k being Element of NAT holds ( ( k <= n implies b1 . k = 1 / ((k !) * ((n -' k) !)) ) & ( k > n implies b1 . k = 0 ) ) ) & ( for k being Element of NAT holds ( ( k <= n implies b2 . k = 1 / ((k !) * ((n -' k) !)) ) & ( k > n implies b2 . k = 0 ) ) ) holds b1 = b2 proof let seq1, seq2 be Real_Sequence; ::_thesis: ( ( for k being Element of NAT holds ( ( k <= n implies seq1 . k = 1 / ((k !) * ((n -' k) !)) ) & ( k > n implies seq1 . k = 0 ) ) ) & ( for k being Element of NAT holds ( ( k <= n implies seq2 . k = 1 / ((k !) * ((n -' k) !)) ) & ( k > n implies seq2 . k = 0 ) ) ) implies seq1 = seq2 ) assume that A1: for k being Element of NAT holds ( ( k <= n implies seq1 . k = 1 / ((k !) * ((n -' k) !)) ) & ( k > n implies seq1 . k = 0 ) ) and A2: for k being Element of NAT holds ( ( k <= n implies seq2 . k = 1 / ((k !) * ((n -' k) !)) ) & ( k > n implies seq2 . k = 0 ) ) ; ::_thesis: seq1 = seq2 now__::_thesis:_for_k_being_Element_of_NAT_holds_seq1_._k_=_seq2_._k let k be Element of NAT ; ::_thesis: seq1 . b1 = seq2 . b1 percases ( k <= n or k > n ) ; supposeA3: k <= n ; ::_thesis: seq1 . b1 = seq2 . b1 hence seq1 . k = 1 / ((k !) * ((n -' k) !)) by A1 .= seq2 . k by A2, A3 ; ::_thesis: verum end; supposeA4: k > n ; ::_thesis: seq1 . b1 = seq2 . b1 hence seq1 . k = 0 by A1 .= seq2 . k by A2, A4 ; ::_thesis: verum end; end; end; hence seq1 = seq2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def4 defines Coef_e LOPBAN_4:def_4_:_ for n being Element of NAT for b2 being Real_Sequence holds ( b2 = Coef_e n iff for k being Element of NAT holds ( ( k <= n implies b2 . k = 1 / ((k !) * ((n -' k) !)) ) & ( k > n implies b2 . k = 0 ) ) ); definition let X be non empty ZeroStr ; let seq be sequence of X; func Shift seq -> sequence of X means :Def5: :: LOPBAN_4:def 5 ( it . 0 = 0. X & ( for k being Element of NAT holds it . (k + 1) = seq . k ) ); existence ex b1 being sequence of X st ( b1 . 0 = 0. X & ( for k being Element of NAT holds b1 . (k + 1) = seq . k ) ) proof deffunc H1( Nat, set ) -> Element of the carrier of X = seq . $1; consider f being Function of NAT, the carrier of X such that A1: ( f . 0 = 0. X & ( for n being Nat holds f . (n + 1) = H1(n,f . n) ) ) from NAT_1:sch_12(); take f ; ::_thesis: ( f . 0 = 0. X & ( for k being Element of NAT holds f . (k + 1) = seq . k ) ) thus ( f . 0 = 0. X & ( for k being Element of NAT holds f . (k + 1) = seq . k ) ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being sequence of X st b1 . 0 = 0. X & ( for k being Element of NAT holds b1 . (k + 1) = seq . k ) & b2 . 0 = 0. X & ( for k being Element of NAT holds b2 . (k + 1) = seq . k ) holds b1 = b2 proof let seq1, seq2 be sequence of X; ::_thesis: ( seq1 . 0 = 0. X & ( for k being Element of NAT holds seq1 . (k + 1) = seq . k ) & seq2 . 0 = 0. X & ( for k being Element of NAT holds seq2 . (k + 1) = seq . k ) implies seq1 = seq2 ) assume that A2: seq1 . 0 = 0. X and A3: for n being Element of NAT holds seq1 . (n + 1) = seq . n and A4: seq2 . 0 = 0. X and A5: for n being Element of NAT holds seq2 . (n + 1) = seq . n ; ::_thesis: seq1 = seq2 defpred S1[ Element of NAT ] means seq1 . $1 = seq2 . $1; A6: 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 seq1 . k = seq2 . k ; ::_thesis: S1[k + 1] thus seq1 . (k + 1) = seq . k by A3 .= seq2 . (k + 1) by A5 ; ::_thesis: verum end; A7: S1[ 0 ] by A2, A4; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A7, A6); hence seq1 = seq2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def5 defines Shift LOPBAN_4:def_5_:_ for X being non empty ZeroStr for seq, b3 being sequence of X holds ( b3 = Shift seq iff ( b3 . 0 = 0. X & ( for k being Element of NAT holds b3 . (k + 1) = seq . k ) ) ); definition let n be Element of NAT ; let X be Banach_Algebra; let z, w be Element of X; func Expan (n,z,w) -> sequence of X means :Def6: :: LOPBAN_4:def 6 for k being Element of NAT holds ( ( k <= n implies it . k = (((Coef n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies it . k = 0. X ) ); existence ex b1 being sequence of X st for k being Element of NAT holds ( ( k <= n implies b1 . k = (((Coef n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies b1 . k = 0. X ) ) proof deffunc H1( Element of NAT , Element of NAT ) -> Element of the carrier of X = (((Coef $1) . $2) * (z #N $2)) * (w #N ($1 -' $2)); for n being Element of NAT ex seq being sequence of X st for k being Element of NAT holds ( ( k <= n implies seq . k = H1(n,k) ) & ( k > n implies seq . k = 0. X ) ) from LOPBAN_4:sch_1(); hence ex b1 being sequence of X st for k being Element of NAT holds ( ( k <= n implies b1 . k = (((Coef n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies b1 . k = 0. X ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being sequence of X st ( for k being Element of NAT holds ( ( k <= n implies b1 . k = (((Coef n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies b1 . k = 0. X ) ) ) & ( for k being Element of NAT holds ( ( k <= n implies b2 . k = (((Coef n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies b2 . k = 0. X ) ) ) holds b1 = b2 proof let seq1, seq2 be sequence of X; ::_thesis: ( ( for k being Element of NAT holds ( ( k <= n implies seq1 . k = (((Coef n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies seq1 . k = 0. X ) ) ) & ( for k being Element of NAT holds ( ( k <= n implies seq2 . k = (((Coef n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies seq2 . k = 0. X ) ) ) implies seq1 = seq2 ) assume that A1: for k being Element of NAT holds ( ( k <= n implies seq1 . k = (((Coef n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( k > n implies seq1 . k = 0. X ) ) and A2: for k being Element of NAT holds ( ( k <= n implies seq2 . k = (((Coef n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( k > n implies seq2 . k = 0. X ) ) ; ::_thesis: seq1 = seq2 now__::_thesis:_for_k_being_Element_of_NAT_holds_seq1_._k_=_seq2_._k let k be Element of NAT ; ::_thesis: seq1 . b1 = seq2 . b1 percases ( k <= n or k > n ) ; supposeA3: k <= n ; ::_thesis: seq1 . b1 = seq2 . b1 hence seq1 . k = (((Coef n) . k) * (z #N k)) * (w #N (n -' k)) by A1 .= seq2 . k by A2, A3 ; ::_thesis: verum end; supposeA4: k > n ; ::_thesis: seq1 . b1 = seq2 . b1 hence seq1 . k = 0. X by A1 .= seq2 . k by A2, A4 ; ::_thesis: verum end; end; end; hence seq1 = seq2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def6 defines Expan LOPBAN_4:def_6_:_ for n being Element of NAT for X being Banach_Algebra for z, w being Element of X for b5 being sequence of X holds ( b5 = Expan (n,z,w) iff for k being Element of NAT holds ( ( k <= n implies b5 . k = (((Coef n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies b5 . k = 0. X ) ) ); definition let n be Element of NAT ; let X be Banach_Algebra; let z, w be Element of X; func Expan_e (n,z,w) -> sequence of X means :Def7: :: LOPBAN_4:def 7 for k being Element of NAT holds ( ( k <= n implies it . k = (((Coef_e n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies it . k = 0. X ) ); existence ex b1 being sequence of X st for k being Element of NAT holds ( ( k <= n implies b1 . k = (((Coef_e n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies b1 . k = 0. X ) ) proof deffunc H1( Element of NAT , Element of NAT ) -> Element of the carrier of X = (((Coef_e $1) . $2) * (z #N $2)) * (w #N ($1 -' $2)); for n being Element of NAT ex seq being sequence of X st for k being Element of NAT holds ( ( k <= n implies seq . k = H1(n,k) ) & ( k > n implies seq . k = 0. X ) ) from LOPBAN_4:sch_1(); hence ex b1 being sequence of X st for k being Element of NAT holds ( ( k <= n implies b1 . k = (((Coef_e n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies b1 . k = 0. X ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being sequence of X st ( for k being Element of NAT holds ( ( k <= n implies b1 . k = (((Coef_e n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies b1 . k = 0. X ) ) ) & ( for k being Element of NAT holds ( ( k <= n implies b2 . k = (((Coef_e n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies b2 . k = 0. X ) ) ) holds b1 = b2 proof let seq1, seq2 be sequence of X; ::_thesis: ( ( for k being Element of NAT holds ( ( k <= n implies seq1 . k = (((Coef_e n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies seq1 . k = 0. X ) ) ) & ( for k being Element of NAT holds ( ( k <= n implies seq2 . k = (((Coef_e n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies seq2 . k = 0. X ) ) ) implies seq1 = seq2 ) assume that A1: for k being Element of NAT holds ( ( k <= n implies seq1 . k = (((Coef_e n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( k > n implies seq1 . k = 0. X ) ) and A2: for k being Element of NAT holds ( ( k <= n implies seq2 . k = (((Coef_e n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( k > n implies seq2 . k = 0. X ) ) ; ::_thesis: seq1 = seq2 now__::_thesis:_for_k_being_Element_of_NAT_holds_seq1_._k_=_seq2_._k let k be Element of NAT ; ::_thesis: seq1 . b1 = seq2 . b1 percases ( k <= n or k > n ) ; supposeA3: k <= n ; ::_thesis: seq1 . b1 = seq2 . b1 hence seq1 . k = (((Coef_e n) . k) * (z #N k)) * (w #N (n -' k)) by A1 .= seq2 . k by A2, A3 ; ::_thesis: verum end; supposeA4: k > n ; ::_thesis: seq1 . b1 = seq2 . b1 hence seq1 . k = 0. X by A1 .= seq2 . k by A2, A4 ; ::_thesis: verum end; end; end; hence seq1 = seq2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def7 defines Expan_e LOPBAN_4:def_7_:_ for n being Element of NAT for X being Banach_Algebra for z, w being Element of X for b5 being sequence of X holds ( b5 = Expan_e (n,z,w) iff for k being Element of NAT holds ( ( k <= n implies b5 . k = (((Coef_e n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies b5 . k = 0. X ) ) ); definition let n be Element of NAT ; let X be Banach_Algebra; let z, w be Element of X; func Alfa (n,z,w) -> sequence of X means :Def8: :: LOPBAN_4:def 8 for k being Element of NAT holds ( ( k <= n implies it . k = ((z rExpSeq) . k) * ((Partial_Sums (w rExpSeq)) . (n -' k)) ) & ( n < k implies it . k = 0. X ) ); existence ex b1 being sequence of X st for k being Element of NAT holds ( ( k <= n implies b1 . k = ((z rExpSeq) . k) * ((Partial_Sums (w rExpSeq)) . (n -' k)) ) & ( n < k implies b1 . k = 0. X ) ) proof deffunc H1( Element of NAT , Element of NAT ) -> Element of the carrier of X = ((z rExpSeq) . $2) * ((Partial_Sums (w rExpSeq)) . ($1 -' $2)); for n being Element of NAT ex seq being sequence of X st for k being Element of NAT holds ( ( k <= n implies seq . k = H1(n,k) ) & ( k > n implies seq . k = 0. X ) ) from LOPBAN_4:sch_1(); hence ex b1 being sequence of X st for k being Element of NAT holds ( ( k <= n implies b1 . k = ((z rExpSeq) . k) * ((Partial_Sums (w rExpSeq)) . (n -' k)) ) & ( n < k implies b1 . k = 0. X ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being sequence of X st ( for k being Element of NAT holds ( ( k <= n implies b1 . k = ((z rExpSeq) . k) * ((Partial_Sums (w rExpSeq)) . (n -' k)) ) & ( n < k implies b1 . k = 0. X ) ) ) & ( for k being Element of NAT holds ( ( k <= n implies b2 . k = ((z rExpSeq) . k) * ((Partial_Sums (w rExpSeq)) . (n -' k)) ) & ( n < k implies b2 . k = 0. X ) ) ) holds b1 = b2 proof let seq1, seq2 be sequence of X; ::_thesis: ( ( for k being Element of NAT holds ( ( k <= n implies seq1 . k = ((z rExpSeq) . k) * ((Partial_Sums (w rExpSeq)) . (n -' k)) ) & ( n < k implies seq1 . k = 0. X ) ) ) & ( for k being Element of NAT holds ( ( k <= n implies seq2 . k = ((z rExpSeq) . k) * ((Partial_Sums (w rExpSeq)) . (n -' k)) ) & ( n < k implies seq2 . k = 0. X ) ) ) implies seq1 = seq2 ) assume that A1: for k being Element of NAT holds ( ( k <= n implies seq1 . k = ((z rExpSeq) . k) * ((Partial_Sums (w rExpSeq)) . (n -' k)) ) & ( k > n implies seq1 . k = 0. X ) ) and A2: for k being Element of NAT holds ( ( k <= n implies seq2 . k = ((z rExpSeq) . k) * ((Partial_Sums (w rExpSeq)) . (n -' k)) ) & ( k > n implies seq2 . k = 0. X ) ) ; ::_thesis: seq1 = seq2 now__::_thesis:_for_k_being_Element_of_NAT_holds_seq1_._k_=_seq2_._k let k be Element of NAT ; ::_thesis: seq1 . b1 = seq2 . b1 percases ( k <= n or k > n ) ; supposeA3: k <= n ; ::_thesis: seq1 . b1 = seq2 . b1 hence seq1 . k = ((z rExpSeq) . k) * ((Partial_Sums (w rExpSeq)) . (n -' k)) by A1 .= seq2 . k by A2, A3 ; ::_thesis: verum end; supposeA4: k > n ; ::_thesis: seq1 . b1 = seq2 . b1 hence seq1 . k = 0. X by A1 .= seq2 . k by A2, A4 ; ::_thesis: verum end; end; end; hence seq1 = seq2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def8 defines Alfa LOPBAN_4:def_8_:_ for n being Element of NAT for X being Banach_Algebra for z, w being Element of X for b5 being sequence of X holds ( b5 = Alfa (n,z,w) iff for k being Element of NAT holds ( ( k <= n implies b5 . k = ((z rExpSeq) . k) * ((Partial_Sums (w rExpSeq)) . (n -' k)) ) & ( n < k implies b5 . k = 0. X ) ) ); definition let X be Banach_Algebra; let z, w be Element of X; let n be Element of NAT ; func Conj (n,z,w) -> sequence of X means :Def9: :: LOPBAN_4:def 9 for k being Element of NAT holds ( ( k <= n implies it . k = ((z rExpSeq) . k) * (((Partial_Sums (w rExpSeq)) . n) - ((Partial_Sums (w rExpSeq)) . (n -' k))) ) & ( n < k implies it . k = 0. X ) ); existence ex b1 being sequence of X st for k being Element of NAT holds ( ( k <= n implies b1 . k = ((z rExpSeq) . k) * (((Partial_Sums (w rExpSeq)) . n) - ((Partial_Sums (w rExpSeq)) . (n -' k))) ) & ( n < k implies b1 . k = 0. X ) ) proof deffunc H1( Element of NAT , Element of NAT ) -> Element of the carrier of X = ((z rExpSeq) . $2) * (((Partial_Sums (w rExpSeq)) . $1) - ((Partial_Sums (w rExpSeq)) . ($1 -' $2))); for n being Element of NAT ex seq being sequence of X st for k being Element of NAT holds ( ( k <= n implies seq . k = H1(n,k) ) & ( k > n implies seq . k = 0. X ) ) from LOPBAN_4:sch_1(); hence ex b1 being sequence of X st for k being Element of NAT holds ( ( k <= n implies b1 . k = ((z rExpSeq) . k) * (((Partial_Sums (w rExpSeq)) . n) - ((Partial_Sums (w rExpSeq)) . (n -' k))) ) & ( n < k implies b1 . k = 0. X ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being sequence of X st ( for k being Element of NAT holds ( ( k <= n implies b1 . k = ((z rExpSeq) . k) * (((Partial_Sums (w rExpSeq)) . n) - ((Partial_Sums (w rExpSeq)) . (n -' k))) ) & ( n < k implies b1 . k = 0. X ) ) ) & ( for k being Element of NAT holds ( ( k <= n implies b2 . k = ((z rExpSeq) . k) * (((Partial_Sums (w rExpSeq)) . n) - ((Partial_Sums (w rExpSeq)) . (n -' k))) ) & ( n < k implies b2 . k = 0. X ) ) ) holds b1 = b2 proof let seq1, seq2 be sequence of X; ::_thesis: ( ( for k being Element of NAT holds ( ( k <= n implies seq1 . k = ((z rExpSeq) . k) * (((Partial_Sums (w rExpSeq)) . n) - ((Partial_Sums (w rExpSeq)) . (n -' k))) ) & ( n < k implies seq1 . k = 0. X ) ) ) & ( for k being Element of NAT holds ( ( k <= n implies seq2 . k = ((z rExpSeq) . k) * (((Partial_Sums (w rExpSeq)) . n) - ((Partial_Sums (w rExpSeq)) . (n -' k))) ) & ( n < k implies seq2 . k = 0. X ) ) ) implies seq1 = seq2 ) assume that A1: for k being Element of NAT holds ( ( k <= n implies seq1 . k = ((z rExpSeq) . k) * (((Partial_Sums (w rExpSeq)) . n) - ((Partial_Sums (w rExpSeq)) . (n -' k))) ) & ( k > n implies seq1 . k = 0. X ) ) and A2: for k being Element of NAT holds ( ( k <= n implies seq2 . k = ((z rExpSeq) . k) * (((Partial_Sums (w rExpSeq)) . n) - ((Partial_Sums (w rExpSeq)) . (n -' k))) ) & ( k > n implies seq2 . k = 0. X ) ) ; ::_thesis: seq1 = seq2 now__::_thesis:_for_k_being_Element_of_NAT_holds_seq1_._k_=_seq2_._k let k be Element of NAT ; ::_thesis: seq1 . b1 = seq2 . b1 percases ( k <= n or k > n ) ; supposeA3: k <= n ; ::_thesis: seq1 . b1 = seq2 . b1 hence seq1 . k = ((z rExpSeq) . k) * (((Partial_Sums (w rExpSeq)) . n) - ((Partial_Sums (w rExpSeq)) . (n -' k))) by A1 .= seq2 . k by A2, A3 ; ::_thesis: verum end; supposeA4: k > n ; ::_thesis: seq1 . b1 = seq2 . b1 hence seq1 . k = 0. X by A1 .= seq2 . k by A2, A4 ; ::_thesis: verum end; end; end; hence seq1 = seq2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def9 defines Conj LOPBAN_4:def_9_:_ for X being Banach_Algebra for z, w being Element of X for n being Element of NAT for b5 being sequence of X holds ( b5 = Conj (n,z,w) iff for k being Element of NAT holds ( ( k <= n implies b5 . k = ((z rExpSeq) . k) * (((Partial_Sums (w rExpSeq)) . n) - ((Partial_Sums (w rExpSeq)) . (n -' k))) ) & ( n < k implies b5 . k = 0. X ) ) ); theorem Th14: :: LOPBAN_4:14 for X being Banach_Algebra for z being Element of X for n being Element of NAT holds ( (z rExpSeq) . (n + 1) = ((1 / (n + 1)) * z) * ((z rExpSeq) . n) & (z rExpSeq) . 0 = 1. X & ||.((z rExpSeq) . n).|| <= (||.z.|| rExpSeq) . n ) proof let X be Banach_Algebra; ::_thesis: for z being Element of X for n being Element of NAT holds ( (z rExpSeq) . (n + 1) = ((1 / (n + 1)) * z) * ((z rExpSeq) . n) & (z rExpSeq) . 0 = 1. X & ||.((z rExpSeq) . n).|| <= (||.z.|| rExpSeq) . n ) let z be Element of X; ::_thesis: for n being Element of NAT holds ( (z rExpSeq) . (n + 1) = ((1 / (n + 1)) * z) * ((z rExpSeq) . n) & (z rExpSeq) . 0 = 1. X & ||.((z rExpSeq) . n).|| <= (||.z.|| rExpSeq) . n ) let n be Element of NAT ; ::_thesis: ( (z rExpSeq) . (n + 1) = ((1 / (n + 1)) * z) * ((z rExpSeq) . n) & (z rExpSeq) . 0 = 1. X & ||.((z rExpSeq) . n).|| <= (||.z.|| rExpSeq) . n ) defpred S1[ Element of NAT ] means ||.((z rExpSeq) . $1).|| <= (||.z.|| rExpSeq) . $1; A1: (z rExpSeq) . 0 = (1 / (0 !)) * (z #N 0) by Def2 .= (1 / 1) * (1. X) by LOPBAN_3:def_9, NEWTON:12 .= 1. X by RLVECT_1:def_8 ; A2: now__::_thesis:_for_n_being_Element_of_NAT_holds_(z_rExpSeq)_._(n_+_1)_=_((1_/_(n_+_1))_*_z)_*_((z_rExpSeq)_._n) let n be Element of NAT ; ::_thesis: (z rExpSeq) . (n + 1) = ((1 / (n + 1)) * z) * ((z rExpSeq) . n) thus (z rExpSeq) . (n + 1) = (1 / ((n + 1) !)) * (z #N (n + 1)) by Def2 .= (1 / ((n + 1) !)) * (((z GeoSeq) . n) * z) by LOPBAN_3:def_9 .= (1 / ((n !) * (n + 1))) * ((z #N n) * z) by NEWTON:15 .= ((1 * 1) / ((n !) * (n + 1))) * (z * (z #N n)) by Lm1 .= ((1 / (n !)) * (1 / (n + 1))) * (z * (z #N n)) by XCMPLX_1:76 .= ((1 / (n + 1)) * z) * ((1 / (n !)) * (z #N n)) by LOPBAN_3:38 .= ((1 / (n + 1)) * z) * ((z rExpSeq) . n) by Def2 ; ::_thesis: verum end; A3: 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] ) assume A4: S1[n] ; ::_thesis: S1[n + 1] 0 <= ||.((1 / (n + 1)) * z).|| by NORMSP_1:4; then A5: ||.((1 / (n + 1)) * z).|| * ||.((z rExpSeq) . n).|| <= ||.((1 / (n + 1)) * z).|| * ((||.z.|| rExpSeq) . n) by A4, XREAL_1:64; A6: ||.(((1 / (n + 1)) * z) * ((z rExpSeq) . n)).|| <= ||.((1 / (n + 1)) * z).|| * ||.((z rExpSeq) . n).|| by LOPBAN_3:38; A7: ((1 / (n + 1)) * ||.z.||) * ((||.z.|| rExpSeq) . n) = (1 / (n + 1)) * (((||.z.|| rExpSeq) . n) * ||.z.||) .= (1 / (n + 1)) * (((||.z.|| |^ n) / (n !)) * ||.z.||) by SIN_COS:def_5 .= (1 / (n + 1)) * (((||.z.|| |^ n) * ||.z.||) / (n !)) by XCMPLX_1:74 .= (1 / (n + 1)) * ((||.z.|| |^ (n + 1)) / (n !)) by NEWTON:6 .= (||.z.|| |^ (n + 1)) / ((n !) * (n + 1)) by XCMPLX_1:103 .= (||.z.|| |^ (n + 1)) / ((n + 1) !) by NEWTON:15 .= (||.z.|| rExpSeq) . (n + 1) by SIN_COS:def_5 ; A8: ||.((1 / (n + 1)) * z).|| = (abs (1 / (n + 1))) * ||.z.|| by NORMSP_1:def_1 .= (1 / (n + 1)) * ||.z.|| by ABSVALUE:def_1 ; ||.((z rExpSeq) . (n + 1)).|| = ||.(((1 / (n + 1)) * z) * ((z rExpSeq) . n)).|| by A2; hence S1[n + 1] by A6, A8, A5, A7, XXREAL_0:2; ::_thesis: verum end; (||.z.|| rExpSeq) . 0 = (||.z.|| |^ 0) / (0 !) by SIN_COS:def_5 .= 1 / (0 !) by NEWTON:4 .= 1 / (Prod_real_n . 0) by SIN_COS:def_3 .= 1 / 1 by SIN_COS:def_2 .= 1 ; then A9: S1[ 0 ] by A1, LOPBAN_3:38; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A9, A3); hence ( (z rExpSeq) . (n + 1) = ((1 / (n + 1)) * z) * ((z rExpSeq) . n) & (z rExpSeq) . 0 = 1. X & ||.((z rExpSeq) . n).|| <= (||.z.|| rExpSeq) . n ) by A2, A1; ::_thesis: verum end; theorem Th15: :: LOPBAN_4:15 for k being Element of NAT for X being non empty ZeroStr for seq being sequence of X st 0 < k holds (Shift seq) . k = seq . (k -' 1) proof let k be Element of NAT ; ::_thesis: for X being non empty ZeroStr for seq being sequence of X st 0 < k holds (Shift seq) . k = seq . (k -' 1) let X be non empty ZeroStr ; ::_thesis: for seq being sequence of X st 0 < k holds (Shift seq) . k = seq . (k -' 1) let seq be sequence of X; ::_thesis: ( 0 < k implies (Shift seq) . k = seq . (k -' 1) ) assume A1: 0 < k ; ::_thesis: (Shift seq) . k = seq . (k -' 1) then A2: 0 + 1 <= k by INT_1:7; consider m being Nat such that A3: m + 1 = k by A1, NAT_1:6; A4: m = k - 1 by A3; m in NAT by ORDINAL1:def_12; hence (Shift seq) . k = seq . m by A3, Def5 .= seq . (k -' 1) by A2, A4, XREAL_1:233 ; ::_thesis: verum end; theorem Th16: :: LOPBAN_4:16 for X being Banach_Algebra for k being Element of NAT for seq being sequence of X holds (Partial_Sums seq) . k = ((Partial_Sums (Shift seq)) . k) + (seq . k) proof let X be Banach_Algebra; ::_thesis: for k being Element of NAT for seq being sequence of X holds (Partial_Sums seq) . k = ((Partial_Sums (Shift seq)) . k) + (seq . k) let k be Element of NAT ; ::_thesis: for seq being sequence of X holds (Partial_Sums seq) . k = ((Partial_Sums (Shift seq)) . k) + (seq . k) let seq be sequence of X; ::_thesis: (Partial_Sums seq) . k = ((Partial_Sums (Shift seq)) . k) + (seq . k) defpred S1[ Element of NAT ] means (Partial_Sums seq) . $1 = ((Partial_Sums (Shift seq)) . $1) + (seq . $1); A1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume (Partial_Sums seq) . k = ((Partial_Sums (Shift seq)) . k) + (seq . k) ; ::_thesis: S1[k + 1] hence (Partial_Sums seq) . (k + 1) = (((Partial_Sums (Shift seq)) . k) + (seq . k)) + (seq . (k + 1)) by BHSP_4:def_1 .= (((Partial_Sums (Shift seq)) . k) + ((Shift seq) . (k + 1))) + (seq . (k + 1)) by Def5 .= ((Partial_Sums (Shift seq)) . (k + 1)) + (seq . (k + 1)) by BHSP_4:def_1 ; ::_thesis: verum end; (Partial_Sums seq) . 0 = seq . 0 by BHSP_4:def_1 .= (0. X) + (seq . 0) by RLVECT_1:4 .= ((Shift seq) . 0) + (seq . 0) by Def5 .= ((Partial_Sums (Shift seq)) . 0) + (seq . 0) by BHSP_4:def_1 ; then A2: S1[ 0 ] ; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A2, A1); hence (Partial_Sums seq) . k = ((Partial_Sums (Shift seq)) . k) + (seq . k) ; ::_thesis: verum end; theorem Th17: :: LOPBAN_4:17 for X being Banach_Algebra for n being Element of NAT for z, w being Element of X st z,w are_commutative holds (z + w) #N n = (Partial_Sums (Expan (n,z,w))) . n proof let X be Banach_Algebra; ::_thesis: for n being Element of NAT for z, w being Element of X st z,w are_commutative holds (z + w) #N n = (Partial_Sums (Expan (n,z,w))) . n let n be Element of NAT ; ::_thesis: for z, w being Element of X st z,w are_commutative holds (z + w) #N n = (Partial_Sums (Expan (n,z,w))) . n let z, w be Element of X; ::_thesis: ( z,w are_commutative implies (z + w) #N n = (Partial_Sums (Expan (n,z,w))) . n ) assume A1: z,w are_commutative ; ::_thesis: (z + w) #N n = (Partial_Sums (Expan (n,z,w))) . n defpred S1[ Element of NAT ] means (z + w) #N $1 = (Partial_Sums (Expan ($1,z,w))) . $1; A2: 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] ) assume A3: (z + w) #N n = (Partial_Sums (Expan (n,z,w))) . n ; ::_thesis: S1[n + 1] A4: n < n + 1 by XREAL_1:29; now__::_thesis:_for_k_being_Element_of_NAT_holds_(((Expan_(n,z,w))_*_w)_+_(Shift_((Expan_(n,z,w))_*_z)))_._k_=_(Expan_((n_+_1),z,w))_._k let k be Element of NAT ; ::_thesis: (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k A5: now__::_thesis:_(_k_<=_n_+_1_implies_(((Expan_(n,z,w))_*_w)_+_(Shift_((Expan_(n,z,w))_*_z)))_._k_=_(Expan_((n_+_1),z,w))_._k_) A6: now__::_thesis:_(_k_<_n_+_1_implies_(((Expan_(n,z,w))_*_w)_+_(Shift_((Expan_(n,z,w))_*_z)))_._k_=_(Expan_((n_+_1),z,w))_._k_) assume A7: k < n + 1 ; ::_thesis: (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k A8: now__::_thesis:_(_k_<>_0_implies_(((Expan_(n,z,w))_*_w)_+_(Shift_((Expan_(n,z,w))_*_z)))_._k_=_(Expan_((n_+_1),z,w))_._k_) A9: ((k !) * ((n -' k) !)) * ((n + 1) - k) = (k !) * (((n -' k) !) * ((n + 1) - k)) ; A10: (k + 1) - 1 <= (n + 1) - 1 by A7, INT_1:7; then A11: (n -' k) + 1 = (n - k) + 1 by XREAL_1:233 .= (n + 1) - k .= (n + 1) -' k by A7, XREAL_1:233 ; (n + 1) - k <> 0 by A7; then A12: (n !) / ((k !) * ((n -' k) !)) = ((n !) * ((n + 1) - k)) / (((k !) * ((n -' k) !)) * ((n + 1) - k)) by XCMPLX_1:91 .= ((n !) * ((n + 1) - k)) / ((k !) * (((n + 1) -' k) !)) by A10, A9, Th13 ; assume A13: k <> 0 ; ::_thesis: (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k then A14: 0 + 1 <= k by INT_1:7; then A15: (k -' 1) + 1 = (k - 1) + 1 by XREAL_1:233 .= k ; k < k + 1 by XREAL_1:29; then k - 1 <= (k + 1) - 1 by XREAL_1:9; then k - 1 <= n by A10, XXREAL_0:2; then A16: k -' 1 <= n by A14, XREAL_1:233; then A17: n -' (k -' 1) = n - (k -' 1) by XREAL_1:233 .= n - (k - 1) by A14, XREAL_1:233 .= (n + 1) - k .= (n + 1) -' k by A7, XREAL_1:233 ; A18: n -' (k -' 1) = n - (k -' 1) by A16, XREAL_1:233 .= n - (k - 1) by A14, XREAL_1:233 .= (n + 1) - k .= (n + 1) -' k by A7, XREAL_1:233 ; (((k -' 1) !) * ((n -' (k -' 1)) !)) * k = (k * ((k -' 1) !)) * ((n -' (k -' 1)) !) .= (k !) * (((n + 1) -' k) !) by A13, A18, Th13 ; then A19: (n !) / (((k -' 1) !) * ((n -' (k -' 1)) !)) = ((n !) * k) / ((k !) * (((n + 1) -' k) !)) by A13, XCMPLX_1:91; (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (((Expan (n,z,w)) * w) . k) + ((Shift ((Expan (n,z,w)) * z)) . k) by NORMSP_1:def_2 .= (((Expan (n,z,w)) . k) * w) + ((Shift ((Expan (n,z,w)) * z)) . k) by LOPBAN_3:def_6 .= (((Expan (n,z,w)) . k) * w) + (((Expan (n,z,w)) * z) . (k -' 1)) by A13, Th15 .= (((Expan (n,z,w)) . k) * w) + (((Expan (n,z,w)) . (k -' 1)) * z) by LOPBAN_3:def_6 .= (((((Coef n) . k) * (z #N k)) * (w #N (n -' k))) * w) + (((Expan (n,z,w)) . (k -' 1)) * z) by A10, Def6 .= (((((Coef n) . k) * (z #N k)) * (w #N (n -' k))) * w) + (((((Coef n) . (k -' 1)) * (z #N (k -' 1))) * (w #N (n -' (k -' 1)))) * z) by A16, Def6 .= ((((Coef n) . k) * (z #N k)) * ((w #N (n -' k)) * w)) + (((((Coef n) . (k -' 1)) * (z #N (k -' 1))) * (w #N (n -' (k -' 1)))) * z) by LOPBAN_3:38 .= ((((Coef n) . k) * (z #N k)) * (w #N ((n -' k) + 1))) + (((((Coef n) . (k -' 1)) * (z #N (k -' 1))) * (w #N (n -' (k -' 1)))) * z) by Lm1 .= ((((Coef n) . k) * (z #N k)) * (w #N ((n -' k) + 1))) + ((((Coef n) . (k -' 1)) * (z #N (k -' 1))) * ((w #N (n -' (k -' 1))) * z)) by LOPBAN_3:38 .= ((((Coef n) . k) * (z #N k)) * (w #N ((n -' k) + 1))) + ((((Coef n) . (k -' 1)) * (z #N (k -' 1))) * (z * (w #N (n -' (k -' 1))))) by A1, Lm2 .= ((((Coef n) . k) * (z #N k)) * (w #N ((n -' k) + 1))) + (((((Coef n) . (k -' 1)) * (z #N (k -' 1))) * z) * (w #N (n -' (k -' 1)))) by LOPBAN_3:38 .= ((((Coef n) . k) * (z #N k)) * (w #N ((n -' k) + 1))) + ((((Coef n) . (k -' 1)) * ((z #N (k -' 1)) * z)) * (w #N (n -' (k -' 1)))) by LOPBAN_3:38 .= ((((Coef n) . k) * (z #N k)) * (w #N ((n -' k) + 1))) + ((((Coef n) . (k -' 1)) * (z #N ((k -' 1) + 1))) * (w #N (n -' (k -' 1)))) by Lm1 ; then A20: (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (((Coef n) . k) * ((z #N k) * (w #N ((n + 1) -' k)))) + ((((Coef n) . (k -' 1)) * (z #N k)) * (w #N ((n + 1) -' k))) by A11, A17, A15, LOPBAN_3:38 .= (((Coef n) . k) * ((z #N k) * (w #N ((n + 1) -' k)))) + (((Coef n) . (k -' 1)) * ((z #N k) * (w #N ((n + 1) -' k)))) by LOPBAN_3:38 .= (((Coef n) . k) + ((Coef n) . (k -' 1))) * ((z #N k) * (w #N ((n + 1) -' k))) by LOPBAN_3:38 ; ((Coef n) . k) + ((Coef n) . (k -' 1)) = ((n !) / ((k !) * ((n -' k) !))) + ((Coef n) . (k -' 1)) by A10, Def3 .= ((n !) / ((k !) * ((n -' k) !))) + ((n !) / (((k -' 1) !) * ((n -' (k -' 1)) !))) by A16, Def3 ; then ((Coef n) . k) + ((Coef n) . (k -' 1)) = (((n !) * ((n + 1) - k)) + ((n !) * k)) / ((k !) * (((n + 1) -' k) !)) by A12, A19, XCMPLX_1:62 .= ((n !) * (((n + 1) - k) + k)) / ((k !) * (((n + 1) -' k) !)) .= ((n + 1) !) / ((k !) * (((n + 1) -' k) !)) by NEWTON:15 .= (Coef (n + 1)) . k by A7, Def3 ; then (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (((Coef (n + 1)) . k) * (z #N k)) * (w #N ((n + 1) -' k)) by A20, LOPBAN_3:38 .= (Expan ((n + 1),z,w)) . k by A7, Def6 ; hence (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k ; ::_thesis: verum end; now__::_thesis:_(_k_=_0_implies_(((Expan_(n,z,w))_*_w)_+_(Shift_((Expan_(n,z,w))_*_z)))_._k_=_(Expan_((n_+_1),z,w))_._k_) A21: (n + 1) ! <> 0 by NEWTON:17; A22: (n + 1) -' 0 = (n + 1) - 0 by XREAL_1:233; then A23: (Coef (n + 1)) . 0 = ((n + 1) !) / ((0 !) * ((n + 1) !)) by Def3 .= 1 by A21, NEWTON:12, XCMPLX_1:60 ; A24: n ! <> 0 by NEWTON:17; A25: n -' 0 = n - 0 by XREAL_1:233; then A26: (Coef n) . 0 = (n !) / ((0 !) * (n !)) by Def3 .= 1 by A24, NEWTON:12, XCMPLX_1:60 ; assume A27: k = 0 ; ::_thesis: (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k then (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (((Expan (n,z,w)) * w) . 0) + ((Shift ((Expan (n,z,w)) * z)) . 0) by NORMSP_1:def_2 .= (((Expan (n,z,w)) . 0) * w) + ((Shift ((Expan (n,z,w)) * z)) . 0) by LOPBAN_3:def_6 .= (((Expan (n,z,w)) . 0) * w) + (0. X) by Def5 .= ((Expan (n,z,w)) . 0) * w by LOPBAN_3:38 .= ((((Coef n) . 0) * (z #N 0)) * (w #N (n -' 0))) * w by Def6 .= (((Coef n) . 0) * (z #N 0)) * ((w #N (n -' 0)) * w) by LOPBAN_3:38 .= (((Coef (n + 1)) . 0) * (z #N 0)) * (w #N ((n + 1) -' 0)) by A25, A22, A26, A23, Lm1 .= (Expan ((n + 1),z,w)) . k by A27, Def6 ; hence (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k ; ::_thesis: verum end; hence (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k by A8; ::_thesis: verum end; A28: now__::_thesis:_(_k_=_n_+_1_implies_(((Expan_(n,z,w))_*_w)_+_(Shift_((Expan_(n,z,w))_*_z)))_._k_=_(Expan_((n_+_1),z,w))_._k_) A29: (n + 1) ! <> 0 by NEWTON:17; A30: (n + 1) -' (n + 1) = (n + 1) - (n + 1) by XREAL_1:233 .= 0 ; then A31: (Coef (n + 1)) . (n + 1) = ((n + 1) !) / (((n + 1) !) * (0 !)) by Def3 .= 1 by A29, NEWTON:12, XCMPLX_1:60 ; A32: n ! <> 0 by NEWTON:17; A33: n -' n = n - n by XREAL_1:233 .= 0 ; then A34: (Coef n) . n = (n !) / ((n !) * (0 !)) by Def3 .= 1 by A32, NEWTON:12, XCMPLX_1:60 ; A35: n < n + 1 by XREAL_1:29; assume A36: k = n + 1 ; ::_thesis: (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k then (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (((Expan (n,z,w)) * w) . (n + 1)) + ((Shift ((Expan (n,z,w)) * z)) . (n + 1)) by NORMSP_1:def_2 .= (((Expan (n,z,w)) . (n + 1)) * w) + ((Shift ((Expan (n,z,w)) * z)) . (n + 1)) by LOPBAN_3:def_6 .= ((0. X) * w) + ((Shift ((Expan (n,z,w)) * z)) . (n + 1)) by A35, Def6 .= (0. X) + ((Shift ((Expan (n,z,w)) * z)) . (n + 1)) by LOPBAN_3:38 .= (Shift ((Expan (n,z,w)) * z)) . (n + 1) by LOPBAN_3:38 .= ((Expan (n,z,w)) * z) . n by Def5 .= ((Expan (n,z,w)) . n) * z by LOPBAN_3:def_6 .= ((((Coef n) . n) * (z #N n)) * (w #N (n -' n))) * z by Def6 .= (((Coef n) . n) * (z #N n)) * ((w #N (n -' n)) * z) by LOPBAN_3:38 .= (((Coef n) . n) * (z #N n)) * (z * (w #N (n -' n))) by A1, Lm2 .= ((((Coef n) . n) * (z #N n)) * z) * (w #N (n -' n)) by LOPBAN_3:38 .= (((Coef n) . n) * ((z #N n) * z)) * (w #N (n -' n)) by LOPBAN_3:38 .= (((Coef (n + 1)) . (n + 1)) * (z #N (n + 1))) * (w #N (n -' n)) by A34, A31, Lm1 .= (Expan ((n + 1),z,w)) . k by A36, A33, A30, Def6 ; hence (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k ; ::_thesis: verum end; assume k <= n + 1 ; ::_thesis: (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k hence (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k by A28, A6, XXREAL_0:1; ::_thesis: verum end; now__::_thesis:_(_n_+_1_<_k_implies_(((Expan_(n,z,w))_*_w)_+_(Shift_((Expan_(n,z,w))_*_z)))_._k_=_(Expan_((n_+_1),z,w))_._k_) assume A37: n + 1 < k ; ::_thesis: (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k then A38: (n + 1) - 1 < k - 1 by XREAL_1:9; then A39: n + 0 < (k - 1) + 1 by XREAL_1:8; 0 + 1 <= n + 1 by XREAL_1:6; then A40: k - 1 = k -' 1 by A37, XREAL_1:233, XXREAL_0:2; (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (((Expan (n,z,w)) * w) . k) + ((Shift ((Expan (n,z,w)) * z)) . k) by NORMSP_1:def_2 .= (((Expan (n,z,w)) . k) * w) + ((Shift ((Expan (n,z,w)) * z)) . k) by LOPBAN_3:def_6 .= (((Expan (n,z,w)) . k) * w) + (((Expan (n,z,w)) * z) . (k -' 1)) by A39, Th15 .= (((Expan (n,z,w)) . k) * w) + (((Expan (n,z,w)) . (k -' 1)) * z) by LOPBAN_3:def_6 .= ((0. X) * w) + (((Expan (n,z,w)) . (k -' 1)) * z) by A39, Def6 .= (0. X) + (((Expan (n,z,w)) . (k -' 1)) * z) by LOPBAN_3:38 .= (0. X) + ((0. X) * z) by A38, A40, Def6 .= (0. X) + (0. X) by LOPBAN_3:38 .= 0. X by LOPBAN_3:38 ; hence (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k by A37, Def6; ::_thesis: verum end; hence (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k by A5; ::_thesis: verum end; then A41: ((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z)) = Expan ((n + 1),z,w) by FUNCT_2:63; A42: n < n + 1 by XREAL_1:29; (Partial_Sums ((Expan (n,z,w)) * w)) . (n + 1) = ((Partial_Sums ((Expan (n,z,w)) * w)) . n) + (((Expan (n,z,w)) * w) . (n + 1)) by BHSP_4:def_1 .= ((Partial_Sums ((Expan (n,z,w)) * w)) . n) + (((Expan (n,z,w)) . (n + 1)) * w) by LOPBAN_3:def_6 ; then A43: (Partial_Sums ((Expan (n,z,w)) * w)) . (n + 1) = ((Partial_Sums ((Expan (n,z,w)) * w)) . n) + ((0. X) * w) by A42, Def6 .= ((Partial_Sums ((Expan (n,z,w)) * w)) . n) + (0. X) by LOPBAN_3:38 .= (Partial_Sums ((Expan (n,z,w)) * w)) . n by LOPBAN_3:38 ; (Partial_Sums ((Expan (n,z,w)) * z)) . (n + 1) = ((Partial_Sums ((Expan (n,z,w)) * z)) . n) + (((Expan (n,z,w)) * z) . (n + 1)) by BHSP_4:def_1 .= ((Partial_Sums ((Expan (n,z,w)) * z)) . n) + (((Expan (n,z,w)) . (n + 1)) * z) by LOPBAN_3:def_6 ; then A44: (Partial_Sums ((Expan (n,z,w)) * z)) . (n + 1) = ((Partial_Sums ((Expan (n,z,w)) * z)) . n) + ((0. X) * z) by A4, Def6 .= ((Partial_Sums ((Expan (n,z,w)) * z)) . n) + (0. X) by LOPBAN_3:38 .= (Partial_Sums ((Expan (n,z,w)) * z)) . n by LOPBAN_3:38 ; 0 + n < n + 1 by XREAL_1:29; then A45: (Expan (n,z,w)) . (n + 1) = 0. X by Def6; (Partial_Sums ((Expan (n,z,w)) * z)) . (n + 1) = ((Partial_Sums (Shift ((Expan (n,z,w)) * z))) . (n + 1)) + (((Expan (n,z,w)) * z) . (n + 1)) by Th16; then A46: (Partial_Sums ((Expan (n,z,w)) * z)) . (n + 1) = ((Partial_Sums (Shift ((Expan (n,z,w)) * z))) . (n + 1)) + (((Expan (n,z,w)) . (n + 1)) * z) by LOPBAN_3:def_6 .= ((Partial_Sums (Shift ((Expan (n,z,w)) * z))) . (n + 1)) + (0. X) by A45, LOPBAN_3:38 .= (Partial_Sums (Shift ((Expan (n,z,w)) * z))) . (n + 1) by LOPBAN_3:38 ; now__::_thesis:_for_k_being_Element_of_NAT_holds_((Expan_(n,z,w))_*_(z_+_w))_._k_=_(((Expan_(n,z,w))_*_z)_+_((Expan_(n,z,w))_*_w))_._k let k be Element of NAT ; ::_thesis: ((Expan (n,z,w)) * (z + w)) . k = (((Expan (n,z,w)) * z) + ((Expan (n,z,w)) * w)) . k thus ((Expan (n,z,w)) * (z + w)) . k = ((Expan (n,z,w)) . k) * (z + w) by LOPBAN_3:def_6 .= (((Expan (n,z,w)) . k) * z) + (((Expan (n,z,w)) . k) * w) by LOPBAN_3:38 .= (((Expan (n,z,w)) * z) . k) + (((Expan (n,z,w)) . k) * w) by LOPBAN_3:def_6 .= (((Expan (n,z,w)) * z) . k) + (((Expan (n,z,w)) * w) . k) by LOPBAN_3:def_6 .= (((Expan (n,z,w)) * z) + ((Expan (n,z,w)) * w)) . k by NORMSP_1:def_2 ; ::_thesis: verum end; then A47: (Expan (n,z,w)) * (z + w) = ((Expan (n,z,w)) * z) + ((Expan (n,z,w)) * w) by FUNCT_2:63; (z + w) #N (n + 1) = (((z + w) GeoSeq) . n) * (z + w) by LOPBAN_3:def_9 .= ((Partial_Sums (Expan (n,z,w))) * (z + w)) . n by A3, LOPBAN_3:def_6 .= (Partial_Sums ((Expan (n,z,w)) * (z + w))) . n by Th9 ; then (z + w) #N (n + 1) = ((Partial_Sums ((Expan (n,z,w)) * z)) + (Partial_Sums ((Expan (n,z,w)) * w))) . n by A47, LOPBAN_3:15 .= ((Partial_Sums ((Expan (n,z,w)) * z)) . n) + ((Partial_Sums ((Expan (n,z,w)) * w)) . n) by NORMSP_1:def_2 ; hence (z + w) #N (n + 1) = ((Partial_Sums ((Expan (n,z,w)) * w)) + (Partial_Sums (Shift ((Expan (n,z,w)) * z)))) . (n + 1) by A44, A43, A46, NORMSP_1:def_2 .= (Partial_Sums (Expan ((n + 1),z,w))) . (n + 1) by A41, LOPBAN_3:15 ; ::_thesis: verum end; A48: 0 -' 0 = 0 - 0 by XREAL_0:def_2 .= 0 ; (Partial_Sums (Expan (0,z,w))) . 0 = (Expan (0,z,w)) . 0 by BHSP_4:def_1 .= (((Coef 0) . 0) * (z #N 0)) * (w #N 0) by A48, Def6 .= ((1 / (1 * 1)) * (z #N 0)) * (w #N 0) by A48, Def3, NEWTON:12 .= ((z GeoSeq) . 0) * (w #N 0) by RLVECT_1:def_8 .= (1. X) * ((w GeoSeq) . 0) by LOPBAN_3:def_9 .= (1. X) * (1. X) by LOPBAN_3:def_9 .= 1. X by LOPBAN_3:38 ; then A49: S1[ 0 ] by LOPBAN_3:def_9; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A49, A2); hence (z + w) #N n = (Partial_Sums (Expan (n,z,w))) . n ; ::_thesis: verum end; theorem Th18: :: LOPBAN_4:18 for X being Banach_Algebra for z, w being Element of X for n being Element of NAT holds Expan_e (n,z,w) = (1 / (n !)) * (Expan (n,z,w)) proof let X be Banach_Algebra; ::_thesis: for z, w being Element of X for n being Element of NAT holds Expan_e (n,z,w) = (1 / (n !)) * (Expan (n,z,w)) let z, w be Element of X; ::_thesis: for n being Element of NAT holds Expan_e (n,z,w) = (1 / (n !)) * (Expan (n,z,w)) let n be Element of NAT ; ::_thesis: Expan_e (n,z,w) = (1 / (n !)) * (Expan (n,z,w)) now__::_thesis:_for_k_being_Element_of_NAT_holds_(Expan_e_(n,z,w))_._k_=_((1_/_(n_!))_*_(Expan_(n,z,w)))_._k let k be Element of NAT ; ::_thesis: (Expan_e (n,z,w)) . k = ((1 / (n !)) * (Expan (n,z,w))) . k A1: now__::_thesis:_(_k_<=_n_implies_(_(Expan_e_(n,z,w))_._k_=_((1_/_((k_!)_*_((n_-'_k)_!)))_*_(z_#N_k))_*_(w_#N_(n_-'_k))_&_(Expan_e_(n,z,w))_._k_=_((1_/_(n_!))_*_(Expan_(n,z,w)))_._k_)_) n ! <> 0 by NEWTON:17; then A2: 1 / ((k !) * ((n -' k) !)) = (((n !) * 1) / (n !)) / ((k !) * ((n -' k) !)) by XCMPLX_1:60 .= ((1 / (n !)) * (n !)) / ((k !) * ((n -' k) !)) by XCMPLX_1:74 ; assume A3: k <= n ; ::_thesis: ( (Expan_e (n,z,w)) . k = ((1 / ((k !) * ((n -' k) !))) * (z #N k)) * (w #N (n -' k)) & (Expan_e (n,z,w)) . k = ((1 / (n !)) * (Expan (n,z,w))) . k ) hence (Expan_e (n,z,w)) . k = (((Coef_e n) . k) * (z #N k)) * (w #N (n -' k)) by Def7 .= ((1 / ((k !) * ((n -' k) !))) * (z #N k)) * (w #N (n -' k)) by A3, Def4 ; ::_thesis: (Expan_e (n,z,w)) . k = ((1 / (n !)) * (Expan (n,z,w))) . k hence (Expan_e (n,z,w)) . k = (((1 / (n !)) * (n !)) / ((k !) * ((n -' k) !))) * ((z #N k) * (w #N (n -' k))) by A2, LOPBAN_3:38 .= ((1 / (n !)) * ((n !) / ((k !) * ((n -' k) !)))) * ((z #N k) * (w #N (n -' k))) by XCMPLX_1:74 .= (1 / (n !)) * (((n !) / ((k !) * ((n -' k) !))) * ((z #N k) * (w #N (n -' k)))) by LOPBAN_3:38 .= (1 / (n !)) * ((((n !) / ((k !) * ((n -' k) !))) * (z #N k)) * (w #N (n -' k))) by LOPBAN_3:38 .= (1 / (n !)) * ((((Coef n) . k) * (z #N k)) * (w #N (n -' k))) by A3, Def3 .= (1 / (n !)) * ((Expan (n,z,w)) . k) by A3, Def6 .= ((1 / (n !)) * (Expan (n,z,w))) . k by NORMSP_1:def_5 ; ::_thesis: verum end; now__::_thesis:_(_n_<_k_implies_(Expan_e_(n,z,w))_._k_=_((1_/_(n_!))_*_(Expan_(n,z,w)))_._k_) assume A4: n < k ; ::_thesis: (Expan_e (n,z,w)) . k = ((1 / (n !)) * (Expan (n,z,w))) . k hence (Expan_e (n,z,w)) . k = 0. X by Def7 .= (1 / (n !)) * (0. X) by LOPBAN_3:38 .= (1 / (n !)) * ((Expan (n,z,w)) . k) by A4, Def6 .= ((1 / (n !)) * (Expan (n,z,w))) . k by NORMSP_1:def_5 ; ::_thesis: verum end; hence (Expan_e (n,z,w)) . k = ((1 / (n !)) * (Expan (n,z,w))) . k by A1; ::_thesis: verum end; hence Expan_e (n,z,w) = (1 / (n !)) * (Expan (n,z,w)) by FUNCT_2:63; ::_thesis: verum end; theorem Th19: :: LOPBAN_4:19 for X being Banach_Algebra for n being Element of NAT for z, w being Element of X st z,w are_commutative holds (1 / (n !)) * ((z + w) #N n) = (Partial_Sums (Expan_e (n,z,w))) . n proof let X be Banach_Algebra; ::_thesis: for n being Element of NAT for z, w being Element of X st z,w are_commutative holds (1 / (n !)) * ((z + w) #N n) = (Partial_Sums (Expan_e (n,z,w))) . n let n be Element of NAT ; ::_thesis: for z, w being Element of X st z,w are_commutative holds (1 / (n !)) * ((z + w) #N n) = (Partial_Sums (Expan_e (n,z,w))) . n let z, w be Element of X; ::_thesis: ( z,w are_commutative implies (1 / (n !)) * ((z + w) #N n) = (Partial_Sums (Expan_e (n,z,w))) . n ) assume z,w are_commutative ; ::_thesis: (1 / (n !)) * ((z + w) #N n) = (Partial_Sums (Expan_e (n,z,w))) . n hence (1 / (n !)) * ((z + w) #N n) = (1 / (n !)) * ((Partial_Sums (Expan (n,z,w))) . n) by Th17 .= ((1 / (n !)) * (Partial_Sums (Expan (n,z,w)))) . n by NORMSP_1:def_5 .= (Partial_Sums ((1 / (n !)) * (Expan (n,z,w)))) . n by LOPBAN_3:19 .= (Partial_Sums (Expan_e (n,z,w))) . n by Th18 ; ::_thesis: verum end; theorem Th20: :: LOPBAN_4:20 for X being Banach_Algebra holds ( (0. X) rExpSeq is norm_summable & Sum ((0. X) rExpSeq) = 1. X ) proof let X be Banach_Algebra; ::_thesis: ( (0. X) rExpSeq is norm_summable & Sum ((0. X) rExpSeq) = 1. X ) defpred S1[ set ] means (Partial_Sums ||.((0. X) rExpSeq).||) . $1 = 1; A1: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A2: (Partial_Sums ||.((0. X) rExpSeq).||) . n = 1 ; ::_thesis: S1[n + 1] A3: n in NAT by ORDINAL1:def_12; hence (Partial_Sums ||.((0. X) rExpSeq).||) . (n + 1) = 1 + (||.((0. X) rExpSeq).|| . (n + 1)) by A2, SERIES_1:def_1 .= 1 + ||.(((0. X) rExpSeq) . (n + 1)).|| by NORMSP_0:def_4 .= 1 + ||.(((1 / (n + 1)) * (0. X)) * (((0. X) rExpSeq) . n)).|| by A3, Th14 .= 1 + ||.((0. X) * (((0. X) rExpSeq) . n)).|| by LOPBAN_3:38 .= 1 + ||.(0. X).|| by LOPBAN_3:38 .= 1 + 0 by LOPBAN_3:38 .= 1 ; ::_thesis: verum end; (Partial_Sums ||.((0. X) rExpSeq).||) . 0 = ||.((0. X) rExpSeq).|| . 0 by SERIES_1:def_1 .= ||.(((0. X) rExpSeq) . 0).|| by NORMSP_0:def_4 .= ||.(1. X).|| by Th14 .= 1 by LOPBAN_3:38 ; then A4: S1[ 0 ] ; A5: for n being Nat holds S1[n] from NAT_1:sch_2(A4, A1); Partial_Sums ||.((0. X) rExpSeq).|| is constant proof take 1 ; :: according to VALUED_0:def_20 ::_thesis: for b1 being set holds (Partial_Sums ||.((0. X) rExpSeq).||) . b1 = 1 let n be Nat; ::_thesis: (Partial_Sums ||.((0. X) rExpSeq).||) . n = 1 thus (Partial_Sums ||.((0. X) rExpSeq).||) . n = 1 by A5; ::_thesis: verum end; then A6: ||.((0. X) rExpSeq).|| is summable by SERIES_1:def_2; defpred S2[ set ] means (Partial_Sums ((0. X) rExpSeq)) . $1 = 1. X; A7: for n being Element of NAT st S2[n] holds S2[n + 1] proof let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] ) assume (Partial_Sums ((0. X) rExpSeq)) . n = 1. X ; ::_thesis: S2[n + 1] hence (Partial_Sums ((0. X) rExpSeq)) . (n + 1) = (1. X) + (((0. X) rExpSeq) . (n + 1)) by BHSP_4:def_1 .= (1. X) + (((1 / (n + 1)) * (0. X)) * (((0. X) rExpSeq) . n)) by Th14 .= (1. X) + ((0. X) * (((0. X) rExpSeq) . n)) by LOPBAN_3:38 .= (1. X) + (0. X) by LOPBAN_3:38 .= 1. X by LOPBAN_3:38 ; ::_thesis: verum end; (Partial_Sums ((0. X) rExpSeq)) . 0 = ((0. X) rExpSeq) . 0 by BHSP_4:def_1 .= 1. X by Th14 ; then A8: S2[ 0 ] ; for n being Element of NAT holds S2[n] from NAT_1:sch_1(A8, A7); hence ( (0. X) rExpSeq is norm_summable & Sum ((0. X) rExpSeq) = 1. X ) by A6, Th2, LOPBAN_3:def_3; ::_thesis: verum end; registration let X be Banach_Algebra; let z be Element of X; clusterz rExpSeq -> norm_summable ; coherence z rExpSeq is norm_summable proof ex m being Element of NAT st for n being Element of NAT st m <= n holds ||.((z rExpSeq) . n).|| <= (||.z.|| rExpSeq) . n proof take 0 ; ::_thesis: for n being Element of NAT st 0 <= n holds ||.((z rExpSeq) . n).|| <= (||.z.|| rExpSeq) . n thus for n being Element of NAT st 0 <= n holds ||.((z rExpSeq) . n).|| <= (||.z.|| rExpSeq) . n by Th14; ::_thesis: verum end; hence z rExpSeq is norm_summable by LOPBAN_3:27, SIN_COS:45; ::_thesis: verum end; end; theorem Th21: :: LOPBAN_4:21 for X being Banach_Algebra for z, w being Element of X holds ( (z rExpSeq) . 0 = 1. X & (Expan (0,z,w)) . 0 = 1. X ) proof let X be Banach_Algebra; ::_thesis: for z, w being Element of X holds ( (z rExpSeq) . 0 = 1. X & (Expan (0,z,w)) . 0 = 1. X ) let z, w be Element of X; ::_thesis: ( (z rExpSeq) . 0 = 1. X & (Expan (0,z,w)) . 0 = 1. X ) thus (z rExpSeq) . 0 = (1 / (0 !)) * (z #N 0) by Def2 .= (1 / 1) * (1. X) by LOPBAN_3:def_9, NEWTON:12 .= 1. X by LOPBAN_3:38 ; ::_thesis: (Expan (0,z,w)) . 0 = 1. X A1: 0 -' 0 = 0 by XREAL_1:232; hence (Expan (0,z,w)) . 0 = (((Coef 0) . 0) * (z #N 0)) * (w #N 0) by Def6 .= ((1 / (1 * 1)) * (z #N 0)) * (w #N 0) by A1, Def3, NEWTON:12 .= ((z GeoSeq) . 0) * (w #N 0) by LOPBAN_3:38 .= (1. X) * ((w GeoSeq) . 0) by LOPBAN_3:def_9 .= (1. X) * (1. X) by LOPBAN_3:def_9 .= 1. X by LOPBAN_3:38 ; ::_thesis: verum end; theorem Th22: :: LOPBAN_4:22 for X being Banach_Algebra for z, w being Element of X for l, k being Element of NAT st l <= k holds (Alfa ((k + 1),z,w)) . l = ((Alfa (k,z,w)) . l) + ((Expan_e ((k + 1),z,w)) . l) proof let X be Banach_Algebra; ::_thesis: for z, w being Element of X for l, k being Element of NAT st l <= k holds (Alfa ((k + 1),z,w)) . l = ((Alfa (k,z,w)) . l) + ((Expan_e ((k + 1),z,w)) . l) let z, w be Element of X; ::_thesis: for l, k being Element of NAT st l <= k holds (Alfa ((k + 1),z,w)) . l = ((Alfa (k,z,w)) . l) + ((Expan_e ((k + 1),z,w)) . l) let l, k be Element of NAT ; ::_thesis: ( l <= k implies (Alfa ((k + 1),z,w)) . l = ((Alfa (k,z,w)) . l) + ((Expan_e ((k + 1),z,w)) . l) ) assume A1: l <= k ; ::_thesis: (Alfa ((k + 1),z,w)) . l = ((Alfa (k,z,w)) . l) + ((Expan_e ((k + 1),z,w)) . l) A2: k < k + 1 by XREAL_1:29; then A3: l <= k + 1 by A1, XXREAL_0:2; A4: ((z rExpSeq) . l) * ((w rExpSeq) . ((k + 1) -' l)) = ((1 / (l !)) * (z #N l)) * ((w rExpSeq) . ((k + 1) -' l)) by Def2 .= ((1 / (l !)) * (z #N l)) * ((1 / (((k + 1) -' l) !)) * (w #N ((k + 1) -' l))) by Def2 .= ((1 / (l !)) * (1 / (((k + 1) -' l) !))) * ((z #N l) * (w #N ((k + 1) -' l))) by LOPBAN_3:38 .= (1 / ((l !) * (((k + 1) -' l) !))) * ((z #N l) * (w #N ((k + 1) -' l))) by XCMPLX_1:102 .= ((Coef_e (k + 1)) . l) * ((z #N l) * (w #N ((k + 1) -' l))) by A3, Def4 .= (((Coef_e (k + 1)) . l) * (z #N l)) * (w #N ((k + 1) -' l)) by LOPBAN_3:38 .= (Expan_e ((k + 1),z,w)) . l by A3, Def7 ; (k + 1) -' l = (k + 1) - l by A1, A2, XREAL_1:233, XXREAL_0:2; then A5: (k + 1) -' l = (k - l) + 1 .= (k -' l) + 1 by A1, XREAL_1:233 ; then (Alfa ((k + 1),z,w)) . l = ((z rExpSeq) . l) * ((Partial_Sums (w rExpSeq)) . ((k -' l) + 1)) by A3, Def8 .= ((z rExpSeq) . l) * (((Partial_Sums (w rExpSeq)) . (k -' l)) + ((w rExpSeq) . ((k + 1) -' l))) by A5, BHSP_4:def_1 .= (((z rExpSeq) . l) * ((Partial_Sums (w rExpSeq)) . (k -' l))) + (((z rExpSeq) . l) * ((w rExpSeq) . ((k + 1) -' l))) by LOPBAN_3:38 .= ((Alfa (k,z,w)) . l) + (((z rExpSeq) . l) * ((w rExpSeq) . ((k + 1) -' l))) by A1, Def8 ; hence (Alfa ((k + 1),z,w)) . l = ((Alfa (k,z,w)) . l) + ((Expan_e ((k + 1),z,w)) . l) by A4; ::_thesis: verum end; theorem Th23: :: LOPBAN_4:23 for X being Banach_Algebra for z, w being Element of X for k being Element of NAT holds (Partial_Sums (Alfa ((k + 1),z,w))) . k = ((Partial_Sums (Alfa (k,z,w))) . k) + ((Partial_Sums (Expan_e ((k + 1),z,w))) . k) proof let X be Banach_Algebra; ::_thesis: for z, w being Element of X for k being Element of NAT holds (Partial_Sums (Alfa ((k + 1),z,w))) . k = ((Partial_Sums (Alfa (k,z,w))) . k) + ((Partial_Sums (Expan_e ((k + 1),z,w))) . k) let z, w be Element of X; ::_thesis: for k being Element of NAT holds (Partial_Sums (Alfa ((k + 1),z,w))) . k = ((Partial_Sums (Alfa (k,z,w))) . k) + ((Partial_Sums (Expan_e ((k + 1),z,w))) . k) let k be Element of NAT ; ::_thesis: (Partial_Sums (Alfa ((k + 1),z,w))) . k = ((Partial_Sums (Alfa (k,z,w))) . k) + ((Partial_Sums (Expan_e ((k + 1),z,w))) . k) now__::_thesis:_for_l_being_Element_of_NAT_st_l_<=_k_holds_ (Alfa_((k_+_1),z,w))_._l_=_((Alfa_(k,z,w))_+_(Expan_e_((k_+_1),z,w)))_._l let l be Element of NAT ; ::_thesis: ( l <= k implies (Alfa ((k + 1),z,w)) . l = ((Alfa (k,z,w)) + (Expan_e ((k + 1),z,w))) . l ) assume l <= k ; ::_thesis: (Alfa ((k + 1),z,w)) . l = ((Alfa (k,z,w)) + (Expan_e ((k + 1),z,w))) . l hence (Alfa ((k + 1),z,w)) . l = ((Alfa (k,z,w)) . l) + ((Expan_e ((k + 1),z,w)) . l) by Th22 .= ((Alfa (k,z,w)) + (Expan_e ((k + 1),z,w))) . l by NORMSP_1:def_2 ; ::_thesis: verum end; hence (Partial_Sums (Alfa ((k + 1),z,w))) . k = (Partial_Sums ((Alfa (k,z,w)) + (Expan_e ((k + 1),z,w)))) . k by Th11 .= ((Partial_Sums (Alfa (k,z,w))) + (Partial_Sums (Expan_e ((k + 1),z,w)))) . k by LOPBAN_3:15 .= ((Partial_Sums (Alfa (k,z,w))) . k) + ((Partial_Sums (Expan_e ((k + 1),z,w))) . k) by NORMSP_1:def_2 ; ::_thesis: verum end; theorem Th24: :: LOPBAN_4:24 for X being Banach_Algebra for z, w being Element of X for k being Element of NAT holds (z rExpSeq) . k = (Expan_e (k,z,w)) . k proof let X be Banach_Algebra; ::_thesis: for z, w being Element of X for k being Element of NAT holds (z rExpSeq) . k = (Expan_e (k,z,w)) . k let z, w be Element of X; ::_thesis: for k being Element of NAT holds (z rExpSeq) . k = (Expan_e (k,z,w)) . k let k be Element of NAT ; ::_thesis: (z rExpSeq) . k = (Expan_e (k,z,w)) . k A1: 0 = k - k ; then A2: (k -' k) ! = 1 by NEWTON:12, XREAL_1:233; k -' k = 0 by A1, XREAL_1:233; hence (Expan_e (k,z,w)) . k = (((Coef_e k) . k) * (z #N k)) * (w #N 0) by Def7 .= (((Coef_e k) . k) * (z #N k)) * (1. X) by LOPBAN_3:39 .= ((Coef_e k) . k) * (z #N k) by LOPBAN_3:38 .= (1 / ((k !) * 1)) * (z #N k) by A2, Def4 .= (z rExpSeq) . k by Def2 ; ::_thesis: verum end; theorem Th25: :: LOPBAN_4:25 for X being Banach_Algebra for n being Element of NAT for z, w being Element of X st z,w are_commutative holds (Partial_Sums ((z + w) rExpSeq)) . n = (Partial_Sums (Alfa (n,z,w))) . n proof let X be Banach_Algebra; ::_thesis: for n being Element of NAT for z, w being Element of X st z,w are_commutative holds (Partial_Sums ((z + w) rExpSeq)) . n = (Partial_Sums (Alfa (n,z,w))) . n let n be Element of NAT ; ::_thesis: for z, w being Element of X st z,w are_commutative holds (Partial_Sums ((z + w) rExpSeq)) . n = (Partial_Sums (Alfa (n,z,w))) . n let z, w be Element of X; ::_thesis: ( z,w are_commutative implies (Partial_Sums ((z + w) rExpSeq)) . n = (Partial_Sums (Alfa (n,z,w))) . n ) assume A1: z,w are_commutative ; ::_thesis: (Partial_Sums ((z + w) rExpSeq)) . n = (Partial_Sums (Alfa (n,z,w))) . n defpred S1[ Element of NAT ] means (Partial_Sums ((z + w) rExpSeq)) . $1 = (Partial_Sums (Alfa ($1,z,w))) . $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: (Partial_Sums ((z + w) rExpSeq)) . k = (Partial_Sums (Alfa (k,z,w))) . k ; ::_thesis: S1[k + 1] (k + 1) -' (k + 1) = 0 by XREAL_1:232; then (Alfa ((k + 1),z,w)) . (k + 1) = ((z rExpSeq) . (k + 1)) * ((Partial_Sums (w rExpSeq)) . 0) by Def8 .= ((z rExpSeq) . (k + 1)) * ((w rExpSeq) . 0) by BHSP_4:def_1 .= ((z rExpSeq) . (k + 1)) * (1. X) by Th21 .= (z rExpSeq) . (k + 1) by LOPBAN_3:38 .= (Expan_e ((k + 1),z,w)) . (k + 1) by Th24 ; then A4: ((Partial_Sums (Expan_e ((k + 1),z,w))) . k) + ((Alfa ((k + 1),z,w)) . (k + 1)) = (Partial_Sums (Expan_e ((k + 1),z,w))) . (k + 1) by BHSP_4:def_1 .= (1 / ((k + 1) !)) * ((z + w) #N (k + 1)) by A1, Th19 ; (Partial_Sums (Alfa ((k + 1),z,w))) . (k + 1) = ((Partial_Sums (Alfa ((k + 1),z,w))) . k) + ((Alfa ((k + 1),z,w)) . (k + 1)) by BHSP_4:def_1 .= (((Partial_Sums (Alfa (k,z,w))) . k) + ((Partial_Sums (Expan_e ((k + 1),z,w))) . k)) + ((Alfa ((k + 1),z,w)) . (k + 1)) by Th23 .= ((Partial_Sums ((z + w) rExpSeq)) . k) + (((Partial_Sums (Expan_e ((k + 1),z,w))) . k) + ((Alfa ((k + 1),z,w)) . (k + 1))) by A3, LOPBAN_3:38 ; then (Partial_Sums (Alfa ((k + 1),z,w))) . (k + 1) = ((Partial_Sums ((z + w) rExpSeq)) . k) + (((z + w) rExpSeq) . (k + 1)) by A4, Def2 .= (Partial_Sums ((z + w) rExpSeq)) . (k + 1) by BHSP_4:def_1 ; hence (Partial_Sums ((z + w) rExpSeq)) . (k + 1) = (Partial_Sums (Alfa ((k + 1),z,w))) . (k + 1) ; ::_thesis: verum end; A5: (Partial_Sums ((z + w) rExpSeq)) . 0 = ((z + w) rExpSeq) . 0 by BHSP_4:def_1 .= 1. X by Th21 ; A6: 0 -' 0 = 0 by XREAL_1:232; (Partial_Sums (Alfa (0,z,w))) . 0 = (Alfa (0,z,w)) . 0 by BHSP_4:def_1 .= ((z rExpSeq) . 0) * ((Partial_Sums (w rExpSeq)) . 0) by A6, Def8 .= ((z rExpSeq) . 0) * ((w rExpSeq) . 0) by BHSP_4:def_1 .= (1. X) * ((w rExpSeq) . 0) by Th21 .= (1. X) * (1. X) by Th21 .= 1. X by LOPBAN_3:38 ; then A7: S1[ 0 ] by A5; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A7, A2); hence (Partial_Sums ((z + w) rExpSeq)) . n = (Partial_Sums (Alfa (n,z,w))) . n ; ::_thesis: verum end; theorem Th26: :: LOPBAN_4:26 for X being Banach_Algebra for k being Element of NAT for z, w being Element of X st z,w are_commutative holds (((Partial_Sums (z rExpSeq)) . k) * ((Partial_Sums (w rExpSeq)) . k)) - ((Partial_Sums ((z + w) rExpSeq)) . k) = (Partial_Sums (Conj (k,z,w))) . k proof let X be Banach_Algebra; ::_thesis: for k being Element of NAT for z, w being Element of X st z,w are_commutative holds (((Partial_Sums (z rExpSeq)) . k) * ((Partial_Sums (w rExpSeq)) . k)) - ((Partial_Sums ((z + w) rExpSeq)) . k) = (Partial_Sums (Conj (k,z,w))) . k let k be Element of NAT ; ::_thesis: for z, w being Element of X st z,w are_commutative holds (((Partial_Sums (z rExpSeq)) . k) * ((Partial_Sums (w rExpSeq)) . k)) - ((Partial_Sums ((z + w) rExpSeq)) . k) = (Partial_Sums (Conj (k,z,w))) . k let z, w be Element of X; ::_thesis: ( z,w are_commutative implies (((Partial_Sums (z rExpSeq)) . k) * ((Partial_Sums (w rExpSeq)) . k)) - ((Partial_Sums ((z + w) rExpSeq)) . k) = (Partial_Sums (Conj (k,z,w))) . k ) assume z,w are_commutative ; ::_thesis: (((Partial_Sums (z rExpSeq)) . k) * ((Partial_Sums (w rExpSeq)) . k)) - ((Partial_Sums ((z + w) rExpSeq)) . k) = (Partial_Sums (Conj (k,z,w))) . k then A1: (((Partial_Sums (z rExpSeq)) . k) * ((Partial_Sums (w rExpSeq)) . k)) - ((Partial_Sums ((z + w) rExpSeq)) . k) = (((Partial_Sums (z rExpSeq)) . k) * ((Partial_Sums (w rExpSeq)) . k)) - ((Partial_Sums (Alfa (k,z,w))) . k) by Th25 .= (((Partial_Sums (z rExpSeq)) * ((Partial_Sums (w rExpSeq)) . k)) . k) - ((Partial_Sums (Alfa (k,z,w))) . k) by LOPBAN_3:def_6 .= ((Partial_Sums ((z rExpSeq) * ((Partial_Sums (w rExpSeq)) . k))) . k) - ((Partial_Sums (Alfa (k,z,w))) . k) by Th9 .= ((Partial_Sums ((z rExpSeq) * ((Partial_Sums (w rExpSeq)) . k))) - (Partial_Sums (Alfa (k,z,w)))) . k by NORMSP_1:def_3 .= (Partial_Sums (((z rExpSeq) * ((Partial_Sums (w rExpSeq)) . k)) - (Alfa (k,z,w)))) . k by LOPBAN_3:16 ; for l being Element of NAT st l <= k holds (((z rExpSeq) * ((Partial_Sums (w rExpSeq)) . k)) - (Alfa (k,z,w))) . l = (Conj (k,z,w)) . l proof let l be Element of NAT ; ::_thesis: ( l <= k implies (((z rExpSeq) * ((Partial_Sums (w rExpSeq)) . k)) - (Alfa (k,z,w))) . l = (Conj (k,z,w)) . l ) assume A2: l <= k ; ::_thesis: (((z rExpSeq) * ((Partial_Sums (w rExpSeq)) . k)) - (Alfa (k,z,w))) . l = (Conj (k,z,w)) . l thus (((z rExpSeq) * ((Partial_Sums (w rExpSeq)) . k)) - (Alfa (k,z,w))) . l = (((z rExpSeq) * ((Partial_Sums (w rExpSeq)) . k)) . l) - ((Alfa (k,z,w)) . l) by NORMSP_1:def_3 .= (((z rExpSeq) . l) * ((Partial_Sums (w rExpSeq)) . k)) - ((Alfa (k,z,w)) . l) by LOPBAN_3:def_6 .= (((z rExpSeq) . l) * ((Partial_Sums (w rExpSeq)) . k)) - (((z rExpSeq) . l) * ((Partial_Sums (w rExpSeq)) . (k -' l))) by A2, Def8 .= ((z rExpSeq) . l) * (((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))) by LOPBAN_3:38 .= (Conj (k,z,w)) . l by A2, Def9 ; ::_thesis: verum end; hence (((Partial_Sums (z rExpSeq)) . k) * ((Partial_Sums (w rExpSeq)) . k)) - ((Partial_Sums ((z + w) rExpSeq)) . k) = (Partial_Sums (Conj (k,z,w))) . k by A1, Th11; ::_thesis: verum end; theorem Th27: :: LOPBAN_4:27 for X being Banach_Algebra for z being Element of X for n being Element of NAT holds 0 <= (||.z.|| rExpSeq) . n proof let X be Banach_Algebra; ::_thesis: for z being Element of X for n being Element of NAT holds 0 <= (||.z.|| rExpSeq) . n let z be Element of X; ::_thesis: for n being Element of NAT holds 0 <= (||.z.|| rExpSeq) . n let n be Element of NAT ; ::_thesis: 0 <= (||.z.|| rExpSeq) . n defpred S1[ Element of NAT ] means 0 <= ||.z.|| |^ $1; A1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: S1[k] ; ::_thesis: S1[k + 1] A3: 0 <= ||.z.|| by NORMSP_1:4; ||.z.|| |^ (k + 1) = (||.z.|| |^ k) * ||.z.|| by NEWTON:6; hence S1[k + 1] by A2, A3; ::_thesis: verum end; A4: S1[ 0 ] by NEWTON:4; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A4, A1); then A5: 0 <= ||.z.|| |^ n ; A6: (||.z.|| |^ n) / (n !) = (||.z.|| |^ n) * ((n !) ") by XCMPLX_0:def_9; n ! > 0 by NEWTON:17; hence 0 <= (||.z.|| rExpSeq) . n by A5, A6, SIN_COS:def_5; ::_thesis: verum end; theorem Th28: :: LOPBAN_4:28 for X being Banach_Algebra for z being Element of X for k being Element of NAT holds ( ||.((Partial_Sums (z rExpSeq)) . k).|| <= (Partial_Sums (||.z.|| rExpSeq)) . k & (Partial_Sums (||.z.|| rExpSeq)) . k <= Sum (||.z.|| rExpSeq) & ||.((Partial_Sums (z rExpSeq)) . k).|| <= Sum (||.z.|| rExpSeq) ) proof let X be Banach_Algebra; ::_thesis: for z being Element of X for k being Element of NAT holds ( ||.((Partial_Sums (z rExpSeq)) . k).|| <= (Partial_Sums (||.z.|| rExpSeq)) . k & (Partial_Sums (||.z.|| rExpSeq)) . k <= Sum (||.z.|| rExpSeq) & ||.((Partial_Sums (z rExpSeq)) . k).|| <= Sum (||.z.|| rExpSeq) ) let z be Element of X; ::_thesis: for k being Element of NAT holds ( ||.((Partial_Sums (z rExpSeq)) . k).|| <= (Partial_Sums (||.z.|| rExpSeq)) . k & (Partial_Sums (||.z.|| rExpSeq)) . k <= Sum (||.z.|| rExpSeq) & ||.((Partial_Sums (z rExpSeq)) . k).|| <= Sum (||.z.|| rExpSeq) ) let k be Element of NAT ; ::_thesis: ( ||.((Partial_Sums (z rExpSeq)) . k).|| <= (Partial_Sums (||.z.|| rExpSeq)) . k & (Partial_Sums (||.z.|| rExpSeq)) . k <= Sum (||.z.|| rExpSeq) & ||.((Partial_Sums (z rExpSeq)) . k).|| <= Sum (||.z.|| rExpSeq) ) defpred S1[ Element of NAT ] means ||.((Partial_Sums (z rExpSeq)) . $1).|| <= (Partial_Sums (||.z.|| rExpSeq)) . $1; A1: (Partial_Sums (||.z.|| rExpSeq)) . 0 = (||.z.|| rExpSeq) . 0 by SERIES_1:def_1 .= (||.z.|| |^ 0) / (0 !) by SIN_COS:def_5 .= 1 by NEWTON:4, NEWTON:12 ; 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 ||.((Partial_Sums (z rExpSeq)) . k).|| <= (Partial_Sums (||.z.|| rExpSeq)) . k ; ::_thesis: S1[k + 1] then A3: ||.((Partial_Sums (z rExpSeq)) . k).|| + ((||.z.|| rExpSeq) . (k + 1)) <= ((Partial_Sums (||.z.|| rExpSeq)) . k) + ((||.z.|| rExpSeq) . (k + 1)) by XREAL_1:6; A4: ||.(((Partial_Sums (z rExpSeq)) . k) + ((z rExpSeq) . (k + 1))).|| <= ||.((Partial_Sums (z rExpSeq)) . k).|| + ||.((z rExpSeq) . (k + 1)).|| by LOPBAN_3:38; ||.((z rExpSeq) . (k + 1)).|| <= (||.z.|| rExpSeq) . (k + 1) by Th14; then A5: ||.((Partial_Sums (z rExpSeq)) . k).|| + ||.((z rExpSeq) . (k + 1)).|| <= ||.((Partial_Sums (z rExpSeq)) . k).|| + ((||.z.|| rExpSeq) . (k + 1)) by XREAL_1:7; A6: ((Partial_Sums (||.z.|| rExpSeq)) . k) + ((||.z.|| rExpSeq) . (k + 1)) = (Partial_Sums (||.z.|| rExpSeq)) . (k + 1) by SERIES_1:def_1; ||.((Partial_Sums (z rExpSeq)) . (k + 1)).|| = ||.(((Partial_Sums (z rExpSeq)) . k) + ((z rExpSeq) . (k + 1))).|| by BHSP_4:def_1; then ||.((Partial_Sums (z rExpSeq)) . (k + 1)).|| <= ||.((Partial_Sums (z rExpSeq)) . k).|| + ((||.z.|| rExpSeq) . (k + 1)) by A4, A5, XXREAL_0:2; hence S1[k + 1] by A3, A6, XXREAL_0:2; ::_thesis: verum end; ||.((Partial_Sums (z rExpSeq)) . 0).|| = ||.((z rExpSeq) . 0).|| by BHSP_4:def_1 .= ||.((1 / (0 !)) * (z #N 0)).|| by Def2 .= ||.((1 / 1) * (1. X)).|| by LOPBAN_3:def_9, NEWTON:12 .= ||.(1. X).|| by LOPBAN_3:38 .= 1 by LOPBAN_3:38 ; then A7: S1[ 0 ] by A1; A8: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A7, A2); hence ||.((Partial_Sums (z rExpSeq)) . k).|| <= (Partial_Sums (||.z.|| rExpSeq)) . k ; ::_thesis: ( (Partial_Sums (||.z.|| rExpSeq)) . k <= Sum (||.z.|| rExpSeq) & ||.((Partial_Sums (z rExpSeq)) . k).|| <= Sum (||.z.|| rExpSeq) ) A9: for n being Element of NAT holds 0 <= (||.z.|| rExpSeq) . n by Th27; ||.z.|| rExpSeq is summable by SIN_COS:45; then A10: Partial_Sums (||.z.|| rExpSeq) is bounded_above by A9, SERIES_1:17; then (Partial_Sums (||.z.|| rExpSeq)) . k <= lim (Partial_Sums (||.z.|| rExpSeq)) by A9, SEQ_4:37, SERIES_1:16; hence (Partial_Sums (||.z.|| rExpSeq)) . k <= Sum (||.z.|| rExpSeq) by SERIES_1:def_3; ::_thesis: ||.((Partial_Sums (z rExpSeq)) . k).|| <= Sum (||.z.|| rExpSeq) now__::_thesis:_for_k_being_Element_of_NAT_holds_(Partial_Sums_(||.z.||_rExpSeq))_._k_<=_Sum_(||.z.||_rExpSeq) let k be Element of NAT ; ::_thesis: (Partial_Sums (||.z.|| rExpSeq)) . k <= Sum (||.z.|| rExpSeq) lim (Partial_Sums (||.z.|| rExpSeq)) = Sum (||.z.|| rExpSeq) by SERIES_1:def_3; hence (Partial_Sums (||.z.|| rExpSeq)) . k <= Sum (||.z.|| rExpSeq) by A9, A10, SEQ_4:37, SERIES_1:16; ::_thesis: verum end; then A11: (Partial_Sums (||.z.|| rExpSeq)) . k <= Sum (||.z.|| rExpSeq) ; ||.((Partial_Sums (z rExpSeq)) . k).|| <= (Partial_Sums (||.z.|| rExpSeq)) . k by A8; hence ||.((Partial_Sums (z rExpSeq)) . k).|| <= Sum (||.z.|| rExpSeq) by A11, XXREAL_0:2; ::_thesis: verum end; theorem Th29: :: LOPBAN_4:29 for X being Banach_Algebra for z being Element of X holds 1 <= Sum (||.z.|| rExpSeq) proof let X be Banach_Algebra; ::_thesis: for z being Element of X holds 1 <= Sum (||.z.|| rExpSeq) let z be Element of X; ::_thesis: 1 <= Sum (||.z.|| rExpSeq) ||.((Partial_Sums (z rExpSeq)) . 0).|| = ||.((z rExpSeq) . 0).|| by BHSP_4:def_1 .= ||.(1. X).|| by Th14 .= 1 by LOPBAN_3:38 ; hence 1 <= Sum (||.z.|| rExpSeq) by Th28; ::_thesis: verum end; theorem Th30: :: LOPBAN_4:30 for X being Banach_Algebra for z being Element of X for n, m being Element of NAT holds ( abs ((Partial_Sums (||.z.|| rExpSeq)) . n) = (Partial_Sums (||.z.|| rExpSeq)) . n & ( n <= m implies abs (((Partial_Sums (||.z.|| rExpSeq)) . m) - ((Partial_Sums (||.z.|| rExpSeq)) . n)) = ((Partial_Sums (||.z.|| rExpSeq)) . m) - ((Partial_Sums (||.z.|| rExpSeq)) . n) ) ) proof let X be Banach_Algebra; ::_thesis: for z being Element of X for n, m being Element of NAT holds ( abs ((Partial_Sums (||.z.|| rExpSeq)) . n) = (Partial_Sums (||.z.|| rExpSeq)) . n & ( n <= m implies abs (((Partial_Sums (||.z.|| rExpSeq)) . m) - ((Partial_Sums (||.z.|| rExpSeq)) . n)) = ((Partial_Sums (||.z.|| rExpSeq)) . m) - ((Partial_Sums (||.z.|| rExpSeq)) . n) ) ) let z be Element of X; ::_thesis: for n, m being Element of NAT holds ( abs ((Partial_Sums (||.z.|| rExpSeq)) . n) = (Partial_Sums (||.z.|| rExpSeq)) . n & ( n <= m implies abs (((Partial_Sums (||.z.|| rExpSeq)) . m) - ((Partial_Sums (||.z.|| rExpSeq)) . n)) = ((Partial_Sums (||.z.|| rExpSeq)) . m) - ((Partial_Sums (||.z.|| rExpSeq)) . n) ) ) let n, m be Element of NAT ; ::_thesis: ( abs ((Partial_Sums (||.z.|| rExpSeq)) . n) = (Partial_Sums (||.z.|| rExpSeq)) . n & ( n <= m implies abs (((Partial_Sums (||.z.|| rExpSeq)) . m) - ((Partial_Sums (||.z.|| rExpSeq)) . n)) = ((Partial_Sums (||.z.|| rExpSeq)) . m) - ((Partial_Sums (||.z.|| rExpSeq)) . n) ) ) for n being Element of NAT holds 0 <= (||.z.|| rExpSeq) . n by Th27; hence ( abs ((Partial_Sums (||.z.|| rExpSeq)) . n) = (Partial_Sums (||.z.|| rExpSeq)) . n & ( n <= m implies abs (((Partial_Sums (||.z.|| rExpSeq)) . m) - ((Partial_Sums (||.z.|| rExpSeq)) . n)) = ((Partial_Sums (||.z.|| rExpSeq)) . m) - ((Partial_Sums (||.z.|| rExpSeq)) . n) ) ) by COMSEQ_3:9; ::_thesis: verum end; theorem Th31: :: LOPBAN_4:31 for X being Banach_Algebra for z, w being Element of X for k, n being Element of NAT holds abs ((Partial_Sums ||.(Conj (k,z,w)).||) . n) = (Partial_Sums ||.(Conj (k,z,w)).||) . n proof let X be Banach_Algebra; ::_thesis: for z, w being Element of X for k, n being Element of NAT holds abs ((Partial_Sums ||.(Conj (k,z,w)).||) . n) = (Partial_Sums ||.(Conj (k,z,w)).||) . n let z, w be Element of X; ::_thesis: for k, n being Element of NAT holds abs ((Partial_Sums ||.(Conj (k,z,w)).||) . n) = (Partial_Sums ||.(Conj (k,z,w)).||) . n let k, n be Element of NAT ; ::_thesis: abs ((Partial_Sums ||.(Conj (k,z,w)).||) . n) = (Partial_Sums ||.(Conj (k,z,w)).||) . n A1: (Partial_Sums ||.(Conj (k,z,w)).||) . 0 = ||.(Conj (k,z,w)).|| . 0 by SERIES_1:def_1; A2: now__::_thesis:_for_n_being_Element_of_NAT_holds_0_<=_||.(Conj_(k,z,w)).||_._n let n be Element of NAT ; ::_thesis: 0 <= ||.(Conj (k,z,w)).|| . n ||.(Conj (k,z,w)).|| . n = ||.((Conj (k,z,w)) . n).|| by NORMSP_0:def_4; hence 0 <= ||.(Conj (k,z,w)).|| . n by NORMSP_1:4; ::_thesis: verum end; then Partial_Sums ||.(Conj (k,z,w)).|| is non-decreasing by SERIES_1:16; then A3: (Partial_Sums ||.(Conj (k,z,w)).||) . 0 <= (Partial_Sums ||.(Conj (k,z,w)).||) . n by SEQM_3:6; 0 <= ||.(Conj (k,z,w)).|| . 0 by A2; hence abs ((Partial_Sums ||.(Conj (k,z,w)).||) . n) = (Partial_Sums ||.(Conj (k,z,w)).||) . n by A3, A1, ABSVALUE:def_1; ::_thesis: verum end; theorem Th32: :: LOPBAN_4:32 for X being Banach_Algebra for z, w being Element of X for p being real number st p > 0 holds ex n being Element of NAT st for k being Element of NAT st n <= k holds abs ((Partial_Sums ||.(Conj (k,z,w)).||) . k) < p proof let X be Banach_Algebra; ::_thesis: for z, w being Element of X for p being real number st p > 0 holds ex n being Element of NAT st for k being Element of NAT st n <= k holds abs ((Partial_Sums ||.(Conj (k,z,w)).||) . k) < p let z, w be Element of X; ::_thesis: for p being real number st p > 0 holds ex n being Element of NAT st for k being Element of NAT st n <= k holds abs ((Partial_Sums ||.(Conj (k,z,w)).||) . k) < p let p be real number ; ::_thesis: ( p > 0 implies ex n being Element of NAT st for k being Element of NAT st n <= k holds abs ((Partial_Sums ||.(Conj (k,z,w)).||) . k) < p ) assume A1: p > 0 ; ::_thesis: ex n being Element of NAT st for k being Element of NAT st n <= k holds abs ((Partial_Sums ||.(Conj (k,z,w)).||) . k) < p reconsider pp = p as Real by XREAL_0:def_1; set p1 = min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq))))); A2: 1 <= Sum (||.z.|| rExpSeq) by Th29; then 0 * (Sum (||.z.|| rExpSeq)) < 4 * (Sum (||.z.|| rExpSeq)) by XREAL_1:68; then A3: 0 / (4 * (Sum (||.z.|| rExpSeq))) < p / (4 * (Sum (||.z.|| rExpSeq))) by A1, XREAL_1:74; A4: 1 <= Sum (||.w.|| rExpSeq) by Th29; then 0 * (Sum (||.w.|| rExpSeq)) < 4 * (Sum (||.w.|| rExpSeq)) by XREAL_1:68; then 0 / (4 * (Sum (||.w.|| rExpSeq))) < p / (4 * (Sum (||.w.|| rExpSeq))) by A1, XREAL_1:74; then A5: min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq))))) > 0 by A3, XXREAL_0:15; Partial_Sums (w rExpSeq) is convergent by LOPBAN_3:def_1; then 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 ||.(((Partial_Sums (w rExpSeq)) . m) - ((Partial_Sums (w rExpSeq)) . n)).|| < s by LOPBAN_3:4; then Partial_Sums (w rExpSeq) is Cauchy_sequence_by_Norm by LOPBAN_3:5; then consider n2 being Element of NAT such that A6: for k, l being Element of NAT st n2 <= k & n2 <= l holds ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . l)).|| < min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq))))) by A5, RSSPACE3:8; ||.z.|| rExpSeq is summable by SIN_COS:45; then Partial_Sums (||.z.|| rExpSeq) is convergent by SERIES_1:def_2; then consider n1 being Element of NAT such that A7: for k, l being Element of NAT st n1 <= k & n1 <= l holds abs (((Partial_Sums (||.z.|| rExpSeq)) . k) - ((Partial_Sums (||.z.|| rExpSeq)) . l)) < min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq))))) by A5, COMSEQ_3:4; set n3 = n1 + n2; take n4 = (n1 + n2) + (n1 + n2); ::_thesis: for k being Element of NAT st n4 <= k holds abs ((Partial_Sums ||.(Conj (k,z,w)).||) . k) < p A8: now__::_thesis:_for_n,_k,_l_being_Element_of_NAT_st_l_<=_k_holds_ ||.(Conj_(k,z,w)).||_._l_<=_((||.z.||_rExpSeq)_._l)_*_||.(((Partial_Sums_(w_rExpSeq))_._k)_-_((Partial_Sums_(w_rExpSeq))_._(k_-'_l))).|| let n, k be Element of NAT ; ::_thesis: for l being Element of NAT st l <= k holds ||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).|| now__::_thesis:_for_l_being_Element_of_NAT_st_l_<=_k_holds_ ||.(Conj_(k,z,w)).||_._l_<=_((||.z.||_rExpSeq)_._l)_*_||.(((Partial_Sums_(w_rExpSeq))_._k)_-_((Partial_Sums_(w_rExpSeq))_._(k_-'_l))).|| let l be Element of NAT ; ::_thesis: ( l <= k implies ||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).|| ) assume A9: l <= k ; ::_thesis: ||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).|| A10: ||.(((z rExpSeq) . l) * (((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l)))).|| <= ||.((z rExpSeq) . l).|| * ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).|| by LOPBAN_3:38; 0 <= ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).|| by NORMSP_1:4; then A11: ||.((z rExpSeq) . l).|| * ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).|| <= ((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).|| by Th14, XREAL_1:64; ||.(Conj (k,z,w)).|| . l = ||.((Conj (k,z,w)) . l).|| by NORMSP_0:def_4 .= ||.(((z rExpSeq) . l) * (((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l)))).|| by A9, Def9 ; hence ||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).|| by A10, A11, XXREAL_0:2; ::_thesis: verum end; hence for l being Element of NAT st l <= k holds ||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).|| ; ::_thesis: verum end; A12: now__::_thesis:_for_k,_l_being_Element_of_NAT_st_l_<=_k_holds_ ||.(Conj_(k,z,w)).||_._l_<=_((||.z.||_rExpSeq)_._l)_*_(2_*_(Sum_(||.w.||_rExpSeq))) let k be Element of NAT ; ::_thesis: for l being Element of NAT st l <= k holds ||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * (2 * (Sum (||.w.|| rExpSeq))) now__::_thesis:_for_l_being_Element_of_NAT_st_l_<=_k_holds_ ||.(Conj_(k,z,w)).||_._l_<=_((||.z.||_rExpSeq)_._l)_*_(2_*_(Sum_(||.w.||_rExpSeq))) let l be Element of NAT ; ::_thesis: ( l <= k implies ||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * (2 * (Sum (||.w.|| rExpSeq))) ) A13: ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).|| <= ||.((Partial_Sums (w rExpSeq)) . k).|| + ||.((Partial_Sums (w rExpSeq)) . (k -' l)).|| by NORMSP_1:3; ||.((Partial_Sums (w rExpSeq)) . (k -' l)).|| <= Sum (||.w.|| rExpSeq) by Th28; then A14: (Sum (||.w.|| rExpSeq)) + ||.((Partial_Sums (w rExpSeq)) . (k -' l)).|| <= (Sum (||.w.|| rExpSeq)) + (Sum (||.w.|| rExpSeq)) by XREAL_1:6; ||.((Partial_Sums (w rExpSeq)) . k).|| <= Sum (||.w.|| rExpSeq) by Th28; then ||.((Partial_Sums (w rExpSeq)) . k).|| + ||.((Partial_Sums (w rExpSeq)) . (k -' l)).|| <= (Sum (||.w.|| rExpSeq)) + ||.((Partial_Sums (w rExpSeq)) . (k -' l)).|| by XREAL_1:6; then ||.((Partial_Sums (w rExpSeq)) . k).|| + ||.((Partial_Sums (w rExpSeq)) . (k -' l)).|| <= 2 * (Sum (||.w.|| rExpSeq)) by A14, XXREAL_0:2; then A15: ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).|| <= 2 * (Sum (||.w.|| rExpSeq)) by A13, XXREAL_0:2; assume l <= k ; ::_thesis: ||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * (2 * (Sum (||.w.|| rExpSeq))) then A16: ||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).|| by A8; 0 <= (||.z.|| rExpSeq) . l by Th27; then ((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).|| <= ((||.z.|| rExpSeq) . l) * (2 * (Sum (||.w.|| rExpSeq))) by A15, XREAL_1:64; hence ||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * (2 * (Sum (||.w.|| rExpSeq))) by A16, XXREAL_0:2; ::_thesis: verum end; hence for l being Element of NAT st l <= k holds ||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * (2 * (Sum (||.w.|| rExpSeq))) ; ::_thesis: verum end; now__::_thesis:_for_k_being_Element_of_NAT_st_n4_<=_k_holds_ abs_((Partial_Sums_||.(Conj_(k,z,w)).||)_._k)_<_p 0 < p / 4 by A1, XREAL_1:224; then A17: 0 + (p / 4) < (p / 4) + (p / 4) by XREAL_1:6; A18: 0 <> Sum (||.z.|| rExpSeq) by Th29; A19: (Sum (||.z.|| rExpSeq)) * (p / (4 * (Sum (||.z.|| rExpSeq)))) = (Sum (||.z.|| rExpSeq)) * (p * ((4 * (Sum (||.z.|| rExpSeq))) ")) by XCMPLX_0:def_9 .= ((Sum (||.z.|| rExpSeq)) * p) * ((4 * (Sum (||.z.|| rExpSeq))) ") .= ((Sum (||.z.|| rExpSeq)) * p) / (4 * (Sum (||.z.|| rExpSeq))) by XCMPLX_0:def_9 .= p / 4 by A18, XCMPLX_1:91 ; let k be Element of NAT ; ::_thesis: ( n4 <= k implies abs ((Partial_Sums ||.(Conj (k,z,w)).||) . k) < p ) assume A20: n4 <= k ; ::_thesis: abs ((Partial_Sums ||.(Conj (k,z,w)).||) . k) < p A21: 0 + (n1 + n2) <= (n1 + n2) + (n1 + n2) by XREAL_1:6; then k -' (n1 + n2) = k - (n1 + n2) by A20, XREAL_1:233, XXREAL_0:2; then A22: k = (k -' (n1 + n2)) + (n1 + n2) ; A23: n1 + n2 <= k by A20, A21, XXREAL_0:2; now__::_thesis:_for_l_being_Element_of_NAT_st_l_<=_n1_+_n2_holds_ ||.(Conj_(k,z,w)).||_._l_<=_(min_((pp_/_(4_*_(Sum_(||.z.||_rExpSeq)))),(pp_/_(4_*_(Sum_(||.w.||_rExpSeq))))))_*_((||.z.||_rExpSeq)_._l) let l be Element of NAT ; ::_thesis: ( l <= n1 + n2 implies ||.(Conj (k,z,w)).|| . l <= (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))))) * ((||.z.|| rExpSeq) . l) ) A24: 0 + n2 <= n1 + n2 by XREAL_1:6; 0 + (n1 + n2) <= (n1 + n2) + (n1 + n2) by XREAL_1:6; then n2 <= n4 by A24, XXREAL_0:2; then A25: n2 <= k by A20, XXREAL_0:2; A26: 0 <= (||.z.|| rExpSeq) . l by Th27; assume A27: l <= n1 + n2 ; ::_thesis: ||.(Conj (k,z,w)).|| . l <= (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))))) * ((||.z.|| rExpSeq) . l) then A28: ((n1 + n2) + (n1 + n2)) - (n1 + n2) <= ((n1 + n2) + (n1 + n2)) - l by XREAL_1:10; l <= k by A23, A27, XXREAL_0:2; then A29: ||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).|| by A8; n4 - l <= k - l by A20, XREAL_1:9; then A30: n1 + n2 <= k - l by A28, XXREAL_0:2; k -' l = k - l by A23, A27, XREAL_1:233, XXREAL_0:2; then n2 <= k -' l by A24, A30, XXREAL_0:2; then ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).|| < min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq))))) by A6, A25; then ((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).|| <= ((||.z.|| rExpSeq) . l) * (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))))) by A26, XREAL_1:64; hence ||.(Conj (k,z,w)).|| . l <= (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))))) * ((||.z.|| rExpSeq) . l) by A29, XXREAL_0:2; ::_thesis: verum end; then A31: (Partial_Sums ||.(Conj (k,z,w)).||) . (n1 + n2) <= ((Partial_Sums (||.z.|| rExpSeq)) . (n1 + n2)) * (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))))) by COMSEQ_3:7; A32: n1 + 0 <= n1 + n2 by XREAL_1:6; then n1 <= k by A23, XXREAL_0:2; then abs (((Partial_Sums (||.z.|| rExpSeq)) . k) - ((Partial_Sums (||.z.|| rExpSeq)) . (n1 + n2))) <= min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq))))) by A7, A32; then ((Partial_Sums (||.z.|| rExpSeq)) . k) - ((Partial_Sums (||.z.|| rExpSeq)) . (n1 + n2)) <= min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq))))) by A20, A21, Th30, XXREAL_0:2; then A33: (((Partial_Sums (||.z.|| rExpSeq)) . k) - ((Partial_Sums (||.z.|| rExpSeq)) . (n1 + n2))) * (2 * (Sum (||.w.|| rExpSeq))) <= (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))))) * (2 * (Sum (||.w.|| rExpSeq))) by A4, XREAL_1:64; for l being Element of NAT st l <= k holds ||.(Conj (k,z,w)).|| . l <= (2 * (Sum (||.w.|| rExpSeq))) * ((||.z.|| rExpSeq) . l) by A12; then ((Partial_Sums ||.(Conj (k,z,w)).||) . k) - ((Partial_Sums ||.(Conj (k,z,w)).||) . (n1 + n2)) <= (((Partial_Sums (||.z.|| rExpSeq)) . k) - ((Partial_Sums (||.z.|| rExpSeq)) . (n1 + n2))) * (2 * (Sum (||.w.|| rExpSeq))) by A22, COMSEQ_3:8; then A34: ((Partial_Sums ||.(Conj (k,z,w)).||) . k) - ((Partial_Sums ||.(Conj (k,z,w)).||) . (n1 + n2)) <= (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))))) * (2 * (Sum (||.w.|| rExpSeq))) by A33, XXREAL_0:2; A35: 0 <> Sum (||.w.|| rExpSeq) by Th29; ((Partial_Sums (||.z.|| rExpSeq)) . (n1 + n2)) * (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))))) <= (Sum (||.z.|| rExpSeq)) * (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))))) by A5, Th28, XREAL_1:64; then A36: (Partial_Sums ||.(Conj (k,z,w)).||) . (n1 + n2) <= (Sum (||.z.|| rExpSeq)) * (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))))) by A31, XXREAL_0:2; (Sum (||.z.|| rExpSeq)) * (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))))) <= (Sum (||.z.|| rExpSeq)) * (p / (4 * (Sum (||.z.|| rExpSeq)))) by A2, XREAL_1:64, XXREAL_0:17; then (Partial_Sums ||.(Conj (k,z,w)).||) . (n1 + n2) <= p / 4 by A36, A19, XXREAL_0:2; then A37: (Partial_Sums ||.(Conj (k,z,w)).||) . (n1 + n2) < p / 2 by A17, XXREAL_0:2; 0 * (Sum (||.w.|| rExpSeq)) < 2 * (Sum (||.w.|| rExpSeq)) by A4, XREAL_1:68; then A38: (2 * (Sum (||.w.|| rExpSeq))) * (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))))) <= (2 * (Sum (||.w.|| rExpSeq))) * (p / (4 * (Sum (||.w.|| rExpSeq)))) by XREAL_1:64, XXREAL_0:17; (2 * (Sum (||.w.|| rExpSeq))) * (p / (4 * (Sum (||.w.|| rExpSeq)))) = (2 * (Sum (||.w.|| rExpSeq))) * (p * ((4 * (Sum (||.w.|| rExpSeq))) ")) by XCMPLX_0:def_9 .= ((2 * (Sum (||.w.|| rExpSeq))) * p) * ((4 * (Sum (||.w.|| rExpSeq))) ") .= ((2 * p) * (Sum (||.w.|| rExpSeq))) / (4 * (Sum (||.w.|| rExpSeq))) by XCMPLX_0:def_9 .= (2 * p) / 4 by A35, XCMPLX_1:91 .= p / 2 ; then ((Partial_Sums ||.(Conj (k,z,w)).||) . k) - ((Partial_Sums ||.(Conj (k,z,w)).||) . (n1 + n2)) <= p / 2 by A34, A38, XXREAL_0:2; then (((Partial_Sums ||.(Conj (k,z,w)).||) . k) - ((Partial_Sums ||.(Conj (k,z,w)).||) . (n1 + n2))) + ((Partial_Sums ||.(Conj (k,z,w)).||) . (n1 + n2)) < (p / 2) + (p / 2) by A37, XREAL_1:8; hence abs ((Partial_Sums ||.(Conj (k,z,w)).||) . k) < p by Th31; ::_thesis: verum end; hence for k being Element of NAT st n4 <= k holds abs ((Partial_Sums ||.(Conj (k,z,w)).||) . k) < p ; ::_thesis: verum end; theorem Th33: :: LOPBAN_4:33 for X being Banach_Algebra for z, w being Element of X for seq being sequence of X st ( for k being Element of NAT holds seq . k = (Partial_Sums (Conj (k,z,w))) . k ) holds ( seq is convergent & lim seq = 0. X ) proof let X be Banach_Algebra; ::_thesis: for z, w being Element of X for seq being sequence of X st ( for k being Element of NAT holds seq . k = (Partial_Sums (Conj (k,z,w))) . k ) holds ( seq is convergent & lim seq = 0. X ) let z, w be Element of X; ::_thesis: for seq being sequence of X st ( for k being Element of NAT holds seq . k = (Partial_Sums (Conj (k,z,w))) . k ) holds ( seq is convergent & lim seq = 0. X ) deffunc H1( Element of NAT ) -> Element of REAL = (Partial_Sums ||.(Conj ($1,z,w)).||) . $1; ex rseq being Real_Sequence st for k being Element of NAT holds rseq . k = H1(k) from SEQ_1:sch_1(); then consider rseq being Real_Sequence such that A1: for k being Element of NAT holds rseq . k = (Partial_Sums ||.(Conj (k,z,w)).||) . k ; let seq be sequence of X; ::_thesis: ( ( for k being Element of NAT holds seq . k = (Partial_Sums (Conj (k,z,w))) . k ) implies ( seq is convergent & lim seq = 0. X ) ) assume A2: for k being Element of NAT holds seq . k = (Partial_Sums (Conj (k,z,w))) . k ; ::_thesis: ( seq is convergent & lim seq = 0. X ) A3: now__::_thesis:_for_k_being_Element_of_NAT_holds_||.(seq_._k).||_<=_(Partial_Sums_||.(Conj_(k,z,w)).||)_._k let k be Element of NAT ; ::_thesis: ||.(seq . k).|| <= (Partial_Sums ||.(Conj (k,z,w)).||) . k ||.(seq . k).|| = ||.((Partial_Sums (Conj (k,z,w))) . k).|| by A2; hence ||.(seq . k).|| <= (Partial_Sums ||.(Conj (k,z,w)).||) . k by Th10; ::_thesis: verum end; A4: now__::_thesis:_for_k_being_Element_of_NAT_holds_||.(seq_._k).||_<=_rseq_._k let k be Element of NAT ; ::_thesis: ||.(seq . k).|| <= rseq . k ||.(seq . k).|| <= (Partial_Sums ||.(Conj (k,z,w)).||) . k by A3; hence ||.(seq . k).|| <= rseq . k by A1; ::_thesis: verum end; A5: now__::_thesis:_for_p_being_real_number_st_p_>_0_holds_ ex_n_being_Element_of_NAT_st_ for_k_being_Element_of_NAT_st_n_<=_k_holds_ abs_((rseq_._k)_-_0)_<_p let p be real number ; ::_thesis: ( p > 0 implies ex n being Element of NAT st for k being Element of NAT st n <= k holds abs ((rseq . k) - 0) < p ) assume p > 0 ; ::_thesis: ex n being Element of NAT st for k being Element of NAT st n <= k holds abs ((rseq . k) - 0) < p then consider n being Element of NAT such that A6: for k being Element of NAT st n <= k holds abs ((Partial_Sums ||.(Conj (k,z,w)).||) . k) < p by Th32; take n = n; ::_thesis: for k being Element of NAT st n <= k holds abs ((rseq . k) - 0) < p now__::_thesis:_for_k_being_Element_of_NAT_st_n_<=_k_holds_ abs_((rseq_._k)_-_0)_<_p let k be Element of NAT ; ::_thesis: ( n <= k implies abs ((rseq . k) - 0) < p ) assume A7: n <= k ; ::_thesis: abs ((rseq . k) - 0) < p abs ((rseq . k) - 0) = abs ((Partial_Sums ||.(Conj (k,z,w)).||) . k) by A1; hence abs ((rseq . k) - 0) < p by A6, A7; ::_thesis: verum end; hence for k being Element of NAT st n <= k holds abs ((rseq . k) - 0) < p ; ::_thesis: verum end; then A8: rseq is convergent by SEQ_2:def_6; then lim rseq = 0 by A5, SEQ_2:def_7; hence ( seq is convergent & lim seq = 0. X ) by A4, A8, Th12; ::_thesis: verum end; Lm3: for X being Banach_Algebra for z, w being Element of X st z,w are_commutative holds (Sum (z rExpSeq)) * (Sum (w rExpSeq)) = Sum ((z + w) rExpSeq) proof let X be Banach_Algebra; ::_thesis: for z, w being Element of X st z,w are_commutative holds (Sum (z rExpSeq)) * (Sum (w rExpSeq)) = Sum ((z + w) rExpSeq) let z, w be Element of X; ::_thesis: ( z,w are_commutative implies (Sum (z rExpSeq)) * (Sum (w rExpSeq)) = Sum ((z + w) rExpSeq) ) assume A1: z,w are_commutative ; ::_thesis: (Sum (z rExpSeq)) * (Sum (w rExpSeq)) = Sum ((z + w) rExpSeq) deffunc H1( Element of NAT ) -> Element of the carrier of X = (Partial_Sums (Conj ($1,z,w))) . $1; ex seq being sequence of X st for k being Element of NAT holds seq . k = H1(k) from FUNCT_2:sch_4(); then consider seq being sequence of X such that A2: for k being Element of NAT holds seq . k = (Partial_Sums (Conj (k,z,w))) . k ; now__::_thesis:_for_k_being_Element_of_NAT_holds_seq_._k_=_(((Partial_Sums_(z_rExpSeq))_*_(Partial_Sums_(w_rExpSeq)))_-_(Partial_Sums_((z_+_w)_rExpSeq)))_._k let k be Element of NAT ; ::_thesis: seq . k = (((Partial_Sums (z rExpSeq)) * (Partial_Sums (w rExpSeq))) - (Partial_Sums ((z + w) rExpSeq))) . k thus seq . k = (Partial_Sums (Conj (k,z,w))) . k by A2 .= (((Partial_Sums (z rExpSeq)) . k) * ((Partial_Sums (w rExpSeq)) . k)) - ((Partial_Sums ((z + w) rExpSeq)) . k) by A1, Th26 .= (((Partial_Sums (z rExpSeq)) * (Partial_Sums (w rExpSeq))) . k) - ((Partial_Sums ((z + w) rExpSeq)) . k) by LOPBAN_3:def_7 .= (((Partial_Sums (z rExpSeq)) * (Partial_Sums (w rExpSeq))) - (Partial_Sums ((z + w) rExpSeq))) . k by NORMSP_1:def_3 ; ::_thesis: verum end; then A3: seq = ((Partial_Sums (z rExpSeq)) * (Partial_Sums (w rExpSeq))) - (Partial_Sums ((z + w) rExpSeq)) by FUNCT_2:63; A4: Partial_Sums (w rExpSeq) is convergent by LOPBAN_3:def_1; A5: lim seq = 0. X by A2, Th33; A6: Partial_Sums ((z + w) rExpSeq) is convergent by LOPBAN_3:def_1; A7: Partial_Sums (z rExpSeq) is convergent by LOPBAN_3:def_1; then A8: lim ((Partial_Sums (z rExpSeq)) * (Partial_Sums (w rExpSeq))) = (lim (Partial_Sums (z rExpSeq))) * (lim (Partial_Sums (w rExpSeq))) by A4, Th8; (Partial_Sums (z rExpSeq)) * (Partial_Sums (w rExpSeq)) is convergent by A7, A4, Th3; hence (Sum (z rExpSeq)) * (Sum (w rExpSeq)) = Sum ((z + w) rExpSeq) by A3, A6, A8, A5, Th1; ::_thesis: verum end; definition let X be Banach_Algebra; func exp_ X -> Function of the carrier of X, the carrier of X means :Def10: :: LOPBAN_4:def 10 for z being Element of X holds it . z = Sum (z rExpSeq); existence ex b1 being Function of the carrier of X, the carrier of X st for z being Element of X holds b1 . z = Sum (z rExpSeq) proof deffunc H1( Element of X) -> Element of the carrier of X = Sum ($1 rExpSeq); ex f being Function of the carrier of X, the carrier of X st for z being Element of X holds f . z = H1(z) from FUNCT_2:sch_4(); hence ex b1 being Function of the carrier of X, the carrier of X st for z being Element of X holds b1 . z = Sum (z rExpSeq) ; ::_thesis: verum end; uniqueness for b1, b2 being Function of the carrier of X, the carrier of X st ( for z being Element of X holds b1 . z = Sum (z rExpSeq) ) & ( for z being Element of X holds b2 . z = Sum (z rExpSeq) ) holds b1 = b2 proof let f1, f2 be Function of the carrier of X, the carrier of X; ::_thesis: ( ( for z being Element of X holds f1 . z = Sum (z rExpSeq) ) & ( for z being Element of X holds f2 . z = Sum (z rExpSeq) ) implies f1 = f2 ) assume that A1: for z being Element of X holds f1 . z = Sum (z rExpSeq) and A2: for z being Element of X holds f2 . z = Sum (z rExpSeq) ; ::_thesis: f1 = f2 for z being Element of X holds f1 . z = f2 . z proof let z be Element of X; ::_thesis: f1 . z = f2 . z thus f1 . z = Sum (z rExpSeq) by A1 .= f2 . z by A2 ; ::_thesis: verum end; hence f1 = f2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def10 defines exp_ LOPBAN_4:def_10_:_ for X being Banach_Algebra for b2 being Function of the carrier of X, the carrier of X holds ( b2 = exp_ X iff for z being Element of X holds b2 . z = Sum (z rExpSeq) ); definition let X be Banach_Algebra; let z be Element of X; func exp z -> Element of X equals :: LOPBAN_4:def 11 (exp_ X) . z; correctness coherence (exp_ X) . z is Element of X; ; end; :: deftheorem defines exp LOPBAN_4:def_11_:_ for X being Banach_Algebra for z being Element of X holds exp z = (exp_ X) . z; theorem :: LOPBAN_4:34 for X being Banach_Algebra for z being Element of X holds exp z = Sum (z rExpSeq) by Def10; theorem Th35: :: LOPBAN_4:35 for X being Banach_Algebra for z1, z2 being Element of X st z1,z2 are_commutative holds ( exp (z1 + z2) = (exp z1) * (exp z2) & exp (z2 + z1) = (exp z2) * (exp z1) & exp (z1 + z2) = exp (z2 + z1) & exp z1, exp z2 are_commutative ) proof let X be Banach_Algebra; ::_thesis: for z1, z2 being Element of X st z1,z2 are_commutative holds ( exp (z1 + z2) = (exp z1) * (exp z2) & exp (z2 + z1) = (exp z2) * (exp z1) & exp (z1 + z2) = exp (z2 + z1) & exp z1, exp z2 are_commutative ) let z1, z2 be Element of X; ::_thesis: ( z1,z2 are_commutative implies ( exp (z1 + z2) = (exp z1) * (exp z2) & exp (z2 + z1) = (exp z2) * (exp z1) & exp (z1 + z2) = exp (z2 + z1) & exp z1, exp z2 are_commutative ) ) assume A1: z1,z2 are_commutative ; ::_thesis: ( exp (z1 + z2) = (exp z1) * (exp z2) & exp (z2 + z1) = (exp z2) * (exp z1) & exp (z1 + z2) = exp (z2 + z1) & exp z1, exp z2 are_commutative ) A2: exp (z2 + z1) = Sum ((z2 + z1) rExpSeq) by Def10 .= (Sum (z2 rExpSeq)) * (Sum (z1 rExpSeq)) by A1, Lm3 .= (exp z2) * (Sum (z1 rExpSeq)) by Def10 .= (exp z2) * (exp z1) by Def10 ; exp (z1 + z2) = Sum ((z1 + z2) rExpSeq) by Def10 .= (Sum (z1 rExpSeq)) * (Sum (z2 rExpSeq)) by A1, Lm3 .= (exp z1) * (Sum (z2 rExpSeq)) by Def10 .= (exp z1) * (exp z2) by Def10 ; hence ( exp (z1 + z2) = (exp z1) * (exp z2) & exp (z2 + z1) = (exp z2) * (exp z1) & exp (z1 + z2) = exp (z2 + z1) & exp z1, exp z2 are_commutative ) by A2, Def1; ::_thesis: verum end; theorem :: LOPBAN_4:36 for X being Banach_Algebra for z1, z2 being Element of X st z1,z2 are_commutative holds z1 * (exp z2) = (exp z2) * z1 proof let X be Banach_Algebra; ::_thesis: for z1, z2 being Element of X st z1,z2 are_commutative holds z1 * (exp z2) = (exp z2) * z1 let z1, z2 be Element of X; ::_thesis: ( z1,z2 are_commutative implies z1 * (exp z2) = (exp z2) * z1 ) assume A1: z1,z2 are_commutative ; ::_thesis: z1 * (exp z2) = (exp z2) * z1 now__::_thesis:_for_n_being_Element_of_NAT_holds_(z1_*_(z2_rExpSeq))_._n_=_((z2_rExpSeq)_*_z1)_._n let n be Element of NAT ; ::_thesis: (z1 * (z2 rExpSeq)) . n = ((z2 rExpSeq) * z1) . n thus (z1 * (z2 rExpSeq)) . n = z1 * ((z2 rExpSeq) . n) by LOPBAN_3:def_5 .= z1 * ((1 / (n !)) * (z2 #N n)) by Def2 .= (1 / (n !)) * (z1 * (z2 #N n)) by LOPBAN_3:38 .= (1 / (n !)) * ((z2 #N n) * z1) by A1, Lm2 .= ((1 / (n !)) * (z2 #N n)) * z1 by LOPBAN_3:38 .= ((z2 rExpSeq) . n) * z1 by Def2 .= ((z2 rExpSeq) * z1) . n by LOPBAN_3:def_6 ; ::_thesis: verum end; then A2: z1 * (z2 rExpSeq) = (z2 rExpSeq) * z1 by FUNCT_2:63; A3: Partial_Sums (z2 rExpSeq) is convergent by LOPBAN_3:def_1; thus z1 * (exp z2) = z1 * (Sum (z2 rExpSeq)) by Def10 .= lim (z1 * (Partial_Sums (z2 rExpSeq))) by A3, Th6 .= lim (Partial_Sums (z1 * (z2 rExpSeq))) by Th9 .= lim ((Partial_Sums (z2 rExpSeq)) * z1) by A2, Th9 .= (Sum (z2 rExpSeq)) * z1 by A3, Th7 .= (exp z2) * z1 by Def10 ; ::_thesis: verum end; theorem Th37: :: LOPBAN_4:37 for X being Banach_Algebra holds exp (0. X) = 1. X proof let X be Banach_Algebra; ::_thesis: exp (0. X) = 1. X exp (0. X) = Sum ((0. X) rExpSeq) by Def10 .= 1. X by Th20 ; hence exp (0. X) = 1. X ; ::_thesis: verum end; theorem Th38: :: LOPBAN_4:38 for X being Banach_Algebra for z being Element of X holds ( (exp z) * (exp (- z)) = 1. X & (exp (- z)) * (exp z) = 1. X ) proof let X be Banach_Algebra; ::_thesis: for z being Element of X holds ( (exp z) * (exp (- z)) = 1. X & (exp (- z)) * (exp z) = 1. X ) let z be Element of X; ::_thesis: ( (exp z) * (exp (- z)) = 1. X & (exp (- z)) * (exp z) = 1. X ) z * (- z) = z * ((- 1) * z) by LOPBAN_3:38 .= (- 1) * (z * z) by LOPBAN_3:38 .= ((- 1) * z) * z by LOPBAN_3:38 .= (- z) * z by LOPBAN_3:38 ; then A1: z, - z are_commutative by Def1; hence (exp z) * (exp (- z)) = exp (z + (- z)) by Th35 .= exp (0. X) by RLVECT_1:5 .= 1. X by Th37 ; ::_thesis: (exp (- z)) * (exp z) = 1. X thus (exp (- z)) * (exp z) = exp ((- z) + z) by A1, Th35 .= exp (0. X) by RLVECT_1:5 .= 1. X by Th37 ; ::_thesis: verum end; theorem :: LOPBAN_4:39 for X being Banach_Algebra for z being Element of X holds ( exp z is invertible & (exp z) " = exp (- z) & exp (- z) is invertible & (exp (- z)) " = exp z ) proof let X be Banach_Algebra; ::_thesis: for z being Element of X holds ( exp z is invertible & (exp z) " = exp (- z) & exp (- z) is invertible & (exp (- z)) " = exp z ) let z be Element of X; ::_thesis: ( exp z is invertible & (exp z) " = exp (- z) & exp (- z) is invertible & (exp (- z)) " = exp z ) A1: (exp (- z)) * (exp z) = 1. X by Th38; A2: (exp z) * (exp (- z)) = 1. X by Th38; hence exp z is invertible by A1, LOPBAN_3:def_4; ::_thesis: ( (exp z) " = exp (- z) & exp (- z) is invertible & (exp (- z)) " = exp z ) hence (exp z) " = exp (- z) by A2, A1, LOPBAN_3:def_8; ::_thesis: ( exp (- z) is invertible & (exp (- z)) " = exp z ) thus exp (- z) is invertible by A2, A1, LOPBAN_3:def_4; ::_thesis: (exp (- z)) " = exp z hence (exp (- z)) " = exp z by A2, A1, LOPBAN_3:def_8; ::_thesis: verum end; theorem Th40: :: LOPBAN_4:40 for X being Banach_Algebra for z being Element of X for s, t being Real holds s * z,t * z are_commutative proof let X be Banach_Algebra; ::_thesis: for z being Element of X for s, t being Real holds s * z,t * z are_commutative let z be Element of X; ::_thesis: for s, t being Real holds s * z,t * z are_commutative let s, t be Real; ::_thesis: s * z,t * z are_commutative (s * z) * (t * z) = (s * t) * (z * z) by LOPBAN_3:38 .= (t * z) * (s * z) by LOPBAN_3:38 ; hence s * z,t * z are_commutative by Def1; ::_thesis: verum end; theorem :: LOPBAN_4:41 for X being Banach_Algebra for z being Element of X for s, t being Real holds ( (exp (s * z)) * (exp (t * z)) = exp ((s + t) * z) & (exp (t * z)) * (exp (s * z)) = exp ((t + s) * z) & exp ((s + t) * z) = exp ((t + s) * z) & exp (s * z), exp (t * z) are_commutative ) proof let X be Banach_Algebra; ::_thesis: for z being Element of X for s, t being Real holds ( (exp (s * z)) * (exp (t * z)) = exp ((s + t) * z) & (exp (t * z)) * (exp (s * z)) = exp ((t + s) * z) & exp ((s + t) * z) = exp ((t + s) * z) & exp (s * z), exp (t * z) are_commutative ) let z be Element of X; ::_thesis: for s, t being Real holds ( (exp (s * z)) * (exp (t * z)) = exp ((s + t) * z) & (exp (t * z)) * (exp (s * z)) = exp ((t + s) * z) & exp ((s + t) * z) = exp ((t + s) * z) & exp (s * z), exp (t * z) are_commutative ) let s, t be Real; ::_thesis: ( (exp (s * z)) * (exp (t * z)) = exp ((s + t) * z) & (exp (t * z)) * (exp (s * z)) = exp ((t + s) * z) & exp ((s + t) * z) = exp ((t + s) * z) & exp (s * z), exp (t * z) are_commutative ) A1: s * z,t * z are_commutative by Th40; hence A2: (exp (s * z)) * (exp (t * z)) = exp ((s * z) + (t * z)) by Th35 .= exp ((s + t) * z) by LOPBAN_3:38 ; ::_thesis: ( (exp (t * z)) * (exp (s * z)) = exp ((t + s) * z) & exp ((s + t) * z) = exp ((t + s) * z) & exp (s * z), exp (t * z) are_commutative ) thus A3: (exp (t * z)) * (exp (s * z)) = exp ((t * z) + (s * z)) by A1, Th35 .= exp ((t + s) * z) by LOPBAN_3:38 ; ::_thesis: ( exp ((s + t) * z) = exp ((t + s) * z) & exp (s * z), exp (t * z) are_commutative ) thus exp ((s + t) * z) = exp ((t + s) * z) ; ::_thesis: exp (s * z), exp (t * z) are_commutative thus exp (s * z), exp (t * z) are_commutative by A2, A3, Def1; ::_thesis: verum end;