let O be set ; :: thesis: for G, H, I being GroupWithOperators of O st G,H are_isomorphic & H,I are_isomorphic holds
G,I are_isomorphic
let G, H, I be GroupWithOperators of O; :: 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, Def22;
consider h1 being Homomorphism of H,I such that
A4: h1 is bijective by A2, Def22;
( g is onto & g is one-to-one ) by A3;
then A5: ( rng g = the carrier of H & g is one-to-one ) by FUNCT_2:def 3;
( h1 is onto & h1 is one-to-one ) by A4;
then A6: ( rng h1 = the carrier of I & h1 is one-to-one ) by FUNCT_2:def 3;
dom h1 = rng g by A5, FUNCT_2:def 1;
then A7: rng (h1 * g) = the carrier of I by A6, RELAT_1:47;
h1 * g is one-to-one by A5, A6;
then ( h1 * g is onto & h1 * g is one-to-one ) by A7, FUNCT_2:def 3;
then h1 * g is bijective ;
hence G,I are_isomorphic by Def22; :: thesis: verum