let X be RealNormSpace; :: thesis: for seq being sequence of X

for rseq1 being Real_Sequence st ( for n being Nat holds rseq1 . n = n -root (||.seq.|| . n) ) & ex m being Nat st

for n being Nat st m <= n holds

rseq1 . n >= 1 holds

not ||.seq.|| is summable

let seq be sequence of X; :: thesis: for rseq1 being Real_Sequence st ( for n being Nat holds rseq1 . n = n -root (||.seq.|| . n) ) & ex m being Nat st

for n being Nat st m <= n holds

rseq1 . n >= 1 holds

not ||.seq.|| is summable

let rseq1 be Real_Sequence; :: thesis: ( ( for n being Nat holds rseq1 . n = n -root (||.seq.|| . n) ) & ex m being Nat st

for n being Nat st m <= n holds

rseq1 . n >= 1 implies not ||.seq.|| is summable )

assume A1: ( ( for n being Nat holds rseq1 . n = n -root (||.seq.|| . n) ) & ex m being Nat st

for n being Nat st m <= n holds

rseq1 . n >= 1 ) ; :: thesis: not ||.seq.|| is summable

for n being Nat holds ||.seq.|| . n >= 0 by Th2;

hence not ||.seq.|| is summable by A1, SERIES_1:29; :: thesis: verum

for rseq1 being Real_Sequence st ( for n being Nat holds rseq1 . n = n -root (||.seq.|| . n) ) & ex m being Nat st

for n being Nat st m <= n holds

rseq1 . n >= 1 holds

not ||.seq.|| is summable

let seq be sequence of X; :: thesis: for rseq1 being Real_Sequence st ( for n being Nat holds rseq1 . n = n -root (||.seq.|| . n) ) & ex m being Nat st

for n being Nat st m <= n holds

rseq1 . n >= 1 holds

not ||.seq.|| is summable

let rseq1 be Real_Sequence; :: thesis: ( ( for n being Nat holds rseq1 . n = n -root (||.seq.|| . n) ) & ex m being Nat st

for n being Nat st m <= n holds

rseq1 . n >= 1 implies not ||.seq.|| is summable )

assume A1: ( ( for n being Nat holds rseq1 . n = n -root (||.seq.|| . n) ) & ex m being Nat st

for n being Nat st m <= n holds

rseq1 . n >= 1 ) ; :: thesis: not ||.seq.|| is summable

for n being Nat holds ||.seq.|| . n >= 0 by Th2;

hence not ||.seq.|| is summable by A1, SERIES_1:29; :: thesis: verum