:: deftheorem defines free_magma ALGSTR_4:def 14 :
for X being set
for n being Nat holds free_magma (X,n) = (free_magma_seq X) . n;