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