Theorem hhlm

Description: The limit sequences of Hilbert space. (Contributed by NM, 19-Nov-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hhlm.1	|- U = <. <. +h , .h >. , normh >.
	hhlm.2	|- D = ( IndMet ` U )
	hhlm.3	|- J = ( MetOpen ` D )
Assertion	hhlm	|- ~~>v = ( ( ~~>t ` J ) |` ( ~H ^m NN ) )

Proof

Step	Hyp	Ref	Expression
1		hhlm.1	|- U = <. <. +h , .h >. , normh >.
2		hhlm.2	|- D = ( IndMet ` U )
3		hhlm.3	|- J = ( MetOpen ` D )
4	1	hhnv	|- U e. NrmCVec
5	1	hhba	|- ~H = ( BaseSet ` U )
6	1 4 5 2 3	h2hlm	|- ~~>v = ( ( ~~>t ` J ) |` ( ~H ^m NN ) )