for G1, G2, H1, H2 being non empty multMagma
for f being Function of G1,H1
for g being Function of G2,H2 st f is one-to-one & g is one-to-one holds
Gr2Iso (f,g) is one-to-one