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;
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 by FUNCT_2:def 3;
hence G,I are_isomorphic by A3, A4, Def22; :: thesis: verum