Description: A linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 23Jan2006) (New usage is discouraged.)
Ref  Expression  

Hypothesis  lnopl.1   T e. LinOp 

Assertion  lnopfi   T : ~H > ~H 
Step  Hyp  Ref  Expression 

1  lnopl.1   T e. LinOp 

2  lnopf   ( T e. LinOp > T : ~H > ~H ) 

3  1 2  axmp   T : ~H > ~H 