 Thus, from now on we can regard formula_69 as satisfying
which means (by definition of modular arithmetic) that

Recall the second assumption, “formula_74”, and remember that we are now in the scope of an implicit quantification for "i", so we don't repeat its quantification for each statement.The second assumption formula_75 implies that
Now by transitivity of equality we get

Our original goal was to prove that the definition
is good for achieving what we declared in the specification of formula_4