let z, w be Element of COMPLEX ; :: 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

A2: now

assume A3: n < k ; :: 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 )) * 0c by Def14
.= (1r / (n !c )) * ((Expan n,z,w) . k) by A3, Def13
.= ((1r / (n !c )) (#) (Expan n,z,w)) . k by VALUED_1:6 ;
:: thesis: verum

end;

now

assume A5: k <= n ; :: thesis: (Expan_e n,z,w) . k = ((1r / (n !c )) (#) (Expan n,z,w)) . k
then A6: (Expan_e n,z,w) . k = (((Coef_e n) . k) * (z |^ k)) * (w |^ (n -' k)) by Def14
.= ((1r / ((k !c ) * ((n -' k) !c ))) * (z |^ k)) * (w |^ (n -' k)) by A5, Def11 ;
1r / ((k !c ) * ((n -' k) !c )) = (((n !c ) * 1r ) / (n !c )) / ((k !c ) * ((n -' k) !c )) by Th1, XCMPLX_1:60
.= ((1r / (n !c )) * (n !c )) / ((k !c ) * ((n -' k) !c )) ;
hence (Expan_e n,z,w) . k = (((1r / (n !c )) * (n !c )) / ((k !c ) * ((n -' k) !c ))) * ((z |^ k) * (w |^ (n -' k))) by A6
.= (1r / (n !c )) * ((((n !c ) / ((k !c ) * ((n -' k) !c ))) * (z |^ k)) * (w |^ (n -' k)))
.= (1r / (n !c )) * ((((Coef n) . k) * (z |^ k)) * (w |^ (n -' k))) by A5, Def10
.= (1r / (n !c )) * ((Expan n,z,w) . k) by A5, Def13
.= ((1r / (n !c )) (#) (Expan n,z,w)) . k by VALUED_1:6 ;
:: thesis: verum

end;

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

end;

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