for X being non empty set
for v, w being Element of free_magma_carrier X holds [[[(v `1),(w `1)],(v `2)],((v `2) + (w `2))] is Element of free_magma_carrier X