:: The Exponential Function on {B}anach Algebra
:: by Yasunari Shidama
::
:: Received February 13, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users


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 )
proofend;

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 )
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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)
proofend;

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
proofend;

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)
proofend;

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 )
proofend;

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
proofend;

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
proofend;

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 ) &amp; rseq is convergent &amp; lim rseq = 0 holds
( seq is convergent &amp; lim seq = 0. X )
proofend;

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)
proofend;
uniqueness
 for b1, b2 being sequence of X st ( for n being Element of NAT holds b1 . n = (1 / (n !)) * (z #N n) ) &amp; ( for n being Element of NAT holds b2 . n = (1 / (n !)) * (z #N n) ) holds
b1 = b2
proofend;
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) ) &amp; ( n > k implies seq . n = 0. F1() ) )
proofend;

theorem Th13: :: LOPBAN_4:13
( ( for k being Element of NAT st 0 < k holds
((k -' 1) !) * k = k ! ) &amp; ( for m, k being Element of NAT st k <= m holds
((m -' k) !) * ((m + 1) - k) = ((m + 1) -' k) ! ) )
proofend;

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) !)) ) &amp; ( 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) !)) ) &amp; ( k > n implies b1 . k = 0 ) )
proofend;
uniqueness
 for b1, b2 being Real_Sequence st ( for k being Element of NAT holds
( ( k <= n implies b1 . k = (n !) / ((k !) * ((n -' k) !)) ) &amp; ( k > n implies b1 . k = 0 ) ) ) &amp; ( for k being Element of NAT holds
( ( k <= n implies b2 . k = (n !) / ((k !) * ((n -' k) !)) ) &amp; ( k > n implies b2 . k = 0 ) ) ) holds
b1 = b2
proofend;
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) !)) ) &amp; ( 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) !)) ) &amp; ( 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) !)) ) &amp; ( k > n implies b1 . k = 0 ) )
proofend;
uniqueness
 for b1, b2 being Real_Sequence st ( for k being Element of NAT holds
( ( k <= n implies b1 . k = 1 / ((k !) * ((n -' k) !)) ) &amp; ( k > n implies b1 . k = 0 ) ) ) &amp; ( for k being Element of NAT holds
( ( k <= n implies b2 . k = 1 / ((k !) * ((n -' k) !)) ) &amp; ( k > n implies b2 . k = 0 ) ) ) holds
b1 = b2
proofend;
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) !)) ) &amp; ( 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 &amp; ( for k being Element of NAT holds it . (k + 1) = seq . k ) );
existence
 ex b1 being sequence of X st
( b1 . 0 = 0. X &amp; ( for k being Element of NAT holds b1 . (k + 1) = seq . k ) )
proofend;
uniqueness
 for b1, b2 being sequence of X st b1 . 0 = 0. X &amp; ( for k being Element of NAT holds b1 . (k + 1) = seq . k ) &amp; b2 . 0 = 0. X &amp; ( for k being Element of NAT holds b2 . (k + 1) = seq . k ) holds
b1 = b2
proofend;
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 &amp; ( 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)) ) &amp; ( 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)) ) &amp; ( n < k implies b1 . k = 0. X ) )
proofend;
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)) ) &amp; ( n < k implies b1 . k = 0. X ) ) ) &amp; ( for k being Element of NAT holds
( ( k <= n implies b2 . k = (((Coef n) . k) * (z #N k)) * (w #N (n -' k)) ) &amp; ( n < k implies b2 . k = 0. X ) ) ) holds
b1 = b2
proofend;
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)) ) &amp; ( 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)) ) &amp; ( 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)) ) &amp; ( n < k implies b1 . k = 0. X ) )
proofend;
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)) ) &amp; ( n < k implies b1 . k = 0. X ) ) ) &amp; ( for k being Element of NAT holds
( ( k <= n implies b2 . k = (((Coef_e n) . k) * (z #N k)) * (w #N (n -' k)) ) &amp; ( n < k implies b2 . k = 0. X ) ) ) holds
b1 = b2
proofend;
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)) ) &amp; ( 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)) ) &amp; ( 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)) ) &amp; ( n < k implies b1 . k = 0. X ) )
proofend;
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)) ) &amp; ( n < k implies b1 . k = 0. X ) ) ) &amp; ( for k being Element of NAT holds
( ( k <= n implies b2 . k = ((z rExpSeq) . k) * ((Partial_Sums (w rExpSeq)) . (n -' k)) ) &amp; ( n < k implies b2 . k = 0. X ) ) ) holds
b1 = b2
proofend;
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)) ) &amp; ( 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))) ) &amp; ( 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))) ) &amp; ( n < k implies b1 . k = 0. X ) )
proofend;
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))) ) &amp; ( n < k implies b1 . k = 0. X ) ) ) &amp; ( 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))) ) &amp; ( n < k implies b2 . k = 0. X ) ) ) holds
b1 = b2
proofend;
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))) ) &amp; ( 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) &amp; (z rExpSeq) . 0 = 1. X &amp; ||.((z rExpSeq) . n).|| <= (||.z.|| rExpSeq) . n )
proofend;

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)
proofend;

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)
proofend;

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
proofend;

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))
proofend;

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
proofend;

theorem Th20: :: LOPBAN_4:20
for X being Banach_Algebra holds
( (0. X) rExpSeq is norm_summable &amp; Sum ((0. X) rExpSeq) = 1. X )
proofend;

registration
let X be Banach_Algebra;
let z be Element of X;
clusterz rExpSeq  ->  norm_summable ;
coherence
 z rExpSeq is norm_summable
proofend;
end;

theorem Th21: :: LOPBAN_4:21
for X being Banach_Algebra
for z, w being Element of X holds
( (z rExpSeq) . 0 = 1. X &amp; (Expan (0,z,w)) . 0 = 1. X )
proofend;

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)
proofend;

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)
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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 &amp; (Partial_Sums (||.z.|| rExpSeq)) . k <= Sum (||.z.|| rExpSeq) &amp; ||.((Partial_Sums (z rExpSeq)) . k).|| <= Sum (||.z.|| rExpSeq) )
proofend;

theorem Th29: :: LOPBAN_4:29
for X being Banach_Algebra
for z being Element of X holds 1 <= Sum (||.z.|| rExpSeq)
proofend;

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 &amp; ( n <= m implies abs (((Partial_Sums (||.z.|| rExpSeq)) . m) - ((Partial_Sums (||.z.|| rExpSeq)) . n)) = ((Partial_Sums (||.z.|| rExpSeq)) . m) - ((Partial_Sums (||.z.|| rExpSeq)) . n) ) )
proofend;

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
proofend;

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
proofend;

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 &amp; lim seq = 0. X )
proofend;

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)
proofend;

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)
proofend;
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) ) &amp; ( for z being Element of X holds b2 . z = Sum (z rExpSeq) ) holds
b1 = b2
proofend;
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) &amp; exp (z2 + z1) = (exp z2) * (exp z1) &amp; exp (z1 + z2) = exp (z2 + z1) &amp; exp z1, exp z2 are_commutative )
proofend;

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
proofend;

theorem Th37: :: LOPBAN_4:37
for X being Banach_Algebra holds exp (0. X) = 1. X
proofend;

theorem Th38: :: LOPBAN_4:38
for X being Banach_Algebra
for z being Element of X holds
( (exp z) * (exp (- z)) = 1. X &amp; (exp (- z)) * (exp z) = 1. X )
proofend;

theorem :: LOPBAN_4:39
for X being Banach_Algebra
for z being Element of X holds
( exp z is invertible &amp; (exp z) " = exp (- z) &amp; exp (- z) is invertible &amp; (exp (- z)) " = exp z )
proofend;

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
proofend;

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) &amp; (exp (t * z)) * (exp (s * z)) = exp ((t + s) * z) &amp; exp ((s + t) * z) = exp ((t + s) * z) &amp; exp (s * z), exp (t * z) are_commutative )
proofend;