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

A1: now

let x be set ; :: thesis: ( ( x in dom ([:B,A:] --> a) implies ex y, z being set st
( x = [z,y] & [y,z] in dom ([:A,B:] --> a) ) ) & ( ex y, z being set st
( x = [z,y] & [y,z] in dom ([:A,B:] --> a) ) implies x in dom ([:B,A:] --> a) ) )

hereby :: thesis: ( ex y, z being set 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 set st
( x = [z,y] & [y,z] in dom ([:A,B:] --> a) )
then consider z, y being set such that
A2: ( z in B & y in A ) and
A3: x = [z,y] by ZFMISC_1:def 2;
take y = y; :: thesis: ex z being set 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 A3; :: thesis: [y,z] in dom ([:A,B:] --> a)
[y,z] in [:A,B:] by A2, ZFMISC_1:106;
hence [y,z] in dom ([:A,B:] --> a) by FUNCOP_1:19; :: thesis: verum

end;

given y, z being set such that A4: x = [z,y] and
A5: [y,z] in dom ([:A,B:] --> a) ; :: thesis: x in dom ([:B,A:] --> a)
( y in A & z in B ) by A5, ZFMISC_1:106;
then x in [:B,A:] by A4, ZFMISC_1:106;
hence x in dom ([:B,A:] --> a) by FUNCOP_1:19; :: thesis: verum

end;

now

let y, z be set ; :: thesis: ( [y,z] in dom ([:A,B:] --> a) implies ([:B,A:] --> a) . z,y = ([:A,B:] --> a) . y,z )
assume A6: [y,z] in dom ([:A,B:] --> a) ; :: thesis: ([:B,A:] --> a) . z,y = ([:A,B:] --> a) . y,z
then ( y in A & z in B ) by ZFMISC_1:106;
then [z,y] in [:B,A:] by ZFMISC_1:106;
hence ([:B,A:] --> a) . z,y = a by FUNCOP_1:13
.= ([:A,B:] --> a) . y,z by A6, FUNCOP_1:13 ;
:: thesis: verum

end;

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