let w, z be Complex; for n being Nat holds Expan_e (n,z,w) = (1r / (n !)) (#) (Expan (n,z,w))
let n be Nat; Expan_e (n,z,w) = (1r / (n !)) (#) (Expan (n,z,w))
now for k being Element of NAT holds (Expan_e (n,z,w)) . k = ((1r / (n !)) (#) (Expan (n,z,w))) . klet k be
Element of
NAT ;
(Expan_e (n,z,w)) . k = ((1r / (n !)) (#) (Expan (n,z,w))) . kA1:
now ( n < k implies (Expan_e (n,z,w)) . k = ((1r / (n !)) (#) (Expan (n,z,w))) . k )assume A2:
n < k
;
(Expan_e (n,z,w)) . k = ((1r / (n !)) (#) (Expan (n,z,w))) . khence (Expan_e (n,z,w)) . k =
(1r / (n !)) * 0c
by Def10
.=
(1r / (n !)) * ((Expan (n,z,w)) . k)
by A2, Def9
.=
((1r / (n !)) (#) (Expan (n,z,w))) . k
by VALUED_1:6
;
verum end; now ( k <= n implies (Expan_e (n,z,w)) . k = ((1r / (n !)) (#) (Expan (n,z,w))) . k )assume A3:
k <= n
;
(Expan_e (n,z,w)) . k = ((1r / (n !)) (#) (Expan (n,z,w))) . kthen A4:
(Expan_e (n,z,w)) . k =
(((Coef_e n) . k) * (z |^ k)) * (w |^ (n -' k))
by Def10
.=
((1r / ((k !) * ((n -' k) !))) * (z |^ k)) * (w |^ (n -' k))
by A3, Def7
;
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, Def6
.=
(1r / (n !)) * ((Expan (n,z,w)) . k)
by A3, Def9
.=
((1r / (n !)) (#) (Expan (n,z,w))) . k
by VALUED_1:6
;
verum end; hence
(Expan_e (n,z,w)) . k = ((1r / (n !)) (#) (Expan (n,z,w))) . k
by A1;
verum end;
hence
Expan_e (n,z,w) = (1r / (n !)) (#) (Expan (n,z,w))
; verum