theorem :: FUNCOP_1:20

for A, y being set
for x being object holds (A --> [x,y]) ~ = A --> [y,x]