let I be set ; :: thesis: for M being ManySortedSet of I
for i being set st i in I holds
i .--> (M . i) = M | {i}
let M be ManySortedSet of I; :: thesis: for i being set st i in I holds
i .--> (M . i) = M | {i}
let i be set ; :: thesis: ( i in I implies i .--> (M . i) = M | {i} )
assume i in I ; :: thesis: i .--> (M . i) = M | {i}
then i in dom M by PARTFUN1:def 2;
hence i .--> (M . i) = M | {i} by Th6; :: thesis: verum