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