let X be Banach_Algebra; :: thesis: ( (0. X) rExpSeq is norm_summable & Sum ((0. X) rExpSeq ) = 1. X )
defpred S₁[ set ] means (Partial_Sums ||.((0. X) rExpSeq ).||) . $1 = 1;
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: (Partial_Sums ||.((0. X) rExpSeq ).||) . n = 1 ; :: thesis: S₁[n + 1]
A3: n in NAT by ORDINAL1:def 13;
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:43
.= 1 + ||.(0. X).|| by LOPBAN_3:43
.= 1 + 0 by LOPBAN_3:43
.= 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:43 ;
then A4: S₁[ 0 ] ;
A5: for n being Nat holds S₁[n] from NAT_1:sch 2(A4, A1);
Partial_Sums ||.((0. X) rExpSeq ).|| is constant

proof

take 1 ; :: according to VALUED_0:def 18 :: thesis: for b₁ being set holds (Partial_Sums ||.((0. X) rExpSeq ).||) . b₁ = 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 S₂[ set ] means (Partial_Sums ((0. X) rExpSeq )) . $1 = 1. X;
A7: 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 (Partial_Sums ((0. X) rExpSeq )) . n = 1. X ; :: thesis: S₂[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:43
.= (1. X) + (0. X) by LOPBAN_3:43
.= 1. X by LOPBAN_3:43 ;
:: thesis: verum

end;

(Partial_Sums ((0. X) rExpSeq )) . 0 = ((0. X) rExpSeq ) . 0 by BHSP_4:def 1
.= 1. X by Th14 ;
then A8: S₂[ 0 ] ;
for n being Element of NAT holds S₂[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 4; :: thesis: verum