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

now :: thesis: for i being object st i in I holds
({A} (\/) {B}) . i = {A,B} . i

let i be object ; :: 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 4
.= ({A} . i) \/ {(B . i)} by A1, Def1
.= {(A . i)} \/ {(B . i)} by A1, Def1
.= {(A . i),(B . i)} by ENUMSET1:1
.= {A,B} . i by A1, Def2 ;
:: thesis: verum

end;

hence {A} (\/) {B} = {A,B} ; :: thesis: verum