Choose free group generators . Construct the Schreier coset graph with vertices the right cosets and a positively oriented edge labelled from to . This is well defined and connected. Its inverse edge carries . A word in the group generators determines a unique path from the base vertex ; that path closes exactly when the word represents an element of .
Deleting a consecutive edge followed by its inverse corresponds exactly to free cancellation in the word. Since reduced words are unique in a free group, the resulting map from based loops modulo these cancellations to is injective as well as surjective, and respects concatenation. Thus is the fundamental group of . More explicitly, choose a spanning tree and, for each unoriented edge outside , choose one orientation. The tree path from the base vertex to that edge, followed by the edge and the returning tree path, defines an element of . Every loop is a product of these elements and their inverses: insert the appropriate tree paths between successive edges, and tree edges contribute trivial factors. Collapsing the tree leaves one loop for each remaining edge. A product of the chosen basis loops maps to the corresponding word in these loop labels. If the original path could cancel to the constant path, its image could do so as well, since collapsing tree edges preserves every backtracking cancellation. A nonempty reduced word in the remaining labels cannot cancel to the empty word, proving that there are no further relations. These elements therefore form a free basis. This proves that is a free group without assuming the subgroup theorem.
If is finite, the graph has vertices and unoriented edges, counted by their positive labels; loops and parallel edges count separately. A spanning tree has edges. The Nielsen–Schreier formula follows:
For a sequence of finite indices , this gives the rank-to-index limit for subgroups of a free group
Finally, let be an endomorphism, and put . It is generated by the images . If its index is finite, it is free of rank . A rank- free group needs at least group generators: its abelianization is , and reduction modulo gives the -dimensional vector space , which cannot be generated by fewer than vectors. Therefore
Since , this forces , hence . This proves that a finite-index image of a free-group endomorphism is surjective: