let X be Banach_Algebra; :: thesis: for n being Element of 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 Element of 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
A2: (Partial_Sums ((z + w) rExpSeq )) . 0 =
((z + w) rExpSeq ) . 0
by BHSP_4:def 1
.=
1. X
by Th21
;
defpred S1[ Element of NAT ] means (Partial_Sums ((z + w) rExpSeq )) . $1 = (Partial_Sums (Alfa $1,z,w)) . $1;
A3:
0 -' 0 = 0
by XREAL_1:234;
(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 A3, 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:43
;
then A4:
S1[ 0 ]
by A2;
A5:
for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be
Element of
NAT ;
:: thesis: ( S1[k] implies S1[k + 1] )
assume A6:
(Partial_Sums ((z + w) rExpSeq )) . k = (Partial_Sums (Alfa k,z,w)) . k
;
:: thesis: S1[k + 1]
thus
(Partial_Sums ((z + w) rExpSeq )) . (k + 1) = (Partial_Sums (Alfa (k + 1),z,w)) . (k + 1)
:: thesis: verumproof
A7:
(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 A6, LOPBAN_3:43
;
(k + 1) -' (k + 1) = 0
by XREAL_1:234;
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:43
.=
(Expan_e (k + 1),z,w) . (k + 1)
by Th24
;
then ((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
;
hence (Partial_Sums (Alfa (k + 1),z,w)) . (k + 1) =
((Partial_Sums ((z + w) rExpSeq )) . k) + (((z + w) rExpSeq ) . (k + 1))
by A7, Def2
.=
(Partial_Sums ((z + w) rExpSeq )) . (k + 1)
by BHSP_4:def 1
;
:: thesis: verum
end;
end;
for n being Element of NAT holds S1[n]
from NAT_1:sch 1(A4, A5);
hence
(Partial_Sums ((z + w) rExpSeq )) . n = (Partial_Sums (Alfa n,z,w)) . n
; :: thesis: verum