Algebraic interpretation of derivation axioms completeness

The operation $(X\to Y)\blacktriangleright(Z\to V)=X\cup(Z\setminus Y)\to (Y\cup V)$ is determined in the full set $\{X\to Y\mid X,Y\subseteq R\}$ of F-dependences over a certain scheme $R$. Let $\Phi$ be an F-dependence, which follows from a set $F$ of F-dependences. We prove that $\Phi=\Phi_1\blacktriangleright\Phi_2\blacktriangleright\ldots \blacktriangleright\Phi_k\blacktriangleright W\cdot\mathbf{F2}\cdot\mathbf{B3}$ for some $\Phi_1,\Phi_2,\ldots,\Phi_k\in F$ and $W\subseteq R$, where $\Phi_k\blacktriangleright W=\Phi_k\blacktriangleright(W\to W)$. The unary operations $\cdot\mathbf{F2}$ and $\cdot\mathbf{B3}$ correspond to axioms of derivation $\mathbf{F2}$ (completion) and $\mathbf{B3}$ (projectivity) pro tanto.