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;
then A3: dom ((A --> [x,y]) ~ ) = dom (A --> [y,x]) by Th19;

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;

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