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

now :: thesis: for k being Element of NAT holds (Expan_e (n,z,w)) . k = ((1r / (n !)) * (Expan (n,z,w))) . k

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

A1: now :: thesis: ( k <= n implies ( (Expan_e (n,z,w)) . k = ((1r / ((k !) * ((n -' k) !))) * (z #N k)) * (w #N (n -' k)) & (Expan_e (n,z,w)) . k = ((1r / (n !)) * (Expan (n,z,w))) . k ) )

reconsider s = n ! as Element of COMPLEX by XCMPLX_0:def 2;
A2: 1r / ((k !) * ((n -' k) !)) = (((n !) * 1r) / (n !)) / ((k !) * ((n -' k) !)) by COMPLEX1:def 4, XCMPLX_1:60
.= ((1r / (n !)) * (n !)) / ((k !) * ((n -' k) !)) by XCMPLX_1:74 ;
assume A3: k <= n ; :: thesis: ( (Expan_e (n,z,w)) . k = ((1r / ((k !) * ((n -' k) !))) * (z #N k)) * (w #N (n -' k)) & (Expan_e (n,z,w)) . k = ((1r / (n !)) * (Expan (n,z,w))) . k )
hence (Expan_e (n,z,w)) . k = (((Coef_e n) . k) * (z #N k)) * (w #N (n -' k)) by Def3
.= ((1r / ((k !) * ((n -' k) !))) * (z #N k)) * (w #N (n -' k)) by A3, SIN_COS:def 7 ;
:: thesis: (Expan_e (n,z,w)) . k = ((1r / (n !)) * (Expan (n,z,w))) . k
hence (Expan_e (n,z,w)) . k = (((1r / (n !)) * (n !)) / ((k !) * ((n -' k) !))) * ((z #N k) * (w #N (n -' k))) by A2, CLOPBAN3:38
.= ((1r / (n !)) * ((n !) / ((k !) * ((n -' k) !)))) * ((z #N k) * (w #N (n -' k))) by XCMPLX_1:74
.= (1r / s) * ((s / ((k !) * ((n -' k) !))) * ((z #N k) * (w #N (n -' k)))) by CLOPBAN3:38
.= (1r / s) * (((s / ((k !) * ((n -' k) !))) * (z #N k)) * (w #N (n -' k))) by CLOPBAN3:38
.= (1r / (n !)) * ((((Coef n) . k) * (z #N k)) * (w #N (n -' k))) by A3, SIN_COS:def 6
.= (1r / (n !)) * ((Expan (n,z,w)) . k) by A3, Def2
.= ((1r / (n !)) * (Expan (n,z,w))) . k by CLVECT_1:def 14 ;
:: thesis: verum

end;

now :: thesis: ( n < k implies (Expan_e (n,z,w)) . k = ((1r / (n !)) * (Expan (n,z,w))) . k )

assume A4: n < k ; :: thesis: (Expan_e (n,z,w)) . k = ((1r / (n !)) * (Expan (n,z,w))) . k
hence (Expan_e (n,z,w)) . k = 0. X by Def3
.= (1r / (n !)) * (0. X) by CLVECT_1:1
.= (1r / (n !)) * ((Expan (n,z,w)) . k) by A4, Def2
.= ((1r / (n !)) * (Expan (n,z,w))) . k by CLVECT_1:def 14 ;
:: thesis: verum

end;

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

end;

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