let X be Banach_Algebra; for w, z being Element of X
for k, l being Nat st l <= k holds
(Alfa ((k + 1),z,w)) . l = ((Alfa (k,z,w)) . l) + ((Expan_e ((k + 1),z,w)) . l)
let w, z be Element of X; for k, l being Nat st l <= k holds
(Alfa ((k + 1),z,w)) . l = ((Alfa (k,z,w)) . l) + ((Expan_e ((k + 1),z,w)) . l)
let k, l be Nat; ( l <= k implies (Alfa ((k + 1),z,w)) . l = ((Alfa (k,z,w)) . l) + ((Expan_e ((k + 1),z,w)) . l) )
assume A1:
l <= k
; (Alfa ((k + 1),z,w)) . l = ((Alfa (k,z,w)) . l) + ((Expan_e ((k + 1),z,w)) . l)
A2:
k < k + 1
by XREAL_1:29;
then A3:
l <= k + 1
by A1, XXREAL_0:2;
A4: ((z rExpSeq) . l) * ((w rExpSeq) . ((k + 1) -' l)) =
((1 / (l !)) * (z #N l)) * ((w rExpSeq) . ((k + 1) -' l))
by Def2
.=
((1 / (l !)) * (z #N l)) * ((1 / (((k + 1) -' l) !)) * (w #N ((k + 1) -' l)))
by Def2
.=
((1 / (l !)) * (1 / (((k + 1) -' l) !))) * ((z #N l) * (w #N ((k + 1) -' l)))
by LOPBAN_3:38
.=
(1 / ((l !) * (((k + 1) -' l) !))) * ((z #N l) * (w #N ((k + 1) -' l)))
by XCMPLX_1:102
.=
((Coef_e (k + 1)) . l) * ((z #N l) * (w #N ((k + 1) -' l)))
by A3, Def4
.=
(((Coef_e (k + 1)) . l) * (z #N l)) * (w #N ((k + 1) -' l))
by LOPBAN_3:38
.=
(Expan_e ((k + 1),z,w)) . l
by A3, Def7
;
(k + 1) -' l = (k + 1) - l
by A1, A2, XREAL_1:233, XXREAL_0:2;
then A5: (k + 1) -' l =
(k - l) + 1
.=
(k -' l) + 1
by A1, XREAL_1:233
;
then (Alfa ((k + 1),z,w)) . l =
((z rExpSeq) . l) * ((Partial_Sums (w rExpSeq)) . ((k -' l) + 1))
by A3, Def8
.=
((z rExpSeq) . l) * (((Partial_Sums (w rExpSeq)) . (k -' l)) + ((w rExpSeq) . ((k + 1) -' l)))
by A5, BHSP_4:def 1
.=
(((z rExpSeq) . l) * ((Partial_Sums (w rExpSeq)) . (k -' l))) + (((z rExpSeq) . l) * ((w rExpSeq) . ((k + 1) -' l)))
by LOPBAN_3:38
.=
((Alfa (k,z,w)) . l) + (((z rExpSeq) . l) * ((w rExpSeq) . ((k + 1) -' l)))
by A1, Def8
;
hence
(Alfa ((k + 1),z,w)) . l = ((Alfa (k,z,w)) . l) + ((Expan_e ((k + 1),z,w)) . l)
by A4; verum