let s, s1 be Real_Sequence; :: thesis: ( ( for n being Nat holds s1 . n = n -root ((abs s) . n) ) & s1 is convergent & lim s1 < 1 implies s is absolutely_summable )
assume that
A1: for n being Nat holds s1 . n = n -root ((abs s) . n) and
A2: ( s1 is convergent & lim s1 < 1 ) ; :: thesis: s is absolutely_summable

now :: thesis: for n being Nat holds
( (abs s) . n >= 0 & s1 . n = n -root ((abs s) . n) )

let n be Nat; :: thesis: ( (abs s) . n >= 0 & s1 . n = n -root ((abs s) . n) )
(abs s) . n = |.(s . n).| by SEQ_1:12;
hence (abs s) . n >= 0 by COMPLEX1:46; :: thesis: s1 . n = n -root ((abs s) . n)
thus s1 . n = n -root ((abs s) . n) by A1; :: thesis: verum

end;

then abs s is summable by A2, Th28;
hence s is absolutely_summable ; :: thesis: verum