let A, B be set ; :: thesis: for a being object holds ~ ([:A,B:] --> a) = [:B,A:] --> a
let a be object ; :: thesis: ~ ([:A,B:] --> a) = [:B,A:] --> a

A1: now :: thesis: 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 ; :: thesis: ( ( 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 :: thesis: ( 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) ; :: thesis: 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; :: thesis: ex z being object st
( x = [z,y] & [y,z] in dom ([:A,B:] --> a) )
take z = z; :: thesis: ( x = [z,y] & [y,z] in dom ([:A,B:] --> a) )
thus x = [z,y] by A4; :: thesis: [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) ; :: thesis: verum

end;

given y, z being object such that A5: x = [z,y] and
A6: [y,z] in dom ([:A,B:] --> a) ; :: thesis: 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) ; :: thesis: verum

end;

now :: thesis: 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 ; :: thesis: ( [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) ; :: thesis: ([: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 ;
:: thesis: verum

end;

hence ~ ([:A,B:] --> a) = [:B,A:] --> a by A1, FUNCT_4:def 2; :: thesis: verum