consider x being set such that
A2: x in dom f by A1, XBOOLE_0:def 1;
take f . x ; :: thesis: ex x being set st
( x in dom f & f . x = f . x )
thus ex x being set st
( x in dom f & f . x = f . x ) by A2; :: thesis: verum