let I, J be set ; :: thesis: for M being ManySortedSet of
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 ; :: 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:106;
thus i,j :-> (M . i,j) = [i,j] .--> (M . [i,j])
.= M | {[i,j]} by A1, Th7
.= M | [:{i},{j}:] by ZFMISC_1:35 ; :: thesis: verum