for G1, G2, H1, H2 being Group
for f being Homomorphism of G1,H1
for g being Homomorphism of G2,H2 st f is bijective & g is bijective holds
Gr2Iso (f,g) is bijective by Th4, Th3;