let X be Complex_Banach_Algebra; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: (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 ExpSeq) . l) * ((w ExpSeq) . ((k + 1) -' l)) = ((1r / (l !)) * (z #N l)) * ((w ExpSeq) . ((k + 1) -' l)) by Def1
.= ((1r / (l !)) * (z #N l)) * ((1r / (((k + 1) -' l) !)) * (w #N ((k + 1) -' l))) by Def1
.= ((1r / (l !)) * (1r / (((k + 1) -' l) !))) * ((z #N l) * (w #N ((k + 1) -' l))) by CLOPBAN3:38
.= ((1r * 1r) / ((l !) * (((k + 1) -' l) !))) * ((z #N l) * (w #N ((k + 1) -' l))) by XCMPLX_1:76
.= ((Coef_e (k + 1)) . l) * ((z #N l) * (w #N ((k + 1) -' l))) by A3, COMPLEX1:def 4, SIN_COS:def 7
.= (((Coef_e (k + 1)) . l) * (z #N l)) * (w #N ((k + 1) -' l)) by CLOPBAN3:38
.= (Expan_e ((k + 1),z,w)) . l by A3, Def3 ;
(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 ExpSeq) . l) * ((Partial_Sums (w ExpSeq)) . ((k -' l) + 1)) by A3, Def4
.= ((z ExpSeq) . l) * (((Partial_Sums (w ExpSeq)) . (k -' l)) + ((w ExpSeq) . ((k + 1) -' l))) by A5, BHSP_4:def 1
.= (((z ExpSeq) . l) * ((Partial_Sums (w ExpSeq)) . (k -' l))) + (((z ExpSeq) . l) * ((w ExpSeq) . ((k + 1) -' l))) by VECTSP_1:def 2
.= ((Alfa (k,z,w)) . l) + (((z ExpSeq) . l) * ((w ExpSeq) . ((k + 1) -' l))) by A1, Def4 ;
hence (Alfa ((k + 1),z,w)) . l = ((Alfa (k,z,w)) . l) + ((Expan_e ((k + 1),z,w)) . l) by A4; :: thesis: verum