let z be object ; :: thesis: for X, Y being set holds ~ ([:X,Y:] --> z) = [:Y,X:] --> z
let X, Y be set ; :: thesis: ~ ([:X,Y:] --> z) = [:Y,X:] --> z
A1: dom ([:X,Y:] --> z) = [:X,Y:] ;
then A2: dom (~ ([:X,Y:] --> z)) = [:Y,X:] by FUNCT_4:46;

A3: now :: thesis: for x being object st x in [:Y,X:] holds
(~ ([:X,Y:] --> z)) . x = ([:Y,X:] --> z) . x

let x be object ; :: 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 object 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:7;
([:Y,X:] --> z) . (y2,y1) = z by A4, A5, FUNCOP_1:7;
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;

thus ~ ([:X,Y:] --> z) = [:Y,X:] --> z by A2, A3; :: thesis: verum