let UN be Universe; :: thesis: for I being Element of UN
for x being UN -valued ManySortedSet of I holds Union (coprod ) is Element of UN
let I be Element of UN; :: thesis: for x being UN -valued ManySortedSet of I holds Union (coprod ) is Element of UN
let x be UN -valued ManySortedSet of I; :: thesis: Union (coprod ) is Element of UN
Union (disjoin x) is Element of UN ;
hence Union (coprod ) is Element of UN ; :: thesis: verum