The map , , is a module homomorphism, and it is injective because and is a torsion-free module. The linear independence in a module of makes the map sending the standard basis to an isomorphism. Thus is a finite free module, and . This proves embedding a finitely generated torsion-free module in a finite free module. No claim that the submodule itself is free over an arbitrary integral domain is needed.