let f be Function; :: thesis: for x, y being object st [y,x] in dom (~ f) holds
(~ f) . (y,x) = f . (x,y)
let x, y be object ; :: thesis: ( [y,x] in dom (~ f) implies (~ f) . (y,x) = f . (x,y) )
assume [y,x] in dom (~ f) ; :: thesis: (~ f) . (y,x) = f . (x,y)
then [x,y] in dom f by Th42;
hence (~ f) . (y,x) = f . (x,y) by Def2; :: thesis: verum