Proof of Part (1):
Firstly, we write the formula \(f\)  in Disjunctive Normal Form (DNF). We can then separate each clause into conjunctions of word equation literals and length constraint literals. By canonical constructions (see e.g. [1]}), we can replace the word equation literals with a single word equation atom (i.e. a positive occurrence of a word equation) without affecting the language expressed by \(x\) . Thus the language expressed by \(x\)  is a finite union of languages, each given by the solutions to a single word equation which adhere to the length constraint literals (projected onto the variable \(x\) ).
