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