dom f <> {} by A1;
then consider x being set such that
A2: x in dom f by 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