Description: The free group is a group. (Contributed by Mario Carneiro, 1-Oct-2015) (Revised by Mario Carneiro, 27-Feb-2016)