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 U1,U2 by Def5;
assume U2,U3 are_isomorphic ; :: thesis: U1,U3 are_isomorphic
then consider g being Function of U2,U3 such that
A2: g is_isomorphism U2,U3 by Def5;
g * f is_isomorphism U1,U3 by A1, A2, Th12;
hence U1,U3 are_isomorphic by Def5; :: thesis: verum