Theorem hlimseqi

Description: A sequence with a limit on a Hilbert space is a sequence. (Contributed by NM, 16-Aug-1999) (New usage is discouraged.)

	Ref	Expression
Hypothesis	hlim.1	|- A e. _V
Assertion	hlimseqi	|- ( F ~~>v A -> F : NN --> ~H )

Proof

Step	Hyp	Ref	Expression
1		hlim.1	|- A e. _V
2	1	hlimi	|- ( F ~~>v A <-> ( ( F : NN --> ~H /\ A e. ~H ) /\ A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` z ) -h A ) ) < x ) )
3	2	simplbi	|- ( F ~~>v A -> ( F : NN --> ~H /\ A e. ~H ) )
4	3	simpld	|- ( F ~~>v A -> F : NN --> ~H )