let X, Y, z be set ; :: thesis: ~ ([:X,Y:] --> z) = [:Y,X:] --> z
A1: ( dom ([:X,Y:] --> z) = [:X,Y:] & dom ([:Y,X:] --> z) = [:Y,X:] ) by FUNCOP_1:19;
then A2: dom (~ ([:X,Y:] --> z)) = [:Y,X:] by FUNCT_4:47;

now

let x be set ; :: thesis: ( x in [:Y,X:] implies (~ ([:X,Y:] --> z)) . x = ([:Y,X:] --> z) . x )
assume A3: x in [:Y,X:] ; :: thesis: (~ ([:X,Y:] --> z)) . x = ([:Y,X:] --> z) . x
then consider y1, y2 being set such that
A4: ( x = [y2,y1] & [y1,y2] in [:X,Y:] ) by A1, A2, FUNCT_4:def 2;
( ([:X,Y:] --> z) . y1,y2 = z & ([:Y,X:] --> z) . y2,y1 = z ) by A3, A4, FUNCOP_1:13;
then (~ ([:X,Y:] --> z)) . y2,y1 = ([:Y,X:] --> z) . y2,y1 by A1, A4, FUNCT_4:def 2;
hence (~ ([:X,Y:] --> z)) . x = ([:Y,X:] --> z) . x by A4; :: thesis: verum

end;

hence ~ ([:X,Y:] --> z) = [:Y,X:] --> z by A1, A2, FUNCT_1:9; :: thesis: verum