let A, x, y be set ; :: thesis: (A --> [x,y]) ~ = A --> [y,x]
A1: dom ((A --> [x,y]) ~) = dom (A --> [x,y]) by Def1;
then A2: dom ((A --> [x,y]) ~) = A by Th19;

A3: now

let z be set ; :: thesis: ( z in dom ((A --> [x,y]) ~) implies ((A --> [x,y]) ~) . z = (A --> [y,x]) . z )
assume A4: z in dom ((A --> [x,y]) ~) ; :: thesis: ((A --> [x,y]) ~) . z = (A --> [y,x]) . z
then (A --> [x,y]) . z = [x,y] by A2, Th13;
hence ((A --> [x,y]) ~) . z = [y,x] by A1, A4, Def1
.= (A --> [y,x]) . z by A2, A4, Th13 ;
:: thesis: verum

end;

dom ((A --> [x,y]) ~) = dom (A --> [y,x]) by A2, Th19;
hence (A --> [x,y]) ~ = A --> [y,x] by A3, FUNCT_1:2; :: thesis: verum