let z, w be Element of COMPLEX ; 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 ; ( 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:31;
A3:
l <= k + 1
by A1, A2, XXREAL_0:2;
A4:
(k + 1) -' l = (k + 1) - l
by A1, A2, XREAL_1:235, XXREAL_0:2;
A5: (k + 1) -' l =
(k - l) + 1
by A4
.=
(k -' l) + 1
by A1, XREAL_1:235
;
A6: (Alfa (k + 1),z,w) . l =
((z ExpSeq ) . l) * ((Partial_Sums (w ExpSeq )) . ((k -' l) + 1))
by A3, A5, Def15
.=
((z ExpSeq ) . l) * (((Partial_Sums (w ExpSeq )) . (k -' l)) + ((w ExpSeq ) . ((k + 1) -' l)))
by A5, COMSEQ_3:def 7
.=
(((z ExpSeq ) . l) * ((Partial_Sums (w ExpSeq )) . (k -' l))) + (((z ExpSeq ) . l) * ((w ExpSeq ) . ((k + 1) -' l)))
.=
((Alfa k,z,w) . l) + (((z ExpSeq ) . l) * ((w ExpSeq ) . ((k + 1) -' l)))
by A1, Def15
;
A7: ((z ExpSeq ) . l) * ((w ExpSeq ) . ((k + 1) -' l)) =
((z |^ l) / (l !c )) * ((w ExpSeq ) . ((k + 1) -' l))
by Def8
.=
((z |^ l) / (l !c )) * ((w |^ ((k + 1) -' l)) / (((k + 1) -' l) !c ))
by Def8
.=
(((z |^ l) * (w |^ ((k + 1) -' l))) * 1r ) / ((l !c ) * (((k + 1) -' l) !c ))
by XCMPLX_1:77
.=
((z |^ l) * (w |^ ((k + 1) -' l))) * (1r / ((l !c ) * (((k + 1) -' l) !c )))
.=
((Coef_e (k + 1)) . l) * ((z |^ l) * (w |^ ((k + 1) -' l)))
by A3, Def11
.=
(((Coef_e (k + 1)) . l) * (z |^ l)) * (w |^ ((k + 1) -' l))
.=
(Expan_e (k + 1),z,w) . l
by A3, Def14
;
thus
(Alfa (k + 1),z,w) . l = ((Alfa k,z,w) . l) + ((Expan_e (k + 1),z,w) . l)
by A6, A7; verum