for U1, U2, U3 being Universal_Algebra
for h1 being Function of U1,U2
for h2 being Function of U2,U3
for a being FinSequence of U1 holds h2 * (h1 * a) = (h2 * h1) * a