consider f being empty Function;
take f ; :: thesis: f is one-to-one
thus f is one-to-one ; :: thesis: verum