let X be RealNormSpace; :: thesis: for seq being sequence of X st ( for n being Element of NAT holds seq . n <> 0. X ) & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
(||.seq.|| . (n + 1)) / (||.seq.|| . n) >= 1 holds
not seq is norm_summable
let seq be sequence of X; :: thesis: ( ( for n being Element of NAT holds seq . n <> 0. X ) & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
(||.seq.|| . (n + 1)) / (||.seq.|| . n) >= 1 implies not seq is norm_summable )
assume A1: ( ( for n being Element of NAT holds seq . n <> 0. X ) & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
(||.seq.|| . (n + 1)) / (||.seq.|| . n) >= 1 ) ; :: thesis: not seq is norm_summable

A2: now

let n be Element of NAT ; :: thesis: ||.seq.|| . n <> 0
seq . n <> 0. X by A1;
then ||.(seq . n).|| <> 0 by NORMSP_1:def 2;
hence ||.seq.|| . n <> 0 by NORMSP_1:def 10; :: thesis: verum

end;

consider m being Element of NAT such that
A3: for n being Element of NAT st n >= m holds
(||.seq.|| . (n + 1)) / (||.seq.|| . n) >= 1 by A1;

now

let n be Element of NAT ; :: thesis: ( n >= m implies ((abs ||.seq.||) . (n + 1)) / ((abs ||.seq.||) . n) >= 1 )
assume A4: n >= m ; :: thesis: ((abs ||.seq.||) . (n + 1)) / ((abs ||.seq.||) . n) >= 1
A5: ( 0 <= ||.seq.|| . n & 0 <= ||.seq.|| . (n + 1) ) by Th2;
A6: (abs ||.seq.||) . n = abs (||.seq.|| . n) by SEQ_1:16
.= ||.seq.|| . n by A5, ABSVALUE:def 1 ;
(abs ||.seq.||) . (n + 1) = abs (||.seq.|| . (n + 1)) by SEQ_1:16
.= ||.seq.|| . (n + 1) by A5, ABSVALUE:def 1 ;
hence ((abs ||.seq.||) . (n + 1)) / ((abs ||.seq.||) . n) >= 1 by A3, A4, A6; :: thesis: verum

end;

hence not ||.seq.|| is summable by A2, SERIES_1:44; :: according to LOPBAN_3:def 4 :: thesis: verum