Metamath Proof Explorer

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 
|- T e. LinFn
Assertion lnfnfi 
|- T : ~H --> CC

Proof

Step Hyp Ref Expression
1 lnfnl.1 
 |-  T e. LinFn
2 lnfnf 
 |-  ( T e. LinFn -> T : ~H --> CC )
3 1 2 ax-mp 
 |-  T : ~H --> CC