let O be set ; 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; ( 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
; 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; verum