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

now

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

A1: now

assume A2: n < k ; :: thesis: (Expan_e (n,z,w)) . k = ((1r / (n !)) (#) (Expan (n,z,w))) . k
hence (Expan_e (n,z,w)) . k = (1r / (n !)) * 0c by Def14
.= (1r / (n !)) * ((Expan (n,z,w)) . k) by A2, Def13
.= ((1r / (n !)) (#) (Expan (n,z,w))) . k by VALUED_1:6 ;
:: thesis: verum

end;

now

assume A3: k <= n ; :: thesis: (Expan_e (n,z,w)) . k = ((1r / (n !)) (#) (Expan (n,z,w))) . k
then A4: (Expan_e (n,z,w)) . k = (((Coef_e n) . k) * (z |^ k)) * (w |^ (n -' k)) by Def14
.= ((1r / ((k !) * ((n -' k) !))) * (z |^ k)) * (w |^ (n -' k)) by A3, Def11 ;
1r / ((k !) * ((n -' k) !)) = (((n !) * 1r) / (n !)) / ((k !) * ((n -' k) !)) by XCMPLX_1:60
.= ((1r / (n !)) * (n !)) / ((k !) * ((n -' k) !)) ;
hence (Expan_e (n,z,w)) . k = (((1r / (n !)) * (n !)) / ((k !) * ((n -' k) !))) * ((z |^ k) * (w |^ (n -' k))) by A4
.= (1r / (n !)) * ((((n !) / ((k !) * ((n -' k) !))) * (z |^ k)) * (w |^ (n -' k)))
.= (1r / (n !)) * ((((Coef n) . k) * (z |^ k)) * (w |^ (n -' k))) by A3, Def10
.= (1r / (n !)) * ((Expan (n,z,w)) . k) by A3, Def13
.= ((1r / (n !)) (#) (Expan (n,z,w))) . k by VALUED_1:6 ;
:: 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