let S be non empty non void ManySortedSign ; :: thesis: for U1, U2, U3 being non-empty MSAlgebra of 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
let U1, U2, U3 be non-empty MSAlgebra of S; :: thesis: 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
let H be ManySortedFunction of U1,U2; :: thesis: 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
let H1 be ManySortedFunction of U2,U3; :: thesis: ( H is_isomorphism U1,U2 & H1 is_isomorphism U2,U3 implies H1 ** H is_isomorphism U1,U3 )
assume A1: ( H is_isomorphism U1,U2 & H1 is_isomorphism U2,U3 ) ; :: thesis: H1 ** H is_isomorphism U1,U3
then ( H is_epimorphism U1,U2 & H1 is_epimorphism U2,U3 ) by Def12;
then A2: H1 ** H is_epimorphism U1,U3 by Th11;
( H is_monomorphism U1,U2 & H1 is_monomorphism U2,U3 ) by A1, Def12;
then H1 ** H is_monomorphism U1,U3 by Th12;
hence H1 ** H is_isomorphism U1,U3 by A2, Def12; :: thesis: verum