Theorem lnfnfi

Description: A linear Hilbert space functional is a functional. (Contributed by NM, 11-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Hypothesis	lnfnl.1	⊢ 𝑇 ∈ LinFn
Assertion	lnfnfi	⊢ 𝑇 : ℋ ⟶ ℂ

Proof

Step	Hyp	Ref	Expression
1		lnfnl.1	⊢ 𝑇 ∈ LinFn
2		lnfnf	⊢ ( 𝑇 ∈ LinFn → 𝑇 : ℋ ⟶ ℂ )
3	1 2	ax-mp	⊢ 𝑇 : ℋ ⟶ ℂ