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:42;
hence f . (x,y) = (~ f) . (y,x) by FUNCT_4:43; :: thesis: verum