:: deftheorem defines are_isomorphic ENDALG:def 7 :
for G, H being non empty well-unital multLoopStr holds
( G,H are_isomorphic iff ex h being Homomorphism of G,H st h is bijective );