:: deftheorem Def1 defines Gr2Iso TOPALG_4:def 1 :
for G1, G2, H1, H2 being non empty multMagma
for f being Function of G1,H1
for g being Function of G2,H2
for b₇ being Function of (product <*G1,G2*>),(product <*H1,H2*>) holds
( b₇ = Gr2Iso (f,g) iff for x being Element of (product <*G1,G2*>) ex x1 being Element of G1 ex x2 being Element of G2 st
( x = <*x1,x2*> & b₇ . x = <*(f . x1),(g . x2)*> ) );