let f be Function; :: thesis: for x, y being object holds
( [x,y] in dom f iff [y,x] in dom (~ f) )
let x, y be object ; :: 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 object such that
A1: [y,x] = [y1,x1] and
A2: [x1,y1] in dom f by Def2;
x1 = x by A1, XTUPLE_0:1;
hence [x,y] in dom f by A1, A2, XTUPLE_0:1; :: thesis: verum