let I be set ; :: thesis: for x being ManySortedSet of I holds {x,x} = {x}
let x be ManySortedSet of I; :: thesis: {x,x} = {x}

now :: thesis: for i being object st i in I holds
{x,x} . i = {x} . i

let i be object ; :: thesis: ( i in I implies {x,x} . i = {x} . i )
assume A1: i in I ; :: thesis: {x,x} . i = {x} . i
hence {x,x} . i = {(x . i),(x . i)} by Def2
.= {(x . i)} by ENUMSET1:29
.= {x} . i by A1, Def1 ;
:: thesis: verum

end;

hence {x,x} = {x} ; :: thesis: verum