:: deftheorem defines are_isomorphic GROUP_9:def 19 :
for O being set
for G, H being GroupWithOperators of O holds
( G,H are_isomorphic iff ex h being Homomorphism of G,H st h is bijective );