DEF-RCOMP.
Let $R$ and $S$ be binary relations. Then
\[S\circ R = \{(x,z)\in \operatorname{dom}R\times\operatorname{ran}S:(\exists y\in\operatorname{ran}R:x\,R\,y\land y\,S\,z)\}\]is also a binary relation and is called the composition of $R$ and $S$.
PROP-RCOMP-ID.
For any binary relation $R$,
\[R\circ\operatorname{id}_{\operatorname{dom}R} = \operatorname{id}_{\operatorname{ran}R}\circ R = R.\]
PROP-RCOMP-ASS. Associativity.
For any binary relations $R$, $S$ and $T$,
\[(R\circ S)\circ T = R\circ(S\circ T).\]
PROP-RCOMP-CV.
For any binary relations $R$ and $S$,
\[(R\circ S)^\intercal = S^\intercal\circ R^\intercal.\]