lemma2.1 - Define left inverse for f

Lemma 2.1 now gives us an instance of Inverse instead of Bijection.
Inverse seems to be more general.