theorem Th20: :: ALGSTR_4:20

for X being set
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 = [:(free_magma (X,p)),(free_magma (X,(n -' p))):] ) & free_magma (X,n) = Union (disjoin fs) )