Thread: translation to relational symbol sets (From "Mathematical Logic" Ebbinghaus, et al)

if anyone has the book "Mathematical Logic" by Ebbinghaus, Flum and Thomas, I'd like to check if the pf of thm 1.3 on pg 117 is correct. I don't think it is. In the pf of part (a)we're not told anything about possible S-formulas where constant symbols appear. The pf of equivalence would be completely non-trivial when we have to deal with such formulas. Can someone tell me why it is that this case isn't treated?

The stipulation that term-reduced formulas will suffice still allows for constants to show up in S-formulas.