let z be complex number ; :: thesis: z * (Sum (z P_dt)) = ((Sum (z ExpSeq)) - 1r) - z
A1: for z being complex number holds z (#) (z P_dt) = (z ExpSeq) ^\ 2

proof

let z be complex number ; :: thesis: z (#) (z P_dt) = (z ExpSeq) ^\ 2
for n being Element of NAT holds (z (#) (z P_dt)) . n = ((z ExpSeq) ^\ 2) . n

proof

let n be Element of NAT ; :: thesis: (z (#) (z P_dt)) . n = ((z ExpSeq) ^\ 2) . n
(z (#) (z P_dt)) . n = z * ((z P_dt) . n) by VALUED_1:6
.= z * ((z |^ (n + 1)) / ((n + 2) !c)) by Def28 ;
then (z (#) (z P_dt)) . n = (z * (z |^ (n + 1))) / ((n + 2) !c)
.= (z |^ ((n + 1) + 1)) / ((n + 2) !c) by NEWTON:11
.= (z ExpSeq) . (n + 2) by Def8
.= ((z ExpSeq) ^\ 2) . n by NAT_1:def 3 ;
hence (z (#) (z P_dt)) . n = ((z ExpSeq) ^\ 2) . n ; :: thesis: verum

end;

hence z (#) (z P_dt) = (z ExpSeq) ^\ 2 by FUNCT_2:113; :: thesis: verum

end;

Sum (z ExpSeq) = ((Partial_Sums (z ExpSeq)) . 1) + (Sum ((z ExpSeq) ^\ (1 + 1))) by COMSEQ_3:61
.= ((Partial_Sums (z ExpSeq)) . 1) + (Sum ((z ExpSeq) ^\ 2)) ;
then A6: Sum (z (#) (z P_dt)) = (Sum (z ExpSeq)) - ((Partial_Sums (z ExpSeq)) . (0 + 1)) by A1
.= (Sum (z ExpSeq)) - (((Partial_Sums (z ExpSeq)) . 0) + ((z ExpSeq) . 1)) by SERIES_1:def 1
.= (Sum (z ExpSeq)) - (((z ExpSeq) . 0) + ((z ExpSeq) . 1)) by SERIES_1:def 1
.= (Sum (z ExpSeq)) - (1r + ((z ExpSeq) . 1)) by Lm9
.= (Sum (z ExpSeq)) - (1r + z) by Lm9
.= ((Sum (z ExpSeq)) - 1r) - z ;
reconsider BBB = z P_dt as absolutely_summable Complex_Sequence by Th61;
BBB is summable ;
hence z * (Sum (z P_dt)) = ((Sum (z ExpSeq)) - 1r) - z by A6, COMSEQ_3:57; :: thesis: verum