reconsider G = ~ F as ManySortedSet of [:I,I:] ;
G is ManySortedFunction of ~ A, ~ B
proof
let ii be
object ;
PBOOLE:def 15 ( not ii in [:I,I:] or G . ii is Element of bool [:((~ A) . ii),((~ B) . ii):] )
assume
ii in [:I,I:]
;
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;
verum
end;
hence
~ F is ManySortedFunction of ~ A, ~ B
; verum