let I, J be set ; :: thesis: for M being ManySortedSet of [:I,J:]
for i, j being set st i in I & j in J holds
(i,j) :-> (M . (i,j)) = M | [:{i},{j}:]
let M be ManySortedSet of [:I,J:]; :: thesis: for i, j being set st i in I & j in J holds
(i,j) :-> (M . (i,j)) = M | [:{i},{j}:]
let i, j be set ; :: thesis: ( i in I & j in J implies (i,j) :-> (M . (i,j)) = M | [:{i},{j}:] )
assume ( i in I & j in J ) ; :: thesis: (i,j) :-> (M . (i,j)) = M | [:{i},{j}:]
then A1: [i,j] in [:I,J:] by ZFMISC_1:87;
thus (i,j) :-> (M . (i,j)) = [i,j] .--> (M . [i,j])
.= M | {[i,j]} by A1, Th7
.= M | [:{i},{j}:] by ZFMISC_1:29 ; :: thesis: verum