let I be set ; :: thesis: for A being non-empty ManySortedSet of I
for F being ManySortedFunction of A, EmptyMS I holds F = EmptyMS I
let A be non-empty ManySortedSet of I; :: thesis: for F being ManySortedFunction of A, EmptyMS I holds F = EmptyMS I
let F be ManySortedFunction of A, EmptyMS I; :: thesis: F = EmptyMS I

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

let i be object ; :: thesis: ( i in I implies F . i = (EmptyMS I) . i )
assume i in I ; :: thesis: F . i = (EmptyMS I) . i
then reconsider f = F . i as Function of (A . i),((EmptyMS I) . i) by PBOOLE:def 15;
f = {} ;
hence F . i = (EmptyMS I) . i ; :: thesis: verum

end;

hence F = EmptyMS I ; :: thesis: verum