for X being set
for w being Element of (free_magma X) st length w >= 2 holds
ex w1, w2 being Element of (free_magma X) st
( w = w1 * w2 & length w1 < length w & length w2 < length w )