let A, B be set ; for a being object holds ~ ([:A,B:] --> a) = [:B,A:] --> a
let a be object ; ~ ([:A,B:] --> a) = [:B,A:] --> a
A1:
now for x being object holds
( ( x in dom ([:B,A:] --> a) implies ex y, z being object st
( x = [z,y] & [y,z] in dom ([:A,B:] --> a) ) ) & ( ex y, z being object st
( x = [z,y] & [y,z] in dom ([:A,B:] --> a) ) implies x in dom ([:B,A:] --> a) ) )let x be
object ;
( ( x in dom ([:B,A:] --> a) implies ex y, z being object st
( x = [z,y] & [y,z] in dom ([:A,B:] --> a) ) ) & ( ex y, z being object st
( x = [z,y] & [y,z] in dom ([:A,B:] --> a) ) implies x in dom ([:B,A:] --> a) ) )hereby ( ex y, z being object st
( x = [z,y] & [y,z] in dom ([:A,B:] --> a) ) implies x in dom ([:B,A:] --> a) )
assume
x in dom ([:B,A:] --> a)
;
ex y, z being object st
( x = [z,y] & [y,z] in dom ([:A,B:] --> a) )then consider z,
y being
object such that A2:
z in B
and A3:
y in A
and A4:
x = [z,y]
by ZFMISC_1:def 2;
take y =
y;
ex z being object st
( x = [z,y] & [y,z] in dom ([:A,B:] --> a) )take z =
z;
( x = [z,y] & [y,z] in dom ([:A,B:] --> a) )thus
x = [z,y]
by A4;
[y,z] in dom ([:A,B:] --> a)
[y,z] in [:A,B:]
by A2, A3, ZFMISC_1:87;
hence
[y,z] in dom ([:A,B:] --> a)
;
verum
end; given y,
z being
object such that A5:
x = [z,y]
and A6:
[y,z] in dom ([:A,B:] --> a)
;
x in dom ([:B,A:] --> a)A7:
y in A
by A6, ZFMISC_1:87;
z in B
by A6, ZFMISC_1:87;
then
x in [:B,A:]
by A5, A7, ZFMISC_1:87;
hence
x in dom ([:B,A:] --> a)
;
verum end;
now for y, z being object st [y,z] in dom ([:A,B:] --> a) holds
([:B,A:] --> a) . (z,y) = ([:A,B:] --> a) . (y,z)let y,
z be
object ;
( [y,z] in dom ([:A,B:] --> a) implies ([:B,A:] --> a) . (z,y) = ([:A,B:] --> a) . (y,z) )assume A8:
[y,z] in dom ([:A,B:] --> a)
;
([:B,A:] --> a) . (z,y) = ([:A,B:] --> a) . (y,z)then A9:
y in A
by ZFMISC_1:87;
z in B
by A8, ZFMISC_1:87;
hence ([:B,A:] --> a) . (
z,
y) =
a
by A9, FUNCOP_1:7, ZFMISC_1:87
.=
([:A,B:] --> a) . (
y,
z)
by A8, FUNCOP_1:7
;
verum end;
hence
~ ([:A,B:] --> a) = [:B,A:] --> a
by A1, FUNCT_4:def 2; verum