let G1, G2, H1, H2 be non empty multMagma ; :: thesis: for f being Function of G1,H1
for g being Function of G2,H2 st f is one-to-one & g is one-to-one holds
Gr2Iso (f,g) is one-to-one
let f be Function of G1,H1; :: thesis: for g being Function of G2,H2 st f is one-to-one & g is one-to-one holds
Gr2Iso (f,g) is one-to-one
let g be Function of G2,H2; :: thesis: ( f is one-to-one & g is one-to-one implies Gr2Iso (f,g) is one-to-one )
assume that
A1: f is one-to-one and
A2: g is one-to-one ; :: thesis: Gr2Iso (f,g) is one-to-one
let a, b be object ; :: according to FUNCT_1:def 4 :: thesis: ( not a in proj1 (Gr2Iso (f,g)) or not b in proj1 (Gr2Iso (f,g)) or not (Gr2Iso (f,g)) . a = (Gr2Iso (f,g)) . b or a = b )
set h = Gr2Iso (f,g);
assume a in dom (Gr2Iso (f,g)) ; :: thesis: ( not b in proj1 (Gr2Iso (f,g)) or not (Gr2Iso (f,g)) . a = (Gr2Iso (f,g)) . b or a = b )
then consider a1 being Element of G1, a2 being Element of G2 such that
A3: a = <*a1,a2*> and
A4: (Gr2Iso (f,g)) . a = <*(f . a1),(g . a2)*> by Def1;
assume b in dom (Gr2Iso (f,g)) ; :: thesis: ( not (Gr2Iso (f,g)) . a = (Gr2Iso (f,g)) . b or a = b )
then consider b1 being Element of G1, b2 being Element of G2 such that
A5: b = <*b1,b2*> and
A6: (Gr2Iso (f,g)) . b = <*(f . b1),(g . b2)*> by Def1;
assume A7: (Gr2Iso (f,g)) . a = (Gr2Iso (f,g)) . b ; :: thesis: a = b
then ( dom f = the carrier of G1 & f . a1 = f . b1 ) by A4, A6, FINSEQ_1:77, FUNCT_2:def 1;
then A8: a1 = b1 by A1;
( dom g = the carrier of G2 & g . a2 = g . b2 ) by A4, A6, A7, FINSEQ_1:77, FUNCT_2:def 1;
hence a = b by A2, A3, A5, A8; :: thesis: verum