lim h = 0 ;
then lim (h ^\ n) = 0 by SEQ_4:20;
then h ^\ n is 0 -convergent ;
hence for b₁ being Real_Sequence st b₁ = h ^\ n holds
( b₁ is non-zero & b₁ is 0 -convergent ) ; :: thesis: verum