let X be non empty 1-sorted ; :: thesis: {} X, [#] X constitute_a_decomposition
[#] X = ({} X) ` ;
hence {} X, [#] X constitute_a_decomposition by Th5; :: thesis: verum