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 by A1, FINSEQ_1:77;
hence (Gr2Iso (f,g)) . <*x1,x2*> = <*(f . x1),(g . x2)*> by A1, A2, FINSEQ_1:77; :: thesis: verum