theorem :: TOPALG_4:2

for G1, G2, H1, H2 being non empty multMagma
for f being Function of G1,H1
for g being Function of G2,H2
for x1 being Element of G1
for x2 being Element of G2 holds (Gr2Iso (f,g)) . <*x1,x2*> = <*(f . x1),(g . x2)*>