:: deftheorem defines free_magma_carrier ALGSTR_4:def 15 :
for X being set holds free_magma_carrier X = Union (disjoin ((free_magma_seq X) | NATPLUS));