for X being non empty 1-sorted holds {} X, [#] X constitute_a_decomposition