for U1, U2, U3 being Universal_Algebra
for h being Function of U1,U2
for h1 being Function of U2,U3 st h is_isomorphism & h1 is_isomorphism holds
h1 * h is_isomorphism