let s1, s be Real_Sequence; :: thesis: ( ( for n being Element of 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 Element of NAT holds s1 . n = n -root ((abs s) . n) and
A2: ( s1 is convergent & lim s1 < 1 ) ; :: thesis: s is absolutely_summable

now

let n be Element of NAT ; :: thesis: ( (abs s) . n >= 0 & s1 . n = n -root ((abs s) . n) )
(abs s) . n = abs (s . n) by SEQ_1:16;
hence (abs s) . n >= 0 by COMPLEX1:132; :: 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, Th32;
hence s is absolutely_summable by Def5; :: thesis: verum