y in rng f by A1, Th5;
then consider x being object such that
A2: ( x in dom f & f . x = y ) by FUNCT_1:def 3;
take x ; :: thesis: ( x is set & x in dom f & f . x = y )
thus ( x is set & x in dom f & f . x = y ) by A2; :: thesis: verum