let X be Banach_Algebra; 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; 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; ( z,w are_commutative implies (Partial_Sums ((z + w) rExpSeq)) . n = (Partial_Sums (Alfa (n,z,w))) . n )
assume A1:
z,w are_commutative
; (Partial_Sums ((z + w) rExpSeq)) . n = (Partial_Sums (Alfa (n,z,w))) . n
defpred S1[ Nat] means (Partial_Sums ((z + w) rExpSeq)) . $1 = (Partial_Sums (Alfa ($1,z,w))) . $1;
A2:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A3:
(Partial_Sums ((z + w) rExpSeq)) . k = (Partial_Sums (Alfa (k,z,w))) . k
;
S1[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)
;
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:
S1[ 0 ]
by A5;
for n being Nat holds S1[n]
from NAT_1:sch 2(A7, A2);
hence
(Partial_Sums ((z + w) rExpSeq)) . n = (Partial_Sums (Alfa (n,z,w))) . n
; verum