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} & u <> v holds
disjoint-union x = disjoint-union (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} & u <> v holds
disjoint-union x = disjoint-union (u,v)
let x be UN -valued ManySortedSet of I; :: thesis: ( I = {{},{{}}} & x . {} = {u} & x . {{}} = {v} & u <> v implies disjoint-union x = disjoint-union (u,v) )
assume that
A1: I = {{},{{}}} and
A2: x . {} = {u} and
A3: x . {{}} = {v} and
A4: u <> v ; :: thesis: disjoint-union x = disjoint-union (u,v)
( disjoint-union (u,v) = {[u,{}],[v,{{}}]} & disjoint-union x = [:{u},{{}}:] \/ [:{v},{{{}}}:] ) by A1, A2, A3, Th33, A4, FUNCT_4:67;
hence disjoint-union x = disjoint-union (u,v) by Th31; :: thesis: verum