Wikipedia's Sequent Calculus article defines substitution in LK sequent calculus like this:
$A[t/x]$ denotes the formula that is obtained by substituting the term $t$ for every free occurrence of the variable $x$ in formula $A$ with the restriction that the term $t$ must be free for the variable $x$ in $A$ (i.e., no occurrence of any free$^1$ variable in $t$ becomes bound in $A[t/x]$).
Does a slightly modified version of the above paragraph work as a definition for substitution in lambda calculus. Maybe the following:
$A[t/x]$ denotes the term that is obtained by substituting the term $t$ for every free occurrence of the variable $x$ in term $A$ with the restriction no occurrence of any free variable in $t$ becomes bound in $A[t/x]$).
$^1$ In sequent calculus, terms have no quantifier or any other kind of binder, so all variables in $t$ are free (in $t$), by definition. See @Taroccoesbrocco's answer to a related question.
Best Answer
Yes, your definition of substitution in the $\lambda$-calculus works fine. It is crucial to mention "free" in the definition of substitution in the $\lambda$-calculus, when it says "no occurrence of any free variable in $t$ becomes bound in $A[t/x]$", because a $\lambda$-term $t$ may contain binders and the restriction takes care only of the free variables of $t$.
On the contrary, as I said here, in the definition of substitution in sequent calculus (and more generally, in languages for first-order logic) there is no need to mention "free" when it says "no occurrence of any free variable in $t$ becomes bound in $A[t/x]$", because terms do not have binders and so any variable in $t$ is necessarily free.
There are at least two crucial differences between sequent calculus (and more generally, languages for first-order logic) and the $\lambda$-calculus.
In the language for first-order logic, there are two kinds of expressions, formulas and terms, which are well distinct from a syntactic and semantic point of view. In the $\lambda$-calculus, there is only one kind of expressions, $\lambda$-terms.
In the language for first-order logic, formulas may have binders for variables, but terms do not have any binders, so variables in a term are always free (if we consider the term alone). In the $\lambda$-calculus, instead, $\lambda$-terms may have binders, called $\lambda$-abstractions, and so a $\lambda$-term may have free and bound variables.