let G, H, I be Group; :: thesis: ( G,H are_isomorphic & H,I are_isomorphic implies G,I are_isomorphic )
assume that
A1: G,H are_isomorphic and
A2: H,I are_isomorphic ; :: thesis: G,I are_isomorphic
consider g being Homomorphism of G,H such that
A3: g is bijective by A1, Def15;
consider h1 being Homomorphism of H,I such that
A4: h1 is bijective by A2, Def15;
h1 * g is bijective by A3, A4, Th74;
hence G,I are_isomorphic by Def15; :: thesis: verum