reconsider G = ~ F as ManySortedSet of [:I,I:] ;

G is ManySortedFunction of ~ A, ~ B

G is ManySortedFunction of ~ A, ~ B

proof

hence
~ F is ManySortedFunction of ~ A, ~ B
; :: thesis: verum
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;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