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

A3: now

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

end;

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