let X be Complex_Banach_Algebra; :: thesis: for z, w being Element of X
for n being Element of NAT holds Expan_e n,z,w = (1r / (n !c )) * (Expan n,z,w)
let z, w be Element of X; :: thesis: for n being Element of NAT holds Expan_e n,z,w = (1r / (n !c )) * (Expan n,z,w)
let n be Element of NAT ; :: thesis: Expan_e n,z,w = (1r / (n !c )) * (Expan n,z,w)

now

let k be Element of NAT ; :: thesis: (Expan_e n,z,w) . k = ((1r / (n !c )) * (Expan n,z,w)) . k

A1: now

A2: 1r / ((k !c ) * ((n -' k) !c )) = (((n !c ) * 1r ) / (n !c )) / ((k !c ) * ((n -' k) !c )) by COMPLEX1:def 7, SIN_COS:1, XCMPLX_1:60
.= ((1r / (n !c )) * (n !c )) / ((k !c ) * ((n -' k) !c )) by XCMPLX_1:75 ;
assume A3: k <= n ; :: thesis: ( (Expan_e n,z,w) . k = ((1r / ((k !c ) * ((n -' k) !c ))) * (z #N k)) * (w #N (n -' k)) & (Expan_e n,z,w) . k = ((1r / (n !c )) * (Expan n,z,w)) . k )
hence (Expan_e n,z,w) . k = (((Coef_e n) . k) * (z #N k)) * (w #N (n -' k)) by Def5
.= ((1r / ((k !c ) * ((n -' k) !c ))) * (z #N k)) * (w #N (n -' k)) by A3, SIN_COS:def 11 ;
:: thesis: (Expan_e n,z,w) . k = ((1r / (n !c )) * (Expan n,z,w)) . k
hence (Expan_e n,z,w) . k = (((1r / (n !c )) * (n !c )) / ((k !c ) * ((n -' k) !c ))) * ((z #N k) * (w #N (n -' k))) by A2, CLOPBAN3:42
.= ((1r / (n !c )) * ((n !c ) / ((k !c ) * ((n -' k) !c )))) * ((z #N k) * (w #N (n -' k))) by XCMPLX_1:75
.= (1r / (n !c )) * (((n !c ) / ((k !c ) * ((n -' k) !c ))) * ((z #N k) * (w #N (n -' k)))) by CLOPBAN3:42
.= (1r / (n !c )) * ((((n !c ) / ((k !c ) * ((n -' k) !c ))) * (z #N k)) * (w #N (n -' k))) by CLOPBAN3:42
.= (1r / (n !c )) * ((((Coef n) . k) * (z #N k)) * (w #N (n -' k))) by A3, SIN_COS:def 10
.= (1r / (n !c )) * ((Expan n,z,w) . k) by A3, Def4
.= ((1r / (n !c )) * (Expan n,z,w)) . k by CLVECT_1:def 15 ;
:: thesis: verum

end;

now

assume A4: n < k ; :: thesis: (Expan_e n,z,w) . k = ((1r / (n !c )) * (Expan n,z,w)) . k
hence (Expan_e n,z,w) . k = 0. X by Def5
.= (1r / (n !c )) * (0. X) by CLOPBAN3:42
.= (1r / (n !c )) * ((Expan n,z,w) . k) by A4, Def4
.= ((1r / (n !c )) * (Expan n,z,w)) . k by CLVECT_1:def 15 ;
:: thesis: verum

end;

hence (Expan_e n,z,w) . k = ((1r / (n !c )) * (Expan n,z,w)) . k by A1; :: thesis: verum

end;

hence Expan_e n,z,w = (1r / (n !c )) * (Expan n,z,w) by FUNCT_2:113; :: thesis: verum