let U1, U2, U3 be Universal_Algebra; :: thesis: ( U1,U2 are_isomorphic & U2,U3 are_isomorphic implies U1,U3 are_isomorphic )
assume U1,U2 are_isomorphic ; :: thesis: ( not U2,U3 are_isomorphic or U1,U3 are_isomorphic )
then consider f being Function of U1,U2 such that
A1: f is_isomorphism ;
assume U2,U3 are_isomorphic ; :: thesis: U1,U3 are_isomorphic
then consider g being Function of U2,U3 such that
A2: g is_isomorphism ;
g * f is_isomorphism by A1, A2, Th11;
hence U1,U3 are_isomorphic ; :: thesis: verum