let A, y be set ; :: thesis: for x being object holds (A --> [x,y]) ~ = A --> [y,x]
let x be object ; :: 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 ;

now :: thesis: for z being object st z in dom ((A --> [x,y]) ~) holds
((A --> [x,y]) ~) . z = (A --> [y,x]) . z

let z be object ; :: 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, Th7;
hence ((A --> [x,y]) ~) . z = [y,x] by A1, A4, Def1
.= (A --> [y,x]) . z by A2, A4, Th7 ;
:: thesis: verum

end;

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