Proposition (extending a single element of a free, finite-dimensional module over a Bézout domain to a basis):
Let
be a Bézout domain, and let
be the
-dimensional free module over
. Let
be such that
. Then there exist elements
such that
is a basis of
.
Proof: We proceed by induction on
. If
, the statement becomes trivial, so that the induction base is handled. Let now a general
be given; we reduce the claim to the same statement for
.
Indeed, if
is given, we may set
,
and then
. Hence, there are elements
such that
.
We define
,
so that
and
,
where for
, as usual,
denotes the vector whose every component is zero except the one in the
-th place, which is one. From these equations it is evident that
.
Also,
and
are linearly independent, because if there existed
such that
, then
and in particular
, so that either
and
and
are linearly independent (almost) by definition, or
, so that
whenever
(once again, if
, then the vectors are automatically linearly independent). But this implies that
for all
, so that contrary to the assumption
.
It now suffices to note that

by the first Noether isomorphism theorem applied to the homomorphism that forgets the first component, which reduces the dimension of the problem by one as we have
.
Proof: We proceed by induction on
, where
is the cardinality of a minimum cardinality generating set of
. Let
be a minimum cardinality generating set of
. Then we have a homomorphism

such that
for
, where
is the element of
whose every entry is zero, except for the
-th entry, which is one. Since
is surjective, the first isomorphism theorem implies that
,
where
. If
, then the claim is demonstrated. We lead
to a contradiction. Indeed, in this case there is a nonzero vector
. We denote
and set
. Then
, for otherwise the image of
in
via the canonical projection would be a torsion element. Since we have
, we may extend
to a basis
of
, and then
is generated by the images of
via the canonical projection. Yet this contradicts the minimality of
.
Proof: If
is torsion-free, then every submodule of
is torsion-free as well. Hence,
as in the theorem's statement is torsion-free and finitely generated. Hence, there exists a basis of
.
Proposition (basis extension over Bézout domains):
Let
be a Bézout domain, and let
be a torsion-free module over
. If
are linearly independent vectors in
such that
is torsion-free and finitely generated, then we find an
and vectors
such that the vectors
constitute a basis of
.
Proof: Since
is torsion-free and finitely generated, upon choosing a generating set of minimal cardinality we obtain a basis of that module. We shall denote this basis by
. If moreover

is the canonical projection, we choose a
for each
. We claim that
is a basis. First, we prove that these vectors are linearly independent. Indeed, suppose that
are such that
.
Since
is a homomorphism,
,
so that
. Thus
,
which by virtue of the linear independence of
implies
.
It remains to show that
is a generating set of
. In order to do so, suppose that
is arbitrary. We choose
such that
.
We further define
, so that
. But by the definition of
, this means that
, so that there are
such that
, hence
,
which shows that
is a generating set of
since
was arbitrary.
Theorem (dimension formula):