let X, Y be set ; :: thesis: for f being Function of X,Y st Y <> {} & ex g being Function of Y,X st g * f = id X holds
f is one-to-one
let f be Function of X,Y; :: thesis: ( Y <> {} & ex g being Function of Y,X st g * f = id X implies f is one-to-one )
assume Y <> {} ; :: thesis: ( for g being Function of Y,X holds not g * f = id X or f is one-to-one )
then A1: dom f = X by Def1;
given g being Function of Y,X such that A2: g * f = id X ; :: thesis: f is one-to-one
thus f is one-to-one by A2, A1, FUNCT_1:31; :: thesis: verum