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 not s is summable )
assume that
A1: for n being Element of NAT holds s1 . n = n -root ((abs s) . n) and
A2: s1 is convergent and
A3: lim s1 > 1 ; :: thesis: not s is summable
(lim s1) - 1 > 0 by A3, XREAL_1:50;
then consider m being Element of NAT such that
A4: for n being Element of NAT st n >= m holds
abs ((s1 . n) - (lim s1)) < (lim s1) - 1 by A2, SEQ_2:def 7;

now

let n be Element of NAT ; :: thesis: ( n >= m + 1 implies abs (s . n) >= 1 )
assume A5: n >= m + 1 ; :: thesis: abs (s . n) >= 1
A6: s1 . n = n -root ((abs s) . n) by A1
.= n -root (abs (s . n)) by SEQ_1:12 ;
m + 1 >= m by NAT_1:11;
then n >= m by A5, XXREAL_0:2;
then abs ((n -root (abs (s . n))) - (lim s1)) < (lim s1) - 1 by A4, A6;
then - ((lim s1) - 1) < (n -root (abs (s . n))) - (lim s1) by SEQ_2:1;
then (1 - (lim s1)) + (lim s1) < ((n -root (abs (s . n))) - (lim s1)) + (lim s1) by XREAL_1:6;
then A7: ( abs (s . n) >= 0 & (n -root (abs (s . n))) |^ n >= 1 ) by COMPLEX1:46, PREPOWER:11;
m + 1 >= 1 by NAT_1:11;
then n >= 1 by A5, XXREAL_0:2;
hence abs (s . n) >= 1 by A7, POWER:4; :: thesis: verum

end;

then ( not s is convergent or lim s <> 0 ) by Th43;
hence not s is summable by Th7; :: thesis: verum