for X being non empty set
for A being Subset of (free_magma X) st A = (canon_image (X,1)) .: X holds
free_magma X = the_submagma_generated_by A