let Rseq be Real_Sequence; :: thesis: for X being RealUnitarySpace
for seq being sequence of X st ( for n being Element of NAT holds Rseq . n = n -root (||.seq.|| . n) ) & Rseq is convergent & lim Rseq > 1 holds
not seq is summable
let X be RealUnitarySpace; :: thesis: for seq being sequence of X st ( for n being Element of NAT holds Rseq . n = n -root (||.seq.|| . n) ) & Rseq is convergent & lim Rseq > 1 holds
not seq is summable
let seq be sequence of X; :: thesis: ( ( for n being Element of NAT holds Rseq . n = n -root (||.seq.|| . n) ) & Rseq is convergent & lim Rseq > 1 implies not seq is summable )
assume that
A1: for n being Element of NAT holds Rseq . n = n -root (||.seq.|| . n) and
A2: ( Rseq is convergent & lim Rseq > 1 ) ; :: thesis: not seq is summable
(lim Rseq) - 1 > 0 by A2, XREAL_1:52;
then consider m being Element of NAT such that
A3: for n being Element of NAT st n >= m holds
abs ((Rseq . n) - (lim Rseq)) < (lim Rseq) - 1 by A2, SEQ_2:def 7;

now

let n be Element of NAT ; :: thesis: ( n >= m + 1 implies ||.(seq . n).|| >= 1 )
assume A4: n >= m + 1 ; :: thesis: ||.(seq . n).|| >= 1
m + 1 >= m by NAT_1:11;
then A5: n >= m by A4, XXREAL_0:2;
A6: ||.(seq . n).|| >= 0 by BHSP_1:34;
Rseq . n = n -root (||.seq.|| . n) by A1
.= n -root ||.(seq . n).|| by BHSP_2:def 3 ;
then abs ((n -root ||.(seq . n).||) - (lim Rseq)) < (lim Rseq) - 1 by A3, A5;
then - ((lim Rseq) - 1) < (n -root ||.(seq . n).||) - (lim Rseq) by SEQ_2:9;
then (1 - (lim Rseq)) + (lim Rseq) < ((n -root ||.(seq . n).||) - (lim Rseq)) + (lim Rseq) by XREAL_1:8;
then A7: (n -root ||.(seq . n).||) |^ n >= 1 by PREPOWER:19;
m + 1 >= 1 by NAT_1:11;
then n >= 1 by A4, XXREAL_0:2;
hence ||.(seq . n).|| >= 1 by A6, A7, POWER:5; :: thesis: verum

end;

then ( not seq is convergent or lim seq <> H₁(X) ) by Th31;
hence not seq is summable by Th9; :: thesis: verum