let x be Real; :: thesis: x rExpSeq is absolutely_summable
for n being Nat holds |.((x rExpSeq) . n).| = (|.x.| rExpSeq) . n

proof

let n be Nat; :: thesis: |.((x rExpSeq) . n).| = (|.x.| rExpSeq) . n
|.((x rExpSeq) . n).| = |.((x |^ n) / (n !)).| by SIN_COS:def 5
.= |.(x |^ n).| / |.(n !).| by COMPLEX1:67
.= |.(x |^ n).| / (n !) by ABSVALUE:def 1
.= (|.x.| |^ n) / (n !) by Th1
.= (|.x.| rExpSeq) . n by SIN_COS:def 5 ;
hence |.((x rExpSeq) . n).| = (|.x.| rExpSeq) . n ; :: thesis: verum

end;

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