for X being non empty set
for w being Element of free_magma_carrier X holds w in [:(free_magma (X,(w `2))),{(w `2)}:]