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;

consider h1 being Homomorphism of H,I such that

A4: h1 is bijective by A2;

A5: rng h1 = the carrier of I by A4, FUNCT_2:def 3;

rng g = the carrier of H by A3, FUNCT_2:def 3;

then dom h1 = rng g by FUNCT_2:def 1;

then rng (h1 * g) = the carrier of I by A5, RELAT_1:28;

then h1 * g is onto ;

hence G,I are_isomorphic by A3, A4; :: thesis: verum

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;

consider h1 being Homomorphism of H,I such that

A4: h1 is bijective by A2;

A5: rng h1 = the carrier of I by A4, FUNCT_2:def 3;

rng g = the carrier of H by A3, FUNCT_2:def 3;

then dom h1 = rng g by FUNCT_2:def 1;

then rng (h1 * g) = the carrier of I by A5, RELAT_1:28;

then h1 * g is onto ;

hence G,I are_isomorphic by A3, A4; :: thesis: verum