A theorem on the formalized arithmetic with function symbols ' and +
scientific article; zbMATH DE number 3608017