let X be Complex_Banach_Algebra; :: thesis: ( (0. X) ExpSeq is norm_summable & Sum ((0. X) ExpSeq) = 1. X )

reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

defpred S_{1}[ set ] means (Partial_Sums ||.((0. X) ExpSeq).||) . $1 = jj;

A1: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]

.= ||.(((0. X) ExpSeq) . 0).|| by NORMSP_0:def 4

.= ||.(1. X).|| by Th13

.= 1 by CLOPBAN3:38 ;

then A3: S_{1}[ 0 ]
;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A3, A1);

then Partial_Sums ||.((0. X) ExpSeq).|| is constant by VALUED_0:def 18;

then A4: ||.((0. X) ExpSeq).|| is summable by SERIES_1:def 2;

defpred S_{2}[ set ] means (Partial_Sums ((0. X) ExpSeq)) . $1 = 1. X;

A5: for n being Nat st S_{2}[n] holds

S_{2}[n + 1]

.= 1. X by Th13 ;

then A6: S_{2}[ 0 ]
;

for n being Nat holds S_{2}[n]
from NAT_1:sch 2(A6, A5);

then lim (Partial_Sums ((0. X) ExpSeq)) = 1. X by Th2;

hence ( (0. X) ExpSeq is norm_summable & Sum ((0. X) ExpSeq) = 1. X ) by A4, CLOPBAN3:def 2, CLOPBAN3:def 3; :: thesis: verum

reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

defpred S

A1: for n being Nat st S

S

proof

(Partial_Sums ||.((0. X) ExpSeq).||) . 0 =
||.((0. X) ExpSeq).|| . 0
by SERIES_1:def 1
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A2: (Partial_Sums ||.((0. X) ExpSeq).||) . n = jj ; :: thesis: S_{1}[n + 1]

thus (Partial_Sums ||.((0. X) ExpSeq).||) . (n + 1) = 1 + (||.((0. X) ExpSeq).|| . (n + 1)) by A2, SERIES_1:def 1

.= 1 + ||.(((0. X) ExpSeq) . (n + 1)).|| by NORMSP_0:def 4

.= 1 + ||.(((1r / (n + 1)) * (0. X)) * (((0. X) ExpSeq) . n)).|| by Th13

.= 1 + ||.((0. X) * (((0. X) ExpSeq) . n)).|| by CLVECT_1:1

.= 1 + ||.(0. X).|| by CLOPBAN3:38

.= 1 + 0 by CLOPBAN3:38

.= jj ; :: thesis: verum

end;assume A2: (Partial_Sums ||.((0. X) ExpSeq).||) . n = jj ; :: thesis: S

thus (Partial_Sums ||.((0. X) ExpSeq).||) . (n + 1) = 1 + (||.((0. X) ExpSeq).|| . (n + 1)) by A2, SERIES_1:def 1

.= 1 + ||.(((0. X) ExpSeq) . (n + 1)).|| by NORMSP_0:def 4

.= 1 + ||.(((1r / (n + 1)) * (0. X)) * (((0. X) ExpSeq) . n)).|| by Th13

.= 1 + ||.((0. X) * (((0. X) ExpSeq) . n)).|| by CLVECT_1:1

.= 1 + ||.(0. X).|| by CLOPBAN3:38

.= 1 + 0 by CLOPBAN3:38

.= jj ; :: thesis: verum

.= ||.(((0. X) ExpSeq) . 0).|| by NORMSP_0:def 4

.= ||.(1. X).|| by Th13

.= 1 by CLOPBAN3:38 ;

then A3: S

for n being Nat holds S

then Partial_Sums ||.((0. X) ExpSeq).|| is constant by VALUED_0:def 18;

then A4: ||.((0. X) ExpSeq).|| is summable by SERIES_1:def 2;

defpred S

A5: for n being Nat st S

S

proof

(Partial_Sums ((0. X) ExpSeq)) . 0 =
((0. X) ExpSeq) . 0
by BHSP_4:def 1
let n be Nat; :: thesis: ( S_{2}[n] implies S_{2}[n + 1] )

assume (Partial_Sums ((0. X) ExpSeq)) . n = 1. X ; :: thesis: S_{2}[n + 1]

hence (Partial_Sums ((0. X) ExpSeq)) . (n + 1) = (1. X) + (((0. X) ExpSeq) . (n + 1)) by BHSP_4:def 1

.= (1. X) + (((1r / (n + 1)) * (0. X)) * (((0. X) ExpSeq) . n)) by Th13

.= (1. X) + ((0. X) * (((0. X) ExpSeq) . n)) by CLVECT_1:1

.= (1. X) + (0. X) by CLOPBAN3:38

.= 1. X by RLVECT_1:def 4 ;

:: thesis: verum

end;assume (Partial_Sums ((0. X) ExpSeq)) . n = 1. X ; :: thesis: S

hence (Partial_Sums ((0. X) ExpSeq)) . (n + 1) = (1. X) + (((0. X) ExpSeq) . (n + 1)) by BHSP_4:def 1

.= (1. X) + (((1r / (n + 1)) * (0. X)) * (((0. X) ExpSeq) . n)) by Th13

.= (1. X) + ((0. X) * (((0. X) ExpSeq) . n)) by CLVECT_1:1

.= (1. X) + (0. X) by CLOPBAN3:38

.= 1. X by RLVECT_1:def 4 ;

:: thesis: verum

.= 1. X by Th13 ;

then A6: S

for n being Nat holds S

then lim (Partial_Sums ((0. X) ExpSeq)) = 1. X by Th2;

hence ( (0. X) ExpSeq is norm_summable & Sum ((0. X) ExpSeq) = 1. X ) by A4, CLOPBAN3:def 2, CLOPBAN3:def 3; :: thesis: verum