let I be set ; :: thesis: for A, B being ManySortedSet of holds {A} \/ {B} = {A,B}
let A, B be ManySortedSet of ; :: thesis: {A} \/ {B} = {A,B}

now

let i be set ; :: thesis: ( i in I implies ({A} \/ {B}) . i = {A,B} . i )
assume A1: i in I ; :: thesis: ({A} \/ {B}) . i = {A,B} . i
hence ({A} \/ {B}) . i = ({A} . i) \/ ({B} . i) by PBOOLE:def 7
.= ({A} . i) \/ {(B . i)} by A1, Def1
.= {(A . i)} \/ {(B . i)} by A1, Def1
.= {(A . i),(B . i)} by ENUMSET1:41
.= {A,B} . i by A1, Def2 ;
:: thesis: verum

end;

hence {A} \/ {B} = {A,B} by PBOOLE:3; :: thesis: verum