let x be Real; :: thesis: x rExpSeq is absolutely_summable
for n being Element of NAT holds abs ((x rExpSeq ) . n) = ((abs x) rExpSeq ) . n

proof

let n be Element of NAT ; :: thesis: abs ((x rExpSeq ) . n) = ((abs x) rExpSeq ) . n
A1: n ! > 0 by NEWTON:23;
abs ((x rExpSeq ) . n) = abs ((x |^ n) / (n ! )) by SIN_COS:def 9
.= (abs (x |^ n)) / (abs (n ! )) by COMPLEX1:153
.= (abs (x |^ n)) / (n ! ) by A1, ABSVALUE:def 1
.= ((abs x) |^ n) / (n ! ) by Th1
.= ((abs x) rExpSeq ) . n by SIN_COS:def 9 ;
hence abs ((x rExpSeq ) . n) = ((abs x) rExpSeq ) . n ; :: thesis: verum

end;

then (abs x) rExpSeq = abs (x rExpSeq ) by SEQ_1:16;
then abs (x rExpSeq ) is summable by SIN_COS:49;
hence x rExpSeq is absolutely_summable by SERIES_1:def 5; :: thesis: verum