let X be Banach_Algebra; :: thesis: for n being 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
let n be Nat; :: thesis: 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
let z, w be Element of X; :: thesis: ( z,w are_commutative implies (Partial_Sums ((z + w) rExpSeq)) . n = (Partial_Sums (Alfa (n,z,w))) . n )
assume A1: z,w are_commutative ; :: thesis: (Partial_Sums ((z + w) rExpSeq)) . n = (Partial_Sums (Alfa (n,z,w))) . n
defpred S₁[ Nat] means (Partial_Sums ((z + w) rExpSeq)) . $1 = (Partial_Sums (Alfa ($1,z,w))) . $1;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: (Partial_Sums ((z + w) rExpSeq)) . k = (Partial_Sums (Alfa (k,z,w))) . k ; :: thesis: S₁[k + 1]
(k + 1) -' (k + 1) = 0 by XREAL_1:232;
then (Alfa ((k + 1),z,w)) . (k + 1) = ((z rExpSeq) . (k + 1)) * ((Partial_Sums (w rExpSeq)) . 0) by Def8
.= ((z rExpSeq) . (k + 1)) * ((w rExpSeq) . 0) by BHSP_4:def 1
.= ((z rExpSeq) . (k + 1)) * (1. X) by Th21
.= (z rExpSeq) . (k + 1) by LOPBAN_3:38
.= (Expan_e ((k + 1),z,w)) . (k + 1) by Th24 ;
then A4: ((Partial_Sums (Expan_e ((k + 1),z,w))) . k) + ((Alfa ((k + 1),z,w)) . (k + 1)) = (Partial_Sums (Expan_e ((k + 1),z,w))) . (k + 1) by BHSP_4:def 1
.= (1 / ((k + 1) !)) * ((z + w) #N (k + 1)) by A1, Th19 ;
(Partial_Sums (Alfa ((k + 1),z,w))) . (k + 1) = ((Partial_Sums (Alfa ((k + 1),z,w))) . k) + ((Alfa ((k + 1),z,w)) . (k + 1)) by BHSP_4:def 1
.= (((Partial_Sums (Alfa (k,z,w))) . k) + ((Partial_Sums (Expan_e ((k + 1),z,w))) . k)) + ((Alfa ((k + 1),z,w)) . (k + 1)) by Th23
.= ((Partial_Sums ((z + w) rExpSeq)) . k) + (((Partial_Sums (Expan_e ((k + 1),z,w))) . k) + ((Alfa ((k + 1),z,w)) . (k + 1))) by A3, LOPBAN_3:38 ;
then (Partial_Sums (Alfa ((k + 1),z,w))) . (k + 1) = ((Partial_Sums ((z + w) rExpSeq)) . k) + (((z + w) rExpSeq) . (k + 1)) by A4, Def2
.= (Partial_Sums ((z + w) rExpSeq)) . (k + 1) by BHSP_4:def 1 ;
hence (Partial_Sums ((z + w) rExpSeq)) . (k + 1) = (Partial_Sums (Alfa ((k + 1),z,w))) . (k + 1) ; :: thesis: verum

end;

A5: (Partial_Sums ((z + w) rExpSeq)) . 0 = ((z + w) rExpSeq) . 0 by BHSP_4:def 1
.= 1. X by Th21 ;
A6: 0 -' 0 = 0 by XREAL_1:232;
(Partial_Sums (Alfa (0,z,w))) . 0 = (Alfa (0,z,w)) . 0 by BHSP_4:def 1
.= ((z rExpSeq) . 0) * ((Partial_Sums (w rExpSeq)) . 0) by A6, Def8
.= ((z rExpSeq) . 0) * ((w rExpSeq) . 0) by BHSP_4:def 1
.= (1. X) * ((w rExpSeq) . 0) by Th21
.= (1. X) * (1. X) by Th21
.= 1. X by LOPBAN_3:38 ;
then A7: S₁[ 0 ] by A5;
for n being Nat holds S₁[n] from NAT_1:sch 2(A7, A2);
hence (Partial_Sums ((z + w) rExpSeq)) . n = (Partial_Sums (Alfa (n,z,w))) . n ; :: thesis: verum