I am trying to prove the following equality of two formulas: $x,z$ are variables, $c$ is a constant and $t$ is a term.
$\alpha {t \over x}{z \over c} =\alpha {z \over c}{t' \over x} $,
with $t' = t {z \over c}$ and we also assume $z \notin var(\alpha,t)$.
$\alpha {z \over c}$ means we replace the constant c with the variable z and $\alpha {t \over x}$ means we replace the variable $x$ with the term $t$, whenever $x$ occurs free in the formula $\alpha$.
Intuitively, the equality is clear to me: if $c$ occurs in the term $t$, on the left side we then replace the term $t$ for x and afterwards we replace $z$ for the constant $c$, so that $c$ does not occur in the formula, anymore.
But if we go from the right side, we first replace $z$ for $c$ and because we have already replaced $z$ for $c$ we need to set $t' = t {z \over c}$, so that $c$ does not occur in the formula anymore.
But I have no idea how to formally prove this, since you cannot really work with the definition of the substitution (at least in my eyes...)