Анотація. Наведено нові доведення двох теорем безтипового екстенсіонального λ-числення: теореми Каррі про те, що будь-який λ-терм має βη-нормальну форму тоді й тільки тоді, коли він має βη-нормальну форму, та теореми нормалізації для βη-редукції. Даний підхід грунтується на двох широко відомих результатах: теоремі про відкладання η-редукції та властивості сильної нормалізовності η-редукції, які дозволяють природним чином розповсюдити деякі твердження зі звичайного λ-числення на екстенсіональний випадок.

Ключові слова: безтиповt екстенсіональнt λ-числення, відкладання η-редукції, теорема про βη-нормальну форму, теорема нормалізації для βη-редукції.