let r be Real; :: thesis: for X being RealUnitarySpace
for seq being sequence of X st r > 0 & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.(seq . n).|| >= r & seq is convergent holds
lim seq <> 0. X
let X be RealUnitarySpace; :: thesis: for seq being sequence of X st r > 0 & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.(seq . n).|| >= r & seq is convergent holds
lim seq <> 0. X
let seq be sequence of X; :: thesis: ( r > 0 & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.(seq . n).|| >= r & seq is convergent implies lim seq <> 0. X )
assume A1: r > 0 ; :: thesis: ( for m being Element of NAT ex n being Element of NAT st
( n >= m & not ||.(seq . n).|| >= r ) or not seq is convergent or lim seq <> 0. X )
given m being Element of NAT such that A2: for n being Element of NAT st n >= m holds
||.(seq . n).|| >= r ; :: thesis: ( not seq is convergent or lim seq <> 0. X )

per cases ( not seq is convergent or seq is convergent ) ;

suppose not seq is convergent ; :: thesis: ( not seq is convergent or lim seq <> 0. X )

hence ( not seq is convergent or lim seq <> 0. X ) ; :: thesis: verum

end;

suppose A3: seq is convergent ; :: thesis: ( not seq is convergent or lim seq <> 0. X )

now

assume lim seq = H₁(X) ; :: thesis: contradiction
then consider k being Element of NAT such that
A4: for n being Element of NAT st n >= k holds
||.((seq . n) - H₁(X)).|| < r by A1, A3, BHSP_2:19;

now

let n be Element of NAT ; :: thesis: not n >= m + k
assume A5: n >= m + k ; :: thesis: contradiction
m + k >= k by NAT_1:11;
then n >= k by A5, XXREAL_0:2;
then ||.((seq . n) - H₁(X)).|| < r by A4;
then A6: ||.(seq . n).|| < r by RLVECT_1:13;
m + k >= m by NAT_1:11;
then n >= m by A5, XXREAL_0:2;
hence contradiction by A2, A6; :: thesis: verum

end;

hence contradiction ; :: thesis: verum

end;

hence ( not seq is convergent or lim seq <> 0. X ) ; :: thesis: verum

end;

end;