let X be Complex_Banach_Algebra; :: thesis: for z, w being Element of X
for l, k being Element of NAT st l <= k holds
(Alfa (k + 1),z,w) . l = ((Alfa k,z,w) . l) + ((Expan_e (k + 1),z,w) . l)
let z, w be Element of X; :: thesis: for l, k being Element of NAT st l <= k holds
(Alfa (k + 1),z,w) . l = ((Alfa k,z,w) . l) + ((Expan_e (k + 1),z,w) . l)
let l, k be Element of 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:31;
then A3: l <= k + 1 by A1, XXREAL_0:2;
(k + 1) -' l = (k + 1) - l by A1, A2, XREAL_1:235, XXREAL_0:2;
then A4: (k + 1) -' l = (k - l) + 1
.= (k -' l) + 1 by A1, XREAL_1:235 ;
then A5: (Alfa (k + 1),z,w) . l = ((z ExpSeq ) . l) * ((Partial_Sums (w ExpSeq )) . ((k -' l) + 1)) by A3, Def6
.= ((z ExpSeq ) . l) * (((Partial_Sums (w ExpSeq )) . (k -' l)) + ((w ExpSeq ) . ((k + 1) -' l))) by A4, BHSP_4:def 1
.= (((z ExpSeq ) . l) * ((Partial_Sums (w ExpSeq )) . (k -' l))) + (((z ExpSeq ) . l) * ((w ExpSeq ) . ((k + 1) -' l))) by CLOPBAN3:42
.= ((Alfa k,z,w) . l) + (((z ExpSeq ) . l) * ((w ExpSeq ) . ((k + 1) -' l))) by A1, Def6 ;
((z ExpSeq ) . l) * ((w ExpSeq ) . ((k + 1) -' l)) = ((1r / (l !c )) * (z #N l)) * ((w ExpSeq ) . ((k + 1) -' l)) by Def2
.= ((1r / (l !c )) * (z #N l)) * ((1r / (((k + 1) -' l) !c )) * (w #N ((k + 1) -' l))) by Def2
.= ((1r / (l !c )) * (1r / (((k + 1) -' l) !c ))) * ((z #N l) * (w #N ((k + 1) -' l))) by CLOPBAN3:42
.= ((1r * 1r ) / ((l !c ) * (((k + 1) -' l) !c ))) * ((z #N l) * (w #N ((k + 1) -' l))) by XCMPLX_1:77
.= ((Coef_e (k + 1)) . l) * ((z #N l) * (w #N ((k + 1) -' l))) by A3, COMPLEX1:def 7, SIN_COS:def 11
.= (((Coef_e (k + 1)) . l) * (z #N l)) * (w #N ((k + 1) -' l)) by CLOPBAN3:42
.= (Expan_e (k + 1),z,w) . l by A3, Def5 ;
hence (Alfa (k + 1),z,w) . l = ((Alfa k,z,w) . l) + ((Expan_e (k + 1),z,w) . l) by A5; :: thesis: verum