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 onto & g is onto holds
Gr2Iso (f,g) is onto
let f be Function of G1,H1; :: thesis: for g being Function of G2,H2 st f is onto & g is onto holds
Gr2Iso (f,g) is onto
let g be Function of G2,H2; :: thesis: ( f is onto & g is onto implies Gr2Iso (f,g) is onto )
assume that
A1: rng f = the carrier of H1 and
A2: rng g = the carrier of H2 ; :: according to FUNCT_2:def 3 :: thesis: Gr2Iso (f,g) is onto
set h = Gr2Iso (f,g);
thus rng (Gr2Iso (f,g)) c= the carrier of (product <*H1,H2*>) ; :: according to XBOOLE_0:def 10,FUNCT_2:def 3 :: thesis: the carrier of (product <*H1,H2*>) c= rng (Gr2Iso (f,g))
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of (product <*H1,H2*>) or a in rng (Gr2Iso (f,g)) )
assume a in the carrier of (product <*H1,H2*>) ; :: thesis: a in rng (Gr2Iso (f,g))
then consider x being Element of H1, y being Element of H2 such that
A3: a = <*x,y*> by Th1;
consider a2 being object such that
A4: a2 in dom g and
A5: g . a2 = y by A2, FUNCT_1:def 3;
consider a1 being object such that
A6: a1 in dom f and
A7: f . a1 = x by A1, FUNCT_1:def 3;
( dom (Gr2Iso (f,g)) = the carrier of (product <*G1,G2*>) & ( for g being Element of G1
for h being Element of G2 holds <*g,h*> in the carrier of (product <*G1,G2*>) ) ) by FUNCT_2:def 1;
then A8: <*a1,a2*> in dom (Gr2Iso (f,g)) by A6, A4;
then consider k1 being Element of G1, k2 being Element of G2 such that
A9: <*a1,a2*> = <*k1,k2*> and
A10: (Gr2Iso (f,g)) . <*a1,a2*> = <*(f . k1),(g . k2)*> by Def1;
( a1 = k1 & a2 = k2 ) by A9, FINSEQ_1:77;
hence a in rng (Gr2Iso (f,g)) by A3, A7, A5, A8, A10, FUNCT_1:def 3; :: thesis: verum