let I be set ; :: thesis: for x, X being ManySortedSet of st x in X holds
{x} \/ X = X
let x, X be ManySortedSet of ; :: thesis: ( x in X implies {x} \/ X = X )
assume A1: x in X ; :: thesis: {x} \/ X = X

now

let i be set ; :: thesis: ( i in I implies ({x} \/ X) . i = X . i )
assume A2: i in I ; :: thesis: ({x} \/ X) . i = X . i
then A3: x . i in X . i by A1, PBOOLE:def 4;
thus ({x} \/ X) . i = ({x} . i) \/ (X . i) by A2, PBOOLE:def 7
.= {(x . i)} \/ (X . i) by A2, Def1
.= X . i by A3, ZFMISC_1:46 ; :: thesis: verum

end;

hence {x} \/ X = X by PBOOLE:3; :: thesis: verum