Question about Regularly Algebraizable Logics I haven't found any posts related to Algebraic Logic, but I'll try anyway; here it is:
Some notions:
A logic is algebraizable when there is a class $K$ of algebras an there are structural Transformers $\tau,\rho$ (from formulas into equations and from equations into formulas, respectively) such that the following are satisfied, for all $\Gamma \cup \varphi \subseteq Fm$ and all $\Theta \cup$ $\{\epsilon \approx \delta\}\subseteq Eq$:
ALG1. $\Gamma \vdash_\mathcal{L} \varphi$  $\Longleftrightarrow$ $\tau\Gamma \models_K \tau\varphi$.
ALG2. $\Theta \models_K \epsilon \approx \delta$ $\Longleftrightarrow$ $\rho\Theta \vdash_\mathcal{L} \rho(\epsilon \approx \delta)$
ALG3. $\varphi \dashv \vdash_\mathcal{L} \rho \tau \varphi$.
ALG4. $\epsilon \approx \delta =\models_K \tau \rho(\epsilon \approx \delta)$.
In such a case, the class $K$ is said to be the equivalent algebraic semantics for $\mathcal{L}$.
A Logic is said to be regularly algebraizable when it is algebraizable and satisfies:
$({G})$   $x, y \vdash_{\mathcal{L}} \Delta(x,y)$  
for any non-empty set $\Delta(x,y)$ of equivalence formulas.
Here the problem:
Let $\mathcal{L}$ be regularly algebraizable, with equivalent algebraic semantics the class $K$.


*

*If $\varphi, \psi$ are any two theorems of $\mathcal{L}$, then $K\models \varphi \approx \psi$.

*If $\varphi$ is any theorem of $\mathcal{L}$, then $\varphi$ is an algebraic constant of the class ${K}$.


Any help would be really appreciated.
 A: Just for reference, you can find this result as Proposition 3.51 in the book Abstract Algebraic Logic. An Introductory Textbook, by J. M. Font.


*

*By (G), $\varphi,\psi \vdash_\mathcal{L} \Delta(\varphi,\psi)$, so from $\vdash_\mathcal{L} \varphi$ and $\vdash_\mathcal{L} \psi$ you obtain $\vdash_\mathcal{L} \Delta(\varphi,\psi)$, i.e., $\vdash_\mathcal{L} \rho(\varphi \approx \psi)$. Now apply (ALG2) to get $\models_\mathsf{K} \varphi \approx \psi$, which is equivalent to $\mathsf{K} \models \varphi \approx \psi$.

*Fix any $\mathbf{A} \in \mathsf{K}$, and let $h,h' \in \text{Hom}(\mathbf{Fm},\mathbf{A})$. You need to prove that $h(\varphi) = h'(\varphi)$. Let $\sigma$ be an injective substitution mapping every variable in $\varphi$ to a variable not ocurring in $\varphi$. Note that such a $\sigma$ exists because the set of variables is infinite and in $\varphi$ appear only finitely many variables. Then, define $h'' \in \text{Hom}(\mathbf{Fm},\mathbf{A})$ by setting $h''(x) := h(x)$ and $h''(\sigma(x)) := h'(x)$ for every variable $x$ occurring in $\varphi$. By structurality, $\sigma(\varphi)$ is also a theorem of $\mathcal{L}$ (it is just $\varphi$ but with the variables renamed), so by item 1 you have $h''(\varphi) = h''(\sigma(\varphi))$. And clearly $h(\varphi) = h''(\varphi)$ and $h'(\varphi) = h''(\sigma(\varphi))$ because $h$ and $h''$ agree on the variables of $\varphi$ and $h'$ and $h''$ agree on the variables of $\sigma(\varphi)$. Thus, $h(\varphi) = h'(\varphi)$.
