let X be RealUnitarySpace; :: 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 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 summable )
assume A1: for n being Element of NAT holds seq . n <> H₁(X) ; :: thesis: ( for m being Element of NAT ex n being Element of NAT st
( n >= m & not ||.(seq . (n + 1)).|| / ||.(seq . n).|| >= 1 ) or not seq is summable )
given m being Element of NAT such that A2: for n being Element of NAT st n >= m holds
||.(seq . (n + 1)).|| / ||.(seq . n).|| >= 1 ; :: thesis: not seq is summable
seq . m <> H₁(X) by A1;
then A3: ||.(seq . m).|| <> 0 by BHSP_1:32;
A4: ||.(seq . m).|| >= 0 by BHSP_1:34;

now

let n be Element of NAT ; :: thesis: ( n >= m implies ||.(seq . n).|| >= ||.(seq . m).|| )
assume A5: n >= m ; :: thesis: ||.(seq . n).|| >= ||.(seq . m).||
defpred S₁[ Element of NAT ] means ||.(seq . (m + $1)).|| >= ||.(seq . m).||;
A6: S₁[ 0 ] ;
A7: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A8: ||.(seq . (m + k)).|| >= ||.(seq . m).|| ; :: thesis: S₁[k + 1]
A9: ||.(seq . ((m + k) + 1)).|| / ||.(seq . (m + k)).|| >= 1 by A2, NAT_1:11;
seq . (m + k) <> H₁(X) by A1;
then A10: ||.(seq . (m + k)).|| <> 0 by BHSP_1:32;
||.(seq . (m + k)).|| >= 0 by BHSP_1:34;
then ||.(seq . ((m + k) + 1)).|| >= ||.(seq . (m + k)).|| by A9, A10, XREAL_1:193;
hence S₁[k + 1] by A8, XXREAL_0:2; :: thesis: verum

end;

A11: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A6, A7);
consider k being Nat such that
A12: n = m + k by A5, NAT_1:10;
k in NAT by ORDINAL1:def 13;
hence ||.(seq . n).|| >= ||.(seq . m).|| by A11, A12; :: thesis: verum

end;

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