When solving example in Banchilhon&Spyratos paper I found that view
equations technique is applicable for proving lemmas about functional
dependencies as well.

Suppose we have functional dependency

A.x->A.y

By "->" definition

for any tuples a1,a2 from A ( a1.x = a2.x implies a1.y != a2.y )

which can be equivalently rewritten as

not exists a1,a2 ( a1.x = a2.x & a1.y != a2.y )

which gives immediately view equation

(select from A a1, A a2
where a1.x = a2.x and a1.y != a2.y) = DUM

/* Equation #1 */

Note, that SQL pseudo syntax above has empty column expression list in
the select clause in order to match void column list in the DUM table.

We'll prove Armstrong transitivity lemma. In addition to the Equation
#1 we demand

A.y->A.z

or equivalently

(select from A a1, A a2
where a1.y = a2.y and a1.z != a2.z) = DUM

/* Equation #2 */

We are asked to evaluate

select from A a1, A a2
where a1.x = a2.x and a1.z != a2.z

If it equals to DUM, then A.x->A.z follows. In the first step we add a
tautological predicate

select from A a1, A a2
where a1.x = a2.x and a1.z != a2.z
and (a1.y = a2.y or a1.y != a2.y)

and rewrite it as a union

select from A a1, A a2
where a1.x = a2.x and a1.z != a2.z
and a1.y = a2.y
union
select from A a1, A a2
where a1.x = a2.x and a1.z != a2.z
and a1.y != a2.y

and reshuffle the predicates conveniently

select from A a1, A a2
where a1.y = a2.y and a1.z != a2.z
and a1.x = a2.x
union
select from A a1, A a2
where a1.x = a2.x and a1.y != a2.y
and a1.z != a2.z

Finally, we notice that the left side of the union is a stricter
version than the left side of Equation #1. In other words, it
evaluates to DUM. Likewise, the right side of the union evaluates to
DUM too. This gives DUM as a result. QED