Description: A member of a subspace of a Hilbert space is a vector. (Contributed by NM, 6-Oct-1999) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | shssi.1 | ||
| sheli.1 | |||
| Assertion | shelii | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | shssi.1 | ||
| 2 | sheli.1 | ||
| 3 | 1 | shssii | |
| 4 | 3 2 | sselii |