let I1, I2 be non empty set ; for M being ManySortedSet of [:I1,I2:]
for o1 being Element of I1
for o2 being Element of I2 holds (~ M) . (o2,o1) = M . (o1,o2)
let M be ManySortedSet of [:I1,I2:]; for o1 being Element of I1
for o2 being Element of I2 holds (~ M) . (o2,o1) = M . (o1,o2)
let o1 be Element of I1; for o2 being Element of I2 holds (~ M) . (o2,o1) = M . (o1,o2)
let o2 be Element of I2; (~ M) . (o2,o1) = M . (o1,o2)
[o1,o2] in [:I1,I2:]
;
then
[o1,o2] in dom M
by PARTFUN1:def 2;
hence
(~ M) . (o2,o1) = M . (o1,o2)
by FUNCT_4:def 2; verum