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:17;
abs ((x rExpSeq) . n) = abs ((x |^ n) / (n !)) by SIN_COS:def 5
.= (abs (x |^ n)) / (abs (n !)) by COMPLEX1:67
.= (abs (x |^ n)) / (n !) by A1, ABSVALUE:def 1
.= ((abs x) |^ n) / (n !) by Th1
.= ((abs x) rExpSeq) . n by SIN_COS:def 5 ;
hence abs ((x rExpSeq) . n) = ((abs x) rExpSeq) . n ; :: thesis: verum

end;

then (abs x) rExpSeq = abs (x rExpSeq) by SEQ_1:12;
then abs (x rExpSeq) is summable by SIN_COS:45;
hence x rExpSeq is absolutely_summable by SERIES_1:def 4; :: thesis: verum