 Submodule theorem for free modules over a principal ideal domain

Every submodule of a finite-rank free module over a principal ideal domain is free. Induction on rank splits off a generator of the image under one coordinate projection and applies the result to the kernel.