consider a being set such that
A3: ( x in a & a in rng P ) by A1, A2, TARSKI:def 4;
ex y being set st
( y in dom P & a = P . y ) by A3, FUNCT_1:def 5;
hence ex b₁ being set st
( b₁ in dom P & x in P . b₁ ) by A3; :: thesis: verum