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 S1[ set ] means (Partial_Sums ||.((0. X) ExpSeq).||) . $1 = jj;
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) ExpSeq).||) . n = jj ; :: thesis: S1[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;
(Partial_Sums ||.((0. X) ExpSeq).||) . 0 = ||.((0. X) ExpSeq).|| . 0 by SERIES_1:def 1
.= ||.(((0. X) ExpSeq) . 0).|| by NORMSP_0:def 4
.= ||.(1. X).|| by Th13
.= 1 by CLOPBAN3:38 ;
then A3: S1[ 0 ] ;
for n being Nat holds S1[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 S2[ set ] means (Partial_Sums ((0. X) ExpSeq)) . $1 = 1. X;
A5: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume (Partial_Sums ((0. X) ExpSeq)) . n = 1. X ; :: thesis: S2[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;
(Partial_Sums ((0. X) ExpSeq)) . 0 = ((0. X) ExpSeq) . 0 by BHSP_4:def 1
.= 1. X by Th13 ;
then A6: S2[ 0 ] ;
for n being Nat holds S2[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