let C, A, B be non empty set ; :: thesis: 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
let f be Function of [:A,B:],C; :: thesis: for x being Element of A
for y being Element of B holds f . x,y = (~ f) . y,x
let x be Element of A; :: thesis: for y being Element of B holds f . x,y = (~ f) . y,x
let y be Element of B; :: thesis: f . x,y = (~ f) . y,x
dom f = [:A,B:] by FUNCT_2:def 1;
then [x,y] in dom f ;
then [y,x] in dom (~ f) by FUNCT_4:43;
hence f . x,y = (~ f) . y,x by FUNCT_4:44; :: thesis: verum