reconsider G = ~ F as ManySortedSet of [:I,I:] ;
G is ManySortedFunction of ~ A, ~ B

proof

let ii be object ; :: according to PBOOLE:def 15 :: thesis: ( not ii in [:I,I:] or G . ii is Element of bool [:((~ A) . ii),((~ B) . ii):] )
assume ii in [:I,I:] ; :: thesis: G . ii is Element of bool [:((~ A) . ii),((~ B) . ii):]
then consider i1, i2 being object such that
A1: ( i1 in I & i2 in I ) and
A2: ii = [i1,i2] by ZFMISC_1:84;
A3: [i2,i1] in [:I,I:] by A1, ZFMISC_1:87;
dom B = [:I,I:] by PARTFUN1:def 2;
then A4: B . (i2,i1) = (~ B) . (i1,i2) by A3, FUNCT_4:def 2;
dom A = [:I,I:] by PARTFUN1:def 2;
then A5: A . (i2,i1) = (~ A) . (i1,i2) by A3, FUNCT_4:def 2;
dom F = [:I,I:] by PARTFUN1:def 2;
then F . (i2,i1) = G . (i1,i2) by A3, FUNCT_4:def 2;
hence G . ii is Element of bool [:((~ A) . ii),((~ B) . ii):] by A2, A3, A5, A4, PBOOLE:def 15; :: thesis: verum

end;

hence ~ F is ManySortedFunction of ~ A, ~ B ; :: thesis: verum