let I1, I2 be non empty set ; :: thesis: 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:]; :: thesis: 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; :: thesis: for o2 being Element of I2 holds (~ M) . (o2,o1) = M . (o1,o2)
let o2 be Element of I2; :: thesis: (~ 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; :: thesis: verum