:: deftheorem Def13 defines free_magma_seq ALGSTR_4:def 13 :
for X being set
for b₂ being sequence of (bool (the_universe_of (X \/ NAT))) holds
( b₂ = free_magma_seq X iff ( b₂ . 0 = {} & b₂ . 1 = X & ( for n being Nat st n >= 2 holds
ex fs being FinSequence st
( len fs = n - 1 & ( for p being Nat st p >= 1 & p <= n - 1 holds
fs . p = [:(b₂ . p),(b₂ . (n - p)):] ) & b₂ . n = Union (disjoin fs) ) ) ) );