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

proof

let z be Complex; :: 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) !)) by Def24 ;
then (z (#) (z P_dt)) . n = (z * (z |^ (n + 1))) / ((n + 2) !)
.= (z |^ ((n + 1) + 1)) / ((n + 2) !) by NEWTON:6
.= (z ExpSeq) . (n + 2) by Def4
.= ((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 ; :: thesis: verum

end;

Sum (z ExpSeq) = ((Partial_Sums (z ExpSeq)) . 1) + (Sum ((z ExpSeq) ^\ (1 + 1))) by COMSEQ_3:60
.= ((Partial_Sums (z ExpSeq)) . 1) + (Sum ((z ExpSeq) ^\ 2)) ;
then A2: 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 Lm8
.= (Sum (z ExpSeq)) - (1r + z) by Lm8
.= ((Sum (z ExpSeq)) - 1r) - z ;
reconsider BBB = z P_dt as absolutely_summable Complex_Sequence by Th55;
BBB is summable ;
hence z * (Sum (z P_dt)) = ((Sum (z ExpSeq)) - 1r) - z by A2, COMSEQ_3:56; :: thesis: verum