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 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 COMSEQ_3:def 7
.= (Sum (z ExpSeq )) - (((z ExpSeq ) . 0 ) + ((z ExpSeq ) . 1)) by COMSEQ_3:def 7
.= (Sum (z ExpSeq )) - (1r + ((z ExpSeq ) . 1)) by Lm13
.= (Sum (z ExpSeq )) - (1r + z) by Lm13
.= ((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 A2, COMSEQ_3:57; :: thesis: verum