let y, x be set ; :: thesis: for f being Function st [y,x] in dom (~ f) holds
(~ f) . (y,x) = f . (x,y)
let f be Function; :: 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 Th43;
hence (~ f) . (y,x) = f . (x,y) by Def2; :: thesis: verum