In [1]:

```
import proveit
# Prepare this notebook for defining the theorems of a theory:
%theorems_notebook # Keep this at the top following 'import proveit'.
from proveit import n
from proveit.logic import Forall, InSet, CartExp, InClass
from proveit.numbers import NaturalPos, Rational, Real, Complex
from proveit.linear_algebra import VecSpaces
```

In [2]:

```
%begin theorems
```

Number field vector sets are vector spaces:

In [3]:

```
rational_vec_set_is_vec_space = Forall(
n, InClass(CartExp(Rational, n), VecSpaces(Rational)),
domain = NaturalPos)
```

In [4]:

```
real_vec_set_is_vec_space = Forall(
n, InClass(CartExp(Real, n), VecSpaces(Real)),
domain = NaturalPos)
```

In [5]:

```
complex_vec_set_is_vec_space = Forall(
n, InClass(CartExp(Complex, n), VecSpaces(Complex)),
domain = NaturalPos)
```

As special cases, number fields are also vector spaces:

In [6]:

```
rational_set_is_vec_space = InClass(Rational, VecSpaces(Rational))
```

In [7]:

```
real_set_is_vec_space = InClass(Real, VecSpaces(Real))
```

In [8]:

```
complex_set_is_vec_space = InClass(Complex, VecSpaces(Complex))
```

In [9]:

```
%end theorems
```