What is the definition of "a derivation of a sequent "?

In Chapter IV. A Sequent Calculus in Ebbinghaus’ Mathematical Logic, a sequent is defined as:

If we call a nonempty list (sequence) of formulas a sequent, then we can use sequents to describe "stages in a proof". For instance, the "stage" with assumptions $phi_1,dots,phi_n$
and claim $phi$ is rendered by the sequent $phi_1dots phi_n phi$. The sequence $phi_1 dotsphi_n$ is called the antecedent and $phi$ the succedent of the sequent $phi_1dots phi_n phi$.

and a sequent is defined to be derivable:

If, in the calculus $mathfrak{S}$, there is a derivation of the sequent $Gamma phi$, then we write
$vdash Gamma phi$ and say that $Gamma phi$ is derivable.

1.1 Definition. A formula $phi$ is formally provable or derivable from a set $Phi$
of formulas (written: $Phi vdash phi$) if and only if there are finitely many formulas
$phi_1,dots,phi_n$ in $Phi$ such that $vdash phi_1 dotsphi_n phi$

Question: What is the definition of "a derivation of the sequent $Gamma phi$"? (Has it been defined in the book?)

Is "a derivation of the sequent $Gamma phi$" defined as a sequence of sequents, where

• the first sequent can be derived from an inference rule which has no sequent in their assumption parts, and
• each following sequent follows from some previous sequents by some inference rule?

Thanks.

---

The book gives rules of inference

We divide the rules of the sequent calculus $mathfrak{S}$ into the following categories:
structural rules (2.1, 2.2), connective rules (2.3, 2.4, 2.5, 2.6), quantifier
rules (4.1,4.2) and equality rules (4.3,4.4).

All the inference rules have the form of

$$ frac{sequent}{sequent} $$

except two inference rules which have no sequent in their assumption parts:

2.2 Assumption Rule (Assm).

$$ frac{}{Gamma phi} $$

if $phi$ is a member of $Gamma$.

and

4.3 Reflexivity Rule for Equality (==).

$$ frac{}{t==t} $$