let G1, G2, H1, H2 be non empty multMagma ; 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; 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; ( 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
; Gr2Iso (f,g) is one-to-one
let a, b be object ; FUNCT_1:def 4 ( 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))
; ( 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))
; ( 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
; 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; verum