Из пустого множества в пустое ровно одна - тождественная - функция есть и она биективна, поэтому доказательство весьма строгое.
А почему нельзя рассмотреть функцию из пустого множества в непустое?
Можно. Берёте Haskell, там есть тип Void, имеющим множеством значений пустое множество, и одна-единственная функция absurd из Void в любой другой тип, в том числе и в Void. Всё очень осязаемо.
Функции из войда в невойд по идее быть не должно, т.к. число таких фунций будет

А я-то думал, когда же тут до разборок с

дело дойдет. Ну теперь, видимо, не раньше чем через месяц
Лучшее доказательство которое я видел
