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.
For each , maximality implies a nontrivial relation
Here , since otherwise this would contradict the linear independence in a module of . Thus . Take , with empty product equal to one. Because is an integral domain, . Every satisfies , and this is also true for . Expressing any element of the finitely generated module as an -linear combination of now gives . This is clearing denominators relative to an independent module subset; it does not require to be a field.