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