let UN be Universe; :: thesis: for I, u, v being Element of UN
for x being UN -valued ManySortedSet of I st I = {{},{{}}} & x . {} = u & x . {{}} = v holds
disjoint-union x = [:u,{{}}:] \/ [:v,{{{}}}:]
let I, u, v be Element of UN; :: thesis: for x being UN -valued ManySortedSet of I st I = {{},{{}}} & x . {} = u & x . {{}} = v holds
disjoint-union x = [:u,{{}}:] \/ [:v,{{{}}}:]
let x be UN -valued ManySortedSet of I; :: thesis: ( I = {{},{{}}} & x . {} = u & x . {{}} = v implies disjoint-union x = [:u,{{}}:] \/ [:v,{{{}}}:] )
assume A1: ( I = {{},{{}}} & x . {} = u & x . {{}} = v ) ; :: thesis: disjoint-union x = [:u,{{}}:] \/ [:v,{{{}}}:]
( {} UN is Element of UN & {({} UN)} is Element of UN ) ;
hence disjoint-union x = [:u,{{}}:] \/ [:v,{{{}}}:] by A1, Th32; :: thesis: verum