Речь идёт про равенство

, где в левой части

обозначает некоторую функцию одной переменной, по которой идёт интегрирование, а в правой части

обозначает функцию от

.
Так здесь целая теорема спрятана, причем нетривиальная.
Я бы её сформулировал так:
Через

я буду обозначать бесконечно малую по той базе, которая указана под именем функции.
Теорема:
Пусть есть функция

, определенная в точке

и в некоторой её (возможно, полу-)окрестности

, причем

(т.е. она непрерывна в

). Так же она интегрируема в этой (возможно, полу-)окрестности. Это значит, что

Тогда:

Доказательство:
Опять буду делать по определению предела.
Выберем произвольный

. Т.к.

непрерывна в

, это значит, что

такая, что для любых

таких, что

и при которых

определена, выполняется

. Выберем произвольный

такой, что как отрезок он является подмножеством области определения нашей альфы, и

.
Из двойного неравенства для альфы получаем следующее:


А дальше все то же самое, что и в предыдущем доказательстве.
Учитывая
получаем, что

а значит (см (2) ):

что и доказывает нужное нам утверждение.
Дргими словами, если обозначить за

то получаем, что

что и требовалось доказать.
По итогу, это равенство просто маскирует в себе всю содержательную часть предыдущего доказательства. Через супремум/инфимум тоже наверное можно, но вряд ли будет сильно уж проще.
И если посмотреть на доказательство (любое из двух), видно, что от всей этой ерунды с контролем областей определения пока избавиться не получается.
Мат.анализ на уровне 18 века.
Ну да, мне нужен анализ с актуальными бесконечно малыми и без пределов. Но без логических вывертов, как в нестандартном анализе или SDG. Или хотя бы какая-то техника, позволяющая нормально делать обычный мат.анализ без постоянного контроля областей определения.
обоснование допустимости перестановки предельных переходов
Если нету пределов, то и таких теорем тоже нету.
Вы все эти теоремы просто к формализму свести хотите?
В определенном смысле да. Я хочу сузить класс функций, но получить гладкость преобразований. Чтобы, например, была возможность алгоритмически определять корректность областей определения. Иными словами, есть у меня функция

. Я пишу

И я не хочу постоянно проверять, корректно ли брать предел по такой-то базе для такой-то функции. Т.е. чтобы если я попытался взять, например,

то компилятор бы подсветил мне, что такой переход делать нельзя.