:: deftheorem defines free_magma ALGSTR_4:def 17 :
for X being set holds free_magma X = multMagma(# (free_magma_carrier X),(free_magma_mult X) #);