Theorem Function.bijective_iff_existsUnique

Modification history