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