The Wikipedia article on substitution states:
In first-order logic, a substitution is a total mapping $σ: V → T$ from variables to terms; many, but not all authors additionally require $σ(x) = x$ for all but finitely many variables $x$.
I really didn't understand the $\sigma(x)=x$ requirement. Does it mean that all variables that occur in the formula, the substitution is applied to, are substituted by themselves, if they are not in the domain of the substitution?