reconsider G = ~ F as ManySortedSet of [:I,I:] ;
G is ManySortedFunction of ~ A, ~ B
proof
let ii be
set ;
:: according to PBOOLE:def 18 :: thesis: ( not ii in [:I,I:] or G . ii is M5((~ A) . ii,(~ B) . ii) )
assume
ii in [:I,I:]
;
:: thesis: G . ii is M5((~ A) . ii,(~ B) . ii)
then consider i1,
i2 being
set such that A1:
(
i1 in I &
i2 in I )
and A2:
ii = [i1,i2]
by ZFMISC_1:103;
A3:
[i2,i1] in [:I,I:]
by A1, ZFMISC_1:106;
dom F = [:I,I:]
by PBOOLE:def 3;
then A4:
F . i2,
i1 = G . i1,
i2
by A3, FUNCT_4:def 2;
dom A = [:I,I:]
by PBOOLE:def 3;
then A5:
A . i2,
i1 = (~ A) . i1,
i2
by A3, FUNCT_4:def 2;
dom B = [:I,I:]
by PBOOLE:def 3;
then
B . i2,
i1 = (~ B) . i1,
i2
by A3, FUNCT_4:def 2;
hence
G . ii is
M5(
(~ A) . ii,
(~ B) . ii)
by A2, A3, A4, A5, PBOOLE:def 18;
:: thesis: verum
end;
hence
~ F is ManySortedFunction of ~ A, ~ B
; :: thesis: verum