Proposition (every chain complex of finitely generated free modules over a Bézout domain is the direct sum of some of its subcomplexes with at most two nonzero terms):
Let

be a chain complex whose objects are finitely generated free modules over a Bézout domain
. This chain complex is then the countable direct sum of chain complexes of the form
,
where
and
.
(On the condition of the countable choice.)
Proof: We shall construct a direct sum decomposition
,
where
. Once this is accomplished, we have in fact obtained a direct sum decomposition of the initial chain complex, because elements of
are mapped to zero by
, and elements of
are mapped to
due to the chain complex condition
.
In order to achieve this decomposition, we invoke Dedekind's theorem for Bézout domains, which tells us that
is finitely generated and free; indeed, it is finitely generated, since a generating set is given by the image (via
) of a generating set of
. Let thus
be a basis of
. For each
, we choose an arbitrary, but fixed
, and then we define
. This yields the desired direct sum decomposition. Indeed,
, since whenever

for some elements
of
, applying
to both sides of this equation and using its
-linearity yields
,
which implies
. Moreover,
, since if
is arbitrary, we may select
such that
,
from which we may easily deduce that
. 
Proposition (every chain complex of finitely generated free modules over a Bézout domain splits as the direct sum of two types of elementary chain complexes):
Let

be a chain complex whose objects are finitely generated free modules over a Bézout domain
. This chain complex is the countable direct sum of copies of the following two chain complexes:

for an element
, ie. the arrow represents the function which is given by multiplication by 
(On the condition of the countable choice.)
Proof: Using the notation of the last theorem, we have
, where
is finitely generated and
is sent to zero by
.