for S being non empty non void ManySortedSign
for U1, U2, U3 being non-empty MSAlgebra over S
for H being ManySortedFunction of U1,U2
for H1 being ManySortedFunction of U2,U3 st H is_isomorphism U1,U2 & H1 is_isomorphism U2,U3 holds
H1 ** H is_isomorphism U1,U3 by Th11, Th12;