hereby :: thesis: ( not x in dom f implies ex b1 being set st b1 = {} )
assume x in dom f ; :: thesis: ex y being set st [x,y] in f
then consider y being object such that
A1: [x,y] in f by XTUPLE_0:def 12;
reconsider y = y as set by TARSKI:1;
take y = y; :: thesis: [x,y] in f
thus [x,y] in f by A1; :: thesis: verum
end;
thus ( not x in dom f implies ex b1 being set st b1 = {} ) ; :: thesis: verum