theorem :: MOD_4:1

for A, B, C being non empty set
for f being Function of [:A,B:],C
for x being Element of A
for y being Element of B holds f . (x,y) = (~ f) . (y,x) by FUNCT_4:def 8;