let x, y be set ; :: thesis: for f being Function holds
( [x,y] in dom f iff [y,x] in dom (~ f) )
let f be Function; :: thesis: ( [x,y] in dom f iff [y,x] in dom (~ f) )
thus ( [x,y] in dom f implies [y,x] in dom (~ f) ) by Def2; :: thesis: ( [y,x] in dom (~ f) implies [x,y] in dom f )
assume [y,x] in dom (~ f) ; :: thesis: [x,y] in dom f
then consider x1, y1 being set such that
A1: [y,x] = [y1,x1] and
A2: [x1,y1] in dom f by Def2;
( x1 = x & y1 = y ) by A1, ZFMISC_1:33;
hence [x,y] in dom f by A2; :: thesis: verum