for X, x, y being set
for n, m being Nat st x in free_magma (X,n) & y in free_magma (X,m) holds
[[x,y],n] in free_magma (X,(n + m))