let X, Y, x be set ; :: thesis: for f being Function of X,Y st Y <> {} & f is one-to-one & x in X holds
(f " ) . (f . x) = x
let f be Function of X,Y; :: thesis: ( Y <> {} & f is one-to-one & x in X implies (f " ) . (f . x) = x )
assume Y <> {} ; :: thesis: ( not f is one-to-one or not x in X or (f " ) . (f . x) = x )
then dom f = X by Def1;
hence ( not f is one-to-one or not x in X or (f " ) . (f . x) = x ) by FUNCT_1:56; :: thesis: verum