let X be RealNormSpace; :: thesis: for seq being sequence of X st ( for n being Nat holds seq . n <> 0. X ) & ex m being Nat st
for n being 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 Nat holds seq . n <> 0. X ) & ex m being Nat st
for n being Nat st n >= m holds
(||.seq.|| . (n + 1)) / (||.seq.|| . n) >= 1 implies not seq is norm_summable )

assume that
A1: for n being Nat holds seq . n <> 0. X and
A2: ex m being Nat st
for n being Nat st n >= m holds
(||.seq.|| . (n + 1)) / (||.seq.|| . n) >= 1 ; :: thesis: not seq is norm_summable
consider m being Nat such that
A3: for n being Nat st n >= m holds
(||.seq.|| . (n + 1)) / (||.seq.|| . n) >= 1 by A2;
A4: now :: thesis: for n being Nat st n >= m holds
((abs ||.seq.||) . (n + 1)) / ((abs ||.seq.||) . n) >= 1
let n be Nat; :: thesis: ( n >= m implies ((abs ||.seq.||) . (n + 1)) / ((abs ||.seq.||) . n) >= 1 )
assume A5: n >= m ; :: thesis: ((abs ||.seq.||) . (n + 1)) / ((abs ||.seq.||) . n) >= 1
A6: 0 <= ||.seq.|| . n by Th2;
A7: 0 <= ||.seq.|| . (n + 1) by Th2;
A8: (abs ||.seq.||) . (n + 1) = |.(||.seq.|| . (n + 1)).| by SEQ_1:12
.= ||.seq.|| . (n + 1) by ;
(abs ||.seq.||) . n = |.(||.seq.|| . n).| by SEQ_1:12
.= ||.seq.|| . n by ;
hence ((abs ||.seq.||) . (n + 1)) / ((abs ||.seq.||) . n) >= 1 by A3, A5, A8; :: thesis: verum
end;
now :: thesis: for n being Nat holds ||.seq.|| . n <> 0
let n be Nat; :: thesis: ||.seq.|| . n <> 0
seq . n <> 0. X by A1;
then ||.(seq . n).|| <> 0 by NORMSP_0:def 5;
hence ||.seq.|| . n <> 0 by NORMSP_0:def 4; :: thesis: verum
end;
hence not ||.seq.|| is summable by ; :: according to LOPBAN_3:def 3 :: thesis: verum