let f be Function; :: thesis: for x, X being set st x in dom f & f . x in f .: X & f is one-to-one holds
x in X
let x, X be set ; :: thesis: ( x in dom f & f . x in f .: X & f is one-to-one implies x in X )
assume A1: x in dom f ; :: thesis: ( not f . x in f .: X or not f is one-to-one or x in X )
assume f . x in f .: X ; :: thesis: ( not f is one-to-one or x in X )
then A2: ex a being object st
( a in dom f & a in X & f . x = f . a ) by FUNCT_1:def 6;
assume f is one-to-one ; :: thesis: x in X
hence x in X by A1, A2, FUNCT_1:def 4; :: thesis: verum