theorem Th21: :: ALGSTR_4:21

for X, x being set
for n being Nat st n >= 2 & x in free_magma (X,n) holds
ex p, m being Nat st
( x `2 = p & 1 <= p & p <= n - 1 & (x `1) `1 in free_magma (X,p) & (x `1) `2 in free_magma (X,m) & n = p + m & x in [:[:(free_magma (X,p)),(free_magma (X,m)):],{p}:] )