let I be set ; :: thesis: for X being ManySortedSet of I st ( for i being object st i in I holds
X . i = {} ) holds
X = EmptyMS I
let X be ManySortedSet of I; :: thesis: ( ( for i being object st i in I holds
X . i = {} ) implies X = EmptyMS I )
assume A1: for i being object st i in I holds
X . i = {} ; :: thesis: X = EmptyMS I

now :: thesis: for i being object st i in I holds
X . i = (EmptyMS I) . i

let i be object ; :: thesis: ( i in I implies X . i = (EmptyMS I) . i )
assume i in I ; :: thesis: X . i = (EmptyMS I) . i
hence X . i = {} by A1
.= (EmptyMS I) . i ;
:: thesis: verum

end;

hence X = EmptyMS I by Th3; :: thesis: verum