let G1, G2, H1, H2 be non empty multMagma ; :: thesis: 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)*>
let f be Function of G1,H1; :: thesis: 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)*>
let g be Function of G2,H2; :: thesis: for x1 being Element of G1
for x2 being Element of G2 holds (Gr2Iso f,g) . <*x1,x2*> = <*(f . x1),(g . x2)*>
let x1 be Element of G1; :: thesis: for x2 being Element of G2 holds (Gr2Iso f,g) . <*x1,x2*> = <*(f . x1),(g . x2)*>
let x2 be Element of G2; :: thesis: (Gr2Iso f,g) . <*x1,x2*> = <*(f . x1),(g . x2)*>
consider y1 being Element of G1, y2 being Element of G2 such that
A1: <*y1,y2*> = <*x1,x2*> and
A2: (Gr2Iso f,g) . <*x1,x2*> = <*(f . y1),(g . y2)*> by Def1;
( x1 = y1 & x2 = y2 ) by A1, GROUP_7:2;
hence (Gr2Iso f,g) . <*x1,x2*> = <*(f . x1),(g . x2)*> by A2; :: thesis: verum