let X be Complex_Banach_Algebra; :: thesis: ( (0. X) ExpSeq is norm_summable & Sum ((0. X) ExpSeq ) = 1. X )
defpred S₁[ set ] means (Partial_Sums ||.((0. X) ExpSeq ).||) . $1 = 1;
(Partial_Sums ||.((0. X) ExpSeq ).||) . 0 = ||.((0. X) ExpSeq ).|| . 0 by SERIES_1:def 1
.= ||.(((0. X) ExpSeq ) . 0 ).|| by CLVECT_1:def 17
.= ||.(1. X).|| by Th13
.= 1 by CLOPBAN3:42 ;
then A1: S₁[ 0 ] ;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: (Partial_Sums ||.((0. X) ExpSeq ).||) . n = 1 ; :: thesis: S₁[n + 1]
X: n in NAT by ORDINAL1:def 13;
thus (Partial_Sums ||.((0. X) ExpSeq ).||) . (n + 1) = 1 + (||.((0. X) ExpSeq ).|| . (n + 1)) by A3, X, SERIES_1:def 1
.= 1 + ||.(((0. X) ExpSeq ) . (n + 1)).|| by CLVECT_1:def 17
.= 1 + ||.(((1r / (n + 1)) * (0. X)) * (((0. X) ExpSeq ) . n)).|| by Th13, X
.= 1 + ||.((0. X) * (((0. X) ExpSeq ) . n)).|| by CLOPBAN3:42
.= 1 + ||.(0. X).|| by CLOPBAN3:42
.= 1 + 0 by CLOPBAN3:42
.= 1 ; :: thesis: verum

end;

A4: (0. X) ExpSeq is norm_summable

proof

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
then Partial_Sums ||.((0. X) ExpSeq ).|| is constant by VALUED_0:def 18;
then Partial_Sums ||.((0. X) ExpSeq ).|| is convergent ;
then ||.((0. X) ExpSeq ).|| is summable by SERIES_1:def 2;
hence (0. X) ExpSeq is norm_summable by CLOPBAN3:def 4; :: thesis: verum

end;

defpred S₂[ set ] means (Partial_Sums ((0. X) ExpSeq )) . $1 = 1. X;
(Partial_Sums ((0. X) ExpSeq )) . 0 = ((0. X) ExpSeq ) . 0 by BHSP_4:def 1
.= 1. X by Th13 ;
then A5: S₂[ 0 ] ;
A6: for n being Element of NAT st S₂[n] holds
S₂[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume A7: (Partial_Sums ((0. X) ExpSeq )) . n = 1. X ; :: thesis: S₂[n + 1]
thus (Partial_Sums ((0. X) ExpSeq )) . (n + 1) = (1. X) + (((0. X) ExpSeq ) . (n + 1)) by A7, 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 CLOPBAN3:42
.= (1. X) + (0. X) by CLOPBAN3:42
.= 1. X by CLOPBAN3:42 ; :: thesis: verum

end;

for n being Element of NAT holds S₂[n] from NAT_1:sch 1(A5, A6);
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 3; :: thesis: verum