let I, J be set ; 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:]; 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 ; ( i in I & j in J implies (i,j) :-> (M . (i,j)) = M | [:{i},{j}:] )
assume
( i in I & j in J )
; (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
; verum